Z3
Public Member Functions | Data Fields
UserPropagateBase Class Reference

Public Member Functions

def __init__ (self, s, ctx=None)
 
def __del__ (self)
 
def ctx (self)
 
def ctx_ref (self)
 
def add_fixed (self, fixed)
 
def add_final (self, final)
 
def add_eq (self, eq)
 
def add_diseq (self, diseq)
 
def push (self)
 
def pop (self, num_scopes)
 
def fresh (self)
 
def add (self, e)
 
def propagate (self, e, ids, eqs=[])
 
def conflict (self, ids)
 

Data Fields

 solver
 
 cb
 
 id
 
 fixed
 
 final
 
 eq
 
 diseq
 

Detailed Description

Definition at line 10588 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  s,
  ctx = None 
)

Definition at line 10597 of file z3py.py.

10597  def __init__(self, s, ctx = None):
10598  assert s is None or ctx is None
10600  self.solver = s
10601  self._ctx = None
10602  self.cb = None
10603  self.id = _prop_closures.insert(self)
10604  self.fixed = None
10605  self.final = None
10606  self.eq = None
10607  self.diseq = None
10608  if ctx:
10609  self._ctx = Context()
10610  Z3_del_context(self._ctx.ctx)
10611  self._ctx.ctx = ctx
10612  self._ctx.eh = Z3_set_error_handler(ctx, z3_error_handler)
10613  Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
10614  if s:
10615  Z3_solver_propagate_init(self.ctx_ref(),
10616  s.solver,
10617  ctypes.c_void_p(self.id),
10618  _user_prop_push,
10619  _user_prop_pop,
10620  _user_prop_fresh)
10621 

◆ __del__()

def __del__ (   self)

Definition at line 10622 of file z3py.py.

10622  def __del__(self):
10623  if self._ctx:
10624  self._ctx.ctx = None
10625 

Member Function Documentation

◆ add()

def add (   self,
  e 
)

Definition at line 10668 of file z3py.py.

10668  def add(self, e):
10669  assert self.solver
10670  assert not self._ctx
10671  return Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
10672 

◆ add_diseq()

def add_diseq (   self,
  diseq 
)

Definition at line 10653 of file z3py.py.

10653  def add_diseq(self, diseq):
10654  assert not self.diseq
10655  assert not self._ctx
10656  Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq)
10657  self.diseq = diseq
10658 

◆ add_eq()

def add_eq (   self,
  eq 
)

Definition at line 10647 of file z3py.py.

10647  def add_eq(self, eq):
10648  assert not self.eq
10649  assert not self._ctx
10650  Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq)
10651  self.eq = eq
10652 

◆ add_final()

def add_final (   self,
  final 
)

Definition at line 10641 of file z3py.py.

10641  def add_final(self, final):
10642  assert not self.final
10643  assert not self._ctx
10644  Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final)
10645  self.final = final
10646 

◆ add_fixed()

def add_fixed (   self,
  fixed 
)

Definition at line 10635 of file z3py.py.

10635  def add_fixed(self, fixed):
10636  assert not self.fixed
10637  assert not self._ctx
10638  Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
10639  self.fixed = fixed
10640 

◆ conflict()

def conflict (   self,
  ids 
)

Definition at line 10689 of file z3py.py.

10689  def conflict(self, ids):
10690  self.propagate(BoolVal(False, self.ctx()), ids, eqs=[])

◆ ctx()

def ctx (   self)

Definition at line 10626 of file z3py.py.

10626  def ctx(self):
10627  if self._ctx:
10628  return self._ctx
10629  else:
10630  return self.solver.ctx
10631 

Referenced by UserPropagateBase.conflict(), and UserPropagateBase.ctx_ref().

◆ ctx_ref()

def ctx_ref (   self)

Definition at line 10632 of file z3py.py.

10632  def ctx_ref(self):
10633  return self.ctx().ref()
10634 

Referenced by UserPropagateBase.add(), UserPropagateBase.add_diseq(), UserPropagateBase.add_eq(), UserPropagateBase.add_final(), and UserPropagateBase.add_fixed().

◆ fresh()

def fresh (   self)

Definition at line 10665 of file z3py.py.

10665  def fresh(self):
10666  raise Z3Exception("fresh needs to be overwritten")
10667 

◆ pop()

def pop (   self,
  num_scopes 
)

Definition at line 10662 of file z3py.py.

10662  def pop(self, num_scopes):
10663  raise Z3Exception("pop needs to be overwritten")
10664 

◆ propagate()

def propagate (   self,
  e,
  ids,
  eqs = [] 
)

Definition at line 10676 of file z3py.py.

10676  def propagate(self, e, ids, eqs = []):
10677  num_fixed = len(ids)
10678  _ids = (ctypes.c_uint * num_fixed)()
10679  for i in range(num_fixed):
10680  _ids[i] = ids[i]
10681  num_eqs = len(eqs)
10682  _lhs = (ctypes.c_uint * num_eqs)()
10683  _rhs = (ctypes.c_uint * num_eqs)()
10684  for i in range(num_eqs):
10685  _lhs[i] = eqs[i][0]
10686  _rhs[i] = eqs[i][1]
10687  Z3_solver_propagate_consequence(e.ctx.ref(), ctypes.c_void_p(self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
10688 

Referenced by UserPropagateBase.conflict().

◆ push()

def push (   self)

Definition at line 10659 of file z3py.py.

10659  def push(self):
10660  raise Z3Exception("push needs to be overwritten")
10661 

Field Documentation

◆ cb

cb

Definition at line 10602 of file z3py.py.

Referenced by UserPropagateBase.propagate().

◆ diseq

diseq

Definition at line 10607 of file z3py.py.

Referenced by UserPropagateBase.add_diseq().

◆ eq

eq

Definition at line 10606 of file z3py.py.

Referenced by AstRef.__eq__(), UserPropagateBase.add_eq(), SortRef.cast(), and BoolSortRef.cast().

◆ final

final

Definition at line 10605 of file z3py.py.

Referenced by UserPropagateBase.add_final().

◆ fixed

fixed

Definition at line 10604 of file z3py.py.

Referenced by UserPropagateBase.add_fixed().

◆ id

id

Definition at line 10603 of file z3py.py.

◆ solver

solver
Z3_solver_propagate_diseq
void Z3_API Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression dis-equalities.
z3py.UserPropagateBase.__init__
def __init__(self, s, ctx=None)
Definition: z3py.py:10597
z3py.UserPropagateBase.add_diseq
def add_diseq(self, diseq)
Definition: z3py.py:10653
Z3_del_context
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3518
z3py.ensure_prop_closures
def ensure_prop_closures()
Definition: z3py.py:10538
Z3_solver_propagate_init
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-properator with the solver.
z3py.UserPropagateBase.pop
def pop(self, num_scopes)
Definition: z3py.py:10662
Z3_solver_propagate_eq
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
z3py.UserPropagateBase.add_final
def add_final(self, final)
Definition: z3py.py:10641
z3py.UserPropagateBase.push
def push(self)
Definition: z3py.py:10659
Z3_set_ast_print_mode
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
Z3_solver_propagate_consequence
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback, unsigned num_fixed, unsigned const *fixed_ids, unsigned num_eqs, unsigned const *eq_lhs, unsigned const *eq_rhs, Z3_ast conseq)
propagate a consequence based on fixed values. This is a callback a client may invoke during the fixe...
z3py.UserPropagateBase.__del__
def __del__(self)
Definition: z3py.py:10622
z3py.UserPropagateBase.add_eq
def add_eq(self, eq)
Definition: z3py.py:10647
z3py.UserPropagateBase.ctx
def ctx(self)
Definition: z3py.py:10626
z3py.UserPropagateBase.ctx_ref
def ctx_ref(self)
Definition: z3py.py:10632
z3py.UserPropagateBase.conflict
def conflict(self, ids)
Definition: z3py.py:10689
Z3_solver_propagate_final
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...
z3py.BoolVal
def BoolVal(val, ctx=None)
Definition: z3py.py:1570
z3py.UserPropagateBase.add_fixed
def add_fixed(self, fixed)
Definition: z3py.py:10635
Z3_solver_propagate_register
unsigned 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...
Z3_set_error_handler
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
Z3_solver_propagate_fixed
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 ...
z3py.UserPropagateBase.propagate
def propagate(self, e, ids, eqs=[])
Definition: z3py.py:10676
z3py.UserPropagateBase.add
def add(self, e)
Definition: z3py.py:10668
z3py.UserPropagateBase.fresh
def fresh(self)
Definition: z3py.py:10665