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

Public Member Functions

def __init__
 
def __del__
 
def ref
 
def interrupt
 
def set
 

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 125 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  args,
  kws 
)

Definition at line 136 of file z3py.py.

136 
137  def __init__(self, *args, **kws):
138  if __debug__:
139  _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
140  conf = Z3_mk_config()
141  for key, value in kws.iteritems():
142  Z3_set_param_value(conf, str(key).upper(), _to_param_value(value))
143  prev = None
144  for a in args:
145  if prev == None:
146  prev = a
147  else:
148  Z3_set_param_value(conf, str(prev), _to_param_value(a))
149  prev = None
150  self.lib = lib()
151  self.ctx = Z3_mk_context_rc(conf)
152  Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
153  lib().Z3_set_error_handler.restype = None
154  lib().Z3_set_error_handler.argtypes = [ContextObj, _error_handler_fptr]
155  lib().Z3_set_error_handler(self.ctx, _Z3Python_error_handler)
156  Z3_del_config(conf)
def __del__ (   self)

Definition at line 157 of file z3py.py.

157 
158  def __del__(self):
159  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 164 of file z3py.py.

164 
165  def interrupt(self):
166  """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
167 
168  This method can be invoked from a thread different from the one executing the
169  interruptable procedure.
170  """
171  Z3_interrupt(self.ref())
def ref (   self) 
Return a reference to the actual C pointer to the Z3 context.

Definition at line 160 of file z3py.py.

Referenced by Context.interrupt().

160 
161  def ref(self):
162  """Return a reference to the actual C pointer to the Z3 context."""
163  return self.ctx
def set (   self,
  args,
  kws 
) 
Set global configuration options. 

Z3 command line options can be set using this method. 
The option names can be specified in different ways:

>>> ctx = Context()
>>> ctx.set('WELL_SORTED_CHECK', True)
>>> ctx.set(':well-sorted-check', True)
>>> ctx.set(well_sorted_check=True)

Definition at line 172 of file z3py.py.

172 
173  def set(self, *args, **kws):
174  """Set global configuration options.
175 
176  Z3 command line options can be set using this method.
177  The option names can be specified in different ways:
178 
179  >>> ctx = Context()
180  >>> ctx.set('WELL_SORTED_CHECK', True)
181  >>> ctx.set(':well-sorted-check', True)
182  >>> ctx.set(well_sorted_check=True)
183  """
184  if __debug__:
185  _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
186  for key, value in kws.iteritems():
187  Z3_update_param_value(self.ctx, str(key).upper(), _to_param_value(value))
188  prev = None
189  for a in args:
190  if prev == None:
191  prev = a
192  else:
193  Z3_update_param_value(self.ctx, str(prev), _to_param_value(a))
194  prev = None
195 
# Global Z3 context

Field Documentation

ctx

Definition at line 150 of file z3py.py.

Referenced by Context.__del__(), ExprRef.__eq__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), ExprRef.__ne__(), Probe.__ne__(), Tactic.apply(), ExprRef.arg(), ApplyResult.as_expr(), BoolSortRef.cast(), ApplyResult.convert_model(), ExprRef.decl(), FuncDeclRef.domain(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), SortRef.kind(), SortRef.name(), FuncDeclRef.name(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), FuncDeclRef.range(), Context.ref(), Context.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), and Fixedpoint.statistics().

lib

Definition at line 149 of file z3py.py.

Generated on Thu Nov 22 2012 18:37:31 for Z3 by   doxygen 1.8.2