Public Member Functions | |
int | getNumTerms () throws Z3Exception |
Expr[] | getTerms () throws Z3Exception |
String | toString () |
Package Functions | |
Pattern (Context ctx, long obj) throws Z3Exception |
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.
Pattern | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 64 of file Pattern.java.
{ super(ctx, obj); }
int getNumTerms | ( | ) | throws Z3Exception [inline] |
The number of terms in the pattern.
Definition at line 29 of file Pattern.java.
Referenced by Pattern.getTerms().
{ return Native.getPatternNumTerms(getContext().nCtx(), getNativeObject()); }
Expr [] getTerms | ( | ) | throws Z3Exception [inline] |
The terms in the pattern.
Z3Exception |
Definition at line 39 of file Pattern.java.
{ int n = getNumTerms(); Expr[] res = new Expr[n]; for (int i = 0; i < n; i++) res[i] = Expr.create(getContext(), Native.getPattern(getContext().nCtx(), getNativeObject(), i)); return res; }
String toString | ( | ) | [inline] |
A string representation of the pattern.
Reimplemented from AST.
Definition at line 53 of file Pattern.java.
{ try { return Native.patternToString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }