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 (Object 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	toString ()
String	getSExpr ()
Public Member Functions inherited from Z3Object
void	dispose ()
Public Member Functions inherited from IDisposable
void	dispose ()

Additional Inherited Members
Protected Member Functions inherited from Z3Object
void	finalize ()

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

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

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

String toString ( )

inline

A string representation of the pattern.

Definition at line 53 of file Pattern.java.

    {
        try
        {
            return Native.patternToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }