FiniteDomainRef Class Reference

Inheritance diagram for FiniteDomainRef:

Public Member Functions
def	sort (self)
def	as_string (self)
Public Member Functions inherited from ExprRef
def	as_ast (self)
def	get_id (self)
def	sort_kind (self)
def	__eq__ (self, other)
def	__hash__ (self)
def	__ne__ (self, other)
def	params (self)
def	decl (self)
def	num_args (self)
def	arg (self, idx)
def	children (self)
def	from_string (self, s)
def	serialize (self)
Public Member Functions inherited from AstRef
def	__init__ (self, ast, ctx=None)
def	__del__ (self)
def	__deepcopy__ (self, memo={})
def	__str__ (self)
def	__repr__ (self)
def	__nonzero__ (self)
def	__bool__ (self)
def	sexpr (self)
def	ctx_ref (self)
def	eq (self, other)
def	translate (self, target)
def	__copy__ (self)
def	hash (self)
Public Member Functions inherited from Z3PPObject
def	use_pp (self)

Additional Inherited Members
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

Finite-domain expressions.

Definition at line 7802 of file z3py.py.

Member Function Documentation

as_string()

def as_string

(

self

)

Return a Z3 floating point expression as a Python string.

Reimplemented in FiniteDomainNumRef.

Definition at line 7809 of file z3py.py.

    def as_string(self):
        """Return a Z3 floating point expression as a Python string."""
        return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
 
 

Referenced by IntNumRef.as_long(), BitVecNumRef.as_long(), and FiniteDomainNumRef.as_long().

sort()

def sort

(

self

)

Return the sort of the finite-domain expression `self`.

Reimplemented from ExprRef.

Definition at line 7805 of file z3py.py.

    def sort(self):
        """Return the sort of the finite-domain expression `self`."""
        return FiniteDomainSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
 

Referenced by FPNumRef.as_string(), ArrayRef.domain(), ArrayRef.domain_n(), FPRef.ebits(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), FPRef.sbits(), BitVecRef.size(), and ExprRef.sort_kind().