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_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 (self, e, ids, eqs=[])
def	conflict (self, ids)

Data Fields
	solver
	cb
	id
	fixed
	final
	eq
	diseq

Detailed Description

Definition at line 11168 of file z3py.py.

Constructor & Destructor Documentation

__init__()

def __init__	(		self,
			s,
			ctx = None
	)

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

__del__()

def __del__

(

self

)

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

add_diseq()

def add_diseq	(		self,
			diseq
	)

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

add_eq()

def add_eq	(		self,
			eq
	)

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

add_final()

def add_final	(		self,
			final
	)

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

add_fixed()

def add_fixed	(		self,
			fixed
	)

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

conflict()

def conflict	(		self,
			ids
	)

Definition at line 11270 of file z3py.py.

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

ctx()

def ctx

(

self

)

Definition at line 11206 of file z3py.py.

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

Referenced by UserPropagateBase.conflict(), and UserPropagateBase.ctx_ref().

ctx_ref()

def ctx_ref

(

self

)

Definition at line 11212 of file z3py.py.

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

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

fresh()

def fresh

(

self

)

Definition at line 11245 of file z3py.py.

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

pop()

def pop	(		self,
			num_scopes
	)

Definition at line 11242 of file z3py.py.

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

propagate()

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

Definition at line 11256 of file z3py.py.

    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)
 

Referenced by UserPropagateBase.conflict().

push()

def push

(

self

)

Definition at line 11239 of file z3py.py.

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

Field Documentation

cb

cb

Definition at line 11182 of file z3py.py.

Referenced by UserPropagateBase.propagate().

diseq

diseq

Definition at line 11187 of file z3py.py.

Referenced by UserPropagateBase.add_diseq().

eq

eq

Definition at line 11186 of file z3py.py.

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

final

final

Definition at line 11185 of file z3py.py.

Referenced by UserPropagateBase.add_final().

fixed

fixed

Definition at line 11184 of file z3py.py.

Referenced by UserPropagateBase.add_fixed().

id

id

Definition at line 11183 of file z3py.py.

solver

solver

Definition at line 11180 of file z3py.py.

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