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 
1313  public boolean isConcat()
1314  {
1316  }
1317 
1325  public boolean isOEQ()
1326  {
1327  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
1328  }
1329 
1335  public boolean isProofTrue()
1336  {
1338  }
1339 
1345  public boolean isProofAsserted()
1346  {
1348  }
1349 
1356  public boolean isProofGoal()
1357  {
1359  }
1360 
1370  public boolean isProofModusPonens()
1371  {
1373  }
1374 
1385  public boolean isProofReflexivity()
1386  {
1388  }
1389 
1397  public boolean isProofSymmetry()
1398  {
1400  }
1401 
1409  public boolean isProofTransitivity()
1410  {
1412  }
1413 
1429  public boolean isProofTransitivityStar()
1430  {
1432  }
1433 
1444  public boolean isProofMonotonicity()
1445  {
1447  }
1448 
1455  public boolean isProofQuantIntro()
1456  {
1458  }
1459 
1474  public boolean isProofDistributivity()
1475  {
1477  }
1478 
1485  public boolean isProofAndElimination()
1486  {
1488  }
1489 
1496  public boolean isProofOrElimination()
1497  {
1499  }
1500 
1516  public boolean isProofRewrite()
1517  {
1519  }
1520 
1532  public boolean isProofRewriteStar()
1533  {
1535  }
1536 
1544  public boolean isProofPullQuant()
1545  {
1547  }
1548 
1549 
1559  public boolean isProofPushQuant()
1560  {
1562  }
1563 
1575  public boolean isProofElimUnusedVars()
1576  {
1578  }
1579 
1591  public boolean isProofDER()
1592  {
1594  }
1595 
1603  public boolean isProofQuantInst()
1604  {
1606  }
1607 
1615  public boolean isProofHypothesis()
1616  {
1618  }
1619 
1631  public boolean isProofLemma()
1632  {
1634  }
1635 
1642  public boolean isProofUnitResolution()
1643  {
1645  }
1646 
1654  public boolean isProofIFFTrue()
1655  {
1657  }
1658 
1666  public boolean isProofIFFFalse()
1667  {
1669  }
1670 
1683  public boolean isProofCommutativity()
1684  {
1686  }
1687 
1709  public boolean isProofDefAxiom()
1710  {
1712  }
1713 
1732  public boolean isProofDefIntro()
1733  {
1735  }
1736 
1744  public boolean isProofApplyDef()
1745  {
1747  }
1748 
1756  public boolean isProofIFFOEQ()
1757  {
1759  }
1760 
1784  public boolean isProofNNFPos()
1785  {
1787  }
1788 
1803  public boolean isProofNNFNeg()
1804  {
1806  }
1807 
1808 
1821  public boolean isProofSkolemize()
1822  {
1824  }
1825 
1834  public boolean isProofModusPonensOEQ()
1835  {
1837  }
1838 
1856  public boolean isProofTheoryLemma()
1857  {
1859  }
1860 
1866  public boolean isRelation()
1867  {
1868  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1869  .getSortKind(getContext().nCtx(),
1870  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1871  .toInt());
1872  }
1873 
1883  public boolean isRelationStore()
1884  {
1886  }
1887 
1893  public boolean isEmptyRelation()
1894  {
1896  }
1897 
1903  public boolean isIsEmptyRelation()
1904  {
1906  }
1907 
1913  public boolean isRelationalJoin()
1914  {
1916  }
1917 
1925  public boolean isRelationUnion()
1926  {
1928  }
1929 
1937  public boolean isRelationWiden()
1938  {
1940  }
1941 
1950  public boolean isRelationProject()
1951  {
1953  }
1954 
1965  public boolean isRelationFilter()
1966  {
1968  }
1969 
1985  public boolean isRelationNegationFilter()
1986  {
1988  }
1989 
1997  public boolean isRelationRename()
1998  {
2000  }
2001 
2007  public boolean isRelationComplement()
2008  {
2010  }
2011 
2021  public boolean isRelationSelect()
2022  {
2024  }
2025 
2037  public boolean isRelationClone()
2038  {
2040  }
2041 
2047  public boolean isFiniteDomain()
2048  {
2049  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
2050  .getSortKind(getContext().nCtx(),
2051  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
2052  .toInt());
2053  }
2054 
2060  public boolean isFiniteDomainLT()
2061  {
2063  }
2064 
2083  public int getIndex()
2084  {
2085  if (!isVar()) {
2086  throw new Z3Exception("Term is not a bound variable.");
2087  }
2088 
2089  return Native.getIndexValue(getContext().nCtx(), getNativeObject());
2090  }
2091 
2096  protected Expr(Context ctx, long obj) {
2097  super(ctx, obj);
2098  }
2099 
2100  @Override
2101  void checkNativeObject(long obj) {
2102  if (!Native.isApp(getContext().nCtx(), obj) &&
2103  Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
2104  Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) {
2105  throw new Z3Exception("Underlying object is not a term");
2106  }
2107  super.checkNativeObject(obj);
2108  }
2109 
2110  static Expr create(Context ctx, FuncDecl f, Expr ... arguments)
2111 
2112  {
2113  long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
2114  AST.arrayLength(arguments), AST.arrayToNative(arguments));
2115  return create(ctx, obj);
2116  }
2117 
2118  static Expr create(Context ctx, long obj)
2119  {
2120  Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
2121  if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
2122  return new Quantifier(ctx, obj);
2123  long s = Native.getSort(ctx.nCtx(), obj);
2125  .fromInt(Native.getSortKind(ctx.nCtx(), s));
2126 
2127  if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast?
2128  return new AlgebraicNum(ctx, obj);
2129 
2130  if (Native.isNumeralAst(ctx.nCtx(), obj))
2131  {
2132  switch (sk)
2133  {
2134  case Z3_INT_SORT:
2135  return new IntNum(ctx, obj);
2136  case Z3_REAL_SORT:
2137  return new RatNum(ctx, obj);
2138  case Z3_BV_SORT:
2139  return new BitVecNum(ctx, obj);
2141  return new FPNum(ctx, obj);
2142  case Z3_ROUNDING_MODE_SORT:
2143  return new FPRMNum(ctx, obj);
2144  case Z3_FINITE_DOMAIN_SORT:
2145  return new FiniteDomainNum(ctx, obj);
2146  default: ;
2147  }
2148  }
2149 
2150  switch (sk)
2151  {
2152  case Z3_BOOL_SORT:
2153  return new BoolExpr(ctx, obj);
2154  case Z3_INT_SORT:
2155  return new IntExpr(ctx, obj);
2156  case Z3_REAL_SORT:
2157  return new RealExpr(ctx, obj);
2158  case Z3_BV_SORT:
2159  return new BitVecExpr(ctx, obj);
2160  case Z3_ARRAY_SORT:
2161  return new ArrayExpr(ctx, obj);
2162  case Z3_DATATYPE_SORT:
2163  return new DatatypeExpr(ctx, obj);
2165  return new FPExpr(ctx, obj);
2166  case Z3_ROUNDING_MODE_SORT:
2167  return new FPRMExpr(ctx, obj);
2168  case Z3_FINITE_DOMAIN_SORT:
2169  return new FiniteDomainExpr(ctx, obj);
2170  case Z3_SEQ_SORT:
2171  return new SeqExpr(ctx, obj);
2172  case Z3_RE_SORT:
2173  return new ReExpr(ctx, obj);
2174  default: ;
2175  }
2176 
2177  return new Expr(ctx, obj);
2178  }
2179 }
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR
Z3_OP_PR_TRANSITIVITY_STAR
Definition: Z3_decl_kind.java:126
com.microsoft.z3.Native.getAppArg
static long getAppArg(long a0, long a1, int a2)
Definition: Native.java:3064
com.microsoft.z3.Expr.isLE
boolean isLE()
Definition: Expr.java:440
com.microsoft.z3.Native.getSortKind
static int getSortKind(long a0, long a1)
Definition: Native.java:2695
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_SELECT
Z3_OP_RA_SELECT
Definition: Z3_decl_kind.java:171
com.microsoft.z3.Expr.isTrue
boolean isTrue()
Definition: Expr.java:298
com.microsoft.z3.Expr.isConst
boolean isConst()
Definition: Expr.java:246
com.microsoft.z3.Expr.isBVToInt
boolean isBVToInt()
Definition: Expr.java:1220
com.microsoft.z3.Expr.isRatNum
boolean isRatNum()
Definition: Expr.java:266
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_MAP
Z3_OP_ARRAY_MAP
Definition: Z3_decl_kind.java:47
com.microsoft.z3.Expr.isIDiv
boolean isIDiv()
Definition: Expr.java:530
com.microsoft.z3.Expr.isFiniteDomain
boolean isFiniteDomain()
Definition: Expr.java:2047
com.microsoft.z3.Expr.isArrayMap
boolean isArrayMap()
Definition: Expr.java:648
com.microsoft.z3.Native.getString
static String getString(long a0, long a1)
Definition: Native.java:2191
com.microsoft.z3.Expr.isProofQuantIntro
boolean isProofQuantIntro()
Definition: Expr.java:1455
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_NOT
Z3_OP_NOT
Definition: Z3_decl_kind.java:23
com.microsoft.z3.Expr.isBVAdd
boolean isBVAdd()
Definition: Expr.java:771
com.microsoft.z3.Expr.isProofIFFTrue
boolean isProofIFFTrue()
Definition: Expr.java:1654
com.microsoft.z3.Expr.isDistinct
boolean isDistinct()
Definition: Expr.java:329
com.microsoft.z3.Expr.isProofApplyDef
boolean isProofApplyDef()
Definition: Expr.java:1744
com.microsoft.z3.Params
Definition: Params.java:24
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TO_REAL
Z3_OP_TO_REAL
Definition: Z3_decl_kind.java:40
com.microsoft.z3.Expr.isDefaultArray
boolean isDefaultArray()
Definition: Expr.java:636
com.microsoft.z3.Expr.isBVAND
boolean isBVAND()
Definition: Expr.java:982
com.microsoft.z3.Expr.isAsArray
boolean isAsArray()
Definition: Expr.java:659
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNOT
Z3_OP_BNOT
Definition: Z3_decl_kind.java:85
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.Expr.isArithmeticNumeral
boolean isArithmeticNumeral()
Definition: Expr.java:430
com.microsoft.z3.Expr.isBVSGE
boolean isBVSGE()
Definition: Expr.java:932
com.microsoft.z3.Expr.isProofAndElimination
boolean isProofAndElimination()
Definition: Expr.java:1485
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BREDAND
Z3_OP_BREDAND
Definition: Z3_decl_kind.java:96
com.microsoft.z3.Native.updateTerm
static long updateTerm(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3478
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PUSH_QUANT
Z3_OP_PR_PUSH_QUANT
Definition: Z3_decl_kind.java:136
Z3_BV_SORT
@ Z3_BV_SORT
Definition: z3_api.h:153
com.microsoft.z3.Expr.isProofTransitivityStar
boolean isProofTransitivityStar()
Definition: Expr.java:1429
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_VAR_AST
Z3_VAR_AST
Definition: Z3_ast_kind.java:16
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IMPLIES
Z3_OP_IMPLIES
Definition: Z3_decl_kind.java:24
com.microsoft.z3.Native.substituteVars
static long substituteVars(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3496
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DEF_AXIOM
Z3_OP_PR_DEF_AXIOM
Definition: Z3_decl_kind.java:146
com.microsoft.z3.Expr.substitute
Expr substitute(Expr[] from, Expr[] to)
Definition: Expr.java:145
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNUM
Z3_OP_BNUM
Definition: Z3_decl_kind.java:58
com.microsoft.z3.Expr.isInt
boolean isInt()
Definition: Expr.java:410
com.microsoft.z3.Expr.isBVSDiv
boolean isBVSDiv()
Definition: Expr.java:801
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_SUBSET
Z3_OP_SET_SUBSET
Definition: Z3_decl_kind.java:53
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:27
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IS_INT
Z3_OP_IS_INT
Definition: Z3_decl_kind.java:42
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_QUANTIFIER_AST
Z3_QUANTIFIER_AST
Definition: Z3_ast_kind.java:17
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TRUE
Z3_OP_TRUE
Definition: Z3_decl_kind.java:14
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_OEQ
Z3_OP_PR_IFF_OEQ
Definition: Z3_decl_kind.java:153
com.microsoft.z3.Expr.isBVULT
boolean isBVULT()
Definition: Expr.java:942
com.microsoft.z3.Native.getAppNumArgs
static int getAppNumArgs(long a0, long a1)
Definition: Native.java:3055
Z3_FINITE_DOMAIN_SORT
@ Z3_FINITE_DOMAIN_SORT
Definition: z3_api.h:157
com.microsoft.z3.Expr.isBVBitOne
boolean isBVBitOne()
Definition: Expr.java:741
com.microsoft.z3.Expr.isBVBitZero
boolean isBVBitZero()
Definition: Expr.java:751
com.microsoft.z3.Expr.isGT
boolean isGT()
Definition: Expr.java:470
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SLEQ
Z3_OP_SLEQ
Definition: Z3_decl_kind.java:76
com.microsoft.z3.Expr.isITE
boolean isITE()
Definition: Expr.java:339
com.microsoft.z3.Native.isAlgebraicNumber
static boolean isAlgebraicNumber(long a0, long a1)
Definition: Native.java:3154
com.microsoft.z3.Sort
Definition: Sort.java:26
com.microsoft.z3.Expr.isBVConcat
boolean isBVConcat()
Definition: Expr.java:1052
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_COMPLEMENT
Z3_OP_RA_COMPLEMENT
Definition: Z3_decl_kind.java:170
com.microsoft.z3.Expr.isProofGoal
boolean isProofGoal()
Definition: Expr.java:1356
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSREM0
Z3_OP_BSREM0
Definition: Z3_decl_kind.java:72
com.microsoft.z3.Expr.isNot
boolean isNot()
Definition: Expr.java:390
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD
Z3_OP_BSMOD
Definition: Z3_decl_kind.java:69
com.microsoft.z3.Expr.isBVSLE
boolean isBVSLE()
Definition: Expr.java:911
com.microsoft.z3.Expr.isEq
boolean isEq()
Definition: Expr.java:318
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_TRUE
Z3_OP_PR_IFF_TRUE
Definition: Z3_decl_kind.java:143
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ITE
Z3_OP_ITE
Definition: Z3_decl_kind.java:18
com.microsoft.z3.Expr.isString
boolean isString()
Definition: Expr.java:1277
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS
Z3_OP_PR_ELIM_UNUSED_VARS
Definition: Z3_decl_kind.java:137
com.microsoft.z3.Expr.isUMinus
boolean isUMinus()
Definition: Expr.java:500
com.microsoft.z3.enumerations.Z3_sort_kind.Z3_INT_SORT
Z3_INT_SORT
Definition: Z3_sort_kind.java:16
com.microsoft.z3.FuncDecl.getDomainSize
int getDomainSize()
Definition: FuncDecl.java:86
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT
Z3_OP_EXT_ROTATE_LEFT
Definition: Z3_decl_kind.java:103
com.microsoft.z3.enumerations.Z3_lbool.fromInt
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
com.microsoft.z3.Expr.isXor
boolean isXor()
Definition: Expr.java:380
com.microsoft.z3.Native.isWellSorted
static boolean isWellSorted(long a0, long a1)
Definition: Native.java:3109
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MODUS_PONENS
Z3_OP_PR_MODUS_PONENS
Definition: Z3_decl_kind.java:122
com.microsoft.z3.Expr.isRelationFilter
boolean isRelationFilter()
Definition: Expr.java:1965
com.microsoft.z3.Expr.isProofDefIntro
boolean isProofDefIntro()
Definition: Expr.java:1732
com.microsoft
com.microsoft.z3.Expr.isWellSorted
boolean isWellSorted()
Definition: Expr.java:225
com.microsoft.z3.Expr.isSub
boolean isSub()
Definition: Expr.java:490
com.microsoft.z3.Expr.isLabel
boolean isLabel()
Definition: Expr.java:1255
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_HYPOTHESIS
Z3_OP_PR_HYPOTHESIS
Definition: Z3_decl_kind.java:140
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BXNOR
Z3_OP_BXNOR
Definition: Z3_decl_kind.java:89
com.microsoft.z3.Expr.isRelation
boolean isRelation()
Definition: Expr.java:1866
com.microsoft.z3.Expr.isBVSRem
boolean isBVSRem()
Definition: Expr.java:821
com.microsoft.z3.Expr.isSetComplement
boolean isSetComplement()
Definition: Expr.java:699
com.microsoft.z3.Expr.isProofPushQuant
boolean isProofPushQuant()
Definition: Expr.java:1559
com.microsoft.z3.Native.isNumeralAst
static boolean isNumeralAst(long a0, long a1)
Definition: Native.java:3145
com.microsoft.z3.Expr.isStore
boolean isStore()
Definition: Expr.java:604
com.microsoft.z3.Expr.isProofTransitivity
boolean isProofTransitivity()
Definition: Expr.java:1409
com.microsoft.z3.Native.simplify
static long simplify(long a0, long a1)
Definition: Native.java:3442
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_RENAME
Z3_OP_RA_RENAME
Definition: Z3_decl_kind.java:169
com.microsoft.z3.Expr.isProofDER
boolean isProofDER()
Definition: Expr.java:1591
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BXOR
Z3_OP_BXOR
Definition: Z3_decl_kind.java:86
com.microsoft.z3.enumerations.Z3_sort_kind.Z3_BV_SORT
Z3_BV_SORT
Definition: Z3_sort_kind.java:18
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LABEL
Z3_OP_LABEL
Definition: Z3_decl_kind.java:203
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONCAT
Z3_OP_CONCAT
Definition: Z3_decl_kind.java:90
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER
Z3_OP_RA_NEGATION_FILTER
Definition: Z3_decl_kind.java:168
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_INT2BV
Z3_OP_INT2BV
Definition: Z3_decl_kind.java:106
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LT
Z3_OP_LT
Definition: Z3_decl_kind.java:30
com.microsoft.z3.enumerations.Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
Z3_FINITE_DOMAIN_SORT
Definition: Z3_sort_kind.java:22
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT0
Z3_OP_BIT0
Definition: Z3_decl_kind.java:60
com.microsoft.z3.Expr.isOr
boolean isOr()
Definition: Expr.java:359
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BV2INT
Z3_OP_BV2INT
Definition: Z3_decl_kind.java:107
com.microsoft.z3.Expr.isImplies
boolean isImplies()
Definition: Expr.java:400
com.microsoft.z3.Expr.isBVZeroExtension
boolean isBVZeroExtension()
Definition: Expr.java:1072
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONST_ARRAY
Z3_OP_CONST_ARRAY
Definition: Z3_decl_kind.java:46
com.microsoft.z3.Expr.isBVRotateLeftExtended
boolean isBVRotateLeftExtended()
Definition: Expr.java:1184
com.microsoft.z3.Expr.isRemainder
boolean isRemainder()
Definition: Expr.java:540
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRANSITIVITY
Z3_OP_PR_TRANSITIVITY
Definition: Z3_decl_kind.java:125
com.microsoft.z3.Expr.isIntToBV
boolean isIntToBV()
Definition: Expr.java:1208
com.microsoft.z3.Expr.isBVSLT
boolean isBVSLT()
Definition: Expr.java:952
com.microsoft.z3.Expr.isConcat
boolean isConcat()
Definition: Expr.java:1313
com.microsoft.z3.Expr.isProofSkolemize
boolean isProofSkolemize()
Definition: Expr.java:1821
com.microsoft.z3.Expr.isProofIFFOEQ
boolean isProofIFFOEQ()
Definition: Expr.java:1756
com.microsoft.z3.enumerations.Z3_decl_kind
Definition: Z3_decl_kind.java:13
com.microsoft.z3.Expr.isAdd
boolean isAdd()
Definition: Expr.java:480
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNAND
Z3_OP_BNAND
Definition: Z3_decl_kind.java:87
com.microsoft.z3.Expr.isBVShiftRightLogical
boolean isBVShiftRightLogical()
Definition: Expr.java:1142
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY
Z3_OP_PR_COMMUTATIVITY
Definition: Z3_decl_kind.java:145
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LE
Z3_OP_LE
Definition: Z3_decl_kind.java:28
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRUE
Z3_OP_PR_TRUE
Definition: Z3_decl_kind.java:119
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ROTATE_RIGHT
Z3_OP_ROTATE_RIGHT
Definition: Z3_decl_kind.java:102
com.microsoft.z3.Expr.isProofAsserted
boolean isProofAsserted()
Definition: Expr.java:1345
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_DIFFERENCE
Z3_OP_SET_DIFFERENCE
Definition: Z3_decl_kind.java:51
com.microsoft.z3.Expr.isSelect
boolean isSelect()
Definition: Expr.java:614
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_JOIN
Z3_OP_RA_JOIN
Definition: Z3_decl_kind.java:163
com.microsoft.z3.Expr.isBVUDiv
boolean isBVUDiv()
Definition: Expr.java:811
Z3_ARRAY_SORT
@ Z3_ARRAY_SORT
Definition: z3_api.h:154
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_QUANT_INST
Z3_OP_PR_QUANT_INST
Definition: Z3_decl_kind.java:139
com.microsoft.z3.Expr.isMul
boolean isMul()
Definition: Expr.java:510
com.microsoft.z3.Expr.isProofModusPonens
boolean isProofModusPonens()
Definition: Expr.java:1370
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_OR
Z3_OP_OR
Definition: Z3_decl_kind.java:20
com.microsoft.z3.Expr.isBVReduceAND
boolean isBVReduceAND()
Definition: Expr.java:1112
com.microsoft.z3.Expr.isProofRewrite
boolean isProofRewrite()
Definition: Expr.java:1516
com.microsoft.z3.Expr.isAlgebraicNumber
boolean isAlgebraicNumber()
Definition: Expr.java:276
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BASHR
Z3_OP_BASHR
Definition: Z3_decl_kind.java:100
com.microsoft.z3.Expr.isProofIFFFalse
boolean isProofIFFFalse()
Definition: Expr.java:1666
com.microsoft.z3.Expr.isRelationRename
boolean isRelationRename()
Definition: Expr.java:1997
com.microsoft.z3.Native.getSort
static long getSort(long a0, long a1)
Definition: Native.java:3100
com.microsoft.z3.Expr.isBVSMod
boolean isBVSMod()
Definition: Expr.java:841
com.microsoft.z3.Expr.isProofMonotonicity
boolean isProofMonotonicity()
Definition: Expr.java:1444
com.microsoft.z3.Expr.update
Expr update(Expr[] args)
Definition: Expr.java:123
com.microsoft.z3.Expr.isBVRotateRight
boolean isBVRotateRight()
Definition: Expr.java:1172
com.microsoft.z3.Expr.isEmptyRelation
boolean isEmptyRelation()
Definition: Expr.java:1893
com.microsoft.z3.Expr.isSetDifference
boolean isSetDifference()
Definition: Expr.java:689
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_REM
Z3_OP_REM
Definition: Z3_decl_kind.java:38
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT1
Z3_OP_BIT1
Definition: Z3_decl_kind.java:59
com.microsoft.z3.Expr.isRelationProject
boolean isRelationProject()
Definition: Expr.java:1950
com.microsoft.z3.Expr.isGE
boolean isGE()
Definition: Expr.java:450
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UGT
Z3_OP_UGT
Definition: Z3_decl_kind.java:81
com.microsoft.z3.Expr.isRelationClone
boolean isRelationClone()
Definition: Expr.java:2037
com.microsoft.z3.Expr.isRelationalJoin
boolean isRelationalJoin()
Definition: Expr.java:1913
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CARRY
Z3_OP_CARRY
Definition: Z3_decl_kind.java:108
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_MOD
Z3_OP_MOD
Definition: Z3_decl_kind.java:39
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TH_LEMMA
Z3_OP_PR_TH_LEMMA
Definition: Z3_decl_kind.java:158
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PULL_QUANT
Z3_OP_PR_PULL_QUANT
Definition: Z3_decl_kind.java:135
com.microsoft.z3.Expr.isBVUGT
boolean isBVUGT()
Definition: Expr.java:962
com.microsoft.z3.Expr.isProofElimUnusedVars
boolean isProofElimUnusedVars()
Definition: Expr.java:1575
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_REPEAT
Z3_OP_REPEAT
Definition: Z3_decl_kind.java:94
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_NEG
Z3_OP_PR_NNF_NEG
Definition: Z3_decl_kind.java:155
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IDIV
Z3_OP_IDIV
Definition: Z3_decl_kind.java:37
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_MUL
Z3_OP_MUL
Definition: Z3_decl_kind.java:35
com.microsoft.z3.Expr.isSetIntersect
boolean isSetIntersect()
Definition: Expr.java:679
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_SYMMETRY
Z3_OP_PR_SYMMETRY
Definition: Z3_decl_kind.java:124
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DEF_INTRO
Z3_OP_PR_DEF_INTRO
Definition: Z3_decl_kind.java:151
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_GT
Z3_OP_GT
Definition: Z3_decl_kind.java:31
com.microsoft.z3.Expr.isLT
boolean isLT()
Definition: Expr.java:460
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:147
com.microsoft.z3.Expr.isProofOrElimination
boolean isProofOrElimination()
Definition: Expr.java:1496
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNOR
Z3_OP_BNOR
Definition: Z3_decl_kind.java:88
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_UNION
Z3_OP_SET_UNION
Definition: Z3_decl_kind.java:49
com.microsoft.z3.Expr.isBool
boolean isBool()
Definition: Expr.java:286
com.microsoft.z3.Expr.isBVComp
boolean isBVComp()
Definition: Expr.java:1122
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSREM
Z3_OP_BSREM
Definition: Z3_decl_kind.java:67
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM
Z3_OP_BUREM
Definition: Z3_decl_kind.java:68
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_CLONE
Z3_OP_RA_CLONE
Definition: Z3_decl_kind.java:172
com.microsoft.z3.Expr.isModulus
boolean isModulus()
Definition: Expr.java:550
com.microsoft.z3.Expr.translate
Expr translate(Context ctx)
Definition: Expr.java:195
com.microsoft.z3.Expr.isProofModusPonensOEQ
boolean isProofModusPonensOEQ()
Definition: Expr.java:1834
com.microsoft.z3.Native.mkBoolSort
static long mkBoolSort(long a0)
Definition: Native.java:954
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_POS
Z3_OP_PR_NNF_POS
Definition: Z3_decl_kind.java:154
com.microsoft.z3.Expr.isRealToInt
boolean isRealToInt()
Definition: Expr.java:570
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSUB
Z3_OP_BSUB
Definition: Z3_decl_kind.java:63
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_IS_EMPTY
Z3_OP_RA_IS_EMPTY
Definition: Z3_decl_kind.java:162
com.microsoft.z3.Native.getAppDecl
static long getAppDecl(long a0, long a1)
Definition: Native.java:3046
com.microsoft.z3.Native.getBoolValue
static int getBoolValue(long a0, long a1)
Definition: Native.java:3118
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_COMPLEMENT
Z3_OP_SET_COMPLEMENT
Definition: Z3_decl_kind.java:52
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ADD
Z3_OP_ADD
Definition: Z3_decl_kind.java:32
Z3_REAL_SORT
@ Z3_REAL_SORT
Definition: z3_api.h:152
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ULT
Z3_OP_ULT
Definition: Z3_decl_kind.java:79
com.microsoft.z3.Expr.isBVNAND
boolean isBVNAND()
Definition: Expr.java:1022
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Expr.substitute
Expr substitute(Expr from, Expr to)
Definition: Expr.java:164
com.microsoft.z3.Expr.isBVReduceOR
boolean isBVReduceOR()
Definition: Expr.java:1102
Z3_FLOATING_POINT_SORT
@ Z3_FLOATING_POINT_SORT
Definition: z3_api.h:158
com.microsoft.z3.Expr.isProofLemma
boolean isProofLemma()
Definition: Expr.java:1631
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD0
Z3_OP_BSMOD0
Definition: Z3_decl_kind.java:74
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ZERO_EXT
Z3_OP_ZERO_EXT
Definition: Z3_decl_kind.java:92
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_GOAL
Z3_OP_PR_GOAL
Definition: Z3_decl_kind.java:121
Z3_INT_SORT
@ Z3_INT_SORT
Definition: z3_api.h:151
com.microsoft.z3.Expr.isBVXOR
boolean isBVXOR()
Definition: Expr.java:1012
com.microsoft.z3.Expr.isDiv
boolean isDiv()
Definition: Expr.java:520
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SIGN_EXT
Z3_OP_SIGN_EXT
Definition: Z3_decl_kind.java:91
com.microsoft.z3.Native.simplifyEx
static long simplifyEx(long a0, long a1, long a2)
Definition: Native.java:3451
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV0
Z3_OP_BUDIV0
Definition: Z3_decl_kind.java:71
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BREDOR
Z3_OP_BREDOR
Definition: Z3_decl_kind.java:95
com.microsoft.z3.Expr.toString
String toString()
Definition: Expr.java:204
com.microsoft.z3.Expr.getIndex
int getIndex()
Definition: Expr.java:2083
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BLSHR
Z3_OP_BLSHR
Definition: Z3_decl_kind.java:99
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REWRITE
Z3_OP_PR_REWRITE
Definition: Z3_decl_kind.java:133
com.microsoft.z3.Expr.isBVSignExtension
boolean isBVSignExtension()
Definition: Expr.java:1062
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_UNION
Z3_OP_RA_UNION
Definition: Z3_decl_kind.java:164
Z3_RE_SORT
@ Z3_RE_SORT
Definition: z3_api.h:161
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EQ
Z3_OP_EQ
Definition: Z3_decl_kind.java:16
com.microsoft.z3.Expr.getArgs
Expr[] getArgs()
Definition: Expr.java:105
com.microsoft.z3.Expr.isProofQuantInst
boolean isProofQuantInst()
Definition: Expr.java:1603
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION
Z3_OP_PR_UNIT_RESOLUTION
Definition: Z3_decl_kind.java:142
com.microsoft.z3.Expr.isRealIsInt
boolean isRealIsInt()
Definition: Expr.java:581
com.microsoft.z3.Expr.isIntToReal
boolean isIntToReal()
Definition: Expr.java:560
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_WIDEN
Z3_OP_RA_WIDEN
Definition: Z3_decl_kind.java:165
com.microsoft.z3.Expr.isSetSubset
boolean isSetSubset()
Definition: Expr.java:709
com.microsoft.z3.Expr.isBVCarry
boolean isBVCarry()
Definition: Expr.java:1231
com.microsoft.z3.enumerations.Z3_ast_kind
Definition: Z3_ast_kind.java:13
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MONOTONICITY
Z3_OP_PR_MONOTONICITY
Definition: Z3_decl_kind.java:127
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY
Z3_OP_PR_DISTRIBUTIVITY
Definition: Z3_decl_kind.java:130
com.microsoft.z3.Expr.isBV
boolean isBV()
Definition: Expr.java:719
com.microsoft.z3.Expr.isBVRotateLeft
boolean isBVRotateLeft()
Definition: Expr.java:1162
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSHL
Z3_OP_BSHL
Definition: Z3_decl_kind.java:98
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXTRACT
Z3_OP_EXTRACT
Definition: Z3_decl_kind.java:93
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_XOR3
Z3_OP_XOR3
Definition: Z3_decl_kind.java:109
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_FALSE
Z3_OP_PR_IFF_FALSE
Definition: Z3_decl_kind.java:144
com.microsoft.z3.Expr.isProofUnitResolution
boolean isProofUnitResolution()
Definition: Expr.java:1642
com.microsoft.z3.Expr.isBVSub
boolean isBVSub()
Definition: Expr.java:781
com.microsoft.z3.Expr
Definition: Expr.java:30
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_STORE
Z3_OP_RA_STORE
Definition: Z3_decl_kind.java:160
com.microsoft.z3.Expr.simplify
Expr simplify()
Definition: Expr.java:37
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BADD
Z3_OP_BADD
Definition: Z3_decl_kind.java:62
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REFLEXIVITY
Z3_OP_PR_REFLEXIVITY
Definition: Z3_decl_kind.java:123
com.microsoft.z3.Expr.simplify
Expr simplify(Params p)
Definition: Expr.java:51
com.microsoft.z3.Expr.isFiniteDomainLT
boolean isFiniteDomainLT()
Definition: Expr.java:2060
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:25
com.microsoft.z3.Native.isString
static boolean isString(long a0, long a1)
Definition: Native.java:2182
com.microsoft.z3.Native.getAstKind
static int getAstKind(long a0, long a1)
Definition: Native.java:3127
com.microsoft.z3.AST
Definition: AST.java:25
com.microsoft.z3.Expr.isIsEmptyRelation
boolean isIsEmptyRelation()
Definition: Expr.java:1903
com.microsoft.z3.Expr.isBVExtract
boolean isBVExtract()
Definition: Expr.java:1082
com.microsoft.z3.Expr.isProofReflexivity
boolean isProofReflexivity()
Definition: Expr.java:1385
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_FILTER
Z3_OP_RA_FILTER
Definition: Z3_decl_kind.java:167
com.microsoft.z3.Expr.isProofCommutativity
boolean isProofCommutativity()
Definition: Expr.java:1683
com.microsoft.z3.enumerations.Z3_lbool
Definition: Z3_lbool.java:13
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REWRITE_STAR
Z3_OP_PR_REWRITE_STAR
Definition: Z3_decl_kind.java:134
com.microsoft.z3.Expr.isBVShiftLeft
boolean isBVShiftLeft()
Definition: Expr.java:1132
com.microsoft.z3.Expr.isBVNOT
boolean isBVNOT()
Definition: Expr.java:1002
com.microsoft.z3.Expr.getBoolValue
Z3_lbool getBoolValue()
Definition: Expr.java:84
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BOR
Z3_OP_BOR
Definition: Z3_decl_kind.java:84
com.microsoft.z3.Expr.isRelationNegationFilter
boolean isRelationNegationFilter()
Definition: Expr.java:1985
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ANUM
Z3_OP_ANUM
Definition: Z3_decl_kind.java:26
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ULEQ
Z3_OP_ULEQ
Definition: Z3_decl_kind.java:75
com.microsoft.z3.Expr.isRelationUnion
boolean isRelationUnion()
Definition: Expr.java:1925
com.microsoft.z3.Expr.isBVXNOR
boolean isBVXNOR()
Definition: Expr.java:1042
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UGEQ
Z3_OP_UGEQ
Definition: Z3_decl_kind.java:77
com.microsoft.z3.Expr.isProofNNFPos
boolean isProofNNFPos()
Definition: Expr.java:1784
com.microsoft.z3.Expr.isRelationComplement
boolean isRelationComplement()
Definition: Expr.java:2007
com.microsoft.z3.Expr.Expr
Expr(Context ctx, long obj)
Definition: Expr.java:2096
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DIV
Z3_OP_DIV
Definition: Z3_decl_kind.java:36
com.microsoft.z3.Expr.isProofPullQuant
boolean isProofPullQuant()
Definition: Expr.java:1544
com.microsoft.z3.Expr.isRelationStore
boolean isRelationStore()
Definition: Expr.java:1883
com.microsoft.z3.Native.getIndexValue
static int getIndexValue(long a0, long a1)
Definition: Native.java:3325
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SGT
Z3_OP_SGT
Definition: Z3_decl_kind.java:82
Z3_BOOL_SORT
@ Z3_BOOL_SORT
Definition: z3_api.h:150
com.microsoft.z3.Expr.isAnd
boolean isAnd()
Definition: Expr.java:349
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SLT
Z3_OP_SLT
Definition: Z3_decl_kind.java:80
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_AND_ELIM
Z3_OP_PR_AND_ELIM
Definition: Z3_decl_kind.java:131
com.microsoft.z3.Expr.isIntNum
boolean isIntNum()
Definition: Expr.java:256
com.microsoft.z3.Expr.isProofTrue
boolean isProofTrue()
Definition: Expr.java:1335
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UMINUS
Z3_OP_UMINUS
Definition: Z3_decl_kind.java:34
com.microsoft.z3.Native.isApp
static boolean isApp(long a0, long a1)
Definition: Native.java:3136
com.microsoft.z3.Expr.isBVNumeral
boolean isBVNumeral()
Definition: Expr.java:731
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT
Z3_OP_EXT_ROTATE_RIGHT
Definition: Z3_decl_kind.java:104
com.microsoft.z3.Expr.isIff
boolean isIff()
Definition: Expr.java:370
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM0
Z3_OP_BUREM0
Definition: Z3_decl_kind.java:73
com.microsoft.z3.Expr.isProofDistributivity
boolean isProofDistributivity()
Definition: Expr.java:1474
com.microsoft.z3.Expr.isBVShiftRightArithmetic
boolean isBVShiftRightArithmetic()
Definition: Expr.java:1152
com
com.microsoft.z3.Expr.isArray
boolean isArray()
Definition: Expr.java:591
com.microsoft.z3.Expr.getFuncDecl
FuncDecl getFuncDecl()
Definition: Expr.java:72
com.microsoft.z3.Expr.isBVMul
boolean isBVMul()
Definition: Expr.java:791
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV0
Z3_OP_BSDIV0
Definition: Z3_decl_kind.java:70
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TO_INT
Z3_OP_TO_INT
Definition: Z3_decl_kind.java:41
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LABEL_LIT
Z3_OP_LABEL_LIT
Definition: Z3_decl_kind.java:204
com.microsoft.z3.Expr.isBVRotateRightExtended
boolean isBVRotateRightExtended()
Definition: Expr.java:1196
com.microsoft.z3.Expr.isProofSymmetry
boolean isProofSymmetry()
Definition: Expr.java:1397
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNEG
Z3_OP_BNEG
Definition: Z3_decl_kind.java:61
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AS_ARRAY
Z3_OP_AS_ARRAY
Definition: Z3_decl_kind.java:54
com.microsoft.z3.Expr.isBVUGE
boolean isBVUGE()
Definition: Expr.java:922
com.microsoft.z3.Expr.isBVULE
boolean isBVULE()
Definition: Expr.java:901
com.microsoft.z3.Expr.getSort
Sort getSort()
Definition: Expr.java:235
com.microsoft.z3.Expr.isOEQ
boolean isOEQ()
Definition: Expr.java:1325
com.microsoft.z3.Expr.isProofHypothesis
boolean isProofHypothesis()
Definition: Expr.java:1615
com.microsoft.z3.enumerations.Z3_sort_kind
Definition: Z3_sort_kind.java:13
com.microsoft.z3.Expr.isProofNNFNeg
boolean isProofNNFNeg()
Definition: Expr.java:1803
com.microsoft.z3.FuncDecl.getDeclKind
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:119
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_CONCAT
Z3_OP_SEQ_CONCAT
Definition: Z3_decl_kind.java:177
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_OEQ
Z3_OP_OEQ
Definition: Z3_decl_kind.java:25
com.microsoft.z3.Expr.isBVSGT
boolean isBVSGT()
Definition: Expr.java:972
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_SKOLEMIZE
Z3_OP_PR_SKOLEMIZE
Definition: Z3_decl_kind.java:156
com.microsoft.z3.Expr.isBVURem
boolean isBVURem()
Definition: Expr.java:831
com.microsoft.z3.Expr.getString
String getString()
Definition: Expr.java:1288
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.AST.isExpr
boolean isExpr()
Definition: AST.java:112
com.microsoft.z3.Expr.isSetUnion
boolean isSetUnion()
Definition: Expr.java:669
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SUB
Z3_OP_SUB
Definition: Z3_decl_kind.java:33
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BMUL
Z3_OP_BMUL
Definition: Z3_decl_kind.java:64
com.microsoft.z3.enumerations.Z3_sort_kind.Z3_REAL_SORT
Z3_REAL_SORT
Definition: Z3_sort_kind.java:17
com.microsoft.z3.enumerations.Z3_sort_kind.Z3_ARRAY_SORT
Z3_ARRAY_SORT
Definition: Z3_sort_kind.java:19
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ROTATE_LEFT
Z3_OP_ROTATE_LEFT
Definition: Z3_decl_kind.java:101
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SGEQ
Z3_OP_SGEQ
Definition: Z3_decl_kind.java:78
com.microsoft.z3.Native.substitute
static long substitute(long a0, long a1, int a2, long[] a3, long[] a4)
Definition: Native.java:3487
com.microsoft.z3.Expr.isLabelLit
boolean isLabelLit()
Definition: Expr.java:1268
Z3_ast_kind
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:177
com.microsoft.z3.Expr.isProofRewriteStar
boolean isProofRewriteStar()
Definition: Expr.java:1532
com.microsoft.z3.Expr.isNumeral
boolean isNumeral()
Definition: Expr.java:214
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SELECT
Z3_OP_SELECT
Definition: Z3_decl_kind.java:45
com.microsoft.z3.Expr.isFalse
boolean isFalse()
Definition: Expr.java:308
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_INTERSECT
Z3_OP_SET_INTERSECT
Definition: Z3_decl_kind.java:50
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BAND
Z3_OP_BAND
Definition: Z3_decl_kind.java:83
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DER
Z3_OP_PR_DER
Definition: Z3_decl_kind.java:138
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_APPLY_DEF
Z3_OP_PR_APPLY_DEF
Definition: Z3_decl_kind.java:152
com.microsoft.z3.AST.isApp
boolean isApp()
Definition: AST.java:131
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_PROJECT
Z3_OP_RA_PROJECT
Definition: Z3_decl_kind.java:166
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV
Z3_OP_BUDIV
Definition: Z3_decl_kind.java:66
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_DEFAULT
Z3_OP_ARRAY_DEFAULT
Definition: Z3_decl_kind.java:48
Z3_SEQ_SORT
@ Z3_SEQ_SORT
Definition: z3_api.h:160
com.microsoft.z3.Expr.isProofTheoryLemma
boolean isProofTheoryLemma()
Definition: Expr.java:1856
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_EMPTY
Z3_OP_RA_EMPTY
Definition: Z3_decl_kind.java:161
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_QUANT_INTRO
Z3_OP_PR_QUANT_INTRO
Definition: Z3_decl_kind.java:128
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV
Z3_OP_BSDIV
Definition: Z3_decl_kind.java:65
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FD_LT
Z3_OP_FD_LT
Definition: Z3_decl_kind.java:174
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DISTINCT
Z3_OP_DISTINCT
Definition: Z3_decl_kind.java:17
com.microsoft.z3.Expr.isBVUMinus
boolean isBVUMinus()
Definition: Expr.java:761
Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1007
com.microsoft.z3.Expr.isBVXOR3
boolean isBVXOR3()
Definition: Expr.java:1242
com.microsoft.z3.Expr.isReal
boolean isReal()
Definition: Expr.java:420
com.microsoft.z3.Expr.isBVOR
boolean isBVOR()
Definition: Expr.java:992
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AND
Z3_OP_AND
Definition: Z3_decl_kind.java:19
com.microsoft.z3.AST.isVar
boolean isVar()
Definition: AST.java:141
Z3_DATATYPE_SORT
@ Z3_DATATYPE_SORT
Definition: z3_api.h:155
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_STORE
Z3_OP_STORE
Definition: Z3_decl_kind.java:44
com.microsoft.z3.Expr.isBVNOR
boolean isBVNOR()
Definition: Expr.java:1032
com.microsoft.z3.enumerations.Z3_sort_kind.Z3_RELATION_SORT
Z3_RELATION_SORT
Definition: Z3_sort_kind.java:21
com.microsoft.z3.Expr.isConstantArray
boolean isConstantArray()
Definition: Expr.java:625
com.microsoft.z3.Expr.substituteVars
Expr substituteVars(Expr[] to)
Definition: Expr.java:179
com.microsoft.z3.Expr.getNumArgs
int getNumArgs()
Definition: Expr.java:95
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ
Z3_OP_PR_MODUS_PONENS_OEQ
Definition: Z3_decl_kind.java:157
com.microsoft.z3.Expr.isBVRepeat
boolean isBVRepeat()
Definition: Expr.java:1092
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM
Z3_OP_PR_NOT_OR_ELIM
Definition: Z3_decl_kind.java:132
com.microsoft.z3.Expr.isProofDefAxiom
boolean isProofDefAxiom()
Definition: Expr.java:1709
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ASSERTED
Z3_OP_PR_ASSERTED
Definition: Z3_decl_kind.java:120
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BCOMP
Z3_OP_BCOMP
Definition: Z3_decl_kind.java:97
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_LEMMA
Z3_OP_PR_LEMMA
Definition: Z3_decl_kind.java:141
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_GE
Z3_OP_GE
Definition: Z3_decl_kind.java:29
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FALSE
Z3_OP_FALSE
Definition: Z3_decl_kind.java:15
com.microsoft.z3.Expr.isRelationWiden
boolean isRelationWiden()
Definition: Expr.java:1937
com.microsoft.z3.Expr.isRelationSelect
boolean isRelationSelect()
Definition: Expr.java:2021
com.microsoft.z3.Native.isEqSort
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:2686
Z3_ROUNDING_MODE_SORT
@ Z3_ROUNDING_MODE_SORT
Definition: z3_api.h:159
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_XOR
Z3_OP_XOR
Definition: Z3_decl_kind.java:22
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IFF
Z3_OP_IFF
Definition: Z3_decl_kind.java:21