Z3
Public Member Functions
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 as_ast (self)
 
def get_id (self)
 
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 kind (self)
 
def num_args (self)
 
def arg (self, idx)
 
def children (self)
 
def update (self, args)
 
def from_string (self, s)
 
def serialize (self)
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__ (self)
 
def __deepcopy__
 
def __str__ (self)
 
def __repr__ (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __nonzero__ (self)
 
def __bool__ (self)
 
def sexpr (self)
 
def as_ast (self)
 
def get_id (self)
 
def ctx_ref (self)
 
def eq (self, other)
 
def translate (self, target)
 
def __copy__ (self)
 
def hash (self)
 
def py_value (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 2054 of file z3py.py.

Member Function Documentation

def as_ast (   self)

Definition at line 2059 of file z3py.py.

2059  def as_ast(self):
2060  return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
2061 
Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p)
Convert a Z3_pattern into Z3_ast. This is just type casting.
def ctx_ref(self)
Definition: z3py.py:427
def as_ast(self)
Definition: z3py.py:2059
def get_id (   self)

Definition at line 2062 of file z3py.py.

2062  def get_id(self):
2063  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
2064 
2065 
def get_id(self)
Definition: z3py.py:2062
def as_ast(self)
Definition: z3py.py:419
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.
def ctx_ref(self)
Definition: z3py.py:427