Package com.microsoft.z3

Class Pattern

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Pattern

All Implemented Interfaces:

Comparable<AST>

public class Pattern
extends AST

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.

Method Summary

Modifier and Type	Method	Description
int	getNumTerms()	The number of terms in the pattern.
Expr<?>[]	getTerms()	The terms in the pattern.
String	toString()	A string representation of the pattern.

Methods inherited from class com.microsoft.z3.AST

compareTo, equals, getASTKind, getId, getSExpr, hashCode, isApp, isExpr, isFuncDecl, isQuantifier, isSort, isVar, translate

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Method Details

getNumTerms

public int getNumTerms()

The number of terms in the pattern.

getTerms

public Expr<?>[] getTerms()

The terms in the pattern.

Throws:

Z3Exception

toString

public String toString()

A string representation of the pattern.

Overrides:

toString in class AST