Z3 |

Public Member Functions | Protected Member Functions
Expr< R extends Sort > Class Template Reference
Inheritance diagram for Expr< R extends Sort >:

## Public Member Functions
Expr< R > | simplify ()
Expr< R > | simplify (Params p)
FuncDecl< R > | getFuncDecl ()
Z3_lbool | getBoolValue ()
int | getNumArgs ()
Expr<?>[] | getArgs ()
Expr< R > | update (Expr<?>[] args)
Expr< R > | substitute (Expr<?>[] from, Expr<?>[] to)
Expr< R > | substitute (Expr<?> from, Expr<?> to)
Expr< R > | substituteVars (Expr<?>[] to)
Expr< R > | translate (Context ctx)
String | toString ()
boolean | isNumeral ()
boolean | isWellSorted ()
R | getSort ()
boolean | isConst ()
boolean | isIntNum ()
boolean | isRatNum ()
boolean | isAlgebraicNumber ()
boolean | isBool ()
boolean | isTrue ()
boolean | isFalse ()
boolean | isEq ()
boolean | isDistinct ()
boolean | isITE ()
boolean | isAnd ()
boolean | isOr ()
boolean | isIff ()
boolean | isXor ()
boolean | isNot ()
boolean | isImplies ()
boolean | isInt ()
boolean | isReal ()
boolean | isArithmeticNumeral ()
boolean | isLE ()
boolean | isGE ()
boolean | isLT ()
boolean | isGT ()
boolean | isAdd ()
boolean | isSub ()
boolean | isUMinus ()
boolean | isMul ()
boolean | isDiv ()
boolean | isIDiv ()
boolean | isRemainder ()
boolean | isModulus ()
boolean | isIntToReal ()
boolean | isRealToInt ()
boolean | isRealIsInt ()
boolean | isArray ()
boolean | isStore ()
boolean | isSelect ()
boolean | isConstantArray ()
boolean | isDefaultArray ()
boolean | isArrayMap ()
boolean | isAsArray ()
boolean | isSetUnion ()
boolean | isSetIntersect ()
boolean | isSetDifference ()
boolean | isSetComplement ()
boolean | isSetSubset ()
boolean | isBV ()
boolean | isBVNumeral ()
boolean | isBVBitOne ()
boolean | isBVBitZero ()
boolean | isBVUMinus ()
boolean | isBVAdd ()
boolean | isBVSub ()
boolean | isBVMul ()
boolean | isBVSDiv ()
boolean | isBVUDiv ()
boolean | isBVSRem ()
boolean | isBVURem ()
boolean | isBVSMod ()
boolean | isBVULE ()
boolean | isBVSLE ()
boolean | isBVUGE ()
boolean | isBVSGE ()
boolean | isBVULT ()
boolean | isBVSLT ()
boolean | isBVUGT ()
boolean | isBVSGT ()
boolean | isBVAND ()
boolean | isBVOR ()
boolean | isBVNOT ()
boolean | isBVXOR ()
boolean | isBVNAND ()
boolean | isBVNOR ()
boolean | isBVXNOR ()
boolean | isBVConcat ()
boolean | isBVSignExtension ()
boolean | isBVZeroExtension ()
boolean | isBVExtract ()
boolean | isBVRepeat ()
boolean | isBVReduceOR ()
boolean | isBVReduceAND ()
boolean | isBVComp ()
boolean | isBVShiftLeft ()
boolean | isBVShiftRightLogical ()
boolean | isBVShiftRightArithmetic ()
boolean | isBVRotateLeft ()
boolean | isBVRotateRight ()
boolean | isBVRotateLeftExtended ()
boolean | isBVRotateRightExtended ()
boolean | isIntToBV ()
boolean | isBVToInt ()
boolean | isBVCarry ()
boolean | isBVXOR3 ()
boolean | isLabel ()
boolean | isLabelLit ()
boolean | isString ()
String | getString ()
boolean | isConcat ()
boolean | isOEQ ()
boolean | isProofTrue ()
boolean | isProofAsserted ()
boolean | isProofGoal ()
boolean | isProofModusPonens ()
boolean | isProofReflexivity ()
boolean | isProofSymmetry ()
boolean | isProofTransitivity ()
boolean | isProofTransitivityStar ()
boolean | isProofMonotonicity ()
boolean | isProofQuantIntro ()
boolean | isProofDistributivity ()
boolean | isProofAndElimination ()
boolean | isProofOrElimination ()
boolean | isProofRewrite ()
boolean | isProofRewriteStar ()
boolean | isProofPullQuant ()
boolean | isProofPushQuant ()
boolean | isProofElimUnusedVars ()
boolean | isProofDER ()
boolean | isProofQuantInst ()
boolean | isProofHypothesis ()
boolean | isProofLemma ()
boolean | isProofUnitResolution ()
boolean | isProofIFFTrue ()
boolean | isProofIFFFalse ()
boolean | isProofCommutativity ()
boolean | isProofDefAxiom ()
boolean | isProofDefIntro ()
boolean | isProofApplyDef ()
boolean | isProofIFFOEQ ()
boolean | isProofNNFPos ()
boolean | isProofNNFNeg ()
boolean | isProofSkolemize ()
boolean | isProofModusPonensOEQ ()
boolean | isProofTheoryLemma ()
boolean | isRelation ()
boolean | isRelationStore ()
boolean | isEmptyRelation ()
boolean | isIsEmptyRelation ()
boolean | isRelationalJoin ()
boolean | isRelationUnion ()
boolean | isRelationWiden ()
boolean | isRelationProject ()
boolean | isRelationFilter ()
boolean | isRelationNegationFilter ()
boolean | isRelationRename ()
boolean | isRelationComplement ()
boolean | isRelationSelect ()
boolean | isRelationClone ()
boolean | isFiniteDomain ()
boolean | isFiniteDomainLT ()
int | getIndex ()
Public Member Functions inherited from AST
boolean | equals (Object o)
int | compareTo (AST 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 ()

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

## Constructor & Destructor Documentation

## ◆ Expr()

Expr | ( | Context | ctx,
|  | long | obj
| ) |  |
| inline protected

Constructor for Expr

Exceptions

  Z3Exception | on error

Definition at line 2119 of file Expr.java.

2119 {
2120 super(ctx, obj);
2121 Type superclass = getClass().getGenericSuperclass();
2122 if (superclass instanceof ParameterizedType) {
2123 Type argType = ((ParameterizedType) superclass).getActualTypeArguments()[0];
2124 if (argType instanceof Class) {
2125 this.sort = (Class) argType;
2126 }
2127 }
2128 }

## Member Function Documentation

## ◆ getArgs()

Expr<?>[] getArgs | ( |  | ) |
| inline

The arguments of the expression.

Exceptions

  Z3Exception | on error

Returns
  an Expr[]

Definition at line 109 of file Expr.java.

110 {
111 int n = getNumArgs();
112 Expr<?>[] res = new Expr[n];
113 for (int i = 0; i < n; i++) {
114 res[i] = Expr.create(getContext(),
115 Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
116 }
117 return res;
118 }
com.microsoft.z3.Expr.Expr
Expr(Context ctx, long obj)
Definition: Expr.java:2119
com.microsoft.z3.Expr.getNumArgs
int getNumArgs()
Definition: Expr.java:99

Referenced by FuncInterp< R extends Sort >.toString().

## ◆ getBoolValue()

Z3_lbool getBoolValue | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a Z3_lbool

Definition at line 88 of file Expr.java.

89 {
90 return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
91 getNativeObject()));
92 }
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102

## ◆ getFuncDecl()

FuncDecl< R > getFuncDecl | ( |  | ) |
| inline

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

Returns
  a FuncDecl

Exceptions

  Z3Exception | on error

Definition at line 76 of file Expr.java.

77 {
78 return new FuncDecl<>(getContext(), Native.getAppDecl(getContext().nCtx(),
79 getNativeObject()));
80 }

## ◆ 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

  Z3Exception | on error

Returns
  an int

Definition at line 2087 of file Expr.java.

2088 {
2089 if (!isVar()) {
2090 throw new Z3Exception("Term is not a bound variable.");
2091 }
2092
2093 return Native.getIndexValue(getContext().nCtx(), getNativeObject());
2094 }
com.microsoft.z3.AST.isVar
boolean isVar()
Definition: AST.java:141

## ◆ getNumArgs()

int getNumArgs | ( |  | ) |
| inline

The number of arguments of the expression.

Exceptions

  Z3Exception | on error

Returns
  an int

Definition at line 99 of file Expr.java.

100 {
101 return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
102 }

## ◆ getSort()

R getSort | ( |  | ) |
| inline

The Sort of the term.

Exceptions

  Z3Exception | on error

Returns
  a sort

Definition at line 239 of file Expr.java.

240 {
241 return (R) Sort.create(getContext(),
242 Native.getSort(getContext().nCtx(), getNativeObject()));
243 }

## ◆ getString()

String getString | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a string

Definition at line 1292 of file Expr.java.

1293 {
1294 return Native.getString(getContext().nCtx(), getNativeObject());
1295 }

## ◆ isAdd()

boolean isAdd | ( |  | ) |
| inline

Indicates whether the term is addition (binary)

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 484 of file Expr.java.

485 {
486 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD;
487 }
com.microsoft.z3.AST.isApp
boolean isApp()
Definition: AST.java:131
com.microsoft.z3.Expr.getFuncDecl
FuncDecl< R > getFuncDecl()
Definition: Expr.java:76
Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000

## ◆ isAlgebraicNumber()

boolean isAlgebraicNumber | ( |  | ) |
| inline

Indicates whether the term is an algebraic number

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 280 of file Expr.java.

281 {
282 return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
283 }

## ◆ isAnd()

boolean isAnd | ( |  | ) |
| inline

Indicates whether the term is an n-ary conjunction

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 353 of file Expr.java.

354 {
355 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND;
356 }

## ◆ isArithmeticNumeral()

boolean isArithmeticNumeral | ( |  | ) |
| inline

Indicates whether the term is an arithmetic numeral.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 434 of file Expr.java.

435 {
436 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM;
437 }

## ◆ isArray()

boolean isArray | ( |  | ) |
| inline

Indicates whether the term is of an array sort.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 595 of file Expr.java.

596 {
597 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
598 .fromInt(Native.getSortKind(getContext().nCtx(),
599 Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
600 }
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 652 of file Expr.java.

653 {
654 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP;
655 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 663 of file Expr.java.

664 {
665 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY;
666 }

## ◆ isBool()

boolean isBool | ( |  | ) |
| inline

Indicates whether the term has Boolean sort.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 290 of file Expr.java.

291 {
292 return (isExpr() && Native.isEqSort(getContext().nCtx(),
293 Native.mkBoolSort(getContext().nCtx()),
294 Native.getSort(getContext().nCtx(), getNativeObject())));
295 }
com.microsoft.z3.AST.isExpr
boolean isExpr()
Definition: AST.java:112
com.microsoft.z3.Context.mkBoolSort
BoolSort mkBoolSort()
Definition: Context.java:161

## ◆ isBV()

boolean isBV | ( |  | ) |
| inline

Indicates whether the terms is of bit-vector sort.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 723 of file Expr.java.

724 {
725 return Native.getSortKind(getContext().nCtx(),
726 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
727 .toInt();
728 }

## ◆ isBVAdd()

boolean isBVAdd | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 775 of file Expr.java.

776 {
777 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD;
778 }

## ◆ isBVAND()

boolean isBVAND | ( |  | ) |
| inline

Indicates whether the term is a bit-wise AND

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 986 of file Expr.java.

987 {
988 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND;
989 }

## ◆ isBVBitOne()

boolean isBVBitOne | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 745 of file Expr.java.

746 {
747 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1;
748 }

## ◆ isBVBitZero()

boolean isBVBitZero | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 755 of file Expr.java.

756 {
757 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0;
758 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1235 of file Expr.java.

1236 {
1237 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY;
1238 }

## ◆ isBVComp()

boolean isBVComp | ( |  | ) |
| inline

Indicates whether the term is a bit-vector comparison

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1126 of file Expr.java.

1127 {
1128 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP;
1129 }

## ◆ isBVConcat()

boolean isBVConcat | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1056 of file Expr.java.

1057 {
1058 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT;
1059 }

## ◆ isBVExtract()

boolean isBVExtract | ( |  | ) |
| inline

Indicates whether the term is a bit-vector extraction

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1086 of file Expr.java.

1087 {
1088 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT;
1089 }

## ◆ isBVMul()

boolean isBVMul | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 795 of file Expr.java.

796 {
797 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL;
798 }

## ◆ isBVNAND()

boolean isBVNAND | ( |  | ) |
| inline

Indicates whether the term is a bit-wise NAND

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1026 of file Expr.java.

1027 {
1028 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND;
1029 }

## ◆ isBVNOR()

boolean isBVNOR | ( |  | ) |
| inline

Indicates whether the term is a bit-wise NOR

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1036 of file Expr.java.

1037 {
1038 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR;
1039 }

## ◆ isBVNOT()

boolean isBVNOT | ( |  | ) |
| inline

Indicates whether the term is a bit-wise NOT

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1006 of file Expr.java.

1007 {
1008 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT;
1009 }

## ◆ isBVNumeral()

boolean isBVNumeral | ( |  | ) |
| inline

Indicates whether the term is a bit-vector numeral

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 735 of file Expr.java.

736 {
737 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM;
738 }

## ◆ isBVOR()

boolean isBVOR | ( |  | ) |
| inline

Indicates whether the term is a bit-wise OR

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 996 of file Expr.java.

997 {
998 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
999 }

## ◆ isBVReduceAND()

boolean isBVReduceAND | ( |  | ) |
| inline

Indicates whether the term is a bit-vector reduce AND

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1116 of file Expr.java.

1117 {
1118 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND;
1119 }

## ◆ isBVReduceOR()

boolean isBVReduceOR | ( |  | ) |
| inline

Indicates whether the term is a bit-vector reduce OR

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1106 of file Expr.java.

1107 {
1108 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR;
1109 }

## ◆ isBVRepeat()

boolean isBVRepeat | ( |  | ) |
| inline

Indicates whether the term is a bit-vector repetition

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1096 of file Expr.java.

1097 {
1098 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT;
1099 }

## ◆ isBVRotateLeft()

boolean isBVRotateLeft | ( |  | ) |
| inline

Indicates whether the term is a bit-vector rotate left

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1166 of file Expr.java.

1167 {
1168 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT;
1169 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1188 of file Expr.java.

1189 {
1190 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT;
1191 }

## ◆ isBVRotateRight()

boolean isBVRotateRight | ( |  | ) |
| inline

Indicates whether the term is a bit-vector rotate right

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1176 of file Expr.java.

1177 {
1178 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT;
1179 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1200 of file Expr.java.

1201 {
1202 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT;
1203 }

## ◆ isBVSDiv()

boolean isBVSDiv | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 805 of file Expr.java.

806 {
807 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV;
808 }

## ◆ isBVSGE()

boolean isBVSGE | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 936 of file Expr.java.

937 {
938 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ;
939 }

## ◆ isBVSGT()

boolean isBVSGT | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 976 of file Expr.java.

977 {
978 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT;
979 }

## ◆ isBVShiftLeft()

boolean isBVShiftLeft | ( |  | ) |
| inline

Indicates whether the term is a bit-vector shift left

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1136 of file Expr.java.

1137 {
1138 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL;
1139 }

## ◆ isBVShiftRightArithmetic()

boolean isBVShiftRightArithmetic | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1156 of file Expr.java.

1157 {
1158 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR;
1159 }

## ◆ isBVShiftRightLogical()

boolean isBVShiftRightLogical | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1146 of file Expr.java.

1147 {
1148 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR;
1149 }

## ◆ isBVSignExtension()

boolean isBVSignExtension | ( |  | ) |
| inline

Indicates whether the term is a bit-vector sign extension

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1066 of file Expr.java.

1067 {
1068 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT;
1069 }

## ◆ isBVSLE()

boolean isBVSLE | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 915 of file Expr.java.

916 {
917 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ;
918 }

## ◆ isBVSLT()

boolean isBVSLT | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 956 of file Expr.java.

957 {
958 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT;
959 }

## ◆ isBVSMod()

boolean isBVSMod | ( |  | ) |
| inline

Indicates whether the term is a bit-vector signed modulus

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 845 of file Expr.java.

846 {
847 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD;
848 }

## ◆ isBVSRem()

boolean isBVSRem | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 825 of file Expr.java.

826 {
827 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM;
828 }

## ◆ isBVSub()

boolean isBVSub | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 785 of file Expr.java.

786 {
787 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB;
788 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1224 of file Expr.java.

1225 {
1226 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT;
1227 }

## ◆ isBVUDiv()

boolean isBVUDiv | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 815 of file Expr.java.

816 {
817 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV;
818 }

## ◆ isBVUGE()

boolean isBVUGE | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 926 of file Expr.java.

927 {
928 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ;
929 }

## ◆ isBVUGT()

boolean isBVUGT | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 966 of file Expr.java.

967 {
968 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT;
969 }

## ◆ isBVULE()

boolean isBVULE | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 905 of file Expr.java.

906 {
907 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ;
908 }

## ◆ isBVULT()

boolean isBVULT | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 946 of file Expr.java.

947 {
948 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT;
949 }

## ◆ isBVUMinus()

boolean isBVUMinus | ( |  | ) |
| inline

Indicates whether the term is a bit-vector unary minus

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 765 of file Expr.java.

766 {
767 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG;
768 }

## ◆ isBVURem()

boolean isBVURem | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 835 of file Expr.java.

836 {
837 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM;
838 }

## ◆ isBVXNOR()

boolean isBVXNOR | ( |  | ) |
| inline

Indicates whether the term is a bit-wise XNOR

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1046 of file Expr.java.

1047 {
1048 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR;
1049 }

## ◆ isBVXOR()

boolean isBVXOR | ( |  | ) |
| inline

Indicates whether the term is a bit-wise XOR

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1016 of file Expr.java.

1017 {
1018 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR;
1019 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1246 of file Expr.java.

1247 {
1248 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3;
1249 }

## ◆ isBVZeroExtension()

boolean isBVZeroExtension | ( |  | ) |
| inline

Indicates whether the term is a bit-vector zero extension

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1076 of file Expr.java.

1077 {
1078 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT;
1079 }

## ◆ 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 1317 of file Expr.java.

1318 {
1319 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SEQ_CONCAT;
1320 }

## ◆ isConst()

boolean isConst | ( |  | ) |
| inline

Indicates whether the term represents a constant.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 250 of file Expr.java.

251 {
252 return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
253 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 629 of file Expr.java.

630 {
631 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY;
632 }

## ◆ isDefaultArray()

boolean isDefaultArray | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 640 of file Expr.java.

641 {
642 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT;
643 }

## ◆ isDistinct()

boolean isDistinct | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 333 of file Expr.java.

334 {
335 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT;
336 }

## ◆ isDiv()

boolean isDiv | ( |  | ) |
| inline

Indicates whether the term is division (binary)

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 524 of file Expr.java.

525 {
526 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV;
527 }

## ◆ isEmptyRelation()

boolean isEmptyRelation | ( |  | ) |
| inline

Indicates whether the term is an empty relation

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1897 of file Expr.java.

1898 {
1899 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY;
1900 }

## ◆ isEq()

boolean isEq | ( |  | ) |
| inline

Indicates whether the term is an equality predicate.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 322 of file Expr.java.

323 {
324 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ;
325 }

## ◆ isFalse()

boolean isFalse | ( |  | ) |
| inline

Indicates whether the term is the constant false.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 312 of file Expr.java.

313 {
314 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE;
315 }

## ◆ isFiniteDomain()

boolean isFiniteDomain | ( |  | ) |
| inline

Indicates whether the term is of an array sort.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 2051 of file Expr.java.

2052 {
2053 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
2054 .getSortKind(getContext().nCtx(),
2055 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
2056 .toInt());
2057 }

## ◆ isFiniteDomainLT()

boolean isFiniteDomainLT | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 2064 of file Expr.java.

2065 {
2066 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT;
2067 }

## ◆ isGE()

boolean isGE | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 454 of file Expr.java.

455 {
456 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE;
457 }

## ◆ isGT()

boolean isGT | ( |  | ) |
| inline

Indicates whether the term is a greater-than

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 474 of file Expr.java.

475 {
476 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT;
477 }

## ◆ isIDiv()

boolean isIDiv | ( |  | ) |
| inline

Indicates whether the term is integer division (binary)

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 534 of file Expr.java.

535 {
536 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV;
537 }

## ◆ isIff()

boolean isIff | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 374 of file Expr.java.

375 {
376 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF;
377 }

## ◆ isImplies()

boolean isImplies | ( |  | ) |
| inline

Indicates whether the term is an implication

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 404 of file Expr.java.

405 {
406 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES;
407 }

## ◆ isInt()

boolean isInt | ( |  | ) |
| inline

Indicates whether the term is of integer sort.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 414 of file Expr.java.

415 {
416 return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT.toInt();
417 }

## ◆ isIntNum()

boolean isIntNum | ( |  | ) |
| inline

Indicates whether the term is an integer numeral.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 260 of file Expr.java.

261 {
262 return isNumeral() && isInt();
263 }
com.microsoft.z3.Expr.isInt
boolean isInt()
Definition: Expr.java:414
com.microsoft.z3.Expr.isNumeral
boolean isNumeral()
Definition: Expr.java:218

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1212 of file Expr.java.

1213 {
1214 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV;
1215 }

## ◆ isIntToReal()

boolean isIntToReal | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 564 of file Expr.java.

565 {
566 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL;
567 }

## ◆ isIsEmptyRelation()

boolean isIsEmptyRelation | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1907 of file Expr.java.

1908 {
1909 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY;
1910 }

## ◆ isITE()

boolean isITE | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 343 of file Expr.java.

344 {
345 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE;
346 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1259 of file Expr.java.

1260 {
1261 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL;
1262 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1272 of file Expr.java.

1273 {
1274 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
1275 }

## ◆ isLE()

boolean isLE | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 444 of file Expr.java.

445 {
446 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE;
447 }

## ◆ isLT()

boolean isLT | ( |  | ) |
| inline

Indicates whether the term is a less-than

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 464 of file Expr.java.

465 {
466 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT;
467 }

## ◆ isModulus()

boolean isModulus | ( |  | ) |
| inline

Indicates whether the term is modulus (binary)

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 554 of file Expr.java.

555 {
556 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD;
557 }

## ◆ isMul()

boolean isMul | ( |  | ) |
| inline

Indicates whether the term is multiplication (binary)

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 514 of file Expr.java.

515 {
516 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL;
517 }

## ◆ isNot()

boolean isNot | ( |  | ) |
| inline

Indicates whether the term is a negation

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 394 of file Expr.java.

395 {
396 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT;
397 }

## ◆ isNumeral()

boolean isNumeral | ( |  | ) |
| inline

Indicates whether the term is a numeral

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 218 of file Expr.java.

219 {
220 return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
221 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1329 of file Expr.java.

1330 {
1331 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
1332 }

## ◆ isOr()

boolean isOr | ( |  | ) |
| inline

Indicates whether the term is an n-ary disjunction

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 363 of file Expr.java.

364 {
365 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR;
366 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1489 of file Expr.java.

1490 {
1491 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM;
1492 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1748 of file Expr.java.

1749 {
1750 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF;
1751 }

## ◆ isProofAsserted()

boolean isProofAsserted | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1349 of file Expr.java.

1350 {
1351 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED;
1352 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1687 of file Expr.java.

1688 {
1689 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY;
1690 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1713 of file Expr.java.

1714 {
1715 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM;
1716 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1736 of file Expr.java.

1737 {
1738 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO;
1739 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1595 of file Expr.java.

1596 {
1597 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER;
1598 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1478 of file Expr.java.

1479 {
1480 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY;
1481 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1579 of file Expr.java.

1580 {
1581 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS;
1582 }

## ◆ isProofGoal()

boolean isProofGoal | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1360 of file Expr.java.

1361 {
1362 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL;
1363 }

## ◆ isProofHypothesis()

boolean isProofHypothesis | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1619 of file Expr.java.

1620 {
1621 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS;
1622 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1670 of file Expr.java.

1671 {
1672 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE;
1673 }

## ◆ isProofIFFOEQ()

boolean isProofIFFOEQ | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1760 of file Expr.java.

1761 {
1762 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ;
1763 }

## ◆ isProofIFFTrue()

boolean isProofIFFTrue | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1658 of file Expr.java.

1659 {
1660 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE;
1661 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1635 of file Expr.java.

1636 {
1637 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA;
1638 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1374 of file Expr.java.

1375 {
1376 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS;
1377 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1838 of file Expr.java.

1839 {
1840 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ;
1841 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1448 of file Expr.java.

1449 {
1450 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY;
1451 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1807 of file Expr.java.

1808 {
1809 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
1810 }

## ◆ 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 R) q) (forall (x R) 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1788 of file Expr.java.

1789 {
1790 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS;
1791 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1500 of file Expr.java.

1501 {
1502 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM;
1503 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1548 of file Expr.java.

1549 {
1550 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
1551 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1563 of file Expr.java.

1564 {
1565 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT;
1566 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1607 of file Expr.java.

1608 {
1609 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST;
1610 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1459 of file Expr.java.

1460 {
1461 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO;
1462 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1389 of file Expr.java.

1390 {
1391 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY;
1392 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1520 of file Expr.java.

1521 {
1522 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE;
1523 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1536 of file Expr.java.

1537 {
1538 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR;
1539 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1825 of file Expr.java.

1826 {
1827 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE;
1828 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1401 of file Expr.java.

1402 {
1403 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY;
1404 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1860 of file Expr.java.

1861 {
1862 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA;
1863 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1413 of file Expr.java.

1414 {
1415 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY;
1416 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1433 of file Expr.java.

1434 {
1435 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR;
1436 }

## ◆ isProofTrue()

boolean isProofTrue | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1339 of file Expr.java.

1340 {
1341 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE;
1342 }

## ◆ 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) ... R(n+1): (not l_n) * [unit-resolution T1 ... R(n+1)]: (or l_1' ... l_m')

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1646 of file Expr.java.

1647 {
1648 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION;
1649 }

## ◆ isRatNum()

boolean isRatNum | ( |  | ) |
| inline

Indicates whether the term is a real numeral.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 270 of file Expr.java.

271 {
272 return isNumeral() && isReal();
273 }
com.microsoft.z3.Expr.isReal
boolean isReal()
Definition: Expr.java:424

## ◆ isReal()

boolean isReal | ( |  | ) |
| inline

Indicates whether the term is of sort real.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 424 of file Expr.java.

425 {
426 return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT.toInt();
427 }

## ◆ isRealIsInt()

boolean isRealIsInt | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 585 of file Expr.java.

586 {
587 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT;
588 }

## ◆ isRealToInt()

boolean isRealToInt | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 574 of file Expr.java.

575 {
576 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT;
577 }

## ◆ isRelation()

boolean isRelation | ( |  | ) |
| inline

Indicates whether the term is of an array sort.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1870 of file Expr.java.

1871 {
1872 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1873 .getSortKind(getContext().nCtx(),
1874 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1875 .toInt());
1876 }

## ◆ isRelationalJoin()

boolean isRelationalJoin | ( |  | ) |
| inline

Indicates whether the term is a relational join

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1917 of file Expr.java.

1918 {
1919 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN;
1920 }

## ◆ 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 `isRelationUnion` to perform destructive updates to the first argument.

See also
  isRelationUnion

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 2041 of file Expr.java.

2042 {
2043 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE;
2044 }

## ◆ isRelationComplement()

boolean isRelationComplement | ( |  | ) |
| inline

Indicates whether the term is the complement of a relation

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 2011 of file Expr.java.

2012 {
2013 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT;
2014 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1969 of file Expr.java.

1970 {
1971 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER;
1972 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1989 of file Expr.java.

1990 {
1991 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER;
1992 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1954 of file Expr.java.

1955 {
1956 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT;
1957 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 2001 of file Expr.java.

2002 {
2003 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME;
2004 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 2025 of file Expr.java.

2026 {
2027 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT;
2028 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 1887 of file Expr.java.

1888 {
1889 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE;
1890 }

## ◆ isRelationUnion()

boolean isRelationUnion | ( |  | ) |
| inline

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

Remarks: The function takes two arguments.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1929 of file Expr.java.

1930 {
1931 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION;
1932 }

## ◆ isRelationWiden()

boolean isRelationWiden | ( |  | ) |
| inline

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

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 1941 of file Expr.java.

1942 {
1943 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN;
1944 }

## ◆ isRemainder()

boolean isRemainder | ( |  | ) |
| inline

Indicates whether the term is remainder (binary)

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 544 of file Expr.java.

545 {
546 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM;
547 }

## ◆ isSelect()

boolean isSelect | ( |  | ) |
| inline

Indicates whether the term is an array select.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 618 of file Expr.java.

619 {
620 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT;
621 }

## ◆ isSetComplement()

boolean isSetComplement | ( |  | ) |
| inline

Indicates whether the term is set complement

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 703 of file Expr.java.

704 {
705 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT;
706 }

## ◆ isSetDifference()

boolean isSetDifference | ( |  | ) |
| inline

Indicates whether the term is set difference

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 693 of file Expr.java.

694 {
695 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE;
696 }

## ◆ isSetIntersect()

boolean isSetIntersect | ( |  | ) |
| inline

Indicates whether the term is set intersection

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 683 of file Expr.java.

684 {
685 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT;
686 }

## ◆ isSetSubset()

boolean isSetSubset | ( |  | ) |
| inline

Indicates whether the term is set subset

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 713 of file Expr.java.

714 {
715 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET;
716 }

## ◆ isSetUnion()

boolean isSetUnion | ( |  | ) |
| inline

Indicates whether the term is set union

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 673 of file Expr.java.

674 {
675 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION;
676 }

## ◆ 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

  Z3Exception | on error

Returns
  a boolean

Definition at line 608 of file Expr.java.

609 {
610 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE;
611 }

## ◆ isString()

boolean isString | ( |  | ) |
| inline

Check whether expression is a string constant.

Returns
  a boolean

Definition at line 1281 of file Expr.java.

1282 {
1283 return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
1284 }

## ◆ isSub()

boolean isSub | ( |  | ) |
| inline

Indicates whether the term is subtraction (binary)

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 494 of file Expr.java.

495 {
496 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB;
497 }

## ◆ isTrue()

boolean isTrue | ( |  | ) |
| inline

Indicates whether the term is the constant true.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 302 of file Expr.java.

303 {
304 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE;
305 }

## ◆ isUMinus()

boolean isUMinus | ( |  | ) |
| inline

Indicates whether the term is a unary minus

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 504 of file Expr.java.

505 {
506 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS;
507 }

## ◆ isWellSorted()

boolean isWellSorted | ( |  | ) |
| inline

Indicates whether the term is well-sorted.

Exceptions

  Z3Exception | on error

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

Definition at line 229 of file Expr.java.

230 {
231 return Native.isWellSorted(getContext().nCtx(), getNativeObject());
232 }

## ◆ isXor()

boolean isXor | ( |  | ) |
| inline

Indicates whether the term is an exclusive or

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 384 of file Expr.java.

385 {
386 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR;
387 }

## ◆ simplify() [1/2]

Expr< R > simplify | ( |  | ) |
| inline

Returns a simplified version of the expression

Returns
  Expr

Exceptions

  Z3Exception | on error

Definition at line 41 of file Expr.java.

42 {
43 return simplify(null);
44 }
com.microsoft.z3.Expr.simplify
Expr< R > simplify()
Definition: Expr.java:41

## ◆ simplify() [2/2]

Expr< R > simplify | ( | Params | p | ) |
| inline

Returns a simplified version of the expression A set of parameters

Parameters

  p | a Params object to configure the simplifier

See also
  Context::SimplifyHelp

Returns
  an Expr

Exceptions

  Z3Exception | on error

Definition at line 55 of file Expr.java.

56 {
57
58 if (p == null) {
59 return (Expr<R>) Expr.create(getContext(),
60 Native.simplify(getContext().nCtx(), getNativeObject()));
61 }
62 else {
63 return (Expr<R>) Expr.create(
64 getContext(),
65 Native.simplifyEx(getContext().nCtx(), getNativeObject(),
66 p.getNativeObject()));
67 }
68 }

## ◆ substitute() [1/2]

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

Substitute every occurrence of `from` in the expression with `to`.

See also
  Expr::substitute(Expr[],Expr[])

Exceptions

  Z3Exception | on error

Returns
  an Expr

Definition at line 168 of file Expr.java.

169 {
170 return substitute(new Expr[] { from }, new Expr[] { to });
171 }
com.microsoft.z3.Expr.substitute
Expr< R > substitute(Expr<?>[] from, Expr<?>[] to)
Definition: Expr.java:149

## ◆ substitute() [2/2]

Expr< R > 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

  Z3Exception | on error

Returns
  an Expr

Definition at line 149 of file Expr.java.

150 {
151 getContext().checkContextMatch(from);
152 getContext().checkContextMatch(to);
153 if (from.length != to.length) {
154 throw new Z3Exception("Argument sizes do not match");
155 }
156 return (Expr<R>) Expr.create(getContext(), Native.substitute(getContext().nCtx(),
157 getNativeObject(), from.length, Expr.arrayToNative(from),
158 Expr.arrayToNative(to)));
159 }

## ◆ substituteVars()

Expr< R > 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

  Z3Exception | on error
  Z3Exception | on error

Returns
  an Expr

Definition at line 183 of file Expr.java.

184 {
185
186 getContext().checkContextMatch(to);
187 return (Expr<R>) Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
188 getNativeObject(), to.length, Expr.arrayToNative(to)));
189 }

## ◆ toString()

String toString | ( |  | ) |
| inline

Returns a string representation of the expression.

Reimplemented from AST.

Definition at line 208 of file Expr.java.

209 {
210 return super.toString();
211 }

Referenced by Optimize.AssertSoft().

## ◆ translate()

Expr< R > translate | ( | Context | ctx | ) |
| inline

Translates (copies) the term to the Context `ctx`.

Parameters

  ctx | A context

Returns
  A copy of the term which is associated with `ctx`

Exceptions

  Z3Exception | on error

Reimplemented from AST.

Definition at line 199 of file Expr.java.

200 {
201 return (Expr<R>) super.translate(ctx);
202 }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Solver.__deepcopy__(), and Expr< R extends Sort >.translate().

## ◆ update()

Expr< R > 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

  args | arguments

Exceptions

  Z3Exception | on error

Definition at line 127 of file Expr.java.

128 {
129 getContext().checkContextMatch(args);
130 if (isApp() && args.length != getNumArgs()) {
131 throw new Z3Exception("Number of arguments does not match");
132 }
133 return (Expr<R>) Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
134 args.length, Expr.arrayToNative(args)));
135 }