Z3
Public Member Functions | Data Fields
Context Class Reference

Public Member Functions

def __init__ (self, args, kws)
 
def __del__ (self)
 
def ref (self)
 
def interrupt (self)
 

Data Fields

 ctx
 
 eh
 

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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  args,
  kws 
)

Definition at line 164 of file z3py.py.

164  def __init__(self, *args, **kws):
165  if __debug__:
166  _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
167  conf = Z3_mk_config()
168  for key in kws:
169  value = kws[key]
170  Z3_set_param_value(conf, str(key).upper(), _to_param_value(value))
171  prev = None
172  for a in args:
173  if prev is None:
174  prev = a
175  else:
176  Z3_set_param_value(conf, str(prev), _to_param_value(a))
177  prev = None
178  self.ctx = Z3_mk_context_rc(conf)
179  self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)
180  Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
181  Z3_del_config(conf)
182 
Z3_context Z3_API Z3_mk_context_rc(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(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.

◆ __del__()

def __del__ (   self)

Definition at line 183 of file z3py.py.

183  def __del__(self):
184  Z3_del_context(self.ctx)
185  self.ctx = None
186  self.eh = None
187 
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.

Member Function Documentation

◆ interrupt()

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
interruptible procedure.

Definition at line 192 of file z3py.py.

192  def interrupt(self):
193  """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
194 
195  This method can be invoked from a thread different from the one executing the
196  interruptible procedure.
197  """
198  Z3_interrupt(self.ref())
199 
200 
201 # Global Z3 context
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...

◆ ref()

def ref (   self)
Return a reference to the actual C pointer to the Z3 context.

Definition at line 188 of file z3py.py.

Referenced by Context.interrupt().

188  def ref(self):
189  """Return a reference to the actual C pointer to the Z3 context."""
190  return self.ctx
191 

Field Documentation

◆ ctx

ctx

Definition at line 178 of file z3py.py.

Referenced by FuncDeclRef.__call__(), Probe.__call__(), AstRef.__copy__(), AstRef.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), 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_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), 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(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Optimize.pop(), Fixedpoint.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), 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().

◆ eh

eh

Definition at line 179 of file z3py.py.

Referenced by Context.__del__().