|
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) |
|
Definition at line 10588 of file z3py.py.
◆ __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
10603 self.id = _prop_closures.insert(self)
10609 self._ctx = Context()
10611 self._ctx.ctx = ctx
10617 ctypes.c_void_p(self.id),
◆ __del__()
Definition at line 10622 of file z3py.py.
10624 self._ctx.ctx =
None
◆ add()
Definition at line 10668 of file z3py.py.
10670 assert not self._ctx
◆ add_diseq()
def add_diseq |
( |
|
self, |
|
|
|
diseq |
|
) |
| |
Definition at line 10653 of file z3py.py.
10654 assert not self.diseq
10655 assert not self._ctx
◆ add_eq()
Definition at line 10647 of file z3py.py.
10649 assert not self._ctx
◆ add_final()
def add_final |
( |
|
self, |
|
|
|
final |
|
) |
| |
Definition at line 10641 of file z3py.py.
10642 assert not self.final
10643 assert not self._ctx
◆ add_fixed()
def add_fixed |
( |
|
self, |
|
|
|
fixed |
|
) |
| |
Definition at line 10635 of file z3py.py.
10636 assert not self.fixed
10637 assert not self._ctx
◆ conflict()
def conflict |
( |
|
self, |
|
|
|
ids |
|
) |
| |
Definition at line 10689 of file z3py.py.
10690 self.propagate(
BoolVal(
False, self.ctx()), ids, eqs=[])
◆ ctx()
◆ ctx_ref()
◆ fresh()
Definition at line 10665 of file z3py.py.
10666 raise Z3Exception(
"fresh needs to be overwritten")
◆ 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")
◆ propagate()
def propagate |
( |
|
self, |
|
|
|
e, |
|
|
|
ids, |
|
|
|
eqs = [] |
|
) |
| |
Definition at line 10676 of file z3py.py.
10677 num_fixed = len(ids)
10678 _ids = (ctypes.c_uint * num_fixed)()
10679 for i
in range(num_fixed):
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]
Referenced by UserPropagateBase.conflict().
◆ push()
Definition at line 10659 of file z3py.py.
10660 raise Z3Exception(
"push needs to be overwritten")
◆ cb
◆ diseq
◆ eq
◆ final
◆ fixed
◆ id
◆ solver
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.
def __init__(self, s, ctx=None)
def add_diseq(self, diseq)
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
expr range(expr const &lo, expr const &hi)
def ensure_prop_closures()
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.
def pop(self, num_scopes)
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
def add_final(self, final)
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.
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...
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...
def BoolVal(val, ctx=None)
def add_fixed(self, fixed)
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...
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
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 ...
def propagate(self, e, ids, eqs=[])