UserPropagateBase Class Reference

Public Member Functions
	__init__ (self, s, ctx=None)
	__del__ (self)
	ctx (self)
	ctx_ref (self)
	add_fixed (self, fixed)
	add_created (self, created)
	add_final (self, final)
	add_eq (self, eq)
	add_diseq (self, diseq)
	add_decide (self, decide)
	add_on_binding (self, binding)
	push (self)
	pop (self, num_scopes)
	fresh (self, new_ctx)
	add (self, e)
	next_split (self, t, idx, phase)
	propagate (self, e, ids, eqs=[])
	conflict (self, deps=[], eqs=[])

Data Fields
	solver
	fresh_ctx
	cb
	id
	fixed
	final
	eq
	diseq
	decide
	created
	binding

Protected Attributes
	_ctx

Detailed Description

Definition at line 11903 of file z3py.py.

Constructor & Destructor Documentation

__init__()

__init__	(		self,
			s,
			ctx = None )

Definition at line 11912 of file z3py.py.

    def __init__(self, s, ctx=None):
        assert s is None or ctx is None
        ensure_prop_closures()
        self.solver = s
        self._ctx = None
        self.fresh_ctx = None
        self.cb = None
        self.id = _prop_closures.insert(self)
        self.fixed = None
        self.final = None
        self.eq = None
        self.diseq = None
        self.decide = None
        self.created = None
        self.binding = None
        if ctx:
            self.fresh_ctx = ctx
        if s:
            Z3_solver_propagate_init(self.ctx_ref(),
                                     s.solver,
                                     ctypes.c_void_p(self.id),
                                     _user_prop_push,
                                     _user_prop_pop,
                                     _user_prop_fresh)
 

__del__()

__del__

(

self

)

Definition at line 11937 of file z3py.py.

    def __del__(self):
        if self._ctx:
            self._ctx.ctx = None
 

Member Function Documentation

add()

add	(		self,
			e )

Definition at line 12008 of file z3py.py.

    def add(self, e):
        assert not self._ctx
        if self.solver:
            Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
        else:
            Z3_solver_propagate_register_cb(self.ctx_ref(), ctypes.c_void_p(self.cb), e.ast)
        

Referenced by Solver.__iadd__().

add_created()

add_created	(		self,
			created )

Definition at line 11957 of file z3py.py.

    def add_created(self, created):
        assert not self.created
        assert not self._ctx
        if self.solver:
            Z3_solver_propagate_created(self.ctx_ref(), self.solver.solver, _user_prop_created)
        self.created = created
        

add_decide()

add_decide	(		self,
			decide )

Definition at line 11985 of file z3py.py.

    def add_decide(self, decide):
        assert not self.decide
        assert not self._ctx
        if self.solver:
            Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide)
        self.decide = decide   
        

add_diseq()

add_diseq	(		self,
			diseq )

Definition at line 11978 of file z3py.py.

    def add_diseq(self, diseq):
        assert not self.diseq
        assert not self._ctx
        if self.solver:
            Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq)
        self.diseq = diseq
 

add_eq()

add_eq	(		self,
			eq )

Definition at line 11971 of file z3py.py.

    def add_eq(self, eq):
        assert not self.eq
        assert not self._ctx
        if self.solver:
            Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq)
        self.eq = eq
 

add_final()

add_final	(		self,
			final )

Definition at line 11964 of file z3py.py.

    def add_final(self, final):
        assert not self.final
        assert not self._ctx
        if self.solver:
            Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final)
        self.final = final
 

add_fixed()

add_fixed	(		self,
			fixed )

Definition at line 11950 of file z3py.py.

    def add_fixed(self, fixed):
        assert not self.fixed
        assert not self._ctx
        if self.solver:
            Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
        self.fixed = fixed
 

add_on_binding()

add_on_binding	(		self,
			binding )

Definition at line 11992 of file z3py.py.

    def add_on_binding(self, binding):
        assert not self.binding
        assert not self._ctx
        if self.solver:
            Z3_solver_propagate_on_binding(self.ctx_ref(), self.solver.solver, _user_prop_binding)
        self.binding = binding
 

conflict()

conflict	(		self,
			deps = [],
			eqs = [] )

Definition at line 12034 of file z3py.py.

    def conflict(self, deps = [], eqs = []):
        self.propagate(BoolVal(False, self.ctx()), deps, eqs)

ctx()

ctx

(

self

)

Definition at line 11941 of file z3py.py.

    def ctx(self):
        if self.fresh_ctx:
            return self.fresh_ctx
        else:
            return self.solver.ctx
 

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__(), Context.__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(), Context.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(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

ctx_ref()

ctx_ref

(

self

)

Definition at line 11947 of file z3py.py.

    def ctx_ref(self):
        return self.ctx().ref()
 

Referenced by BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), SortRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BitVecRef.__mul__(), ExprRef.__ne__(), SortRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncDeclRef.arity(), BitVecNumRef.as_binary_string(), IntNumRef.as_binary_string(), AlgebraicNumRef.as_decimal(), RatNumRef.as_decimal(), BitVecNumRef.as_string(), IntNumRef.as_string(), RatNumRef.as_string(), QuantifierRef.body(), ExprRef.decl(), ArrayRef.default(), RatNumRef.denominator(), FuncDeclRef.domain(), ArraySortRef.domain_n(), AstRef.eq(), AstRef.get_id(), ExprRef.get_id(), FuncDeclRef.get_id(), PatternRef.get_id(), QuantifierRef.get_id(), SortRef.get_id(), AstRef.hash(), AlgebraicNumRef.index(), QuantifierRef.is_exists(), QuantifierRef.is_lambda(), FuncDeclRef.kind(), SortRef.name(), QuantifierRef.no_pattern(), ExprRef.num_args(), QuantifierRef.num_no_patterns(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), RatNumRef.py_value(), QuantifierRef.qid(), ArraySortRef.range(), FuncDeclRef.range(), DatatypeSortRef.recognizer(), AstRef.sexpr(), QuantifierRef.skolem_id(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

fresh()

fresh	(		self,
			new_ctx )

Definition at line 12005 of file z3py.py.

    def fresh(self, new_ctx):
        raise Z3Exception("fresh needs to be overwritten")
 

next_split()

next_split	(		self,
			t,
			idx,
			phase )

Definition at line 12020 of file z3py.py.

    def next_split(self, t, idx, phase):
        return Z3_solver_next_split(self.ctx_ref(), ctypes.c_void_p(self.cb), t.ast, idx, phase)
        

pop()

pop	(		self,
			num_scopes )

Definition at line 12002 of file z3py.py.

    def pop(self, num_scopes):
        raise Z3Exception("pop needs to be overwritten")
 

Referenced by Solver.__exit__().

propagate()

propagate	(		self,
			e,
			ids,
			eqs = [] )

Definition at line 12026 of file z3py.py.

    def propagate(self, e, ids, eqs=[]):
        _ids, num_fixed = _to_ast_array(ids)
        num_eqs = len(eqs)
        _lhs, _num_lhs = _to_ast_array([x for x, y in eqs])
        _rhs, _num_rhs = _to_ast_array([y for x, y in eqs])
        return Z3_solver_propagate_consequence(e.ctx.ref(), ctypes.c_void_p(
            self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
 

push()

push

(

self

)

Definition at line 11999 of file z3py.py.

    def push(self):
        raise Z3Exception("push needs to be overwritten")
 

Referenced by Solver.__enter__().

Field Documentation

_ctx

_ctx

protected

Definition at line 11916 of file z3py.py.

binding

binding

Definition at line 11926 of file z3py.py.

cb

cb

Definition at line 11918 of file z3py.py.

created

created

Definition at line 11925 of file z3py.py.

decide

decide

Definition at line 11924 of file z3py.py.

diseq

diseq

Definition at line 11923 of file z3py.py.

eq

eq

Definition at line 11922 of file z3py.py.

Referenced by AstRef.__eq__(), and SortRef.cast().

final

final

Definition at line 11921 of file z3py.py.

fixed

fixed

Definition at line 11920 of file z3py.py.

fresh_ctx

fresh_ctx

Definition at line 11917 of file z3py.py.

id

id

Definition at line 11919 of file z3py.py.

solver

solver

Definition at line 11915 of file z3py.py.

Referenced by Solver.__del__(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.check(), Solver.model(), Solver.num_scopes(), Solver.pop(), Solver.push(), Solver.reset(), and Solver.set().