Pattern Class Reference

Inheritance diagram for Pattern:

Public Member Functions
int	getNumTerms () throws Z3Exception
Expr[]	getTerms () throws Z3Exception
String	toString ()
Public Member Functions inherited from AST
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
Public Member Functions inherited from Z3Object
void	dispose () throws Z3Exception
Public Member Functions inherited from IDisposable
void	dispose () throws Z3Exception

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

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

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