Z3 |

Public Member Functions
Pattern Class Reference
Inheritance diagram for Pattern:

## Public Member Functions
int | getNumTerms ()
Expr<?>[] | getTerms ()
String | toString ()
Public Member Functions inherited from AST
boolean | equals (Object o)
int | compareTo (AST other)
int | hashCode ()
int | getId ()
AST | translate (Context ctx)
Z3_ast_kind | getASTKind ()
boolean | isExpr ()
boolean | isApp ()
boolean | isVar ()
boolean | isQuantifier ()
boolean | isSort ()
boolean | isFuncDecl ()
String | toString ()
String | getSExpr ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## 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 24 of file Pattern.java.

## Member Function Documentation

## ◆ getNumTerms()

int getNumTerms | ( |  | ) |
| inline

The number of terms in the pattern.

Definition at line 29 of file Pattern.java.

30 {
31 return Native.getPatternNumTerms(getContext().nCtx(), getNativeObject());
32 }

Referenced by Pattern.getTerms().

## ◆ getTerms()

Expr<?>[] getTerms | ( |  | ) |
| inline

The terms in the pattern.

Exceptions

  Z3Exception |

Definition at line 39 of file Pattern.java.

40 {
41
42 int n = getNumTerms();
43 Expr<?>[] res = new Expr[n];
44 for (int i = 0; i < n; i++)
45 res[i] = Expr.create(getContext(),
46 Native.getPattern(getContext().nCtx(), getNativeObject(), i));
47 return res;
48 }
com.microsoft.z3.Pattern.getNumTerms
int getNumTerms()
Definition: Pattern.java:29

## ◆ toString()

String toString | ( |  | ) |
| inline

A string representation of the pattern.

Reimplemented from AST.

Definition at line 54 of file Pattern.java.

55 {
56 return Native.patternToString(getContext().nCtx(), getNativeObject());
57 }