Z3
Public Member Functions
Pattern Class Reference
+ Inheritance diagram for Pattern:

Public Member Functions

int getNumTerms () throws Z3Exception
 
Expr[] getTerms () throws Z3Exception
 
String toString ()
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (Object other) throws Z3Exception
 
int hashCode ()
 
int getId () throws Z3Exception
 
AST translate (Context ctx) throws Z3Exception
 
Z3_ast_kind getASTKind () throws Z3Exception
 
boolean isExpr () throws Z3Exception
 
boolean isApp () throws Z3Exception
 
boolean isVar () throws Z3Exception
 
boolean isQuantifier () throws Z3Exception
 
boolean isSort () throws Z3Exception
 
boolean isFuncDecl () throws Z3Exception
 
String toString ()
 
String getSExpr () throws Z3Exception
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

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

int getNumTerms ( ) throws Z3Exception
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  }
Expr [] getTerms ( ) throws Z3Exception
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  }
String toString ( )
inline

A string representation of the pattern.

Definition at line 53 of file Pattern.java.

54  {
55  try
56  {
57  return Native.patternToString(getContext().nCtx(), getNativeObject());
58  } catch (Z3Exception e)
59  {
60  return "Z3Exception: " + e.getMessage();
61  }
62  }