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
Constructor & Destructor Documentation
◆ __init__()
| __init__ | ( | self, | |
| s, | |||
| ctx = None ) |
Definition at line 12502 of file z3py.py.
12502 def __init__(self, s, ctx=None):
12503 assert s is None or ctx is None
12504 ensure_prop_closures()
12505 self.solver = s
12506 self._ctx = None
12507 self.fresh_ctx = None
12508 self.cb = None
12509 self.id = _prop_closures.insert(self)
12510 self.fixed = None
12511 self.final = None
12512 self.eq = None
12513 self.diseq = None
12514 self.decide = None
12515 self.created = None
12516 self.binding = None
12517 if ctx:
12518 self.fresh_ctx = ctx
12519 if s:
12520 Z3_solver_propagate_init(self.ctx_ref(),
12521 s.solver,
12522 ctypes.c_void_p(self.id),
12523 _user_prop_push,
12524 _user_prop_pop,
12525 _user_prop_fresh)
12526
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 | ) |
Member Function Documentation
◆ add()
| add | ( | self, | |
| e ) |
Definition at line 12612 of file z3py.py.
12612 def add(self, e):
12613 if self._ctx:
12614 raise Z3Exception("context already initialized")
12615 if self.solver:
12616 Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
12617 else:
12618 Z3_solver_propagate_register_cb(self.ctx_ref(), ctypes.c_void_p(self.cb), e.ast)
12619
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...
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 12549 of file z3py.py.
12549 def add_created(self, created):
12550 if self.created:
12551 raise Z3Exception("created callback already registered")
12552 if self._ctx:
12553 raise Z3Exception("context already initialized")
12554 if self.solver:
12555 Z3_solver_propagate_created(self.ctx_ref(), self.solver.solver, _user_prop_created)
12556 self.created = created
12557
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 12585 of file z3py.py.
12585 def add_decide(self, decide):
12586 if self.decide:
12587 raise Z3Exception("decide callback already registered")
12588 if self._ctx:
12589 raise Z3Exception("context already initialized")
12590 if self.solver:
12591 Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide)
12592 self.decide = decide
12593
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 12576 of file z3py.py.
12576 def add_diseq(self, diseq):
12577 if self.diseq:
12578 raise Z3Exception("diseq callback already registered")
12579 if self._ctx:
12580 raise Z3Exception("context already initialized")
12581 if self.solver:
12582 Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq)
12583 self.diseq = diseq
12584
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 12567 of file z3py.py.
12567 def add_eq(self, eq):
12568 if self.eq:
12569 raise Z3Exception("eq callback already registered")
12570 if self._ctx:
12571 raise Z3Exception("context already initialized")
12572 if self.solver:
12573 Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq)
12574 self.eq = eq
12575
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 12558 of file z3py.py.
12558 def add_final(self, final):
12559 if self.final:
12560 raise Z3Exception("final callback already registered")
12561 if self._ctx:
12562 raise Z3Exception("context already initialized")
12563 if self.solver:
12564 Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final)
12565 self.final = final
12566
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 12540 of file z3py.py.
12540 def add_fixed(self, fixed):
12541 if self.fixed:
12542 raise Z3Exception("fixed callback already registered")
12543 if self._ctx:
12544 raise Z3Exception("context already initialized")
12545 if self.solver:
12546 Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
12547 self.fixed = fixed
12548
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 12594 of file z3py.py.
12594 def add_on_binding(self, binding):
12595 if self.binding:
12596 raise Z3Exception("binding callback already registered")
12597 if self._ctx:
12598 raise Z3Exception("context already initialized")
12599 if self.solver:
12600 Z3_solver_propagate_on_binding(self.ctx_ref(), self.solver.solver, _user_prop_binding)
12601 self.binding = binding
12602
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 = [] ) |
◆ ctx()
| ctx | ( | self | ) |
◆ ctx_ref()
| ctx_ref | ( | self | ) |
◆ fresh()
| fresh | ( | self, | |
| new_ctx ) |
◆ next_split()
| next_split | ( | self, | |
| t, | |||
| idx, | |||
| phase ) |
◆ pop()
| pop | ( | self, | |
| num_scopes ) |
◆ propagate()
| propagate | ( | self, | |
| e, | |||
| ids, | |||
| eqs = [] ) |
Definition at line 12631 of file z3py.py.
12631 def propagate(self, e, ids, eqs=[]):
12632 _ids, num_fixed = _to_ast_array(ids)
12633 num_eqs = len(eqs)
12634 _lhs, _num_lhs = _to_ast_array([x for x, y in eqs])
12635 _rhs, _num_rhs = _to_ast_array([y for x, y in eqs])
12637 self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
12638
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 | ) |
Field Documentation
◆ _ctx
◆ binding
◆ cb
◆ created
◆ decide
◆ diseq
◆ eq
| eq = None |
Definition at line 12512 of file z3py.py.
Referenced by AstRef.__eq__(), FiniteSetSortRef.cast(), and SortRef.cast().
◆ final
◆ fixed
◆ fresh_ctx
◆ id
◆ solver
Generated by
1.18.0