Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions | Properties
Pattern Class Reference

Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern. More...

+ Inheritance diagram for Pattern:

Public Member Functions

override string ToString ()
 A string representation of the pattern. More...
 
- Public Member Functions inherited from AST
override bool Equals (object o)
 Object comparison. More...
 
virtual int CompareTo (object other)
 Object Comparison. More...
 
override int GetHashCode ()
 The AST's hash code. More...
 
AST Translate (Context ctx)
 Translates (copies) the AST to the Context ctx . More...
 
override string ToString ()
 A string representation of the AST. More...
 
string SExpr ()
 A string representation of the AST in s-expression notation. More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 

Properties

uint NumTerms [get]
 The number of terms in the pattern. More...
 
Expr[] Terms [get]
 The terms in the pattern. More...
 
- Properties inherited from AST
uint Id [get]
 A unique identifier for the AST (unique among all ASTs). More...
 
Z3_ast_kind ASTKind [get]
 The kind of the AST. More...
 
bool IsExpr [get]
 Indicates whether the AST is an Expr More...
 
bool IsApp [get]
 Indicates whether the AST is an application More...
 
bool IsVar [get]
 Indicates whether the AST is a BoundVariable More...
 
bool IsQuantifier [get]
 Indicates whether the AST is a Quantifier More...
 
bool IsSort [get]
 Indicates whether the AST is a Sort More...
 
bool IsFuncDecl [get]
 Indicates whether the AST is a FunctionDeclaration More...
 

Additional Inherited Members

- Static Public Member Functions inherited from AST
static bool operator== (AST a, AST b)
 Comparison operator. More...
 
static bool operator!= (AST a, AST b)
 Comparison operator. More...
 

Detailed Description

Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern.

Definition at line 32 of file Pattern.cs.

Member Function Documentation

override string ToString ( )
inline

A string representation of the pattern.

Definition at line 62 of file Pattern.cs.

63  {
64  return Native.Z3_pattern_to_string(Context.nCtx, NativeObject);
65  }

Property Documentation

uint NumTerms
get

The number of terms in the pattern.

Definition at line 38 of file Pattern.cs.

Expr [] Terms
get

The terms in the pattern.

Definition at line 46 of file Pattern.cs.