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()).


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)’