UserPropagateBase Class Reference

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

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

Detailed Description

Definition at line 11700 of file z3py.py.

Constructor & Destructor Documentation

__init__()

def __init__	(		self,
			s,
			ctx = None
	)

Definition at line 11709 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.created = 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__()

def __del__

(

self

)

Definition at line 11732 of file z3py.py.

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

Member Function Documentation

add()

def add	(		self,
			e
	)

Definition at line 11796 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__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

add_created()

def add_created	(		self,
			created
	)

Definition at line 11752 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()

def add_decide	(		self,
			decide
	)

Definition at line 11780 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()

def add_diseq	(		self,
			diseq
	)

Definition at line 11773 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()

def add_eq	(		self,
			eq
	)

Definition at line 11766 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()

def add_final	(		self,
			final
	)

Definition at line 11759 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()

def add_fixed	(		self,
			fixed
	)

Definition at line 11745 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
 

conflict()

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

Definition at line 11822 of file z3py.py.

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

ctx()

def ctx

(

self

)

Definition at line 11736 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__(), 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__(), Simplifier.__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__(), Simplifier.__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(), Simplifier.add(), 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(), Simplifier.help(), Tactic.help(), Solver.import_model_converter(), Goal.inconsistent(), Solver.interrupt(), 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(), Simplifier.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(), QuantifierRef.qid(), 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(), Solver.set_initial_value(), Optimize.set_initial_value(), 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(), QuantifierRef.skolem_id(), 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(), Simplifier.using_params(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

ctx_ref()

def ctx_ref

(

self

)

Definition at line 11742 of file z3py.py.

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

Referenced by BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), ArithRef.__div__(), BitVecRef.__div__(), SortRef.__eq__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), SeqRef.__ge__(), SeqRef.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), SeqRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), SeqRef.__le__(), CharRef.__le__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), SeqRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BitVecRef.__mul__(), SortRef.__ne__(), ExprRef.__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(), UserPropagateBase.add(), UserPropagateBase.add_created(), UserPropagateBase.add_decide(), UserPropagateBase.add_diseq(), UserPropagateBase.add_eq(), UserPropagateBase.add_final(), UserPropagateBase.add_fixed(), AlgebraicNumRef.approx(), ExprRef.arg(), FuncDeclRef.arity(), SortRef.as_ast(), FuncDeclRef.as_ast(), PatternRef.as_ast(), IntNumRef.as_binary_string(), BitVecNumRef.as_binary_string(), RatNumRef.as_decimal(), AlgebraicNumRef.as_decimal(), IntNumRef.as_string(), RatNumRef.as_string(), BitVecNumRef.as_string(), FiniteDomainRef.as_string(), FiniteDomainNumRef.as_string(), FPRef.as_string(), FPRMRef.as_string(), SeqRef.as_string(), SeqRef.at(), SeqSortRef.basis(), ReSortRef.basis(), QuantifierRef.body(), DatatypeSortRef.constructor(), ExprRef.decl(), ArrayRef.default(), RatNumRef.denominator(), ArraySortRef.domain(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FPSortRef.ebits(), AstRef.eq(), AstRef.get_id(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), PatternRef.get_id(), QuantifierRef.get_id(), AstRef.hash(), AlgebraicNumRef.index(), CharRef.is_digit(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), QuantifierRef.is_lambda(), SeqSortRef.is_string(), SeqRef.is_string(), SeqRef.is_string_value(), FuncDeclRef.kind(), SortRef.name(), FuncDeclRef.name(), UserPropagateBase.next_split(), QuantifierRef.no_pattern(), ExprRef.num_args(), DatatypeSortRef.num_constructors(), QuantifierRef.num_no_patterns(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), RatNumRef.numerator(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), QuantifierRef.qid(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), FPSortRef.sbits(), AstRef.sexpr(), BitVecSortRef.size(), FiniteDomainSortRef.size(), QuantifierRef.skolem_id(), BoolRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), FiniteDomainRef.sort(), FPRef.sort(), SeqRef.sort(), CharRef.to_bv(), CharRef.to_int(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

fresh()

def fresh	(		self,
			new_ctx
	)

Definition at line 11793 of file z3py.py.

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

next_split()

def next_split	(		self,
			t,
			idx,
			phase
	)

Definition at line 11808 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()

def pop	(		self,
			num_scopes
	)

Definition at line 11790 of file z3py.py.

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

Referenced by Solver.__exit__().

propagate()

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

Definition at line 11814 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)
 

Referenced by UserPropagateBase.conflict().

push()

def push

(

self

)

Definition at line 11787 of file z3py.py.

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

Referenced by Solver.__enter__().

Field Documentation

cb

cb

Definition at line 11715 of file z3py.py.

Referenced by UserPropagateBase.add(), UserPropagateBase.next_split(), and UserPropagateBase.propagate().

created

created

Definition at line 11721 of file z3py.py.

Referenced by UserPropagateBase.add_created().

decide

decide

Definition at line 11785 of file z3py.py.

Referenced by UserPropagateBase.add_decide().

diseq

diseq

Definition at line 11720 of file z3py.py.

Referenced by UserPropagateBase.add_diseq().

eq

eq

Definition at line 11719 of file z3py.py.

Referenced by AstRef.__eq__(), UserPropagateBase.add_eq(), SortRef.cast(), and BoolSortRef.cast().

final

final

Definition at line 11718 of file z3py.py.

Referenced by UserPropagateBase.add_final().

fixed

fixed

Definition at line 11717 of file z3py.py.

Referenced by UserPropagateBase.add_fixed().

fresh_ctx

fresh_ctx

Definition at line 11714 of file z3py.py.

Referenced by UserPropagateBase.ctx().

id

id

Definition at line 11716 of file z3py.py.

solver

solver

Definition at line 11712 of file z3py.py.

Referenced by Solver.__del__(), UserPropagateBase.add(), UserPropagateBase.add_created(), UserPropagateBase.add_decide(), UserPropagateBase.add_diseq(), UserPropagateBase.add_eq(), UserPropagateBase.add_final(), UserPropagateBase.add_fixed(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.assertions(), Solver.check(), Solver.consequences(), UserPropagateBase.ctx(), Solver.dimacs(), Solver.from_file(), Solver.from_string(), Solver.help(), Solver.import_model_converter(), Solver.interrupt(), Solver.model(), Solver.next(), Solver.non_units(), Solver.num_scopes(), Solver.param_descrs(), Solver.pop(), Solver.proof(), Solver.push(), Solver.reason_unknown(), Solver.reset(), Solver.root(), Solver.set(), Solver.set_initial_value(), Solver.sexpr(), Solver.statistics(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), and Solver.unsat_core().