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 {
37  public Expr simplify()
38  {
39  return simplify(null);
40  }
41 
51  public Expr simplify(Params p)
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 new Expr(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 
179  public Expr substituteVars(Expr[] to)
180  {
181 
182  getContext().checkContextMatch(to);
183  return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
184  getNativeObject(), to.length, Expr.arrayToNative(to)));
185  }
186 
195  public Expr translate(Context ctx)
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  }
206 
210  @Override
211  public String toString()
212  {
213  return super.toString();
214  }
215 
221  public boolean isNumeral()
222  {
223  return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
224  }
225 
232  public boolean isWellSorted()
233  {
234  return Native.isWellSorted(getContext().nCtx(), getNativeObject());
235  }
236 
242  public Sort getSort()
243  {
244  return Sort.create(getContext(),
245  Native.getSort(getContext().nCtx(), getNativeObject()));
246  }
247 
253  public boolean isConst()
254  {
255  return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
256  }
257 
263  public boolean isIntNum()
264  {
265  return isNumeral() && isInt();
266  }
267 
273  public boolean isRatNum()
274  {
275  return isNumeral() && isReal();
276  }
277 
283  public boolean isAlgebraicNumber()
284  {
285  return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
286  }
287 
293  public boolean isBool()
294  {
295  return (isExpr() && Native.isEqSort(getContext().nCtx(),
296  Native.mkBoolSort(getContext().nCtx()),
297  Native.getSort(getContext().nCtx(), getNativeObject())));
298  }
299 
305  public boolean isTrue()
306  {
308  }
309 
315  public boolean isFalse()
316  {
318  }
319 
325  public boolean isEq()
326  {
328  }
329 
336  public boolean isDistinct()
337  {
339  }
340 
346  public boolean isITE()
347  {
349  }
350 
356  public boolean isAnd()
357  {
359  }
360 
366  public boolean isOr()
367  {
369  }
370 
377  public boolean isIff()
378  {
380  }
381 
387  public boolean isXor()
388  {
390  }
391 
397  public boolean isNot()
398  {
400  }
401 
407  public boolean isImplies()
408  {
410  }
411 
417  public boolean isInt()
418  {
419  return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT.toInt();
420  }
421 
427  public boolean isReal()
428  {
429  return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT.toInt();
430  }
431 
437  public boolean isArithmeticNumeral()
438  {
440  }
441 
447  public boolean isLE()
448  {
450  }
451 
457  public boolean isGE()
458  {
460  }
461 
467  public boolean isLT()
468  {
470  }
471 
477  public boolean isGT()
478  {
480  }
481 
487  public boolean isAdd()
488  {
490  }
491 
497  public boolean isSub()
498  {
500  }
501 
507  public boolean isUMinus()
508  {
510  }
511 
517  public boolean isMul()
518  {
520  }
521 
527  public boolean isDiv()
528  {
530  }
531 
537  public boolean isIDiv()
538  {
540  }
541 
547  public boolean isRemainder()
548  {
550  }
551 
557  public boolean isModulus()
558  {
560  }
561 
567  public boolean isIntToReal()
568  {
570  }
571 
577  public boolean isRealToInt()
578  {
580  }
581 
588  public boolean isRealIsInt()
589  {
591  }
592 
598  public boolean isArray()
599  {
600  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
601  .fromInt(Native.getSortKind(getContext().nCtx(),
602  Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
603  }
604 
611  public boolean isStore()
612  {
614  }
615 
621  public boolean isSelect()
622  {
624  }
625 
632  public boolean isConstantArray()
633  {
635  }
636 
643  public boolean isDefaultArray()
644  {
646  }
647 
655  public boolean isArrayMap()
656  {
658  }
659 
666  public boolean isAsArray()
667  {
669  }
670 
676  public boolean isSetUnion()
677  {
679  }
680 
686  public boolean isSetIntersect()
687  {
689  }
690 
696  public boolean isSetDifference()
697  {
699  }
700 
706  public boolean isSetComplement()
707  {
709  }
710 
716  public boolean isSetSubset()
717  {
719  }
720 
726  public boolean isBV()
727  {
728  return Native.getSortKind(getContext().nCtx(),
729  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
730  .toInt();
731  }
732 
738  public boolean isBVNumeral()
739  {
741  }
742 
748  public boolean isBVBitOne()
749  {
751  }
752 
758  public boolean isBVBitZero()
759  {
761  }
762 
768  public boolean isBVUMinus()
769  {
771  }
772 
778  public boolean isBVAdd()
779  {
781  }
782 
788  public boolean isBVSub()
789  {
791  }
792 
798  public boolean isBVMul()
799  {
801  }
802 
808  public boolean isBVSDiv()
809  {
811  }
812 
818  public boolean isBVUDiv()
819  {
821  }
822 
828  public boolean isBVSRem()
829  {
831  }
832 
838  public boolean isBVURem()
839  {
841  }
842 
848  public boolean isBVSMod()
849  {
851  }
852 
858  boolean isBVSDiv0()
859  {
861  }
862 
868  boolean isBVUDiv0()
869  {
871  }
872 
878  boolean isBVSRem0()
879  {
881  }
882 
888  boolean isBVURem0()
889  {
891  }
892 
898  boolean isBVSMod0()
899  {
901  }
902 
908  public boolean isBVULE()
909  {
911  }
912 
918  public boolean isBVSLE()
919  {
921  }
922 
929  public boolean isBVUGE()
930  {
932  }
933 
939  public boolean isBVSGE()
940  {
942  }
943 
949  public boolean isBVULT()
950  {
952  }
953 
959  public boolean isBVSLT()
960  {
962  }
963 
969  public boolean isBVUGT()
970  {
972  }
973 
979  public boolean isBVSGT()
980  {
982  }
983 
989  public boolean isBVAND()
990  {
992  }
993 
999  public boolean isBVOR()
1000  {
1001  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
1002  }
1003 
1009  public boolean isBVNOT()
1010  {
1012  }
1013 
1019  public boolean isBVXOR()
1020  {
1022  }
1023 
1029  public boolean isBVNAND()
1030  {
1032  }
1033 
1039  public boolean isBVNOR()
1040  {
1042  }
1043 
1049  public boolean isBVXNOR()
1050  {
1052  }
1053 
1059  public boolean isBVConcat()
1060  {
1062  }
1063 
1069  public boolean isBVSignExtension()
1070  {
1072  }
1073 
1079  public boolean isBVZeroExtension()
1080  {
1082  }
1083 
1089  public boolean isBVExtract()
1090  {
1092  }
1093 
1099  public boolean isBVRepeat()
1100  {
1102  }
1103 
1109  public boolean isBVReduceOR()
1110  {
1112  }
1113 
1119  public boolean isBVReduceAND()
1120  {
1122  }
1123 
1129  public boolean isBVComp()
1130  {
1132  }
1133 
1139  public boolean isBVShiftLeft()
1140  {
1142  }
1143 
1149  public boolean isBVShiftRightLogical()
1150  {
1152  }
1153 
1159  public boolean isBVShiftRightArithmetic()
1160  {
1162  }
1163 
1169  public boolean isBVRotateLeft()
1170  {
1172  }
1173 
1179  public boolean isBVRotateRight()
1180  {
1182  }
1183 
1191  public boolean isBVRotateLeftExtended()
1192  {
1194  }
1195 
1203  public boolean isBVRotateRightExtended()
1204  {
1206  }
1207 
1215  public boolean isIntToBV()
1216  {
1218  }
1219 
1227  public boolean isBVToInt()
1228  {
1230  }
1231 
1238  public boolean isBVCarry()
1239  {
1241  }
1242 
1249  public boolean isBVXOR3()
1250  {
1252  }
1253 
1262  public boolean isLabel()
1263  {
1265  }
1266 
1275  public boolean isLabelLit()
1276  {
1278  }
1279 
1287  public boolean isOEQ()
1288  {
1289  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
1290  }
1291 
1297  public boolean isProofTrue()
1298  {
1300  }
1301 
1307  public boolean isProofAsserted()
1308  {
1310  }
1311 
1318  public boolean isProofGoal()
1319  {
1321  }
1322 
1332  public boolean isProofModusPonens()
1333  {
1335  }
1336 
1347  public boolean isProofReflexivity()
1348  {
1350  }
1351 
1359  public boolean isProofSymmetry()
1360  {
1362  }
1363 
1371  public boolean isProofTransitivity()
1372  {
1374  }
1375 
1392  public boolean isProofTransitivityStar()
1393  {
1395  }
1396 
1407  public boolean isProofMonotonicity()
1408  {
1410  }
1411 
1418  public boolean isProofQuantIntro()
1419  {
1421  }
1422 
1437  public boolean isProofDistributivity()
1438  {
1440  }
1441 
1448  public boolean isProofAndElimination()
1449  {
1451  }
1452 
1459  public boolean isProofOrElimination()
1460  {
1462  }
1463 
1479  public boolean isProofRewrite()
1480  {
1482  }
1483 
1498  public boolean isProofRewriteStar()
1499  {
1501  }
1502 
1510  public boolean isProofPullQuant()
1511  {
1513  }
1514 
1522  public boolean isProofPullQuantStar()
1523  {
1525  }
1526 
1536  public boolean isProofPushQuant()
1537  {
1539  }
1540 
1552  public boolean isProofElimUnusedVars()
1553  {
1555  }
1556 
1568  public boolean isProofDER()
1569  {
1571  }
1572 
1580  public boolean isProofQuantInst()
1581  {
1583  }
1584 
1592  public boolean isProofHypothesis()
1593  {
1595  }
1596 
1608  public boolean isProofLemma()
1609  {
1611  }
1612 
1619  public boolean isProofUnitResolution()
1620  {
1622  }
1623 
1631  public boolean isProofIFFTrue()
1632  {
1634  }
1635 
1643  public boolean isProofIFFFalse()
1644  {
1646  }
1647 
1660  public boolean isProofCommutativity()
1661  {
1663  }
1664 
1686  public boolean isProofDefAxiom()
1687  {
1689  }
1690 
1709  public boolean isProofDefIntro()
1710  {
1712  }
1713 
1721  public boolean isProofApplyDef()
1722  {
1724  }
1725 
1733  public boolean isProofIFFOEQ()
1734  {
1736  }
1737 
1761  public boolean isProofNNFPos()
1762  {
1764  }
1765 
1780  public boolean isProofNNFNeg()
1781  {
1783  }
1784 
1798  public boolean isProofNNFStar()
1799  {
1801  }
1802 
1813  public boolean isProofCNFStar()
1814  {
1816  }
1817 
1830  public boolean isProofSkolemize()
1831  {
1833  }
1834 
1843  public boolean isProofModusPonensOEQ()
1844  {
1846  }
1847 
1865  public boolean isProofTheoryLemma()
1866  {
1868  }
1869 
1875  public boolean isRelation()
1876  {
1877  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1878  .getSortKind(getContext().nCtx(),
1879  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1880  .toInt());
1881  }
1882 
1892  public boolean isRelationStore()
1893  {
1895  }
1896 
1902  public boolean isEmptyRelation()
1903  {
1905  }
1906 
1912  public boolean isIsEmptyRelation()
1913  {
1915  }
1916 
1922  public boolean isRelationalJoin()
1923  {
1925  }
1926 
1934  public boolean isRelationUnion()
1935  {
1937  }
1938 
1946  public boolean isRelationWiden()
1947  {
1949  }
1950 
1959  public boolean isRelationProject()
1960  {
1962  }
1963 
1974  public boolean isRelationFilter()
1975  {
1977  }
1978 
1994  public boolean isRelationNegationFilter()
1995  {
1997  }
1998 
2006  public boolean isRelationRename()
2007  {
2009  }
2010 
2016  public boolean isRelationComplement()
2017  {
2019  }
2020 
2030  public boolean isRelationSelect()
2031  {
2033  }
2034 
2046  public boolean isRelationClone()
2047  {
2049  }
2050 
2056  public boolean isFiniteDomain()
2057  {
2058  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
2059  .getSortKind(getContext().nCtx(),
2060  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
2061  .toInt());
2062  }
2063 
2069  public boolean isFiniteDomainLT()
2070  {
2072  }
2073 
2092  public int getIndex()
2093  {
2094  if (!isVar()) {
2095  throw new Z3Exception("Term is not a bound variable.");
2096  }
2097 
2098  return Native.getIndexValue(getContext().nCtx(), getNativeObject());
2099  }
2100 
2105  protected Expr(Context ctx, long obj) {
2106  super(ctx, obj);
2107  }
2108 
2109  @Override
2110  void checkNativeObject(long obj) {
2111  if (!Native.isApp(getContext().nCtx(), obj) &&
2112  Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
2113  Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) {
2114  throw new Z3Exception("Underlying object is not a term");
2115  }
2116  super.checkNativeObject(obj);
2117  }
2118 
2119  static Expr create(Context ctx, FuncDecl f, Expr ... arguments)
2120 
2121  {
2122  long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
2123  AST.arrayLength(arguments), AST.arrayToNative(arguments));
2124  return create(ctx, obj);
2125  }
2126 
2127  static Expr create(Context ctx, long obj)
2128  {
2129  Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
2130  if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
2131  return new Quantifier(ctx, obj);
2132  long s = Native.getSort(ctx.nCtx(), obj);
2134  .fromInt(Native.getSortKind(ctx.nCtx(), s));
2135 
2136  if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast?
2137  return new AlgebraicNum(ctx, obj);
2138 
2139  if (Native.isNumeralAst(ctx.nCtx(), obj))
2140  {
2141  switch (sk)
2142  {
2143  case Z3_INT_SORT:
2144  return new IntNum(ctx, obj);
2145  case Z3_REAL_SORT:
2146  return new RatNum(ctx, obj);
2147  case Z3_BV_SORT:
2148  return new BitVecNum(ctx, obj);
2150  return new FPNum(ctx, obj);
2151  case Z3_ROUNDING_MODE_SORT:
2152  return new FPRMNum(ctx, obj);
2153  case Z3_FINITE_DOMAIN_SORT:
2154  return new FiniteDomainNum(ctx, obj);
2155  default: ;
2156  }
2157  }
2158 
2159  switch (sk)
2160  {
2161  case Z3_BOOL_SORT:
2162  return new BoolExpr(ctx, obj);
2163  case Z3_INT_SORT:
2164  return new IntExpr(ctx, obj);
2165  case Z3_REAL_SORT:
2166  return new RealExpr(ctx, obj);
2167  case Z3_BV_SORT:
2168  return new BitVecExpr(ctx, obj);
2169  case Z3_ARRAY_SORT:
2170  return new ArrayExpr(ctx, obj);
2171  case Z3_DATATYPE_SORT:
2172  return new DatatypeExpr(ctx, obj);
2174  return new FPExpr(ctx, obj);
2175  case Z3_ROUNDING_MODE_SORT:
2176  return new FPRMExpr(ctx, obj);
2177  case Z3_FINITE_DOMAIN_SORT:
2178  return new FiniteDomainExpr(ctx, obj);
2179  case Z3_SEQ_SORT:
2180  return new SeqExpr(ctx, obj);
2181  case Z3_RE_SORT:
2182  return new ReExpr(ctx, obj);
2183  default: ;
2184  }
2185 
2186  return new Expr(ctx, obj);
2187  }
2188 }
boolean isProofNNFStar()
Definition: Expr.java:1798
boolean isEmptyRelation()
Definition: Expr.java:1902
static int getBoolValue(long a0, long a1)
Definition: Native.java:2753
boolean isApp()
Definition: AST.java:133
boolean isBVSGT()
Definition: Expr.java:979
boolean isProofTransitivityStar()
Definition: Expr.java:1392
boolean isProofModusPonens()
Definition: Expr.java:1332
boolean isBVBitZero()
Definition: Expr.java:758
boolean isIDiv()
Definition: Expr.java:537
boolean isProofRewrite()
Definition: Expr.java:1479
boolean isLT()
Definition: Expr.java:467
boolean isBVShiftLeft()
Definition: Expr.java:1139
boolean isBVSLE()
Definition: Expr.java:918
boolean isLE()
Definition: Expr.java:447
boolean isBVXNOR()
Definition: Expr.java:1049
static long mkApp(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1043
boolean isDiv()
Definition: Expr.java:527
boolean isBVULT()
Definition: Expr.java:949
boolean isGE()
Definition: Expr.java:457
boolean isWellSorted()
Definition: Expr.java:232
boolean isProofIFFOEQ()
Definition: Expr.java:1733
boolean isSetComplement()
Definition: Expr.java:706
boolean isProofElimUnusedVars()
Definition: Expr.java:1552
boolean isProofMonotonicity()
Definition: Expr.java:1407
boolean isBVRotateLeft()
Definition: Expr.java:1169
boolean isProofCNFStar()
Definition: Expr.java:1813
boolean isBVUGE()
Definition: Expr.java:929
static final Z3_ast_kind fromInt(int v)
Expr update(Expr[] args)
Definition: Expr.java:123
boolean isBVSDiv()
Definition: Expr.java:808
boolean isEq()
Definition: Expr.java:325
boolean isBVSub()
Definition: Expr.java:788
boolean isArrayMap()
Definition: Expr.java:655
static int getSortKind(long a0, long a1)
Definition: Native.java:2348
static final Z3_sort_kind fromInt(int v)
boolean isRealIsInt()
Definition: Expr.java:588
static int getAppNumArgs(long a0, long a1)
Definition: Native.java:2690
boolean isNot()
Definition: Expr.java:397
boolean isRelationSelect()
Definition: Expr.java:2030
boolean isRelationStore()
Definition: Expr.java:1892
boolean isProofNNFNeg()
Definition: Expr.java:1780
boolean isRemainder()
Definition: Expr.java:547
boolean isBVRotateLeftExtended()
Definition: Expr.java:1191
boolean isBVZeroExtension()
Definition: Expr.java:1079
boolean isUMinus()
Definition: Expr.java:507
static long substitute(long a0, long a1, int a2, long[] a3, long[] a4)
Definition: Native.java:3095
boolean isIff()
Definition: Expr.java:377
boolean isSetUnion()
Definition: Expr.java:676
boolean isBVSLT()
Definition: Expr.java:959
boolean isBVComp()
Definition: Expr.java:1129
boolean isBVConcat()
Definition: Expr.java:1059
boolean isProofSkolemize()
Definition: Expr.java:1830
boolean isConstantArray()
Definition: Expr.java:632
boolean isProofReflexivity()
Definition: Expr.java:1347
boolean isBVNumeral()
Definition: Expr.java:738
boolean isProofIFFFalse()
Definition: Expr.java:1643
boolean isProofDER()
Definition: Expr.java:1568
boolean isBVNAND()
Definition: Expr.java:1029
boolean isProofLemma()
Definition: Expr.java:1608
boolean isBVShiftRightArithmetic()
Definition: Expr.java:1159
boolean isProofPullQuantStar()
Definition: Expr.java:1522
static long updateTerm(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3086
boolean isXor()
Definition: Expr.java:387
static boolean isWellSorted(long a0, long a1)
Definition: Native.java:2744
boolean isBVUMinus()
Definition: Expr.java:768
boolean isStore()
Definition: Expr.java:611
boolean isProofIFFTrue()
Definition: Expr.java:1631
boolean isMul()
Definition: Expr.java:517
boolean isBVRotateRight()
Definition: Expr.java:1179
boolean isRealToInt()
Definition: Expr.java:577
boolean isRelationProject()
Definition: Expr.java:1959
boolean isAdd()
Definition: Expr.java:487
boolean isBVAND()
Definition: Expr.java:989
boolean isBVNOT()
Definition: Expr.java:1009
boolean isProofCommutativity()
Definition: Expr.java:1660
boolean isVar()
Definition: AST.java:143
boolean isDistinct()
Definition: Expr.java:336
boolean isDefaultArray()
Definition: Expr.java:643
static boolean isNumeralAst(long a0, long a1)
Definition: Native.java:2780
boolean isRelationNegationFilter()
Definition: Expr.java:1994
boolean isProofAndElimination()
Definition: Expr.java:1448
boolean isAnd()
Definition: Expr.java:356
boolean isExpr()
Definition: AST.java:114
static int getIndexValue(long a0, long a1)
Definition: Native.java:2951
boolean isBVBitOne()
Definition: Expr.java:748
Expr substitute(Expr from, Expr to)
Definition: Expr.java:164
boolean isBVReduceAND()
Definition: Expr.java:1119
boolean isSetDifference()
Definition: Expr.java:696
boolean isImplies()
Definition: Expr.java:407
boolean isAlgebraicNumber()
Definition: Expr.java:283
String toString()
Definition: Expr.java:211
boolean isBVURem()
Definition: Expr.java:838
boolean isBVRepeat()
Definition: Expr.java:1099
boolean isRelationRename()
Definition: Expr.java:2006
boolean isGT()
Definition: Expr.java:477
boolean isProofRewriteStar()
Definition: Expr.java:1498
boolean isProofPushQuant()
Definition: Expr.java:1536
boolean isRelationClone()
Definition: Expr.java:2046
boolean isProofPullQuant()
Definition: Expr.java:1510
boolean isRelationUnion()
Definition: Expr.java:1934
boolean isSetSubset()
Definition: Expr.java:716
Expr [] getArgs()
Definition: Expr.java:105
boolean isRelation()
Definition: Expr.java:1875
boolean isProofHypothesis()
Definition: Expr.java:1592
boolean isBVSRem()
Definition: Expr.java:828
boolean isLabel()
Definition: Expr.java:1262
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:107
boolean isAsArray()
Definition: Expr.java:666
boolean isBVExtract()
Definition: Expr.java:1089
boolean isReal()
Definition: Expr.java:427
boolean isRelationFilter()
Definition: Expr.java:1974
boolean isIntToBV()
Definition: Expr.java:1215
boolean isProofNNFPos()
Definition: Expr.java:1761
boolean isProofTransitivity()
Definition: Expr.java:1371
FuncDecl getFuncDecl()
Definition: Expr.java:72
static long simplifyEx(long a0, long a1, long a2)
Definition: Native.java:3059
boolean isBVToInt()
Definition: Expr.java:1227
boolean isProofOrElimination()
Definition: Expr.java:1459
boolean isProofTrue()
Definition: Expr.java:1297
boolean isProofUnitResolution()
Definition: Expr.java:1619
boolean isBVSignExtension()
Definition: Expr.java:1069
boolean isIntNum()
Definition: Expr.java:263
boolean isBVOR()
Definition: Expr.java:999
boolean isBVAdd()
Definition: Expr.java:778
boolean isBVShiftRightLogical()
Definition: Expr.java:1149
Expr translate(Context ctx)
Definition: Expr.java:195
boolean isIntToReal()
Definition: Expr.java:567
boolean isBVMul()
Definition: Expr.java:798
static boolean isApp(long a0, long a1)
Definition: Native.java:2771
boolean isBVReduceOR()
Definition: Expr.java:1109
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:2339
boolean isSub()
Definition: Expr.java:497
boolean isBVCarry()
Definition: Expr.java:1238
static long getAppArg(long a0, long a1, int a2)
Definition: Native.java:2699
boolean isFiniteDomain()
Definition: Expr.java:2056
boolean isRelationWiden()
Definition: Expr.java:1946
boolean isProofDefIntro()
Definition: Expr.java:1709
boolean isProofSymmetry()
Definition: Expr.java:1359
boolean isFiniteDomainLT()
Definition: Expr.java:2069
boolean isProofQuantIntro()
Definition: Expr.java:1418
boolean isTrue()
Definition: Expr.java:305
boolean isOr()
Definition: Expr.java:366
boolean isRatNum()
Definition: Expr.java:273
boolean isBV()
Definition: Expr.java:726
boolean isBVULE()
Definition: Expr.java:908
static int getAstKind(long a0, long a1)
Definition: Native.java:2762
boolean isProofGoal()
Definition: Expr.java:1318
Expr substituteVars(Expr[] to)
Definition: Expr.java:179
boolean isProofModusPonensOEQ()
Definition: Expr.java:1843
boolean isProofDefAxiom()
Definition: Expr.java:1686
static long simplify(long a0, long a1)
Definition: Native.java:3050
boolean isBVUGT()
Definition: Expr.java:969
boolean isProofDistributivity()
Definition: Expr.java:1437
static long getAppDecl(long a0, long a1)
Definition: Native.java:2681
boolean isNumeral()
Definition: Expr.java:221
boolean isIsEmptyRelation()
Definition: Expr.java:1912
boolean isBVSMod()
Definition: Expr.java:848
boolean isArithmeticNumeral()
Definition: Expr.java:437
boolean isArray()
Definition: Expr.java:598
boolean isProofQuantInst()
Definition: Expr.java:1580
boolean isFalse()
Definition: Expr.java:315
boolean isRelationalJoin()
Definition: Expr.java:1922
boolean isRelationComplement()
Definition: Expr.java:2016
boolean isBVXOR3()
Definition: Expr.java:1249
boolean isConst()
Definition: Expr.java:253
Expr(Context ctx, long obj)
Definition: Expr.java:2105
boolean isInt()
Definition: Expr.java:417
static long mkBoolSort(long a0)
Definition: Native.java:894
static long getSort(long a0, long a1)
Definition: Native.java:2735
Expr substitute(Expr[] from, Expr[] to)
Definition: Expr.java:145
static long substituteVars(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3104
boolean isLabelLit()
Definition: Expr.java:1275
boolean isProofApplyDef()
Definition: Expr.java:1721
boolean isBVXOR()
Definition: Expr.java:1019
boolean isITE()
Definition: Expr.java:346
boolean isBool()
Definition: Expr.java:293
boolean isProofAsserted()
Definition: Expr.java:1307
boolean isBVNOR()
Definition: Expr.java:1039
Z3_lbool getBoolValue()
Definition: Expr.java:84
boolean isBVSGE()
Definition: Expr.java:939
boolean isBVUDiv()
Definition: Expr.java:818
boolean isBVRotateRightExtended()
Definition: Expr.java:1203
boolean isSelect()
Definition: Expr.java:621
boolean isSetIntersect()
Definition: Expr.java:686
Expr simplify(Params p)
Definition: Expr.java:51
boolean isProofTheoryLemma()
Definition: Expr.java:1865
static long translate(long a0, long a1, long a2)
Definition: Native.java:3113
static boolean isAlgebraicNumber(long a0, long a1)
Definition: Native.java:2789
def String(name, ctx=None)
Definition: z3py.py:9443
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
boolean isModulus()
Definition: Expr.java:557