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. More...
e by a unique identifier that is returned by the call. More...
Definition at line 4291 of file z3++.h.
◆ user_propagator_base() [1/2]Definition at line 4374 of file z3++.h.
4374: s(
nullptr), c(&c) {}
◆ user_propagator_base() [2/2]Definition at line 4376 of file z3++.h.
4376: s(s), c(
nullptr) {
void Z3_API Z3_solver_propagate_init(Z3_context c, Z3_solver s, void *user_context, Z3_push_eh push_eh, Z3_pop_eh pop_eh, Z3_fresh_eh fresh_eh)
register a user-propagator with the solver.
◆ ~user_propagator_base()Definition at line 4383 of file z3++.h.
4384 for(
auto& subcontext : subcontexts) {
4385subcontext->detach();
◆ add() void add ( expr const & e ) inlinetracks 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.
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__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
◆ conflict() [1/2]Definition at line 4536 of file z3++.h.
4539array<Z3_ast> _fixed(
fixed);
virtual void fixed(expr const &, expr const &)
bool Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const *fixed, unsigned num_eqs, Z3_ast const *eq_lhs, Z3_ast const *eq_rhs, Z3_ast conseq)
propagate a consequence based on fixed values and equalities. A client may invoke it during the pro...
◆ conflict() [2/2]Definition at line 4543 of file z3++.h.
4545assert(lhs.size() == rhs.size());
4547array<Z3_ast> _fixed(
fixed);
4548array<Z3_ast> _lhs(lhs);
4549array<Z3_ast> _rhs(rhs);
◆ created() virtual void created ( expr const & ) inlinevirtual ◆ ctx()Definition at line 4390 of file z3++.h.
4391 returnc ? *c : s->
ctx();
Referenced by ArithRef::__add__(), BitVecRef::__add__(), FPRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), Probe::__call__(), AstMap::__contains__(), AstRef::__copy__(), Goal::__copy__(), AstVector::__copy__(), FuncInterp::__copy__(), ModelRef::__copy__(), Solver::__copy__(), AstRef::__deepcopy__(), Datatype::__deepcopy__(), ParamsRef::__deepcopy__(), ParamDescrsRef::__deepcopy__(), Goal::__deepcopy__(), AstVector::__deepcopy__(), AstMap::__deepcopy__(), FuncEntry::__deepcopy__(), FuncInterp::__deepcopy__(), ModelRef::__deepcopy__(), Statistics::__deepcopy__(), Solver::__deepcopy__(), Fixedpoint::__deepcopy__(), Optimize::__deepcopy__(), ApplyResult::__deepcopy__(), Simplifier::__deepcopy__(), Tactic::__deepcopy__(), Probe::__deepcopy__(), Context::__del__(), AstRef::__del__(), ScopedConstructor::__del__(), ScopedConstructorList::__del__(), ParamsRef::__del__(), ParamDescrsRef::__del__(), Goal::__del__(), AstVector::__del__(), AstMap::__del__(), FuncEntry::__del__(), FuncInterp::__del__(), ModelRef::__del__(), Statistics::__del__(), Solver::__del__(), Fixedpoint::__del__(), Optimize::__del__(), ApplyResult::__del__(), Simplifier::__del__(), Tactic::__del__(), Probe::__del__(), ParserContext::__del__(), ArithRef::__div__(), BitVecRef::__div__(), FPRef::__div__(), ExprRef::__eq__(), Probe::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), Probe::__ge__(), FPRef::__ge__(), SeqRef::__ge__(), AstVector::__getitem__(), SeqRef::__getitem__(), ModelRef::__getitem__(), Statistics::__getitem__(), ApplyResult::__getitem__(), AstMap::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), Probe::__gt__(), FPRef::__gt__(), SeqRef::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), Probe::__le__(), FPRef::__le__(), SeqRef::__le__(), CharRef::__le__(), AstVector::__len__(), AstMap::__len__(), ModelRef::__len__(), Statistics::__len__(), ApplyResult::__len__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), Probe::__lt__(), FPRef::__lt__(), SeqRef::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), BoolRef::__mul__(), ArithRef::__mul__(), BitVecRef::__mul__(), FPRef::__mul__(), ExprRef::__ne__(), Probe::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), FPRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), FPRef::__rdiv__(), ParamsRef::__repr__(), ParamDescrsRef::__repr__(), AstMap::__repr__(), Statistics::__repr__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), FPRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), FPRef::__rsub__(), BitVecRef::__rxor__(), AstVector::__setitem__(), AstMap::__setitem__(), ArithRef::__sub__(), BitVecRef::__sub__(), FPRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), user_propagator_base::add(), Simplifier::add(), Fixedpoint::add_cover(), ParserContext::add_decl(), Fixedpoint::add_rule(), Optimize::add_soft(), ParserContext::add_sort(), Tactic::apply(), AlgebraicNumRef::approx(), ExprRef::arg(), FuncEntry::arg_value(), FuncInterp::arity(), Goal::as_expr(), ApplyResult::as_expr(), FPNumRef::as_string(), Solver::assert_and_track(), Optimize::assert_and_track(), Goal::assert_exprs(), Solver::assert_exprs(), Fixedpoint::assert_exprs(), Optimize::assert_exprs(), Solver::assertions(), Optimize::assertions(), SeqRef::at(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), BoolSortRef::cast(), Solver::check(), Optimize::check(), user_propagator_base::conflict(), UserPropagateBase::conflict(), Solver::consequences(), DatatypeSortRef::constructor(), Goal::convert_model(), AstRef::ctx_ref(), UserPropagateBase::ctx_ref(), ExprRef::decl(), ModelRef::decls(), ArrayRef::default(), RatNumRef::denominator(), Goal::depth(), Goal::dimacs(), Solver::dimacs(), ArraySortRef::domain(), FuncDeclRef::domain(), ArraySortRef::domain_n(), FuncInterp::else_value(), FuncInterp::entry(), AstMap::erase(), ModelRef::eval(), FPNumRef::exponent(), FPNumRef::exponent_as_bv(), FPNumRef::exponent_as_long(), Solver::from_file(), Optimize::from_file(), Solver::from_string(), Optimize::from_string(), ParserContext::from_string(), Goal::get(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), ParamDescrsRef::get_documentation(), Fixedpoint::get_ground_sat_answer(), ModelRef::get_interp(), Statistics::get_key_value(), ParamDescrsRef::get_kind(), ParamDescrsRef::get_name(), Fixedpoint::get_num_levels(), Fixedpoint::get_rule_names_along_trace(), Fixedpoint::get_rules(), Fixedpoint::get_rules_along_trace(), ModelRef::get_sort(), ModelRef::get_universe(), Solver::help(), Fixedpoint::help(), Optimize::help(), Simplifier::help(), Tactic::help(), Solver::import_model_converter(), Goal::inconsistent(), Solver::interrupt(), CharRef::is_digit(), FPNumRef::isInf(), FPNumRef::isNaN(), FPNumRef::isNegative(), FPNumRef::isNormal(), FPNumRef::isPositive(), FPNumRef::isSubnormal(), FPNumRef::isZero(), AstMap::keys(), Statistics::keys(), SortRef::kind(), Optimize::maximize(), Optimize::minimize(), Solver::model(), Optimize::model(), SortRef::name(), FuncDeclRef::name(), Solver::next(), user_propagator_base::next_split(), QuantifierRef::no_pattern(), Solver::non_units(), FuncEntry::num_args(), FuncInterp::num_entries(), Solver::num_scopes(), ModelRef::num_sorts(), RatNumRef::numerator(), Optimize::objectives(), Solver::param_descrs(), Fixedpoint::param_descrs(), Optimize::param_descrs(), Simplifier::param_descrs(), Tactic::param_descrs(), FuncDeclRef::params(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), QuantifierRef::pattern(), AlgebraicNumRef::poly(), Optimize::pop(), Solver::pop(), Goal::prec(), Solver::proof(), user_propagator_base::propagate(), Solver::push(), Optimize::push(), AstVector::push(), QuantifierRef::qid(), Fixedpoint::query(), Fixedpoint::query_from_lvl(), FuncDeclRef::range(), ArraySortRef::range(), Solver::reason_unknown(), Fixedpoint::reason_unknown(), Optimize::reason_unknown(), DatatypeSortRef::recognizer(), Context::ref(), user_propagator_base::register_created(), user_propagator_base::register_decide(), user_propagator_base::register_eq(), user_propagator_base::register_final(), user_propagator_base::register_fixed(), Fixedpoint::register_relation(), AstMap::reset(), Solver::reset(), AstVector::resize(), Solver::root(), Solver::set(), Fixedpoint::set(), Optimize::set(), ParamsRef::set(), Solver::set_initial_value(), Optimize::set_initial_value(), Optimize::set_on_model(), Fixedpoint::set_predicate_representation(), Goal::sexpr(), AstVector::sexpr(), ModelRef::sexpr(), Solver::sexpr(), Fixedpoint::sexpr(), Optimize::sexpr(), ApplyResult::sexpr(), FPNumRef::sign(), FPNumRef::sign_as_bv(), FPNumRef::significand(), FPNumRef::significand_as_bv(), FPNumRef::significand_as_long(), ParamDescrsRef::size(), Goal::size(), QuantifierRef::skolem_id(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), FiniteDomainRef::sort(), FPRef::sort(), SeqRef::sort(), Solver::statistics(), Fixedpoint::statistics(), Optimize::statistics(), CharRef::to_bv(), CharRef::to_int(), Solver::to_smt2(), Fixedpoint::to_string(), Solver::trail(), Solver::trail_levels(), AstVector::translate(), FuncInterp::translate(), AstRef::translate(), Goal::translate(), ModelRef::translate(), Solver::translate(), Solver::units(), Solver::unsat_core(), Optimize::unsat_core(), Fixedpoint::update_rule(), user_propagator_base::user_propagator_base(), Simplifier::using_params(), ParamsRef::validate(), FuncEntry::value(), QuantifierRef::var_name(), and QuantifierRef::var_sort().
◆ decide() virtual void decide ( expr const & , unsigned , bool ) inlinevirtual ◆ eq() virtual void eq ( expr const & , expr const & ) inlinevirtual ◆ final() ◆ fixed() virtual void fixed ( expr const & , expr const & ) inlinevirtual ◆ fresh()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.
Definition at line 4508 of file z3++.h.
bool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)
◆ pop() ◆ propagate() [1/2] ◆ propagate() [2/2] ◆ push() ◆ register_created() [1/2] void register_created ( ) inlineDefinition at line 4473 of file z3++.h.
4474m_created_eh = [
this](expr
const& e) {
virtual void created(expr const &)
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh)
register a callback when a new expression with a registered function is used by the solver The regist...
◆ register_created() [2/2] void register_created ( created_eh_t & c ) inline ◆ register_decide() [1/2]Definition at line 4489 of file z3++.h.
4490m_decide_eh = [
this](expr val,
unsignedbit,
boolis_pos) {
4491 decide(val, bit, is_pos);
virtual void decide(expr const &, unsigned, bool)
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh)
register a callback when the solver decides to split on a registered expression. The callback may cha...
◆ register_decide() [2/2] void register_decide ( decide_eh_t & c ) inline ◆ register_eq() [1/2]Definition at line 4433 of file z3++.h.
4434m_eq_eh = [
this](expr
const& x, expr
const& y) {
virtual void eq(expr const &, expr const &)
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
◆ register_eq() [2/2] void register_eq ( eq_eh_t & f ) inline ◆ register_final() [1/2]Definition at line 4457 of file z3++.h.
4458m_final_eh = [
this]() {
void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh)
register a callback on final check. This provides freedom to the propagator to delay actions or imple...
◆ register_final() [2/2] void register_final ( final_eh_t & f ) inlineregister 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.
Definition at line 4450 of file z3++.h.
◆ register_fixed() [1/2]Definition at line 4417 of file z3++.h.
4418m_fixed_eh = [
this](expr
const&id, expr
const&e) {
void Z3_API Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh)
register a callback for when an expression is bound to a fixed value. The supported expression types ...
◆ register_fixed() [2/2] void register_fixed ( fixed_eh_t & f ) inlineregister callbacks. Callbacks can only be registered with user_propagators that were created using a solver.
Definition at line 4410 of file z3++.h.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4