Inheritance diagram for Quantifier:

Public Member Functions
boolean	isUniversal ()

boolean	isExistential ()

int	getWeight ()

int	getNumPatterns ()

Pattern[]	getPatterns ()

int	getNumNoPatterns ()

Pattern[]	getNoPatterns ()

int	getNumBound ()

Symbol[]	getBoundVariableNames ()

Sort[]	getBoundVariableSorts ()

BoolExpr	getBody ()

Quantifier	translate (Context ctx)

Public Member Functions inherited from Expr< BoolSort >
Expr< R >	simplify ()

Expr< R >	simplify (Params p)

FuncDecl< R >	getFuncDecl ()

Z3_lbool	getBoolValue ()

int	getNumArgs ()

Expr<?>[]	getArgs ()

Expr< R >	update (Expr<?>[] args)

Expr< R >	substitute (Expr<?>[] from, Expr<?>[] to)

Expr< R >	substitute (Expr<?> from, Expr<?> to)

Expr< R >	substituteVars (Expr<?>[] to)

Expr< R >	translate (Context ctx)

String	toString ()

boolean	isNumeral ()

boolean	isWellSorted ()

R	getSort ()

boolean	isConst ()

boolean	isIntNum ()

boolean	isRatNum ()

boolean	isAlgebraicNumber ()

boolean	isBool ()

boolean	isTrue ()

boolean	isFalse ()

boolean	isEq ()

boolean	isDistinct ()

boolean	isITE ()

boolean	isAnd ()

boolean	isOr ()

boolean	isIff ()

boolean	isXor ()

boolean	isNot ()

boolean	isImplies ()

boolean	isInt ()

boolean	isReal ()

boolean	isArithmeticNumeral ()

boolean	isLE ()

boolean	isGE ()

boolean	isLT ()

boolean	isGT ()

boolean	isAdd ()

boolean	isSub ()

boolean	isUMinus ()

boolean	isMul ()

boolean	isDiv ()

boolean	isIDiv ()

boolean	isRemainder ()

boolean	isModulus ()

boolean	isIntToReal ()

boolean	isRealToInt ()

boolean	isRealIsInt ()

boolean	isArray ()

boolean	isStore ()

boolean	isSelect ()

boolean	isConstantArray ()

boolean	isDefaultArray ()

boolean	isArrayMap ()

boolean	isAsArray ()

boolean	isSetUnion ()

boolean	isSetIntersect ()

boolean	isSetDifference ()

boolean	isSetComplement ()

boolean	isSetSubset ()

boolean	isBV ()

boolean	isBVNumeral ()

boolean	isBVBitOne ()

boolean	isBVBitZero ()

boolean	isBVUMinus ()

boolean	isBVAdd ()

boolean	isBVSub ()

boolean	isBVMul ()

boolean	isBVSDiv ()

boolean	isBVUDiv ()

boolean	isBVSRem ()

boolean	isBVURem ()

boolean	isBVSMod ()

boolean	isBVULE ()

boolean	isBVSLE ()

boolean	isBVUGE ()

boolean	isBVSGE ()

boolean	isBVULT ()

boolean	isBVSLT ()

boolean	isBVUGT ()

boolean	isBVSGT ()

boolean	isBVAND ()

boolean	isBVOR ()

boolean	isBVNOT ()

boolean	isBVXOR ()

boolean	isBVNAND ()

boolean	isBVNOR ()

boolean	isBVXNOR ()

boolean	isBVConcat ()

boolean	isBVSignExtension ()

boolean	isBVZeroExtension ()

boolean	isBVExtract ()

boolean	isBVRepeat ()

boolean	isBVReduceOR ()

boolean	isBVReduceAND ()

boolean	isBVComp ()

boolean	isBVShiftLeft ()

boolean	isBVShiftRightLogical ()

boolean	isBVShiftRightArithmetic ()

boolean	isBVRotateLeft ()

boolean	isBVRotateRight ()

boolean	isBVRotateLeftExtended ()

boolean	isBVRotateRightExtended ()

boolean	isIntToBV ()

boolean	isBVToInt ()

boolean	isBVCarry ()

boolean	isBVXOR3 ()

boolean	isLabel ()

boolean	isLabelLit ()

boolean	isString ()

String	getString ()

boolean	isConcat ()

boolean	isOEQ ()

boolean	isProofTrue ()

boolean	isProofAsserted ()

boolean	isProofGoal ()

boolean	isProofModusPonens ()

boolean	isProofReflexivity ()

boolean	isProofSymmetry ()

boolean	isProofTransitivity ()

boolean	isProofTransitivityStar ()

boolean	isProofMonotonicity ()

boolean	isProofQuantIntro ()

boolean	isProofDistributivity ()

boolean	isProofAndElimination ()

boolean	isProofOrElimination ()

boolean	isProofRewrite ()

boolean	isProofRewriteStar ()

boolean	isProofPullQuant ()

boolean	isProofPushQuant ()

boolean	isProofElimUnusedVars ()

boolean	isProofDER ()

boolean	isProofQuantInst ()

boolean	isProofHypothesis ()

boolean	isProofLemma ()

boolean	isProofUnitResolution ()

boolean	isProofIFFTrue ()

boolean	isProofIFFFalse ()

boolean	isProofCommutativity ()

boolean	isProofDefAxiom ()

boolean	isProofDefIntro ()

boolean	isProofApplyDef ()

boolean	isProofIFFOEQ ()

boolean	isProofNNFPos ()

boolean	isProofNNFNeg ()

boolean	isProofSkolemize ()

boolean	isProofModusPonensOEQ ()

boolean	isProofTheoryLemma ()

boolean	isRelation ()

boolean	isRelationStore ()

boolean	isEmptyRelation ()

boolean	isIsEmptyRelation ()

boolean	isRelationalJoin ()

boolean	isRelationUnion ()

boolean	isRelationWiden ()

boolean	isRelationProject ()

boolean	isRelationFilter ()

boolean	isRelationNegationFilter ()

boolean	isRelationRename ()

boolean	isRelationComplement ()

boolean	isRelationSelect ()

boolean	isRelationClone ()

boolean	isFiniteDomain ()

boolean	isFiniteDomainLT ()

int	getIndex ()

Static Public Member Functions
static Quantifier	of (Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)

static Quantifier	of (Context ctx, boolean isForall, Expr<?>[] bound, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)

Additional Inherited Members
Protected Member Functions inherited from Expr< BoolSort >
	Expr (Context ctx, long obj)

Detailed Description

Quantifier expressions.

Definition at line 25 of file Quantifier.java.

Member Function Documentation

◆ getBody()

BoolExpr getBody ( )

inline

The body of the quantifier.

Exceptions

Z3Exception

Definition at line 142 of file Quantifier.java.

     {
         return (BoolExpr) Expr.create(getContext(), Native.getQuantifierBody(getContext()
                 .nCtx(), getNativeObject()));
     }

◆ getBoundVariableNames()

Symbol [] getBoundVariableNames ( )

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

◆ getBoundVariableSorts()

Sort [] getBoundVariableSorts ( )

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

◆ getNoPatterns()

Pattern [] getNoPatterns ( )

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

◆ getNumBound()

int getNumBound ( )

inline

The number of bound variables.

Definition at line 102 of file Quantifier.java.

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

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

◆ getNumNoPatterns()

int getNumNoPatterns ( )

inline

The number of no-patterns.

Definition at line 78 of file Quantifier.java.

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

Referenced by Quantifier.getNoPatterns().

◆ getNumPatterns()

int getNumPatterns ( )

inline

The number of patterns.

Definition at line 54 of file Quantifier.java.

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

Referenced by Quantifier.getPatterns().

◆ getPatterns()

Pattern [] getPatterns ( )

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

◆ getWeight()

int getWeight ( )

inline

The weight of the quantifier.

Definition at line 46 of file Quantifier.java.

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

◆ isExistential()

boolean isExistential ( )

inline

Indicates whether the quantifier is existential.

Definition at line 38 of file Quantifier.java.

     {
         return Native.isQuantifierExists(getContext().nCtx(), getNativeObject());
     }

◆ isUniversal()

boolean isUniversal ( )

inline

Indicates whether the quantifier is universal.

Definition at line 30 of file Quantifier.java.

     {
         return Native.isQuantifierForall(getContext().nCtx(), getNativeObject());
     }

◆ of() [1/2]

static Quantifier of	(	Context	ctx,
		boolean	isForall,
		Expr<?>[]	bound,
		Expr< BoolSort >	body,
		int	weight,
		Pattern[]	patterns,
		Expr<?>[]	noPatterns,
		Symbol	quantifierID,
		Symbol	skolemID
	)

inlinestatic

Parameters

ctx	Context to create the quantifier on.
isForall	Quantifier type.
bound	Bound variables.
body	Body of the quantifier.
weight	Weight.
patterns	Nullable array of patterns.
noPatterns	Nullable array of noPatterns.
quantifierID	Nullable quantifier identifier.
skolemID	Nullable skolem identifier.

Definition at line 221 of file Quantifier.java.

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

◆ of() [2/2]

static Quantifier of	(	Context	ctx,
		boolean	isForall,
		Sort[]	sorts,
		Symbol[]	names,
		Expr< BoolSort >	body,
		int	weight,
		Pattern[]	patterns,
		Expr<?>[]	noPatterns,
		Symbol	quantifierID,
		Symbol	skolemID
	)

inlinestatic

Create a quantified expression.

Parameters

ctx	Context to create the quantifier on.
isForall	Quantifier type.
sorts	Sorts of bound variables.
names	Names of bound variables
body	Body of quantifier
weight	Weight used to indicate priority for quantifier instantiation
patterns	Nullable patterns
noPatterns	Nullable noPatterns
quantifierID	Nullable quantifierID
skolemID	Nullable skolemID

Definition at line 175 of file Quantifier.java.

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

Referenced by Context.mkExists(), and Context.mkForall().

◆ translate()

Quantifier translate ( Context ctx )

inline

Translates (copies) the quantifier to the Context

ctx

.

Parameters

ctx A context

Returns: A copy of the quantifier which is associated with
ctx

Exceptions

Z3Exception on error

Definition at line 156 of file Quantifier.java.

     {
         return (Quantifier) super.translate(ctx);
     }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Solver.__deepcopy__(), and Quantifier.translate().

Public Member Functions

Static Public Member Functions

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ getBody()

◆ getBoundVariableNames()

◆ getBoundVariableSorts()

◆ getNoPatterns()

◆ getNumBound()

◆ getNumNoPatterns()

◆ getNumPatterns()

◆ getPatterns()

◆ getWeight()

◆ isExistential()

◆ isUniversal()

◆ of() [1/2]

◆ of() [2/2]

◆ translate()