idp_engine.Annotate¶
Methods to annotate the Abstract Syntax Tree (AST) of an IDP-Z3 program.
-
get_instantiables
(self, 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
-
rename_args
(self, new_vars)[source] for Clark’s completion input : ‘!v: f(args) <- body(args)’ output: ‘!nv: f(nv) <- nv=args & body(args)’