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	add_on_binding (self, binding)
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
	binding

Detailed Description

Definition at line 12012 of file z3py.py.

Constructor & Destructor Documentation

def __init__	(		self,
			s,
			ctx = None
	)

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

def __del__

(

self

)

Definition at line 12046 of file z3py.py.

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

Member Function Documentation

def add	(		self,
			e
	)

Definition at line 12131 of file z3py.py.

    def add(self, e):
        if self._ctx:
            raise Z3Exception("context already initialized")
        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 12068 of file z3py.py.

    def add_created(self, created):
        if self.created:
            raise Z3Exception("created callback already registered")
        if self._ctx:
            raise Z3Exception("context already initialized")
        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 12104 of file z3py.py.

    def add_decide(self, decide):
        if self.decide:
            raise Z3Exception("decide callback already registered")
        if self._ctx:
            raise Z3Exception("context already initialized")
        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 12095 of file z3py.py.

    def add_diseq(self, diseq):
        if self.diseq:
            raise Z3Exception("diseq callback already registered")
        if self._ctx:
            raise Z3Exception("context already initialized")
        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 12086 of file z3py.py.

    def add_eq(self, eq):
        if self.eq:
            raise Z3Exception("eq callback already registered")
        if self._ctx:
            raise Z3Exception("context already initialized")
        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 12077 of file z3py.py.

    def add_final(self, final):
        if self.final:
            raise Z3Exception("final callback already registered")
        if self._ctx:
            raise Z3Exception("context already initialized")
        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 12059 of file z3py.py.

    def add_fixed(self, fixed):
        if self.fixed:
            raise Z3Exception("fixed callback already registered")
        if self._ctx:
            raise Z3Exception("context already initialized")
        if self.solver:
            Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
        self.fixed = fixed

def add_on_binding	(		self,
			binding
	)

Definition at line 12113 of file z3py.py.

    def add_on_binding(self, binding):
        if self.binding:
            raise Z3Exception("binding callback already registered")
        if self._ctx:
            raise Z3Exception("context already initialized")
        if self.solver:
            Z3_solver_propagate_on_binding(self.ctx_ref(), self.solver.solver, _user_prop_binding)
        self.binding = binding

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

Definition at line 12158 of file z3py.py.

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

def ctx

(

self

)

Definition at line 12050 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 12056 of file z3py.py.

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

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

def fresh	(		self,
			new_ctx
	)

Definition at line 12128 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 12144 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 12125 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 12150 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 12122 of file z3py.py.

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

Field Documentation

binding

Definition at line 12035 of file z3py.py.

Referenced by UserPropagateBase.add_on_binding().

cb

Definition at line 12027 of file z3py.py.

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

created

Definition at line 12034 of file z3py.py.

Referenced by UserPropagateBase.add_created().

decide

Definition at line 12033 of file z3py.py.

Referenced by UserPropagateBase.add_decide().

diseq

Definition at line 12032 of file z3py.py.

Referenced by UserPropagateBase.add_diseq().

eq

Definition at line 12031 of file z3py.py.

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

final

Definition at line 12030 of file z3py.py.

Referenced by UserPropagateBase.add_final().

fixed

Definition at line 12029 of file z3py.py.

Referenced by UserPropagateBase.add_fixed().

fresh_ctx

Definition at line 12026 of file z3py.py.

Referenced by UserPropagateBase.ctx().

id

Definition at line 12028 of file z3py.py.

solver

Definition at line 12024 of file z3py.py.

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

---

Generated on Sun Apr 26 2026 02:49:44 for Z3 by   1.8.10