Public Member Functions | |
def | __init__ (self, args, kws) |
def | __del__ (self) |
def | ref (self) |
def | interrupt (self) |
Data Fields | |
lib | |
ctx | |
A Context manages all other Z3 objects, global configuration options, etc. Z3Py uses a default global context. For most applications this is sufficient. An application may use multiple Z3 contexts. Objects created in one context cannot be used in another one. However, several objects may be "translated" from one context to another. It is not safe to access Z3 objects from multiple threads. The only exception is the method `interrupt()` that can be used to interrupt() a long computation. The initialization method receives global configuration options for the new context.
def __init__ | ( | self, | |
args, | |||
kws | |||
) |
Definition at line 156 of file z3py.py.
def interrupt | ( | self | ) |
Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions. This method can be invoked from a thread different from the one executing the interruptable procedure.
def ref | ( | self | ) |
Return a reference to the actual C pointer to the Z3 context.
Definition at line 182 of file z3py.py.
Referenced by Context.interrupt().
ctx |
Definition at line 171 of file z3py.py.
Referenced by FuncDeclRef.__call__(), Probe.__call__(), Context.__del__(), AstRef.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), ExprRef.__eq__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), ExprRef.__ne__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ExprRef.arg(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), BoolSortRef.cast(), Optimize.check(), ApplyResult.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), FuncDeclRef.domain(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_num_levels(), Fixedpoint.get_rules(), Fixedpoint.help(), Optimize.help(), Tactic.help(), SortRef.kind(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Optimize.pop(), Fixedpoint.push(), Optimize.push(), Fixedpoint.query(), FuncDeclRef.range(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Context.ref(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), FiniteDomainRef.sort(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), AstRef.translate(), and Fixedpoint.update_rule().
lib |
Definition at line 170 of file z3py.py.
Referenced by Context.__del__().