Z3
Expr.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import java.lang.reflect.Type;
21import java.lang.reflect.ParameterizedType;
22
23import com.microsoft.z3.enumerations.Z3_ast_kind;
24import com.microsoft.z3.enumerations.Z3_decl_kind;
25import com.microsoft.z3.enumerations.Z3_lbool;
26import com.microsoft.z3.enumerations.Z3_sort_kind;
27
28/* using System; */
29
33@SuppressWarnings("unchecked")
34public class Expr<R extends Sort> extends AST
35{
42 {
43 return simplify(null);
44 }
45
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 }
69
77 {
78 return new FuncDecl<>(getContext(), Native.getAppDecl(getContext().nCtx(),
79 getNativeObject()));
80 }
81
89 {
90 return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
91 getNativeObject()));
92 }
93
99 public int getNumArgs()
100 {
101 return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
102 }
103
109 public Expr<?>[] getArgs()
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 }
119
127 public Expr<R> update(Expr<?>[] args)
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 }
136
149 public Expr<R> substitute(Expr<?>[] from, Expr<?>[] to)
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 }
160
169 {
170 return substitute(new Expr[] { from }, new Expr[] { to });
171 }
172
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 }
190
200 {
201 return (Expr<R>) super.translate(ctx);
202 }
203
207 @Override
209 {
210 return super.toString();
211 }
212
218 public boolean isNumeral()
219 {
220 return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
221 }
222
229 public boolean isWellSorted()
230 {
231 return Native.isWellSorted(getContext().nCtx(), getNativeObject());
232 }
233
239 public R getSort()
240 {
241 return (R) Sort.create(getContext(),
242 Native.getSort(getContext().nCtx(), getNativeObject()));
243 }
244
250 public boolean isConst()
251 {
252 return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
253 }
254
260 public boolean isIntNum()
261 {
262 return isNumeral() && isInt();
263 }
264
270 public boolean isRatNum()
271 {
272 return isNumeral() && isReal();
273 }
274
280 public boolean isAlgebraicNumber()
281 {
282 return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
283 }
284
290 public boolean isBool()
291 {
292 return (isExpr() && Native.isEqSort(getContext().nCtx(),
293 Native.mkBoolSort(getContext().nCtx()),
294 Native.getSort(getContext().nCtx(), getNativeObject())));
295 }
296
302 public boolean isTrue()
303 {
304 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE;
305 }
306
312 public boolean isFalse()
313 {
314 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE;
315 }
316
322 public boolean isEq()
323 {
324 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ;
325 }
326
333 public boolean isDistinct()
334 {
335 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT;
336 }
337
343 public boolean isITE()
344 {
345 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE;
346 }
347
353 public boolean isAnd()
354 {
355 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND;
356 }
357
363 public boolean isOr()
364 {
365 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR;
366 }
367
374 public boolean isIff()
375 {
376 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF;
377 }
378
384 public boolean isXor()
385 {
386 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR;
387 }
388
394 public boolean isNot()
395 {
396 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT;
397 }
398
404 public boolean isImplies()
405 {
406 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES;
407 }
408
414 public boolean isInt()
415 {
416 return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT.toInt();
417 }
418
424 public boolean isReal()
425 {
426 return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT.toInt();
427 }
428
434 public boolean isArithmeticNumeral()
435 {
436 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM;
437 }
438
444 public boolean isLE()
445 {
446 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE;
447 }
448
454 public boolean isGE()
455 {
456 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE;
457 }
458
464 public boolean isLT()
465 {
466 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT;
467 }
468
474 public boolean isGT()
475 {
476 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT;
477 }
478
484 public boolean isAdd()
485 {
486 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD;
487 }
488
494 public boolean isSub()
495 {
496 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB;
497 }
498
504 public boolean isUMinus()
505 {
506 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS;
507 }
508
514 public boolean isMul()
515 {
516 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL;
517 }
518
524 public boolean isDiv()
525 {
526 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV;
527 }
528
534 public boolean isIDiv()
535 {
536 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV;
537 }
538
544 public boolean isRemainder()
545 {
546 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM;
547 }
548
554 public boolean isModulus()
555 {
556 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD;
557 }
558
564 public boolean isIntToReal()
565 {
566 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL;
567 }
568
574 public boolean isRealToInt()
575 {
576 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT;
577 }
578
585 public boolean isRealIsInt()
586 {
587 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT;
588 }
589
595 public boolean isArray()
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 }
601
608 public boolean isStore()
609 {
610 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE;
611 }
612
618 public boolean isSelect()
619 {
620 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT;
621 }
622
629 public boolean isConstantArray()
630 {
631 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY;
632 }
633
640 public boolean isDefaultArray()
641 {
642 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT;
643 }
644
652 public boolean isArrayMap()
653 {
654 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP;
655 }
656
663 public boolean isAsArray()
664 {
665 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY;
666 }
667
673 public boolean isSetUnion()
674 {
675 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION;
676 }
677
683 public boolean isSetIntersect()
684 {
685 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT;
686 }
687
693 public boolean isSetDifference()
694 {
695 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE;
696 }
697
703 public boolean isSetComplement()
704 {
705 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT;
706 }
707
713 public boolean isSetSubset()
714 {
715 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET;
716 }
717
723 public boolean isBV()
724 {
725 return Native.getSortKind(getContext().nCtx(),
726 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
727 .toInt();
728 }
729
735 public boolean isBVNumeral()
736 {
737 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM;
738 }
739
745 public boolean isBVBitOne()
746 {
747 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1;
748 }
749
755 public boolean isBVBitZero()
756 {
757 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0;
758 }
759
765 public boolean isBVUMinus()
766 {
767 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG;
768 }
769
775 public boolean isBVAdd()
776 {
777 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD;
778 }
779
785 public boolean isBVSub()
786 {
787 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB;
788 }
789
795 public boolean isBVMul()
796 {
797 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL;
798 }
799
805 public boolean isBVSDiv()
806 {
807 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV;
808 }
809
815 public boolean isBVUDiv()
816 {
817 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV;
818 }
819
825 public boolean isBVSRem()
826 {
827 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM;
828 }
829
835 public boolean isBVURem()
836 {
837 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM;
838 }
839
845 public boolean isBVSMod()
846 {
847 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD;
848 }
849
855 boolean isBVSDiv0()
856 {
857 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV0;
858 }
859
865 boolean isBVUDiv0()
866 {
867 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV0;
868 }
869
875 boolean isBVSRem0()
876 {
877 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM0;
878 }
879
885 boolean isBVURem0()
886 {
887 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM0;
888 }
889
895 boolean isBVSMod0()
896 {
897 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD0;
898 }
899
905 public boolean isBVULE()
906 {
907 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ;
908 }
909
915 public boolean isBVSLE()
916 {
917 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ;
918 }
919
926 public boolean isBVUGE()
927 {
928 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ;
929 }
930
936 public boolean isBVSGE()
937 {
938 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ;
939 }
940
946 public boolean isBVULT()
947 {
948 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT;
949 }
950
956 public boolean isBVSLT()
957 {
958 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT;
959 }
960
966 public boolean isBVUGT()
967 {
968 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT;
969 }
970
976 public boolean isBVSGT()
977 {
978 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT;
979 }
980
986 public boolean isBVAND()
987 {
988 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND;
989 }
990
996 public boolean isBVOR()
997 {
998 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
999 }
1000
1006 public boolean isBVNOT()
1007 {
1008 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT;
1009 }
1010
1016 public boolean isBVXOR()
1017 {
1018 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR;
1019 }
1020
1026 public boolean isBVNAND()
1027 {
1028 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND;
1029 }
1030
1036 public boolean isBVNOR()
1037 {
1038 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR;
1039 }
1040
1046 public boolean isBVXNOR()
1047 {
1048 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR;
1049 }
1050
1056 public boolean isBVConcat()
1057 {
1058 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT;
1059 }
1060
1066 public boolean isBVSignExtension()
1067 {
1068 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT;
1069 }
1070
1076 public boolean isBVZeroExtension()
1077 {
1078 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT;
1079 }
1080
1086 public boolean isBVExtract()
1087 {
1088 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT;
1089 }
1090
1096 public boolean isBVRepeat()
1097 {
1098 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT;
1099 }
1100
1106 public boolean isBVReduceOR()
1107 {
1108 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR;
1109 }
1110
1116 public boolean isBVReduceAND()
1117 {
1118 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND;
1119 }
1120
1126 public boolean isBVComp()
1127 {
1128 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP;
1129 }
1130
1136 public boolean isBVShiftLeft()
1137 {
1138 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL;
1139 }
1140
1146 public boolean isBVShiftRightLogical()
1147 {
1148 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR;
1149 }
1150
1157 {
1158 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR;
1159 }
1160
1166 public boolean isBVRotateLeft()
1167 {
1168 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT;
1169 }
1170
1176 public boolean isBVRotateRight()
1177 {
1178 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT;
1179 }
1180
1188 public boolean isBVRotateLeftExtended()
1189 {
1190 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT;
1191 }
1192
1201 {
1202 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT;
1203 }
1204
1212 public boolean isIntToBV()
1213 {
1214 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV;
1215 }
1216
1224 public boolean isBVToInt()
1225 {
1226 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT;
1227 }
1228
1235 public boolean isBVCarry()
1236 {
1237 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY;
1238 }
1239
1246 public boolean isBVXOR3()
1247 {
1248 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3;
1249 }
1250
1259 public boolean isLabel()
1260 {
1261 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL;
1262 }
1263
1272 public boolean isLabelLit()
1273 {
1274 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
1275 }
1276
1281 public boolean isString()
1282 {
1283 return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
1284 }
1285
1293 {
1294 return Native.getString(getContext().nCtx(), getNativeObject());
1295 }
1296
1317 public boolean isConcat()
1318 {
1319 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SEQ_CONCAT;
1320 }
1321
1329 public boolean isOEQ()
1330 {
1331 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
1332 }
1333
1339 public boolean isProofTrue()
1340 {
1341 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE;
1342 }
1343
1349 public boolean isProofAsserted()
1350 {
1351 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED;
1352 }
1353
1360 public boolean isProofGoal()
1361 {
1362 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL;
1363 }
1364
1374 public boolean isProofModusPonens()
1375 {
1376 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS;
1377 }
1378
1389 public boolean isProofReflexivity()
1390 {
1391 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY;
1392 }
1393
1401 public boolean isProofSymmetry()
1402 {
1403 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY;
1404 }
1405
1413 public boolean isProofTransitivity()
1414 {
1415 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY;
1416 }
1417
1434 {
1435 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR;
1436 }
1437
1448 public boolean isProofMonotonicity()
1449 {
1450 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY;
1451 }
1452
1459 public boolean isProofQuantIntro()
1460 {
1461 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO;
1462 }
1463
1478 public boolean isProofDistributivity()
1479 {
1480 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY;
1481 }
1482
1489 public boolean isProofAndElimination()
1490 {
1491 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM;
1492 }
1493
1500 public boolean isProofOrElimination()
1501 {
1502 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM;
1503 }
1504
1520 public boolean isProofRewrite()
1521 {
1522 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE;
1523 }
1524
1536 public boolean isProofRewriteStar()
1537 {
1538 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR;
1539 }
1540
1548 public boolean isProofPullQuant()
1549 {
1550 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
1551 }
1552
1553
1563 public boolean isProofPushQuant()
1564 {
1565 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT;
1566 }
1567
1579 public boolean isProofElimUnusedVars()
1580 {
1581 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS;
1582 }
1583
1595 public boolean isProofDER()
1596 {
1597 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER;
1598 }
1599
1607 public boolean isProofQuantInst()
1608 {
1609 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST;
1610 }
1611
1619 public boolean isProofHypothesis()
1620 {
1621 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS;
1622 }
1623
1635 public boolean isProofLemma()
1636 {
1637 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA;
1638 }
1639
1646 public boolean isProofUnitResolution()
1647 {
1648 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION;
1649 }
1650
1658 public boolean isProofIFFTrue()
1659 {
1660 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE;
1661 }
1662
1670 public boolean isProofIFFFalse()
1671 {
1672 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE;
1673 }
1674
1687 public boolean isProofCommutativity()
1688 {
1689 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY;
1690 }
1691
1713 public boolean isProofDefAxiom()
1714 {
1715 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM;
1716 }
1717
1736 public boolean isProofDefIntro()
1737 {
1738 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO;
1739 }
1740
1748 public boolean isProofApplyDef()
1749 {
1750 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF;
1751 }
1752
1760 public boolean isProofIFFOEQ()
1761 {
1762 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ;
1763 }
1764
1788 public boolean isProofNNFPos()
1789 {
1790 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS;
1791 }
1792
1807 public boolean isProofNNFNeg()
1808 {
1809 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
1810 }
1811
1812
1825 public boolean isProofSkolemize()
1826 {
1827 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE;
1828 }
1829
1838 public boolean isProofModusPonensOEQ()
1839 {
1840 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ;
1841 }
1842
1860 public boolean isProofTheoryLemma()
1861 {
1862 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA;
1863 }
1864
1870 public boolean isRelation()
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 }
1877
1887 public boolean isRelationStore()
1888 {
1889 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE;
1890 }
1891
1897 public boolean isEmptyRelation()
1898 {
1899 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY;
1900 }
1901
1907 public boolean isIsEmptyRelation()
1908 {
1909 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY;
1910 }
1911
1917 public boolean isRelationalJoin()
1918 {
1919 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN;
1920 }
1921
1929 public boolean isRelationUnion()
1930 {
1931 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION;
1932 }
1933
1941 public boolean isRelationWiden()
1942 {
1943 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN;
1944 }
1945
1954 public boolean isRelationProject()
1955 {
1956 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT;
1957 }
1958
1969 public boolean isRelationFilter()
1970 {
1971 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER;
1972 }
1973
1990 {
1991 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER;
1992 }
1993
2001 public boolean isRelationRename()
2002 {
2003 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME;
2004 }
2005
2011 public boolean isRelationComplement()
2012 {
2013 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT;
2014 }
2015
2025 public boolean isRelationSelect()
2026 {
2027 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT;
2028 }
2029
2041 public boolean isRelationClone()
2042 {
2043 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE;
2044 }
2045
2051 public boolean isFiniteDomain()
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 }
2058
2064 public boolean isFiniteDomainLT()
2065 {
2066 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT;
2067 }
2068
2087 public int getIndex()
2088 {
2089 if (!isVar()) {
2090 throw new Z3Exception("Term is not a bound variable.");
2091 }
2092
2093 return Native.getIndexValue(getContext().nCtx(), getNativeObject());
2094 }
2095
2096 private Class sort = null;
2097
2106 public <S extends R> Expr<S> distillSort(Class<S> newSort) {
2107 if (sort != null && !newSort.isAssignableFrom(sort)) {
2108 throw new Z3Exception(
2109 String.format("Cannot distill expression of sort %s to %s.", sort.getName(), newSort.getName()));
2110 }
2111
2112 return (Expr<S>) ((Expr<?>) this);
2113 }
2114
2119 protected Expr(Context ctx, long obj) {
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 }
2129
2130 @Override
2131 void checkNativeObject(long obj) {
2132 if (!Native.isApp(getContext().nCtx(), obj) &&
2133 Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
2134 Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) {
2135 throw new Z3Exception("Underlying object is not a term");
2136 }
2137 super.checkNativeObject(obj);
2138 }
2139
2140 static <U extends Sort> Expr<U> create(Context ctx, FuncDecl<U> f, Expr<?> ... arguments)
2141 {
2142 long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
2143 AST.arrayLength(arguments), AST.arrayToNative(arguments));
2144 return (Expr<U>) create(ctx, obj);
2145 }
2146
2147 // TODO generify, but it conflicts with AST.create
2148 static Expr<?> create(Context ctx, long obj)
2149 {
2150 Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
2151 if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
2152 return new Quantifier(ctx, obj);
2153 long s = Native.getSort(ctx.nCtx(), obj);
2155 .fromInt(Native.getSortKind(ctx.nCtx(), s));
2156
2157 if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast?
2158 return new AlgebraicNum(ctx, obj);
2159
2160 if (Native.isNumeralAst(ctx.nCtx(), obj))
2161 {
2162 switch (sk)
2163 {
2164 case Z3_INT_SORT:
2165 return new IntNum(ctx, obj);
2166 case Z3_REAL_SORT:
2167 return new RatNum(ctx, obj);
2168 case Z3_BV_SORT:
2169 return new BitVecNum(ctx, obj);
2171 return new FPNum(ctx, obj);
2173 return new FPRMNum(ctx, obj);
2175 return new FiniteDomainNum(ctx, obj);
2176 default:
2177 }
2178 }
2179
2180 switch (sk)
2181 {
2182 case Z3_BOOL_SORT:
2183 return new BoolExpr(ctx, obj);
2184 case Z3_INT_SORT:
2185 return new IntExpr(ctx, obj);
2186 case Z3_REAL_SORT:
2187 return new RealExpr(ctx, obj);
2188 case Z3_BV_SORT:
2189 return new BitVecExpr(ctx, obj);
2190 case Z3_ARRAY_SORT:
2191 return new ArrayExpr<>(ctx, obj);
2192 case Z3_DATATYPE_SORT:
2193 return new DatatypeExpr<>(ctx, obj);
2195 return new FPExpr(ctx, obj);
2197 return new FPRMExpr(ctx, obj);
2199 return new FiniteDomainExpr(ctx, obj);
2200 case Z3_SEQ_SORT:
2201 return new SeqExpr<>(ctx, obj);
2202 case Z3_RE_SORT:
2203 return new ReExpr<>(ctx, obj);
2204 default:
2205 }
2206
2207 return new Expr<>(ctx, obj);
2208 }
2209}
boolean isBVOR()
Definition: Expr.java:996
boolean isProofLemma()
Definition: Expr.java:1635
boolean isSetUnion()
Definition: Expr.java:673
boolean isRelation()
Definition: Expr.java:1870
boolean isSelect()
Definition: Expr.java:618
boolean isBVRepeat()
Definition: Expr.java:1096
boolean isLT()
Definition: Expr.java:464
boolean isConstantArray()
Definition: Expr.java:629
Expr(Context ctx, long obj)
Definition: Expr.java:2119
boolean isProofHypothesis()
Definition: Expr.java:1619
boolean isProofDER()
Definition: Expr.java:1595
boolean isBVSRem()
Definition: Expr.java:825
boolean isImplies()
Definition: Expr.java:404
boolean isArrayMap()
Definition: Expr.java:652
boolean isDiv()
Definition: Expr.java:524
boolean isProofTransitivityStar()
Definition: Expr.java:1433
boolean isMul()
Definition: Expr.java:514
boolean isProofAsserted()
Definition: Expr.java:1349
boolean isNot()
Definition: Expr.java:394
boolean isBVSLT()
Definition: Expr.java:956
boolean isBVRotateRightExtended()
Definition: Expr.java:1200
boolean isInt()
Definition: Expr.java:414
Expr< R > substitute(Expr<?>[] from, Expr<?>[] to)
Definition: Expr.java:149
boolean isRelationFilter()
Definition: Expr.java:1969
boolean isEmptyRelation()
Definition: Expr.java:1897
Z3_lbool getBoolValue()
Definition: Expr.java:88
Expr< R > substituteVars(Expr<?>[] to)
Definition: Expr.java:183
boolean isBVXOR()
Definition: Expr.java:1016
boolean isProofIFFTrue()
Definition: Expr.java:1658
boolean isIntToBV()
Definition: Expr.java:1212
boolean isUMinus()
Definition: Expr.java:504
boolean isRelationalJoin()
Definition: Expr.java:1917
boolean isBVUGE()
Definition: Expr.java:926
boolean isFalse()
Definition: Expr.java:312
boolean isProofApplyDef()
Definition: Expr.java:1748
boolean isBVXOR3()
Definition: Expr.java:1246
Expr< R > simplify(Params p)
Definition: Expr.java:55
boolean isProofNNFNeg()
Definition: Expr.java:1807
boolean isBVToInt()
Definition: Expr.java:1224
Expr< R > simplify()
Definition: Expr.java:41
boolean isBVSLE()
Definition: Expr.java:915
boolean isProofTrue()
Definition: Expr.java:1339
boolean isBVNAND()
Definition: Expr.java:1026
boolean isProofQuantIntro()
Definition: Expr.java:1459
boolean isProofReflexivity()
Definition: Expr.java:1389
boolean isIff()
Definition: Expr.java:374
boolean isProofModusPonensOEQ()
Definition: Expr.java:1838
boolean isProofTransitivity()
Definition: Expr.java:1413
boolean isWellSorted()
Definition: Expr.java:229
boolean isBVComp()
Definition: Expr.java:1126
boolean isProofPullQuant()
Definition: Expr.java:1548
boolean isProofOrElimination()
Definition: Expr.java:1500
boolean isBVSGT()
Definition: Expr.java:976
boolean isLE()
Definition: Expr.java:444
boolean isProofIFFFalse()
Definition: Expr.java:1670
boolean isProofQuantInst()
Definition: Expr.java:1607
boolean isBVExtract()
Definition: Expr.java:1086
boolean isProofPushQuant()
Definition: Expr.java:1563
boolean isRelationUnion()
Definition: Expr.java:1929
boolean isProofTheoryLemma()
Definition: Expr.java:1860
boolean isRealToInt()
Definition: Expr.java:574
boolean isBVRotateLeftExtended()
Definition: Expr.java:1188
Expr<?>[] getArgs()
Definition: Expr.java:109
boolean isProofSkolemize()
Definition: Expr.java:1825
boolean isRelationClone()
Definition: Expr.java:2041
boolean isBV()
Definition: Expr.java:723
boolean isBVBitZero()
Definition: Expr.java:755
boolean isBVSub()
Definition: Expr.java:785
boolean isProofElimUnusedVars()
Definition: Expr.java:1579
boolean isProofSymmetry()
Definition: Expr.java:1401
boolean isProofMonotonicity()
Definition: Expr.java:1448
boolean isXor()
Definition: Expr.java:384
boolean isIDiv()
Definition: Expr.java:534
boolean isBVXNOR()
Definition: Expr.java:1046
boolean isBVZeroExtension()
Definition: Expr.java:1076
Expr< R > translate(Context ctx)
Definition: Expr.java:199
boolean isAlgebraicNumber()
Definition: Expr.java:280
boolean isSetDifference()
Definition: Expr.java:693
boolean isProofAndElimination()
Definition: Expr.java:1489
boolean isProofDefIntro()
Definition: Expr.java:1736
boolean isGE()
Definition: Expr.java:454
boolean isBVRotateRight()
Definition: Expr.java:1176
boolean isArray()
Definition: Expr.java:595
boolean isSetComplement()
Definition: Expr.java:703
boolean isProofGoal()
Definition: Expr.java:1360
boolean isConcat()
Definition: Expr.java:1317
boolean isStore()
Definition: Expr.java:608
boolean isIntToReal()
Definition: Expr.java:564
boolean isString()
Definition: Expr.java:1281
boolean isArithmeticNumeral()
Definition: Expr.java:434
boolean isBVShiftRightArithmetic()
Definition: Expr.java:1156
boolean isBVCarry()
Definition: Expr.java:1235
boolean isRatNum()
Definition: Expr.java:270
boolean isFiniteDomainLT()
Definition: Expr.java:2064
FuncDecl< R > getFuncDecl()
Definition: Expr.java:76
boolean isIsEmptyRelation()
Definition: Expr.java:1907
boolean isLabel()
Definition: Expr.java:1259
boolean isReal()
Definition: Expr.java:424
boolean isBVSGE()
Definition: Expr.java:936
boolean isBVRotateLeft()
Definition: Expr.java:1166
boolean isITE()
Definition: Expr.java:343
boolean isBVSDiv()
Definition: Expr.java:805
Expr< R > update(Expr<?>[] args)
Definition: Expr.java:127
boolean isAnd()
Definition: Expr.java:353
boolean isRealIsInt()
Definition: Expr.java:585
boolean isProofUnitResolution()
Definition: Expr.java:1646
boolean isBVShiftLeft()
Definition: Expr.java:1136
boolean isBVShiftRightLogical()
Definition: Expr.java:1146
boolean isFiniteDomain()
Definition: Expr.java:2051
boolean isRelationProject()
Definition: Expr.java:1954
boolean isSetIntersect()
Definition: Expr.java:683
boolean isSub()
Definition: Expr.java:494
boolean isTrue()
Definition: Expr.java:302
boolean isAsArray()
Definition: Expr.java:663
boolean isLabelLit()
Definition: Expr.java:1272
boolean isSetSubset()
Definition: Expr.java:713
boolean isRelationNegationFilter()
Definition: Expr.java:1989
boolean isGT()
Definition: Expr.java:474
boolean isDistinct()
Definition: Expr.java:333
boolean isBVSMod()
Definition: Expr.java:845
boolean isBVAND()
Definition: Expr.java:986
String toString()
Definition: Expr.java:208
boolean isRelationWiden()
Definition: Expr.java:1941
boolean isRelationSelect()
Definition: Expr.java:2025
String getString()
Definition: Expr.java:1292
boolean isBVConcat()
Definition: Expr.java:1056
boolean isIntNum()
Definition: Expr.java:260
boolean isProofDefAxiom()
Definition: Expr.java:1713
boolean isBVUDiv()
Definition: Expr.java:815
boolean isBVReduceAND()
Definition: Expr.java:1116
boolean isBVULE()
Definition: Expr.java:905
boolean isDefaultArray()
Definition: Expr.java:640
boolean isBVUGT()
Definition: Expr.java:966
boolean isBVURem()
Definition: Expr.java:835
boolean isBVUMinus()
Definition: Expr.java:765
boolean isBVReduceOR()
Definition: Expr.java:1106
boolean isProofModusPonens()
Definition: Expr.java:1374
boolean isBVNOR()
Definition: Expr.java:1036
boolean isBVNOT()
Definition: Expr.java:1006
boolean isRelationStore()
Definition: Expr.java:1887
boolean isBool()
Definition: Expr.java:290
boolean isProofRewriteStar()
Definition: Expr.java:1536
boolean isBVMul()
Definition: Expr.java:795
boolean isProofDistributivity()
Definition: Expr.java:1478
boolean isModulus()
Definition: Expr.java:554
boolean isRelationRename()
Definition: Expr.java:2001
boolean isOr()
Definition: Expr.java:363
boolean isNumeral()
Definition: Expr.java:218
boolean isBVBitOne()
Definition: Expr.java:745
boolean isProofNNFPos()
Definition: Expr.java:1788
boolean isProofIFFOEQ()
Definition: Expr.java:1760
boolean isBVULT()
Definition: Expr.java:946
boolean isBVSignExtension()
Definition: Expr.java:1066
boolean isBVAdd()
Definition: Expr.java:775
boolean isRemainder()
Definition: Expr.java:544
boolean isEq()
Definition: Expr.java:322
boolean isProofCommutativity()
Definition: Expr.java:1687
boolean isConst()
Definition: Expr.java:250
Expr< R > substitute(Expr<?> from, Expr<?> to)
Definition: Expr.java:168
boolean isBVNumeral()
Definition: Expr.java:735
boolean isRelationComplement()
Definition: Expr.java:2011
boolean isProofRewrite()
Definition: Expr.java:1520
boolean isAdd()
Definition: Expr.java:484
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
def simplify(a, *arguments, **keywords)
Utils.
Definition: z3py.py:8645
def String(name, ctx=None)
Definition: z3py.py:10693
def substitute(t, *m)
Definition: z3py.py:8680
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150
@ Z3_BOOL_SORT
Definition: z3_api.h:152
@ Z3_ROUNDING_MODE_SORT
Definition: z3_api.h:161
@ Z3_BV_SORT
Definition: z3_api.h:155
@ Z3_DATATYPE_SORT
Definition: z3_api.h:157
@ Z3_INT_SORT
Definition: z3_api.h:153
@ Z3_FINITE_DOMAIN_SORT
Definition: z3_api.h:159
@ Z3_RE_SORT
Definition: z3_api.h:163
@ Z3_FLOATING_POINT_SORT
Definition: z3_api.h:160
@ Z3_ARRAY_SORT
Definition: z3_api.h:156
@ Z3_REAL_SORT
Definition: z3_api.h:154
@ Z3_SEQ_SORT
Definition: z3_api.h:162
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102