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) | |
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 | |
Protected Attributes | |
_ctx = None | |
__init__ | ( | self, | |
s, | |||
ctx = None ) |
Definition at line 11815 of file z3py.py.
__del__ | ( | self | ) |
add | ( | self, | |
e ) |
Definition at line 11903 of file z3py.py.
add_created | ( | self, | |
created ) |
Definition at line 11859 of file z3py.py.
add_decide | ( | self, | |
decide ) |
Definition at line 11887 of file z3py.py.
add_diseq | ( | self, | |
diseq ) |
Definition at line 11880 of file z3py.py.
add_eq | ( | self, | |
eq ) |
Definition at line 11873 of file z3py.py.
add_final | ( | self, | |
final ) |
Definition at line 11866 of file z3py.py.
add_fixed | ( | self, | |
fixed ) |
Definition at line 11852 of file z3py.py.
conflict | ( | self, | |
deps = [], | |||
eqs = [] ) |
ctx | ( | self | ) |
ctx_ref | ( | self | ) |
fresh | ( | self, | |
new_ctx ) |
next_split | ( | self, | |
t, | |||
idx, | |||
phase ) |
pop | ( | self, | |
num_scopes ) |
propagate | ( | self, | |
e, | |||
ids, | |||
eqs = [] ) |
Definition at line 11921 of file z3py.py.
push | ( | self | ) |
eq = None |
Definition at line 11825 of file z3py.py.
Referenced by AstRef.__eq__(), and SortRef.cast().