Z3
 
Loading...
Searching...
No Matches
Public Member Functions | Data Fields | Protected Attributes
UserPropagateBase Class Reference

Public Member Functions

 __init__ (self, s, ctx=None)
 
 __del__ (self)
 
 ctx (self)
 
 ctx_ref (self)
 
 add_fixed (self, fixed)
 
 add_created (self, created)
 
 add_final (self, final)
 
 add_eq (self, eq)
 
 add_diseq (self, diseq)
 
 add_decide (self, decide)
 
 add_on_binding (self, binding)
 
 push (self)
 
 pop (self, num_scopes)
 
 fresh (self, new_ctx)
 
 add (self, e)
 
 next_split (self, t, idx, phase)
 
 propagate (self, e, ids, eqs=[])
 
 conflict (self, deps=[], eqs=[])
 

Data Fields

 solver = s
 
 fresh_ctx = None
 
 cb = None
 
 id = _prop_closures.insert(self)
 
 fixed = None
 
 final = None
 
 eq = None
 
 diseq = None
 
 decide = None
 
 created = None
 
 binding = None
 

Protected Attributes

 _ctx = None
 

Detailed Description

Definition at line 11973 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
s,
ctx = None )

Definition at line 11982 of file z3py.py.

11982 def __init__(self, s, ctx=None):
11983 assert s is None or ctx is None
11984 ensure_prop_closures()
11985 self.solver = s
11986 self._ctx = None
11987 self.fresh_ctx = None
11988 self.cb = None
11989 self.id = _prop_closures.insert(self)
11990 self.fixed = None
11991 self.final = None
11992 self.eq = None
11993 self.diseq = None
11994 self.decide = None
11995 self.created = None
11996 self.binding = None
11997 if ctx:
11998 self.fresh_ctx = ctx
11999 if s:
12000 Z3_solver_propagate_init(self.ctx_ref(),
12001 s.solver,
12002 ctypes.c_void_p(self.id),
12003 _user_prop_push,
12004 _user_prop_pop,
12005 _user_prop_fresh)
12006
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-propagator with the solver.

◆ __del__()

__del__ ( self)

Definition at line 12007 of file z3py.py.

12007 def __del__(self):
12008 if self._ctx:
12009 self._ctx.ctx = None
12010

Member Function Documentation

◆ add()

add ( self,
e )

Definition at line 12092 of file z3py.py.

12092 def add(self, e):
12093 if self._ctx:
12094 raise Z3Exception("context already initialized")
12095 if self.solver:
12096 Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
12097 else:
12098 Z3_solver_propagate_register_cb(self.ctx_ref(), ctypes.c_void_p(self.cb), e.ast)
12099
Z3_solver_propagate_register_cb
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...
Z3_solver_propagate_register
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...

◆ add_created()

add_created ( self,
created )

Definition at line 12029 of file z3py.py.

12029 def add_created(self, created):
12030 if self.created:
12031 raise Z3Exception("created callback already registered")
12032 if self._ctx:
12033 raise Z3Exception("context already initialized")
12034 if self.solver:
12035 Z3_solver_propagate_created(self.ctx_ref(), self.solver.solver, _user_prop_created)
12036 self.created = created
12037
Z3_solver_propagate_created
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...

◆ add_decide()

add_decide ( self,
decide )

Definition at line 12065 of file z3py.py.

12065 def add_decide(self, decide):
12066 if self.decide:
12067 raise Z3Exception("decide callback already registered")
12068 if self._ctx:
12069 raise Z3Exception("context already initialized")
12070 if self.solver:
12071 Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide)
12072 self.decide = decide
12073
Z3_solver_propagate_decide
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...

◆ add_diseq()

add_diseq ( self,
diseq )

Definition at line 12056 of file z3py.py.

12056 def add_diseq(self, diseq):
12057 if self.diseq:
12058 raise Z3Exception("diseq callback already registered")
12059 if self._ctx:
12060 raise Z3Exception("context already initialized")
12061 if self.solver:
12062 Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq)
12063 self.diseq = diseq
12064
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.

◆ add_eq()

add_eq ( self,
eq )

Definition at line 12047 of file z3py.py.

12047 def add_eq(self, eq):
12048 if self.eq:
12049 raise Z3Exception("eq callback already registered")
12050 if self._ctx:
12051 raise Z3Exception("context already initialized")
12052 if self.solver:
12053 Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq)
12054 self.eq = eq
12055
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.

◆ add_final()

add_final ( self,
final )

Definition at line 12038 of file z3py.py.

12038 def add_final(self, final):
12039 if self.final:
12040 raise Z3Exception("final callback already registered")
12041 if self._ctx:
12042 raise Z3Exception("context already initialized")
12043 if self.solver:
12044 Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final)
12045 self.final = final
12046
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...

◆ add_fixed()

add_fixed ( self,
fixed )

Definition at line 12020 of file z3py.py.

12020 def add_fixed(self, fixed):
12021 if self.fixed:
12022 raise Z3Exception("fixed callback already registered")
12023 if self._ctx:
12024 raise Z3Exception("context already initialized")
12025 if self.solver:
12026 Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
12027 self.fixed = fixed
12028
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 ...

◆ add_on_binding()

add_on_binding ( self,
binding )

Definition at line 12074 of file z3py.py.

12074 def add_on_binding(self, binding):
12075 if self.binding:
12076 raise Z3Exception("binding callback already registered")
12077 if self._ctx:
12078 raise Z3Exception("context already initialized")
12079 if self.solver:
12080 Z3_solver_propagate_on_binding(self.ctx_ref(), self.solver.solver, _user_prop_binding)
12081 self.binding = binding
12082
Z3_solver_propagate_on_binding
void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh on_binding_eh)
register a callback when the solver instantiates a quantifier. If the callback returns false,...

◆ conflict()

conflict ( self,
deps = [],
eqs = [] )

Definition at line 12119 of file z3py.py.

12119 def conflict(self, deps = [], eqs = []):
12120 self.propagate(BoolVal(False, self.ctx()), deps, eqs)

◆ ctx()

ctx ( self)

Definition at line 12011 of file z3py.py.

12011 def ctx(self):
12012 if self.fresh_ctx:
12013 return self.fresh_ctx
12014 else:
12015 return self.solver.ctx
12016

◆ ctx_ref()

ctx_ref ( self)

Definition at line 12017 of file z3py.py.

12017 def ctx_ref(self):
12018 return self.ctx().ref()
12019

◆ fresh()

fresh ( self,
new_ctx )

Definition at line 12089 of file z3py.py.

12089 def fresh(self, new_ctx):
12090 raise Z3Exception("fresh needs to be overwritten")
12091

◆ next_split()

next_split ( self,
t,
idx,
phase )

Definition at line 12105 of file z3py.py.

12105 def next_split(self, t, idx, phase):
12106 return Z3_solver_next_split(self.ctx_ref(), ctypes.c_void_p(self.cb), t.ast, idx, phase)
12107
Z3_solver_next_split
bool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)

◆ pop()

pop ( self,
num_scopes )

Definition at line 12086 of file z3py.py.

12086 def pop(self, num_scopes):
12087 raise Z3Exception("pop needs to be overwritten")
12088

◆ propagate()

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

Definition at line 12111 of file z3py.py.

12111 def propagate(self, e, ids, eqs=[]):
12112 _ids, num_fixed = _to_ast_array(ids)
12113 num_eqs = len(eqs)
12114 _lhs, _num_lhs = _to_ast_array([x for x, y in eqs])
12115 _rhs, _num_rhs = _to_ast_array([y for x, y in eqs])
12116 return Z3_solver_propagate_consequence(e.ctx.ref(), ctypes.c_void_p(
12117 self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
12118
Z3_solver_propagate_consequence
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...

◆ push()

push ( self)

Definition at line 12083 of file z3py.py.

12083 def push(self):
12084 raise Z3Exception("push needs to be overwritten")
12085

Field Documentation

◆ _ctx

_ctx = None
protected

Definition at line 11986 of file z3py.py.

◆ binding

binding = None

Definition at line 11996 of file z3py.py.

◆ cb

cb = None

Definition at line 11988 of file z3py.py.

◆ created

created = None

Definition at line 11995 of file z3py.py.

◆ decide

decide = None

Definition at line 11994 of file z3py.py.

◆ diseq

diseq = None

Definition at line 11993 of file z3py.py.

◆ eq

eq = None

Definition at line 11992 of file z3py.py.

Referenced by AstRef.__eq__(), and SortRef.cast().

◆ final

final = None

Definition at line 11991 of file z3py.py.

◆ fixed

fixed = None

Definition at line 11990 of file z3py.py.

◆ fresh_ctx

fresh_ctx = None

Definition at line 11987 of file z3py.py.

◆ id

id = _prop_closures.insert(self)

Definition at line 11989 of file z3py.py.

◆ solver

solver = s

Definition at line 11985 of file z3py.py.

Generated by doxygen 1.13.2