Z3
Expr.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.enumerations.Z3_ast_kind;
21import com.microsoft.z3.enumerations.Z3_decl_kind;
22import com.microsoft.z3.enumerations.Z3_lbool;
23import com.microsoft.z3.enumerations.Z3_sort_kind;
24
25/* using System; */
26
30public class Expr extends AST
31{
37 public Expr simplify()
38 {
39 return simplify(null);
40 }
41
52 {
53
54 if (p == null) {
55 return Expr.create(getContext(),
56 Native.simplify(getContext().nCtx(), getNativeObject()));
57 }
58 else {
59 return Expr.create(
60 getContext(),
61 Native.simplifyEx(getContext().nCtx(), getNativeObject(),
62 p.getNativeObject()));
63 }
64 }
65
73 {
74 return new FuncDecl(getContext(), Native.getAppDecl(getContext().nCtx(),
75 getNativeObject()));
76 }
77
85 {
86 return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
87 getNativeObject()));
88 }
89
95 public int getNumArgs()
96 {
97 return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
98 }
99
105 public Expr[] getArgs()
106 {
107 int n = getNumArgs();
108 Expr[] res = new Expr[n];
109 for (int i = 0; i < n; i++) {
110 res[i] = Expr.create(getContext(),
111 Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
112 }
113 return res;
114 }
115
123 public Expr update(Expr[] args)
124 {
125 getContext().checkContextMatch(args);
126 if (isApp() && args.length != getNumArgs()) {
127 throw new Z3Exception("Number of arguments does not match");
128 }
129 return Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
130 args.length, Expr.arrayToNative(args)));
131 }
132
145 public Expr substitute(Expr[] from, Expr[] to)
146 {
147 getContext().checkContextMatch(from);
148 getContext().checkContextMatch(to);
149 if (from.length != to.length) {
150 throw new Z3Exception("Argument sizes do not match");
151 }
152 return Expr.create(getContext(), Native.substitute(getContext().nCtx(),
153 getNativeObject(), from.length, Expr.arrayToNative(from),
154 Expr.arrayToNative(to)));
155 }
156
164 public Expr substitute(Expr from, Expr to)
165 {
166 return substitute(new Expr[] { from }, new Expr[] { to });
167 }
168
180 {
181
182 getContext().checkContextMatch(to);
183 return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
184 getNativeObject(), to.length, Expr.arrayToNative(to)));
185 }
186
196 {
197 return (Expr) super.translate(ctx);
198 }
199
203 @Override
205 {
206 return super.toString();
207 }
208
214 public boolean isNumeral()
215 {
216 return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
217 }
218
225 public boolean isWellSorted()
226 {
227 return Native.isWellSorted(getContext().nCtx(), getNativeObject());
228 }
229
235 public Sort getSort()
236 {
237 return Sort.create(getContext(),
238 Native.getSort(getContext().nCtx(), getNativeObject()));
239 }
240
246 public boolean isConst()
247 {
248 return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
249 }
250
256 public boolean isIntNum()
257 {
258 return isNumeral() && isInt();
259 }
260
266 public boolean isRatNum()
267 {
268 return isNumeral() && isReal();
269 }
270
276 public boolean isAlgebraicNumber()
277 {
278 return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
279 }
280
286 public boolean isBool()
287 {
288 return (isExpr() && Native.isEqSort(getContext().nCtx(),
289 Native.mkBoolSort(getContext().nCtx()),
290 Native.getSort(getContext().nCtx(), getNativeObject())));
291 }
292
298 public boolean isTrue()
299 {
301 }
302
308 public boolean isFalse()
309 {
311 }
312
318 public boolean isEq()
319 {
321 }
322
329 public boolean isDistinct()
330 {
332 }
333
339 public boolean isITE()
340 {
342 }
343
349 public boolean isAnd()
350 {
352 }
353
359 public boolean isOr()
360 {
362 }
363
370 public boolean isIff()
371 {
373 }
374
380 public boolean isXor()
381 {
383 }
384
390 public boolean isNot()
391 {
393 }
394
400 public boolean isImplies()
401 {
403 }
404
410 public boolean isInt()
411 {
412 return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT.toInt();
413 }
414
420 public boolean isReal()
421 {
422 return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT.toInt();
423 }
424
430 public boolean isArithmeticNumeral()
431 {
433 }
434
440 public boolean isLE()
441 {
443 }
444
450 public boolean isGE()
451 {
453 }
454
460 public boolean isLT()
461 {
463 }
464
470 public boolean isGT()
471 {
473 }
474
480 public boolean isAdd()
481 {
483 }
484
490 public boolean isSub()
491 {
493 }
494
500 public boolean isUMinus()
501 {
503 }
504
510 public boolean isMul()
511 {
513 }
514
520 public boolean isDiv()
521 {
523 }
524
530 public boolean isIDiv()
531 {
533 }
534
540 public boolean isRemainder()
541 {
543 }
544
550 public boolean isModulus()
551 {
553 }
554
560 public boolean isIntToReal()
561 {
563 }
564
570 public boolean isRealToInt()
571 {
573 }
574
581 public boolean isRealIsInt()
582 {
584 }
585
591 public boolean isArray()
592 {
593 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
594 .fromInt(Native.getSortKind(getContext().nCtx(),
595 Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
596 }
597
604 public boolean isStore()
605 {
607 }
608
614 public boolean isSelect()
615 {
617 }
618
625 public boolean isConstantArray()
626 {
628 }
629
636 public boolean isDefaultArray()
637 {
639 }
640
648 public boolean isArrayMap()
649 {
651 }
652
659 public boolean isAsArray()
660 {
662 }
663
669 public boolean isSetUnion()
670 {
672 }
673
679 public boolean isSetIntersect()
680 {
682 }
683
689 public boolean isSetDifference()
690 {
692 }
693
699 public boolean isSetComplement()
700 {
702 }
703
709 public boolean isSetSubset()
710 {
712 }
713
719 public boolean isBV()
720 {
721 return Native.getSortKind(getContext().nCtx(),
722 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
723 .toInt();
724 }
725
731 public boolean isBVNumeral()
732 {
734 }
735
741 public boolean isBVBitOne()
742 {
744 }
745
751 public boolean isBVBitZero()
752 {
754 }
755
761 public boolean isBVUMinus()
762 {
764 }
765
771 public boolean isBVAdd()
772 {
774 }
775
781 public boolean isBVSub()
782 {
784 }
785
791 public boolean isBVMul()
792 {
794 }
795
801 public boolean isBVSDiv()
802 {
804 }
805
811 public boolean isBVUDiv()
812 {
814 }
815
821 public boolean isBVSRem()
822 {
824 }
825
831 public boolean isBVURem()
832 {
834 }
835
841 public boolean isBVSMod()
842 {
844 }
845
851 boolean isBVSDiv0()
852 {
854 }
855
861 boolean isBVUDiv0()
862 {
864 }
865
871 boolean isBVSRem0()
872 {
874 }
875
881 boolean isBVURem0()
882 {
884 }
885
891 boolean isBVSMod0()
892 {
894 }
895
901 public boolean isBVULE()
902 {
904 }
905
911 public boolean isBVSLE()
912 {
914 }
915
922 public boolean isBVUGE()
923 {
925 }
926
932 public boolean isBVSGE()
933 {
935 }
936
942 public boolean isBVULT()
943 {
945 }
946
952 public boolean isBVSLT()
953 {
955 }
956
962 public boolean isBVUGT()
963 {
965 }
966
972 public boolean isBVSGT()
973 {
975 }
976
982 public boolean isBVAND()
983 {
985 }
986
992 public boolean isBVOR()
993 {
995 }
996
1002 public boolean isBVNOT()
1003 {
1005 }
1006
1012 public boolean isBVXOR()
1013 {
1015 }
1016
1022 public boolean isBVNAND()
1023 {
1025 }
1026
1032 public boolean isBVNOR()
1033 {
1035 }
1036
1042 public boolean isBVXNOR()
1043 {
1045 }
1046
1052 public boolean isBVConcat()
1053 {
1055 }
1056
1062 public boolean isBVSignExtension()
1063 {
1065 }
1066
1072 public boolean isBVZeroExtension()
1073 {
1075 }
1076
1082 public boolean isBVExtract()
1083 {
1085 }
1086
1092 public boolean isBVRepeat()
1093 {
1095 }
1096
1102 public boolean isBVReduceOR()
1103 {
1105 }
1106
1112 public boolean isBVReduceAND()
1113 {
1115 }
1116
1122 public boolean isBVComp()
1123 {
1125 }
1126
1132 public boolean isBVShiftLeft()
1133 {
1135 }
1136
1142 public boolean isBVShiftRightLogical()
1143 {
1145 }
1146
1153 {
1155 }
1156
1162 public boolean isBVRotateLeft()
1163 {
1165 }
1166
1172 public boolean isBVRotateRight()
1173 {
1175 }
1176
1184 public boolean isBVRotateLeftExtended()
1185 {
1187 }
1188
1197 {
1199 }
1200
1208 public boolean isIntToBV()
1209 {
1211 }
1212
1220 public boolean isBVToInt()
1221 {
1223 }
1224
1231 public boolean isBVCarry()
1232 {
1234 }
1235
1242 public boolean isBVXOR3()
1243 {
1245 }
1246
1255 public boolean isLabel()
1256 {
1258 }
1259
1268 public boolean isLabelLit()
1269 {
1271 }
1272
1277 public boolean isString()
1278 {
1279 return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
1280 }
1281
1289 {
1290 return Native.getString(getContext().nCtx(), getNativeObject());
1291 }
1292
1313 public boolean isConcat()
1314 {
1316 }
1317
1325 public boolean isOEQ()
1326 {
1328 }
1329
1335 public boolean isProofTrue()
1336 {
1338 }
1339
1345 public boolean isProofAsserted()
1346 {
1348 }
1349
1356 public boolean isProofGoal()
1357 {
1359 }
1360
1370 public boolean isProofModusPonens()
1371 {
1373 }
1374
1385 public boolean isProofReflexivity()
1386 {
1388 }
1389
1397 public boolean isProofSymmetry()
1398 {
1400 }
1401
1409 public boolean isProofTransitivity()
1410 {
1412 }
1413
1430 {
1432 }
1433
1444 public boolean isProofMonotonicity()
1445 {
1447 }
1448
1455 public boolean isProofQuantIntro()
1456 {
1458 }
1459
1474 public boolean isProofDistributivity()
1475 {
1477 }
1478
1485 public boolean isProofAndElimination()
1486 {
1488 }
1489
1496 public boolean isProofOrElimination()
1497 {
1499 }
1500
1516 public boolean isProofRewrite()
1517 {
1519 }
1520
1532 public boolean isProofRewriteStar()
1533 {
1535 }
1536
1544 public boolean isProofPullQuant()
1545 {
1547 }
1548
1549
1559 public boolean isProofPushQuant()
1560 {
1562 }
1563
1575 public boolean isProofElimUnusedVars()
1576 {
1578 }
1579
1591 public boolean isProofDER()
1592 {
1594 }
1595
1603 public boolean isProofQuantInst()
1604 {
1606 }
1607
1615 public boolean isProofHypothesis()
1616 {
1618 }
1619
1631 public boolean isProofLemma()
1632 {
1634 }
1635
1642 public boolean isProofUnitResolution()
1643 {
1645 }
1646
1654 public boolean isProofIFFTrue()
1655 {
1657 }
1658
1666 public boolean isProofIFFFalse()
1667 {
1669 }
1670
1683 public boolean isProofCommutativity()
1684 {
1686 }
1687
1709 public boolean isProofDefAxiom()
1710 {
1712 }
1713
1732 public boolean isProofDefIntro()
1733 {
1735 }
1736
1744 public boolean isProofApplyDef()
1745 {
1747 }
1748
1756 public boolean isProofIFFOEQ()
1757 {
1759 }
1760
1784 public boolean isProofNNFPos()
1785 {
1787 }
1788
1803 public boolean isProofNNFNeg()
1804 {
1806 }
1807
1808
1821 public boolean isProofSkolemize()
1822 {
1824 }
1825
1834 public boolean isProofModusPonensOEQ()
1835 {
1837 }
1838
1856 public boolean isProofTheoryLemma()
1857 {
1859 }
1860
1866 public boolean isRelation()
1867 {
1868 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1869 .getSortKind(getContext().nCtx(),
1870 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1871 .toInt());
1872 }
1873
1883 public boolean isRelationStore()
1884 {
1886 }
1887
1893 public boolean isEmptyRelation()
1894 {
1896 }
1897
1903 public boolean isIsEmptyRelation()
1904 {
1906 }
1907
1913 public boolean isRelationalJoin()
1914 {
1916 }
1917
1925 public boolean isRelationUnion()
1926 {
1928 }
1929
1937 public boolean isRelationWiden()
1938 {
1940 }
1941
1950 public boolean isRelationProject()
1951 {
1953 }
1954
1965 public boolean isRelationFilter()
1966 {
1968 }
1969
1986 {
1988 }
1989
1997 public boolean isRelationRename()
1998 {
2000 }
2001
2007 public boolean isRelationComplement()
2008 {
2010 }
2011
2021 public boolean isRelationSelect()
2022 {
2024 }
2025
2037 public boolean isRelationClone()
2038 {
2040 }
2041
2047 public boolean isFiniteDomain()
2048 {
2049 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
2050 .getSortKind(getContext().nCtx(),
2051 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
2052 .toInt());
2053 }
2054
2060 public boolean isFiniteDomainLT()
2061 {
2063 }
2064
2083 public int getIndex()
2084 {
2085 if (!isVar()) {
2086 throw new Z3Exception("Term is not a bound variable.");
2087 }
2088
2089 return Native.getIndexValue(getContext().nCtx(), getNativeObject());
2090 }
2091
2096 protected Expr(Context ctx, long obj) {
2097 super(ctx, obj);
2098 }
2099
2100 @Override
2101 void checkNativeObject(long obj) {
2102 if (!Native.isApp(getContext().nCtx(), obj) &&
2103 Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
2104 Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) {
2105 throw new Z3Exception("Underlying object is not a term");
2106 }
2107 super.checkNativeObject(obj);
2108 }
2109
2110 static Expr create(Context ctx, FuncDecl f, Expr ... arguments)
2111
2112 {
2113 long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
2114 AST.arrayLength(arguments), AST.arrayToNative(arguments));
2115 return create(ctx, obj);
2116 }
2117
2118 static Expr create(Context ctx, long obj)
2119 {
2120 Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
2121 if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
2122 return new Quantifier(ctx, obj);
2123 long s = Native.getSort(ctx.nCtx(), obj);
2125 .fromInt(Native.getSortKind(ctx.nCtx(), s));
2126
2127 if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast?
2128 return new AlgebraicNum(ctx, obj);
2129
2130 if (Native.isNumeralAst(ctx.nCtx(), obj))
2131 {
2132 switch (sk)
2133 {
2134 case Z3_INT_SORT:
2135 return new IntNum(ctx, obj);
2136 case Z3_REAL_SORT:
2137 return new RatNum(ctx, obj);
2138 case Z3_BV_SORT:
2139 return new BitVecNum(ctx, obj);
2141 return new FPNum(ctx, obj);
2143 return new FPRMNum(ctx, obj);
2145 return new FiniteDomainNum(ctx, obj);
2146 default: ;
2147 }
2148 }
2149
2150 switch (sk)
2151 {
2152 case Z3_BOOL_SORT:
2153 return new BoolExpr(ctx, obj);
2154 case Z3_INT_SORT:
2155 return new IntExpr(ctx, obj);
2156 case Z3_REAL_SORT:
2157 return new RealExpr(ctx, obj);
2158 case Z3_BV_SORT:
2159 return new BitVecExpr(ctx, obj);
2160 case Z3_ARRAY_SORT:
2161 return new ArrayExpr(ctx, obj);
2162 case Z3_DATATYPE_SORT:
2163 return new DatatypeExpr(ctx, obj);
2165 return new FPExpr(ctx, obj);
2167 return new FPRMExpr(ctx, obj);
2169 return new FiniteDomainExpr(ctx, obj);
2170 case Z3_SEQ_SORT:
2171 return new SeqExpr(ctx, obj);
2172 case Z3_RE_SORT:
2173 return new ReExpr(ctx, obj);
2174 default: ;
2175 }
2176
2177 return new Expr(ctx, obj);
2178 }
2179}
boolean isApp()
Definition: AST.java:131
boolean isExpr()
Definition: AST.java:112
boolean isVar()
Definition: AST.java:141
boolean isBVOR()
Definition: Expr.java:992
boolean isProofLemma()
Definition: Expr.java:1631
boolean isSetUnion()
Definition: Expr.java:669
Expr substituteVars(Expr[] to)
Definition: Expr.java:179
boolean isRelation()
Definition: Expr.java:1866
boolean isSelect()
Definition: Expr.java:614
boolean isBVRepeat()
Definition: Expr.java:1092
boolean isLT()
Definition: Expr.java:460
boolean isConstantArray()
Definition: Expr.java:625
Expr(Context ctx, long obj)
Definition: Expr.java:2096
boolean isProofHypothesis()
Definition: Expr.java:1615
boolean isProofDER()
Definition: Expr.java:1591
boolean isBVSRem()
Definition: Expr.java:821
boolean isImplies()
Definition: Expr.java:400
boolean isArrayMap()
Definition: Expr.java:648
boolean isDiv()
Definition: Expr.java:520
boolean isProofTransitivityStar()
Definition: Expr.java:1429
boolean isMul()
Definition: Expr.java:510
boolean isProofAsserted()
Definition: Expr.java:1345
boolean isNot()
Definition: Expr.java:390
FuncDecl getFuncDecl()
Definition: Expr.java:72
boolean isBVSLT()
Definition: Expr.java:952
boolean isBVRotateRightExtended()
Definition: Expr.java:1196
boolean isInt()
Definition: Expr.java:410
Expr[] getArgs()
Definition: Expr.java:105
boolean isRelationFilter()
Definition: Expr.java:1965
boolean isEmptyRelation()
Definition: Expr.java:1893
Z3_lbool getBoolValue()
Definition: Expr.java:84
boolean isBVXOR()
Definition: Expr.java:1012
Expr substitute(Expr from, Expr to)
Definition: Expr.java:164
boolean isProofIFFTrue()
Definition: Expr.java:1654
boolean isIntToBV()
Definition: Expr.java:1208
boolean isUMinus()
Definition: Expr.java:500
boolean isRelationalJoin()
Definition: Expr.java:1913
boolean isBVUGE()
Definition: Expr.java:922
boolean isFalse()
Definition: Expr.java:308
boolean isProofApplyDef()
Definition: Expr.java:1744
boolean isBVXOR3()
Definition: Expr.java:1242
boolean isProofNNFNeg()
Definition: Expr.java:1803
boolean isBVToInt()
Definition: Expr.java:1220
boolean isBVSLE()
Definition: Expr.java:911
boolean isProofTrue()
Definition: Expr.java:1335
boolean isBVNAND()
Definition: Expr.java:1022
boolean isProofQuantIntro()
Definition: Expr.java:1455
boolean isProofReflexivity()
Definition: Expr.java:1385
boolean isIff()
Definition: Expr.java:370
boolean isProofModusPonensOEQ()
Definition: Expr.java:1834
boolean isProofTransitivity()
Definition: Expr.java:1409
boolean isWellSorted()
Definition: Expr.java:225
boolean isBVComp()
Definition: Expr.java:1122
boolean isProofPullQuant()
Definition: Expr.java:1544
boolean isProofOrElimination()
Definition: Expr.java:1496
boolean isBVSGT()
Definition: Expr.java:972
boolean isLE()
Definition: Expr.java:440
boolean isProofIFFFalse()
Definition: Expr.java:1666
boolean isProofQuantInst()
Definition: Expr.java:1603
boolean isBVExtract()
Definition: Expr.java:1082
boolean isProofPushQuant()
Definition: Expr.java:1559
boolean isRelationUnion()
Definition: Expr.java:1925
boolean isProofTheoryLemma()
Definition: Expr.java:1856
boolean isRealToInt()
Definition: Expr.java:570
boolean isBVRotateLeftExtended()
Definition: Expr.java:1184
boolean isProofSkolemize()
Definition: Expr.java:1821
boolean isRelationClone()
Definition: Expr.java:2037
boolean isBV()
Definition: Expr.java:719
boolean isBVBitZero()
Definition: Expr.java:751
boolean isBVSub()
Definition: Expr.java:781
boolean isProofElimUnusedVars()
Definition: Expr.java:1575
boolean isProofSymmetry()
Definition: Expr.java:1397
boolean isProofMonotonicity()
Definition: Expr.java:1444
Expr translate(Context ctx)
Definition: Expr.java:195
boolean isXor()
Definition: Expr.java:380
boolean isIDiv()
Definition: Expr.java:530
boolean isBVXNOR()
Definition: Expr.java:1042
boolean isBVZeroExtension()
Definition: Expr.java:1072
boolean isAlgebraicNumber()
Definition: Expr.java:276
boolean isSetDifference()
Definition: Expr.java:689
boolean isProofAndElimination()
Definition: Expr.java:1485
boolean isProofDefIntro()
Definition: Expr.java:1732
boolean isGE()
Definition: Expr.java:450
boolean isBVRotateRight()
Definition: Expr.java:1172
boolean isArray()
Definition: Expr.java:591
boolean isSetComplement()
Definition: Expr.java:699
boolean isProofGoal()
Definition: Expr.java:1356
boolean isConcat()
Definition: Expr.java:1313
boolean isStore()
Definition: Expr.java:604
Expr update(Expr[] args)
Definition: Expr.java:123
boolean isIntToReal()
Definition: Expr.java:560
boolean isString()
Definition: Expr.java:1277
boolean isArithmeticNumeral()
Definition: Expr.java:430
boolean isBVShiftRightArithmetic()
Definition: Expr.java:1152
boolean isBVCarry()
Definition: Expr.java:1231
boolean isRatNum()
Definition: Expr.java:266
boolean isFiniteDomainLT()
Definition: Expr.java:2060
boolean isIsEmptyRelation()
Definition: Expr.java:1903
boolean isLabel()
Definition: Expr.java:1255
boolean isReal()
Definition: Expr.java:420
boolean isBVSGE()
Definition: Expr.java:932
boolean isBVRotateLeft()
Definition: Expr.java:1162
boolean isITE()
Definition: Expr.java:339
boolean isBVSDiv()
Definition: Expr.java:801
boolean isAnd()
Definition: Expr.java:349
boolean isRealIsInt()
Definition: Expr.java:581
boolean isProofUnitResolution()
Definition: Expr.java:1642
boolean isBVShiftLeft()
Definition: Expr.java:1132
boolean isBVShiftRightLogical()
Definition: Expr.java:1142
boolean isFiniteDomain()
Definition: Expr.java:2047
boolean isRelationProject()
Definition: Expr.java:1950
boolean isSetIntersect()
Definition: Expr.java:679
boolean isSub()
Definition: Expr.java:490
boolean isTrue()
Definition: Expr.java:298
boolean isAsArray()
Definition: Expr.java:659
boolean isLabelLit()
Definition: Expr.java:1268
boolean isSetSubset()
Definition: Expr.java:709
boolean isRelationNegationFilter()
Definition: Expr.java:1985
boolean isGT()
Definition: Expr.java:470
boolean isDistinct()
Definition: Expr.java:329
boolean isBVSMod()
Definition: Expr.java:841
boolean isBVAND()
Definition: Expr.java:982
String toString()
Definition: Expr.java:204
boolean isRelationWiden()
Definition: Expr.java:1937
boolean isRelationSelect()
Definition: Expr.java:2021
String getString()
Definition: Expr.java:1288
boolean isBVConcat()
Definition: Expr.java:1052
Expr simplify(Params p)
Definition: Expr.java:51
boolean isIntNum()
Definition: Expr.java:256
boolean isProofDefAxiom()
Definition: Expr.java:1709
boolean isBVUDiv()
Definition: Expr.java:811
boolean isBVReduceAND()
Definition: Expr.java:1112
boolean isBVULE()
Definition: Expr.java:901
boolean isDefaultArray()
Definition: Expr.java:636
boolean isBVUGT()
Definition: Expr.java:962
boolean isBVURem()
Definition: Expr.java:831
boolean isBVUMinus()
Definition: Expr.java:761
boolean isBVReduceOR()
Definition: Expr.java:1102
boolean isProofModusPonens()
Definition: Expr.java:1370
boolean isBVNOR()
Definition: Expr.java:1032
boolean isBVNOT()
Definition: Expr.java:1002
boolean isRelationStore()
Definition: Expr.java:1883
boolean isBool()
Definition: Expr.java:286
boolean isProofRewriteStar()
Definition: Expr.java:1532
boolean isBVMul()
Definition: Expr.java:791
boolean isProofDistributivity()
Definition: Expr.java:1474
boolean isModulus()
Definition: Expr.java:550
boolean isRelationRename()
Definition: Expr.java:1997
boolean isOr()
Definition: Expr.java:359
boolean isNumeral()
Definition: Expr.java:214
boolean isBVBitOne()
Definition: Expr.java:741
boolean isProofNNFPos()
Definition: Expr.java:1784
boolean isProofIFFOEQ()
Definition: Expr.java:1756
boolean isBVULT()
Definition: Expr.java:942
boolean isBVSignExtension()
Definition: Expr.java:1062
boolean isBVAdd()
Definition: Expr.java:771
boolean isRemainder()
Definition: Expr.java:540
boolean isEq()
Definition: Expr.java:318
boolean isProofCommutativity()
Definition: Expr.java:1683
boolean isConst()
Definition: Expr.java:246
Expr substitute(Expr[] from, Expr[] to)
Definition: Expr.java:145
boolean isBVNumeral()
Definition: Expr.java:731
boolean isRelationComplement()
Definition: Expr.java:2007
boolean isProofRewrite()
Definition: Expr.java:1516
boolean isAdd()
Definition: Expr.java:480
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:119
static long getAppDecl(long a0, long a1)
Definition: Native.java:3044
static boolean isNumeralAst(long a0, long a1)
Definition: Native.java:3143
static long substitute(long a0, long a1, int a2, long[] a3, long[] a4)
Definition: Native.java:3485
static int getAppNumArgs(long a0, long a1)
Definition: Native.java:3053
static int getSortKind(long a0, long a1)
Definition: Native.java:2693
static long updateTerm(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3476
static long simplify(long a0, long a1)
Definition: Native.java:3440
static boolean isAlgebraicNumber(long a0, long a1)
Definition: Native.java:3152
static int getAstKind(long a0, long a1)
Definition: Native.java:3125
static boolean isString(long a0, long a1)
Definition: Native.java:2180
static boolean isApp(long a0, long a1)
Definition: Native.java:3134
static boolean isWellSorted(long a0, long a1)
Definition: Native.java:3107
static String getString(long a0, long a1)
Definition: Native.java:2189
static long mkBoolSort(long a0)
Definition: Native.java:952
static long simplifyEx(long a0, long a1, long a2)
Definition: Native.java:3449
static long getAppArg(long a0, long a1, int a2)
Definition: Native.java:3062
static long substituteVars(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3494
static long getSort(long a0, long a1)
Definition: Native.java:3098
static int getBoolValue(long a0, long a1)
Definition: Native.java:3116
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:2684
static int getIndexValue(long a0, long a1)
Definition: Native.java:3323
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
def String(name, ctx=None)
Definition: z3py.py:10085
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:178
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1007
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:148
@ Z3_BOOL_SORT
Definition: z3_api.h:150
@ Z3_ROUNDING_MODE_SORT
Definition: z3_api.h:159
@ Z3_BV_SORT
Definition: z3_api.h:153
@ Z3_DATATYPE_SORT
Definition: z3_api.h:155
@ Z3_INT_SORT
Definition: z3_api.h:151
@ Z3_FINITE_DOMAIN_SORT
Definition: z3_api.h:157
@ Z3_RE_SORT
Definition: z3_api.h:161
@ Z3_FLOATING_POINT_SORT
Definition: z3_api.h:158
@ Z3_ARRAY_SORT
Definition: z3_api.h:154
@ Z3_REAL_SORT
Definition: z3_api.h:152
@ Z3_SEQ_SORT
Definition: z3_api.h:160