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)
 
def param_descrs (self)
 

Data Fields

 ctx
 
 owner
 
 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 180 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
args,
**  kws 
)

Definition at line 192 of file z3py.py.

192  def __init__(self, *args, **kws):
193  if z3_debug():
194  _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
195  conf = Z3_mk_config()
196  for key in kws:
197  value = kws[key]
198  Z3_set_param_value(conf, str(key).upper(), _to_param_value(value))
199  prev = None
200  for a in args:
201  if prev is None:
202  prev = a
203  else:
204  Z3_set_param_value(conf, str(prev), _to_param_value(a))
205  prev = None
206  self.ctx = Z3_mk_context_rc(conf)
207  self.owner = True
208  self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)
209  Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
210  Z3_del_config(conf)
211 
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....
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_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.
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
def z3_debug()
Definition: z3py.py:62

◆ __del__()

def __del__ (   self)

Definition at line 212 of file z3py.py.

212  def __del__(self):
213  if Z3_del_context is not None and self.owner:
214  Z3_del_context(self.ctx)
215  self.ctx = None
216  self.eh = None
217 
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 222 of file z3py.py.

222  def interrupt(self):
223  """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
224 
225  This method can be invoked from a thread different from the one executing the
226  interruptible procedure.
227  """
228  Z3_interrupt(self.ref())
229 
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...

◆ param_descrs()

def param_descrs (   self)
Return the global parameter description set.

Definition at line 230 of file z3py.py.

230  def param_descrs(self):
231  """Return the global parameter description set."""
232  return ParamDescrsRef(Z3_get_global_param_descrs(self.ref()), self)
233 
234 
235 # Global Z3 context
Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c)
Retrieve description of global parameters.

◆ ref()

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

Definition at line 218 of file z3py.py.

218  def ref(self):
219  """Return a reference to the actual C pointer to the Z3 context."""
220  return self.ctx
221 

Referenced by Context.interrupt(), and Context.param_descrs().

Field Documentation

◆ ctx

ctx

Definition at line 206 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), FPRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), Probe.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), ParserContext.__del__(), ArithRef.__div__(), BitVecRef.__div__(), FPRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), FPRef.__ge__(), SeqRef.__ge__(), AstVector.__getitem__(), SeqRef.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ApplyResult.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), FPRef.__gt__(), SeqRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), FPRef.__le__(), SeqRef.__le__(), CharRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ApplyResult.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), FPRef.__lt__(), SeqRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), BitVecRef.__mul__(), FPRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), FPRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), FPRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), FPRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), FPRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), FPRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Fixedpoint.add_cover(), ParserContext.add_decl(), Fixedpoint.add_rule(), Optimize.add_soft(), ParserContext.add_sort(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), ApplyResult.as_expr(), FPNumRef.as_string(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), SeqRef.at(), SeqSortRef.basis(), ReSortRef.basis(), QuantifierRef.body(), BoolSortRef.cast(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), DatatypeSortRef.constructor(), Goal.convert_model(), AstRef.ctx_ref(), UserPropagateBase.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), Solver.dimacs(), ArraySortRef.domain(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), FPNumRef.exponent(), FPNumRef.exponent_as_bv(), FPNumRef.exponent_as_long(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), ParserContext.from_string(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ParamDescrsRef.get_documentation(), Fixedpoint.get_ground_sat_answer(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), ModelRef.get_sort(), ModelRef.get_universe(), Solver.help(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Solver.import_model_converter(), Goal.inconsistent(), CharRef.is_digit(), FPNumRef.isInf(), FPNumRef.isNaN(), FPNumRef.isNegative(), FPNumRef.isNormal(), FPNumRef.isPositive(), FPNumRef.isSubnormal(), FPNumRef.isZero(), AstMap.keys(), Statistics.keys(), SortRef.kind(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), Solver.next(), QuantifierRef.no_pattern(), Solver.non_units(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), RatNumRef.numerator(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Optimize.pop(), Solver.pop(), Goal.prec(), Solver.proof(), Solver.push(), Optimize.push(), AstVector.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), FuncDeclRef.range(), ArraySortRef.range(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), DatatypeSortRef.recognizer(), Context.ref(), Fixedpoint.register_relation(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.root(), Solver.set(), Fixedpoint.set(), Optimize.set(), ParamsRef.set(), Optimize.set_on_model(), Fixedpoint.set_predicate_representation(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), FPNumRef.sign(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPNumRef.significand_as_long(), ParamDescrsRef.size(), Goal.size(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), FiniteDomainRef.sort(), FPRef.sort(), SeqRef.sort(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), CharRef.to_bv(), CharRef.to_int(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), AstVector.translate(), FuncInterp.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ eh

eh

Definition at line 208 of file z3py.py.

Referenced by Context.__del__().

◆ owner

owner

Definition at line 207 of file z3py.py.

Referenced by Context.__del__().