user_propagator_base Class Reference

#include <z3++.h>

Public Member Functions
	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 ()
void	register_on_binding ()
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)
virtual bool	on_binding (expr const &, expr const &)
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)

Detailed Description

Definition at line 4741 of file z3++.h.

Constructor & Destructor Documentation

user_propagator_base() [1/2]

user_propagator_base ( context &  c )

inline

Definition at line 4836 of file z3++.h.

: s(nullptr), c(&c) {}

user_propagator_base() [2/2]

user_propagator_base ( solver *  s )

inline

Definition at line 4838 of file z3++.h.

                                       : s(s), c(nullptr) {
            Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
        }

~user_propagator_base()

virtual ~user_propagator_base ( )

inlinevirtual

Definition at line 4845 of file z3++.h.

                                        {
            for (auto& subcontext : subcontexts) {
                subcontext->detach(); // detach first; the subcontexts will be freed internally!
                delete subcontext;
            }
        }

Member Function Documentation

add()

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 4999 of file z3++.h.

                                {
            if (cb)
                Z3_solver_propagate_register_cb(ctx(), cb, e);
            else if (s)
                Z3_solver_propagate_register(ctx(), *s, e);
            else
                assert(false);
        }

Referenced by Solver::__iadd__().

conflict() [1/2]

void conflict ( expr_vector const &  fixed )

inline

Definition at line 5008 of file z3++.h.

                                                {
            assert(cb);
            expr conseq = ctx().bool_val(false);
            array<Z3_ast> _fixed(fixed);
            Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
        }

conflict() [2/2]

void conflict ( expr_vector const &  fixed, expr_vector const &  lhs, expr_vector const &  rhs  )

inline

Definition at line 5015 of file z3++.h.

                                                                                                {
            assert(cb);
            assert(lhs.size() == rhs.size());
            expr conseq = ctx().bool_val(false);
            array<Z3_ast> _fixed(fixed);
            array<Z3_ast> _lhs(lhs);
            array<Z3_ast> _rhs(rhs);
            Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
        }

created()

virtual void created ( expr const &  )

inlinevirtual

Definition at line 4974 of file z3++.h.

{}

Referenced by user_propagator_base::register_created().

ctx()

context & ctx ( )

inline

Definition at line 4852 of file z3++.h.

                       {
            return c ? *c : s->ctx();
        }

Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), AstMap::__contains__(), AstRef::__copy__(), Goal::__copy__(), AstVector::__copy__(), FuncInterp::__copy__(), ModelRef::__copy__(), AstRef::__deepcopy__(), Datatype::__deepcopy__(), ParamsRef::__deepcopy__(), ParamDescrsRef::__deepcopy__(), Goal::__deepcopy__(), AstVector::__deepcopy__(), AstMap::__deepcopy__(), FuncEntry::__deepcopy__(), FuncInterp::__deepcopy__(), ModelRef::__deepcopy__(), Statistics::__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__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), AstVector::__getitem__(), ModelRef::__getitem__(), Statistics::__getitem__(), AstMap::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), AstVector::__len__(), AstMap::__len__(), ModelRef::__len__(), Statistics::__len__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), BoolRef::__mul__(), ArithRef::__mul__(), BitVecRef::__mul__(), ExprRef::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), ParamsRef::__repr__(), ParamDescrsRef::__repr__(), AstMap::__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__(), AstVector::__setitem__(), AstMap::__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(), FiniteSetSortRef::cast(), 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(), ModelRef::project(), ModelRef::project_with_witness(), user_propagator_base::propagate(), user_propagator_base::propagate(), Solver::push(), AstVector::push(), QuantifierRef::qid(), FuncDeclRef::range(), ArraySortRef::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(), user_propagator_base::register_on_binding(), AstMap::reset(), Solver::reset(), AstVector::resize(), Solver::set(), ParamsRef::set(), Goal::sexpr(), AstVector::sexpr(), ModelRef::sexpr(), ParamDescrsRef::size(), Goal::size(), QuantifierRef::skolem_id(), AstVector::translate(), AstRef::translate(), Goal::translate(), ModelRef::translate(), ExprRef::update(), DatatypeRef::update_field(), user_propagator_base::user_propagator_base(), ParamsRef::validate(), FuncEntry::value(), QuantifierRef::var_name(), and QuantifierRef::var_sort().

decide()

virtual void decide ( expr const &  , unsigned  , bool    )

inlinevirtual

Definition at line 4976 of file z3++.h.

{}

Referenced by user_propagator_base::register_decide().

eq()

virtual void eq ( expr const &  , expr const &    )

inlinevirtual

Definition at line 4970 of file z3++.h.

{ }

Referenced by AstRef::__eq__(), SortRef::cast(), FiniteSetSortRef::cast(), and user_propagator_base::register_eq().

final()

virtual void final ( )

inlinevirtual

Definition at line 4972 of file z3++.h.

{ }

fixed()

virtual void fixed ( expr const &  , expr const &    )

inlinevirtual

Definition at line 4968 of file z3++.h.

{ }

Referenced by user_propagator_base::conflict(), user_propagator_base::conflict(), user_propagator_base::propagate(), user_propagator_base::propagate(), and user_propagator_base::register_fixed().

fresh()

virtual user_propagator_base * fresh ( context &  ctx )

pure virtual

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.

next_split()

bool next_split ( expr const &  e, unsigned  idx, Z3_lbool  phase  )

inline

Definition at line 4980 of file z3++.h.

                                                                     {
            assert(cb);
            return Z3_solver_next_split(ctx(), cb, e, idx, phase);
        }

on_binding()

virtual bool on_binding ( expr const &  , expr const &    )

inlinevirtual

Definition at line 4978 of file z3++.h.

{ return true; }

Referenced by user_propagator_base::register_on_binding().

pop()

virtual void pop ( unsigned  num_scopes )

pure virtual

Referenced by Solver::__exit__().

propagate() [1/2]

bool propagate ( expr_vector const &  fixed, expr const &  conseq  )

inline

Definition at line 5025 of file z3++.h.

                                                                     {
            assert(cb);
            assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
            array<Z3_ast> _fixed(fixed);
            return Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
        }

propagate() [2/2]

bool propagate ( expr_vector const &  fixed, expr_vector const &  lhs, expr_vector const &  rhs, expr const &  conseq  )

inline

Definition at line 5032 of file z3++.h.

                                           {
            assert(cb);
            assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
            assert(lhs.size() == rhs.size());
            array<Z3_ast> _fixed(fixed);
            array<Z3_ast> _lhs(lhs);
            array<Z3_ast> _rhs(rhs);
            
            return Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
        }

push()

virtual void push ( )

pure virtual

Referenced by Solver::__enter__().

register_created() [1/2]

void register_created ( )

inline

Definition at line 4935 of file z3++.h.

                                {
            m_created_eh = [this](expr const& e) {
                created(e);
            };
            if (s) {
                Z3_solver_propagate_created(ctx(), *s, created_eh);
            }
        }

register_created() [2/2]

void register_created ( created_eh_t &  c )

inline

Definition at line 4928 of file z3++.h.

                                               {
            m_created_eh = c;
            if (s) {
                Z3_solver_propagate_created(ctx(), *s, created_eh);
            }
        }

register_decide() [1/2]

void register_decide ( )

inline

Definition at line 4951 of file z3++.h.

                               {
            m_decide_eh = [this](expr val, unsigned bit, bool is_pos) {
                decide(val, bit, is_pos);
            };
            if (s) {
                Z3_solver_propagate_decide(ctx(), *s, decide_eh);
            }
        }

register_decide() [2/2]

void register_decide ( decide_eh_t &  c )

inline

Definition at line 4944 of file z3++.h.

                                             {
            m_decide_eh = c;
            if (s) {
                Z3_solver_propagate_decide(ctx(), *s, decide_eh);
            }
        }

register_eq() [1/2]

void register_eq ( )

inline

Definition at line 4895 of file z3++.h.

                           {
            m_eq_eh = [this](expr const& x, expr const& y) {
                eq(x, y);
            };
            if (s) {
                Z3_solver_propagate_eq(ctx(), *s, eq_eh);
            }
        }

register_eq() [2/2]

void register_eq ( eq_eh_t &  f )

inline

Definition at line 4888 of file z3++.h.

                                     {
            m_eq_eh = f;
            if (s) {
                Z3_solver_propagate_eq(ctx(), *s, eq_eh);
            }
        }

register_final() [1/2]

void register_final ( )

inline

Definition at line 4919 of file z3++.h.

                              {
            m_final_eh = [this]() {
                final();
            };
            if (s) {
                Z3_solver_propagate_final(ctx(), *s, final_eh);
            }
        }

register_final() [2/2]

void register_final ( final_eh_t &  f )

inline

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.

Definition at line 4912 of file z3++.h.

                                           {
            m_final_eh = f;
            if (s) {
                Z3_solver_propagate_final(ctx(), *s, final_eh);
            }
        }

register_fixed() [1/2]

void register_fixed ( )

inline

Definition at line 4879 of file z3++.h.

                              {
            m_fixed_eh = [this](expr const &id, expr const &e) {
                fixed(id, e);
            };
            if (s) {
                Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
            }
        }

register_fixed() [2/2]

void register_fixed ( fixed_eh_t &  f )

inline

register callbacks. Callbacks can only be registered with user_propagators that were created using a solver.

Definition at line 4872 of file z3++.h.

                                           {
            m_fixed_eh = f;
            if (s) {
                Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
            }
        }

register_on_binding()

void register_on_binding ( )

inline

Definition at line 4960 of file z3++.h.

                                   {
            m_on_binding_eh = [this](expr const& q, expr const& inst) {
                return on_binding(q, inst);
            };
            if (s) 
                Z3_solver_propagate_on_binding(ctx(), *s, on_binding_eh);
        }