idp_engine.Interpret

Methods to ground / interpret a theory in a data structure

• expand quantifiers

• replace symbols interpreted in the structure by their interpretation

This module also includes methods to:

• substitute a node by another in an AST tree

• instantiate an expresion, i.e. replace a variable by a value

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

( see docs/zettlr/Substitute.md )

add_def_constraints(self, instantiables, problem, result)

result is updated with the constraints for this definition.

The instantiables (of the definition) are expanded in problem.

Parameters

• instantiables (Dict[SymbolDeclaration, list[Expression]]) – the constraints without the quantification

• problem (Theory) – contains the structure for the expansion/interpretation of the constraints

• result (Dict[SymbolDeclaration, Definition, list[Expression]]) – a mapping from (Symbol, Definition) to the list of constraints