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

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

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.

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

Referenced by Pattern.getTerms().

getTerms()

Expr<?> [] getTerms ( )

inline

The terms in the pattern.

Exceptions

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;
    }

toString()

String toString ( )

inline

A string representation of the pattern.

Reimplemented from AST.

Definition at line 54 of file Pattern.java.

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