Public Member Functions | |
int | getNumTerms () throws Z3Exception |
Expr[] | getTerms () throws Z3Exception |
String | toString () |
![]() | |
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 |
![]() | |
void | dispose () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
Additional Inherited Members | |
![]() | |
void | finalize () 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.
|
inline |
The number of terms in the pattern.
Definition at line 29 of file Pattern.java.
Referenced by Pattern.getTerms().
|
inline |
|
inline |
A string representation of the pattern.
Definition at line 53 of file Pattern.java.