Quantifier.java

Go to the documentation of this file.

package com.microsoft.z3;

import com.microsoft.z3.enumerations.Z3_ast_kind;

public class Quantifier extends BoolExpr
{
    public boolean isUniversal()
    {
        return Native.isQuantifierForall(getContext().nCtx(), getNativeObject());
    }

    public boolean isExistential()
    {
        return !isUniversal();
    }

    public int getWeight()
    {
        return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject());
    }

    public int getNumPatterns()
    {
        return Native
                .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject());
    }

    public Pattern[] getPatterns()
    {
        int n = getNumPatterns();
        Pattern[] res = new Pattern[n];
        for (int i = 0; i < n; i++)
            res[i] = new Pattern(getContext(), Native.getQuantifierPatternAst(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }

    public int getNumNoPatterns()
    {
        return Native.getQuantifierNumNoPatterns(getContext().nCtx(),
                getNativeObject());
    }

    public Pattern[] getNoPatterns()
    {
        int n = getNumNoPatterns();
        Pattern[] res = new Pattern[n];
        for (int i = 0; i < n; i++)
            res[i] = new Pattern(getContext(), Native.getQuantifierNoPatternAst(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }

    public int getNumBound()
    {
        return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
    }

    public Symbol[] getBoundVariableNames()
    {
        int n = getNumBound();
        Symbol[] res = new Symbol[n];
        for (int i = 0; i < n; i++)
            res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }

    public Sort[] getBoundVariableSorts()
    {
        int n = getNumBound();
        Sort[] res = new Sort[n];
        for (int i = 0; i < n; i++)
            res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }

    public BoolExpr getBody()
    {
        return new BoolExpr(getContext(), Native.getQuantifierBody(getContext()
                .nCtx(), getNativeObject()));
    }

    public static Quantifier of(
            Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
            Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
            Symbol quantifierID, Symbol skolemID) {
        ctx.checkContextMatch(patterns);
        ctx.checkContextMatch(noPatterns);
        ctx.checkContextMatch(sorts);
        ctx.checkContextMatch(names);
        ctx.checkContextMatch(body);

        if (sorts.length != names.length) {
            throw new Z3Exception(
                    "Number of sorts does not match number of names");
        }

        long nativeObj;
        if (noPatterns == null && quantifierID == null && skolemID == null) {
            nativeObj = Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST
                    .arrayToNative(patterns), AST.arrayLength(sorts), AST
                    .arrayToNative(sorts), Symbol.arrayToNative(names), body
                    .getNativeObject());
        } else {
            nativeObj = Native.mkQuantifierEx(ctx.nCtx(),
                    (isForall), weight, AST.getNativeObject(quantifierID),
                    AST.getNativeObject(skolemID),
                    AST.arrayLength(patterns), AST.arrayToNative(patterns),
                    AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns),
                    AST.arrayLength(sorts), AST.arrayToNative(sorts),
                    Symbol.arrayToNative(names),
                    body.getNativeObject());
        }
        return new Quantifier(ctx, nativeObj);
    }


    public static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body,
            int weight, Pattern[] patterns, Expr[] noPatterns,
            Symbol quantifierID, Symbol skolemID) {
        ctx.checkContextMatch(noPatterns);
        ctx.checkContextMatch(patterns);
        ctx.checkContextMatch(body);

        long nativeObj;
        if (noPatterns == null && quantifierID == null && skolemID == null) {
            nativeObj = Native.mkQuantifierConst(ctx.nCtx(),
                isForall, weight, AST.arrayLength(bound),
                    AST.arrayToNative(bound), AST.arrayLength(patterns),
                    AST.arrayToNative(patterns), body.getNativeObject());
        } else {
            nativeObj = Native.mkQuantifierConstEx(ctx.nCtx(),
                isForall, weight,
                    AST.getNativeObject(quantifierID),
                    AST.getNativeObject(skolemID), AST.arrayLength(bound),
                    AST.arrayToNative(bound), AST.arrayLength(patterns),
                    AST.arrayToNative(patterns), AST.arrayLength(noPatterns),
                    AST.arrayToNative(noPatterns), body.getNativeObject());
        }
        return new Quantifier(ctx, nativeObj);
    }

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

    @Override
    void checkNativeObject(long obj) {
        if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
                .toInt()) {
            throw new Z3Exception("Underlying object is not a quantifier");
        }
        super.checkNativeObject(obj);
    }
}