UserPropagateBase Class Reference

Public Member Functions
def	__init__
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
def	conflict

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

Detailed Description

Definition at line 11810 of file z3py.py.

Constructor & Destructor Documentation

def __init__	(		self,
			s,
			ctx = None
	)

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

def __del__

(

self

)

Definition at line 11843 of file z3py.py.

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

Member Function Documentation

def add	(		self,
			e
	)

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

def add_created	(		self,
			created
	)

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

def add_decide	(		self,
			decide
	)

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

def add_diseq	(		self,
			diseq
	)

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

def add_eq	(		self,
			eq
	)

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

def add_final	(		self,
			final
	)

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

def add_fixed	(		self,
			fixed
	)

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

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

Definition at line 11933 of file z3py.py.

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

def ctx

(

self

)

Definition at line 11847 of file z3py.py.

Referenced by UserPropagateBase.conflict().

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

def ctx_ref

(

self

)

Definition at line 11853 of file z3py.py.

Referenced by UserPropagateBase.add(), UserPropagateBase.add_created(), UserPropagateBase.add_decide(), UserPropagateBase.add_diseq(), UserPropagateBase.add_eq(), UserPropagateBase.add_final(), and UserPropagateBase.add_fixed().

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

def fresh	(		self,
			new_ctx
	)

Definition at line 11904 of file z3py.py.

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

def next_split	(		self,
			t,
			idx,
			phase
	)

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

def pop	(		self,
			num_scopes
	)

Definition at line 11901 of file z3py.py.

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

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

Definition at line 11925 of file z3py.py.

Referenced by UserPropagateBase.conflict().

    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)

def push

(

self

)

Definition at line 11898 of file z3py.py.

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

Field Documentation

cb

Definition at line 11825 of file z3py.py.

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

created

Definition at line 11832 of file z3py.py.

Referenced by UserPropagateBase.add_created().

decide

Definition at line 11831 of file z3py.py.

Referenced by UserPropagateBase.add_decide().

diseq

Definition at line 11830 of file z3py.py.

Referenced by UserPropagateBase.add_diseq().

eq

Definition at line 11829 of file z3py.py.

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

final

Definition at line 11828 of file z3py.py.

Referenced by UserPropagateBase.add_final().

fixed

Definition at line 11827 of file z3py.py.

Referenced by UserPropagateBase.add_fixed().

fresh_ctx

Definition at line 11824 of file z3py.py.

Referenced by UserPropagateBase.ctx().

id

Definition at line 11826 of file z3py.py.

solver

Definition at line 11822 of file z3py.py.

Referenced by UserPropagateBase.add(), UserPropagateBase.add_created(), UserPropagateBase.add_decide(), UserPropagateBase.add_diseq(), UserPropagateBase.add_eq(), UserPropagateBase.add_final(), and UserPropagateBase.add_fixed().

---

Generated on Fri Dec 19 2025 12:04:19 for Z3 by   1.8.10