idp_engine.Interpret

Methods to ground / interpret a theory in a data structure

• expand quantifiers

• replace symbols interpreted in the structure by their interpretation

• instantiate definitions

This module monkey-patches the ASTNode class and sub-classes.

( see docs/zettlr/Substitute.md )

interpret(self, problem, subs)

expand quantifiers and replace symbols interpreted in the structure by their interpretation

Parameters

• self (Expression) – the expression to be interpreted

• problem (Optional[Theory]) – the theory to be applied

• subs (dict[str, Expression]) – a dictionary mapping variable names to their value

Returns

the interpreted expression

Return type

Expression

get_supersets(self, problem)

determine the domain of the variables, if possible, and add filter to the quantified expression if needed

Parameters

• self (AQuantification | AAggregate) –

• problem (Optional[Theory]) –