Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
Pattern Class Reference
+ Inheritance diagram for Pattern:

Public Member Functions

int getNumTerms () throws Z3Exception
Expr[] getTerms () throws Z3Exception
String toString ()

Package Functions

 Pattern (Context ctx, long obj) 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.


Constructor & Destructor Documentation

Pattern ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 64 of file Pattern.java.

    {
        super(ctx, obj);
    }

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.

Reimplemented from AST.

Definition at line 53 of file Pattern.java.

    {
        try
        {
            return Native.patternToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines