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 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 
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  return (Expr) super.translate(ctx);
198  }
199 
203  @Override
204  public String toString()
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 
1152  public boolean isBVShiftRightArithmetic()
1153  {
1155  }
1156 
1162  public boolean isBVRotateLeft()
1163  {
1165  }
1166 
1172  public boolean isBVRotateRight()
1173  {
1175  }
1176 
1184  public boolean isBVRotateLeftExtended()
1185  {
1187  }
1188 
1196  public boolean isBVRotateRightExtended()
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 
1297  public boolean isConcat()
1298  {
1300  }
1301 
1309  public boolean isOEQ()
1310  {
1311  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
1312  }
1313 
1319  public boolean isProofTrue()
1320  {
1322  }
1323 
1329  public boolean isProofAsserted()
1330  {
1332  }
1333 
1340  public boolean isProofGoal()
1341  {
1343  }
1344 
1354  public boolean isProofModusPonens()
1355  {
1357  }
1358 
1369  public boolean isProofReflexivity()
1370  {
1372  }
1373 
1381  public boolean isProofSymmetry()
1382  {
1384  }
1385 
1393  public boolean isProofTransitivity()
1394  {
1396  }
1397 
1414  public boolean isProofTransitivityStar()
1415  {
1417  }
1418 
1429  public boolean isProofMonotonicity()
1430  {
1432  }
1433 
1440  public boolean isProofQuantIntro()
1441  {
1443  }
1444 
1459  public boolean isProofDistributivity()
1460  {
1462  }
1463 
1470  public boolean isProofAndElimination()
1471  {
1473  }
1474 
1481  public boolean isProofOrElimination()
1482  {
1484  }
1485 
1501  public boolean isProofRewrite()
1502  {
1504  }
1505 
1520  public boolean isProofRewriteStar()
1521  {
1523  }
1524 
1532  public boolean isProofPullQuant()
1533  {
1535  }
1536 
1544  public boolean isProofPullQuantStar()
1545  {
1547  }
1548 
1558  public boolean isProofPushQuant()
1559  {
1561  }
1562 
1574  public boolean isProofElimUnusedVars()
1575  {
1577  }
1578 
1590  public boolean isProofDER()
1591  {
1593  }
1594 
1602  public boolean isProofQuantInst()
1603  {
1605  }
1606 
1614  public boolean isProofHypothesis()
1615  {
1617  }
1618 
1630  public boolean isProofLemma()
1631  {
1633  }
1634 
1641  public boolean isProofUnitResolution()
1642  {
1644  }
1645 
1653  public boolean isProofIFFTrue()
1654  {
1656  }
1657 
1665  public boolean isProofIFFFalse()
1666  {
1668  }
1669 
1682  public boolean isProofCommutativity()
1683  {
1685  }
1686 
1708  public boolean isProofDefAxiom()
1709  {
1711  }
1712 
1731  public boolean isProofDefIntro()
1732  {
1734  }
1735 
1743  public boolean isProofApplyDef()
1744  {
1746  }
1747 
1755  public boolean isProofIFFOEQ()
1756  {
1758  }
1759 
1783  public boolean isProofNNFPos()
1784  {
1786  }
1787 
1802  public boolean isProofNNFNeg()
1803  {
1805  }
1806 
1820  public boolean isProofNNFStar()
1821  {
1823  }
1824 
1835  public boolean isProofCNFStar()
1836  {
1838  }
1839 
1852  public boolean isProofSkolemize()
1853  {
1855  }
1856 
1865  public boolean isProofModusPonensOEQ()
1866  {
1868  }
1869 
1887  public boolean isProofTheoryLemma()
1888  {
1890  }
1891 
1897  public boolean isRelation()
1898  {
1899  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1900  .getSortKind(getContext().nCtx(),
1901  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1902  .toInt());
1903  }
1904 
1914  public boolean isRelationStore()
1915  {
1917  }
1918 
1924  public boolean isEmptyRelation()
1925  {
1927  }
1928 
1934  public boolean isIsEmptyRelation()
1935  {
1937  }
1938 
1944  public boolean isRelationalJoin()
1945  {
1947  }
1948 
1956  public boolean isRelationUnion()
1957  {
1959  }
1960 
1968  public boolean isRelationWiden()
1969  {
1971  }
1972 
1981  public boolean isRelationProject()
1982  {
1984  }
1985 
1996  public boolean isRelationFilter()
1997  {
1999  }
2000 
2016  public boolean isRelationNegationFilter()
2017  {
2019  }
2020 
2028  public boolean isRelationRename()
2029  {
2031  }
2032 
2038  public boolean isRelationComplement()
2039  {
2041  }
2042 
2052  public boolean isRelationSelect()
2053  {
2055  }
2056 
2068  public boolean isRelationClone()
2069  {
2071  }
2072 
2078  public boolean isFiniteDomain()
2079  {
2080  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
2081  .getSortKind(getContext().nCtx(),
2082  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
2083  .toInt());
2084  }
2085 
2091  public boolean isFiniteDomainLT()
2092  {
2094  }
2095 
2114  public int getIndex()
2115  {
2116  if (!isVar()) {
2117  throw new Z3Exception("Term is not a bound variable.");
2118  }
2119 
2120  return Native.getIndexValue(getContext().nCtx(), getNativeObject());
2121  }
2122 
2127  protected Expr(Context ctx, long obj) {
2128  super(ctx, obj);
2129  }
2130 
2131  @Override
2132  void checkNativeObject(long obj) {
2133  if (!Native.isApp(getContext().nCtx(), obj) &&
2134  Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
2135  Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) {
2136  throw new Z3Exception("Underlying object is not a term");
2137  }
2138  super.checkNativeObject(obj);
2139  }
2140 
2141  static Expr create(Context ctx, FuncDecl f, Expr ... arguments)
2142 
2143  {
2144  long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
2145  AST.arrayLength(arguments), AST.arrayToNative(arguments));
2146  return create(ctx, obj);
2147  }
2148 
2149  static Expr create(Context ctx, long obj)
2150  {
2151  Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
2152  if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
2153  return new Quantifier(ctx, obj);
2154  long s = Native.getSort(ctx.nCtx(), obj);
2156  .fromInt(Native.getSortKind(ctx.nCtx(), s));
2157 
2158  if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast?
2159  return new AlgebraicNum(ctx, obj);
2160 
2161  if (Native.isNumeralAst(ctx.nCtx(), obj))
2162  {
2163  switch (sk)
2164  {
2165  case Z3_INT_SORT:
2166  return new IntNum(ctx, obj);
2167  case Z3_REAL_SORT:
2168  return new RatNum(ctx, obj);
2169  case Z3_BV_SORT:
2170  return new BitVecNum(ctx, obj);
2172  return new FPNum(ctx, obj);
2173  case Z3_ROUNDING_MODE_SORT:
2174  return new FPRMNum(ctx, obj);
2175  case Z3_FINITE_DOMAIN_SORT:
2176  return new FiniteDomainNum(ctx, obj);
2177  default: ;
2178  }
2179  }
2180 
2181  switch (sk)
2182  {
2183  case Z3_BOOL_SORT:
2184  return new BoolExpr(ctx, obj);
2185  case Z3_INT_SORT:
2186  return new IntExpr(ctx, obj);
2187  case Z3_REAL_SORT:
2188  return new RealExpr(ctx, obj);
2189  case Z3_BV_SORT:
2190  return new BitVecExpr(ctx, obj);
2191  case Z3_ARRAY_SORT:
2192  return new ArrayExpr(ctx, obj);
2193  case Z3_DATATYPE_SORT:
2194  return new DatatypeExpr(ctx, obj);
2196  return new FPExpr(ctx, obj);
2197  case Z3_ROUNDING_MODE_SORT:
2198  return new FPRMExpr(ctx, obj);
2199  case Z3_FINITE_DOMAIN_SORT:
2200  return new FiniteDomainExpr(ctx, obj);
2201  case Z3_SEQ_SORT:
2202  return new SeqExpr(ctx, obj);
2203  case Z3_RE_SORT:
2204  return new ReExpr(ctx, obj);
2205  default: ;
2206  }
2207 
2208  return new Expr(ctx, obj);
2209  }
2210 }
boolean isProofNNFStar()
Definition: Expr.java:1820
boolean isEmptyRelation()
Definition: Expr.java:1924
static int getBoolValue(long a0, long a1)
Definition: Native.java:2922
boolean isApp()
Definition: AST.java:131
boolean isBVSGT()
Definition: Expr.java:972
boolean isProofTransitivityStar()
Definition: Expr.java:1414
String getString()
Definition: Expr.java:1288
boolean isProofModusPonens()
Definition: Expr.java:1354
boolean isBVBitZero()
Definition: Expr.java:751
boolean isIDiv()
Definition: Expr.java:530
boolean isProofRewrite()
Definition: Expr.java:1501
boolean isLT()
Definition: Expr.java:460
boolean isBVShiftLeft()
Definition: Expr.java:1132
boolean isBVSLE()
Definition: Expr.java:911
boolean isLE()
Definition: Expr.java:440
boolean isBVXNOR()
Definition: Expr.java:1042
static long mkApp(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1086
boolean isDiv()
Definition: Expr.java:520
boolean isBVULT()
Definition: Expr.java:942
boolean isGE()
Definition: Expr.java:450
boolean isWellSorted()
Definition: Expr.java:225
boolean isProofIFFOEQ()
Definition: Expr.java:1755
boolean isSetComplement()
Definition: Expr.java:699
boolean isProofElimUnusedVars()
Definition: Expr.java:1574
boolean isProofMonotonicity()
Definition: Expr.java:1429
boolean isBVRotateLeft()
Definition: Expr.java:1162
boolean isProofCNFStar()
Definition: Expr.java:1835
boolean isBVUGE()
Definition: Expr.java:922
static final Z3_ast_kind fromInt(int v)
Expr update(Expr[] args)
Definition: Expr.java:123
boolean isBVSDiv()
Definition: Expr.java:801
boolean isEq()
Definition: Expr.java:318
boolean isBVSub()
Definition: Expr.java:781
boolean isArrayMap()
Definition: Expr.java:648
static int getSortKind(long a0, long a1)
Definition: Native.java:2499
static final Z3_sort_kind fromInt(int v)
boolean isRealIsInt()
Definition: Expr.java:581
static int getAppNumArgs(long a0, long a1)
Definition: Native.java:2859
boolean isNot()
Definition: Expr.java:390
boolean isRelationSelect()
Definition: Expr.java:2052
boolean isRelationStore()
Definition: Expr.java:1914
boolean isProofNNFNeg()
Definition: Expr.java:1802
boolean isRemainder()
Definition: Expr.java:540
boolean isBVRotateLeftExtended()
Definition: Expr.java:1184
boolean isBVZeroExtension()
Definition: Expr.java:1072
boolean isUMinus()
Definition: Expr.java:500
static long substitute(long a0, long a1, int a2, long[] a3, long[] a4)
Definition: Native.java:3264
boolean isIff()
Definition: Expr.java:370
boolean isSetUnion()
Definition: Expr.java:669
boolean isBVSLT()
Definition: Expr.java:952
boolean isBVComp()
Definition: Expr.java:1122
boolean isBVConcat()
Definition: Expr.java:1052
boolean isProofSkolemize()
Definition: Expr.java:1852
boolean isConstantArray()
Definition: Expr.java:625
boolean isProofReflexivity()
Definition: Expr.java:1369
boolean isBVNumeral()
Definition: Expr.java:731
boolean isProofIFFFalse()
Definition: Expr.java:1665
boolean isProofDER()
Definition: Expr.java:1590
boolean isBVNAND()
Definition: Expr.java:1022
boolean isProofLemma()
Definition: Expr.java:1630
boolean isBVShiftRightArithmetic()
Definition: Expr.java:1152
boolean isProofPullQuantStar()
Definition: Expr.java:1544
static long updateTerm(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3255
boolean isXor()
Definition: Expr.java:380
static boolean isWellSorted(long a0, long a1)
Definition: Native.java:2913
boolean isBVUMinus()
Definition: Expr.java:761
boolean isStore()
Definition: Expr.java:604
boolean isProofIFFTrue()
Definition: Expr.java:1653
boolean isMul()
Definition: Expr.java:510
boolean isBVRotateRight()
Definition: Expr.java:1172
boolean isRealToInt()
Definition: Expr.java:570
boolean isRelationProject()
Definition: Expr.java:1981
boolean isAdd()
Definition: Expr.java:480
boolean isBVAND()
Definition: Expr.java:982
boolean isBVNOT()
Definition: Expr.java:1002
boolean isProofCommutativity()
Definition: Expr.java:1682
boolean isVar()
Definition: AST.java:141
boolean isDistinct()
Definition: Expr.java:329
boolean isDefaultArray()
Definition: Expr.java:636
static boolean isNumeralAst(long a0, long a1)
Definition: Native.java:2949
boolean isRelationNegationFilter()
Definition: Expr.java:2016
boolean isProofAndElimination()
Definition: Expr.java:1470
boolean isAnd()
Definition: Expr.java:349
boolean isExpr()
Definition: AST.java:112
static int getIndexValue(long a0, long a1)
Definition: Native.java:3120
boolean isBVBitOne()
Definition: Expr.java:741
Expr substitute(Expr from, Expr to)
Definition: Expr.java:164
boolean isBVReduceAND()
Definition: Expr.java:1112
boolean isSetDifference()
Definition: Expr.java:689
boolean isImplies()
Definition: Expr.java:400
boolean isAlgebraicNumber()
Definition: Expr.java:276
String toString()
Definition: Expr.java:204
boolean isBVURem()
Definition: Expr.java:831
boolean isBVRepeat()
Definition: Expr.java:1092
boolean isRelationRename()
Definition: Expr.java:2028
boolean isGT()
Definition: Expr.java:470
boolean isProofRewriteStar()
Definition: Expr.java:1520
boolean isProofPushQuant()
Definition: Expr.java:1558
boolean isRelationClone()
Definition: Expr.java:2068
boolean isProofPullQuant()
Definition: Expr.java:1532
boolean isRelationUnion()
Definition: Expr.java:1956
boolean isSetSubset()
Definition: Expr.java:709
Expr [] getArgs()
Definition: Expr.java:105
boolean isRelation()
Definition: Expr.java:1897
boolean isProofHypothesis()
Definition: Expr.java:1614
boolean isBVSRem()
Definition: Expr.java:821
boolean isLabel()
Definition: Expr.java:1255
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:119
boolean isAsArray()
Definition: Expr.java:659
boolean isBVExtract()
Definition: Expr.java:1082
boolean isReal()
Definition: Expr.java:420
boolean isRelationFilter()
Definition: Expr.java:1996
boolean isIntToBV()
Definition: Expr.java:1208
boolean isProofNNFPos()
Definition: Expr.java:1783
boolean isProofTransitivity()
Definition: Expr.java:1393
FuncDecl getFuncDecl()
Definition: Expr.java:72
static long simplifyEx(long a0, long a1, long a2)
Definition: Native.java:3228
boolean isBVToInt()
Definition: Expr.java:1220
boolean isProofOrElimination()
Definition: Expr.java:1481
boolean isProofTrue()
Definition: Expr.java:1319
boolean isProofUnitResolution()
Definition: Expr.java:1641
boolean isBVSignExtension()
Definition: Expr.java:1062
boolean isIntNum()
Definition: Expr.java:256
boolean isBVOR()
Definition: Expr.java:992
boolean isBVAdd()
Definition: Expr.java:771
boolean isBVShiftRightLogical()
Definition: Expr.java:1142
Expr translate(Context ctx)
Definition: Expr.java:195
boolean isIntToReal()
Definition: Expr.java:560
boolean isBVMul()
Definition: Expr.java:791
static boolean isApp(long a0, long a1)
Definition: Native.java:2940
boolean isBVReduceOR()
Definition: Expr.java:1102
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:2490
boolean isSub()
Definition: Expr.java:490
boolean isBVCarry()
Definition: Expr.java:1231
static long getAppArg(long a0, long a1, int a2)
Definition: Native.java:2868
boolean isFiniteDomain()
Definition: Expr.java:2078
boolean isRelationWiden()
Definition: Expr.java:1968
boolean isProofDefIntro()
Definition: Expr.java:1731
boolean isProofSymmetry()
Definition: Expr.java:1381
boolean isFiniteDomainLT()
Definition: Expr.java:2091
boolean isProofQuantIntro()
Definition: Expr.java:1440
boolean isTrue()
Definition: Expr.java:298
boolean isOr()
Definition: Expr.java:359
boolean isRatNum()
Definition: Expr.java:266
boolean isBV()
Definition: Expr.java:719
boolean isBVULE()
Definition: Expr.java:901
static int getAstKind(long a0, long a1)
Definition: Native.java:2931
boolean isProofGoal()
Definition: Expr.java:1340
Expr substituteVars(Expr[] to)
Definition: Expr.java:179
boolean isProofModusPonensOEQ()
Definition: Expr.java:1865
boolean isProofDefAxiom()
Definition: Expr.java:1708
static long simplify(long a0, long a1)
Definition: Native.java:3219
boolean isBVUGT()
Definition: Expr.java:962
boolean isProofDistributivity()
Definition: Expr.java:1459
static String getString(long a0, long a1)
Definition: Native.java:2103
static long getAppDecl(long a0, long a1)
Definition: Native.java:2850
boolean isNumeral()
Definition: Expr.java:214
boolean isIsEmptyRelation()
Definition: Expr.java:1934
boolean isBVSMod()
Definition: Expr.java:841
boolean isArithmeticNumeral()
Definition: Expr.java:430
boolean isArray()
Definition: Expr.java:591
boolean isProofQuantInst()
Definition: Expr.java:1602
boolean isFalse()
Definition: Expr.java:308
boolean isRelationalJoin()
Definition: Expr.java:1944
boolean isRelationComplement()
Definition: Expr.java:2038
boolean isBVXOR3()
Definition: Expr.java:1242
boolean isConst()
Definition: Expr.java:246
Expr(Context ctx, long obj)
Definition: Expr.java:2127
boolean isInt()
Definition: Expr.java:410
static long mkBoolSort(long a0)
Definition: Native.java:928
static long getSort(long a0, long a1)
Definition: Native.java:2904
Expr substitute(Expr[] from, Expr[] to)
Definition: Expr.java:145
static long substituteVars(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3273
boolean isConcat()
Definition: Expr.java:1297
boolean isLabelLit()
Definition: Expr.java:1268
boolean isProofApplyDef()
Definition: Expr.java:1743
boolean isBVXOR()
Definition: Expr.java:1012
boolean isITE()
Definition: Expr.java:339
boolean isBool()
Definition: Expr.java:286
boolean isProofAsserted()
Definition: Expr.java:1329
boolean isBVNOR()
Definition: Expr.java:1032
Z3_lbool getBoolValue()
Definition: Expr.java:84
boolean isBVSGE()
Definition: Expr.java:932
boolean isBVUDiv()
Definition: Expr.java:811
static boolean isString(long a0, long a1)
Definition: Native.java:2094
boolean isBVRotateRightExtended()
Definition: Expr.java:1196
boolean isSelect()
Definition: Expr.java:614
boolean isSetIntersect()
Definition: Expr.java:679
Expr simplify(Params p)
Definition: Expr.java:51
boolean isProofTheoryLemma()
Definition: Expr.java:1887
static boolean isAlgebraicNumber(long a0, long a1)
Definition: Native.java:2958
def String(name, ctx=None)
Definition: z3py.py:9738
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
boolean isModulus()
Definition: Expr.java:550
boolean isString()
Definition: Expr.java:1277