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)[source]
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)[source]
determine the extent of the variables, if possible, and add a filter to the quantified expression if needed. This is used to ground quantification over unary predicates.
Example
type T := {1,2,3} p : T -> Bool // p is a subset of T !x in p: q(x)
The formula is equivalent to !x in T: p(x) => q(x). -> The superset of p is {1,2,3}, the filter is p(x). The grounding is (p(1)=>q(1)) & (p(2)=>q(2)) & (p(3)=>q(3))
If p is enumerated (p:={1,2}) in a structure, however, the superset is now {1,2} and there is no need for a filter. The grounding is q(1) & q(2)
- Result:
self.supersets is updated to contain the supersets self.sub_exprs are updated with the appropriate filters
- Parameters
self (AQuantification | AAggregate) –
problem (Optional[Theory]) –