idp_engine.Interpret¶
Methods to interpret a theory in a data structure
substitute a constant by its value in an expression
replace symbols interpreted in a structure by their interpretation
expand quantifiers
This module also includes methods to:
substitute an 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 )
-
idp_engine.Interpret.
add_def_constraints
(self, instantiables, problem, result)[source]¶ 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 (Problem) – 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