|
| user_propagator_base (context &c) |
|
| user_propagator_base (solver *s) |
|
virtual void | push ()=0 |
|
virtual void | pop (unsigned num_scopes)=0 |
|
virtual | ~user_propagator_base () |
|
context & | ctx () |
|
virtual user_propagator_base * | fresh (context &ctx)=0 |
| user_propagators created using fresh() are created during search and their lifetimes are restricted to search time. They should be garbage collected by the propagator used to invoke fresh() . The life-time of the Z3_context object can only be assumed valid during callbacks, such as fixed() , which contains expressions based on the context.
|
|
void | register_fixed (fixed_eh_t &f) |
| register callbacks. Callbacks can only be registered with user_propagators that were created using a solver.
|
|
void | register_fixed () |
|
void | register_eq (eq_eh_t &f) |
|
void | register_eq () |
|
void | register_final (final_eh_t &f) |
| register a callback on final-check. During the final check stage, all propagations have been processed. This is an opportunity for the user-propagator to delay some analysis that could be expensive to perform incrementally. It is also an opportunity for the propagator to implement branch and bound optimization.
|
|
void | register_final () |
|
void | register_created (created_eh_t &c) |
|
void | register_created () |
|
void | register_decide (decide_eh_t &c) |
|
void | register_decide () |
|
virtual void | fixed (expr const &, expr const &) |
|
virtual void | eq (expr const &, expr const &) |
|
virtual void | final () |
|
virtual void | created (expr const &) |
|
virtual void | decide (expr const &, unsigned, bool) |
|
bool | next_split (expr const &e, unsigned idx, Z3_lbool phase) |
|
void | add (expr const &e) |
| tracks e by a unique identifier that is returned by the call.
|
|
void | conflict (expr_vector const &fixed) |
|
void | conflict (expr_vector const &fixed, expr_vector const &lhs, expr_vector const &rhs) |
|
bool | propagate (expr_vector const &fixed, expr const &conseq) |
|
bool | propagate (expr_vector const &fixed, expr_vector const &lhs, expr_vector const &rhs, expr const &conseq) |
|
Definition at line 4291 of file z3++.h.
void add |
( |
expr const & | e | ) |
|
|
inline |
tracks e
by a unique identifier that is returned by the call.
If the fixed()
callback is registered and if e
is a Boolean or Bit-vector, the fixed()
callback gets invoked when e
is bound to a value. If the eq()
callback is registered, then equalities between registered expressions are reported. A consumer can use the propagate
or conflict
functions to invoke propagations or conflicts as a consequence of these callbacks. These functions take a list of identifiers for registered expressions that have been fixed. The list of identifiers must correspond to already fixed values. Similarly, a list of propagated equalities can be supplied. These must correspond to equalities that have been registered during a callback.
Definition at line 4527 of file z3++.h.
4527 {
4528 if (cb)
4530 else if (s)
4532 else
4533 assert(false);
4534 }
void Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
void Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
Referenced by Solver::__iadd__().
Definition at line 4390 of file z3++.h.
4390 {
4391 return c ? *c : s->
ctx();
4392 }
Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), AstMap::__contains__(), AstRef::__copy__(), AstVector::__copy__(), FuncInterp::__copy__(), Goal::__copy__(), ModelRef::__copy__(), AstMap::__deepcopy__(), AstRef::__deepcopy__(), AstVector::__deepcopy__(), Datatype::__deepcopy__(), FuncEntry::__deepcopy__(), FuncInterp::__deepcopy__(), Goal::__deepcopy__(), ModelRef::__deepcopy__(), ParamDescrsRef::__deepcopy__(), ParamsRef::__deepcopy__(), Statistics::__deepcopy__(), AstMap::__del__(), AstRef::__del__(), AstVector::__del__(), Context::__del__(), FuncEntry::__del__(), FuncInterp::__del__(), Goal::__del__(), ModelRef::__del__(), ParamDescrsRef::__del__(), ParamsRef::__del__(), ScopedConstructor::__del__(), ScopedConstructorList::__del__(), Solver::__del__(), Statistics::__del__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), AstMap::__getitem__(), AstVector::__getitem__(), ModelRef::__getitem__(), Statistics::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), AstMap::__len__(), AstVector::__len__(), ModelRef::__len__(), Statistics::__len__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), ArithRef::__mul__(), BitVecRef::__mul__(), BoolRef::__mul__(), ExprRef::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), AstMap::__repr__(), ParamDescrsRef::__repr__(), ParamsRef::__repr__(), Statistics::__repr__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), BitVecRef::__rxor__(), AstMap::__setitem__(), AstVector::__setitem__(), ArithRef::__sub__(), BitVecRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), user_propagator_base::add(), ExprRef::arg(), FuncEntry::arg_value(), FuncInterp::arity(), Goal::as_expr(), Solver::assert_and_track(), Goal::assert_exprs(), Solver::assert_exprs(), QuantifierRef::body(), Solver::check(), user_propagator_base::conflict(), user_propagator_base::conflict(), Goal::convert_model(), AstRef::ctx_ref(), ExprRef::decl(), ModelRef::decls(), ArrayRef::default(), RatNumRef::denominator(), Goal::depth(), Goal::dimacs(), FuncDeclRef::domain(), ArraySortRef::domain_n(), FuncInterp::else_value(), FuncInterp::entry(), AstMap::erase(), ModelRef::eval(), Goal::get(), ParamDescrsRef::get_documentation(), ModelRef::get_interp(), Statistics::get_key_value(), ParamDescrsRef::get_kind(), ParamDescrsRef::get_name(), ModelRef::get_sort(), ModelRef::get_universe(), Goal::inconsistent(), AstMap::keys(), Statistics::keys(), Solver::model(), SortRef::name(), user_propagator_base::next_split(), QuantifierRef::no_pattern(), FuncEntry::num_args(), FuncInterp::num_entries(), Solver::num_scopes(), ModelRef::num_sorts(), FuncDeclRef::params(), QuantifierRef::pattern(), AlgebraicNumRef::poly(), Solver::pop(), Goal::prec(), user_propagator_base::propagate(), user_propagator_base::propagate(), AstVector::push(), Solver::push(), QuantifierRef::qid(), ArraySortRef::range(), FuncDeclRef::range(), DatatypeSortRef::recognizer(), Context::ref(), user_propagator_base::register_created(), user_propagator_base::register_created(), user_propagator_base::register_decide(), user_propagator_base::register_decide(), user_propagator_base::register_eq(), user_propagator_base::register_eq(), user_propagator_base::register_final(), user_propagator_base::register_final(), user_propagator_base::register_fixed(), user_propagator_base::register_fixed(), AstMap::reset(), Solver::reset(), AstVector::resize(), ParamsRef::set(), Solver::set(), AstVector::sexpr(), Goal::sexpr(), ModelRef::sexpr(), Goal::size(), ParamDescrsRef::size(), QuantifierRef::skolem_id(), AstRef::translate(), AstVector::translate(), Goal::translate(), ModelRef::translate(), user_propagator_base::user_propagator_base(), ParamsRef::validate(), FuncEntry::value(), QuantifierRef::var_name(), and QuantifierRef::var_sort().