Adds an axiom to the logical context.
Adds an axiom to the logical context. The axiom should always be a
tautology with respect to the theory. The axiom is guaranteed to be
maintained in all (backtracking) levels beyond the one where it is
asserted. Note that in the current version, calling
assertAxiom from within the following callbacks does not
work: newElem, newApp, push,
pop. It is strongly advised to call it from within the
following callbacks only: newEq, newDiseq,
newAssignment, finalCheck. It is unclear whether
this is a bug with Z3 or a feature.
Indicates to Z3 that in the model being built by the theory, two elements are equal.
Indicates to Z3 that in the model being built by the theory, two elements are equal.
Method that Z3 will call (if activated) to delete the theory.
Method that Z3 will call (if activated) to delete the theory. After that call, no more callbacks will be made by Z3.
Method that Z3 will call (if activated) just before Z3 starts building a model.
Returns an iterator over all theory function applications in the context.
Returns an iterator over all theory function applications in the context.
Returns an iterator over all theory elements in the context.
Returns an iterator over all theory elements in the context.
Returns an iterator over all elements of the equivalence class of a term.
Returns an iterator over all elements of the equivalence class of a term.
Returns an iterator over all terms that have a given term as a subtree.
Returns an iterator over all terms that have a given term as a subtree.
Method that Z3 will call (if activated) when it starts the search.
Method that Z3 will call (if activated) when an application of a theory function enters the context.
Method that Z3 will call (if activated) when a theory predicate is assigned to a truth value in the logical context.
Method that Z3 will call (if activated) when a theory predicate is assigned to a truth value in the logical context.
the predicate
its truth value in the context
Method that Z3 will call (if activated) when a disequality is concluded in the logical context.
Method that Z3 will call (if activated) when an element of a theory sort enters the context.
Method that Z3 will call (if activated) when an equality is concluded in the logical context.
Method that Z3 will call (if activated) when it backtracks a case-split.
Method that Z3 will call (if activated) when it creates a case-split (backtracking point).
Method that Z3 will call (if activated) to simplify an application of a theory function.
Method that Z3 will call (if activated) to simplify a (n-ary) disequality tree, when the operands are of a theory sort.
Method that Z3 will call (if activated) to simplify an equality tree, when the operands are of a theory sort.
Method that Z3 will call (if activated) to simplify an equality tree, when the operands are of a theory sort.
the left operand of the equality
the right operand of the equality
Method that Z3 will call (if activated) when the context is reset by the user.
Method that Z3 will call (if activated) when it restarts the search.
Use this function at construction time to set which callbacks should be used.
Use this function at construction time to set which callbacks should be used.
Displays all callbacks, with their arguments.
Displays all callbacks, with their arguments. Off by default.
whether callbacks should be printed out
This class is inherited to create user defined theories.
The class should be instantiated before anything is added to the
Z3Context, as constructing the class automatically registers the plugin with the context. The user can choose which callbacks to activate by callingsetCallbackswith the appropriate arguments at construction time. For debugging purposes, the methodshowCallbackscan be useful.