Z3
Expr.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
24 
25 /* using System; */
26 
30 public class Expr extends AST
31 {
38  public Expr simplify()
39  {
40  return simplify(null);
41  }
42 
53  public Expr simplify(Params p)
54  {
55 
56  if (p == null)
57  return Expr.create(getContext(),
58  Native.simplify(getContext().nCtx(), getNativeObject()));
59  else
60  return Expr.create(
61  getContext(),
62  Native.simplifyEx(getContext().nCtx(), getNativeObject(),
63  p.getNativeObject()));
64  }
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  return res;
113  }
114 
122  public void update(Expr[] args)
123  {
124  getContext().checkContextMatch(args);
125  if (isApp() && args.length != getNumArgs())
126  throw new Z3Exception("Number of arguments does not match");
127  setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(),
128  (int) args.length, Expr.arrayToNative(args)));
129  }
130 
143  public Expr substitute(Expr[] from, Expr[] to)
144  {
145  getContext().checkContextMatch(from);
146  getContext().checkContextMatch(to);
147  if (from.length != to.length)
148  throw new Z3Exception("Argument sizes do not match");
149  return Expr.create(getContext(), Native.substitute(getContext().nCtx(),
150  getNativeObject(), (int) from.length, Expr.arrayToNative(from),
151  Expr.arrayToNative(to)));
152  }
153 
161  public Expr substitute(Expr from, Expr to)
162  {
163 
164  return substitute(new Expr[] { from }, new Expr[] { to });
165  }
166 
177  public Expr substituteVars(Expr[] to)
178  {
179 
180  getContext().checkContextMatch(to);
181  return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
182  getNativeObject(), (int) to.length, Expr.arrayToNative(to)));
183  }
184 
194  public Expr translate(Context ctx)
195  {
196 
197  if (getContext() == ctx)
198  return this;
199  else
200  return Expr.create(
201  ctx,
202  Native.translate(getContext().nCtx(), getNativeObject(),
203  ctx.nCtx()));
204  }
205 
209  public String toString()
210  {
211  return super.toString();
212  }
213 
219  public boolean isNumeral()
220  {
221  return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
222  }
223 
231  public boolean isWellSorted()
232  {
233  return Native.isWellSorted(getContext().nCtx(), getNativeObject());
234  }
235 
241  public Sort getSort()
242  {
243  return Sort.create(getContext(),
244  Native.getSort(getContext().nCtx(), getNativeObject()));
245  }
246 
252  public boolean isConst()
253  {
254  return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
255  }
256 
262  public boolean isIntNum()
263  {
264  return isNumeral() && isInt();
265  }
266 
272  public boolean isRatNum()
273  {
274  return isNumeral() && isReal();
275  }
276 
282  public boolean isAlgebraicNumber()
283  {
284  return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
285  }
286 
292  public boolean isBool()
293  {
294  return (isExpr() && Native.isEqSort(getContext().nCtx(),
295  Native.mkBoolSort(getContext().nCtx()),
296  Native.getSort(getContext().nCtx(), getNativeObject())));
297  }
298 
304  public boolean isTrue()
305  {
307  }
308 
314  public boolean isFalse()
315  {
317  }
318 
324  public boolean isEq()
325  {
327  }
328 
335  public boolean isDistinct()
336  {
338  }
339 
345  public boolean isITE()
346  {
348  }
349 
355  public boolean isAnd()
356  {
358  }
359 
365  public boolean isOr()
366  {
368  }
369 
376  public boolean isIff()
377  {
379  }
380 
386  public boolean isXor()
387  {
389  }
390 
396  public boolean isNot()
397  {
399  }
400 
406  public boolean isImplies()
407  {
409  }
410 
416  public boolean isInt()
417  {
418  return (Native.isNumeralAst(getContext().nCtx(), getNativeObject()) && Native
419  .getSortKind(getContext().nCtx(),
420  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT
421  .toInt());
422  }
423 
429  public boolean isReal()
430  {
431  return Native.getSortKind(getContext().nCtx(),
432  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT
433  .toInt();
434  }
435 
441  public boolean isArithmeticNumeral()
442  {
444  }
445 
451  public boolean isLE()
452  {
454  }
455 
461  public boolean isGE()
462  {
464  }
465 
471  public boolean isLT()
472  {
474  }
475 
481  public boolean isGT()
482  {
484  }
485 
491  public boolean isAdd()
492  {
494  }
495 
501  public boolean isSub()
502  {
504  }
505 
511  public boolean isUMinus()
512  {
514  }
515 
521  public boolean isMul()
522  {
524  }
525 
531  public boolean isDiv()
532  {
534  }
535 
541  public boolean isIDiv()
542  {
544  }
545 
551  public boolean isRemainder()
552  {
554  }
555 
561  public boolean isModulus()
562  {
564  }
565 
571  public boolean isIntToReal()
572  {
574  }
575 
581  public boolean isRealToInt()
582  {
584  }
585 
592  public boolean isRealIsInt()
593  {
595  }
596 
602  public boolean isArray()
603  {
604  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
605  .fromInt(Native.getSortKind(getContext().nCtx(),
606  Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
607  }
608 
615  public boolean isStore()
616  {
618  }
619 
625  public boolean isSelect()
626  {
628  }
629 
636  public boolean isConstantArray()
637  {
639  }
640 
647  public boolean isDefaultArray()
648  {
650  }
651 
659  public boolean isArrayMap()
660  {
662  }
663 
670  public boolean isAsArray()
671  {
673  }
674 
680  public boolean isSetUnion()
681  {
683  }
684 
690  public boolean isSetIntersect()
691  {
693  }
694 
700  public boolean isSetDifference()
701  {
703  }
704 
710  public boolean isSetComplement()
711  {
713  }
714 
720  public boolean isSetSubset()
721  {
723  }
724 
730  public boolean isBV()
731  {
732  return Native.getSortKind(getContext().nCtx(),
733  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
734  .toInt();
735  }
736 
742  public boolean isBVNumeral()
743  {
745  }
746 
752  public boolean isBVBitOne()
753  {
755  }
756 
762  public boolean isBVBitZero()
763  {
765  }
766 
772  public boolean isBVUMinus()
773  {
775  }
776 
782  public boolean isBVAdd()
783  {
785  }
786 
792  public boolean isBVSub()
793  {
795  }
796 
802  public boolean isBVMul()
803  {
805  }
806 
812  public boolean isBVSDiv()
813  {
815  }
816 
822  public boolean isBVUDiv()
823  {
825  }
826 
832  public boolean isBVSRem()
833  {
835  }
836 
842  public boolean isBVURem()
843  {
845  }
846 
852  public boolean isBVSMod()
853  {
855  }
856 
862  boolean isBVSDiv0()
863  {
865  }
866 
872  boolean isBVUDiv0()
873  {
875  }
876 
882  boolean isBVSRem0()
883  {
885  }
886 
892  boolean isBVURem0()
893  {
895  }
896 
902  boolean isBVSMod0()
903  {
905  }
906 
912  public boolean isBVULE()
913  {
915  }
916 
922  public boolean isBVSLE()
923  {
925  }
926 
933  public boolean isBVUGE()
934  {
936  }
937 
943  public boolean isBVSGE()
944  {
946  }
947 
953  public boolean isBVULT()
954  {
956  }
957 
963  public boolean isBVSLT()
964  {
966  }
967 
973  public boolean isBVUGT()
974  {
976  }
977 
983  public boolean isBVSGT()
984  {
986  }
987 
993  public boolean isBVAND()
994  {
996  }
997 
1003  public boolean isBVOR()
1004  {
1005  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
1006  }
1007 
1013  public boolean isBVNOT()
1014  {
1016  }
1017 
1023  public boolean isBVXOR()
1024  {
1026  }
1027 
1033  public boolean isBVNAND()
1034  {
1036  }
1037 
1043  public boolean isBVNOR()
1044  {
1046  }
1047 
1053  public boolean isBVXNOR()
1054  {
1056  }
1057 
1063  public boolean isBVConcat()
1064  {
1066  }
1067 
1073  public boolean isBVSignExtension()
1074  {
1076  }
1077 
1083  public boolean isBVZeroExtension()
1084  {
1086  }
1087 
1093  public boolean isBVExtract()
1094  {
1096  }
1097 
1103  public boolean isBVRepeat()
1104  {
1106  }
1107 
1113  public boolean isBVReduceOR()
1114  {
1116  }
1117 
1123  public boolean isBVReduceAND()
1124  {
1126  }
1127 
1133  public boolean isBVComp()
1134  {
1136  }
1137 
1143  public boolean isBVShiftLeft()
1144  {
1146  }
1147 
1153  public boolean isBVShiftRightLogical()
1154  {
1156  }
1157 
1163  public boolean isBVShiftRightArithmetic()
1164  {
1166  }
1167 
1173  public boolean isBVRotateLeft()
1174  {
1176  }
1177 
1183  public boolean isBVRotateRight()
1184  {
1186  }
1187 
1195  public boolean isBVRotateLeftExtended()
1196  {
1198  }
1199 
1207  public boolean isBVRotateRightExtended()
1208  {
1210  }
1211 
1219  public boolean isIntToBV()
1220  {
1222  }
1223 
1231  public boolean isBVToInt()
1232  {
1234  }
1235 
1242  public boolean isBVCarry()
1243  {
1245  }
1246 
1253  public boolean isBVXOR3()
1254  {
1256  }
1257 
1266  public boolean isLabel()
1267  {
1269  }
1270 
1279  public boolean isLabelLit()
1280  {
1282  }
1283 
1291  public boolean isOEQ()
1292  {
1293  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
1294  }
1295 
1301  public boolean isProofTrue()
1302  {
1304  }
1305 
1311  public boolean isProofAsserted()
1312  {
1314  }
1315 
1322  public boolean isProofGoal()
1323  {
1325  }
1326 
1336  public boolean isProofModusPonens()
1337  {
1339  }
1340 
1351  public boolean isProofReflexivity()
1352  {
1354  }
1355 
1363  public boolean isProofSymmetry()
1364  {
1366  }
1367 
1375  public boolean isProofTransitivity()
1376  {
1378  }
1379 
1396  public boolean isProofTransitivityStar()
1397  {
1399  }
1400 
1411  public boolean isProofMonotonicity()
1412  {
1414  }
1415 
1422  public boolean isProofQuantIntro()
1423  {
1425  }
1426 
1441  public boolean isProofDistributivity()
1442  {
1444  }
1445 
1452  public boolean isProofAndElimination()
1453  {
1455  }
1456 
1463  public boolean isProofOrElimination()
1464  {
1466  }
1467 
1483  public boolean isProofRewrite()
1484  {
1486  }
1487 
1502  public boolean isProofRewriteStar()
1503  {
1505  }
1506 
1514  public boolean isProofPullQuant()
1515  {
1517  }
1518 
1526  public boolean isProofPullQuantStar()
1527  {
1529  }
1530 
1540  public boolean isProofPushQuant()
1541  {
1543  }
1544 
1556  public boolean isProofElimUnusedVars()
1557  {
1559  }
1560 
1572  public boolean isProofDER()
1573  {
1575  }
1576 
1584  public boolean isProofQuantInst()
1585  {
1587  }
1588 
1596  public boolean isProofHypothesis()
1597  {
1599  }
1600 
1612  public boolean isProofLemma()
1613  {
1615  }
1616 
1623  public boolean isProofUnitResolution()
1624  {
1626  }
1627 
1635  public boolean isProofIFFTrue()
1636  {
1638  }
1639 
1647  public boolean isProofIFFFalse()
1648  {
1650  }
1651 
1664  public boolean isProofCommutativity()
1665  {
1667  }
1668 
1690  public boolean isProofDefAxiom()
1691  {
1693  }
1694 
1713  public boolean isProofDefIntro()
1714  {
1716  }
1717 
1725  public boolean isProofApplyDef()
1726  {
1728  }
1729 
1737  public boolean isProofIFFOEQ()
1738  {
1740  }
1741 
1765  public boolean isProofNNFPos()
1766  {
1768  }
1769 
1784  public boolean isProofNNFNeg()
1785  {
1787  }
1788 
1802  public boolean isProofNNFStar()
1803  {
1805  }
1806 
1817  public boolean isProofCNFStar()
1818  {
1820  }
1821 
1834  public boolean isProofSkolemize()
1835  {
1837  }
1838 
1847  public boolean isProofModusPonensOEQ()
1848  {
1850  }
1851 
1869  public boolean isProofTheoryLemma()
1870  {
1872  }
1873 
1879  public boolean isRelation()
1880  {
1881  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1882  .getSortKind(getContext().nCtx(),
1883  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1884  .toInt());
1885  }
1886 
1896  public boolean isRelationStore()
1897  {
1899  }
1900 
1906  public boolean isEmptyRelation()
1907  {
1909  }
1910 
1916  public boolean isIsEmptyRelation()
1917  {
1919  }
1920 
1926  public boolean isRelationalJoin()
1927  {
1929  }
1930 
1938  public boolean isRelationUnion()
1939  {
1941  }
1942 
1950  public boolean isRelationWiden()
1951  {
1953  }
1954 
1963  public boolean isRelationProject()
1964  {
1966  }
1967 
1978  public boolean isRelationFilter()
1979  {
1981  }
1982 
1998  public boolean isRelationNegationFilter()
1999  {
2001  }
2002 
2010  public boolean isRelationRename()
2011  {
2013  }
2014 
2020  public boolean isRelationComplement()
2021  {
2023  }
2024 
2034  public boolean isRelationSelect()
2035  {
2037  }
2038 
2050  public boolean isRelationClone()
2051  {
2053  }
2054 
2060  public boolean isFiniteDomain()
2061  {
2062  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
2063  .getSortKind(getContext().nCtx(),
2064  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
2065  .toInt());
2066  }
2067 
2073  public boolean isFiniteDomainLT()
2074  {
2076  }
2077 
2096  public int getIndex()
2097  {
2098  if (!isVar())
2099  throw new Z3Exception("Term is not a bound variable.");
2100 
2101  return Native.getIndexValue(getContext().nCtx(), getNativeObject());
2102  }
2103 
2107  protected Expr(Context ctx)
2108  {
2109  super(ctx);
2110  {
2111  }
2112  }
2113 
2118  protected Expr(Context ctx, long obj)
2119  {
2120  super(ctx, obj);
2121  {
2122  }
2123  }
2124 
2125  void checkNativeObject(long obj)
2126  {
2127  if (!Native.isApp(getContext().nCtx(), obj) &&
2128  Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
2129  Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt())
2130  throw new Z3Exception("Underlying object is not a term");
2131  super.checkNativeObject(obj);
2132  }
2133 
2134  static Expr create(Context ctx, FuncDecl f, Expr ... arguments)
2135 
2136  {
2137  long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
2138  AST.arrayLength(arguments), AST.arrayToNative(arguments));
2139  return create(ctx, obj);
2140  }
2141 
2142  static Expr create(Context ctx, long obj)
2143  {
2144  Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
2145  if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
2146  return new Quantifier(ctx, obj);
2147  long s = Native.getSort(ctx.nCtx(), obj);
2149  .fromInt(Native.getSortKind(ctx.nCtx(), s));
2150 
2151  if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast?
2152  return new AlgebraicNum(ctx, obj);
2153 
2154  if (Native.isNumeralAst(ctx.nCtx(), obj))
2155  {
2156  switch (sk)
2157  {
2158  case Z3_INT_SORT:
2159  return new IntNum(ctx, obj);
2160  case Z3_REAL_SORT:
2161  return new RatNum(ctx, obj);
2162  case Z3_BV_SORT:
2163  return new BitVecNum(ctx, obj);
2165  return new FPNum(ctx, obj);
2166  case Z3_ROUNDING_MODE_SORT:
2167  return new FPRMNum(ctx, obj);
2168  default: ;
2169  }
2170  }
2171 
2172  switch (sk)
2173  {
2174  case Z3_BOOL_SORT:
2175  return new BoolExpr(ctx, obj);
2176  case Z3_INT_SORT:
2177  return new IntExpr(ctx, obj);
2178  case Z3_REAL_SORT:
2179  return new RealExpr(ctx, obj);
2180  case Z3_BV_SORT:
2181  return new BitVecExpr(ctx, obj);
2182  case Z3_ARRAY_SORT:
2183  return new ArrayExpr(ctx, obj);
2184  case Z3_DATATYPE_SORT:
2185  return new DatatypeExpr(ctx, obj);
2187  return new FPExpr(ctx, obj);
2188  case Z3_ROUNDING_MODE_SORT:
2189  return new FPRMExpr(ctx, obj);
2190  default: ;
2191  }
2192 
2193  return new Expr(ctx, obj);
2194  }
2195 }
boolean isProofNNFStar()
Definition: Expr.java:1802
boolean isEmptyRelation()
Definition: Expr.java:1906
static int getBoolValue(long a0, long a1)
Definition: Native.java:2486
boolean isApp()
Definition: AST.java:157
boolean isBVSGT()
Definition: Expr.java:983
boolean isProofTransitivityStar()
Definition: Expr.java:1396
boolean isProofModusPonens()
Definition: Expr.java:1336
boolean isBVBitZero()
Definition: Expr.java:762
boolean isIDiv()
Definition: Expr.java:541
boolean isProofRewrite()
Definition: Expr.java:1483
boolean isLT()
Definition: Expr.java:471
boolean isBVShiftLeft()
Definition: Expr.java:1143
boolean isBVSLE()
Definition: Expr.java:922
boolean isLE()
Definition: Expr.java:451
boolean isBVXNOR()
Definition: Expr.java:1053
static long mkApp(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1037
boolean isDiv()
Definition: Expr.java:531
boolean isBVULT()
Definition: Expr.java:953
boolean isGE()
Definition: Expr.java:461
boolean isWellSorted()
Definition: Expr.java:231
boolean isProofIFFOEQ()
Definition: Expr.java:1737
boolean isSetComplement()
Definition: Expr.java:710
boolean isProofElimUnusedVars()
Definition: Expr.java:1556
boolean isProofMonotonicity()
Definition: Expr.java:1411
boolean isBVRotateLeft()
Definition: Expr.java:1173
boolean isProofCNFStar()
Definition: Expr.java:1817
boolean isBVUGE()
Definition: Expr.java:933
static final Z3_ast_kind fromInt(int v)
boolean isBVSDiv()
Definition: Expr.java:812
boolean isEq()
Definition: Expr.java:324
boolean isBVSub()
Definition: Expr.java:792
boolean isArrayMap()
Definition: Expr.java:659
static int getSortKind(long a0, long a1)
Definition: Native.java:2090
Expr(Context ctx)
Definition: Expr.java:2107
static final Z3_sort_kind fromInt(int v)
boolean isRealIsInt()
Definition: Expr.java:592
static int getAppNumArgs(long a0, long a1)
Definition: Native.java:2423
boolean isNot()
Definition: Expr.java:396
boolean isRelationSelect()
Definition: Expr.java:2034
boolean isRelationStore()
Definition: Expr.java:1896
boolean isProofNNFNeg()
Definition: Expr.java:1784
boolean isRemainder()
Definition: Expr.java:551
boolean isBVRotateLeftExtended()
Definition: Expr.java:1195
boolean isBVZeroExtension()
Definition: Expr.java:1083
boolean isUMinus()
Definition: Expr.java:511
static long substitute(long a0, long a1, int a2, long[] a3, long[] a4)
Definition: Native.java:2828
boolean isIff()
Definition: Expr.java:376
boolean isSetUnion()
Definition: Expr.java:680
boolean isBVSLT()
Definition: Expr.java:963
boolean isBVComp()
Definition: Expr.java:1133
boolean isBVConcat()
Definition: Expr.java:1063
boolean isProofSkolemize()
Definition: Expr.java:1834
boolean isConstantArray()
Definition: Expr.java:636
boolean isProofReflexivity()
Definition: Expr.java:1351
boolean isBVNumeral()
Definition: Expr.java:742
boolean isProofIFFFalse()
Definition: Expr.java:1647
boolean isProofDER()
Definition: Expr.java:1572
boolean isBVNAND()
Definition: Expr.java:1033
boolean isProofLemma()
Definition: Expr.java:1612
boolean isBVShiftRightArithmetic()
Definition: Expr.java:1163
boolean isProofPullQuantStar()
Definition: Expr.java:1526
static long updateTerm(long a0, long a1, int a2, long[] a3)
Definition: Native.java:2819
boolean isXor()
Definition: Expr.java:386
static boolean isWellSorted(long a0, long a1)
Definition: Native.java:2477
boolean isBVUMinus()
Definition: Expr.java:772
boolean isStore()
Definition: Expr.java:615
boolean isProofIFFTrue()
Definition: Expr.java:1635
boolean isMul()
Definition: Expr.java:521
boolean isBVRotateRight()
Definition: Expr.java:1183
boolean isRealToInt()
Definition: Expr.java:581
boolean isRelationProject()
Definition: Expr.java:1963
boolean isAdd()
Definition: Expr.java:491
void update(Expr[] args)
Definition: Expr.java:122
boolean isBVAND()
Definition: Expr.java:993
boolean isBVNOT()
Definition: Expr.java:1013
boolean isProofCommutativity()
Definition: Expr.java:1664
boolean isVar()
Definition: AST.java:167
boolean isDistinct()
Definition: Expr.java:335
boolean isDefaultArray()
Definition: Expr.java:647
static boolean isNumeralAst(long a0, long a1)
Definition: Native.java:2513
boolean isRelationNegationFilter()
Definition: Expr.java:1998
boolean isProofAndElimination()
Definition: Expr.java:1452
boolean isAnd()
Definition: Expr.java:355
boolean isExpr()
Definition: AST.java:138
static int getIndexValue(long a0, long a1)
Definition: Native.java:2684
boolean isBVBitOne()
Definition: Expr.java:752
Expr substitute(Expr from, Expr to)
Definition: Expr.java:161
boolean isBVReduceAND()
Definition: Expr.java:1123
boolean isSetDifference()
Definition: Expr.java:700
boolean isImplies()
Definition: Expr.java:406
boolean isAlgebraicNumber()
Definition: Expr.java:282
String toString()
Definition: Expr.java:209
boolean isBVURem()
Definition: Expr.java:842
boolean isBVRepeat()
Definition: Expr.java:1103
boolean isRelationRename()
Definition: Expr.java:2010
boolean isGT()
Definition: Expr.java:481
boolean isProofRewriteStar()
Definition: Expr.java:1502
boolean isProofPushQuant()
Definition: Expr.java:1540
boolean isRelationClone()
Definition: Expr.java:2050
boolean isProofPullQuant()
Definition: Expr.java:1514
boolean isRelationUnion()
Definition: Expr.java:1938
boolean isSetSubset()
Definition: Expr.java:720
Expr[] getArgs()
Definition: Expr.java:105
boolean isRelation()
Definition: Expr.java:1879
boolean isProofHypothesis()
Definition: Expr.java:1596
boolean isBVSRem()
Definition: Expr.java:832
boolean isLabel()
Definition: Expr.java:1266
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
boolean isAsArray()
Definition: Expr.java:670
boolean isBVExtract()
Definition: Expr.java:1093
boolean isReal()
Definition: Expr.java:429
boolean isRelationFilter()
Definition: Expr.java:1978
boolean isIntToBV()
Definition: Expr.java:1219
boolean isProofNNFPos()
Definition: Expr.java:1765
boolean isProofTransitivity()
Definition: Expr.java:1375
FuncDecl getFuncDecl()
Definition: Expr.java:72
static long simplifyEx(long a0, long a1, long a2)
Definition: Native.java:2792
boolean isBVToInt()
Definition: Expr.java:1231
boolean isProofOrElimination()
Definition: Expr.java:1463
boolean isProofTrue()
Definition: Expr.java:1301
boolean isProofUnitResolution()
Definition: Expr.java:1623
boolean isBVSignExtension()
Definition: Expr.java:1073
boolean isIntNum()
Definition: Expr.java:262
boolean isBVOR()
Definition: Expr.java:1003
boolean isBVAdd()
Definition: Expr.java:782
boolean isBVShiftRightLogical()
Definition: Expr.java:1153
Expr translate(Context ctx)
Definition: Expr.java:194
boolean isIntToReal()
Definition: Expr.java:571
boolean isBVMul()
Definition: Expr.java:802
static boolean isApp(long a0, long a1)
Definition: Native.java:2504
boolean isBVReduceOR()
Definition: Expr.java:1113
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:2081
boolean isSub()
Definition: Expr.java:501
boolean isBVCarry()
Definition: Expr.java:1242
static long getAppArg(long a0, long a1, int a2)
Definition: Native.java:2432
boolean isFiniteDomain()
Definition: Expr.java:2060
boolean isRelationWiden()
Definition: Expr.java:1950
boolean isProofDefIntro()
Definition: Expr.java:1713
boolean isProofSymmetry()
Definition: Expr.java:1363
boolean isFiniteDomainLT()
Definition: Expr.java:2073
boolean isProofQuantIntro()
Definition: Expr.java:1422
boolean isTrue()
Definition: Expr.java:304
boolean isOr()
Definition: Expr.java:365
boolean isRatNum()
Definition: Expr.java:272
boolean isBV()
Definition: Expr.java:730
boolean isBVULE()
Definition: Expr.java:912
static int getAstKind(long a0, long a1)
Definition: Native.java:2495
boolean isProofGoal()
Definition: Expr.java:1322
Expr substituteVars(Expr[] to)
Definition: Expr.java:177
boolean isProofModusPonensOEQ()
Definition: Expr.java:1847
boolean isProofDefAxiom()
Definition: Expr.java:1690
static long simplify(long a0, long a1)
Definition: Native.java:2783
boolean isBVUGT()
Definition: Expr.java:973
boolean isProofDistributivity()
Definition: Expr.java:1441
static long getAppDecl(long a0, long a1)
Definition: Native.java:2414
boolean isNumeral()
Definition: Expr.java:219
boolean isIsEmptyRelation()
Definition: Expr.java:1916
boolean isBVSMod()
Definition: Expr.java:852
boolean isArithmeticNumeral()
Definition: Expr.java:441
boolean isArray()
Definition: Expr.java:602
boolean isProofQuantInst()
Definition: Expr.java:1584
boolean isFalse()
Definition: Expr.java:314
boolean isRelationalJoin()
Definition: Expr.java:1926
boolean isRelationComplement()
Definition: Expr.java:2020
boolean isBVXOR3()
Definition: Expr.java:1253
boolean isConst()
Definition: Expr.java:252
Expr(Context ctx, long obj)
Definition: Expr.java:2118
boolean isInt()
Definition: Expr.java:416
static long mkBoolSort(long a0)
Definition: Native.java:888
static long getSort(long a0, long a1)
Definition: Native.java:2468
Expr substitute(Expr[] from, Expr[] to)
Definition: Expr.java:143
static long substituteVars(long a0, long a1, int a2, long[] a3)
Definition: Native.java:2837
boolean isLabelLit()
Definition: Expr.java:1279
boolean isProofApplyDef()
Definition: Expr.java:1725
boolean isBVXOR()
Definition: Expr.java:1023
boolean isITE()
Definition: Expr.java:345
boolean isBool()
Definition: Expr.java:292
boolean isProofAsserted()
Definition: Expr.java:1311
boolean isBVNOR()
Definition: Expr.java:1043
Z3_lbool getBoolValue()
Definition: Expr.java:84
boolean isBVSGE()
Definition: Expr.java:943
boolean isBVUDiv()
Definition: Expr.java:822
boolean isBVRotateRightExtended()
Definition: Expr.java:1207
boolean isSelect()
Definition: Expr.java:625
boolean isSetIntersect()
Definition: Expr.java:690
Expr simplify(Params p)
Definition: Expr.java:53
boolean isProofTheoryLemma()
Definition: Expr.java:1869
static long translate(long a0, long a1, long a2)
Definition: Native.java:2846
static boolean isAlgebraicNumber(long a0, long a1)
Definition: Native.java:2522
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:21
boolean isModulus()
Definition: Expr.java:561