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 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  }

◆ 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  }
com.microsoft.z3.Pattern.getNumTerms
int getNumTerms()
Definition: Pattern.java:29