Z3 |

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 31 of file Pattern.cs.

## Member Function Documentation

## ◆ ToString()

override string ToString | ( |  | ) |
| inline

A string representation of the pattern.

Definition at line 60 of file Pattern.cs.

61 {
62 return Native.Z3_pattern_to_string(Context.nCtx, NativeObject);
63 }

## Property Documentation

## ◆ NumTerms

uint NumTerms
| get

The number of terms in the pattern.

Definition at line 36 of file Pattern.cs.

37 {
38 get { return Native.Z3_get_pattern_num_terms(Context.nCtx, NativeObject); }
39 }

## ◆ Terms

Expr [] Terms
| get

The terms in the pattern.

Definition at line 44 of file Pattern.cs.

45 {
46 get
47 {
48
49 uint n = NumTerms;
50 Expr[] res = new Expr[n];
51 for (uint i = 0; i < n; i++)
52 res[i] = Expr.Create(Context, Native.Z3_get_pattern(Context.nCtx, NativeObject, i));
53 return res;
54 }
55 }
Microsoft.Z3.Pattern.NumTerms
uint NumTerms
The number of terms in the pattern.
Definition: Pattern.cs:37