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