idp_engine.Annotate¶
Methods to annotate the Abstract Syntax Tree (AST) of an IDP-Z3 program.
- get_instantiables(self, interpretations, extensions, for_explain=False)[source]
compute Definition.instantiables, with level-mapping if definition is inductive
Uses implications instead of equivalence if for_explain is True
Example: { p() <- q(). p() <- r().} Result when not for_explain: p() <=> q() | r() Result when for_explain : p() <= q(). p() <= r(). p() => (q() | r()).
- Parameters
for_explain (Bool) – Use implications instead of equivalence, for rule-specific explanations
interpretations (Dict[str, idp_engine.Parse.SymbolInterpretation]) –
extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –
- Return type
Dict[idp_engine.Parse.SymbolDeclaration, List[idp_engine.Expression.Expression]]
- rename_args(self, new_vars)[source]
for Clark’s completion input : ‘!v: f(args) <- body(args)’ output: ‘!nv: f(nv) <- nv=args & body(args)’