idp_engine.Annotate¶
Methods to annotate the Abstract Syntax Tree (AST) of an IDP-Z3 program.
-
idp_engine.Annotate.
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