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 ()
 
Expr 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 isString ()
 
String getString ()
 
boolean isConcat ()
 
boolean isOEQ ()
 
boolean isProofTrue ()
 
boolean isProofAsserted ()
 
boolean isProofGoal ()
 
boolean isProofModusPonens ()
 
boolean isProofReflexivity ()
 
boolean isProofSymmetry ()
 
boolean isProofTransitivity ()
 
boolean isProofTransitivityStar ()
 
boolean isProofMonotonicity ()
 
boolean isProofQuantIntro ()
 
boolean isProofDistributivity ()
 
boolean isProofAndElimination ()
 
boolean isProofOrElimination ()
 
boolean isProofRewrite ()
 
boolean isProofRewriteStar ()
 
boolean isProofPullQuant ()
 
boolean isProofPushQuant ()
 
boolean isProofElimUnusedVars ()
 
boolean isProofDER ()
 
boolean isProofQuantInst ()
 
boolean isProofHypothesis ()
 
boolean isProofLemma ()
 
boolean isProofUnitResolution ()
 
boolean isProofIFFTrue ()
 
boolean isProofIFFFalse ()
 
boolean isProofCommutativity ()
 
boolean isProofDefAxiom ()
 
boolean isProofDefIntro ()
 
boolean isProofApplyDef ()
 
boolean isProofIFFOEQ ()
 
boolean isProofNNFPos ()
 
boolean isProofNNFNeg ()
 
boolean isProofSkolemize ()
 
boolean isProofModusPonensOEQ ()
 
boolean isProofTheoryLemma ()
 
boolean isRelation ()
 
boolean isRelationStore ()
 
boolean isEmptyRelation ()
 
boolean isIsEmptyRelation ()
 
boolean isRelationalJoin ()
 
boolean isRelationUnion ()
 
boolean isRelationWiden ()
 
boolean isRelationProject ()
 
boolean isRelationFilter ()
 
boolean isRelationNegationFilter ()
 
boolean isRelationRename ()
 
boolean isRelationComplement ()
 
boolean isRelationSelect ()
 
boolean isRelationClone ()
 
boolean isFiniteDomain ()
 
boolean isFiniteDomainLT ()
 
int getIndex ()
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (AST other)
 
int hashCode ()
 
int getId ()
 
Z3_ast_kind getASTKind ()
 
boolean isExpr ()
 
boolean isApp ()
 
boolean isVar ()
 
boolean isQuantifier ()
 
boolean isSort ()
 
boolean isFuncDecl ()
 
String getSExpr ()
 

Protected Member Functions

 Expr (Context ctx, long obj)
 

Additional Inherited Members

- Static Public Member Functions inherited from Z3Object
static long[] arrayToNative (Z3Object[] a)
 
static int arrayLength (Z3Object[] a)
 

Detailed Description

Expressions are terms.

Definition at line 30 of file Expr.java.

Constructor & Destructor Documentation

◆ Expr()

Expr ( Context  ctx,
long  obj 
)
inlineprotected

Constructor for Expr

Exceptions
Z3Exceptionon error

Definition at line 2096 of file Expr.java.

2096  {
2097  super(ctx, obj);
2098  }

Member Function Documentation

◆ getArgs()

Expr [] getArgs ( )
inline

The arguments of the expression.

Exceptions
Z3Exceptionon error
Returns
an Expr[]

Definition at line 105 of file Expr.java.

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  }
113  return res;
114  }

Referenced by FuncInterp.toString().

◆ getBoolValue()

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  }

◆ getFuncDecl()

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.

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

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.isConcat(), 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.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.isProofOrElimination(), Expr.isProofPullQuant(), 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().

◆ getIndex()

int getIndex ( )
inline

The de-Bruijn 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 2083 of file Expr.java.

2084  {
2085  if (!isVar()) {
2086  throw new Z3Exception("Term is not a bound variable.");
2087  }
2088 
2089  return Native.getIndexValue(getContext().nCtx(), getNativeObject());
2090  }

◆ getNumArgs()

int getNumArgs ( )
inline

The number of arguments of the expression.

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 95 of file Expr.java.

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

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

◆ getSort()

Sort getSort ( )
inline

The Sort of the term.

Exceptions
Z3Exceptionon error
Returns
a sort

Definition at line 235 of file Expr.java.

236  {
237  return Sort.create(getContext(),
238  Native.getSort(getContext().nCtx(), getNativeObject()));
239  }

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

◆ getString()

String getString ( )
inline

Retrieve string corresponding to string constant. Remark: the expression should be a string constant, (isString() should return true).

Exceptions
Z3Exceptionon error
Returns
a string

Definition at line 1288 of file Expr.java.

1289  {
1290  return Native.getString(getContext().nCtx(), getNativeObject());
1291  }

◆ isAdd()

boolean isAdd ( )
inline

Indicates whether the term is addition (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 480 of file Expr.java.

481  {
483  }

◆ isAlgebraicNumber()

boolean isAlgebraicNumber ( )
inline

Indicates whether the term is an algebraic number

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 276 of file Expr.java.

277  {
278  return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
279  }

◆ isAnd()

boolean isAnd ( )
inline

Indicates whether the term is an n-ary conjunction

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 349 of file Expr.java.

350  {
352  }

◆ isArithmeticNumeral()

boolean isArithmeticNumeral ( )
inline

Indicates whether the term is an arithmetic numeral.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 430 of file Expr.java.

431  {
433  }

◆ isArray()

boolean isArray ( )
inline

Indicates whether the term is of an array sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 591 of file Expr.java.

592  {
593  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
594  .fromInt(Native.getSortKind(getContext().nCtx(),
595  Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
596  }

◆ isArrayMap()

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 648 of file Expr.java.

649  {
651  }

◆ isAsArray()

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 659 of file Expr.java.

660  {
662  }

◆ isBool()

boolean isBool ( )
inline

Indicates whether the term has Boolean sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 286 of file Expr.java.

287  {
288  return (isExpr() && Native.isEqSort(getContext().nCtx(),
289  Native.mkBoolSort(getContext().nCtx()),
290  Native.getSort(getContext().nCtx(), getNativeObject())));
291  }

◆ isBV()

boolean isBV ( )
inline

Indicates whether the terms is of bit-vector sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 719 of file Expr.java.

720  {
721  return Native.getSortKind(getContext().nCtx(),
722  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
723  .toInt();
724  }

◆ isBVAdd()

boolean isBVAdd ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 771 of file Expr.java.

772  {
774  }

◆ isBVAND()

boolean isBVAND ( )
inline

Indicates whether the term is a bit-wise AND

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 982 of file Expr.java.

983  {
985  }

◆ isBVBitOne()

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 741 of file Expr.java.

742  {
744  }

◆ isBVBitZero()

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 751 of file Expr.java.

752  {
754  }

◆ isBVCarry()

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 1231 of file Expr.java.

1232  {
1234  }

◆ isBVComp()

boolean isBVComp ( )
inline

Indicates whether the term is a bit-vector comparison

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1122 of file Expr.java.

1123  {
1125  }

◆ isBVConcat()

boolean isBVConcat ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1052 of file Expr.java.

1053  {
1055  }

◆ isBVExtract()

boolean isBVExtract ( )
inline

Indicates whether the term is a bit-vector extraction

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1082 of file Expr.java.

1083  {
1085  }

◆ isBVMul()

boolean isBVMul ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 791 of file Expr.java.

792  {
794  }

◆ isBVNAND()

boolean isBVNAND ( )
inline

Indicates whether the term is a bit-wise NAND

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1022 of file Expr.java.

1023  {
1025  }

◆ isBVNOR()

boolean isBVNOR ( )
inline

Indicates whether the term is a bit-wise NOR

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1032 of file Expr.java.

1033  {
1035  }

◆ isBVNOT()

boolean isBVNOT ( )
inline

Indicates whether the term is a bit-wise NOT

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1002 of file Expr.java.

1003  {
1005  }

◆ isBVNumeral()

boolean isBVNumeral ( )
inline

Indicates whether the term is a bit-vector numeral

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 731 of file Expr.java.

732  {
734  }

◆ isBVOR()

boolean isBVOR ( )
inline

Indicates whether the term is a bit-wise OR

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 992 of file Expr.java.

993  {
995  }

◆ isBVReduceAND()

boolean isBVReduceAND ( )
inline

Indicates whether the term is a bit-vector reduce AND

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1112 of file Expr.java.

1113  {
1115  }

◆ isBVReduceOR()

boolean isBVReduceOR ( )
inline

Indicates whether the term is a bit-vector reduce OR

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1102 of file Expr.java.

1103  {
1105  }

◆ isBVRepeat()

boolean isBVRepeat ( )
inline

Indicates whether the term is a bit-vector repetition

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1092 of file Expr.java.

1093  {
1095  }

◆ isBVRotateLeft()

boolean isBVRotateLeft ( )
inline

Indicates whether the term is a bit-vector rotate left

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1162 of file Expr.java.

1163  {
1165  }

◆ isBVRotateLeftExtended()

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 1184 of file Expr.java.

1185  {
1187  }

◆ isBVRotateRight()

boolean isBVRotateRight ( )
inline

Indicates whether the term is a bit-vector rotate right

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1172 of file Expr.java.

1173  {
1175  }

◆ isBVRotateRightExtended()

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 1196 of file Expr.java.

1197  {
1199  }

◆ isBVSDiv()

boolean isBVSDiv ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 801 of file Expr.java.

802  {
804  }

◆ isBVSGE()

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 932 of file Expr.java.

933  {
935  }

◆ isBVSGT()

boolean isBVSGT ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 972 of file Expr.java.

973  {
975  }

◆ isBVShiftLeft()

boolean isBVShiftLeft ( )
inline

Indicates whether the term is a bit-vector shift left

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1132 of file Expr.java.

1133  {
1135  }

◆ isBVShiftRightArithmetic()

boolean isBVShiftRightArithmetic ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1152 of file Expr.java.

1153  {
1155  }

◆ isBVShiftRightLogical()

boolean isBVShiftRightLogical ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1142 of file Expr.java.

1143  {
1145  }

◆ isBVSignExtension()

boolean isBVSignExtension ( )
inline

Indicates whether the term is a bit-vector sign extension

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1062 of file Expr.java.

1063  {
1065  }

◆ isBVSLE()

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 911 of file Expr.java.

912  {
914  }

◆ isBVSLT()

boolean isBVSLT ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 952 of file Expr.java.

953  {
955  }

◆ isBVSMod()

boolean isBVSMod ( )
inline

Indicates whether the term is a bit-vector signed modulus

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 841 of file Expr.java.

842  {
844  }

◆ isBVSRem()

boolean isBVSRem ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 821 of file Expr.java.

822  {
824  }

◆ isBVSub()

boolean isBVSub ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 781 of file Expr.java.

782  {
784  }

◆ isBVToInt()

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 1220 of file Expr.java.

1221  {
1223  }

◆ isBVUDiv()

boolean isBVUDiv ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 811 of file Expr.java.

812  {
814  }

◆ isBVUGE()

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 922 of file Expr.java.

923  {
925  }

◆ isBVUGT()

boolean isBVUGT ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 962 of file Expr.java.

963  {
965  }

◆ isBVULE()

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 901 of file Expr.java.

902  {
904  }

◆ isBVULT()

boolean isBVULT ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 942 of file Expr.java.

943  {
945  }

◆ isBVUMinus()

boolean isBVUMinus ( )
inline

Indicates whether the term is a bit-vector unary minus

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 761 of file Expr.java.

762  {
764  }

◆ isBVURem()

boolean isBVURem ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 831 of file Expr.java.

832  {
834  }

◆ isBVXNOR()

boolean isBVXNOR ( )
inline

Indicates whether the term is a bit-wise XNOR

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1042 of file Expr.java.

1043  {
1045  }

◆ isBVXOR()

boolean isBVXOR ( )
inline

Indicates whether the term is a bit-wise XOR

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1012 of file Expr.java.

1013  {
1015  }

◆ isBVXOR3()

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 1242 of file Expr.java.

1243  {
1245  }

◆ isBVZeroExtension()

boolean isBVZeroExtension ( )
inline

Indicates whether the term is a bit-vector zero extension

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1072 of file Expr.java.

1073  {
1075  }

◆ isConcat()

boolean isConcat ( )
inline

TBD: sketch for #2522, 'Pointer' seems deprecated and instead approach seems to be around Set/Get CharArrayRegion and updating Native.cpp code generation to produce the char[].

public char[] getNativeString() { Native.IntPtr len = new Native.IntPtr(); long s = Native.getLstring(getContext().nCtx(), getNativeObject(), len); char[] result = new char[len.value]; Pointer ptr = Pointer.createConstant(s); for (int i = 0; i < len.value; ++i) result[i] = ptr.getChar(i); return result; } Check whether expression is a concatenation

Returns
a boolean

Definition at line 1313 of file Expr.java.

1314  {
1316  }

◆ isConst()

boolean isConst ( )
inline

Indicates whether the term represents a constant.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 246 of file Expr.java.

247  {
248  return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
249  }

◆ isConstantArray()

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 625 of file Expr.java.

626  {
628  }

◆ isDefaultArray()

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 636 of file Expr.java.

637  {
639  }

◆ isDistinct()

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 329 of file Expr.java.

330  {
332  }

◆ isDiv()

boolean isDiv ( )
inline

Indicates whether the term is division (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 520 of file Expr.java.

521  {
523  }

◆ isEmptyRelation()

boolean isEmptyRelation ( )
inline

Indicates whether the term is an empty relation

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1893 of file Expr.java.

1894  {
1896  }

◆ isEq()

boolean isEq ( )
inline

Indicates whether the term is an equality predicate.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 318 of file Expr.java.

319  {
321  }

◆ isFalse()

boolean isFalse ( )
inline

Indicates whether the term is the constant false.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 308 of file Expr.java.

309  {
311  }

◆ isFiniteDomain()

boolean isFiniteDomain ( )
inline

Indicates whether the term is of an array sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 2047 of file Expr.java.

2048  {
2049  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
2050  .getSortKind(getContext().nCtx(),
2051  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
2052  .toInt());
2053  }

◆ isFiniteDomainLT()

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 2060 of file Expr.java.

2061  {
2063  }

◆ isGE()

boolean isGE ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 450 of file Expr.java.

451  {
453  }

◆ isGT()

boolean isGT ( )
inline

Indicates whether the term is a greater-than

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 470 of file Expr.java.

471  {
473  }

◆ isIDiv()

boolean isIDiv ( )
inline

Indicates whether the term is integer division (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 530 of file Expr.java.

531  {
533  }

◆ isIff()

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 370 of file Expr.java.

371  {
373  }

◆ isImplies()

boolean isImplies ( )
inline

Indicates whether the term is an implication

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 400 of file Expr.java.

401  {
403  }

◆ isInt()

boolean isInt ( )
inline

Indicates whether the term is of integer sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 410 of file Expr.java.

411  {
412  return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT.toInt();
413  }

Referenced by Expr.isIntNum().

◆ isIntNum()

boolean isIntNum ( )
inline

Indicates whether the term is an integer numeral.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 256 of file Expr.java.

257  {
258  return isNumeral() && isInt();
259  }

◆ isIntToBV()

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 1208 of file Expr.java.

1209  {
1211  }

◆ isIntToReal()

boolean isIntToReal ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 560 of file Expr.java.

561  {
563  }

◆ isIsEmptyRelation()

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 1903 of file Expr.java.

1904  {
1906  }

◆ isITE()

boolean isITE ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 339 of file Expr.java.

340  {
342  }

◆ isLabel()

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 1255 of file Expr.java.

1256  {
1258  }

◆ isLabelLit()

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 1268 of file Expr.java.

1269  {
1271  }

◆ isLE()

boolean isLE ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 440 of file Expr.java.

441  {
443  }

◆ isLT()

boolean isLT ( )
inline

Indicates whether the term is a less-than

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 460 of file Expr.java.

461  {
463  }

◆ isModulus()

boolean isModulus ( )
inline

Indicates whether the term is modulus (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 550 of file Expr.java.

551  {
553  }

◆ isMul()

boolean isMul ( )
inline

Indicates whether the term is multiplication (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 510 of file Expr.java.

511  {
513  }

◆ isNot()

boolean isNot ( )
inline

Indicates whether the term is a negation

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 390 of file Expr.java.

391  {
393  }

◆ isNumeral()

boolean isNumeral ( )
inline

Indicates whether the term is a numeral

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 214 of file Expr.java.

215  {
216  return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
217  }

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

◆ isOEQ()

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 1325 of file Expr.java.

1326  {
1327  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
1328  }

◆ isOr()

boolean isOr ( )
inline

Indicates whether the term is an n-ary disjunction

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 359 of file Expr.java.

360  {
362  }

◆ isProofAndElimination()

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 1485 of file Expr.java.

1486  {
1488  }

◆ isProofApplyDef()

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 1744 of file Expr.java.

1745  {
1747  }

◆ isProofAsserted()

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 1345 of file Expr.java.

1346  {
1348  }

◆ isProofCommutativity()

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 1683 of file Expr.java.

1684  {
1686  }

◆ isProofDefAxiom()

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 1709 of file Expr.java.

1710  {
1712  }

◆ isProofDefIntro()

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 1732 of file Expr.java.

1733  {
1735  }

◆ isProofDER()

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 1591 of file Expr.java.

1592  {
1594  }

◆ isProofDistributivity()

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 1474 of file Expr.java.

1475  {
1477  }

◆ isProofElimUnusedVars()

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 1575 of file Expr.java.

1576  {
1578  }

◆ isProofGoal()

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 1356 of file Expr.java.

1357  {
1359  }

◆ isProofHypothesis()

boolean isProofHypothesis ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1615 of file Expr.java.

1616  {
1618  }

◆ isProofIFFFalse()

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 1666 of file Expr.java.

1667  {
1669  }

◆ isProofIFFOEQ()

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 1756 of file Expr.java.

1757  {
1759  }

◆ isProofIFFTrue()

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 1654 of file Expr.java.

1655  {
1657  }

◆ isProofLemma()

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 1631 of file Expr.java.

1632  {
1634  }

◆ isProofModusPonens()

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 1370 of file Expr.java.

1371  {
1373  }

◆ isProofModusPonensOEQ()

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 1834 of file Expr.java.

1835  {
1837  }

◆ isProofMonotonicity()

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 suppressed to save space.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1444 of file Expr.java.

1445  {
1447  }

◆ isProofNNFNeg()

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 1803 of file Expr.java.

1804  {
1806  }

◆ isProofNNFPos()

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 1784 of file Expr.java.

1785  {
1787  }

◆ isProofOrElimination()

boolean isProofOrElimination ( )
inline

Indicates whether the term is a proof by elimination 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 1496 of file Expr.java.

1497  {
1499  }

◆ isProofPullQuant()

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 1544 of file Expr.java.

1545  {
1547  }

◆ isProofPushQuant()

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 1559 of file Expr.java.

1560  {
1562  }

◆ isProofQuantInst()

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 1603 of file Expr.java.

1604  {
1606  }

◆ isProofQuantIntro()

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 1455 of file Expr.java.

1456  {
1458  }

◆ isProofReflexivity()

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 1385 of file Expr.java.

1386  {
1388  }

◆ isProofRewrite()

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 1516 of file Expr.java.

1517  {
1519  }

◆ isProofRewriteStar()

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 can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is used in a few cases . The cases are: - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to Booleans (BIT2BOOL=true)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1532 of file Expr.java.

1533  {
1535  }

◆ isProofSkolemize()

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 1821 of file Expr.java.

1822  {
1824  }

◆ isProofSymmetry()

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 1397 of file Expr.java.

1398  {
1400  }

◆ isProofTheoryLemma()

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 1856 of file Expr.java.

1857  {
1859  }

◆ isProofTransitivity()

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 1409 of file Expr.java.

1410  {
1412  }

◆ isProofTransitivityStar()

boolean isProofTransitivityStar ( )
inline

Indicates whether the term is a proof by condensed transitivity of a relation Remarks: Condensed transitivity proof. 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 1429 of file Expr.java.

1430  {
1432  }

◆ isProofTrue()

boolean isProofTrue ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1335 of file Expr.java.

1336  {
1338  }

◆ isProofUnitResolution()

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 1642 of file Expr.java.

1643  {
1645  }

◆ isRatNum()

boolean isRatNum ( )
inline

Indicates whether the term is a real numeral.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 266 of file Expr.java.

267  {
268  return isNumeral() && isReal();
269  }

◆ isReal()

boolean isReal ( )
inline

Indicates whether the term is of sort real.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 420 of file Expr.java.

421  {
422  return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT.toInt();
423  }

Referenced by Expr.isRatNum().

◆ isRealIsInt()

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 581 of file Expr.java.

582  {
584  }

◆ isRealToInt()

boolean isRealToInt ( )
inline

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

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 570 of file Expr.java.

571  {
573  }

◆ isRelation()

boolean isRelation ( )
inline

Indicates whether the term is of an array sort.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1866 of file Expr.java.

1867  {
1868  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1869  .getSortKind(getContext().nCtx(),
1870  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1871  .toInt());
1872  }

◆ isRelationalJoin()

boolean isRelationalJoin ( )
inline

Indicates whether the term is a relational join

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 1913 of file Expr.java.

1914  {
1916  }

◆ isRelationClone()

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 2037 of file Expr.java.

2038  {
2040  }

◆ isRelationComplement()

boolean isRelationComplement ( )
inline

Indicates whether the term is the complement of a relation

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 2007 of file Expr.java.

2008  {
2010  }

◆ isRelationFilter()

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-Bruijn 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 1965 of file Expr.java.

1966  {
1968  }

◆ isRelationNegationFilter()

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 1985 of file Expr.java.

1986  {
1988  }

◆ isRelationProject()

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 1950 of file Expr.java.

1951  {
1953  }

◆ isRelationRename()

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 1997 of file Expr.java.

1998  {
2000  }

◆ isRelationSelect()

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 2021 of file Expr.java.

2022  {
2024  }

◆ isRelationStore()

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 1883 of file Expr.java.

1884  {
1886  }

◆ isRelationUnion()

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 1925 of file Expr.java.

1926  {
1928  }

◆ isRelationWiden()

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 1937 of file Expr.java.

1938  {
1940  }

◆ isRemainder()

boolean isRemainder ( )
inline

Indicates whether the term is remainder (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 540 of file Expr.java.

541  {
543  }

◆ isSelect()

boolean isSelect ( )
inline

Indicates whether the term is an array select.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 614 of file Expr.java.

615  {
617  }

◆ isSetComplement()

boolean isSetComplement ( )
inline

Indicates whether the term is set complement

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 699 of file Expr.java.

700  {
702  }

◆ isSetDifference()

boolean isSetDifference ( )
inline

Indicates whether the term is set difference

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 689 of file Expr.java.

690  {
692  }

◆ isSetIntersect()

boolean isSetIntersect ( )
inline

Indicates whether the term is set intersection

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 679 of file Expr.java.

680  {
682  }

◆ isSetSubset()

boolean isSetSubset ( )
inline

Indicates whether the term is set subset

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 709 of file Expr.java.

710  {
712  }

◆ isSetUnion()

boolean isSetUnion ( )
inline

Indicates whether the term is set union

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 669 of file Expr.java.

670  {
672  }

◆ isStore()

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 604 of file Expr.java.

605  {
607  }

◆ isString()

boolean isString ( )
inline

Check whether expression is a string constant.

Returns
a boolean

Definition at line 1277 of file Expr.java.

1278  {
1279  return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
1280  }

◆ isSub()

boolean isSub ( )
inline

Indicates whether the term is subtraction (binary)

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 490 of file Expr.java.

491  {
493  }

◆ isTrue()

boolean isTrue ( )
inline

Indicates whether the term is the constant true.

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 298 of file Expr.java.

299  {
301  }

◆ isUMinus()

boolean isUMinus ( )
inline

Indicates whether the term is a unary minus

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 500 of file Expr.java.

501  {
503  }

◆ isWellSorted()

boolean isWellSorted ( )
inline

Indicates whether the term is well-sorted.

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

Definition at line 225 of file Expr.java.

226  {
227  return Native.isWellSorted(getContext().nCtx(), getNativeObject());
228  }

◆ isXor()

boolean isXor ( )
inline

Indicates whether the term is an exclusive or

Exceptions
Z3Exceptionon error
Returns
a boolean

Definition at line 380 of file Expr.java.

381  {
383  }

◆ simplify() [1/2]

Expr simplify ( )
inline

Returns a simplified version of the expression

Returns
Expr
Exceptions
Z3Exceptionon error

Definition at line 37 of file Expr.java.

38  {
39  return simplify(null);
40  }

◆ simplify() [2/2]

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

Definition at line 51 of file Expr.java.

52  {
53 
54  if (p == null) {
55  return Expr.create(getContext(),
56  Native.simplify(getContext().nCtx(), getNativeObject()));
57  }
58  else {
59  return Expr.create(
60  getContext(),
61  Native.simplifyEx(getContext().nCtx(), getNativeObject(),
62  p.getNativeObject()));
63  }
64  }

◆ substitute() [1/2]

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 164 of file Expr.java.

165  {
166  return substitute(new Expr[] { from }, new Expr[] { to });
167  }

◆ substitute() [2/2]

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 145 of file Expr.java.

146  {
147  getContext().checkContextMatch(from);
148  getContext().checkContextMatch(to);
149  if (from.length != to.length) {
150  throw new Z3Exception("Argument sizes do not match");
151  }
152  return Expr.create(getContext(), Native.substitute(getContext().nCtx(),
153  getNativeObject(), from.length, Expr.arrayToNative(from),
154  Expr.arrayToNative(to)));
155  }

Referenced by Expr.substitute().

◆ substituteVars()

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 179 of file Expr.java.

180  {
181 
182  getContext().checkContextMatch(to);
183  return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
184  getNativeObject(), to.length, Expr.arrayToNative(to)));
185  }

◆ toString()

String toString ( )
inline

Returns a string representation of the expression.

Reimplemented from AST.

Reimplemented in RatNum, IntNum, FPNum, FiniteDomainNum, and BitVecNum.

Definition at line 204 of file Expr.java.

205  {
206  return super.toString();
207  }

◆ translate()

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

Reimplemented from AST.

Reimplemented in Quantifier, and Lambda.

Definition at line 195 of file Expr.java.

196  {
197  return (Expr) super.translate(ctx);
198  }

Referenced by Expr.translate().

◆ update()

Expr 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 123 of file Expr.java.

124  {
125  getContext().checkContextMatch(args);
126  if (isApp() && args.length != getNumArgs()) {
127  throw new Z3Exception("Number of arguments does not match");
128  }
129  return Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
130  args.length, Expr.arrayToNative(args)));
131  }
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR
Z3_OP_PR_TRANSITIVITY_STAR
Definition: Z3_decl_kind.java:126
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_SELECT
Z3_OP_RA_SELECT
Definition: Z3_decl_kind.java:171
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_MAP
Z3_OP_ARRAY_MAP
Definition: Z3_decl_kind.java:47
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_NOT
Z3_OP_NOT
Definition: Z3_decl_kind.java:23
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TO_REAL
Z3_OP_TO_REAL
Definition: Z3_decl_kind.java:40
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNOT
Z3_OP_BNOT
Definition: Z3_decl_kind.java:85
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BREDAND
Z3_OP_BREDAND
Definition: Z3_decl_kind.java:96
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PUSH_QUANT
Z3_OP_PR_PUSH_QUANT
Definition: Z3_decl_kind.java:136
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IMPLIES
Z3_OP_IMPLIES
Definition: Z3_decl_kind.java:24
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DEF_AXIOM
Z3_OP_PR_DEF_AXIOM
Definition: Z3_decl_kind.java:146
com.microsoft.z3.Expr.substitute
Expr substitute(Expr[] from, Expr[] to)
Definition: Expr.java:145
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNUM
Z3_OP_BNUM
Definition: Z3_decl_kind.java:58
com.microsoft.z3.Expr.isInt
boolean isInt()
Definition: Expr.java:410
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_SUBSET
Z3_OP_SET_SUBSET
Definition: Z3_decl_kind.java:53
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IS_INT
Z3_OP_IS_INT
Definition: Z3_decl_kind.java:42
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TRUE
Z3_OP_TRUE
Definition: Z3_decl_kind.java:14
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_OEQ
Z3_OP_PR_IFF_OEQ
Definition: Z3_decl_kind.java:153
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SLEQ
Z3_OP_SLEQ
Definition: Z3_decl_kind.java:76
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_COMPLEMENT
Z3_OP_RA_COMPLEMENT
Definition: Z3_decl_kind.java:170
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD
Z3_OP_BSMOD
Definition: Z3_decl_kind.java:69
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_TRUE
Z3_OP_PR_IFF_TRUE
Definition: Z3_decl_kind.java:143
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ITE
Z3_OP_ITE
Definition: Z3_decl_kind.java:18
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS
Z3_OP_PR_ELIM_UNUSED_VARS
Definition: Z3_decl_kind.java:137
com.microsoft.z3.FuncDecl.getDomainSize
int getDomainSize()
Definition: FuncDecl.java:86
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT
Z3_OP_EXT_ROTATE_LEFT
Definition: Z3_decl_kind.java:103
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MODUS_PONENS
Z3_OP_PR_MODUS_PONENS
Definition: Z3_decl_kind.java:122
z3::abs
expr abs(expr const &a)
Definition: z3++.h:1722
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_HYPOTHESIS
Z3_OP_PR_HYPOTHESIS
Definition: Z3_decl_kind.java:140
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BXNOR
Z3_OP_BXNOR
Definition: Z3_decl_kind.java:89
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_RENAME
Z3_OP_RA_RENAME
Definition: Z3_decl_kind.java:169
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BXOR
Z3_OP_BXOR
Definition: Z3_decl_kind.java:86
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LABEL
Z3_OP_LABEL
Definition: Z3_decl_kind.java:203
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONCAT
Z3_OP_CONCAT
Definition: Z3_decl_kind.java:90
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER
Z3_OP_RA_NEGATION_FILTER
Definition: Z3_decl_kind.java:168
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_INT2BV
Z3_OP_INT2BV
Definition: Z3_decl_kind.java:106
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LT
Z3_OP_LT
Definition: Z3_decl_kind.java:30
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT0
Z3_OP_BIT0
Definition: Z3_decl_kind.java:60
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BV2INT
Z3_OP_BV2INT
Definition: Z3_decl_kind.java:107
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONST_ARRAY
Z3_OP_CONST_ARRAY
Definition: Z3_decl_kind.java:46
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:100
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRANSITIVITY
Z3_OP_PR_TRANSITIVITY
Definition: Z3_decl_kind.java:125
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNAND
Z3_OP_BNAND
Definition: Z3_decl_kind.java:87
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY
Z3_OP_PR_COMMUTATIVITY
Definition: Z3_decl_kind.java:145
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LE
Z3_OP_LE
Definition: Z3_decl_kind.java:28
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRUE
Z3_OP_PR_TRUE
Definition: Z3_decl_kind.java:119
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ROTATE_RIGHT
Z3_OP_ROTATE_RIGHT
Definition: Z3_decl_kind.java:102
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_DIFFERENCE
Z3_OP_SET_DIFFERENCE
Definition: Z3_decl_kind.java:51
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_JOIN
Z3_OP_RA_JOIN
Definition: Z3_decl_kind.java:163
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_QUANT_INST
Z3_OP_PR_QUANT_INST
Definition: Z3_decl_kind.java:139
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_OR
Z3_OP_OR
Definition: Z3_decl_kind.java:20
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BASHR
Z3_OP_BASHR
Definition: Z3_decl_kind.java:100
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_REM
Z3_OP_REM
Definition: Z3_decl_kind.java:38
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT1
Z3_OP_BIT1
Definition: Z3_decl_kind.java:59
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UGT
Z3_OP_UGT
Definition: Z3_decl_kind.java:81
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CARRY
Z3_OP_CARRY
Definition: Z3_decl_kind.java:108
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_MOD
Z3_OP_MOD
Definition: Z3_decl_kind.java:39
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TH_LEMMA
Z3_OP_PR_TH_LEMMA
Definition: Z3_decl_kind.java:158
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PULL_QUANT
Z3_OP_PR_PULL_QUANT
Definition: Z3_decl_kind.java:135
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_REPEAT
Z3_OP_REPEAT
Definition: Z3_decl_kind.java:94
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_NEG
Z3_OP_PR_NNF_NEG
Definition: Z3_decl_kind.java:155
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IDIV
Z3_OP_IDIV
Definition: Z3_decl_kind.java:37
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_MUL
Z3_OP_MUL
Definition: Z3_decl_kind.java:35
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_SYMMETRY
Z3_OP_PR_SYMMETRY
Definition: Z3_decl_kind.java:124
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DEF_INTRO
Z3_OP_PR_DEF_INTRO
Definition: Z3_decl_kind.java:151
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_GT
Z3_OP_GT
Definition: Z3_decl_kind.java:31
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:148
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNOR
Z3_OP_BNOR
Definition: Z3_decl_kind.java:88
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_UNION
Z3_OP_SET_UNION
Definition: Z3_decl_kind.java:49
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSREM
Z3_OP_BSREM
Definition: Z3_decl_kind.java:67
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM
Z3_OP_BUREM
Definition: Z3_decl_kind.java:68
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_CLONE
Z3_OP_RA_CLONE
Definition: Z3_decl_kind.java:172
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_POS
Z3_OP_PR_NNF_POS
Definition: Z3_decl_kind.java:154
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSUB
Z3_OP_BSUB
Definition: Z3_decl_kind.java:63
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_IS_EMPTY
Z3_OP_RA_IS_EMPTY
Definition: Z3_decl_kind.java:162
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_COMPLEMENT
Z3_OP_SET_COMPLEMENT
Definition: Z3_decl_kind.java:52
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ADD
Z3_OP_ADD
Definition: Z3_decl_kind.java:32
com.microsoft.z3.Context.mkBoolSort
BoolSort mkBoolSort()
Definition: Context.java:160
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ULT
Z3_OP_ULT
Definition: Z3_decl_kind.java:79
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ZERO_EXT
Z3_OP_ZERO_EXT
Definition: Z3_decl_kind.java:92
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_GOAL
Z3_OP_PR_GOAL
Definition: Z3_decl_kind.java:121
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SIGN_EXT
Z3_OP_SIGN_EXT
Definition: Z3_decl_kind.java:91
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BREDOR
Z3_OP_BREDOR
Definition: Z3_decl_kind.java:95
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BLSHR
Z3_OP_BLSHR
Definition: Z3_decl_kind.java:99
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REWRITE
Z3_OP_PR_REWRITE
Definition: Z3_decl_kind.java:133
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_UNION
Z3_OP_RA_UNION
Definition: Z3_decl_kind.java:164
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EQ
Z3_OP_EQ
Definition: Z3_decl_kind.java:16
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION
Z3_OP_PR_UNIT_RESOLUTION
Definition: Z3_decl_kind.java:142
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_WIDEN
Z3_OP_RA_WIDEN
Definition: Z3_decl_kind.java:165
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MONOTONICITY
Z3_OP_PR_MONOTONICITY
Definition: Z3_decl_kind.java:127
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY
Z3_OP_PR_DISTRIBUTIVITY
Definition: Z3_decl_kind.java:130
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSHL
Z3_OP_BSHL
Definition: Z3_decl_kind.java:98
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXTRACT
Z3_OP_EXTRACT
Definition: Z3_decl_kind.java:93
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_XOR3
Z3_OP_XOR3
Definition: Z3_decl_kind.java:109
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_FALSE
Z3_OP_PR_IFF_FALSE
Definition: Z3_decl_kind.java:144
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_STORE
Z3_OP_RA_STORE
Definition: Z3_decl_kind.java:160
com.microsoft.z3.Expr.simplify
Expr simplify()
Definition: Expr.java:37
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BADD
Z3_OP_BADD
Definition: Z3_decl_kind.java:62
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REFLEXIVITY
Z3_OP_PR_REFLEXIVITY
Definition: Z3_decl_kind.java:123
z3::forall
expr forall(expr const &x, expr const &b)
Definition: z3++.h:1982
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_FILTER
Z3_OP_RA_FILTER
Definition: Z3_decl_kind.java:167
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REWRITE_STAR
Z3_OP_PR_REWRITE_STAR
Definition: Z3_decl_kind.java:134
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BOR
Z3_OP_BOR
Definition: Z3_decl_kind.java:84
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ANUM
Z3_OP_ANUM
Definition: Z3_decl_kind.java:26
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ULEQ
Z3_OP_ULEQ
Definition: Z3_decl_kind.java:75
com.microsoft.z3.Expr.isRelationUnion
boolean isRelationUnion()
Definition: Expr.java:1925
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UGEQ
Z3_OP_UGEQ
Definition: Z3_decl_kind.java:77
com.microsoft.z3.Expr.Expr
Expr(Context ctx, long obj)
Definition: Expr.java:2096
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DIV
Z3_OP_DIV
Definition: Z3_decl_kind.java:36
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SGT
Z3_OP_SGT
Definition: Z3_decl_kind.java:82
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SLT
Z3_OP_SLT
Definition: Z3_decl_kind.java:80
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_AND_ELIM
Z3_OP_PR_AND_ELIM
Definition: Z3_decl_kind.java:131
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UMINUS
Z3_OP_UMINUS
Definition: Z3_decl_kind.java:34
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT
Z3_OP_EXT_ROTATE_RIGHT
Definition: Z3_decl_kind.java:104
com.microsoft.z3.Expr.getFuncDecl
FuncDecl getFuncDecl()
Definition: Expr.java:72
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TO_INT
Z3_OP_TO_INT
Definition: Z3_decl_kind.java:41
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LABEL_LIT
Z3_OP_LABEL_LIT
Definition: Z3_decl_kind.java:204
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNEG
Z3_OP_BNEG
Definition: Z3_decl_kind.java:61
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AS_ARRAY
Z3_OP_AS_ARRAY
Definition: Z3_decl_kind.java:54
com.microsoft.z3.FuncDecl.getDeclKind
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:119
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_CONCAT
Z3_OP_SEQ_CONCAT
Definition: Z3_decl_kind.java:177
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_OEQ
Z3_OP_OEQ
Definition: Z3_decl_kind.java:25
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_SKOLEMIZE
Z3_OP_PR_SKOLEMIZE
Definition: Z3_decl_kind.java:156
com.microsoft.z3.AST.isExpr
boolean isExpr()
Definition: AST.java:112
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SUB
Z3_OP_SUB
Definition: Z3_decl_kind.java:33
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BMUL
Z3_OP_BMUL
Definition: Z3_decl_kind.java:64
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ROTATE_LEFT
Z3_OP_ROTATE_LEFT
Definition: Z3_decl_kind.java:101
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SGEQ
Z3_OP_SGEQ
Definition: Z3_decl_kind.java:78
com.microsoft.z3.Expr.isNumeral
boolean isNumeral()
Definition: Expr.java:214
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SELECT
Z3_OP_SELECT
Definition: Z3_decl_kind.java:45
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_INTERSECT
Z3_OP_SET_INTERSECT
Definition: Z3_decl_kind.java:50
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BAND
Z3_OP_BAND
Definition: Z3_decl_kind.java:83
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DER
Z3_OP_PR_DER
Definition: Z3_decl_kind.java:138
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_APPLY_DEF
Z3_OP_PR_APPLY_DEF
Definition: Z3_decl_kind.java:152
com.microsoft.z3.AST.isApp
boolean isApp()
Definition: AST.java:131
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_PROJECT
Z3_OP_RA_PROJECT
Definition: Z3_decl_kind.java:166
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV
Z3_OP_BUDIV
Definition: Z3_decl_kind.java:66
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_DEFAULT
Z3_OP_ARRAY_DEFAULT
Definition: Z3_decl_kind.java:48
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_EMPTY
Z3_OP_RA_EMPTY
Definition: Z3_decl_kind.java:161
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_QUANT_INTRO
Z3_OP_PR_QUANT_INTRO
Definition: Z3_decl_kind.java:128
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV
Z3_OP_BSDIV
Definition: Z3_decl_kind.java:65
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FD_LT
Z3_OP_FD_LT
Definition: Z3_decl_kind.java:174
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DISTINCT
Z3_OP_DISTINCT
Definition: Z3_decl_kind.java:17
Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1007
com.microsoft.z3.Expr.isReal
boolean isReal()
Definition: Expr.java:420
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AND
Z3_OP_AND
Definition: Z3_decl_kind.java:19
com.microsoft.z3.AST.isVar
boolean isVar()
Definition: AST.java:141
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_STORE
Z3_OP_STORE
Definition: Z3_decl_kind.java:44
com.microsoft.z3.Expr.getNumArgs
int getNumArgs()
Definition: Expr.java:95
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ
Z3_OP_PR_MODUS_PONENS_OEQ
Definition: Z3_decl_kind.java:157
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM
Z3_OP_PR_NOT_OR_ELIM
Definition: Z3_decl_kind.java:132
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ASSERTED
Z3_OP_PR_ASSERTED
Definition: Z3_decl_kind.java:120
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BCOMP
Z3_OP_BCOMP
Definition: Z3_decl_kind.java:97
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_LEMMA
Z3_OP_PR_LEMMA
Definition: Z3_decl_kind.java:141
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_GE
Z3_OP_GE
Definition: Z3_decl_kind.java:29
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FALSE
Z3_OP_FALSE
Definition: Z3_decl_kind.java:15
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_XOR
Z3_OP_XOR
Definition: Z3_decl_kind.java:22
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IFF
Z3_OP_IFF
Definition: Z3_decl_kind.java:21