user_propagator_base Class Reference

Public Member Functions
	user_propagator_base (Z3_context c)
	user_propagator_base (solver *s)
virtual void	push ()=0
virtual void	pop (unsigned num_scopes)=0
virtual	~user_propagator_base ()=default
virtual user_propagator_base *	fresh (Z3_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. More...
void	register_fixed (fixed_eh_t &f)
	register callbacks. Callbacks can only be registered with user_propagators that were created using a solver. More...
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. More...
void	register_final ()
virtual void	fixed (unsigned, expr const &)
virtual void	eq (unsigned, unsigned)
virtual void	final ()
unsigned	add (expr const &e)
	tracks e by a unique identifier that is returned by the call. More...
void	conflict (unsigned num_fixed, unsigned const *fixed)
void	propagate (unsigned num_fixed, unsigned const *fixed, expr const &conseq)
void	propagate (unsigned num_fixed, unsigned const *fixed, unsigned num_eqs, unsigned const *lhs, unsigned const *rhs, expr const &conseq)

Detailed Description

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

Constructor & Destructor Documentation

user_propagator_base ( Z3_context  c )

inline

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

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

user_propagator_base ( solver *  s )

inline

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

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

virtual ~user_propagator_base ( )

virtualdefault

Member Function Documentation

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

                                    {
            assert(s);
            return Z3_solver_propagate_register(ctx(), *s, e);
        }

void conflict ( unsigned  num_fixed, unsigned const *  fixed  )

inline

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

                                                                 {
            assert(cb);
            scoped_context _ctx(ctx());
            expr conseq = _ctx().bool_val(false);
            Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
        }

virtual void eq ( unsigned  , unsigned    )

inlinevirtual

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

Referenced by user_propagator_base::register_eq().

{ }

virtual void final ( )

inlinevirtual

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

{ }

virtual void fixed ( unsigned  , expr const &    )

inlinevirtual

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

Referenced by user_propagator_base::register_fixed().

{ }

virtual user_propagator_base* fresh ( Z3_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.

virtual void pop ( unsigned  num_scopes )

pure virtual

void propagate ( unsigned  num_fixed, unsigned const *  fixed, expr const &  conseq  )

inline

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

                                                                                      {
            assert(cb);
            assert(conseq.ctx() == ctx());
            Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
        }

void propagate ( unsigned  num_fixed, unsigned const *  fixed, unsigned  num_eqs, unsigned const *  lhs, unsigned const *  rhs, expr const &  conseq  )

inline

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

                                           {
            assert(cb);
            assert(conseq.ctx() == ctx());
            Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, num_eqs, lhs, rhs, conseq);
        }

virtual void push ( )

pure virtual

void register_eq ( eq_eh_t &  f )

inline

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

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

void register_eq ( )

inline

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

                           {
            assert(s);
            m_eq_eh = [this](unsigned x, unsigned y) {
                eq(x, y);
            };
            Z3_solver_propagate_eq(ctx(), *s, eq_eh);
        }

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

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

void register_final ( )

inline

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

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

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

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

void register_fixed ( )

inline

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

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