PatternRef Class Reference

Patterns. More...

Inheritance diagram for PatternRef:

Public Member Functions
def	as_ast (self)
def	get_id (self)
Public Member Functions inherited from ExprRef
def	sort (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

Patterns.

Patterns are hints for quantifier instantiation.

Definition at line 1961 of file z3py.py.

Member Function Documentation

as_ast()

def as_ast

(

self

)

Return a pointer to the corresponding C Z3_ast object.

Reimplemented from ExprRef.

Definition at line 1966 of file z3py.py.

    def as_ast(self):
        return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
 

Referenced by AstRef.__del__(), SeqRef.__ge__(), SeqRef.__getitem__(), SeqRef.__gt__(), BitVecRef.__invert__(), SeqRef.__le__(), CharRef.__le__(), SeqRef.__lt__(), ArithRef.__neg__(), BitVecRef.__neg__(), AlgebraicNumRef.approx(), ExprRef.arg(), IntNumRef.as_binary_string(), BitVecNumRef.as_binary_string(), RatNumRef.as_decimal(), AlgebraicNumRef.as_decimal(), IntNumRef.as_string(), RatNumRef.as_string(), BitVecNumRef.as_string(), FiniteDomainRef.as_string(), FiniteDomainNumRef.as_string(), FPRef.as_string(), FPRMRef.as_string(), FPNumRef.as_string(), SeqRef.as_string(), SeqRef.at(), ExprRef.decl(), ArrayRef.default(), RatNumRef.denominator(), AstRef.eq(), FPNumRef.exponent(), FPNumRef.exponent_as_bv(), FPNumRef.exponent_as_long(), AstRef.get_id(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), PatternRef.get_id(), QuantifierRef.get_id(), AstRef.hash(), AlgebraicNumRef.index(), CharRef.is_digit(), SeqRef.is_string(), SeqRef.is_string_value(), FPNumRef.isInf(), FPNumRef.isNaN(), FPNumRef.isNegative(), FPNumRef.isNormal(), FPNumRef.isPositive(), FPNumRef.isSubnormal(), FPNumRef.isZero(), ExprRef.num_args(), RatNumRef.numerator(), AlgebraicNumRef.poly(), AstRef.sexpr(), FPNumRef.sign(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPNumRef.significand_as_long(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), FiniteDomainRef.sort(), FPRef.sort(), SeqRef.sort(), CharRef.to_bv(), CharRef.to_int(), and AstRef.translate().

get_id()

def get_id

(

self

)

Return unique identifier for object. It can be used for hash-tables and maps.

Reimplemented from ExprRef.

Definition at line 1969 of file z3py.py.

    def get_id(self):
        return Z3_get_ast_id(self.ctx_ref(), self.as_ast())