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