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_final (self, final)
def	add_eq (self, eq)
def	add_diseq (self, diseq)
def	push (self)
def	pop (self, num_scopes)
def	fresh (self)
def	add (self, e)
def	propagate
def	conflict (self, ids)

Data Fields
	solver
	cb
	id
	fixed
	final
	eq
	diseq

Detailed Description

Definition at line 11198 of file z3py.py.

Constructor & Destructor Documentation

def __init__	(		self,
			s,
			ctx = None
	)

Definition at line 11207 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.cb = None
        self.id = _prop_closures.insert(self)
        self.fixed = None
        self.final = None
        self.eq = None
        self.diseq = None
        if ctx:
            # TBD fresh is broken: ctx is not of the right type when we reach here.
            self._ctx = Context()
            #Z3_del_context(self._ctx.ctx)
            #self._ctx.ctx = ctx
            #self._ctx.eh = Z3_set_error_handler(ctx, z3_error_handler)
            #Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
        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 11233 of file z3py.py.

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

Member Function Documentation

def add	(		self,
			e
	)

Definition at line 11279 of file z3py.py.

    def add(self, e):
        assert self.solver
        assert not self._ctx
        return Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)

def add_diseq	(		self,
			diseq
	)

Definition at line 11264 of file z3py.py.

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

def add_eq	(		self,
			eq
	)

Definition at line 11258 of file z3py.py.

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

def add_final	(		self,
			final
	)

Definition at line 11252 of file z3py.py.

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

def add_fixed	(		self,
			fixed
	)

Definition at line 11246 of file z3py.py.

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

def conflict	(		self,
			ids
	)

Definition at line 11301 of file z3py.py.

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

def ctx

(

self

)

Definition at line 11237 of file z3py.py.

Referenced by UserPropagateBase.conflict().

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

def ctx_ref

(

self

)

Definition at line 11243 of file z3py.py.

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

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

def fresh

(

self

)

Definition at line 11276 of file z3py.py.

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

def pop	(		self,
			num_scopes
	)

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

Referenced by UserPropagateBase.conflict().

    def propagate(self, e, ids, eqs=[]):
        num_fixed = len(ids)
        _ids = (ctypes.c_uint * num_fixed)()
        for i in range(num_fixed):
            _ids[i] = ids[i]
        num_eqs = len(eqs)
        _lhs = (ctypes.c_uint * num_eqs)()
        _rhs = (ctypes.c_uint * num_eqs)()
        for i in range(num_eqs):
            _lhs[i] = eqs[i][0]
            _rhs[i] = eqs[i][1]
        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 11270 of file z3py.py.

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

Field Documentation

cb

Definition at line 11212 of file z3py.py.

Referenced by UserPropagateBase.propagate().

diseq

Definition at line 11217 of file z3py.py.

Referenced by UserPropagateBase.add_diseq().

eq

Definition at line 11216 of file z3py.py.

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

final

Definition at line 11215 of file z3py.py.

Referenced by UserPropagateBase.add_final().

fixed

Definition at line 11214 of file z3py.py.

Referenced by UserPropagateBase.add_fixed().

id

Definition at line 11213 of file z3py.py.

solver

Definition at line 11210 of file z3py.py.

Referenced by UserPropagateBase.add().

---

Generated on Mon Dec 20 2021 20:12:00 for Z3 by   1.8.10