Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions | Data Fields
Context Class Reference

Public Member Functions

def __init__
 
def __del__
 
def ref
 
def interrupt
 

Data Fields

 lib
 
 ctx
 

Detailed Description

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.

Definition at line 137 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  args,
  kws 
)

Definition at line 148 of file z3py.py.

149  def __init__(self, *args, **kws):
150  if __debug__:
151  _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
152  conf = Z3_mk_config()
153  for key in kws:
154  value = kws[key]
155  Z3_set_param_value(conf, str(key).upper(), _to_param_value(value))
156  prev = None
157  for a in args:
158  if prev == None:
159  prev = a
160  else:
161  Z3_set_param_value(conf, str(prev), _to_param_value(a))
162  prev = None
163  self.lib = lib()
164  self.ctx = Z3_mk_context_rc(conf)
165  Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
166  lib().Z3_set_error_handler.restype = None
167  lib().Z3_set_error_handler.argtypes = [ContextObj, _error_handler_fptr]
168  lib().Z3_set_error_handler(self.ctx, _Z3Python_error_handler)
169  Z3_del_config(conf)
Z3_context Z3_API Z3_mk_context_rc(__in Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
void Z3_API Z3_set_ast_print_mode(__in Z3_context c, __in Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
void Z3_API Z3_set_error_handler(__in Z3_context c, __in Z3_error_handler h)
Register a Z3 error handler.
void Z3_API Z3_del_config(__in Z3_config c)
Delete the given configuration object.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
def __init__
Definition: z3py.py:148
void Z3_API Z3_set_param_value(__in Z3_config c, __in Z3_string param_id, __in Z3_string param_value)
Set a configuration parameter.
def __del__ (   self)

Definition at line 170 of file z3py.py.

171  def __del__(self):
172  self.lib.Z3_del_context(self.ctx)
def __del__
Definition: z3py.py:170

Member Function Documentation

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.

178  def interrupt(self):
179  """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
180 
181  This method can be invoked from a thread different from the one executing the
182  interruptable procedure.
183  """
184  Z3_interrupt(self.ref())
185 
186 
# Global Z3 context
def ref
Definition: z3py.py:173
void Z3_API Z3_interrupt(__in Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
def interrupt
Definition: z3py.py:177
def ref (   self)
Return a reference to the actual C pointer to the Z3 context.

Definition at line 173 of file z3py.py.

Referenced by Context.interrupt().

174  def ref(self):
175  """Return a reference to the actual C pointer to the Z3 context."""
176  return self.ctx
def ref
Definition: z3py.py:173

Field Documentation

ctx

Definition at line 163 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), Context.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), ArrayRef.__getitem__(), AstVector.__getitem__(), AstMap.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), Fixedpoint.add_rule(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), BoolSortRef.cast(), ApplyResult.convert_model(), ExprRef.decl(), FuncDeclRef.domain(), ArraySortRef.domain(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), AstMap.keys(), SortRef.kind(), SortRef.name(), FuncDeclRef.name(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), FuncDeclRef.range(), ArraySortRef.range(), Context.ref(), Fixedpoint.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), Fixedpoint.statistics(), Solver.to_smt2(), and Fixedpoint.update_rule().

lib

Definition at line 162 of file z3py.py.