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

Data Fields
	ctx = Z3_mk_context_rc(conf)
bool	owner = True
	eh = Z3_set_error_handler(self.ctx, z3_error_handler)

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

◆ init()

__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)
 

◆ del()

__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

◆ interrupt()

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())
 

◆ param_descrs()

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)
 

◆ ref()

ref ( self )

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

Definition at line 228 of file z3py.py.

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

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

◆ set_ast_print_mode()

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

ctx = Z3_mk_context_rc(conf)

Definition at line 216 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), AstRef.__deepcopy__(), AstVector.__deepcopy__(), Datatype.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), Goal.__deepcopy__(), ModelRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), ParamsRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), AstRef.__del__(), AstVector.__del__(), __del__(), FuncEntry.__del__(), FuncInterp.__del__(), Goal.__del__(), ModelRef.__del__(), ParamDescrsRef.__del__(), ParamsRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), Solver.__del__(), Statistics.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstMap.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstMap.__len__(), AstVector.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), BoolRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), AstMap.__repr__(), ParamDescrsRef.__repr__(), ParamsRef.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstMap.__setitem__(), AstVector.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), ModelRef.project(), ModelRef.project_with_witness(), AstVector.push(), Solver.push(), QuantifierRef.qid(), ArraySortRef.range(), FuncDeclRef.range(), DatatypeSortRef.recognizer(), ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), ParamsRef.set(), Solver.set(), AstVector.sexpr(), Goal.sexpr(), ModelRef.sexpr(), Goal.size(), ParamDescrsRef.size(), QuantifierRef.skolem_id(), AstRef.translate(), AstVector.translate(), Goal.translate(), ModelRef.translate(), ExprRef.update(), DatatypeRef.update_field(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ eh

eh = Z3_set_error_handler(self.ctx, z3_error_handler)

Definition at line 218 of file z3py.py.

Referenced by __del__().

◆ owner

bool owner = True

Definition at line 217 of file z3py.py.