Public Member Functions | |
def | __init__ |
def | __del__ (self) |
def | ctx (self) |
def | ctx_ref (self) |
def | add_fixed (self, fixed) |
def | add_created (self, created) |
def | add_final (self, final) |
def | add_eq (self, eq) |
def | add_diseq (self, diseq) |
def | add_decide (self, decide) |
def | push (self) |
def | pop (self, num_scopes) |
def | fresh (self, new_ctx) |
def | add (self, e) |
def | next_split (self, t, idx, phase) |
def | propagate |
def | conflict |
Data Fields | |
solver | |
fresh_ctx | |
cb | |
id | |
fixed | |
final | |
eq | |
diseq | |
created | |
decide | |
def __init__ | ( | self, | |
s, | |||
ctx = None |
|||
) |
def add | ( | self, | |
e | |||
) |
Definition at line 11753 of file z3py.py.
def add_created | ( | self, | |
created | |||
) |
def add_decide | ( | self, | |
decide | |||
) |
def add_diseq | ( | self, | |
diseq | |||
) |
def add_eq | ( | self, | |
eq | |||
) |
def add_final | ( | self, | |
final | |||
) |
def add_fixed | ( | self, | |
fixed | |||
) |
def conflict | ( | self, | |
deps = [] , |
|||
eqs = [] |
|||
) |
def ctx | ( | self | ) |
def ctx_ref | ( | self | ) |
Definition at line 11699 of file z3py.py.
Referenced by UserPropagateBase.add(), UserPropagateBase.add_created(), UserPropagateBase.add_decide(), UserPropagateBase.add_diseq(), UserPropagateBase.add_eq(), UserPropagateBase.add_final(), and UserPropagateBase.add_fixed().
def next_split | ( | self, | |
t, | |||
idx, | |||
phase | |||
) |
def propagate | ( | self, | |
e, | |||
ids, | |||
eqs = [] |
|||
) |
Definition at line 11771 of file z3py.py.
Referenced by UserPropagateBase.conflict().
cb |
Definition at line 11672 of file z3py.py.
Referenced by UserPropagateBase.add(), UserPropagateBase.next_split(), and UserPropagateBase.propagate().
created |
Definition at line 11678 of file z3py.py.
Referenced by UserPropagateBase.add_created().
decide |
Definition at line 11742 of file z3py.py.
Referenced by UserPropagateBase.add_decide().
diseq |
Definition at line 11677 of file z3py.py.
Referenced by UserPropagateBase.add_diseq().
eq |
Definition at line 11676 of file z3py.py.
Referenced by AstRef.__eq__(), UserPropagateBase.add_eq(), SortRef.cast(), and BoolSortRef.cast().
final |
Definition at line 11675 of file z3py.py.
Referenced by UserPropagateBase.add_final().
fixed |
Definition at line 11674 of file z3py.py.
Referenced by UserPropagateBase.add_fixed().
fresh_ctx |
Definition at line 11671 of file z3py.py.
Referenced by UserPropagateBase.ctx().
solver |
Definition at line 11669 of file z3py.py.
Referenced by UserPropagateBase.add(), UserPropagateBase.add_created(), UserPropagateBase.add_decide(), UserPropagateBase.add_diseq(), UserPropagateBase.add_eq(), UserPropagateBase.add_final(), and UserPropagateBase.add_fixed().