Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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.

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)

Definition at line 170 of file z3py.py.

00170 
00171     def __del__(self):
00172         self.lib.Z3_del_context(self.ctx)


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.

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)
Return a reference to the actual C pointer to the Z3 context.

Definition at line 173 of file z3py.py.

Referenced by Context.interrupt().

00173 
00174     def ref(self):
00175         """Return a reference to the actual C pointer to the Z3 context."""
00176         return self.ctx


Field Documentation

ctx
lib

Definition at line 148 of file z3py.py.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines