Z3
Public Member Functions | Static Public Member Functions
Quantifier Class Reference
+ 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 ()
 
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.

143  {
144  return (BoolExpr) Expr.create(getContext(), Native.getQuantifierBody(getContext()
145  .nCtx(), getNativeObject()));
146  }
Expr(Context ctx, long obj)
Definition: Expr.java:2119

◆ getBoundVariableNames()

Symbol [] getBoundVariableNames ( )
inline

The symbols for the bound variables.

Exceptions
Z3Exception

Definition at line 112 of file Quantifier.java.

113  {
114  int n = getNumBound();
115  Symbol[] res = new Symbol[n];
116  for (int i = 0; i < n; i++)
117  res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
118  getContext().nCtx(), getNativeObject(), i));
119  return res;
120  }

◆ getBoundVariableSorts()

Sort [] getBoundVariableSorts ( )
inline

The sorts of the bound variables.

Exceptions
Z3Exception

Definition at line 127 of file Quantifier.java.

128  {
129  int n = getNumBound();
130  Sort[] res = new Sort[n];
131  for (int i = 0; i < n; i++)
132  res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
133  getContext().nCtx(), getNativeObject(), i));
134  return res;
135  }

◆ getNoPatterns()

Pattern [] getNoPatterns ( )
inline

The no-patterns.

Exceptions
Z3Exception

Definition at line 89 of file Quantifier.java.

90  {
91  int n = getNumNoPatterns();
92  Pattern[] res = new Pattern[n];
93  for (int i = 0; i < n; i++)
94  res[i] = new Pattern(getContext(), Native.getQuantifierNoPatternAst(
95  getContext().nCtx(), getNativeObject(), i));
96  return res;
97  }

◆ getNumBound()

int getNumBound ( )
inline

The number of bound variables.

Definition at line 102 of file Quantifier.java.

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

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

◆ getNumNoPatterns()

int getNumNoPatterns ( )
inline

The number of no-patterns.

Definition at line 78 of file Quantifier.java.

79  {
80  return Native.getQuantifierNumNoPatterns(getContext().nCtx(),
81  getNativeObject());
82  }

Referenced by Quantifier.getNoPatterns().

◆ getNumPatterns()

int getNumPatterns ( )
inline

The number of patterns.

Definition at line 54 of file Quantifier.java.

55  {
56  return Native
57  .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject());
58  }

Referenced by Quantifier.getPatterns().

◆ getPatterns()

Pattern [] getPatterns ( )
inline

The patterns.

Exceptions
Z3Exception

Definition at line 65 of file Quantifier.java.

66  {
67  int n = getNumPatterns();
68  Pattern[] res = new Pattern[n];
69  for (int i = 0; i < n; i++)
70  res[i] = new Pattern(getContext(), Native.getQuantifierPatternAst(
71  getContext().nCtx(), getNativeObject(), i));
72  return res;
73  }

◆ getWeight()

int getWeight ( )
inline

The weight of the quantifier.

Definition at line 46 of file Quantifier.java.

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

◆ isExistential()

boolean isExistential ( )
inline

Indicates whether the quantifier is existential.

Definition at line 38 of file Quantifier.java.

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

◆ isUniversal()

boolean isUniversal ( )
inline

Indicates whether the quantifier is universal.

Definition at line 30 of file Quantifier.java.

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

◆ 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
ctxContext to create the quantifier on.
isForallQuantifier type.
boundBound variables.
bodyBody of the quantifier.
weightWeight.
patternsNullable array of patterns.
noPatternsNullable array of noPatterns.
quantifierIDNullable quantifier identifier.
skolemIDNullable skolem identifier.

Definition at line 221 of file Quantifier.java.

223  {
224  ctx.checkContextMatch(noPatterns);
225  ctx.checkContextMatch(patterns);
226  ctx.checkContextMatch(body);
227 
228  long nativeObj;
229  if (noPatterns == null && quantifierID == null && skolemID == null) {
230  nativeObj = Native.mkQuantifierConst(ctx.nCtx(),
231  isForall, weight, AST.arrayLength(bound),
232  AST.arrayToNative(bound), AST.arrayLength(patterns),
233  AST.arrayToNative(patterns), body.getNativeObject());
234  } else {
235  nativeObj = Native.mkQuantifierConstEx(ctx.nCtx(),
236  isForall, weight,
237  AST.getNativeObject(quantifierID),
238  AST.getNativeObject(skolemID), AST.arrayLength(bound),
239  AST.arrayToNative(bound), AST.arrayLength(patterns),
240  AST.arrayToNative(patterns), AST.arrayLength(noPatterns),
241  AST.arrayToNative(noPatterns), body.getNativeObject());
242  }
243  return new Quantifier(ctx, nativeObj);
244  }

◆ 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
ctxContext to create the quantifier on.
isForallQuantifier type.
sortsSorts of bound variables.
namesNames of bound variables
bodyBody of quantifier
weightWeight used to indicate priority for qunatifier instantiation
patternsNullable patterns
noPatternsNullable noPatterns
quantifierIDNullable quantifierID
skolemIDNullable skolemID

Definition at line 175 of file Quantifier.java.

178  {
179  ctx.checkContextMatch(patterns);
180  ctx.checkContextMatch(noPatterns);
181  ctx.checkContextMatch(sorts);
182  ctx.checkContextMatch(names);
183  ctx.checkContextMatch(body);
184 
185  if (sorts.length != names.length) {
186  throw new Z3Exception(
187  "Number of sorts does not match number of names");
188  }
189 
190  long nativeObj;
191  if (noPatterns == null && quantifierID == null && skolemID == null) {
192  nativeObj = Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST
193  .arrayToNative(patterns), AST.arrayLength(sorts), AST
194  .arrayToNative(sorts), Symbol.arrayToNative(names), body
195  .getNativeObject());
196  } else {
197  nativeObj = Native.mkQuantifierEx(ctx.nCtx(),
198  (isForall), weight, AST.getNativeObject(quantifierID),
199  AST.getNativeObject(skolemID),
200  AST.arrayLength(patterns), AST.arrayToNative(patterns),
201  AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns),
202  AST.arrayLength(sorts), AST.arrayToNative(sorts),
203  Symbol.arrayToNative(names),
204  body.getNativeObject());
205  }
206  return new Quantifier(ctx, nativeObj);
207  }

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

◆ translate()

Quantifier translate ( Context  ctx)
inline

Translates (copies) the quantifier to the Context

ctx

.

Parameters
ctxA context
Returns
A copy of the quantifier which is associated with
ctx
Exceptions
Z3Exceptionon error

Definition at line 156 of file Quantifier.java.

157  {
158  return (Quantifier) super.translate(ctx);
159  }

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().