Context Class Reference

Public Member Functions
def	__init__ (self, args, kws)
def	__del__ (self)
def	ref (self)
def	interrupt (self)
def	param_descrs (self)
def	set_ast_print_mode (self, mode)

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

Constructor & Destructor Documentation

def __init__	(		self,
			args,
			kws
	)

Definition at line 202 of file z3py.py.

    def __init__(self, *args, **kws):
        if z3_debug():
            _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
        conf = Z3_mk_config()
        for key in kws:
            value = kws[key]
            Z3_set_param_value(conf, str(key).upper(), _to_param_value(value))
        prev = None
        for a in args:
            if prev is None:
                prev = a
            else:
                Z3_set_param_value(conf, str(prev), _to_param_value(a))
                prev = None
        self.ctx = Z3_mk_context_rc(conf)
        self.owner = True
        self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)
        Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
        Z3_del_config(conf)

def __del__

(

self

)

Definition at line 222 of file z3py.py.

    def __del__(self):
        if Z3_del_context is not None and self.owner:
            Z3_del_context(self.ctx)
        self.ctx = None
        self.eh = None

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

Definition at line 232 of file z3py.py.

    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.
        """
        Z3_interrupt(self.ref())

def param_descrs

(

self

)

Return the global parameter description set.

Definition at line 240 of file z3py.py.

    def param_descrs(self):
        """Return the global parameter description set."""
        return ParamDescrsRef(Z3_get_global_param_descrs(self.ref()), self)

def ref

(

self

)

Return a reference to the actual C pointer to the Z3 context.

Definition at line 228 of file z3py.py.

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

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

def set_ast_print_mode	(		self,
			mode
	)

Set the pretty printing mode for ASTs.

The following modes are available:
- Z3_PRINT_SMTLIB_FULL (0): Print AST nodes in SMTLIB verbose format.
- Z3_PRINT_LOW_LEVEL (1): Print AST nodes using a low-level format.
- Z3_PRINT_SMTLIB2_COMPLIANT (2): Print AST nodes in SMTLIB 2.x compliant format.

Example:
>>> c = Context()
>>> x = Int('x', c)
>>> c.set_ast_print_mode(Z3_PRINT_SMTLIB2_COMPLIANT)
>>> print(x)
x

Definition at line 244 of file z3py.py.

    def set_ast_print_mode(self, mode):
        """Set the pretty printing mode for ASTs.

        The following modes are available:
        - Z3_PRINT_SMTLIB_FULL (0): Print AST nodes in SMTLIB verbose format.
        - Z3_PRINT_LOW_LEVEL (1): Print AST nodes using a low-level format.
        - Z3_PRINT_SMTLIB2_COMPLIANT (2): Print AST nodes in SMTLIB 2.x compliant format.

        Example:
        >>> c = Context()
        >>> x = Int('x', c)
        >>> c.set_ast_print_mode(Z3_PRINT_SMTLIB2_COMPLIANT)
        >>> print(x)
        x
        """
        Z3_set_ast_print_mode(self.ref(), mode)
        

# Global Z3 context

Field Documentation

ctx

Definition at line 216 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstRef.__copy__(), AstVector.__copy__(), AstRef.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Simplifier.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Context.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), AstVector.__getitem__(), AstMap.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), CharRef.__le__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), 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__(), Simplifier.add(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), ApplyResult.as_expr(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), BoolSortRef.cast(), ExprRef.decl(), ArrayRef.default(), FuncDeclRef.domain(), ArraySortRef.domain(), ArraySortRef.domain_n(), ParserContext.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), CharRef.is_digit(), AstMap.keys(), SortRef.kind(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Simplifier.param_descrs(), Tactic.param_descrs(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), AlgebraicNumRef.poly(), Fixedpoint.query(), FuncDeclRef.range(), ArraySortRef.range(), Context.ref(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), FiniteDomainRef.sort(), Fixedpoint.statistics(), Optimize.statistics(), CharRef.to_bv(), CharRef.to_int(), Solver.to_smt2(), Optimize.unsat_core(), ExprRef.update(), Fixedpoint.update_rule(), and Simplifier.using_params().

eh

Definition at line 218 of file z3py.py.

Referenced by Context.__del__().

owner

Definition at line 217 of file z3py.py.

Referenced by Context.__del__().