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 ()
 

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.

Referenced by Pattern.getTerms().

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

§ 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.

Definition at line 54 of file Pattern.java.

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