18package com.microsoft.z3;
20import static com.microsoft.z3.Constructor.of;
22import com.microsoft.z3.enumerations.Z3_ast_print_mode;
35@SuppressWarnings(
"unchecked")
38 static final Object creation_lock =
new Object();
41 synchronized (creation_lock) {
42 m_ctx = Native.mkContextRc(0);
48 synchronized (creation_lock) {
72 public Context(Map<String, String> settings) {
73 synchronized (creation_lock) {
74 long cfg = Native.mkConfig();
76 Native.setParamValue(cfg, kv.getKey(), kv.getValue());
78 m_ctx = Native.mkContextRc(cfg);
79 Native.delConfig(cfg);
86 Native.setInternalErrorHandler(m_ctx);
115 for (
int i = 0; i < names.length; ++i)
116 result[i] = mkSymbol(names[i]);
121 private IntSort m_intSort =
null;
123 private SeqSort<BitVecSort> m_stringSort =
null;
130 if (m_boolSort ==
null) {
141 if (m_intSort ==
null) {
152 if (m_realSort ==
null) {
171 if (m_stringSort ==
null) {
172 m_stringSort = mkStringSort();
182 checkContextMatch(s);
191 return mkUninterpretedSort(mkSymbol(str));
215 return new BitVecSort(
this, Native.mkBvSort(nCtx(), size));
223 checkContextMatch(domain);
224 checkContextMatch(
range);
232 public <R extends Sort> ArraySort<Sort, R> mkArraySort(Sort[] domains, R
range)
234 checkContextMatch(domains);
235 checkContextMatch(
range);
236 return new ArraySort<>(
this, domains,
range);
244 return new SeqSort<>(
this, Native.mkStringSort(nCtx()));
250 public <R extends Sort>
SeqSort<R> mkSeqSort(R s)
252 return new SeqSort<>(
this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
258 public <R extends Sort> ReSort<R> mkReSort(R s)
260 return new ReSort<>(
this, Native.mkReSort(nCtx(), s.getNativeObject()));
270 checkContextMatch(name);
271 checkContextMatch(fieldNames);
272 checkContextMatch(fieldSorts);
273 return new TupleSort(
this, name, fieldNames.length, fieldNames,
283 checkContextMatch(name);
284 checkContextMatch(enumNames);
291 public <R> EnumSort<R> mkEnumSort(
String name,
String... enumNames)
294 return new EnumSort<>(
this, mkSymbol(name), mkSymbols(enumNames));
300 public <R extends Sort> ListSort<R> mkListSort(Symbol name, R elemSort)
302 checkContextMatch(name);
303 checkContextMatch(elemSort);
304 return new ListSort<>(
this, name, elemSort);
310 public <R extends Sort> ListSort<R> mkListSort(
String name, R elemSort)
312 checkContextMatch(elemSort);
313 return new ListSort<>(
this, mkSymbol(name), elemSort);
319 public <R> FiniteDomainSort<R> mkFiniteDomainSort(Symbol name,
long size)
322 checkContextMatch(name);
323 return new FiniteDomainSort<>(
this, name, size);
329 public <R> FiniteDomainSort<R> mkFiniteDomainSort(
String name,
long size)
332 return new FiniteDomainSort<>(
this, mkSymbol(name), size);
346 public <R> Constructor<R> mkConstructor(Symbol name, Symbol recognizer,
347 Symbol[] fieldNames, Sort[] sorts,
int[] sortRefs)
350 return of(
this, name, recognizer, fieldNames, sorts, sortRefs);
356 public <R> Constructor<R> mkConstructor(
String name,
String recognizer,
357 String[] fieldNames, Sort[] sorts,
int[] sortRefs)
359 return of(
this, mkSymbol(name), mkSymbol(recognizer), mkSymbols(fieldNames), sorts, sortRefs);
365 public <R> DatatypeSort<R> mkDatatypeSort(Symbol name, Constructor<R>[] constructors)
367 checkContextMatch(name);
368 checkContextMatch(constructors);
369 return new DatatypeSort<>(
this, name, constructors);
375 public <R> DatatypeSort<R> mkDatatypeSort(
String name, Constructor<R>[] constructors)
378 checkContextMatch(constructors);
379 return new DatatypeSort<>(
this, mkSymbol(name), constructors);
389 checkContextMatch(names);
390 int n = names.length;
392 long[] n_constr =
new long[n];
393 for (
int i = 0; i < n; i++)
397 checkContextMatch(constructor);
399 n_constr[i] = cla[i].getNativeObject();
401 long[] n_res =
new long[n];
405 for (
int i = 0; i < n; i++)
416 return mkDatatypeSorts(mkSymbols(names), c);
429 Native.datatypeUpdateField
430 (nCtx(), field.getNativeObject(),
431 t.getNativeObject(), v.getNativeObject()));
438 public <R extends Sort> FuncDecl<R> mkFuncDecl(Symbol name, Sort[] domain, R
range)
440 checkContextMatch(name);
441 checkContextMatch(domain);
442 checkContextMatch(
range);
443 return new FuncDecl<>(
this, name, domain,
range);
449 public <R extends Sort> FuncDecl<R> mkFuncDecl(Symbol name, Sort domain, R
range)
452 checkContextMatch(name);
453 checkContextMatch(domain);
454 checkContextMatch(
range);
455 Sort[] q =
new Sort[] { domain };
456 return new FuncDecl<>(
this, name, q,
range);
462 public <R extends Sort> FuncDecl<R> mkFuncDecl(
String name, Sort[] domain, R
range)
465 checkContextMatch(domain);
466 checkContextMatch(
range);
467 return new FuncDecl<>(
this, mkSymbol(name), domain,
range);
473 public <R extends Sort> FuncDecl<R> mkFuncDecl(
String name, Sort domain, R
range)
476 checkContextMatch(domain);
477 checkContextMatch(
range);
478 Sort[] q =
new Sort[] { domain };
479 return new FuncDecl<>(
this, mkSymbol(name), q,
range);
485 public <R extends Sort> FuncDecl<R> mkRecFuncDecl(Symbol name, Sort[] domain, R
range)
487 checkContextMatch(name);
488 checkContextMatch(domain);
489 checkContextMatch(
range);
490 return new FuncDecl<>(
this, name, domain,
range,
true);
500 public <R extends Sort>
void AddRecDef(FuncDecl<R> f, Expr<?>[] args, Expr<R> body)
502 checkContextMatch(f);
503 checkContextMatch(args);
504 checkContextMatch(body);
505 long[] argsNative = AST.arrayToNative(args);
506 Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject());
515 public <R extends Sort> FuncDecl<R> mkFreshFuncDecl(
String prefix, Sort[] domain, R
range)
518 checkContextMatch(domain);
519 checkContextMatch(
range);
520 return new FuncDecl<>(
this, prefix, domain,
range);
526 public <R extends Sort> FuncDecl<R> mkConstDecl(Symbol name, R
range)
528 checkContextMatch(name);
529 checkContextMatch(
range);
530 return new FuncDecl<>(
this, name,
null,
range);
536 public <R extends Sort> FuncDecl<R> mkConstDecl(
String name, R
range)
538 checkContextMatch(
range);
539 return new FuncDecl<>(
this, mkSymbol(name),
null,
range);
548 public <R extends Sort> FuncDecl<R> mkFreshConstDecl(
String prefix, R
range)
551 checkContextMatch(
range);
552 return new FuncDecl<>(
this, prefix,
null,
range);
560 public <R extends Sort> Expr<R> mkBound(
int index, R ty)
562 return (Expr<R>) Expr.create(
this,
563 Native.mkBound(nCtx(), index, ty.getNativeObject()));
572 if (terms.length == 0)
573 throw new Z3Exception(
"Cannot create a pattern from zero terms");
576 return new Pattern(
this, Native.mkPattern(nCtx(), terms.length,
586 checkContextMatch(name);
587 checkContextMatch(
range);
591 Native.mkConst(nCtx(), name.getNativeObject(),
592 range.getNativeObject()));
599 public <R extends Sort> Expr<R> mkConst(
String name, R
range)
601 return mkConst(mkSymbol(name),
range);
608 public <R extends Sort> Expr<R> mkFreshConst(
String prefix, R
range)
610 checkContextMatch(
range);
611 return (Expr<R>) Expr.create(
this,
612 Native.mkFreshConst(nCtx(), prefix,
range.getNativeObject()));
619 public <R extends Sort> Expr<R> mkConst(FuncDecl<R> f)
621 return mkApp(f, (Expr<?>[])
null);
629 return (
BoolExpr) mkConst(name, getBoolSort());
637 return (
BoolExpr) mkConst(mkSymbol(name), getBoolSort());
645 return (
IntExpr) mkConst(name, getIntSort());
653 return (
IntExpr) mkConst(name, getIntSort());
661 return (
RealExpr) mkConst(name, getRealSort());
669 return (
RealExpr) mkConst(name, getRealSort());
677 return (
BitVecExpr) mkConst(name, mkBitVecSort(size));
685 return (
BitVecExpr) mkConst(name, mkBitVecSort(size));
694 checkContextMatch(f);
695 checkContextMatch(args);
696 return Expr.create(
this, f, args);
704 return new BoolExpr(
this, Native.mkTrue(nCtx()));
712 return new BoolExpr(
this, Native.mkFalse(nCtx()));
720 return value ? mkTrue() : mkFalse();
728 checkContextMatch(x);
729 checkContextMatch(y);
730 return new BoolExpr(
this, Native.mkEq(nCtx(), x.getNativeObject(),
731 y.getNativeObject()));
740 checkContextMatch(args);
741 return new BoolExpr(
this, Native.mkDistinct(nCtx(), args.length,
750 checkContextMatch(a);
751 return new BoolExpr(
this, Native.mkNot(nCtx(), a.getNativeObject()));
763 checkContextMatch(t1);
764 checkContextMatch(t2);
765 checkContextMatch(t3);
766 return (
Expr<R>)
Expr.create(
this, Native.mkIte(nCtx(), t1.getNativeObject(),
767 t2.getNativeObject(), t3.getNativeObject()));
775 checkContextMatch(t1);
776 checkContextMatch(t2);
777 return new BoolExpr(
this, Native.mkIff(nCtx(), t1.getNativeObject(),
778 t2.getNativeObject()));
786 checkContextMatch(t1);
787 checkContextMatch(t2);
788 return new BoolExpr(
this, Native.mkImplies(nCtx(),
789 t1.getNativeObject(), t2.getNativeObject()));
797 checkContextMatch(t1);
798 checkContextMatch(t2);
799 return new BoolExpr(
this, Native.mkXor(nCtx(), t1.getNativeObject(),
800 t2.getNativeObject()));
809 checkContextMatch(t);
810 return new BoolExpr(
this, Native.mkAnd(nCtx(), t.length,
820 checkContextMatch(t);
821 return new BoolExpr(
this, Native.mkOr(nCtx(), t.length,
831 checkContextMatch(t);
842 checkContextMatch(t);
853 checkContextMatch(t);
863 checkContextMatch(t);
865 Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
871 public <R extends ArithSort> ArithExpr<R> mkDiv(Expr<? extends R> t1, Expr<? extends R> t2)
873 checkContextMatch(t1);
874 checkContextMatch(t2);
875 return (ArithExpr<R>) Expr.create(
this, Native.mkDiv(nCtx(),
876 t1.getNativeObject(), t2.getNativeObject()));
886 checkContextMatch(t1);
887 checkContextMatch(t2);
888 return new IntExpr(
this, Native.mkMod(nCtx(), t1.getNativeObject(),
889 t2.getNativeObject()));
899 checkContextMatch(t1);
900 checkContextMatch(t2);
901 return new IntExpr(
this, Native.mkRem(nCtx(), t1.getNativeObject(),
902 t2.getNativeObject()));
911 checkContextMatch(t1);
912 checkContextMatch(t2);
915 Native.mkPower(nCtx(), t1.getNativeObject(),
916 t2.getNativeObject()));
924 checkContextMatch(t1);
925 checkContextMatch(t2);
926 return new BoolExpr(
this, Native.mkLt(nCtx(), t1.getNativeObject(),
927 t2.getNativeObject()));
935 checkContextMatch(t1);
936 checkContextMatch(t2);
937 return new BoolExpr(
this, Native.mkLe(nCtx(), t1.getNativeObject(),
938 t2.getNativeObject()));
946 checkContextMatch(t1);
947 checkContextMatch(t2);
948 return new BoolExpr(
this, Native.mkGt(nCtx(), t1.getNativeObject(),
949 t2.getNativeObject()));
957 checkContextMatch(t1);
958 checkContextMatch(t2);
959 return new BoolExpr(
this, Native.mkGe(nCtx(), t1.getNativeObject(),
960 t2.getNativeObject()));
975 checkContextMatch(t);
977 Native.mkInt2real(nCtx(), t.getNativeObject()));
988 checkContextMatch(t);
989 return new IntExpr(
this, Native.mkReal2int(nCtx(), t.getNativeObject()));
997 checkContextMatch(t);
998 return new BoolExpr(
this, Native.mkIsInt(nCtx(), t.getNativeObject()));
1008 checkContextMatch(t);
1009 return new BitVecExpr(
this, Native.mkBvnot(nCtx(), t.getNativeObject()));
1019 checkContextMatch(t);
1020 return new BitVecExpr(
this, Native.mkBvredand(nCtx(),
1021 t.getNativeObject()));
1031 checkContextMatch(t);
1032 return new BitVecExpr(
this, Native.mkBvredor(nCtx(),
1033 t.getNativeObject()));
1043 checkContextMatch(t1);
1044 checkContextMatch(t2);
1045 return new BitVecExpr(
this, Native.mkBvand(nCtx(),
1046 t1.getNativeObject(), t2.getNativeObject()));
1056 checkContextMatch(t1);
1057 checkContextMatch(t2);
1058 return new BitVecExpr(
this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1059 t2.getNativeObject()));
1069 checkContextMatch(t1);
1070 checkContextMatch(t2);
1071 return new BitVecExpr(
this, Native.mkBvxor(nCtx(),
1072 t1.getNativeObject(), t2.getNativeObject()));
1082 checkContextMatch(t1);
1083 checkContextMatch(t2);
1084 return new BitVecExpr(
this, Native.mkBvnand(nCtx(),
1085 t1.getNativeObject(), t2.getNativeObject()));
1095 checkContextMatch(t1);
1096 checkContextMatch(t2);
1097 return new BitVecExpr(
this, Native.mkBvnor(nCtx(),
1098 t1.getNativeObject(), t2.getNativeObject()));
1108 checkContextMatch(t1);
1109 checkContextMatch(t2);
1110 return new BitVecExpr(
this, Native.mkBvxnor(nCtx(),
1111 t1.getNativeObject(), t2.getNativeObject()));
1121 checkContextMatch(t);
1122 return new BitVecExpr(
this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1132 checkContextMatch(t1);
1133 checkContextMatch(t2);
1134 return new BitVecExpr(
this, Native.mkBvadd(nCtx(),
1135 t1.getNativeObject(), t2.getNativeObject()));
1145 checkContextMatch(t1);
1146 checkContextMatch(t2);
1147 return new BitVecExpr(
this, Native.mkBvsub(nCtx(),
1148 t1.getNativeObject(), t2.getNativeObject()));
1158 checkContextMatch(t1);
1159 checkContextMatch(t2);
1160 return new BitVecExpr(
this, Native.mkBvmul(nCtx(),
1161 t1.getNativeObject(), t2.getNativeObject()));
1173 checkContextMatch(t1);
1174 checkContextMatch(t2);
1175 return new BitVecExpr(
this, Native.mkBvudiv(nCtx(),
1176 t1.getNativeObject(), t2.getNativeObject()));
1194 checkContextMatch(t1);
1195 checkContextMatch(t2);
1196 return new BitVecExpr(
this, Native.mkBvsdiv(nCtx(),
1197 t1.getNativeObject(), t2.getNativeObject()));
1209 checkContextMatch(t1);
1210 checkContextMatch(t2);
1211 return new BitVecExpr(
this, Native.mkBvurem(nCtx(),
1212 t1.getNativeObject(), t2.getNativeObject()));
1227 checkContextMatch(t1);
1228 checkContextMatch(t2);
1229 return new BitVecExpr(
this, Native.mkBvsrem(nCtx(),
1230 t1.getNativeObject(), t2.getNativeObject()));
1241 checkContextMatch(t1);
1242 checkContextMatch(t2);
1243 return new BitVecExpr(
this, Native.mkBvsmod(nCtx(),
1244 t1.getNativeObject(), t2.getNativeObject()));
1254 checkContextMatch(t1);
1255 checkContextMatch(t2);
1256 return new BoolExpr(
this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1257 t2.getNativeObject()));
1267 checkContextMatch(t1);
1268 checkContextMatch(t2);
1269 return new BoolExpr(
this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1270 t2.getNativeObject()));
1280 checkContextMatch(t1);
1281 checkContextMatch(t2);
1282 return new BoolExpr(
this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1283 t2.getNativeObject()));
1293 checkContextMatch(t1);
1294 checkContextMatch(t2);
1295 return new BoolExpr(
this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1296 t2.getNativeObject()));
1306 checkContextMatch(t1);
1307 checkContextMatch(t2);
1308 return new BoolExpr(
this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1309 t2.getNativeObject()));
1319 checkContextMatch(t1);
1320 checkContextMatch(t2);
1321 return new BoolExpr(
this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1322 t2.getNativeObject()));
1332 checkContextMatch(t1);
1333 checkContextMatch(t2);
1334 return new BoolExpr(
this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1335 t2.getNativeObject()));
1345 checkContextMatch(t1);
1346 checkContextMatch(t2);
1347 return new BoolExpr(
this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1348 t2.getNativeObject()));
1363 checkContextMatch(t1);
1364 checkContextMatch(t2);
1365 return new BitVecExpr(
this, Native.mkConcat(nCtx(),
1366 t1.getNativeObject(), t2.getNativeObject()));
1380 checkContextMatch(t);
1381 return new BitVecExpr(
this, Native.mkExtract(nCtx(), high, low,
1382 t.getNativeObject()));
1394 checkContextMatch(t);
1395 return new BitVecExpr(
this, Native.mkSignExt(nCtx(), i,
1396 t.getNativeObject()));
1408 checkContextMatch(t);
1409 return new BitVecExpr(
this, Native.mkZeroExt(nCtx(), i,
1410 t.getNativeObject()));
1420 checkContextMatch(t);
1421 return new BitVecExpr(
this, Native.mkRepeat(nCtx(), i,
1422 t.getNativeObject()));
1438 checkContextMatch(t1);
1439 checkContextMatch(t2);
1440 return new BitVecExpr(
this, Native.mkBvshl(nCtx(),
1441 t1.getNativeObject(), t2.getNativeObject()));
1457 checkContextMatch(t1);
1458 checkContextMatch(t2);
1459 return new BitVecExpr(
this, Native.mkBvlshr(nCtx(),
1460 t1.getNativeObject(), t2.getNativeObject()));
1477 checkContextMatch(t1);
1478 checkContextMatch(t2);
1479 return new BitVecExpr(
this, Native.mkBvashr(nCtx(),
1480 t1.getNativeObject(), t2.getNativeObject()));
1490 checkContextMatch(t);
1491 return new BitVecExpr(
this, Native.mkRotateLeft(nCtx(), i,
1492 t.getNativeObject()));
1502 checkContextMatch(t);
1503 return new BitVecExpr(
this, Native.mkRotateRight(nCtx(), i,
1504 t.getNativeObject()));
1516 checkContextMatch(t1);
1517 checkContextMatch(t2);
1518 return new BitVecExpr(
this, Native.mkExtRotateLeft(nCtx(),
1519 t1.getNativeObject(), t2.getNativeObject()));
1531 checkContextMatch(t1);
1532 checkContextMatch(t2);
1533 return new BitVecExpr(
this, Native.mkExtRotateRight(nCtx(),
1534 t1.getNativeObject(), t2.getNativeObject()));
1548 checkContextMatch(t);
1549 return new BitVecExpr(
this, Native.mkInt2bv(nCtx(), n,
1550 t.getNativeObject()));
1569 checkContextMatch(t);
1570 return new IntExpr(
this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1582 checkContextMatch(t1);
1583 checkContextMatch(t2);
1584 return new BoolExpr(
this, Native.mkBvaddNoOverflow(nCtx(), t1
1585 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1596 checkContextMatch(t1);
1597 checkContextMatch(t2);
1598 return new BoolExpr(
this, Native.mkBvaddNoUnderflow(nCtx(),
1599 t1.getNativeObject(), t2.getNativeObject()));
1610 checkContextMatch(t1);
1611 checkContextMatch(t2);
1612 return new BoolExpr(
this, Native.mkBvsubNoOverflow(nCtx(),
1613 t1.getNativeObject(), t2.getNativeObject()));
1624 checkContextMatch(t1);
1625 checkContextMatch(t2);
1626 return new BoolExpr(
this, Native.mkBvsubNoUnderflow(nCtx(), t1
1627 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1638 checkContextMatch(t1);
1639 checkContextMatch(t2);
1640 return new BoolExpr(
this, Native.mkBvsdivNoOverflow(nCtx(),
1641 t1.getNativeObject(), t2.getNativeObject()));
1651 checkContextMatch(t);
1652 return new BoolExpr(
this, Native.mkBvnegNoOverflow(nCtx(),
1653 t.getNativeObject()));
1664 checkContextMatch(t1);
1665 checkContextMatch(t2);
1666 return new BoolExpr(
this, Native.mkBvmulNoOverflow(nCtx(), t1
1667 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1678 checkContextMatch(t1);
1679 checkContextMatch(t2);
1680 return new BoolExpr(
this, Native.mkBvmulNoUnderflow(nCtx(),
1681 t1.getNativeObject(), t2.getNativeObject()));
1696 public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkArrayConst(
String name, D domain, R
range)
1699 return (ArrayExpr<D, R>) mkConst(mkSymbol(name), mkArraySort(domain,
range));
1715 public <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
1717 checkContextMatch(a);
1718 checkContextMatch(i);
1719 return (Expr<R>) Expr.create(
1721 Native.mkSelect(nCtx(), a.getNativeObject(),
1722 i.getNativeObject()));
1737 public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort, R>> a, Expr<?>[] args)
1739 checkContextMatch(a);
1740 checkContextMatch(args);
1741 return (Expr<R>) Expr.create(
1743 Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
1762 public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)
1764 checkContextMatch(a);
1765 checkContextMatch(i);
1766 checkContextMatch(v);
1767 return new ArrayExpr<>(
this, Native.mkStore(nCtx(), a.getNativeObject(),
1768 i.getNativeObject(), v.getNativeObject()));
1787 public <R extends Sort> ArrayExpr<Sort, R> mkStore(Expr<ArraySort<Sort, R>> a, Expr<?>[] args, Expr<R> v)
1789 checkContextMatch(a);
1790 checkContextMatch(args);
1791 checkContextMatch(v);
1792 return new ArrayExpr<>(
this, Native.mkStoreN(nCtx(), a.getNativeObject(),
1793 args.length, AST.arrayToNative(args), v.getNativeObject()));
1805 public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkConstArray(D domain, Expr<R> v)
1807 checkContextMatch(domain);
1808 checkContextMatch(v);
1809 return new ArrayExpr<>(
this, Native.mkConstArray(nCtx(),
1810 domain.getNativeObject(), v.getNativeObject()));
1829 checkContextMatch(f);
1830 checkContextMatch(args);
1844 checkContextMatch(array);
1846 Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1852 public <D extends Sort, R extends Sort> Expr<D> mkArrayExt(Expr<ArraySort<D, R>> arg1, Expr<ArraySort<D, R>> arg2)
1854 checkContextMatch(arg1);
1855 checkContextMatch(arg2);
1856 return (Expr<D>) Expr.create(
this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
1863 public <D extends Sort> SetSort<D> mkSetSort(D ty)
1865 checkContextMatch(ty);
1866 return new SetSort<>(
this, ty);
1872 public <D extends Sort> ArrayExpr<D, BoolSort> mkEmptySet(D domain)
1874 checkContextMatch(domain);
1875 return (ArrayExpr<D, BoolSort>) Expr.create(
this,
1876 Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1882 public <D extends Sort> ArrayExpr<D, BoolSort> mkFullSet(D domain)
1884 checkContextMatch(domain);
1885 return (ArrayExpr<D, BoolSort>) Expr.create(
this,
1886 Native.mkFullSet(nCtx(), domain.getNativeObject()));
1892 public <D extends Sort> ArrayExpr<D, BoolSort> mkSetAdd(Expr<ArraySort<D, BoolSort>>
set, Expr<D> element)
1894 checkContextMatch(
set);
1895 checkContextMatch(element);
1896 return (ArrayExpr<D, BoolSort>) Expr.create(
this,
1897 Native.mkSetAdd(nCtx(),
set.getNativeObject(),
1898 element.getNativeObject()));
1904 public <D extends Sort> ArrayExpr<D, BoolSort> mkSetDel(Expr<ArraySort<D, BoolSort>>
set, Expr<D> element)
1906 checkContextMatch(
set);
1907 checkContextMatch(element);
1908 return (ArrayExpr<D, BoolSort>)Expr.create(
this,
1909 Native.mkSetDel(nCtx(),
set.getNativeObject(),
1910 element.getNativeObject()));
1919 checkContextMatch(args);
1921 Native.mkSetUnion(nCtx(), args.length,
1931 checkContextMatch(args);
1933 Native.mkSetIntersect(nCtx(), args.length,
1942 checkContextMatch(arg1);
1943 checkContextMatch(arg2);
1945 Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1946 arg2.getNativeObject()));
1952 public <D extends Sort> ArrayExpr<D, BoolSort> mkSetComplement(Expr<ArraySort<D, BoolSort>> arg)
1954 checkContextMatch(arg);
1955 return (ArrayExpr<D, BoolSort>)Expr.create(
this,
1956 Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1962 public <D extends Sort> BoolExpr mkSetMembership(Expr<D> elem, Expr<ArraySort<D, BoolSort>>
set)
1964 checkContextMatch(elem);
1965 checkContextMatch(
set);
1966 return (BoolExpr) Expr.create(
this,
1967 Native.mkSetMember(nCtx(), elem.getNativeObject(),
1968 set.getNativeObject()));
1974 public <D extends Sort> BoolExpr mkSetSubset(Expr<ArraySort<D, BoolSort>> arg1, Expr<ArraySort<D, BoolSort>> arg2)
1976 checkContextMatch(arg1);
1977 checkContextMatch(arg2);
1978 return (BoolExpr) Expr.create(
this,
1979 Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1980 arg2.getNativeObject()));
1991 public <R extends Sort> SeqExpr<R> mkEmptySeq(R s)
1993 checkContextMatch(s);
1994 return (SeqExpr<R>) Expr.create(
this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
2000 public <R extends Sort> SeqExpr<R> mkUnit(Expr<R> elem)
2002 checkContextMatch(elem);
2003 return (SeqExpr<R>) Expr.create(
this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
2027 return (
IntExpr)
Expr.create(
this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
2036 checkContextMatch(t);
2046 checkContextMatch(s);
2047 return (
IntExpr)
Expr.create(
this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
2053 public <R extends Sort> BoolExpr mkPrefixOf(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
2055 checkContextMatch(s1, s2);
2056 return (BoolExpr) Expr.create(
this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2062 public <R extends Sort> BoolExpr mkSuffixOf(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
2064 checkContextMatch(s1, s2);
2065 return (BoolExpr)Expr.create(
this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2071 public <R extends Sort> BoolExpr mkContains(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
2073 checkContextMatch(s1, s2);
2074 return (BoolExpr) Expr.create(
this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2080 public <R extends Sort> SeqExpr<R> mkAt(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> index)
2082 checkContextMatch(s, index);
2083 return (SeqExpr<R>) Expr.create(
this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
2089 public <R extends Sort> Expr<R> MkNth(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> index)
2091 checkContextMatch(s, index);
2092 return (Expr<R>) Expr.create(
this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
2099 public <R extends Sort> SeqExpr<R> mkExtract(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> offset, Expr<IntSort> length)
2101 checkContextMatch(s, offset, length);
2102 return (SeqExpr<R>) Expr.create(
this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
2108 public <R extends Sort> IntExpr mkIndexOf(Expr<SeqSort<BitVecSort>> s, Expr<SeqSort<BitVecSort>> substr, Expr<IntSort> offset)
2110 checkContextMatch(s, substr, offset);
2111 return (IntExpr)Expr.create(
this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
2117 public <R extends Sort> SeqExpr<R> mkReplace(Expr<SeqSort<BitVecSort>> s, Expr<SeqSort<BitVecSort>> src, Expr<SeqSort<BitVecSort>> dst)
2119 checkContextMatch(s, src, dst);
2120 return (SeqExpr<R>) Expr.create(
this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
2126 public <R extends Sort> ReExpr<R> mkToRe(Expr<SeqSort<BitVecSort>> s)
2128 checkContextMatch(s);
2129 return (ReExpr<R>) Expr.create(
this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
2136 public <R extends Sort> BoolExpr mkInRe(Expr<SeqSort<BitVecSort>> s, Expr<ReSort<R>> re)
2138 checkContextMatch(s, re);
2139 return (BoolExpr) Expr.create(
this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
2145 public <R extends Sort> ReExpr<R> mkStar(Expr<ReSort<R>> re)
2147 checkContextMatch(re);
2148 return (ReExpr<R>) Expr.create(
this, Native.mkReStar(nCtx(), re.getNativeObject()));
2154 public <R extends Sort> ReExpr<R> mkLoop(Expr<ReSort<R>> re,
int lo,
int hi)
2156 return (ReExpr<R>) Expr.create(
this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
2162 public <R extends Sort> ReExpr<R> mkLoop(Expr<ReSort<R>> re,
int lo)
2164 return (ReExpr<R>) Expr.create(
this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
2171 public <R extends Sort> ReExpr<R> mkPlus(Expr<ReSort<R>> re)
2173 checkContextMatch(re);
2174 return (ReExpr<R>) Expr.create(
this, Native.mkRePlus(nCtx(), re.getNativeObject()));
2180 public <R extends Sort> ReExpr<R> mkOption(Expr<ReSort<R>> re)
2182 checkContextMatch(re);
2183 return (ReExpr<R>) Expr.create(
this, Native.mkReOption(nCtx(), re.getNativeObject()));
2189 public <R extends Sort> ReExpr<R> mkComplement(Expr<ReSort<R>> re)
2191 checkContextMatch(re);
2192 return (ReExpr<R>) Expr.create(
this, Native.mkReComplement(nCtx(), re.getNativeObject()));
2201 checkContextMatch(t);
2211 checkContextMatch(t);
2221 checkContextMatch(t);
2228 public <R extends Sort>
ReExpr<R> mkEmptyRe(R s)
2230 return (
ReExpr<R>)
Expr.create(
this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
2236 public <R extends Sort> ReExpr<R> mkFullRe(R s)
2238 return (ReExpr<R>) Expr.create(
this, Native.mkReFull(nCtx(), s.getNativeObject()));
2244 public <R extends Sort> ReExpr<R> mkRange(Expr<SeqSort<BitVecSort>> lo, Expr<SeqSort<BitVecSort>> hi)
2246 checkContextMatch(lo, hi);
2247 return (ReExpr<R>) Expr.create(
this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
2256 checkContextMatch(args);
2265 checkContextMatch(args);
2274 checkContextMatch(args);
2283 checkContextMatch(args);
2292 checkContextMatch(args);
2309 checkContextMatch(ty);
2311 Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
2324 public <R extends Sort> Expr<R> mkNumeral(
int v, R ty)
2326 checkContextMatch(ty);
2327 return (Expr<R>) Expr.create(
this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
2340 public <R extends Sort> Expr<R> mkNumeral(
long v, R ty)
2342 checkContextMatch(ty);
2343 return (Expr<R>) Expr.create(
this,
2344 Native.mkInt64(nCtx(), v, ty.getNativeObject()));
2362 return new RatNum(
this, Native.mkReal(nCtx(), num, den));
2374 return new RatNum(
this, Native.mkNumeral(nCtx(), v, getRealSort()
2375 .getNativeObject()));
2387 return new RatNum(
this, Native.mkInt(nCtx(), v, getRealSort()
2388 .getNativeObject()));
2400 return new RatNum(
this, Native.mkInt64(nCtx(), v, getRealSort()
2401 .getNativeObject()));
2411 return new IntNum(
this, Native.mkNumeral(nCtx(), v, getIntSort()
2412 .getNativeObject()));
2424 return new IntNum(
this, Native.mkInt(nCtx(), v, getIntSort()
2425 .getNativeObject()));
2437 return new IntNum(
this, Native.mkInt64(nCtx(), v, getIntSort()
2438 .getNativeObject()));
2448 return (
BitVecNum) mkNumeral(v, mkBitVecSort(size));
2458 return (
BitVecNum) mkNumeral(v, mkBitVecSort(size));
2468 return (
BitVecNum) mkNumeral(v, mkBitVecSort(size));
2500 return Quantifier.
of(
this,
true, sorts, names, body, weight, patterns,
2501 noPatterns, quantifierID, skolemID);
2513 return Quantifier.
of(
this,
true, boundConstants, body, weight,
2514 patterns, noPatterns, quantifierID, skolemID);
2526 return Quantifier.
of(
this,
false, sorts, names, body, weight,
2527 patterns, noPatterns, quantifierID, skolemID);
2539 return Quantifier.
of(
this,
false, boundConstants, body, weight,
2540 patterns, noPatterns, quantifierID, skolemID);
2554 return mkForall(sorts, names, body, weight, patterns, noPatterns,
2555 quantifierID, skolemID);
2557 return mkExists(sorts, names, body, weight, patterns, noPatterns,
2558 quantifierID, skolemID);
2571 return mkForall(boundConstants, body, weight, patterns, noPatterns,
2572 quantifierID, skolemID);
2574 return mkExists(boundConstants, body, weight, patterns, noPatterns,
2575 quantifierID, skolemID);
2597 return Lambda.
of(
this, sorts, names, body);
2606 public <R extends Sort> Lambda<R> mkLambda(Expr<?>[] boundConstants, Expr<R> body)
2608 return Lambda.of(
this, boundConstants, body);
2628 Native.setAstPrintMode(nCtx(), value.toInt());
2649 return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2650 attributes, assumptions.length,
2670 if (csn != cs || cdn != cd) {
2691 if (csn != cs || cdn != cd)
2711 public Goal mkGoal(
boolean models,
boolean unsatCores,
boolean proofs)
2713 return new Goal(
this, models, unsatCores, proofs);
2729 return Native.getNumTactics(nCtx());
2738 int n = getNumTactics();
2740 for (
int i = 0; i < n; i++)
2741 res[i] = Native.getTacticName(nCtx(), i);
2751 return Native.tacticGetDescr(nCtx(), name);
2759 return new Tactic(
this, name);
2769 checkContextMatch(t1);
2770 checkContextMatch(t2);
2771 checkContextMatch(ts);
2774 if (ts !=
null && ts.length > 0)
2776 last = ts[ts.length - 1].getNativeObject();
2777 for (
int i = ts.length - 2; i >= 0; i--) {
2778 last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2784 last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2785 return new Tactic(
this, Native.tacticAndThen(nCtx(),
2786 t1.getNativeObject(), last));
2788 return new Tactic(
this, Native.tacticAndThen(nCtx(),
2789 t1.getNativeObject(), t2.getNativeObject()));
2800 return andThen(t1, t2, ts);
2810 checkContextMatch(t1);
2811 checkContextMatch(t2);
2812 return new Tactic(
this, Native.tacticOrElse(nCtx(),
2813 t1.getNativeObject(), t2.getNativeObject()));
2824 checkContextMatch(t);
2825 return new Tactic(
this, Native.tacticTryFor(nCtx(),
2826 t.getNativeObject(), ms));
2837 checkContextMatch(t);
2838 checkContextMatch(p);
2839 return new Tactic(
this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2840 t.getNativeObject()));
2850 checkContextMatch(p);
2851 checkContextMatch(t1);
2852 checkContextMatch(t2);
2853 return new Tactic(
this, Native.tacticCond(nCtx(), p.getNativeObject(),
2854 t1.getNativeObject(), t2.getNativeObject()));
2863 checkContextMatch(t);
2864 return new Tactic(
this, Native.tacticRepeat(nCtx(),
2865 t.getNativeObject(),
max));
2873 return new Tactic(
this, Native.tacticSkip(nCtx()));
2881 return new Tactic(
this, Native.tacticFail(nCtx()));
2890 checkContextMatch(p);
2892 Native.tacticFailIf(nCtx(), p.getNativeObject()));
2901 return new Tactic(
this, Native.tacticFailIfNotDecided(nCtx()));
2910 checkContextMatch(t);
2911 checkContextMatch(p);
2912 return new Tactic(
this, Native.tacticUsingParams(nCtx(),
2913 t.getNativeObject(), p.getNativeObject()));
2924 return usingParams(t, p);
2932 checkContextMatch(t);
2933 return new Tactic(
this, Native.tacticParOr(nCtx(),
2943 checkContextMatch(t1);
2944 checkContextMatch(t2);
2945 return new Tactic(
this, Native.tacticParAndThen(nCtx(),
2946 t1.getNativeObject(), t2.getNativeObject()));
2956 Native.interrupt(nCtx());
2964 return Native.getNumProbes(nCtx());
2973 int n = getNumProbes();
2975 for (
int i = 0; i < n; i++)
2976 res[i] = Native.getProbeName(nCtx(), i);
2986 return Native.probeGetDescr(nCtx(), name);
2994 return new Probe(
this, name);
3002 return new Probe(
this, Native.probeConst(nCtx(), val));
3011 checkContextMatch(p1);
3012 checkContextMatch(p2);
3013 return new Probe(
this, Native.probeLt(nCtx(), p1.getNativeObject(),
3014 p2.getNativeObject()));
3023 checkContextMatch(p1);
3024 checkContextMatch(p2);
3025 return new Probe(
this, Native.probeGt(nCtx(), p1.getNativeObject(),
3026 p2.getNativeObject()));
3036 checkContextMatch(p1);
3037 checkContextMatch(p2);
3038 return new Probe(
this, Native.probeLe(nCtx(), p1.getNativeObject(),
3039 p2.getNativeObject()));
3049 checkContextMatch(p1);
3050 checkContextMatch(p2);
3051 return new Probe(
this, Native.probeGe(nCtx(), p1.getNativeObject(),
3052 p2.getNativeObject()));
3061 checkContextMatch(p1);
3062 checkContextMatch(p2);
3063 return new Probe(
this, Native.probeEq(nCtx(), p1.getNativeObject(),
3064 p2.getNativeObject()));
3072 checkContextMatch(p1);
3073 checkContextMatch(p2);
3074 return new Probe(
this, Native.probeAnd(nCtx(), p1.getNativeObject(),
3075 p2.getNativeObject()));
3083 checkContextMatch(p1);
3084 checkContextMatch(p2);
3085 return new Probe(
this, Native.probeOr(nCtx(), p1.getNativeObject(),
3086 p2.getNativeObject()));
3094 checkContextMatch(p);
3095 return new Probe(
this, Native.probeNot(nCtx(), p.getNativeObject()));
3107 return mkSolver((
Symbol)
null);
3121 return new Solver(
this, Native.mkSolver(nCtx()));
3123 return new Solver(
this, Native.mkSolverForLogic(nCtx(),
3124 logic.getNativeObject()));
3133 return mkSolver(mkSymbol(logic));
3141 return new Solver(
this, Native.mkSimpleSolver(nCtx()));
3153 return new Solver(
this, Native.mkSolverFromTactic(nCtx(),
3154 t.getNativeObject()));
3189 return new FPRMExpr(
this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3198 return new FPRMNum(
this, Native.mkFpaRne(nCtx()));
3207 return new FPRMNum(
this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3216 return new FPRMNum(
this, Native.mkFpaRna(nCtx()));
3225 return new FPRMNum(
this, Native.mkFpaRoundTowardPositive(nCtx()));
3234 return new FPRMNum(
this, Native.mkFpaRtp(nCtx()));
3243 return new FPRMNum(
this, Native.mkFpaRoundTowardNegative(nCtx()));
3252 return new FPRMNum(
this, Native.mkFpaRtn(nCtx()));
3261 return new FPRMNum(
this, Native.mkFpaRoundTowardZero(nCtx()));
3270 return new FPRMNum(
this, Native.mkFpaRtz(nCtx()));
3281 return new FPSort(
this, ebits, sbits);
3290 return new FPSort(
this, Native.mkFpaSortHalf(nCtx()));
3299 return new FPSort(
this, Native.mkFpaSort16(nCtx()));
3308 return new FPSort(
this, Native.mkFpaSortSingle(nCtx()));
3317 return new FPSort(
this, Native.mkFpaSort32(nCtx()));
3326 return new FPSort(
this, Native.mkFpaSortDouble(nCtx()));
3335 return new FPSort(
this, Native.mkFpaSort64(nCtx()));
3344 return new FPSort(
this, Native.mkFpaSortQuadruple(nCtx()));
3353 return new FPSort(
this, Native.mkFpaSort128(nCtx()));
3364 return new FPNum(
this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3375 return new FPNum(
this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3386 return new FPNum(
this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3397 return new FPNum(
this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3408 return new FPNum(
this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3419 return new FPNum(
this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3432 return new FPNum(
this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3445 return new FPNum(
this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3456 return mkFPNumeral(v, s);
3467 return mkFPNumeral(v, s);
3479 return mkFPNumeral(v, s);
3492 return mkFPNumeral(sgn, exp, sig, s);
3505 return mkFPNumeral(sgn, exp, sig, s);
3516 return new FPExpr(
this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3526 return new FPExpr(
this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3538 return new FPExpr(
this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3550 return new FPExpr(
this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3562 return new FPExpr(
this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3574 return new FPExpr(
this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3589 return new FPExpr(
this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3600 return new FPExpr(
this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3611 return new FPExpr(
this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3623 return new FPExpr(
this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3634 return new FPExpr(
this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3645 return new FPExpr(
this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3656 return new BoolExpr(
this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3667 return new BoolExpr(
this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3678 return new BoolExpr(
this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3689 return new BoolExpr(
this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3702 return new BoolExpr(
this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3712 return new BoolExpr(
this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3722 return new BoolExpr(
this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3732 return new BoolExpr(
this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3742 return new BoolExpr(
this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3752 return new BoolExpr(
this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3762 return new BoolExpr(
this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3772 return new BoolExpr(
this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3790 return new FPExpr(
this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3806 return new FPExpr(
this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3822 return new FPExpr(
this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3838 return new FPExpr(
this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3857 return new FPExpr(
this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3859 return new FPExpr(
this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3874 return new FPExpr(
this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3892 return new BitVecExpr(
this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3894 return new BitVecExpr(
this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3908 return new RealExpr(
this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3923 return new BitVecExpr(
this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3941 return new BitVecExpr(
this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3957 return AST.create(
this, nativeObject);
3974 return a.getNativeObject();
3983 return Native.simplifyGetHelp(nCtx());
3991 return new ParamDescrs(
this, Native.simplifyGetParamDescrs(nCtx()));
4004 Native.updateParamValue(nCtx(),
id, value);
4016 void checkContextMatch(
Z3Object other)
4018 if (
this != other.getContext())
4022 void checkContextMatch(Z3Object other1, Z3Object other2)
4024 checkContextMatch(other1);
4025 checkContextMatch(other2);
4028 void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
4030 checkContextMatch(other1);
4031 checkContextMatch(other2);
4032 checkContextMatch(other3);
4035 void checkContextMatch(Z3Object[] arr)
4038 for (Z3Object a : arr)
4039 checkContextMatch(a);
4042 private ASTDecRefQueue m_AST_DRQ =
new ASTDecRefQueue();
4043 private ASTMapDecRefQueue m_ASTMap_DRQ =
new ASTMapDecRefQueue();
4044 private ASTVectorDecRefQueue m_ASTVector_DRQ =
new ASTVectorDecRefQueue();
4045 private ApplyResultDecRefQueue m_ApplyResult_DRQ =
new ApplyResultDecRefQueue();
4046 private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ =
new FuncInterpEntryDecRefQueue();
4047 private FuncInterpDecRefQueue m_FuncInterp_DRQ =
new FuncInterpDecRefQueue();
4048 private GoalDecRefQueue m_Goal_DRQ =
new GoalDecRefQueue();
4049 private ModelDecRefQueue m_Model_DRQ =
new ModelDecRefQueue();
4050 private ParamsDecRefQueue m_Params_DRQ =
new ParamsDecRefQueue();
4051 private ParamDescrsDecRefQueue m_ParamDescrs_DRQ =
new ParamDescrsDecRefQueue();
4052 private ProbeDecRefQueue m_Probe_DRQ =
new ProbeDecRefQueue();
4053 private SolverDecRefQueue m_Solver_DRQ =
new SolverDecRefQueue();
4054 private StatisticsDecRefQueue m_Statistics_DRQ =
new StatisticsDecRefQueue();
4055 private TacticDecRefQueue m_Tactic_DRQ =
new TacticDecRefQueue();
4056 private FixedpointDecRefQueue m_Fixedpoint_DRQ =
new FixedpointDecRefQueue();
4057 private OptimizeDecRefQueue m_Optimize_DRQ =
new OptimizeDecRefQueue();
4058 private ConstructorDecRefQueue m_Constructor_DRQ =
new ConstructorDecRefQueue();
4059 private ConstructorListDecRefQueue m_ConstructorList_DRQ =
4060 new ConstructorListDecRefQueue();
4063 return m_Constructor_DRQ;
4067 return m_ConstructorList_DRQ;
4077 return m_ASTMap_DRQ;
4082 return m_ASTVector_DRQ;
4087 return m_ApplyResult_DRQ;
4092 return m_FuncEntry_DRQ;
4097 return m_FuncInterp_DRQ;
4112 return m_Params_DRQ;
4117 return m_ParamDescrs_DRQ;
4127 return m_Solver_DRQ;
4132 return m_Statistics_DRQ;
4137 return m_Tactic_DRQ;
4142 return m_Fixedpoint_DRQ;
4147 return m_Optimize_DRQ;
4156 m_AST_DRQ.forceClear(
this);
4157 m_ASTMap_DRQ.forceClear(
this);
4158 m_ASTVector_DRQ.forceClear(
this);
4159 m_ApplyResult_DRQ.forceClear(
this);
4160 m_FuncEntry_DRQ.forceClear(
this);
4161 m_FuncInterp_DRQ.forceClear(
this);
4162 m_Goal_DRQ.forceClear(
this);
4163 m_Model_DRQ.forceClear(
this);
4164 m_Params_DRQ.forceClear(
this);
4165 m_Probe_DRQ.forceClear(
this);
4166 m_Solver_DRQ.forceClear(
this);
4167 m_Optimize_DRQ.forceClear(
this);
4168 m_Statistics_DRQ.forceClear(
this);
4169 m_Tactic_DRQ.forceClear(
this);
4170 m_Fixedpoint_DRQ.forceClear(
this);
4175 m_stringSort =
null;
4177 synchronized (creation_lock) {
4178 Native.delContext(m_ctx);
BoolExpr[] ToBoolExprArray()
Probe ge(Probe p1, Probe p2)
Solver mkSolver(String logic)
Tactic repeat(Tactic t, int max)
BitVecExpr mkBVXOR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
final BoolExpr mkDistinct(Expr<?>... args)
BitVecExpr mkBVUDiv(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
String getProbeDescription(String name)
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
final< D extends Sort > ArrayExpr< D, BoolSort > mkSetIntersection(Expr< ArraySort< D, BoolSort > >... args)
SeqExpr< BitVecSort > mkString(String s)
BoolExpr mkFPIsPositive(Expr< FPSort > t)
BitVecExpr mkBVNOR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
FPExpr mkFPToFP(Expr< FPRMSort > rm, Expr< BitVecSort > t, FPSort s, boolean signed)
FPRMExpr mkFPRoundNearestTiesToEven()
Fixedpoint mkFixedpoint()
Tactic usingParams(Tactic t, Params p)
Tactic parOr(Tactic... t)
BoolExpr mkBVULE(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BoolExpr mkBVSubNoOverflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BoolExpr mkBVNegNoOverflow(Expr< BitVecSort > t)
Tactic then(Tactic t1, Tactic t2, Tactic... ts)
FPExpr mkFPMax(Expr< FPSort > t1, Expr< FPSort > t2)
IntExpr mkBV2Int(Expr< BitVecSort > t, boolean signed)
FPSort mkFPSort(int ebits, int sbits)
BoolExpr mkBVSDivNoOverflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Probe le(Probe p1, Probe p2)
AST wrapAST(long nativeObject)
SeqSort< BitVecSort > getStringSort()
UninterpretedSort mkUninterpretedSort(Symbol s)
BitVecExpr mkBVXNOR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BoolExpr mkImplies(Expr< BoolSort > t1, Expr< BoolSort > t2)
BoolExpr mkBVAddNoOverflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
BitVecExpr mkBVRotateRight(int i, Expr< BitVecSort > t)
RealExpr mkInt2Real(Expr< IntSort > t)
BitVecExpr mkBVLSHR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
FPNum mkFP(double v, FPSort s)
BoolExpr mkLe(Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
IDecRefQueue< FuncInterp<?> > getFuncInterpDRQ()
IntExpr mkReal2Int(Expr< RealSort > t)
FPNum mkFPInf(FPSort s, boolean negative)
FPExpr mkFPRoundToIntegral(Expr< FPRMSort > rm, Expr< FPSort > t)
BoolExpr mkAtLeast(Expr< BoolSort >[] args, int k)
BitVecExpr mkBVSMod(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BitVecExpr mkInt2BV(int n, Expr< IntSort > t)
BoolExpr mkBVSGE(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BitVecExpr mkBVConst(Symbol name, int size)
BitVecExpr mkExtract(int high, int low, Expr< BitVecSort > t)
FPRMNum mkFPRoundTowardZero()
BoolExpr mkFPGEq(Expr< FPSort > t1, Expr< FPSort > t2)
Probe or(Probe p1, Probe p2)
IDecRefQueue< ASTMap > getASTMapDRQ()
BitVecExpr mkBVURem(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
final< D extends Sort, R1 extends Sort, R2 extends Sort > ArrayExpr< D, R2 > mkMap(FuncDecl< R2 > f, Expr< ArraySort< D, R1 > >... args)
Tactic cond(Probe p, Tactic t1, Tactic t2)
IDecRefQueue< Statistics > getStatisticsDRQ()
BoolExpr mkBVSGT(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
IDecRefQueue< Model > getModelDRQ()
BitVecExpr mkBVConst(String name, int size)
IDecRefQueue< Optimize > getOptimizeDRQ()
BoolExpr mkAtMost(Expr< BoolSort >[] args, int k)
IDecRefQueue< AST > getASTDRQ()
BoolExpr mkFPIsSubnormal(Expr< FPSort > t)
IntExpr mkMod(Expr< IntSort > t1, Expr< IntSort > t2)
FPExpr mkFPToFP(Expr< FPRMSort > rm, RealExpr t, FPSort s)
BoolExpr mkNot(Expr< BoolSort > a)
FPExpr mkFPSub(Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
BoolExpr mkBVMulNoOverflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
FPExpr mkFPSqrt(Expr< FPRMSort > rm, Expr< FPSort > t)
FPNum mkFPNumeral(int v, FPSort s)
FPExpr mkFPMul(Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
BitVecExpr mkConcat(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
IDecRefQueue< ApplyResult > getApplyResultDRQ()
BitVecExpr mkSignExt(int i, Expr< BitVecSort > t)
BitVecExpr mkBVAdd(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
void updateParamValue(String id, String value)
BitVecExpr mkZeroExt(int i, Expr< BitVecSort > t)
final< R extends Sort > ReExpr< R > mkConcat(ReExpr< R >... t)
BoolExpr mkFPLt(Expr< FPSort > t1, Expr< FPSort > t2)
IntExpr stringToInt(Expr< SeqSort< BitVecSort > > e)
BitVecExpr mkBVRedAND(Expr< BitVecSort > t)
BitVecNum mkBV(long v, int size)
BitVecExpr mkBVSRem(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
FPNum mkFPNumeral(float v, FPSort s)
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Tactic when(Probe p, Tactic t)
IDecRefQueue< Goal > getGoalDRQ()
Probe mkProbe(String name)
BoolExpr mkPBLe(int[] coeffs, Expr< BoolSort >[] args, int k)
RealExpr mkRealConst(String name)
final< R extends ArithSort > ArithExpr< R > mkAdd(Expr<? extends R >... t)
Tactic failIfNotDecided()
ParamDescrs getSimplifyParameterDescriptions()
BitVecExpr mkBVRotateRight(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
SeqSort< BitVecSort > mkStringSort()
Probe gt(Probe p1, Probe p2)
BoolExpr mkFPIsNaN(Expr< FPSort > t)
BoolExpr mkEq(Expr<?> x, Expr<?> y)
Tactic with(Tactic t, Params p)
BitVecExpr mkBVASHR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
String[] getTacticNames()
String benchmarkToSMTString(String name, String logic, String status, String attributes, Expr< BoolSort >[] assumptions, Expr< BoolSort > formula)
FPRMNum mkFPRoundNearestTiesToAway()
BoolExpr mkBool(boolean value)
BitVecExpr mkBVMul(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BitVecExpr mkBVSub(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
BitVecExpr mkBVOR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BoolExpr mkLt(Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
final Pattern mkPattern(Expr<?>... terms)
BitVecExpr mkRepeat(int i, Expr< BitVecSort > t)
BoolExpr mkXor(Expr< BoolSort > t1, Expr< BoolSort > t2)
FPRMNum mkFPRoundTowardNegative()
IDecRefQueue< Params > getParamsDRQ()
Probe eq(Probe p1, Probe p2)
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
BitVecExpr mkBVRotateLeft(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
IDecRefQueue< Solver > getSolverDRQ()
Quantifier mkQuantifier(boolean universal, Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
BitVecExpr mkBVRedOR(Expr< BitVecSort > t)
BoolExpr mkBVUGE(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
FPExpr mkFPDiv(Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
BitVecExpr mkBVNAND(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
FPExpr mkFPRem(Expr< FPSort > t1, Expr< FPSort > t2)
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
IntExpr mkIntConst(String name)
Solver mkSolver(Tactic t)
BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
final< R extends Sort > Expr< R > mkApp(FuncDecl< R > f, Expr<?>... args)
BoolExpr mkBVAddNoUnderflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BoolExpr mkBVSubNoUnderflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
BoolExpr mkFPIsZero(Expr< FPSort > t)
IntExpr mkIntConst(Symbol name)
IDecRefQueue< ConstructorList<?> > getConstructorListDRQ()
BitVecExpr mkBVNeg(Expr< BitVecSort > t)
Tactic mkTactic(String name)
SeqExpr< BitVecSort > intToString(Expr< IntSort > e)
BoolExpr mkBVSLE(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
FPNum mkFPNumeral(double v, FPSort s)
Tactic parAndThen(Tactic t1, Tactic t2)
BoolExpr mkGt(Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
BitVecNum mkBV(int v, int size)
Context(Map< String, String > settings)
IDecRefQueue< FuncInterp.Entry<?> > getFuncEntryDRQ()
final< R extends Sort > ReExpr< R > mkIntersect(Expr< ReSort< R > >... t)
final< R extends ArithSort > ArithExpr< R > mkMul(Expr<? extends R >... t)
BoolExpr mkBVMulNoUnderflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BitVecExpr mkBVSDiv(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
FPRMSort mkFPRoundingModeSort()
RealExpr mkRealConst(Symbol name)
String getTacticDescription(String name)
IDecRefQueue< Probe > getProbeDRQ()
Solver mkSolver(Symbol logic)
BoolExpr mkFPEq(Expr< FPSort > t1, Expr< FPSort > t2)
BoolExpr mkFPLEq(Expr< FPSort > t1, Expr< FPSort > t2)
RatNum mkReal(int num, int den)
BitVecSort mkBitVecSort(int size)
FPExpr mkFPToFP(Expr< BitVecSort > bv, FPSort s)
BoolExpr mkBVSLT(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BoolExpr mkFPGt(Expr< FPSort > t1, Expr< FPSort > t2)
BoolExpr mkIff(Expr< BoolSort > t1, Expr< BoolSort > t2)
BoolExpr mkGe(Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
BitVecExpr mkFPToFP(Expr< FPRMSort > rm, Expr< IntSort > exp, Expr< RealSort > sig, FPSort s)
BoolExpr mkIsInteger(Expr< RealSort > t)
FPExpr mkFPToFP(Expr< FPRMSort > rm, FPExpr t, FPSort s)
Probe constProbe(double val)
BoolExpr mkFPIsNegative(Expr< FPSort > t)
BoolExpr mkBoolConst(String name)
RealExpr mkFPToReal(Expr< FPSort > t)
FPExpr mkFP(Expr< BitVecSort > sgn, Expr< BitVecSort > sig, Expr< BitVecSort > exp)
FPExpr mkFPToFP(FPSort s, Expr< FPRMSort > rm, Expr< FPSort > t)
FPExpr mkFPNeg(Expr< FPSort > t)
IDecRefQueue< Tactic > getTacticDRQ()
final< R extends Sort > SeqExpr< R > mkConcat(Expr< SeqSort< R > >... t)
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
FPSort mkFPSortQuadruple()
FPRMNum mkFPRoundTowardPositive()
Quantifier mkExists(Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
final< D extends Sort > ArrayExpr< D, BoolSort > mkSetUnion(Expr< ArraySort< D, BoolSort > >... args)
BoolExpr mkBVULT(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
BoolExpr mkFPIsNormal(Expr< FPSort > t)
DatatypeSort< Object >[] mkDatatypeSorts(String[] names, Constructor< Object >[][] c)
Probe and(Probe p1, Probe p2)
Tactic tryFor(Tactic t, int ms)
FPExpr mkFPFMA(Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2, Expr< FPSort > t3)
UninterpretedSort mkUninterpretedSort(String str)
void setPrintMode(Z3_ast_print_mode value)
DatatypeSort< Object >[] mkDatatypeSorts(Symbol[] names, Constructor< Object >[][] c)
final BoolExpr mkAnd(Expr< BoolSort >... t)
BitVecNum mkBV(String v, int size)
BitVecExpr mkBVRotateLeft(int i, Expr< BitVecSort > t)
Probe lt(Probe p1, Probe p2)
Quantifier mkForall(Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
IntExpr mkRem(Expr< IntSort > t1, Expr< IntSort > t2)
BitVecExpr mkBVNot(Expr< BitVecSort > t)
final< R extends ArithSort > ArithExpr< R > mkSub(Expr<? extends R >... t)
BitVecExpr mkBVAND(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
FPExpr mkFPAbs(Expr< FPSort > t)
BoolExpr mkPBEq(int[] coeffs, Expr< BoolSort >[] args, int k)
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
IDecRefQueue< Constructor<?> > getConstructorDRQ()
FPExpr mkFPAdd(Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
BoolExpr mkBVUGT(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
FPNum mkFP(float v, FPSort s)
final BoolExpr mkOr(Expr< BoolSort >... t)
BitVecExpr mkBVSHL(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
BitVecExpr mkFPToIEEEBV(Expr< FPSort > t)
FPExpr mkFPMin(Expr< FPSort > t1, Expr< FPSort > t2)
Tactic orElse(Tactic t1, Tactic t2)
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
FPNum mkFP(int v, FPSort s)
final< R extends Sort > ReExpr< R > mkUnion(Expr< ReSort< R > >... t)
IntSymbol mkSymbol(int i)
StringSymbol mkSymbol(String name)
FPNum mkFPZero(FPSort s, boolean negative)
BoolExpr mkFPIsInfinite(Expr< FPSort > t)
BoolExpr mkBoolConst(Symbol name)
IDecRefQueue< ASTVector > getASTVectorDRQ()
BitVecExpr mkFPToBV(Expr< FPRMSort > rm, Expr< FPSort > t, int sz, boolean signed)
BoolExpr mkPBGe(int[] coeffs, Expr< BoolSort >[] args, int k)
static< R extends Sort > Lambda< R > of(Context ctx, Sort[] sorts, Symbol[] names, Expr< R > body)
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long[] arrayToNative(Z3Object[] a)
static int arrayLength(Z3Object[] a)
expr range(expr const &lo, expr const &hi)
expr max(expr const &a, expr const &b)
def String(name, ctx=None)
def FPSort(ebits, sbits, ctx=None)
def TupleSort(name, sorts, ctx=None)
def BitVecSort(sz, ctx=None)
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).