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 {
35  public Expr simplify() throws Z3Exception
36  {
37  return simplify(null);
38  }
39 
46  public Expr simplify(Params p) throws Z3Exception
47  {
48 
49  if (p == null)
50  return Expr.create(getContext(),
51  Native.simplify(getContext().nCtx(), getNativeObject()));
52  else
53  return Expr.create(
54  getContext(),
55  Native.simplifyEx(getContext().nCtx(), getNativeObject(),
56  p.getNativeObject()));
57  }
58 
64  {
65  return new FuncDecl(getContext(), Native.getAppDecl(getContext().nCtx(),
66  getNativeObject()));
67  }
68 
74  {
75  return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
76  getNativeObject()));
77  }
78 
82  public int getNumArgs() throws Z3Exception
83  {
84  return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
85  }
86 
90  public Expr[] getArgs() throws Z3Exception
91  {
92  int n = getNumArgs();
93  Expr[] res = new Expr[n];
94  for (int i = 0; i < n; i++)
95  res[i] = Expr.create(getContext(),
96  Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
97  return res;
98  }
99 
105  public void update(Expr[] args) throws Z3Exception
106  {
107  getContext().checkContextMatch(args);
108  if (isApp() && args.length != getNumArgs())
109  throw new Z3Exception("Number of arguments does not match");
110  setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(),
111  (int) args.length, Expr.arrayToNative(args)));
112  }
113 
123  public Expr substitute(Expr[] from, Expr[] to) throws Z3Exception
124  {
125  getContext().checkContextMatch(from);
126  getContext().checkContextMatch(to);
127  if (from.length != to.length)
128  throw new Z3Exception("Argument sizes do not match");
129  return Expr.create(getContext(), Native.substitute(getContext().nCtx(),
130  getNativeObject(), (int) from.length, Expr.arrayToNative(from),
131  Expr.arrayToNative(to)));
132  }
133 
138  public Expr substitute(Expr from, Expr to) throws Z3Exception
139  {
140 
141  return substitute(new Expr[] { from }, new Expr[] { to });
142  }
143 
150  public Expr substituteVars(Expr[] to) throws Z3Exception
151  {
152 
153  getContext().checkContextMatch(to);
154  return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
155  getNativeObject(), (int) to.length, Expr.arrayToNative(to)));
156  }
157 
165  public Expr translate(Context ctx) throws Z3Exception
166  {
167 
168  if (getContext() == ctx)
169  return this;
170  else
171  return Expr.create(
172  ctx,
173  Native.translate(getContext().nCtx(), getNativeObject(),
174  ctx.nCtx()));
175  }
176 
180  public String toString()
181  {
182  return super.toString();
183  }
184 
188  public boolean isNumeral() throws Z3Exception
189  {
190  return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
191  }
192 
198  public boolean isWellSorted() throws Z3Exception
199  {
200  return Native.isWellSorted(getContext().nCtx(), getNativeObject());
201  }
202 
206  public Sort getSort() throws Z3Exception
207  {
208  return Sort.create(getContext(),
209  Native.getSort(getContext().nCtx(), getNativeObject()));
210  }
211 
215  public boolean isConst() throws Z3Exception
216  {
217  return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
218  }
219 
223  public boolean isIntNum() throws Z3Exception
224  {
225  return isNumeral() && isInt();
226  }
227 
231  public boolean isRatNum() throws Z3Exception
232  {
233  return isNumeral() && isReal();
234  }
235 
239  public boolean isAlgebraicNumber() throws Z3Exception
240  {
241  return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
242  }
243 
247  public boolean isBool() throws Z3Exception
248  {
249  return (isExpr() && Native.isEqSort(getContext().nCtx(),
250  Native.mkBoolSort(getContext().nCtx()),
251  Native.getSort(getContext().nCtx(), getNativeObject())));
252  }
253 
257  public boolean isTrue() throws Z3Exception
258  {
260  }
261 
265  public boolean isFalse() throws Z3Exception
266  {
268  }
269 
273  public boolean isEq() throws Z3Exception
274  {
276  }
277 
282  public boolean isDistinct() throws Z3Exception
283  {
285  }
286 
290  public boolean isITE() throws Z3Exception
291  {
293  }
294 
298  public boolean isAnd() throws Z3Exception
299  {
301  }
302 
306  public boolean isOr() throws Z3Exception
307  {
309  }
310 
315  public boolean isIff() throws Z3Exception
316  {
318  }
319 
323  public boolean isXor() throws Z3Exception
324  {
326  }
327 
331  public boolean isNot() throws Z3Exception
332  {
334  }
335 
339  public boolean isImplies() throws Z3Exception
340  {
342  }
343 
347  public boolean isInt() throws Z3Exception
348  {
349  return (Native.isNumeralAst(getContext().nCtx(), getNativeObject()) && Native
350  .getSortKind(getContext().nCtx(),
351  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT
352  .toInt());
353  }
354 
358  public boolean isReal() throws Z3Exception
359  {
360  return Native.getSortKind(getContext().nCtx(),
361  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT
362  .toInt();
363  }
364 
368  public boolean isArithmeticNumeral() throws Z3Exception
369  {
371  }
372 
376  public boolean isLE() throws Z3Exception
377  {
379  }
380 
384  public boolean isGE() throws Z3Exception
385  {
387  }
388 
392  public boolean isLT() throws Z3Exception
393  {
395  }
396 
400  public boolean isGT() throws Z3Exception
401  {
403  }
404 
408  public boolean isAdd() throws Z3Exception
409  {
411  }
412 
416  public boolean isSub() throws Z3Exception
417  {
419  }
420 
424  public boolean isUMinus() throws Z3Exception
425  {
427  }
428 
432  public boolean isMul() throws Z3Exception
433  {
435  }
436 
440  public boolean isDiv() throws Z3Exception
441  {
443  }
444 
448  public boolean isIDiv() throws Z3Exception
449  {
451  }
452 
456  public boolean isRemainder() throws Z3Exception
457  {
459  }
460 
464  public boolean isModulus() throws Z3Exception
465  {
467  }
468 
472  public boolean isIntToReal() throws Z3Exception
473  {
475  }
476 
480  public boolean isRealToInt() throws Z3Exception
481  {
483  }
484 
489  public boolean isRealIsInt() throws Z3Exception
490  {
492  }
493 
497  public boolean isArray() throws Z3Exception
498  {
499  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
500  .fromInt(Native.getSortKind(getContext().nCtx(),
501  Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
502  }
503 
509  public boolean isStore() throws Z3Exception
510  {
512  }
513 
517  public boolean isSelect() throws Z3Exception
518  {
520  }
521 
527  public boolean isConstantArray() throws Z3Exception
528  {
530  }
531 
536  public boolean isDefaultArray() throws Z3Exception
537  {
539  }
540 
545  public boolean isArrayMap() throws Z3Exception
546  {
548  }
549 
555  public boolean isAsArray() throws Z3Exception
556  {
558  }
559 
563  public boolean isSetUnion() throws Z3Exception
564  {
566  }
567 
571  public boolean isSetIntersect() throws Z3Exception
572  {
574  }
575 
579  public boolean isSetDifference() throws Z3Exception
580  {
582  }
583 
587  public boolean isSetComplement() throws Z3Exception
588  {
590  }
591 
595  public boolean isSetSubset() throws Z3Exception
596  {
598  }
599 
603  public boolean isBV() throws Z3Exception
604  {
605  return Native.getSortKind(getContext().nCtx(),
606  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
607  .toInt();
608  }
609 
613  public boolean isBVNumeral() throws Z3Exception
614  {
616  }
617 
621  public boolean isBVBitOne() throws Z3Exception
622  {
624  }
625 
629  public boolean isBVBitZero() throws Z3Exception
630  {
632  }
633 
637  public boolean isBVUMinus() throws Z3Exception
638  {
640  }
641 
645  public boolean isBVAdd() throws Z3Exception
646  {
648  }
649 
653  public boolean isBVSub() throws Z3Exception
654  {
656  }
657 
661  public boolean isBVMul() throws Z3Exception
662  {
664  }
665 
669  public boolean isBVSDiv() throws Z3Exception
670  {
672  }
673 
677  public boolean isBVUDiv() throws Z3Exception
678  {
680  }
681 
685  public boolean isBVSRem() throws Z3Exception
686  {
688  }
689 
693  public boolean isBVURem() throws Z3Exception
694  {
696  }
697 
701  public boolean isBVSMod() throws Z3Exception
702  {
704  }
705 
709  boolean IsBVSDiv0() throws Z3Exception
710  {
712  }
713 
717  boolean IsBVUDiv0() throws Z3Exception
718  {
720  }
721 
725  boolean IsBVSRem0() throws Z3Exception
726  {
728  }
729 
733  boolean IsBVURem0() throws Z3Exception
734  {
736  }
737 
741  boolean IsBVSMod0() throws Z3Exception
742  {
744  }
745 
749  public boolean isBVULE() throws Z3Exception
750  {
752  }
753 
757  public boolean isBVSLE() throws Z3Exception
758  {
760  }
761 
766  public boolean isBVUGE() throws Z3Exception
767  {
769  }
770 
774  public boolean isBVSGE() throws Z3Exception
775  {
777  }
778 
782  public boolean isBVULT() throws Z3Exception
783  {
785  }
786 
790  public boolean isBVSLT() throws Z3Exception
791  {
793  }
794 
798  public boolean isBVUGT() throws Z3Exception
799  {
801  }
802 
806  public boolean isBVSGT() throws Z3Exception
807  {
809  }
810 
814  public boolean isBVAND() throws Z3Exception
815  {
817  }
818 
822  public boolean isBVOR() throws Z3Exception
823  {
825  }
826 
830  public boolean isBVNOT() throws Z3Exception
831  {
833  }
834 
838  public boolean isBVXOR() throws Z3Exception
839  {
841  }
842 
846  public boolean isBVNAND() throws Z3Exception
847  {
849  }
850 
854  public boolean isBVNOR() throws Z3Exception
855  {
857  }
858 
862  public boolean isBVXNOR() throws Z3Exception
863  {
865  }
866 
870  public boolean isBVConcat() throws Z3Exception
871  {
873  }
874 
878  public boolean isBVSignExtension() throws Z3Exception
879  {
881  }
882 
886  public boolean isBVZeroExtension() throws Z3Exception
887  {
889  }
890 
894  public boolean isBVExtract() throws Z3Exception
895  {
897  }
898 
902  public boolean isBVRepeat() throws Z3Exception
903  {
905  }
906 
910  public boolean isBVReduceOR() throws Z3Exception
911  {
913  }
914 
918  public boolean isBVReduceAND() throws Z3Exception
919  {
921  }
922 
926  public boolean isBVComp() throws Z3Exception
927  {
929  }
930 
934  public boolean isBVShiftLeft() throws Z3Exception
935  {
937  }
938 
942  public boolean isBVShiftRightLogical() throws Z3Exception
943  {
945  }
946 
950  public boolean isBVShiftRightArithmetic() throws Z3Exception
951  {
953  }
954 
958  public boolean isBVRotateLeft() throws Z3Exception
959  {
961  }
962 
966  public boolean isBVRotateRight() throws Z3Exception
967  {
969  }
970 
976  public boolean isBVRotateLeftExtended() throws Z3Exception
977  {
979  }
980 
986  public boolean isBVRotateRightExtended() throws Z3Exception
987  {
989  }
990 
997  public boolean isIntToBV() throws Z3Exception
998  {
1000  }
1001 
1008  public boolean isBVToInt() throws Z3Exception
1009  {
1011  }
1012 
1018  public boolean isBVCarry() throws Z3Exception
1019  {
1021  }
1022 
1028  public boolean isBVXOR3() throws Z3Exception
1029  {
1031  }
1032 
1038  public boolean isLabel() throws Z3Exception
1039  {
1041  }
1042 
1048  public boolean isLabelLit() throws Z3Exception
1049  {
1051  }
1052 
1058  public boolean isOEQ() throws Z3Exception
1059  {
1060  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
1061  }
1062 
1066  public boolean isProofTrue() throws Z3Exception
1067  {
1069  }
1070 
1074  public boolean isProofAsserted() throws Z3Exception
1075  {
1077  }
1078 
1083  public boolean isProofGoal() throws Z3Exception
1084  {
1086  }
1087 
1094  public boolean isProofModusPonens() throws Z3Exception
1095  {
1097  }
1098 
1106  public boolean isProofReflexivity() throws Z3Exception
1107  {
1109  }
1110 
1117  public boolean isProofSymmetry() throws Z3Exception
1118  {
1120  }
1121 
1128  public boolean isProofTransitivity() throws Z3Exception
1129  {
1131  }
1132 
1146  public boolean isProofTransitivityStar() throws Z3Exception
1147  {
1149  }
1150 
1158  public boolean isProofMonotonicity() throws Z3Exception
1159  {
1161  }
1162 
1168  public boolean isProofQuantIntro() throws Z3Exception
1169  {
1171  }
1172 
1184  public boolean isProofDistributivity() throws Z3Exception
1185  {
1187  }
1188 
1194  public boolean isProofAndElimination() throws Z3Exception
1195  {
1197  }
1198 
1204  public boolean isProofOrElimination() throws Z3Exception
1205  {
1207  }
1208 
1221  public boolean isProofRewrite() throws Z3Exception
1222  {
1224  }
1225 
1237  public boolean isProofRewriteStar() throws Z3Exception
1238  {
1240  }
1241 
1247  public boolean isProofPullQuant() throws Z3Exception
1248  {
1250  }
1251 
1258  public boolean isProofPullQuantStar() throws Z3Exception
1259  {
1261  }
1262 
1270  public boolean isProofPushQuant() throws Z3Exception
1271  {
1273  }
1274 
1283  public boolean isProofElimUnusedVars() throws Z3Exception
1284  {
1286  }
1287 
1297  public boolean isProofDER() throws Z3Exception
1298  {
1300  }
1301 
1306  public boolean isProofQuantInst() throws Z3Exception
1307  {
1309  }
1310 
1315  public boolean isProofHypothesis() throws Z3Exception
1316  {
1318  }
1319 
1328  public boolean isProofLemma() throws Z3Exception
1329  {
1331  }
1332 
1338  public boolean isProofUnitResolution() throws Z3Exception
1339  {
1341  }
1342 
1347  public boolean isProofIFFTrue() throws Z3Exception
1348  {
1350  }
1351 
1356  public boolean isProofIFFFalse() throws Z3Exception
1357  {
1359  }
1360 
1370  public boolean isProofCommutativity() throws Z3Exception
1371  {
1373  }
1374 
1393  public boolean isProofDefAxiom() throws Z3Exception
1394  {
1396  }
1397 
1414  public boolean isProofDefIntro() throws Z3Exception
1415  {
1417  }
1418 
1424  public boolean isProofApplyDef() throws Z3Exception
1425  {
1427  }
1428 
1433  public boolean isProofIFFOEQ() throws Z3Exception
1434  {
1436  }
1437 
1458  public boolean isProofNNFPos() throws Z3Exception
1459  {
1461  }
1462 
1474  public boolean isProofNNFNeg() throws Z3Exception
1475  {
1477  }
1478 
1489  public boolean isProofNNFStar() throws Z3Exception
1490  {
1492  }
1493 
1501  public boolean isProofCNFStar() throws Z3Exception
1502  {
1504  }
1505 
1515  public boolean isProofSkolemize() throws Z3Exception
1516  {
1518  }
1519 
1525  public boolean isProofModusPonensOEQ() throws Z3Exception
1526  {
1528  }
1529 
1544  public boolean isProofTheoryLemma() throws Z3Exception
1545  {
1547  }
1548 
1552  public boolean isRelation() throws Z3Exception
1553  {
1554  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1555  .getSortKind(getContext().nCtx(),
1556  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1557  .toInt());
1558  }
1559 
1566  public boolean isRelationStore() throws Z3Exception
1567  {
1569  }
1570 
1574  public boolean isEmptyRelation() throws Z3Exception
1575  {
1577  }
1578 
1582  public boolean isIsEmptyRelation() throws Z3Exception
1583  {
1585  }
1586 
1590  public boolean isRelationalJoin() throws Z3Exception
1591  {
1593  }
1594 
1599  public boolean isRelationUnion() throws Z3Exception
1600  {
1602  }
1603 
1608  public boolean isRelationWiden() throws Z3Exception
1609  {
1611  }
1612 
1618  public boolean isRelationProject() throws Z3Exception
1619  {
1621  }
1622 
1630  public boolean isRelationFilter() throws Z3Exception
1631  {
1633  }
1634 
1647  public boolean isRelationNegationFilter() throws Z3Exception
1648  {
1650  }
1651 
1657  public boolean isRelationRename() throws Z3Exception
1658  {
1660  }
1661 
1665  public boolean isRelationComplement() throws Z3Exception
1666  {
1668  }
1669 
1676  public boolean isRelationSelect() throws Z3Exception
1677  {
1679  }
1680 
1688  public boolean isRelationClone() throws Z3Exception
1689  {
1691  }
1692 
1696  public boolean isFiniteDomain() throws Z3Exception
1697  {
1698  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1699  .getSortKind(getContext().nCtx(),
1700  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
1701  .toInt());
1702  }
1703 
1707  public boolean isFiniteDomainLT() throws Z3Exception
1708  {
1710  }
1711 
1727  public int getIndex() throws Z3Exception
1728  {
1729  if (!isVar())
1730  throw new Z3Exception("Term is not a bound variable.");
1731 
1732  return Native.getIndexValue(getContext().nCtx(), getNativeObject());
1733  }
1734 
1738  protected Expr(Context ctx)
1739  {
1740  super(ctx);
1741  {
1742  }
1743  }
1744 
1748  protected Expr(Context ctx, long obj) throws Z3Exception
1749  {
1750  super(ctx, obj);
1751  {
1752  }
1753  }
1754 
1755  void checkNativeObject(long obj) throws Z3Exception
1756  {
1757  if (!Native.isApp(getContext().nCtx(), obj) &&
1758  Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
1759  Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt())
1760  throw new Z3Exception("Underlying object is not a term");
1761  super.checkNativeObject(obj);
1762  }
1763 
1764  static Expr create(Context ctx, FuncDecl f, Expr ... arguments)
1765  throws Z3Exception
1766  {
1767  long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
1768  AST.arrayLength(arguments), AST.arrayToNative(arguments));
1769  return create(ctx, obj);
1770  }
1771 
1772  static Expr create(Context ctx, long obj) throws Z3Exception
1773  {
1774  Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
1775  if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
1776  return new Quantifier(ctx, obj);
1777  long s = Native.getSort(ctx.nCtx(), obj);
1779  .fromInt(Native.getSortKind(ctx.nCtx(), s));
1780 
1781  if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast?
1782  return new AlgebraicNum(ctx, obj);
1783 
1784  if (Native.isNumeralAst(ctx.nCtx(), obj))
1785  {
1786  switch (sk)
1787  {
1788  case Z3_INT_SORT:
1789  return new IntNum(ctx, obj);
1790  case Z3_REAL_SORT:
1791  return new RatNum(ctx, obj);
1792  case Z3_BV_SORT:
1793  return new BitVecNum(ctx, obj);
1794  default: ;
1795  }
1796  }
1797 
1798  switch (sk)
1799  {
1800  case Z3_BOOL_SORT:
1801  return new BoolExpr(ctx, obj);
1802  case Z3_INT_SORT:
1803  return new IntExpr(ctx, obj);
1804  case Z3_REAL_SORT:
1805  return new RealExpr(ctx, obj);
1806  case Z3_BV_SORT:
1807  return new BitVecExpr(ctx, obj);
1808  case Z3_ARRAY_SORT:
1809  return new ArrayExpr(ctx, obj);
1810  case Z3_DATATYPE_SORT:
1811  return new DatatypeExpr(ctx, obj);
1812  default: ;
1813  }
1814 
1815  return new Expr(ctx, obj);
1816  }
1817 }
boolean isProofNNFStar()
Definition: Expr.java:1489
boolean isEmptyRelation()
Definition: Expr.java:1574
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
static int getBoolValue(long a0, long a1)
Definition: Native.java:2363
boolean isApp()
Definition: AST.java:144
boolean isBVSGT()
Definition: Expr.java:806
boolean isProofTransitivityStar()
Definition: Expr.java:1146
boolean isProofModusPonens()
Definition: Expr.java:1094
boolean isBVBitZero()
Definition: Expr.java:629
boolean isIDiv()
Definition: Expr.java:448
boolean isProofRewrite()
Definition: Expr.java:1221
boolean isLT()
Definition: Expr.java:392
boolean isBVShiftLeft()
Definition: Expr.java:934
boolean isBVSLE()
Definition: Expr.java:757
boolean isLE()
Definition: Expr.java:376
boolean isBVXNOR()
Definition: Expr.java:862
boolean isDiv()
Definition: Expr.java:440
boolean isBVULT()
Definition: Expr.java:782
boolean isGE()
Definition: Expr.java:384
boolean isWellSorted()
Definition: Expr.java:198
boolean isProofIFFOEQ()
Definition: Expr.java:1433
boolean isSetComplement()
Definition: Expr.java:587
boolean isProofElimUnusedVars()
Definition: Expr.java:1283
boolean isProofMonotonicity()
Definition: Expr.java:1158
boolean isBVRotateLeft()
Definition: Expr.java:958
boolean isProofCNFStar()
Definition: Expr.java:1501
boolean isBVUGE()
Definition: Expr.java:766
boolean isBVSDiv()
Definition: Expr.java:669
boolean isEq()
Definition: Expr.java:273
boolean isBVSub()
Definition: Expr.java:653
boolean isArrayMap()
Definition: Expr.java:545
static int getSortKind(long a0, long a1)
Definition: Native.java:1994
Expr(Context ctx)
Definition: Expr.java:1738
static final Z3_sort_kind fromInt(int v)
boolean isRealIsInt()
Definition: Expr.java:489
static int getAppNumArgs(long a0, long a1)
Definition: Native.java:2300
boolean isNot()
Definition: Expr.java:331
boolean isRelationSelect()
Definition: Expr.java:1676
boolean isRelationStore()
Definition: Expr.java:1566
boolean isProofNNFNeg()
Definition: Expr.java:1474
boolean isRemainder()
Definition: Expr.java:456
boolean isBVRotateLeftExtended()
Definition: Expr.java:976
boolean isBVZeroExtension()
Definition: Expr.java:886
boolean isUMinus()
Definition: Expr.java:424
static long substitute(long a0, long a1, int a2, long[] a3, long[] a4)
Definition: Native.java:2705
boolean isIff()
Definition: Expr.java:315
boolean isSetUnion()
Definition: Expr.java:563
boolean isBVSLT()
Definition: Expr.java:790
boolean isBVComp()
Definition: Expr.java:926
boolean isBVConcat()
Definition: Expr.java:870
boolean isProofSkolemize()
Definition: Expr.java:1515
boolean isConstantArray()
Definition: Expr.java:527
boolean isProofReflexivity()
Definition: Expr.java:1106
boolean isBVNumeral()
Definition: Expr.java:613
boolean isProofIFFFalse()
Definition: Expr.java:1356
boolean isProofDER()
Definition: Expr.java:1297
boolean isBVNAND()
Definition: Expr.java:846
boolean isProofLemma()
Definition: Expr.java:1328
boolean isBVShiftRightArithmetic()
Definition: Expr.java:950
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
boolean isProofPullQuantStar()
Definition: Expr.java:1258
static long updateTerm(long a0, long a1, int a2, long[] a3)
Definition: Native.java:2696
boolean isXor()
Definition: Expr.java:323
static boolean isWellSorted(long a0, long a1)
Definition: Native.java:2354
boolean isBVUMinus()
Definition: Expr.java:637
boolean isStore()
Definition: Expr.java:509
boolean isProofIFFTrue()
Definition: Expr.java:1347
boolean isMul()
Definition: Expr.java:432
boolean isBVRotateRight()
Definition: Expr.java:966
boolean isRealToInt()
Definition: Expr.java:480
boolean isRelationProject()
Definition: Expr.java:1618
boolean isAdd()
Definition: Expr.java:408
void update(Expr[] args)
Definition: Expr.java:105
boolean isBVAND()
Definition: Expr.java:814
boolean isBVNOT()
Definition: Expr.java:830
boolean isProofCommutativity()
Definition: Expr.java:1370
boolean isVar()
Definition: AST.java:152
boolean isDistinct()
Definition: Expr.java:282
boolean isDefaultArray()
Definition: Expr.java:536
static boolean isNumeralAst(long a0, long a1)
Definition: Native.java:2390
boolean isRelationNegationFilter()
Definition: Expr.java:1647
boolean isProofAndElimination()
Definition: Expr.java:1194
boolean isAnd()
Definition: Expr.java:298
boolean isExpr()
Definition: AST.java:127
static int getIndexValue(long a0, long a1)
Definition: Native.java:2561
boolean isBVBitOne()
Definition: Expr.java:621
Expr substitute(Expr from, Expr to)
Definition: Expr.java:138
boolean isBVReduceAND()
Definition: Expr.java:918
boolean isSetDifference()
Definition: Expr.java:579
boolean isImplies()
Definition: Expr.java:339
boolean isAlgebraicNumber()
Definition: Expr.java:239
String toString()
Definition: Expr.java:180
boolean isBVURem()
Definition: Expr.java:693
boolean isBVRepeat()
Definition: Expr.java:902
boolean isRelationRename()
Definition: Expr.java:1657
boolean isGT()
Definition: Expr.java:400
boolean isProofRewriteStar()
Definition: Expr.java:1237
boolean isProofPushQuant()
Definition: Expr.java:1270
boolean isRelationClone()
Definition: Expr.java:1688
boolean isProofPullQuant()
Definition: Expr.java:1247
boolean isRelationUnion()
Definition: Expr.java:1599
boolean isSetSubset()
Definition: Expr.java:595
Expr[] getArgs()
Definition: Expr.java:90
boolean isRelation()
Definition: Expr.java:1552
boolean isProofHypothesis()
Definition: Expr.java:1315
boolean isBVSRem()
Definition: Expr.java:685
boolean isLabel()
Definition: Expr.java:1038
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
boolean isAsArray()
Definition: Expr.java:555
boolean isBVExtract()
Definition: Expr.java:894
boolean isReal()
Definition: Expr.java:358
boolean isRelationFilter()
Definition: Expr.java:1630
boolean isIntToBV()
Definition: Expr.java:997
boolean isProofNNFPos()
Definition: Expr.java:1458
boolean isProofTransitivity()
Definition: Expr.java:1128
FuncDecl getFuncDecl()
Definition: Expr.java:63
static long simplifyEx(long a0, long a1, long a2)
Definition: Native.java:2669
boolean isBVToInt()
Definition: Expr.java:1008
boolean isProofOrElimination()
Definition: Expr.java:1204
boolean isProofTrue()
Definition: Expr.java:1066
boolean isProofUnitResolution()
Definition: Expr.java:1338
boolean isBVSignExtension()
Definition: Expr.java:878
boolean isIntNum()
Definition: Expr.java:223
boolean isBVOR()
Definition: Expr.java:822
boolean isBVAdd()
Definition: Expr.java:645
boolean isBVShiftRightLogical()
Definition: Expr.java:942
Expr translate(Context ctx)
Definition: Expr.java:165
boolean isIntToReal()
Definition: Expr.java:472
boolean isBVMul()
Definition: Expr.java:661
static boolean isApp(long a0, long a1)
Definition: Native.java:2381
boolean isBVReduceOR()
Definition: Expr.java:910
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:1985
boolean isSub()
Definition: Expr.java:416
boolean isBVCarry()
Definition: Expr.java:1018
static long getAppArg(long a0, long a1, int a2)
Definition: Native.java:2309
boolean isFiniteDomain()
Definition: Expr.java:1696
boolean isRelationWiden()
Definition: Expr.java:1608
boolean isProofDefIntro()
Definition: Expr.java:1414
boolean isProofSymmetry()
Definition: Expr.java:1117
boolean isFiniteDomainLT()
Definition: Expr.java:1707
boolean isProofQuantIntro()
Definition: Expr.java:1168
boolean isTrue()
Definition: Expr.java:257
boolean isOr()
Definition: Expr.java:306
boolean isRatNum()
Definition: Expr.java:231
boolean isBV()
Definition: Expr.java:603
boolean isBVULE()
Definition: Expr.java:749
static int getAstKind(long a0, long a1)
Definition: Native.java:2372
boolean isProofGoal()
Definition: Expr.java:1083
Expr substituteVars(Expr[] to)
Definition: Expr.java:150
boolean isProofModusPonensOEQ()
Definition: Expr.java:1525
boolean isProofDefAxiom()
Definition: Expr.java:1393
static long simplify(long a0, long a1)
Definition: Native.java:2660
boolean isBVUGT()
Definition: Expr.java:798
boolean isProofDistributivity()
Definition: Expr.java:1184
static long getAppDecl(long a0, long a1)
Definition: Native.java:2291
boolean isNumeral()
Definition: Expr.java:188
boolean isIsEmptyRelation()
Definition: Expr.java:1582
boolean isBVSMod()
Definition: Expr.java:701
boolean isArithmeticNumeral()
Definition: Expr.java:368
boolean isArray()
Definition: Expr.java:497
boolean isProofQuantInst()
Definition: Expr.java:1306
boolean isFalse()
Definition: Expr.java:265
boolean isRelationalJoin()
Definition: Expr.java:1590
boolean isRelationComplement()
Definition: Expr.java:1665
boolean isBVXOR3()
Definition: Expr.java:1028
boolean isConst()
Definition: Expr.java:215
Expr(Context ctx, long obj)
Definition: Expr.java:1748
boolean isInt()
Definition: Expr.java:347
static long mkBoolSort(long a0)
Definition: Native.java:792
static long getSort(long a0, long a1)
Definition: Native.java:2345
Expr substitute(Expr[] from, Expr[] to)
Definition: Expr.java:123
static long substituteVars(long a0, long a1, int a2, long[] a3)
Definition: Native.java:2714
boolean isLabelLit()
Definition: Expr.java:1048
boolean isProofApplyDef()
Definition: Expr.java:1424
boolean isBVXOR()
Definition: Expr.java:838
boolean isITE()
Definition: Expr.java:290
boolean isBool()
Definition: Expr.java:247
boolean isProofAsserted()
Definition: Expr.java:1074
boolean isBVNOR()
Definition: Expr.java:854
Z3_lbool getBoolValue()
Definition: Expr.java:73
boolean isBVSGE()
Definition: Expr.java:774
boolean isBVUDiv()
Definition: Expr.java:677
boolean isBVRotateRightExtended()
Definition: Expr.java:986
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isSelect()
Definition: Expr.java:517
boolean isSetIntersect()
Definition: Expr.java:571
Expr simplify(Params p)
Definition: Expr.java:46
boolean isProofTheoryLemma()
Definition: Expr.java:1544
static long translate(long a0, long a1, long a2)
Definition: Native.java:2723
static boolean isAlgebraicNumber(long a0, long a1)
Definition: Native.java:2399
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:21
boolean isModulus()
Definition: Expr.java:464