Z3
Public Member Functions | Protected Member Functions
Expr Class Reference
+ Inheritance diagram for Expr:

Public Member Functions

Expr simplify ()
 
Expr simplify (Params p)
 
FuncDecl getFuncDecl ()
 
Z3_lbool getBoolValue ()
 
int getNumArgs ()
 
Expr[] getArgs ()
 
void update (Expr[] args)
 
Expr substitute (Expr[] from, Expr[] to)
 
Expr substitute (Expr from, Expr to)
 
Expr substituteVars (Expr[] to)
 
Expr translate (Context ctx)
 
String toString ()
 
boolean isNumeral ()
 
boolean isWellSorted ()
 
Sort 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 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 isProofPullQuantStar ()
 
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 isProofNNFStar ()
 
boolean isProofCNFStar ()
 
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 ()
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (Object other)
 
int hashCode ()
 
int getId ()
 
AST translate (Context ctx)
 
Z3_ast_kind getASTKind ()
 
boolean isExpr ()
 
boolean isApp ()
 
boolean isVar ()
 
boolean isQuantifier ()
 
boolean isSort ()
 
boolean isFuncDecl ()
 
String toString ()
 
String getSExpr ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Protected Member Functions

 Expr (Context ctx)
 
 Expr (Context ctx, long obj)
 
- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

Expressions are terms.

Definition at line 30 of file Expr.java.

Constructor & Destructor Documentation

Expr ( Context  ctx)
inlineprotected

Constructor for Expr

Definition at line 2107 of file Expr.java.

Referenced by Expr.Expr().

2108  {
2109  super(ctx);
2110  {
2111  }
2112  }
Expr ( Context  ctx,
long  obj 
)
inlineprotected

Constructor for Expr

Exceptions
Z3Exceptionon error

Definition at line 2118 of file Expr.java.

2119  {
2120  super(ctx, obj);
2121  {
2122  }
2123  }

Member Function Documentation

Expr [] getArgs ( )
inline

The arguments of the expression.

Exceptions
Z3Exceptionon error
Returns
an Expr[]

Definition at line 105 of file Expr.java.

Referenced by FuncInterp.toString().

106  {
107  int n = getNumArgs();
108  Expr[] res = new Expr[n];
109  for (int i = 0; i < n; i++)
110  res[i] = Expr.create(getContext(),
111  Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
112  return res;
113  }
Expr(Context ctx)
Definition: Expr.java:2107
Z3_lbool getBoolValue ( )
inline

Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF).

Exceptions
Z3Exceptionon error
Returns
a Z3_lbool

Definition at line 84 of file Expr.java.

85  {
86  return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
87  getNativeObject()));
88  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
FuncDecl getFuncDecl ( )
inline

The function declaration of the function that is applied in this expression.

Returns
a FuncDecl
Exceptions
Z3Exceptionon error

Definition at line 72 of file Expr.java.

Referenced by Model.getConstInterp(), Expr.isAdd(), Expr.isAnd(), Expr.isArithmeticNumeral(), Expr.isArrayMap(), Expr.isAsArray(), Expr.isBVAdd(), Expr.isBVAND(), Expr.isBVBitOne(), Expr.isBVBitZero(), Expr.isBVCarry(), Expr.isBVComp(), Expr.isBVConcat(), Expr.isBVExtract(), Expr.isBVMul(), Expr.isBVNAND(), Expr.isBVNOR(), Expr.isBVNOT(), Expr.isBVNumeral(), Expr.isBVOR(), Expr.isBVReduceAND(), Expr.isBVReduceOR(), Expr.isBVRepeat(), Expr.isBVRotateLeft(), Expr.isBVRotateLeftExtended(), Expr.isBVRotateRight(), Expr.isBVRotateRightExtended(), Expr.isBVSDiv(), Expr.isBVSGE(), Expr.isBVSGT(), Expr.isBVShiftLeft(), Expr.isBVShiftRightArithmetic(), Expr.isBVShiftRightLogical(), Expr.isBVSignExtension(), Expr.isBVSLE(), Expr.isBVSLT(), Expr.isBVSMod(), Expr.isBVSRem(), Expr.isBVSub(), Expr.isBVToInt(), Expr.isBVUDiv(), Expr.isBVUGE(), Expr.isBVUGT(), Expr.isBVULE(), Expr.isBVULT(), Expr.isBVUMinus(), Expr.isBVURem(), Expr.isBVXNOR(), Expr.isBVXOR(), Expr.isBVXOR3(), Expr.isBVZeroExtension(), Expr.isConst(), Expr.isConstantArray(), Expr.isDefaultArray(), Expr.isDistinct(), Expr.isDiv(), Expr.isEmptyRelation(), Expr.isEq(), Expr.isFalse(), Expr.isFiniteDomainLT(), Expr.isGE(), Expr.isGT(), Expr.isIDiv(), Expr.isIff(), Expr.isImplies(), Expr.isIntToBV(), Expr.isIntToReal(), Expr.isIsEmptyRelation(), Expr.isITE(), Expr.isLabel(), Expr.isLabelLit(), Expr.isLE(), Expr.isLT(), Expr.isModulus(), Expr.isMul(), Expr.isNot(), Expr.isOEQ(), Expr.isOr(), Expr.isProofAndElimination(), Expr.isProofApplyDef(), Expr.isProofAsserted(), Expr.isProofCNFStar(), Expr.isProofCommutativity(), Expr.isProofDefAxiom(), Expr.isProofDefIntro(), Expr.isProofDER(), Expr.isProofDistributivity(), Expr.isProofElimUnusedVars(), Expr.isProofGoal(), Expr.isProofHypothesis(), Expr.isProofIFFFalse(), Expr.isProofIFFOEQ(), Expr.isProofIFFTrue(), Expr.isProofLemma(), Expr.isProofModusPonens(), Expr.isProofModusPonensOEQ(), Expr.isProofMonotonicity(), Expr.isProofNNFNeg(), Expr.isProofNNFPos(), Expr.isProofNNFStar(), Expr.isProofOrElimination(), Expr.isProofPullQuant(), Expr.isProofPullQuantStar(), Expr.isProofPushQuant(), Expr.isProofQuantInst(), Expr.isProofQuantIntro(), Expr.isProofReflexivity(), Expr.isProofRewrite(), Expr.isProofRewriteStar(), Expr.isProofSkolemize(), Expr.isProofSymmetry(), Expr.isProofTheoryLemma(), Expr.isProofTransitivity(), Expr.isProofTransitivityStar(), Expr.isProofTrue(), Expr.isProofUnitResolution(), Expr.isRealIsInt(), Expr.isRealToInt(), Expr.isRelationalJoin(), Expr.isRelationClone(), Expr.isRelationComplement(), Expr.isRelationFilter(), Expr.isRelationNegationFilter(), Expr.isRelationProject(), Expr.isRelationRename(), Expr.isRelationSelect(), Expr.isRelationStore(), Expr.isRelationUnion(), Expr.isRelationWiden(), Expr.isRemainder(), FPRMNum.isRNA(), FPRMNum.isRNE(), FPRMNum.isRoundNearestTiesToAway(), FPRMNum.isRoundNearestTiesToEven(), FPRMNum.isRoundTowardNegative(), FPRMNum.isRoundTowardPositive(), FPRMNum.isRoundTowardZero(), FPRMNum.isRTN(), FPRMNum.isRTP(), FPRMNum.isRTZ(), Expr.isSelect(), Expr.isSetComplement(), Expr.isSetDifference(), Expr.isSetIntersect(), Expr.isSetSubset(), Expr.isSetUnion(), Expr.isStore(), Expr.isSub(), Expr.isTrue(), Expr.isUMinus(), and Expr.isXor().

73  {
74  return new FuncDecl(getContext(), Native.getAppDecl(getContext().nCtx(),
75  getNativeObject()));
76  }
int getIndex ( )
inline

The de-Burijn index of a bound variable. Remarks: Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format.

abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
abs1(x, x, n) = b_n
abs1(y, x, n) = y
abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))

The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 2096 of file Expr.java.

2097  {
2098  if (!isVar())
2099  throw new Z3Exception("Term is not a bound variable.");
2100 
2101  return Native.getIndexValue(getContext().nCtx(), getNativeObject());
2102  }
boolean isVar()
Definition: AST.java:167
int getNumArgs ( )
inline

The number of arguments of the expression.

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 95 of file Expr.java.

Referenced by Expr.getArgs(), Expr.isConst(), and Expr.update().

96  {
97  return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
98  }
Sort getSort ( )
inline

The Sort of the term.

Exceptions
Z3Exceptionon error
Returns
a sort

Definition at line 241 of file Expr.java.

Referenced by FPExpr.getEBits(), FPExpr.getSBits(), and BitVecExpr.getSortSize().

242  {
243  return Sort.create(getContext(),
244  Native.getSort(getContext().nCtx(), getNativeObject()));
245  }
boolean isAdd ( )
inline

Indicates whether the term is addition (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 491 of file Expr.java.

492  {
494  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isAlgebraicNumber ( )
inline

Indicates whether the term is an algebraic number

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 282 of file Expr.java.

283  {
284  return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
285  }
boolean isAnd ( )
inline

Indicates whether the term is an n-ary conjunction

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 355 of file Expr.java.

356  {
358  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isArithmeticNumeral ( )
inline

Indicates whether the term is an arithmetic numeral.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 441 of file Expr.java.

442  {
444  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isArray ( )
inline

Indicates whether the term is of an array sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 602 of file Expr.java.

603  {
604  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
605  .fromInt(Native.getSortKind(getContext().nCtx(),
606  Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
607  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:194
boolean isArrayMap ( )
inline

Indicates whether the term is an array map. Remarks: It satisfies mapf[i] = f(a1[i],...,a_n[i]) for every i.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 659 of file Expr.java.

660  {
662  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isAsArray ( )
inline

Indicates whether the term is an as-array term. Remarks: An as-array term * is n array value that behaves as the function graph of the function * passed as parameter.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 670 of file Expr.java.

671  {
673  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBool ( )
inline

Indicates whether the term has Boolean sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 292 of file Expr.java.

293  {
294  return (isExpr() && Native.isEqSort(getContext().nCtx(),
295  Native.mkBoolSort(getContext().nCtx()),
296  Native.getSort(getContext().nCtx(), getNativeObject())));
297  }
boolean isExpr()
Definition: AST.java:138
boolean isBV ( )
inline

Indicates whether the terms is of bit-vector sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 730 of file Expr.java.

731  {
732  return Native.getSortKind(getContext().nCtx(),
733  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
734  .toInt();
735  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:194
boolean isBVAdd ( )
inline

Indicates whether the term is a bit-vector addition (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 782 of file Expr.java.

783  {
785  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVAND ( )
inline

Indicates whether the term is a bit-wise AND

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 993 of file Expr.java.

994  {
996  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVBitOne ( )
inline

Indicates whether the term is a one-bit bit-vector with value one

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 752 of file Expr.java.

753  {
755  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVBitZero ( )
inline

Indicates whether the term is a one-bit bit-vector with value zero

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 762 of file Expr.java.

763  {
765  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVCarry ( )
inline

Indicates whether the term is a bit-vector carry Remarks: Compute the * carry bit in a full-adder. The meaning is given by the equivalence (carry * l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1242 of file Expr.java.

1243  {
1245  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVComp ( )
inline

Indicates whether the term is a bit-vector comparison

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1133 of file Expr.java.

1134  {
1136  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVConcat ( )
inline

Indicates whether the term is a bit-vector concatenation (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1063 of file Expr.java.

1064  {
1066  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVExtract ( )
inline

Indicates whether the term is a bit-vector extraction

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1093 of file Expr.java.

1094  {
1096  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVMul ( )
inline

Indicates whether the term is a bit-vector multiplication (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 802 of file Expr.java.

803  {
805  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVNAND ( )
inline

Indicates whether the term is a bit-wise NAND

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1033 of file Expr.java.

1034  {
1036  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVNOR ( )
inline

Indicates whether the term is a bit-wise NOR

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1043 of file Expr.java.

1044  {
1046  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVNOT ( )
inline

Indicates whether the term is a bit-wise NOT

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1013 of file Expr.java.

1014  {
1016  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVNumeral ( )
inline

Indicates whether the term is a bit-vector numeral

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 742 of file Expr.java.

743  {
745  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVOR ( )
inline

Indicates whether the term is a bit-wise OR

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1003 of file Expr.java.

1004  {
1005  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
1006  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVReduceAND ( )
inline

Indicates whether the term is a bit-vector reduce AND

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1123 of file Expr.java.

1124  {
1126  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVReduceOR ( )
inline

Indicates whether the term is a bit-vector reduce OR

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1113 of file Expr.java.

1114  {
1116  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVRepeat ( )
inline

Indicates whether the term is a bit-vector repetition

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1103 of file Expr.java.

1104  {
1106  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVRotateLeft ( )
inline

Indicates whether the term is a bit-vector rotate left

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1173 of file Expr.java.

1174  {
1176  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVRotateLeftExtended ( )
inline

Indicates whether the term is a bit-vector rotate left (extended) Remarks: Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1195 of file Expr.java.

1196  {
1198  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVRotateRight ( )
inline

Indicates whether the term is a bit-vector rotate right

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1183 of file Expr.java.

1184  {
1186  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVRotateRightExtended ( )
inline

Indicates whether the term is a bit-vector rotate right (extended) Remarks: Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1207 of file Expr.java.

1208  {
1210  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVSDiv ( )
inline

Indicates whether the term is a bit-vector signed division (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 812 of file Expr.java.

813  {
815  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVSGE ( )
inline

Indicates whether the term is a signed bit-vector greater-than-or-equal

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 943 of file Expr.java.

944  {
946  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVSGT ( )
inline

Indicates whether the term is a signed bit-vector greater-than

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 983 of file Expr.java.

984  {
986  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVShiftLeft ( )
inline

Indicates whether the term is a bit-vector shift left

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1143 of file Expr.java.

1144  {
1146  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVShiftRightArithmetic ( )
inline

Indicates whether the term is a bit-vector arithmetic shift left

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1163 of file Expr.java.

1164  {
1166  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVShiftRightLogical ( )
inline

Indicates whether the term is a bit-vector logical shift right

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1153 of file Expr.java.

1154  {
1156  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVSignExtension ( )
inline

Indicates whether the term is a bit-vector sign extension

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1073 of file Expr.java.

1074  {
1076  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVSLE ( )
inline

Indicates whether the term is a signed bit-vector less-than-or-equal

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 922 of file Expr.java.

923  {
925  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVSLT ( )
inline

Indicates whether the term is a signed bit-vector less-than

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 963 of file Expr.java.

964  {
966  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVSMod ( )
inline

Indicates whether the term is a bit-vector signed modulus

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 852 of file Expr.java.

853  {
855  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVSRem ( )
inline

Indicates whether the term is a bit-vector signed remainder (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 832 of file Expr.java.

833  {
835  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVSub ( )
inline

Indicates whether the term is a bit-vector subtraction (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 792 of file Expr.java.

793  {
795  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVToInt ( )
inline

Indicates whether the term is a coercion from bit-vector to integer

Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1231 of file Expr.java.

1232  {
1234  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVUDiv ( )
inline

Indicates whether the term is a bit-vector unsigned division (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 822 of file Expr.java.

823  {
825  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVUGE ( )
inline

Indicates whether the term is an unsigned bit-vector greater-than-or-equal

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 933 of file Expr.java.

934  {
936  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVUGT ( )
inline

Indicates whether the term is an unsigned bit-vector greater-than

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 973 of file Expr.java.

974  {
976  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVULE ( )
inline

Indicates whether the term is an unsigned bit-vector less-than-or-equal

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 912 of file Expr.java.

913  {
915  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVULT ( )
inline

Indicates whether the term is an unsigned bit-vector less-than

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 953 of file Expr.java.

954  {
956  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVUMinus ( )
inline

Indicates whether the term is a bit-vector unary minus

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 772 of file Expr.java.

773  {
775  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVURem ( )
inline

Indicates whether the term is a bit-vector unsigned remainder (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 842 of file Expr.java.

843  {
845  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVXNOR ( )
inline

Indicates whether the term is a bit-wise XNOR

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1053 of file Expr.java.

1054  {
1056  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVXOR ( )
inline

Indicates whether the term is a bit-wise XOR

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1023 of file Expr.java.

1024  {
1026  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVXOR3 ( )
inline

Indicates whether the term is a bit-vector ternary XOR Remarks: The * meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor * l1 l2) l3)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1253 of file Expr.java.

1254  {
1256  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isBVZeroExtension ( )
inline

Indicates whether the term is a bit-vector zero extension

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1083 of file Expr.java.

1084  {
1086  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isConst ( )
inline

Indicates whether the term represents a constant.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 252 of file Expr.java.

253  {
254  return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
255  }
boolean isApp()
Definition: AST.java:157
FuncDecl getFuncDecl()
Definition: Expr.java:72
boolean isConstantArray ( )
inline

Indicates whether the term is a constant array. Remarks: For example, * select(const(v),i) = v holds for every v and i. The function is * unary.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 636 of file Expr.java.

637  {
639  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isDefaultArray ( )
inline

Indicates whether the term is a default array. Remarks: For example default(const(v)) = v. The function is unary.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 647 of file Expr.java.

648  {
650  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isDistinct ( )
inline

Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 335 of file Expr.java.

336  {
338  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isDiv ( )
inline

Indicates whether the term is division (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 531 of file Expr.java.

532  {
534  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isEmptyRelation ( )
inline

Indicates whether the term is an empty relation

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1906 of file Expr.java.

1907  {
1909  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isEq ( )
inline

Indicates whether the term is an equality predicate.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 324 of file Expr.java.

325  {
327  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isFalse ( )
inline

Indicates whether the term is the constant false.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 314 of file Expr.java.

315  {
317  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isFiniteDomain ( )
inline

Indicates whether the term is of an array sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 2060 of file Expr.java.

2061  {
2062  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
2063  .getSortKind(getContext().nCtx(),
2064  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
2065  .toInt());
2066  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:194
boolean isFiniteDomainLT ( )
inline

Indicates whether the term is a less than predicate over a finite domain.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 2073 of file Expr.java.

2074  {
2076  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isGE ( )
inline

Indicates whether the term is a greater-than-or-equal

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 461 of file Expr.java.

462  {
464  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isGT ( )
inline

Indicates whether the term is a greater-than

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 481 of file Expr.java.

482  {
484  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isIDiv ( )
inline

Indicates whether the term is integer division (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 541 of file Expr.java.

542  {
544  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isIff ( )
inline

Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 376 of file Expr.java.

377  {
379  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isImplies ( )
inline

Indicates whether the term is an implication

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 406 of file Expr.java.

407  {
409  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isInt ( )
inline

Indicates whether the term is of integer sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 416 of file Expr.java.

Referenced by Expr.isIntNum().

417  {
418  return (Native.isNumeralAst(getContext().nCtx(), getNativeObject()) && Native
419  .getSortKind(getContext().nCtx(),
420  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT
421  .toInt());
422  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:194
boolean isIntNum ( )
inline

Indicates whether the term is an integer numeral.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 262 of file Expr.java.

263  {
264  return isNumeral() && isInt();
265  }
boolean isNumeral()
Definition: Expr.java:219
boolean isInt()
Definition: Expr.java:416
boolean isIntToBV ( )
inline

Indicates whether the term is a coercion from integer to bit-vector

Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1219 of file Expr.java.

1220  {
1222  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isIntToReal ( )
inline

Indicates whether the term is a coercion of integer to real (unary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 571 of file Expr.java.

572  {
574  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isIsEmptyRelation ( )
inline

Indicates whether the term is a test for the emptiness of a relation

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1916 of file Expr.java.

1917  {
1919  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isITE ( )
inline

Indicates whether the term is a ternary if-then-else term

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 345 of file Expr.java.

346  {
348  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isLabel ( )
inline

Indicates whether the term is a label (used by the Boogie Verification condition generator). Remarks: The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1266 of file Expr.java.

1267  {
1269  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isLabelLit ( )
inline

Indicates whether the term is a label literal (used by the Boogie Verification condition generator). Remarks: A label literal has a set of string parameters. It takes no arguments.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1279 of file Expr.java.

1280  {
1282  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isLE ( )
inline

Indicates whether the term is a less-than-or-equal

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 451 of file Expr.java.

452  {
454  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isLT ( )
inline

Indicates whether the term is a less-than

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 471 of file Expr.java.

472  {
474  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isModulus ( )
inline

Indicates whether the term is modulus (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 561 of file Expr.java.

562  {
564  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isMul ( )
inline

Indicates whether the term is multiplication (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 521 of file Expr.java.

522  {
524  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isNot ( )
inline

Indicates whether the term is a negation

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 396 of file Expr.java.

397  {
399  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isNumeral ( )
inline

Indicates whether the term is a numeral

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 219 of file Expr.java.

Referenced by Expr.isIntNum(), and Expr.isRatNum().

220  {
221  return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
222  }
boolean isOEQ ( )
inline

Indicates whether the term is a binary equivalence modulo namings. Remarks: This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1291 of file Expr.java.

1292  {
1293  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
1294  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isOr ( )
inline

Indicates whether the term is an n-ary disjunction

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 365 of file Expr.java.

366  {
368  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofAndElimination ( )
inline

Indicates whether the term is a proof by elimination of AND Remarks: * Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and * l_1 ... l_n) [and-elim T1]: l_i

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1452 of file Expr.java.

1453  {
1455  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofApplyDef ( )
inline

Indicates whether the term is a proof for application of a definition Remarks: [apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is a proof that n is a name for F.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1725 of file Expr.java.

1726  {
1728  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofAsserted ( )
inline

Indicates whether the term is a proof for a fact asserted by the user.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1311 of file Expr.java.

1312  {
1314  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofCNFStar ( )
inline

Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. Remarks: A proof for (~ P Q) where Q is in conjunctive normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1817 of file Expr.java.

1818  {
1820  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofCommutativity ( )
inline

Indicates whether the term is a proof by commutativity Remarks: [comm]: (= (f a b) (f b a))

f is a commutative operator.

This proof object has no antecedents. Remark: if f is bool, then = is iff.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1664 of file Expr.java.

1665  {
1667  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofDefAxiom ( )
inline

Indicates whether the term is a proof for Tseitin-like axioms Remarks: Proof object used to justify Tseitin's like axioms:

(or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p) (or (not (and p q r)) q) (or (not (and p q r)) r) ... (or (and p q) (not p) (not q)) (or (not (or p q)) p q) (or (or p q) (not p)) (or (or p q) (not q)) (or (not (iff p q)) (not p) q) (or (not (iff p q)) p (not q)) (or (iff p q) (not p) (not q)) (or (iff p q) p q) (or (not (ite a b c)) (not a) b) (or (not (ite a b c)) a c) (or (ite a b c) (not a) (not b)) (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a)

This proof object has no antecedents. Note: all axioms are propositional tautologies. Note also that 'and' and 'or' can take multiple arguments. You can recover the propositional tautologies by unfolding the Boolean connectives in the axioms a small bounded number of steps (=3).

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1690 of file Expr.java.

1691  {
1693  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofDefIntro ( )
inline

Indicates whether the term is a proof for introduction of a name Remarks: Introduces a name for a formula/term. Suppose e is an expression with free variables x, and def-intro introduces the name n(x). The possible cases are:

When e is of Boolean type: [def-intro]: (and (or n (not e)) (or (not n) e))

or: [def-intro]: (or (not n) e) when e only occurs positively.

When e is of the form (ite cond th el): [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))

Otherwise: [def-intro]: (= n e)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1713 of file Expr.java.

1714  {
1716  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofDER ( )
inline

Indicates whether the term is a proof for destructive equality resolution Remarks: A proof for destructive equality resolution: (iff (forall (x) (or (not (= x t)) P[x])) P[t]) if x does not occur in t.

This proof object has no antecedents.

Several variables can be eliminated simultaneously.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1572 of file Expr.java.

1573  {
1575  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofDistributivity ( )
inline

Indicates whether the term is a distributivity proof object. Remarks: Given that f (= or) distributes over g (= and), produces a proof for (= (f a (g c d)) (g (f a c) (f a d))) If f and g are associative, this proof also justifies the following equality: (= (f (g a b) (g c d)) (g (f a c) (f a d) (f b c) (f b d))) where each f and g can have arbitrary number of arguments.

This proof object has no antecedents. Remark. This rule is used by the CNF conversion pass and instantiated by f = or, and g = and.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1441 of file Expr.java.

1442  {
1444  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofElimUnusedVars ( )
inline

Indicates whether the term is a proof for elimination of unused variables. Remarks: A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) (forall (x_1 ... x_n) p[x_1 ... x_n]))

It is used to justify the elimination of unused variables. This proof object has no antecedents.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1556 of file Expr.java.

1557  {
1559  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofGoal ( )
inline

Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1322 of file Expr.java.

1323  {
1325  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofHypothesis ( )
inline

Indicates whether the term is a hypthesis marker. Remarks: Mark a hypothesis in a natural deduction style proof.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1596 of file Expr.java.

1597  {
1599  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofIFFFalse ( )
inline

Indicates whether the term is a proof by iff-false Remarks: T1: (not p) [iff-false T1]: (iff p false)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1647 of file Expr.java.

1648  {
1650  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofIFFOEQ ( )
inline

Indicates whether the term is a proof iff-oeq Remarks: T1: (iff p q) [iff~ T1]: (~ p q)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1737 of file Expr.java.

1738  {
1740  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofIFFTrue ( )
inline

Indicates whether the term is a proof by iff-true Remarks: T1: p [iff-true T1]: (iff p true)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1635 of file Expr.java.

1636  {
1638  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofLemma ( )
inline

Indicates whether the term is a proof by lemma Remarks: T1: false [lemma T1]: (or (not l_1) ... (not l_n))

This proof object has one antecedent: a hypothetical proof for false. It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the hypotheses: l_1, ..., l_n.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1612 of file Expr.java.

1613  {
1615  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofModusPonens ( )
inline

Indicates whether the term is proof via modus ponens Remarks: Given a proof for p and a proof for (implies p q), produces a proof for q. T1: p T2: (implies p q) [mp T1 T2]: q The second antecedents may also be a proof for (iff p q).

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1336 of file Expr.java.

1337  {
1339  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofModusPonensOEQ ( )
inline

Indicates whether the term is a proof by modus ponens for equi-satisfiability. Remarks: Modus ponens style rule for equi-satisfiability. T1: p T2: (~ p q) [mp~ T1 T2]: q

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1847 of file Expr.java.

1848  {
1850  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofMonotonicity ( )
inline

Indicates whether the term is a monotonicity proof object. Remarks: T1: (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are supressed to save space.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1411 of file Expr.java.

1412  {
1414  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofNNFNeg ( )
inline

Indicates whether the term is a proof for a negative NNF step Remarks: Proof for a (negative) NNF step. Examples:

T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n) and T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n) and T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2' [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1 r_2) (or r_1' r_2')))

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1784 of file Expr.java.

1785  {
1787  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofNNFPos ( )
inline

Indicates whether the term is a proof for a positive NNF step Remarks: Proof for a (positive) NNF step. Example:

T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2'

r_2)))

The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: (a) When creating the NNF of a positive force quantifier. The quantifier is retained (unless the bound variables are eliminated). Example T1: q ~ q_new [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))

(b) When recursively creating NNF over Boolean formulas, where the top-level connective is changed during NNF conversion. The relevant Boolean connectives for NNF_POS are 'implies', 'iff', 'xor', 'ite'. NNF_NEG furthermore handles the case where negation is pushed over Boolean connectives 'and' and 'or'.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1765 of file Expr.java.

1766  {
1768  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofNNFStar ( )
inline

Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. Remarks: A proof for (~ P Q) where Q is in negation normal form.

This proof object is only used if the parameter PROOF_MODE is 1.

This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1802 of file Expr.java.

1803  {
1805  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofOrElimination ( )
inline

Indicates whether the term is a proof by eliminiation of not-or Remarks: * Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). * T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1463 of file Expr.java.

1464  {
1466  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofPullQuant ( )
inline

Indicates whether the term is a proof for pulling quantifiers out. Remarks: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1514 of file Expr.java.

1515  {
1517  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofPullQuantStar ( )
inline

Indicates whether the term is a proof for pulling quantifiers out.

Remarks: A proof for (iff P Q) where Q is in prenex normal form. This * proof object is only used if the parameter PROOF_MODE is 1. This proof * object has no antecedents

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1526 of file Expr.java.

1527  {
1529  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofPushQuant ( )
inline

Indicates whether the term is a proof for pushing quantifiers in. Remarks: A proof for: (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) ... (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) This proof object has no antecedents

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1540 of file Expr.java.

1541  {
1543  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofQuantInst ( )
inline

Indicates whether the term is a proof for quantifier instantiation

Remarks: A proof of (or (not (forall (x) (P x))) (P a))

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1584 of file Expr.java.

1585  {
1587  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofQuantIntro ( )
inline

Indicates whether the term is a quant-intro proof Remarks: Given a proof * for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: * (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q))

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1422 of file Expr.java.

1423  {
1425  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofReflexivity ( )
inline

Indicates whether the term is a proof for (R t t), where R is a reflexive relation. Remarks: This proof object has no antecedents. The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. That is, R is either '~', '=' or 'iff'.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1351 of file Expr.java.

1352  {
1354  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofRewrite ( )
inline

Indicates whether the term is a proof by rewriting Remarks: A proof for a local rewriting step (= t s). The head function symbol of t is interpreted.

This proof object has no antecedents. The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s). Remark: if f is bool, then = is iff.

Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1483 of file Expr.java.

1484  {
1486  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofRewriteStar ( )
inline

Indicates whether the term is a proof by rewriting Remarks: A proof for rewriting an expression t into an expression s. This proof object is used if the parameter PROOF_MODE is 1. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is also used in a few cases if the parameter PROOF_MODE is 2. The cases are: - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to Booleans (BIT2BOOL=true) - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1502 of file Expr.java.

1503  {
1505  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofSkolemize ( )
inline

Indicates whether the term is a proof for a Skolemization step Remarks: Proof for:

(p x y)) (p (sk y) y))

This proof object has no antecedents.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1834 of file Expr.java.

1835  {
1837  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofSymmetry ( )
inline

Indicates whether the term is proof by symmetricity of a relation

Remarks: Given an symmetric relation R and a proof for (R t s), produces * a proof for (R s t). T1: (R t s) [symmetry T1]: (R s t) T1 is the * antecedent of this proof object.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1363 of file Expr.java.

1364  {
1366  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofTheoryLemma ( )
inline

Indicates whether the term is a proof for theory lemma Remarks: Generic proof for theory lemmas.

The theory lemma function comes with one or more parameters. The first parameter indicates the name of the theory. For the theory of arithmetic, additional parameters provide hints for checking the theory lemma. The hints for arithmetic are: - farkas - followed by rational coefficients. Multiply the coefficients to the inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. - triangle-eq - Indicates a lemma related to the equivalence: (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1869 of file Expr.java.

1870  {
1872  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofTransitivity ( )
inline

Indicates whether the term is a proof by transitivity of a relation

Remarks: Given a transitive relation R, and proofs for (R t s) and (R s * u), produces a proof for (R t u). T1: (R t s) T2: (R s u) [trans T1 T2]: * (R t u)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1375 of file Expr.java.

1376  {
1378  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofTransitivityStar ( )
inline

Indicates whether the term is a proof by condensed transitivity of a relation Remarks: Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. It combines several symmetry and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d) [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.

Assuming that this proof object is a proof for (R s t), then a proof checker must check if it is possible to prove (R s t) using the antecedents, symmetry and transitivity. That is, if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1396 of file Expr.java.

1397  {
1399  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofTrue ( )
inline

Indicates whether the term is a Proof for the expression 'true'.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1301 of file Expr.java.

1302  {
1304  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isProofUnitResolution ( )
inline

Indicates whether the term is a proof by unit resolution Remarks: T1: * (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... T(n+1): (not l_n) * [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1623 of file Expr.java.

1624  {
1626  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRatNum ( )
inline

Indicates whether the term is a real numeral.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 272 of file Expr.java.

273  {
274  return isNumeral() && isReal();
275  }
boolean isReal()
Definition: Expr.java:429
boolean isNumeral()
Definition: Expr.java:219
boolean isReal ( )
inline

Indicates whether the term is of sort real.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 429 of file Expr.java.

Referenced by Expr.isRatNum().

430  {
431  return Native.getSortKind(getContext().nCtx(),
432  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT
433  .toInt();
434  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:194
boolean isRealIsInt ( )
inline

Indicates whether the term is a check that tests whether a real is integral (unary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 592 of file Expr.java.

593  {
595  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRealToInt ( )
inline

Indicates whether the term is a coercion of real to integer (unary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 581 of file Expr.java.

582  {
584  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelation ( )
inline

Indicates whether the term is of an array sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1879 of file Expr.java.

1880  {
1881  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1882  .getSortKind(getContext().nCtx(),
1883  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1884  .toInt());
1885  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:194
boolean isRelationalJoin ( )
inline

Indicates whether the term is a relational join

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1926 of file Expr.java.

1927  {
1929  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelationClone ( )
inline

Indicates whether the term is a relational clone (copy) Remarks: Create a fresh copy (clone) of a relation. The function is logically the identity, but in the context of a register machine allows for terms of kind

to perform destructive updates to the first argument.

See also
isRelationUnion
Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 2050 of file Expr.java.

2051  {
2053  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelationComplement ( )
inline

Indicates whether the term is the complement of a relation

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 2020 of file Expr.java.

2021  {
2023  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelationFilter ( )
inline

Indicates whether the term is a relation filter Remarks: Filter (restrict) a relation with respect to a predicate. The first argument is a relation. The second argument is a predicate with free de-Brujin indices corresponding to the columns of the relation. So the first column in the relation has index 0.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1978 of file Expr.java.

1979  {
1981  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelationNegationFilter ( )
inline

Indicates whether the term is an intersection of a relation with the negation of another. Remarks: Intersect the first relation with respect to negation of the second relation (the function takes two arguments). Logically, the specification can be described by a function

target = filter_by_negation(pos, neg, columns)

where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in x in pos, such that there is no y in neg that agrees with x on the columns c1, d1, .., cN, dN.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1998 of file Expr.java.

1999  {
2001  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelationProject ( )
inline

Indicates whether the term is a projection of columns (provided as numbers in the parameters). Remarks: The function takes one argument.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1963 of file Expr.java.

1964  {
1966  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelationRename ( )
inline

Indicates whether the term is the renaming of a column in a relation Remarks: The function takes one argument. The parameters contain the renaming as a cycle.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 2010 of file Expr.java.

2011  {
2013  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelationSelect ( )
inline

Indicates whether the term is a relational select Remarks: Check if a record is an element of the relation. The function takes

n+1

arguments, where the first argument is a relation, and the remaining

n

arguments correspond to a record.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 2034 of file Expr.java.

2035  {
2037  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelationStore ( )
inline

Indicates whether the term is an relation store Remarks: Insert a record into a relation. The function takes

n+1

arguments, where the first argument is the relation and the remaining

n

elements correspond to the

n

columns of the relation.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1896 of file Expr.java.

1897  {
1899  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelationUnion ( )
inline

Indicates whether the term is the union or convex hull of two relations.

Remarks: The function takes two arguments.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1938 of file Expr.java.

1939  {
1941  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRelationWiden ( )
inline

Indicates whether the term is the widening of two relations Remarks: The function takes two arguments.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1950 of file Expr.java.

1951  {
1953  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isRemainder ( )
inline

Indicates whether the term is remainder (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 551 of file Expr.java.

552  {
554  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isSelect ( )
inline

Indicates whether the term is an array select.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 625 of file Expr.java.

626  {
628  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isSetComplement ( )
inline

Indicates whether the term is set complement

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 710 of file Expr.java.

711  {
713  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isSetDifference ( )
inline

Indicates whether the term is set difference

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 700 of file Expr.java.

701  {
703  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isSetIntersect ( )
inline

Indicates whether the term is set intersection

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 690 of file Expr.java.

691  {
693  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isSetSubset ( )
inline

Indicates whether the term is set subset

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 720 of file Expr.java.

721  {
723  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isSetUnion ( )
inline

Indicates whether the term is set union

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 680 of file Expr.java.

681  {
683  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isStore ( )
inline

Indicates whether the term is an array store. Remarks: It satisfies * select(store(a,i,v),j) = if i = j then v else select(a,j). Array store * takes at least 3 arguments.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 615 of file Expr.java.

616  {
618  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isSub ( )
inline

Indicates whether the term is subtraction (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 501 of file Expr.java.

502  {
504  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isTrue ( )
inline

Indicates whether the term is the constant true.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 304 of file Expr.java.

305  {
307  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isUMinus ( )
inline

Indicates whether the term is a unary minus

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 511 of file Expr.java.

512  {
514  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
boolean isWellSorted ( )
inline

Indicates whether the term is well-sorted.

Returns
True if the term is well-sorted, false otherwise.
Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 231 of file Expr.java.

232  {
233  return Native.isWellSorted(getContext().nCtx(), getNativeObject());
234  }
boolean isXor ( )
inline

Indicates whether the term is an exclusive or

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 386 of file Expr.java.

387  {
389  }
boolean isApp()
Definition: AST.java:157
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
FuncDecl getFuncDecl()
Definition: Expr.java:72
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
Expr simplify ( )
inline

Returns a simplified version of the expression

Returns
Expr
Exceptions
Z3Exceptionon error
Returns
an Expr

Definition at line 38 of file Expr.java.

39  {
40  return simplify(null);
41  }
Expr simplify ( Params  p)
inline

Returns a simplified version of the expression A set of parameters

Parameters
pa Params object to configure the simplifier
See also
Context::SimplifyHelp
Returns
an Expr
Exceptions
Z3Exceptionon error
Returns
an Expr

Definition at line 53 of file Expr.java.

54  {
55 
56  if (p == null)
57  return Expr.create(getContext(),
58  Native.simplify(getContext().nCtx(), getNativeObject()));
59  else
60  return Expr.create(
61  getContext(),
62  Native.simplifyEx(getContext().nCtx(), getNativeObject(),
63  p.getNativeObject()));
64  }
Expr(Context ctx)
Definition: Expr.java:2107
Expr substitute ( Expr[]  from,
Expr[]  to 
)
inline

Substitute every occurrence of

from[i]

in the expression with

to[i]

, for

i

smaller than

num_exprs

. Remarks: The result is the new expression. The arrays

from

and

to

must have size

num_exprs

. For every

i

smaller than

num_exprs

, we must have that sort of

from[i]

must be equal to sort of

to[i]

.

Exceptions
Z3Exceptionon error
Returns
an Expr

Definition at line 143 of file Expr.java.

Referenced by Expr.substitute().

144  {
145  getContext().checkContextMatch(from);
146  getContext().checkContextMatch(to);
147  if (from.length != to.length)
148  throw new Z3Exception("Argument sizes do not match");
149  return Expr.create(getContext(), Native.substitute(getContext().nCtx(),
150  getNativeObject(), (int) from.length, Expr.arrayToNative(from),
151  Expr.arrayToNative(to)));
152  }
Expr(Context ctx)
Definition: Expr.java:2107
Expr substitute ( Expr  from,
Expr  to 
)
inline

Substitute every occurrence of

from

in the expression with

to

.

See also
Expr::substitute(Expr[],Expr[])
Exceptions
Z3Exceptionon error
Returns
an Expr

Definition at line 161 of file Expr.java.

162  {
163 
164  return substitute(new Expr[] { from }, new Expr[] { to });
165  }
Expr(Context ctx)
Definition: Expr.java:2107
Expr substitute(Expr[] from, Expr[] to)
Definition: Expr.java:143
Expr substituteVars ( Expr[]  to)
inline

Substitute the free variables in the expression with the expressions in

to

Remarks: For every

i

smaller than *

num_exprs

, the variable with de-Bruijn index

i

* is replaced with term

to[i]

.

Exceptions
Z3Exceptionon error
Z3Exceptionon error
Returns
an Expr

Definition at line 177 of file Expr.java.

178  {
179 
180  getContext().checkContextMatch(to);
181  return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
182  getNativeObject(), (int) to.length, Expr.arrayToNative(to)));
183  }
Expr(Context ctx)
Definition: Expr.java:2107
String toString ( )
inline

Returns a string representation of the expression.

Definition at line 209 of file Expr.java.

Referenced by Optimize.Handle.toString().

210  {
211  return super.toString();
212  }
Expr translate ( Context  ctx)
inline

Translates (copies) the term to the Context

ctx

.

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

Definition at line 194 of file Expr.java.

195  {
196 
197  if (getContext() == ctx)
198  return this;
199  else
200  return Expr.create(
201  ctx,
202  Native.translate(getContext().nCtx(), getNativeObject(),
203  ctx.nCtx()));
204  }
Expr(Context ctx)
Definition: Expr.java:2107
void update ( Expr[]  args)
inline

Update the arguments of the expression using the arguments

args

The number of new arguments should coincide with the current number of arguments.

Parameters
argsarguments
Exceptions
Z3Exceptionon error

Definition at line 122 of file Expr.java.

123  {
124  getContext().checkContextMatch(args);
125  if (isApp() && args.length != getNumArgs())
126  throw new Z3Exception("Number of arguments does not match");
127  setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(),
128  (int) args.length, Expr.arrayToNative(args)));
129  }
boolean isApp()
Definition: AST.java:157
Expr(Context ctx)
Definition: Expr.java:2107