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

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