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

Public Member Functions

boolean isUniversal () throws Z3Exception
boolean isExistential () throws Z3Exception
int getWeight () throws Z3Exception
int getNumPatterns () throws Z3Exception
Pattern[] getPatterns () throws Z3Exception
int getNumNoPatterns () throws Z3Exception
Pattern[] getNoPatterns () throws Z3Exception
int getNumBound () throws Z3Exception
Symbol[] getBoundVariableNames () throws Z3Exception
Sort[] getBoundVariableSorts () throws Z3Exception
BoolExpr getBody () throws Z3Exception

Package Functions

 Quantifier (Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
 Quantifier (Context ctx, boolean isForall, Expr[] bound, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
 Quantifier (Context ctx, long obj) throws Z3Exception
void checkNativeObject (long obj) throws Z3Exception

Detailed Description

Quantifier expressions.

Definition at line 25 of file Quantifier.java.


Constructor & Destructor Documentation

Quantifier ( Context  ctx,
boolean  isForall,
Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception [inline, package]

Definition at line 148 of file Quantifier.java.

    {
        super(ctx);

        getContext().checkContextMatch(patterns);
        getContext().checkContextMatch(noPatterns);
        getContext().checkContextMatch(sorts);
        getContext().checkContextMatch(names);
        getContext().checkContextMatch(body);

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

        if (noPatterns == null && quantifierID == null && skolemID == null)
        {
            setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true
                    : false, weight, AST.arrayLength(patterns), AST
                    .arrayToNative(patterns), AST.arrayLength(sorts), AST
                    .arrayToNative(sorts), Symbol.arrayToNative(names), body
                    .getNativeObject()));
        } else
        {
            setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), 
                    (isForall) ? true : false, 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()));
        }
    }
Quantifier ( Context  ctx,
boolean  isForall,
Expr[]  bound,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception [inline, package]

Definition at line 184 of file Quantifier.java.

    {
        super(ctx);

        getContext().checkContextMatch(noPatterns);
        getContext().checkContextMatch(patterns);
        // Context().CheckContextMatch(bound);
        getContext().checkContextMatch(body);

        if (noPatterns == null && quantifierID == null && skolemID == null)
        {
            setNativeObject(Native.mkQuantifierConst(ctx.nCtx(),
                    (isForall) ? true : false, weight, AST.arrayLength(bound),
                    AST.arrayToNative(bound), AST.arrayLength(patterns),
                    AST.arrayToNative(patterns), body.getNativeObject()));
        } else
        {
            setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(),
                    (isForall) ? true : false, 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()));
        }
    }
Quantifier ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 213 of file Quantifier.java.

    {
        super(ctx, obj);
    }

Member Function Documentation

void checkNativeObject ( long  obj) throws Z3Exception [inline, package]

Reimplemented from Expr.

Definition at line 218 of file Quantifier.java.

    {
        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);
    }
BoolExpr getBody ( ) throws Z3Exception [inline]

The body of the quantifier.

Exceptions:
Z3Exception

Definition at line 142 of file Quantifier.java.

    {
        return new BoolExpr(getContext(), Native.getQuantifierBody(getContext()
                .nCtx(), getNativeObject()));
    }
Symbol [] getBoundVariableNames ( ) throws Z3Exception [inline]

The symbols for the bound variables.

Exceptions:
Z3Exception

Definition at line 112 of file Quantifier.java.

    {
        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;
    }
Sort [] getBoundVariableSorts ( ) throws Z3Exception [inline]

The sorts of the bound variables.

Exceptions:
Z3Exception

Definition at line 127 of file Quantifier.java.

    {
        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;
    }
Pattern [] getNoPatterns ( ) throws Z3Exception [inline]

The no-patterns.

Exceptions:
Z3Exception

Definition at line 89 of file Quantifier.java.

    {
        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;
    }
int getNumBound ( ) throws Z3Exception [inline]

The number of bound variables.

Definition at line 102 of file Quantifier.java.

Referenced by Quantifier.getBoundVariableNames(), and Quantifier.getBoundVariableSorts().

    {
        return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
    }
int getNumNoPatterns ( ) throws Z3Exception [inline]

The number of no-patterns.

Definition at line 78 of file Quantifier.java.

Referenced by Quantifier.getNoPatterns().

    {
        return Native.getQuantifierNumNoPatterns(getContext().nCtx(),
                getNativeObject());
    }
int getNumPatterns ( ) throws Z3Exception [inline]

The number of patterns.

Definition at line 54 of file Quantifier.java.

Referenced by Quantifier.getPatterns().

    {
        return Native
                .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject());
    }
Pattern [] getPatterns ( ) throws Z3Exception [inline]

The patterns.

Exceptions:
Z3Exception

Definition at line 65 of file Quantifier.java.

    {
        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;
    }
int getWeight ( ) throws Z3Exception [inline]

The weight of the quantifier.

Definition at line 46 of file Quantifier.java.

    {
        return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject());
    }
boolean isExistential ( ) throws Z3Exception [inline]

Indicates whether the quantifier is existential.

Definition at line 38 of file Quantifier.java.

    {
        return !isUniversal();
    }
boolean isUniversal ( ) throws Z3Exception [inline]

Indicates whether the quantifier is universal.

Definition at line 30 of file Quantifier.java.

Referenced by Quantifier.isExistential().

    {
        return Native.isQuantifierForall(getContext().nCtx(), getNativeObject());
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines