Public Member Functions | |
def | __init__ |
def | __del__ |
def | ref |
def | interrupt |
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 148 of file z3py.py.
00148 00149 def __init__(self, *args, **kws): 00150 if __debug__: 00151 _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.") 00152 conf = Z3_mk_config() 00153 for key in kws: 00154 value = kws[key] 00155 Z3_set_param_value(conf, str(key).upper(), _to_param_value(value)) 00156 prev = None 00157 for a in args: 00158 if prev == None: 00159 prev = a 00160 else: 00161 Z3_set_param_value(conf, str(prev), _to_param_value(a)) 00162 prev = None 00163 self.lib = lib() 00164 self.ctx = Z3_mk_context_rc(conf) 00165 Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT) 00166 lib().Z3_set_error_handler.restype = None 00167 lib().Z3_set_error_handler.argtypes = [ContextObj, _error_handler_fptr] 00168 lib().Z3_set_error_handler(self.ctx, _Z3Python_error_handler) 00169 Z3_del_config(conf)
def __del__ | ( | self | ) |
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.
Definition at line 177 of file z3py.py.
00177 00178 def interrupt(self): 00179 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions. 00180 00181 This method can be invoked from a thread different from the one executing the 00182 interruptable procedure. 00183 """ 00184 Z3_interrupt(self.ref()) 00185 00186 # Global Z3 context
def ref | ( | self | ) |
Definition at line 148 of file z3py.py.
Referenced by FuncDeclRef.__call__(), Context.__del__(), ExprRef.__eq__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), ExprRef.__ne__(), Probe.__ne__(), Fixedpoint.add_rule(), Tactic.apply(), ExprRef.arg(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), BoolSortRef.cast(), ApplyResult.convert_model(), ExprRef.decl(), FuncDeclRef.domain(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), SortRef.kind(), SortRef.name(), FuncDeclRef.name(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), FuncDeclRef.range(), Context.ref(), Fixedpoint.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), Fixedpoint.statistics(), Solver.to_smt2(), and Fixedpoint.update_rule().