Pattern.java

Go to the documentation of this file.

package com.microsoft.z3;

public class Pattern extends AST
{
    public int getNumTerms()
    {
        return Native.getPatternNumTerms(getContext().nCtx(), getNativeObject());
    }

    public Expr[] getTerms()
    {

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

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

    Pattern(Context ctx, long obj)
    {
        super(ctx, obj);
    }
}