Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
PatternRef Class Reference

Patterns. More...

+ Inheritance diagram for PatternRef:

Public Member Functions

def as_ast
def get_id

Detailed Description

Patterns.

Patterns are hints for quantifier instantiation. 

See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

Definition at line 1534 of file z3py.py.


Member Function Documentation

def as_ast (   self)
Return a pointer to the corresponding C Z3_ast object.

Reimplemented from ExprRef.

Definition at line 1539 of file z3py.py.

Referenced by BoolRef.sort().

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

def get_id (   self)
Return unique identifier for object. It can be used for hash-tables and maps.

Reimplemented from ExprRef.

Definition at line 1542 of file z3py.py.

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

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines