21 using System.Collections.Generic;
22 using System.Runtime.InteropServices;
23 using System.Diagnostics.Contracts;
30 [ContractVerification(
true)]
62 public Context(Dictionary<string, string> settings)
65 Contract.Requires(settings != null);
68 foreach (KeyValuePair<string, string> kv
in settings)
86 Contract.Ensures(Contract.Result<
IntSymbol>() != null);
96 Contract.Ensures(Contract.Result<
StringSymbol>() != null);
104 internal Symbol[] MkSymbols(
string[] names)
106 Contract.Ensures(names == null || Contract.Result<
Symbol[]>() != null);
107 Contract.Ensures(names != null || Contract.Result<
Symbol[]>() == null);
108 Contract.Ensures(Contract.Result<
Symbol[]>() == null || Contract.Result<
Symbol[]>().Length == names.Length);
109 Contract.Ensures(Contract.Result<
Symbol[]>() == null || Contract.ForAll(Contract.Result<
Symbol[]>(), s => s != null));
111 if (names == null)
return null;
113 for (
int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
120 private IntSort m_intSort = null;
130 Contract.Ensures(Contract.Result<
BoolSort>() != null);
131 if (m_boolSort == null) m_boolSort =
new BoolSort(
this);
return m_boolSort;
142 Contract.Ensures(Contract.Result<
IntSort>() != null);
143 if (m_intSort == null) m_intSort =
new IntSort(
this);
return m_intSort;
155 Contract.Ensures(Contract.Result<
RealSort>() != null);
156 if (m_realSort == null) m_realSort =
new RealSort(
this);
return m_realSort;
165 Contract.Ensures(Contract.Result<
BoolSort>() != null);
174 Contract.Requires(s != null);
177 CheckContextMatch(s);
188 return MkUninterpretedSort(MkSymbol(str));
196 Contract.Ensures(Contract.Result<
IntSort>() != null);
206 Contract.Ensures(Contract.Result<
RealSort>() != null);
215 Contract.Ensures(Contract.Result<
BitVecSort>() != null);
225 Contract.Requires(domain != null);
226 Contract.Requires(range != null);
227 Contract.Ensures(Contract.Result<
ArraySort>() != null);
229 CheckContextMatch(domain);
230 CheckContextMatch(range);
231 return new ArraySort(
this, domain, range);
239 Contract.Requires(name != null);
240 Contract.Requires(fieldNames != null);
241 Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
242 Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
243 Contract.Ensures(Contract.Result<
TupleSort>() != null);
245 CheckContextMatch(name);
246 CheckContextMatch(fieldNames);
247 CheckContextMatch(fieldSorts);
248 return new TupleSort(
this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
256 Contract.Requires(name != null);
257 Contract.Requires(enumNames != null);
258 Contract.Requires(Contract.ForAll(enumNames, f => f != null));
260 Contract.Ensures(Contract.Result<
EnumSort>() != null);
262 CheckContextMatch(name);
263 CheckContextMatch(enumNames);
264 return new EnumSort(
this, name, enumNames);
272 Contract.Requires(enumNames != null);
273 Contract.Ensures(Contract.Result<
EnumSort>() != null);
275 return new EnumSort(
this, MkSymbol(name), MkSymbols(enumNames));
283 Contract.Requires(name != null);
284 Contract.Requires(elemSort != null);
285 Contract.Ensures(Contract.Result<
ListSort>() != null);
287 CheckContextMatch(name);
288 CheckContextMatch(elemSort);
289 return new ListSort(
this, name, elemSort);
297 Contract.Requires(elemSort != null);
298 Contract.Ensures(Contract.Result<
ListSort>() != null);
300 CheckContextMatch(elemSort);
301 return new ListSort(
this, MkSymbol(name), elemSort);
312 Contract.Requires(name != null);
315 CheckContextMatch(name);
348 Contract.Requires(name != null);
349 Contract.Requires(recognizer != null);
350 Contract.Ensures(Contract.Result<
Constructor>() != null);
352 return new Constructor(
this, name, recognizer, fieldNames, sorts, sortRefs);
366 Contract.Ensures(Contract.Result<
Constructor>() != null);
368 return new Constructor(
this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
376 Contract.Requires(name != null);
377 Contract.Requires(constructors != null);
378 Contract.Requires(Contract.ForAll(constructors, c => c != null));
380 Contract.Ensures(Contract.Result<
DatatypeSort>() != null);
382 CheckContextMatch(name);
383 CheckContextMatch(constructors);
392 Contract.Requires(constructors != null);
393 Contract.Requires(Contract.ForAll(constructors, c => c != null));
394 Contract.Ensures(Contract.Result<
DatatypeSort>() != null);
396 CheckContextMatch(constructors);
397 return new DatatypeSort(
this, MkSymbol(name), constructors);
407 Contract.Requires(names != null);
408 Contract.Requires(c != null);
409 Contract.Requires(names.Length == c.Length);
410 Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
411 Contract.Requires(Contract.ForAll(names, name => name != null));
412 Contract.Ensures(Contract.Result<
DatatypeSort[]>() != null);
414 CheckContextMatch(names);
415 uint n = (uint)names.Length;
417 IntPtr[] n_constr =
new IntPtr[n];
418 for (uint i = 0; i < n; i++)
421 Contract.Assume(Contract.ForAll(constructor, arr => arr != null),
"Clousot does not support yet quantified formula on multidimensional arrays");
422 CheckContextMatch(constructor);
424 n_constr[i] = cla[i].NativeObject;
426 IntPtr[] n_res =
new IntPtr[n];
429 for (uint i = 0; i < n; i++)
442 Contract.Requires(names != null);
443 Contract.Requires(c != null);
444 Contract.Requires(names.Length == c.Length);
445 Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
446 Contract.Requires(Contract.ForAll(names, name => name != null));
447 Contract.Ensures(Contract.Result<
DatatypeSort[]>() != null);
449 return MkDatatypeSorts(MkSymbols(names), c);
455 #region Function Declarations
461 Contract.Requires(name != null);
462 Contract.Requires(range != null);
463 Contract.Requires(Contract.ForAll(domain, d => d != null));
464 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
466 CheckContextMatch(name);
467 CheckContextMatch(domain);
468 CheckContextMatch(range);
469 return new FuncDecl(
this, name, domain, range);
477 Contract.Requires(name != null);
478 Contract.Requires(domain != null);
479 Contract.Requires(range != null);
480 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
482 CheckContextMatch(name);
483 CheckContextMatch(domain);
484 CheckContextMatch(range);
486 return new FuncDecl(
this, name, q, range);
494 Contract.Requires(range != null);
495 Contract.Requires(Contract.ForAll(domain, d => d != null));
496 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
498 CheckContextMatch(domain);
499 CheckContextMatch(range);
500 return new FuncDecl(
this, MkSymbol(name), domain, range);
508 Contract.Requires(range != null);
509 Contract.Requires(domain != null);
510 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
512 CheckContextMatch(domain);
513 CheckContextMatch(range);
515 return new FuncDecl(
this, MkSymbol(name), q, range);
525 Contract.Requires(range != null);
526 Contract.Requires(Contract.ForAll(domain, d => d != null));
527 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
529 CheckContextMatch(domain);
530 CheckContextMatch(range);
531 return new FuncDecl(
this, prefix, domain, range);
539 Contract.Requires(name != null);
540 Contract.Requires(range != null);
541 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
543 CheckContextMatch(name);
544 CheckContextMatch(range);
545 return new FuncDecl(
this, name, null, range);
553 Contract.Requires(range != null);
554 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
556 CheckContextMatch(range);
557 return new FuncDecl(
this, MkSymbol(name), null, range);
567 Contract.Requires(range != null);
568 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
570 CheckContextMatch(range);
571 return new FuncDecl(
this, prefix, null, range);
575 #region Bound Variables
576 public Expr MkBound(uint index,
Sort ty)
583 Contract.Requires(ty != null);
584 Contract.Ensures(Contract.Result<
Expr>() != null);
590 #region Quantifier Patterns
591 public Pattern MkPattern(params Expr[] terms)
596 Contract.Requires(terms != null);
597 if (terms.Length == 0)
598 throw new Z3Exception(
"Cannot create a pattern from zero terms");
600 Contract.Ensures(Contract.Result<Pattern>() != null);
602 Contract.EndContractBlock();
604 IntPtr[] termsNative = AST.ArrayToNative(terms);
605 return new Pattern(
this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
610 public Expr MkConst(Symbol name, Sort range)
615 Contract.Requires(name != null);
616 Contract.Requires(range != null);
617 Contract.Ensures(Contract.Result<Expr>() != null);
619 CheckContextMatch(name);
620 CheckContextMatch(range);
622 return Expr.Create(
this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
630 Contract.Requires(range != null);
631 Contract.Ensures(Contract.Result<
Expr>() != null);
633 return MkConst(MkSymbol(name), range);
642 Contract.Requires(range != null);
643 Contract.Ensures(Contract.Result<
Expr>() != null);
645 CheckContextMatch(range);
655 Contract.Requires(f != null);
656 Contract.Ensures(Contract.Result<
Expr>() != null);
666 Contract.Requires(name != null);
667 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
677 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
687 Contract.Requires(name != null);
688 Contract.Ensures(Contract.Result<
IntExpr>() != null);
698 Contract.Requires(name != null);
699 Contract.Ensures(Contract.Result<
IntExpr>() != null);
709 Contract.Requires(name != null);
710 Contract.Ensures(Contract.Result<
RealExpr>() != null);
720 Contract.Ensures(Contract.Result<
RealExpr>() != null);
730 Contract.Requires(name != null);
731 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
733 return (
BitVecExpr)MkConst(name, MkBitVecSort(size));
741 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
743 return (
BitVecExpr)MkConst(name, MkBitVecSort(size));
753 Contract.Requires(f != null);
754 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
755 Contract.Ensures(Contract.Result<
Expr>() != null);
757 CheckContextMatch(f);
758 CheckContextMatch(args);
759 return Expr.Create(
this, f, args);
762 #region Propositional
763 public BoolExpr MkTrue()
768 Contract.Ensures(Contract.Result<BoolExpr>() != null);
770 return new BoolExpr(
this, Native.Z3_mk_true(nCtx));
778 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
788 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
790 return value ? MkTrue() : MkFalse();
798 Contract.Requires(x != null);
799 Contract.Requires(y != null);
800 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
802 CheckContextMatch(x);
803 CheckContextMatch(y);
812 Contract.Requires(args != null);
813 Contract.Requires(Contract.ForAll(args, a => a != null));
815 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
817 CheckContextMatch(args);
826 Contract.Requires(a != null);
827 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
829 CheckContextMatch(a);
841 Contract.Requires(t1 != null);
842 Contract.Requires(t2 != null);
843 Contract.Requires(t3 != null);
844 Contract.Ensures(Contract.Result<
Expr>() != null);
846 CheckContextMatch(t1);
847 CheckContextMatch(t2);
848 CheckContextMatch(t3);
849 return Expr.Create(
this,
Native.
Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
857 Contract.Requires(t1 != null);
858 Contract.Requires(t2 != null);
859 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
861 CheckContextMatch(t1);
862 CheckContextMatch(t2);
871 Contract.Requires(t1 != null);
872 Contract.Requires(t2 != null);
873 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
875 CheckContextMatch(t1);
876 CheckContextMatch(t2);
885 Contract.Requires(t1 != null);
886 Contract.Requires(t2 != null);
887 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
889 CheckContextMatch(t1);
890 CheckContextMatch(t2);
899 Contract.Requires(t != null);
900 Contract.Requires(Contract.ForAll(t, a => a != null));
901 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
903 CheckContextMatch(t);
912 Contract.Requires(t != null);
913 Contract.Requires(Contract.ForAll(t, a => a != null));
914 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
916 CheckContextMatch(t);
929 Contract.Requires(t != null);
930 Contract.Requires(Contract.ForAll(t, a => a != null));
931 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
933 CheckContextMatch(t);
942 Contract.Requires(t != null);
943 Contract.Requires(Contract.ForAll(t, a => a != null));
944 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
946 CheckContextMatch(t);
955 Contract.Requires(t != null);
956 Contract.Requires(Contract.ForAll(t, a => a != null));
957 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
959 CheckContextMatch(t);
968 Contract.Requires(t != null);
969 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
971 CheckContextMatch(t);
980 Contract.Requires(t1 != null);
981 Contract.Requires(t2 != null);
982 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
984 CheckContextMatch(t1);
985 CheckContextMatch(t2);
995 Contract.Requires(t1 != null);
996 Contract.Requires(t2 != null);
997 Contract.Ensures(Contract.Result<
IntExpr>() != null);
999 CheckContextMatch(t1);
1000 CheckContextMatch(t2);
1010 Contract.Requires(t1 != null);
1011 Contract.Requires(t2 != null);
1012 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1014 CheckContextMatch(t1);
1015 CheckContextMatch(t2);
1024 Contract.Requires(t1 != null);
1025 Contract.Requires(t2 != null);
1026 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
1028 CheckContextMatch(t1);
1029 CheckContextMatch(t2);
1038 Contract.Requires(t1 != null);
1039 Contract.Requires(t2 != null);
1040 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1042 CheckContextMatch(t1);
1043 CheckContextMatch(t2);
1052 Contract.Requires(t1 != null);
1053 Contract.Requires(t2 != null);
1054 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1056 CheckContextMatch(t1);
1057 CheckContextMatch(t2);
1066 Contract.Requires(t1 != null);
1067 Contract.Requires(t2 != null);
1068 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1070 CheckContextMatch(t1);
1071 CheckContextMatch(t2);
1080 Contract.Requires(t1 != null);
1081 Contract.Requires(t2 != null);
1082 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1084 CheckContextMatch(t1);
1085 CheckContextMatch(t2);
1101 Contract.Requires(t != null);
1102 Contract.Ensures(Contract.Result<
RealExpr>() != null);
1104 CheckContextMatch(t);
1117 Contract.Requires(t != null);
1118 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1120 CheckContextMatch(t);
1129 Contract.Requires(t != null);
1130 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1132 CheckContextMatch(t);
1144 Contract.Requires(t != null);
1145 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1147 CheckContextMatch(t);
1157 Contract.Requires(t != null);
1158 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1160 CheckContextMatch(t);
1170 Contract.Requires(t != null);
1171 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1173 CheckContextMatch(t);
1183 Contract.Requires(t1 != null);
1184 Contract.Requires(t2 != null);
1185 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1187 CheckContextMatch(t1);
1188 CheckContextMatch(t2);
1198 Contract.Requires(t1 != null);
1199 Contract.Requires(t2 != null);
1200 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1202 CheckContextMatch(t1);
1203 CheckContextMatch(t2);
1213 Contract.Requires(t1 != null);
1214 Contract.Requires(t2 != null);
1215 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1217 CheckContextMatch(t1);
1218 CheckContextMatch(t2);
1228 Contract.Requires(t1 != null);
1229 Contract.Requires(t2 != null);
1230 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1232 CheckContextMatch(t1);
1233 CheckContextMatch(t2);
1243 Contract.Requires(t1 != null);
1244 Contract.Requires(t2 != null);
1245 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1247 CheckContextMatch(t1);
1248 CheckContextMatch(t2);
1258 Contract.Requires(t1 != null);
1259 Contract.Requires(t2 != null);
1260 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1262 CheckContextMatch(t1);
1263 CheckContextMatch(t2);
1273 Contract.Requires(t != null);
1274 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1276 CheckContextMatch(t);
1286 Contract.Requires(t1 != null);
1287 Contract.Requires(t2 != null);
1288 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1290 CheckContextMatch(t1);
1291 CheckContextMatch(t2);
1301 Contract.Requires(t1 != null);
1302 Contract.Requires(t2 != null);
1303 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1305 CheckContextMatch(t1);
1306 CheckContextMatch(t2);
1316 Contract.Requires(t1 != null);
1317 Contract.Requires(t2 != null);
1318 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1320 CheckContextMatch(t1);
1321 CheckContextMatch(t2);
1336 Contract.Requires(t1 != null);
1337 Contract.Requires(t2 != null);
1338 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1340 CheckContextMatch(t1);
1341 CheckContextMatch(t2);
1360 Contract.Requires(t1 != null);
1361 Contract.Requires(t2 != null);
1362 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1364 CheckContextMatch(t1);
1365 CheckContextMatch(t2);
1379 Contract.Requires(t1 != null);
1380 Contract.Requires(t2 != null);
1381 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1383 CheckContextMatch(t1);
1384 CheckContextMatch(t2);
1400 Contract.Requires(t1 != null);
1401 Contract.Requires(t2 != null);
1402 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1404 CheckContextMatch(t1);
1405 CheckContextMatch(t2);
1418 Contract.Requires(t1 != null);
1419 Contract.Requires(t2 != null);
1420 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1422 CheckContextMatch(t1);
1423 CheckContextMatch(t2);
1435 Contract.Requires(t1 != null);
1436 Contract.Requires(t2 != null);
1437 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1439 CheckContextMatch(t1);
1440 CheckContextMatch(t2);
1452 Contract.Requires(t1 != null);
1453 Contract.Requires(t2 != null);
1454 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1456 CheckContextMatch(t1);
1457 CheckContextMatch(t2);
1469 Contract.Requires(t1 != null);
1470 Contract.Requires(t2 != null);
1471 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1473 CheckContextMatch(t1);
1474 CheckContextMatch(t2);
1486 Contract.Requires(t1 != null);
1487 Contract.Requires(t2 != null);
1488 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1490 CheckContextMatch(t1);
1491 CheckContextMatch(t2);
1503 Contract.Requires(t1 != null);
1504 Contract.Requires(t2 != null);
1505 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1507 CheckContextMatch(t1);
1508 CheckContextMatch(t2);
1520 Contract.Requires(t1 != null);
1521 Contract.Requires(t2 != null);
1522 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1524 CheckContextMatch(t1);
1525 CheckContextMatch(t2);
1537 Contract.Requires(t1 != null);
1538 Contract.Requires(t2 != null);
1539 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1541 CheckContextMatch(t1);
1542 CheckContextMatch(t2);
1554 Contract.Requires(t1 != null);
1555 Contract.Requires(t2 != null);
1556 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1558 CheckContextMatch(t1);
1559 CheckContextMatch(t2);
1575 Contract.Requires(t1 != null);
1576 Contract.Requires(t2 != null);
1577 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1579 CheckContextMatch(t1);
1580 CheckContextMatch(t2);
1595 Contract.Requires(t != null);
1596 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1598 CheckContextMatch(t);
1612 Contract.Requires(t != null);
1613 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1615 CheckContextMatch(t);
1630 Contract.Requires(t != null);
1631 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1633 CheckContextMatch(t);
1645 Contract.Requires(t != null);
1646 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1648 CheckContextMatch(t);
1666 Contract.Requires(t1 != null);
1667 Contract.Requires(t2 != null);
1668 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1670 CheckContextMatch(t1);
1671 CheckContextMatch(t2);
1689 Contract.Requires(t1 != null);
1690 Contract.Requires(t2 != null);
1691 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1693 CheckContextMatch(t1);
1694 CheckContextMatch(t2);
1714 Contract.Requires(t1 != null);
1715 Contract.Requires(t2 != null);
1716 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1718 CheckContextMatch(t1);
1719 CheckContextMatch(t2);
1732 Contract.Requires(t != null);
1733 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1735 CheckContextMatch(t);
1748 Contract.Requires(t != null);
1749 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1751 CheckContextMatch(t);
1764 Contract.Requires(t1 != null);
1765 Contract.Requires(t2 != null);
1766 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1768 CheckContextMatch(t1);
1769 CheckContextMatch(t2);
1782 Contract.Requires(t1 != null);
1783 Contract.Requires(t2 != null);
1784 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1786 CheckContextMatch(t1);
1787 CheckContextMatch(t2);
1803 Contract.Requires(t != null);
1804 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1806 CheckContextMatch(t);
1827 Contract.Requires(t != null);
1828 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1830 CheckContextMatch(t);
1842 Contract.Requires(t1 != null);
1843 Contract.Requires(t2 != null);
1844 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1846 CheckContextMatch(t1);
1847 CheckContextMatch(t2);
1859 Contract.Requires(t1 != null);
1860 Contract.Requires(t2 != null);
1861 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1863 CheckContextMatch(t1);
1864 CheckContextMatch(t2);
1876 Contract.Requires(t1 != null);
1877 Contract.Requires(t2 != null);
1878 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1880 CheckContextMatch(t1);
1881 CheckContextMatch(t2);
1893 Contract.Requires(t1 != null);
1894 Contract.Requires(t2 != null);
1895 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1897 CheckContextMatch(t1);
1898 CheckContextMatch(t2);
1910 Contract.Requires(t1 != null);
1911 Contract.Requires(t2 != null);
1912 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1914 CheckContextMatch(t1);
1915 CheckContextMatch(t2);
1927 Contract.Requires(t != null);
1928 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1930 CheckContextMatch(t);
1942 Contract.Requires(t1 != null);
1943 Contract.Requires(t2 != null);
1944 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1946 CheckContextMatch(t1);
1947 CheckContextMatch(t2);
1959 Contract.Requires(t1 != null);
1960 Contract.Requires(t2 != null);
1961 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1963 CheckContextMatch(t1);
1964 CheckContextMatch(t2);
1975 Contract.Requires(name != null);
1976 Contract.Requires(domain != null);
1977 Contract.Requires(range != null);
1978 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
1980 return (
ArrayExpr)MkConst(name, MkArraySort(domain, range));
1988 Contract.Requires(domain != null);
1989 Contract.Requires(range != null);
1990 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
1992 return (
ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
2010 Contract.Requires(a != null);
2011 Contract.Requires(i != null);
2012 Contract.Ensures(Contract.Result<
Expr>() != null);
2014 CheckContextMatch(a);
2015 CheckContextMatch(i);
2038 Contract.Requires(a != null);
2039 Contract.Requires(i != null);
2040 Contract.Requires(v != null);
2041 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2043 CheckContextMatch(a);
2044 CheckContextMatch(i);
2045 CheckContextMatch(v);
2060 Contract.Requires(domain != null);
2061 Contract.Requires(v != null);
2062 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2064 CheckContextMatch(domain);
2065 CheckContextMatch(v);
2082 Contract.Requires(f != null);
2083 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2084 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2086 CheckContextMatch(f);
2087 CheckContextMatch(args);
2100 Contract.Requires(array != null);
2101 Contract.Ensures(Contract.Result<
Expr>() != null);
2103 CheckContextMatch(array);
2114 Contract.Requires(ty != null);
2115 Contract.Ensures(Contract.Result<
SetSort>() != null);
2117 CheckContextMatch(ty);
2126 Contract.Requires(domain != null);
2127 Contract.Ensures(Contract.Result<
Expr>() != null);
2129 CheckContextMatch(domain);
2138 Contract.Requires(domain != null);
2139 Contract.Ensures(Contract.Result<
Expr>() != null);
2141 CheckContextMatch(domain);
2150 Contract.Requires(set != null);
2151 Contract.Requires(element != null);
2152 Contract.Ensures(Contract.Result<
Expr>() != null);
2154 CheckContextMatch(set);
2155 CheckContextMatch(element);
2165 Contract.Requires(set != null);
2166 Contract.Requires(element != null);
2167 Contract.Ensures(Contract.Result<
Expr>() != null);
2169 CheckContextMatch(set);
2170 CheckContextMatch(element);
2179 Contract.Requires(args != null);
2180 Contract.Requires(Contract.ForAll(args, a => a != null));
2182 CheckContextMatch(args);
2191 Contract.Requires(args != null);
2192 Contract.Requires(Contract.ForAll(args, a => a != null));
2193 Contract.Ensures(Contract.Result<
Expr>() != null);
2195 CheckContextMatch(args);
2204 Contract.Requires(arg1 != null);
2205 Contract.Requires(arg2 != null);
2206 Contract.Ensures(Contract.Result<
Expr>() != null);
2208 CheckContextMatch(arg1);
2209 CheckContextMatch(arg2);
2218 Contract.Requires(arg != null);
2219 Contract.Ensures(Contract.Result<
Expr>() != null);
2221 CheckContextMatch(arg);
2230 Contract.Requires(elem != null);
2231 Contract.Requires(set != null);
2232 Contract.Ensures(Contract.Result<
Expr>() != null);
2234 CheckContextMatch(elem);
2235 CheckContextMatch(set);
2244 Contract.Requires(arg1 != null);
2245 Contract.Requires(arg2 != null);
2246 Contract.Ensures(Contract.Result<
Expr>() != null);
2248 CheckContextMatch(arg1);
2249 CheckContextMatch(arg2);
2256 #region General Numerals
2257 public Expr MkNumeral(
string v,
Sort ty)
2265 Contract.Requires(ty != null);
2266 Contract.Ensures(Contract.Result<
Expr>() != null);
2268 CheckContextMatch(ty);
2281 Contract.Requires(ty != null);
2282 Contract.Ensures(Contract.Result<
Expr>() != null);
2284 CheckContextMatch(ty);
2297 Contract.Requires(ty != null);
2298 Contract.Ensures(Contract.Result<
Expr>() != null);
2300 CheckContextMatch(ty);
2313 Contract.Requires(ty != null);
2314 Contract.Ensures(Contract.Result<
Expr>() != null);
2316 CheckContextMatch(ty);
2329 Contract.Requires(ty != null);
2330 Contract.Ensures(Contract.Result<
Expr>() != null);
2332 CheckContextMatch(ty);
2338 public RatNum MkReal(
int num,
int den)
2350 Contract.Ensures(Contract.Result<
RatNum>() != null);
2351 Contract.EndContractBlock();
2363 Contract.Ensures(Contract.Result<
RatNum>() != null);
2375 Contract.Ensures(Contract.Result<
RatNum>() != null);
2387 Contract.Ensures(Contract.Result<
RatNum>() != null);
2399 Contract.Ensures(Contract.Result<
RatNum>() != null);
2411 Contract.Ensures(Contract.Result<
RatNum>() != null);
2418 public IntNum MkInt(
string v)
2424 Contract.Ensures(Contract.Result<
IntNum>() != null);
2436 Contract.Ensures(Contract.Result<
IntNum>() != null);
2448 Contract.Ensures(Contract.Result<
IntNum>() != null);
2460 Contract.Ensures(Contract.Result<
IntNum>() != null);
2472 Contract.Ensures(Contract.Result<
IntNum>() != null);
2479 public BitVecNum MkBV(
string v, uint size)
2486 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2488 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2498 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2500 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2510 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2512 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2522 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2524 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2534 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2536 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2540 #endregion // Numerals
2564 Contract.Requires(sorts != null);
2565 Contract.Requires(names != null);
2566 Contract.Requires(body != null);
2567 Contract.Requires(sorts.Length == names.Length);
2568 Contract.Requires(Contract.ForAll(sorts, s => s != null));
2569 Contract.Requires(Contract.ForAll(names, n => n != null));
2570 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2571 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2573 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2575 return new Quantifier(
this,
true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2584 Contract.Requires(body != null);
2585 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
2586 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2587 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2589 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2591 return new Quantifier(
this,
true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2600 Contract.Requires(sorts != null);
2601 Contract.Requires(names != null);
2602 Contract.Requires(body != null);
2603 Contract.Requires(sorts.Length == names.Length);
2604 Contract.Requires(Contract.ForAll(sorts, s => s != null));
2605 Contract.Requires(Contract.ForAll(names, n => n != null));
2606 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2607 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2608 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2610 return new Quantifier(
this,
false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2618 Contract.Requires(body != null);
2619 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2620 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2621 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2622 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2624 return new Quantifier(
this,
false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2633 Contract.Requires(body != null);
2634 Contract.Requires(names != null);
2635 Contract.Requires(sorts != null);
2636 Contract.Requires(sorts.Length == names.Length);
2637 Contract.Requires(Contract.ForAll(sorts, s => s != null));
2638 Contract.Requires(Contract.ForAll(names, n => n != null));
2639 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2640 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2642 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2645 return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2647 return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2656 Contract.Requires(body != null);
2657 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2658 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2659 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2661 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2664 return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2666 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2696 #region SMT Files & Strings
2697 public string BenchmarkToSMTString(
string name,
string logic,
string status,
string attributes,
2710 Contract.Requires(assumptions != null);
2711 Contract.Requires(formula != null);
2712 Contract.Ensures(Contract.Result<
string>() != null);
2715 (uint)assumptions.Length,
AST.ArrayToNative(assumptions),
2716 formula.NativeObject);
2731 uint csn =
Symbol.ArrayLength(sortNames);
2732 uint cs =
Sort.ArrayLength(sorts);
2733 uint cdn =
Symbol.ArrayLength(declNames);
2734 uint cd =
AST.ArrayLength(decls);
2735 if (csn != cs || cdn != cd)
2738 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
2739 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls));
2748 uint csn =
Symbol.ArrayLength(sortNames);
2749 uint cs =
Sort.ArrayLength(sorts);
2750 uint cdn =
Symbol.ArrayLength(declNames);
2751 uint cd =
AST.ArrayLength(decls);
2752 if (csn != cs || cdn != cd)
2755 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
2756 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls));
2771 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
2773 uint n = NumSMTLIBFormulas;
2775 for (uint i = 0; i < n; i++)
2789 public BoolExpr[] SMTLIBAssumptions
2793 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
2795 uint n = NumSMTLIBAssumptions;
2797 for (uint i = 0; i < n; i++)
2815 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
2817 uint n = NumSMTLIBDecls;
2819 for (uint i = 0; i < n; i++)
2833 public Sort[] SMTLIBSorts
2837 Contract.Ensures(Contract.Result<
Sort[]>() != null);
2839 uint n = NumSMTLIBSorts;
2841 for (uint i = 0; i < n; i++)
2854 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2856 uint csn =
Symbol.ArrayLength(sortNames);
2857 uint cs =
Sort.ArrayLength(sorts);
2858 uint cdn =
Symbol.ArrayLength(declNames);
2859 uint cd =
AST.ArrayLength(decls);
2860 if (csn != cs || cdn != cd)
2863 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
2864 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls)));
2873 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2875 uint csn =
Symbol.ArrayLength(sortNames);
2876 uint cs =
Sort.ArrayLength(sorts);
2877 uint cdn =
Symbol.ArrayLength(declNames);
2878 uint cd =
AST.ArrayLength(decls);
2879 if (csn != cs || cdn != cd)
2882 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
2883 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls)));
2888 public Goal MkGoal(
bool models =
true,
bool unsatCores =
false,
bool proofs =
false)
2900 Contract.Ensures(Contract.Result<
Goal>() != null);
2902 return new Goal(
this, models, unsatCores, proofs);
2906 #region ParameterSets
2907 public Params MkParams()
2912 Contract.Ensures(Contract.Result<Params>() != null);
2914 return new Params(
this);
2919 public uint NumTactics
2930 public string[] TacticNames
2934 Contract.Ensures(Contract.Result<
string[]>() != null);
2936 uint n = NumTactics;
2937 string[] res =
new string[n];
2938 for (uint i = 0; i < n; i++)
2949 Contract.Ensures(Contract.Result<
string>() != null);
2959 Contract.Ensures(Contract.Result<
Tactic>() != null);
2961 return new Tactic(
this, name);
2970 Contract.Requires(t1 != null);
2971 Contract.Requires(t2 != null);
2972 Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
2973 Contract.Ensures(Contract.Result<
Tactic>() != null);
2976 CheckContextMatch(t1);
2977 CheckContextMatch(t2);
2978 CheckContextMatch(ts);
2980 IntPtr last = IntPtr.Zero;
2981 if (ts != null && ts.Length > 0)
2983 last = ts[ts.Length - 1].NativeObject;
2984 for (
int i = ts.Length - 2; i >= 0; i--)
2987 if (last != IntPtr.Zero)
3005 Contract.Requires(t1 != null);
3006 Contract.Requires(t2 != null);
3007 Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3008 Contract.Ensures(Contract.Result<
Tactic>() != null);
3019 Contract.Requires(t1 != null);
3020 Contract.Requires(t2 != null);
3021 Contract.Ensures(Contract.Result<
Tactic>() != null);
3023 CheckContextMatch(t1);
3024 CheckContextMatch(t2);
3036 Contract.Requires(t != null);
3037 Contract.Ensures(Contract.Result<
Tactic>() != null);
3039 CheckContextMatch(t);
3052 Contract.Requires(p != null);
3053 Contract.Requires(t != null);
3054 Contract.Ensures(Contract.Result<
Tactic>() != null);
3056 CheckContextMatch(t);
3057 CheckContextMatch(p);
3067 Contract.Requires(p != null);
3068 Contract.Requires(t1 != null);
3069 Contract.Requires(t2 != null);
3070 Contract.Ensures(Contract.Result<
Tactic>() != null);
3072 CheckContextMatch(p);
3073 CheckContextMatch(t1);
3074 CheckContextMatch(t2);
3084 Contract.Requires(t != null);
3085 Contract.Ensures(Contract.Result<
Tactic>() != null);
3087 CheckContextMatch(t);
3096 Contract.Ensures(Contract.Result<
Tactic>() != null);
3106 Contract.Ensures(Contract.Result<
Tactic>() != null);
3116 Contract.Requires(p != null);
3117 Contract.Ensures(Contract.Result<
Tactic>() != null);
3119 CheckContextMatch(p);
3129 Contract.Ensures(Contract.Result<
Tactic>() != null);
3139 Contract.Requires(t != null);
3140 Contract.Requires(p != null);
3141 Contract.Ensures(Contract.Result<
Tactic>() != null);
3143 CheckContextMatch(t);
3144 CheckContextMatch(p);
3154 Contract.Requires(t != null);
3155 Contract.Requires(p != null);
3156 Contract.Ensures(Contract.Result<
Tactic>() != null);
3158 return UsingParams(t, p);
3166 Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3167 Contract.Ensures(Contract.Result<
Tactic>() != null);
3169 CheckContextMatch(t);
3179 Contract.Requires(t1 != null);
3180 Contract.Requires(t2 != null);
3181 Contract.Ensures(Contract.Result<
Tactic>() != null);
3183 CheckContextMatch(t1);
3184 CheckContextMatch(t2);
3199 public uint NumProbes
3210 public string[] ProbeNames
3214 Contract.Ensures(Contract.Result<
string[]>() != null);
3217 string[] res =
new string[n];
3218 for (uint i = 0; i < n; i++)
3229 Contract.Ensures(Contract.Result<
string>() != null);
3239 Contract.Ensures(Contract.Result<
Probe>() != null);
3241 return new Probe(
this, name);
3249 Contract.Ensures(Contract.Result<
Probe>() != null);
3260 Contract.Requires(p1 != null);
3261 Contract.Requires(p2 != null);
3262 Contract.Ensures(Contract.Result<
Probe>() != null);
3264 CheckContextMatch(p1);
3265 CheckContextMatch(p2);
3275 Contract.Requires(p1 != null);
3276 Contract.Requires(p2 != null);
3277 Contract.Ensures(Contract.Result<
Probe>() != null);
3279 CheckContextMatch(p1);
3280 CheckContextMatch(p2);
3290 Contract.Requires(p1 != null);
3291 Contract.Requires(p2 != null);
3292 Contract.Ensures(Contract.Result<
Probe>() != null);
3294 CheckContextMatch(p1);
3295 CheckContextMatch(p2);
3305 Contract.Requires(p1 != null);
3306 Contract.Requires(p2 != null);
3307 Contract.Ensures(Contract.Result<
Probe>() != null);
3309 CheckContextMatch(p1);
3310 CheckContextMatch(p2);
3320 Contract.Requires(p1 != null);
3321 Contract.Requires(p2 != null);
3322 Contract.Ensures(Contract.Result<
Probe>() != null);
3324 CheckContextMatch(p1);
3325 CheckContextMatch(p2);
3335 Contract.Requires(p1 != null);
3336 Contract.Requires(p2 != null);
3337 Contract.Ensures(Contract.Result<
Probe>() != null);
3339 CheckContextMatch(p1);
3340 CheckContextMatch(p2);
3350 Contract.Requires(p1 != null);
3351 Contract.Requires(p2 != null);
3352 Contract.Ensures(Contract.Result<
Probe>() != null);
3354 CheckContextMatch(p1);
3355 CheckContextMatch(p2);
3365 Contract.Requires(p != null);
3366 Contract.Ensures(Contract.Result<
Probe>() != null);
3368 CheckContextMatch(p);
3384 Contract.Ensures(Contract.Result<
Solver>() != null);
3398 Contract.Ensures(Contract.Result<
Solver>() != null);
3400 return MkSolver(MkSymbol(logic));
3408 Contract.Ensures(Contract.Result<
Solver>() != null);
3422 Contract.Requires(t != null);
3423 Contract.Ensures(Contract.Result<
Solver>() != null);
3435 Contract.Ensures(Contract.Result<
Fixedpoint>() != null);
3441 #region Floating-Point Arithmetic
3443 #region Rounding Modes
3444 #region RoundingMode Sort
3445 public FPRMSort MkFPRoundingModeSort()
3450 Contract.Ensures(Contract.Result<FPRMSort>() != null);
3451 return new FPRMSort(
this);
3456 public FPRMExpr MkFPRoundNearestTiesToEven()
3461 Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3462 return new FPRMExpr(
this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
3470 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3479 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3488 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3497 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3506 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3515 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3524 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3533 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3542 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3548 #region FloatingPoint Sorts
3549 public FPSort MkFPSort(uint ebits, uint sbits)
3556 Contract.Ensures(Contract.Result<
FPSort>() != null);
3557 return new FPSort(
this, ebits, sbits);
3565 Contract.Ensures(Contract.Result<
FPSort>() != null);
3574 Contract.Ensures(Contract.Result<
FPSort>() != null);
3583 Contract.Ensures(Contract.Result<
FPSort>() != null);
3592 Contract.Ensures(Contract.Result<
FPSort>() != null);
3601 Contract.Ensures(Contract.Result<
FPSort>() != null);
3610 Contract.Ensures(Contract.Result<
FPSort>() != null);
3619 Contract.Ensures(Contract.Result<
FPSort>() != null);
3628 Contract.Ensures(Contract.Result<
FPSort>() != null);
3640 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3651 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3662 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3673 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3684 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3695 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3708 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3721 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3732 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3733 return MkFPNumeral(v, s);
3743 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3744 return MkFPNumeral(v, s);
3754 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3755 return MkFPNumeral(v, s);
3767 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3768 return MkFPNumeral(sgn, exp, sig, s);
3780 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3781 return MkFPNumeral(sgn, exp, sig, s);
3793 Contract.Ensures(Contract.Result<
FPNum>() != null);
3803 Contract.Ensures(Contract.Result<
FPNum>() != null);
3815 Contract.Ensures(Contract.Result<
FPNum>() != null);
3827 Contract.Ensures(Contract.Result<
FPNum>() != null);
3839 Contract.Ensures(Contract.Result<
FPNum>() != null);
3851 Contract.Ensures(Contract.Result<
FPNum>() != null);
3867 Contract.Ensures(Contract.Result<
FPNum>() != null);
3868 return new FPExpr(
this,
Native.
Z3_mk_fpa_fma(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
3878 Contract.Ensures(Contract.Result<
FPNum>() != null);
3889 Contract.Ensures(Contract.Result<
FPNum>() != null);
3901 Contract.Ensures(Contract.Result<
FPNum>() != null);
3912 Contract.Ensures(Contract.Result<
FPNum>() != null);
3923 Contract.Ensures(Contract.Result<
FPNum>() != null);
3934 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
3945 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
3956 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
3967 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
3981 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
3991 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4001 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4011 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4021 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4031 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4041 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4051 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4056 #region Conversions to FloatingPoint terms
4072 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4089 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4106 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4123 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4142 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4161 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4166 #region Conversions from FloatingPoint terms
4181 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
4199 Contract.Ensures(Contract.Result<
RealExpr>() != null);
4204 #region Z3-specific extensions
4217 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
4235 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
4239 #endregion // Floating-point Arithmetic
4241 #region Miscellaneous
4242 public AST WrapAST(IntPtr nativeObject)
4254 Contract.Ensures(Contract.Result<
AST>() != null);
4255 return AST.Create(
this, nativeObject);
4271 return a.NativeObject;
4279 Contract.Ensures(Contract.Result<
string>() != null);
4293 #region Error Handling
4310 public void UpdateParamValue(
string id,
string value)
4327 internal IntPtr m_ctx = IntPtr.Zero;
4328 internal Native.Z3_error_handler m_n_err_handler = null;
4329 internal IntPtr nCtx {
get {
return m_ctx; } }
4331 internal void NativeErrorHandler(IntPtr ctx,
Z3_error_code errorCode)
4336 internal void InitContext()
4339 m_n_err_handler =
new Native.Z3_error_handler(NativeErrorHandler);
4340 Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
4341 GC.SuppressFinalize(
this);
4345 internal void CheckContextMatch(Z3Object other)
4347 Contract.Requires(other != null);
4349 if (!ReferenceEquals(
this, other.Context))
4350 throw new Z3Exception(
"Context mismatch");
4354 internal void CheckContextMatch(Z3Object[] arr)
4356 Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
4360 foreach (Z3Object a
in arr)
4362 Contract.Assert(a != null);
4363 CheckContextMatch(a);
4368 [ContractInvariantMethod]
4369 private void ObjectInvariant()
4371 Contract.Invariant(m_AST_DRQ != null);
4372 Contract.Invariant(m_ASTMap_DRQ != null);
4373 Contract.Invariant(m_ASTVector_DRQ != null);
4374 Contract.Invariant(m_ApplyResult_DRQ != null);
4375 Contract.Invariant(m_FuncEntry_DRQ != null);
4376 Contract.Invariant(m_FuncInterp_DRQ != null);
4377 Contract.Invariant(m_Goal_DRQ != null);
4378 Contract.Invariant(m_Model_DRQ != null);
4379 Contract.Invariant(m_Params_DRQ != null);
4380 Contract.Invariant(m_ParamDescrs_DRQ != null);
4381 Contract.Invariant(m_Probe_DRQ != null);
4382 Contract.Invariant(m_Solver_DRQ != null);
4383 Contract.Invariant(m_Statistics_DRQ != null);
4384 Contract.Invariant(m_Tactic_DRQ != null);
4385 Contract.Invariant(m_Fixedpoint_DRQ != null);
4388 readonly
private AST.DecRefQueue m_AST_DRQ =
new AST.DecRefQueue();
4389 readonly
private ASTMap.DecRefQueue m_ASTMap_DRQ =
new ASTMap.DecRefQueue(10);
4390 readonly
private ASTVector.DecRefQueue m_ASTVector_DRQ =
new ASTVector.DecRefQueue(10);
4391 readonly
private ApplyResult.DecRefQueue m_ApplyResult_DRQ =
new ApplyResult.DecRefQueue(10);
4392 readonly
private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ =
new FuncInterp.Entry.DecRefQueue(10);
4393 readonly
private FuncInterp.DecRefQueue m_FuncInterp_DRQ =
new FuncInterp.DecRefQueue(10);
4394 readonly
private Goal.DecRefQueue m_Goal_DRQ =
new Goal.DecRefQueue(10);
4395 readonly
private Model.DecRefQueue m_Model_DRQ =
new Model.DecRefQueue(10);
4396 readonly
private Params.DecRefQueue m_Params_DRQ =
new Params.DecRefQueue(10);
4397 readonly
private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ =
new ParamDescrs.DecRefQueue(10);
4398 readonly
private Probe.DecRefQueue m_Probe_DRQ =
new Probe.DecRefQueue(10);
4399 readonly
private Solver.DecRefQueue m_Solver_DRQ =
new Solver.DecRefQueue(10);
4400 readonly
private Statistics.DecRefQueue m_Statistics_DRQ =
new Statistics.DecRefQueue(10);
4401 readonly
private Tactic.DecRefQueue m_Tactic_DRQ =
new Tactic.DecRefQueue(10);
4402 readonly
private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ =
new Fixedpoint.DecRefQueue(10);
4412 public IDecRefQueue ASTMap_DRQ {
get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null);
return m_ASTMap_DRQ; } }
4480 internal long refCount = 0;
4492 m_n_err_handler = null;
4494 m_ctx = IntPtr.Zero;
4497 GC.ReRegisterForFinalize(
this);
4506 AST_DRQ.Clear(
this);
4507 ASTMap_DRQ.Clear(
this);
4508 ASTVector_DRQ.Clear(
this);
4509 ApplyResult_DRQ.Clear(
this);
4510 FuncEntry_DRQ.Clear(
this);
4511 FuncInterp_DRQ.Clear(
this);
4512 Goal_DRQ.Clear(
this);
4513 Model_DRQ.Clear(
this);
4514 Params_DRQ.Clear(
this);
4515 ParamDescrs_DRQ.Clear(
this);
4516 Probe_DRQ.Clear(
this);
4517 Solver_DRQ.Clear(
this);
4518 Statistics_DRQ.Clear(
this);
4519 Tactic_DRQ.Clear(
this);
4520 Fixedpoint_DRQ.Clear(
this);
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
static Z3_ast Z3_mk_bvmul(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_solver Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1)
static Z3_sort Z3_mk_fpa_sort_64(Z3_context a0)
BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
Two's complement signed remainder (sign follows divisor).
string SimplifyHelp()
Return a string describing all available parameters to Expr.Simplify.
static Z3_ast Z3_mk_bvadd_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
static string Z3_get_tactic_name(Z3_context a0, uint a1)
static Z3_ast Z3_mk_fpa_abs(Z3_context a0, Z3_ast a1)
BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
Floating-point less than or equal.
static Z3_tactic Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
FPExpr MkFPRem(FPExpr t1, FPExpr t2)
Floating-point remainder
static Z3_ast Z3_mk_fpa_round_to_integral(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_get_smtlib_formula(Z3_context a0, uint a1)
static Z3_ast Z3_mk_bvneg_no_overflow(Z3_context a0, Z3_ast a1)
BoolExpr MkIsInteger(RealExpr t)
Creates an expression that checks whether a real number is an integer.
static Z3_tactic Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort...
FPRMNum MkFPRNE()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode...
Expr MkSetMembership(Expr elem, Expr set)
Check for set membership.
static Z3_ast Z3_mk_fpa_to_real(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_real2int(Z3_context a0, Z3_ast a1)
FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point division
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
Bitwise conjunction.
static Z3_ast Z3_mk_fpa_to_ubv(Z3_context a0, Z3_ast a1, Z3_ast a2, uint a3)
static Z3_ast Z3_mk_set_intersect(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static Z3_ast Z3_mk_bvuge(Z3_context a0, Z3_ast a1, Z3_ast a2)
DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
Create a new datatype sort.
Expr MkNumeral(uint v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
static Z3_ast Z3_mk_mul(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Tactic MkTactic(string name)
Creates a new Tactic.
static Z3_ast Z3_mk_mod(Z3_context a0, Z3_ast a1, Z3_ast a2)
UninterpretedSort MkUninterpretedSort(string str)
Create a new uninterpreted sort.
RealExpr MkFPToReal(FPExpr t)
Conversion of a floating-point term into a real-numbered term.
FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
Create a new finite domain sort.
static Z3_ast Z3_mk_empty_set(Z3_context a0, Z3_sort a1)
static Z3_ast Z3_mk_fpa_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
FPRMNum MkFPRTN()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode...
ArrayExpr MkConstArray(Sort domain, Expr v)
Create a constant array.
string ProbeDescription(string name)
Returns a string containing a description of the probe with the given name.
static Z3_ast Z3_mk_fpa_to_fp_float(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Floating-point fused multiply-add
BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
Unsigned greater than or equal to.
static Z3_ast Z3_mk_fpa_to_fp_signed(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
RatNum MkReal(string v)
Create a real numeral.
Expr MkFreshConst(string prefix, Sort range)
Creates a fresh Constant of sort range and a name prefixed with prefix .
static Z3_tactic Z3_tactic_par_or(Z3_context a0, uint a1, [In] Z3_tactic[] a2)
FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two integers.
static Z3_ast Z3_mk_bvashr(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_parse_smtlib_string(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
static Z3_ast Z3_mk_bv2int(Z3_context a0, Z3_ast a1, int a2)
static string Z3_tactic_get_descr(Z3_context a0, string a1)
BitVecNum MkBV(long v, uint size)
Create a bit-vector numeral.
FPExpr MkFPMax(FPExpr t1, FPExpr t2)
Maximum of floating-point numbers.
static Z3_ast Z3_mk_fpa_is_normal(Z3_context a0, Z3_ast a1)
Probe Not(Probe p)
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
static Z3_ast Z3_mk_fpa_numeral_int_uint(Z3_context a0, int a1, int a2, uint a3, Z3_sort a4)
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Unsigned division.
Tactic When(Probe p, Tactic t)
Create a tactic that applies t to a given goal if the probe p evaluates to true.
Tactic Repeat(Tactic t, uint max=uint.MaxValue)
Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number o...
BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater than or equal to.
static Z3_ast Z3_mk_fpa_max(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_probe Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2)
BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
Bit-vector extraction.
static Z3_ast Z3_mk_fresh_const(Z3_context a0, string a1, Z3_sort a2)
Probe Ge(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value returned by p1 is greater than or equal the v...
IntExpr MkIntConst(Symbol name)
Creates an integer constant.
static uint Z3_get_num_probes(Z3_context a0)
BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
Parse the given string using the SMT-LIB2 parser.
static Z3_ast Z3_mk_bvmul_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_fpa_geq(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvshl(Z3_context a0, Z3_ast a1, Z3_ast a2)
IntNum MkInt(int v)
Create an integer numeral.
Tactic ParOr(params Tactic[] t)
Create a tactic that applies the given tactics in parallel.
BitVecExpr MkBVNeg(BitVecExpr t)
Standard two's complement unary minus.
static Z3_sort Z3_mk_fpa_sort_128(Z3_context a0)
static Z3_probe Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2)
ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
Maps f on the argument arrays.
Z3_error_code
Z3 error codes (See Z3_get_error_code).
static Z3_ast Z3_mk_real(Z3_context a0, int a1, int a2)
static Z3_ast Z3_mk_fpa_numeral_float(Z3_context a0, float a1, Z3_sort a2)
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
void Interrupt()
Interrupt the execution of a Z3 procedure.
Probe Le(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value returned by p1 is less than or equal the valu...
Objects of this class track statistical information about solvers.
FPRMNum MkFPRTZ()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode...
static Z3_tactic Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3)
FPNum MkFPInf(FPSort s, bool negative)
Create a floating-point infinity of sort s.
Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
Create an expression representing an if-then-else: ite(t1, t2, t3).
Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create an existential Quantifier.
Expr MkNumeral(ulong v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
static Z3_ast Z3_mk_or(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
Create a new finite domain sort.
Expr MkConst(string name, Sort range)
Creates a new Constant of sort range and named name .
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
Creates a new function declaration.
static Z3_ast Z3_mk_fpa_to_fp_int_real(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3, Z3_sort a4)
BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
Unsigned greater-than.
FPSort MkFPSortSingle()
Create the single-precision (32-bit) FloatingPoint sort.
Floating-point rounding mode numerals
static Z3_probe Z3_probe_eq(Z3_context a0, Z3_probe a1, Z3_probe a2)
BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than or equal to.
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
static Z3_ast Z3_mk_fpa_is_negative(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_fpa_round_nearest_ties_to_away(Z3_context a0)
static Z3_ast Z3_mk_bvredand(Z3_context a0, Z3_ast a1)
BoolExpr MkBoolConst(Symbol name)
Create a Boolean constant.
IntNum MkInt(uint v)
Create an integer numeral.
static Z3_ast Z3_mk_fpa_fp(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 ...
void ParseSMTLIBString(string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
Parse the given string using the SMT-LIB parser.
Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create an existential Quantifier.
BoolExpr MkEq(Expr x, Expr y)
Creates the equality x = y .
Probe And(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".
static Z3_ast Z3_mk_fpa_leq(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_tactic Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, uint a2)
Expr MkSetAdd(Expr set, Expr element)
Add an element to the set.
static Z3_tactic Z3_tactic_fail(Z3_context a0)
Expr MkEmptySet(Sort domain)
Create an empty set.
static Z3_ast Z3_mk_fpa_round_toward_negative(Z3_context a0)
static Z3_ast Z3_mk_implies(Z3_context a0, Z3_ast a1, Z3_ast a2)
ListSort MkListSort(Symbol name, Sort elemSort)
Create a new list sort.
BoolExpr MkFPIsNaN(FPExpr t)
Predicate indicating whether t is a NaN.
static Z3_solver Z3_mk_solver(Z3_context a0)
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
static Z3_ast Z3_mk_fpa_numeral_int64_uint64(Z3_context a0, int a1, Int64 a2, UInt64 a3, Z3_sort a4)
DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
Create mutually recursive data-types.
static string Z3_simplify_get_help(Z3_context a0)
static Z3_ast Z3_mk_set_add(Z3_context a0, Z3_ast a1, Z3_ast a2)
Tactics are the basic building block for creating custom solvers for specific problem domains...
Expr MkSetDifference(Expr arg1, Expr arg2)
Take the difference between two sets.
static Z3_ast Z3_mk_zero_ext(Z3_context a0, uint a1, Z3_ast a2)
FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two integers.
static Z3_ast Z3_mk_le(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_probe Z3_probe_const(Z3_context a0, double a1)
static Z3_ast Z3_mk_set_subset(Z3_context a0, Z3_ast a1, Z3_ast a2)
FPRMNum MkFPRoundTowardZero()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode...
FPSort MkFPSort16()
Create the half-precision (16-bit) FloatingPoint sort.
static Z3_ast Z3_mk_fpa_fma(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3, Z3_ast a4)
FPNum MkFP(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
Creates a fresh function declaration with a name prefixed with prefix .
BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise subtraction does not overflow.
BoolExpr MkBoolConst(string name)
Create a Boolean constant.
BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise signed division does not overflow.
FuncDecl MkFreshConstDecl(string prefix, Sort range)
Creates a fresh constant function declaration with a name prefixed with prefix .
FuncDecl MkConstDecl(Symbol name, Sort range)
Creates a new constant function declaration.
static Z3_ast Z3_mk_bvudiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
Solver MkSolver(string logic)
Creates a new (incremental) solver.
BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Rotate Right.
Probe Lt(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value returned by p1 is less than the value returne...
static Z3_ast Z3_mk_fpa_inf(Z3_context a0, Z3_sort a1, int a2)
static Z3_ast Z3_mk_fpa_is_infinite(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_fpa_to_sbv(Z3_context a0, Z3_ast a1, Z3_ast a2, uint a3)
Expr MkNumeral(long v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
static Z3_ast Z3_mk_is_int(Z3_context a0, Z3_ast a1)
RatNum MkReal(int v)
Create a real numeral.
static Z3_ast Z3_mk_not(Z3_context a0, Z3_ast a1)
FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
Creates a new function declaration.
Expr MkSetComplement(Expr arg)
Take the complement of a set.
static Z3_ast Z3_mk_bvredor(Z3_context a0, Z3_ast a1)
FPExpr MkFPNeg(FPExpr t)
Floating-point negation
DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
Create a new datatype sort.
static void Z3_interrupt(Z3_context a0)
BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XNOR.
BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Rotate Left.
BitVecExpr MkBVRedAND(BitVecExpr t)
Take conjunction of bits in a vector, return vector of length 1.
static Z3_ast Z3_mk_bvand(Z3_context a0, Z3_ast a1, Z3_ast a2)
BoolExpr MkFPIsInfinite(FPExpr t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.
BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than
FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
static Z3_ast Z3_mk_sub(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static Z3_func_decl Z3_get_smtlib_decl(Z3_context a0, uint a1)
RealExpr MkRealConst(string name)
Creates a real constant.
static Z3_sort Z3_mk_bv_sort(Z3_context a0, uint a1)
Expr MkSetIntersection(params Expr[] args)
Take the intersection of a list of sets.
RealSort MkRealSort()
Create a real sort.
Expr MkSetUnion(params Expr[] args)
Take the union of a list of sets.
FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
static string Z3_probe_get_descr(Z3_context a0, string a1)
BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise NOR.
static void Z3_set_ast_print_mode(Z3_context a0, uint a1)
string TacticDescription(string name)
Returns a string containing a description of the tactic with the given name.
Expr MkNumeral(int v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
Expr MkSetDel(Expr set, Expr element)
Remove an element from a set.
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Conversion of a floating-point number to another FloatingPoint sort s.
static string Z3_get_probe_name(Z3_context a0, uint a1)
static Z3_ast Z3_mk_sign_ext(Z3_context a0, uint a1, Z3_ast a2)
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
FuncDecl MkConstDecl(string name, Sort range)
Creates a new constant function declaration.
Tactic ParAndThen(Tactic t1, Tactic t2)
Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 ...
BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
Two's complement addition.
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Signed division.
Solver MkSolver(Tactic t)
Creates a solver that is implemented using the given tactic.
ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
Create an array constant.
static Z3_ast Z3_mk_fpa_to_fp_unsigned(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
static Z3_ast Z3_mk_bvsrem(Z3_context a0, Z3_ast a1, Z3_ast a2)
StringSymbol MkSymbol(string name)
Create a symbol using a string.
static Z3_ast Z3_parse_smtlib2_string(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
static Z3_ast Z3_mk_repeat(Z3_context a0, uint a1, Z3_ast a2)
FPSort MkFPSort128()
Create the quadruple-precision (128-bit) FloatingPoint sort.
static Z3_ast Z3_mk_fpa_rtn(Z3_context a0)
BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XOR.
BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Logical shift right
BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise subtraction does not underflow.
BitVecExpr MkSignExt(uint i, BitVecExpr t)
Bit-vector sign extension.
static Z3_sort Z3_mk_fpa_sort_half(Z3_context a0)
static Z3_ast Z3_mk_unsigned_int(Z3_context a0, uint a1, Z3_sort a2)
static Z3_ast Z3_mk_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvxnor(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_context Z3_mk_context_rc(Z3_config a0)
static Z3_ast Z3_mk_bvadd_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_set_del(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_ext_rotate_left(Z3_context a0, Z3_ast a1, Z3_ast a2)
static string Z3_benchmark_to_smtlib_string(Z3_context a0, string a1, string a2, string a3, string a4, uint a5, [In] Z3_ast[] a6, Z3_ast a7)
FPNum MkFPZero(FPSort s, bool negative)
Create a floating-point zero of sort s.
static Z3_ast Z3_mk_bvsdiv_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise addition does not underflow.
static Z3_ast Z3_mk_bvule(Z3_context a0, Z3_ast a1, Z3_ast a2)
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
static Z3_ast Z3_mk_fpa_sub(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point addition
FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
static Z3_ast Z3_mk_bvslt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_power(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvmul_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater-than.
static Z3_ast Z3_mk_const_array(Z3_context a0, Z3_sort a1, Z3_ast a2)
static Z3_ast Z3_mk_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise multiplication does not overflow.
static Z3_ast Z3_mk_xor(Z3_context a0, Z3_ast a1, Z3_ast a2)
BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
Floating-point equality.
Constructors are used for datatype sorts.
Probe MkProbe(string name)
Creates a new Probe.
static Z3_ast Z3_mk_ite(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
Shift left.
static Z3_ast Z3_mk_bvadd(Z3_context a0, Z3_ast a1, Z3_ast a2)
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
Bitwise disjunction.
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
static Z3_ast Z3_mk_fpa_rem(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_parse_smtlib_file(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
FloatingPoint Expressions
BitVecExpr MkBVConst(Symbol name, uint size)
Creates a bit-vector constant.
FPNum MkFP(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
static Z3_ast Z3_mk_iff(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_and(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static Z3_ast Z3_mk_unsigned_int64(Z3_context a0, UInt64 a1, Z3_sort a2)
static Z3_ast Z3_mk_distinct(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Tactic OrElse(Tactic t1, Tactic t2)
Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 appli...
static Z3_ast Z3_mk_select(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_int2bv(Z3_context a0, uint a1, Z3_ast a2)
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
static Z3_param_descrs Z3_simplify_get_param_descrs(Z3_context a0)
static Z3_tactic Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
BoolSort MkBoolSort()
Create a new Boolean sort.
BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
Arithmetic shift right
FPRMNum MkFPRoundNearestTiesToAway()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
static Z3_ast Z3_mk_fpa_rtp(Z3_context a0)
static Z3_sort Z3_mk_fpa_sort_16(Z3_context a0)
BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than or equal to.
static Z3_ast Z3_mk_false(Z3_context a0)
BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
Rotate Right.
static Z3_ast Z3_mk_bound(Z3_context a0, uint a1, Z3_sort a2)
static Z3_ast Z3_mk_fpa_rtz(Z3_context a0)
EnumSort MkEnumSort(string name, params string[] enumNames)
Create a new enumeration sort.
static Z3_ast Z3_mk_bvnor(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_probe Z3_probe_not(Z3_context a0, Z3_probe a1)
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
static Z3_ast Z3_mk_fpa_nan(Z3_context a0, Z3_sort a1)
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 -> t2.
static Z3_tactic Z3_tactic_fail_if(Z3_context a0, Z3_probe a1)
BoolExpr MkFPIsNegative(FPExpr t)
Predicate indicating whether t is a negative floating-point number.
static Z3_ast Z3_mk_bvsgt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_probe Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2)
BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise multiplication does not underflow.
static Z3_ast Z3_mk_fpa_numeral_double(Z3_context a0, double a1, Z3_sort a2)
static Z3_ast Z3_mk_bvxor(Z3_context a0, Z3_ast a1, Z3_ast a2)
FPRMNum MkFPRoundTowardPositive()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode...
FPSort MkFPSortDouble()
Create the double-precision (64-bit) FloatingPoint sort.
static uint Z3_get_smtlib_num_decls(Z3_context a0)
BitVecExpr MkRepeat(uint i, BitVecExpr t)
Bit-vector repetition.
Constructor MkConstructor(string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
Create a datatype constructor.
static Z3_ast Z3_mk_unary_minus(Z3_context a0, Z3_ast a1)
Expr MkSetSubset(Expr arg1, Expr arg2)
Check for subsetness of sets.
static Z3_sort Z3_mk_fpa_sort_quadruple(Z3_context a0)
static Z3_ast Z3_mk_fpa_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_set_member(Z3_context a0, Z3_ast a1, Z3_ast a2)
Probe Or(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".
static Z3_ast Z3_mk_fpa_is_zero(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_bvlshr(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_add(Z3_context a0, uint a1, [In] Z3_ast[] a2)
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
static void Z3_mk_datatypes(Z3_context a0, uint a1, [In] IntPtr[] a2, [Out] Z3_sort[] a3, [In, Out] Z3_constructor_list[] a4)
static Z3_ast Z3_mk_fpa_to_fp_real(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
static void Z3_del_context(Z3_context a0)
A Params objects represents a configuration in the form of Symbol/value pairs.
ListSort MkListSort(string name, Sort elemSort)
Create a new list sort.
static Z3_ast Z3_mk_fpa_sqrt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_full_set(Z3_context a0, Z3_sort a1)
BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise addition does not overflow.
static Z3_ast Z3_mk_fpa_round_toward_zero(Z3_context a0)
static Z3_ast Z3_mk_fpa_neg(Z3_context a0, Z3_ast a1)
BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
Floating-point less than.
static Z3_tactic Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2)
Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create a Quantifier.
static Z3_ast Z3_mk_set_difference(Z3_context a0, Z3_ast a1, Z3_ast a2)
A ParamDescrs describes a set of parameters.
static Z3_ast Z3_mk_bvnot(Z3_context a0, Z3_ast a1)
BitVecNum MkBV(int v, uint size)
Create a bit-vector numeral.
static void Z3_del_config(Z3_config a0)
static Z3_config Z3_mk_config()
static Z3_ast Z3_mk_bvsub(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvsge(Z3_context a0, Z3_ast a1, Z3_ast a2)
A Model contains interpretations (assignments) of constants and functions.
BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
static Z3_ast Z3_mk_store(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
BoolExpr MkBVNegNoOverflow(BitVecExpr t)
Create a predicate that checks that the bit-wise negation does not overflow.
Probe Eq(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value returned by p1 is equal to the value returned...
BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
Bit-vector concatenation.
static Z3_ast Z3_mk_ext_rotate_right(Z3_context a0, Z3_ast a1, Z3_ast a2)
RealExpr MkInt2Real(IntExpr t)
Coerce an integer to a real.
static Z3_ast Z3_mk_fpa_is_subnormal(Z3_context a0, Z3_ast a1)
FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point multiplication
static Z3_ast Z3_mk_fpa_is_positive(Z3_context a0, Z3_ast a1)
IntExpr MkIntConst(string name)
Creates an integer constant.
BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
Floating-point greater than.
static Z3_ast Z3_mk_rem(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_ge(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_tactic Z3_tactic_fail_if_not_decided(Z3_context a0)
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
Create a new enumeration sort.
static Z3_ast Z3_mk_fpa_zero(Z3_context a0, Z3_sort a1, int a2)
static Z3_solver Z3_mk_simple_solver(Z3_context a0)
Tactic FailIf(Probe p)
Create a tactic that fails if the probe p evaluates to false.
BitVecNum MkBV(uint v, uint size)
Create a bit-vector numeral.
BitVecExpr MkBVRedOR(BitVecExpr t)
Take disjunction of bits in a vector, return vector of length 1.
TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Create a new tuple sort.
FPExpr MkFPMin(FPExpr t1, FPExpr t2)
Minimum of floating-point numbers.
Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create a universal Quantifier.
static Z3_ast Z3_mk_fpa_to_ieee_bv(Z3_context a0, Z3_ast a1)
static Z3_sort Z3_get_smtlib_sort(Z3_context a0, uint a1)
static Z3_ast Z3_mk_bvult(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_tactic Z3_tactic_skip(Z3_context a0)
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 iff t2.
The main interaction with Z3 happens via the Context.
static uint Z3_get_num_tactics(Z3_context a0)
static Z3_ast Z3_mk_bvsub_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 ...
static Z3_ast Z3_mk_bvurem(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvsdiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.
BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
Signed remainder.
static Z3_probe Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2)
Tactic Fail()
Create a tactic always fails.
BitVecExpr MkInt2BV(uint n, IntExpr t)
Create an n bit bit-vector from the integer argument t .
The Sort class implements type information for ASTs.
BoolExpr MkNot(BoolExpr a)
Mk an expression representing not(a).
static uint Z3_get_smtlib_num_formulas(Z3_context a0)
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
BoolExpr MkFPIsSubnormal(FPExpr t)
Predicate indicating whether t is a subnormal floating-point number.
FPRMNum MkFPRTP()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode...
static Z3_ast Z3_mk_bvsmod(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_rotate_right(Z3_context a0, uint a1, Z3_ast a2)
FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
Floating-point square root
Arithmetic expressions (int/real)
ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 ^ t2.
static Z3_ast Z3_mk_bvsle(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_int2real(Z3_context a0, Z3_ast a1)
The exception base class for error reporting from Z3
static Z3_ast Z3_mk_rotate_left(Z3_context a0, uint a1, Z3_ast a2)
static Z3_probe Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2)
Expr MkTermArray(ArrayExpr array)
Access the array default value.
RatNum MkReal(ulong v)
Create a real numeral.
ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
Array update.
FPNum MkFPNumeral(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Tactic With(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
The abstract syntax tree (AST) class.
FPSort MkFPSortQuadruple()
Create the quadruple-precision (128-bit) FloatingPoint sort.
FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point subtraction
static uint Z3_get_smtlib_num_sorts(Z3_context a0)
static Z3_ast Z3_mk_bvugt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_fpa_min(Z3_context a0, Z3_ast a1, Z3_ast a2)
RealExpr MkRealConst(Symbol name)
Creates a real constant.
static Z3_ast Z3_mk_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
IntNum MkInt(ulong v)
Create an integer numeral.
FloatingPoint RoundingMode Expressions
FPRMNum MkFPRoundTowardNegative()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode...
IntPtr UnwrapAST(AST a)
Unwraps an AST.
static Z3_ast Z3_mk_fpa_mul(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
static Z3_ast Z3_mk_fpa_is_nan(Z3_context a0, Z3_ast a1)
Object for managing fixedpoints
static Z3_ast Z3_mk_fpa_add(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
static Z3_ast Z3_mk_int(Z3_context a0, int a1, Z3_sort a2)
FPNum MkFP(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Probe ConstProbe(double val)
Create a probe that always evaluates to val .
static void Z3_update_param_value(Z3_context a0, string a1, string a2)
IntExpr MkBV2Int(BitVecExpr t, bool signed)
Create an integer from the bit-vector argument t .
BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
Unsigned remainder.
RatNum MkReal(long v)
Create a real numeral.
Expr MkFullSet(Sort domain)
Create the full set.
IntNum MkInt(long v)
Create an integer numeral.
Expr MkSelect(ArrayExpr a, Expr i)
Array read.
static Z3_tactic Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, uint a2)
void ParseSMTLIBFile(string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
Parse the given file using the SMT-LIB parser.
BoolExpr MkFPIsNormal(FPExpr t)
Predicate indicating whether t is a normal floating-point number.
FPNum MkFPNumeral(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Tactic Cond(Probe p, Tactic t1, Tactic t2)
Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise...
static Z3_ast Z3_mk_set_union(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Tactic FailIfNotDecided()
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatis...
Z3_ast_print_mode
Z3_ast_print_mode
static Z3_ast Z3_mk_array_default(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_bvnand(Z3_context a0, Z3_ast a1, Z3_ast a2)
BoolExpr MkFalse()
The false Term.
BoolExpr MkFPIsZero(FPExpr t)
Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0...
Tactic TryFor(Tactic t, uint ms)
Create a tactic that applies t to a goal for ms milliseconds.
BitVecExpr MkBVConst(string name, uint size)
Creates a bit-vector constant.
BitVecNum MkBV(ulong v, uint size)
Create a bit-vector numeral.
static Z3_ast Z3_mk_fpa_round_toward_positive(Z3_context a0)
Probe Gt(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value returned by p1 is greater than the value retu...
IntExpr MkRem(IntExpr t1, IntExpr t2)
Create an expression representing t1 rem t2.
static Z3_ast Z3_mk_fpa_div(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
FPSort MkFPSort32()
Create the single-precision (32-bit) FloatingPoint sort.
static Z3_ast Z3_mk_int64(Z3_context a0, Int64 a1, Z3_sort a2)
Tactic Skip()
Create a tactic that just returns the given goal.
static Z3_ast Z3_mk_numeral(Z3_context a0, string a1, Z3_sort a2)
FPSort MkFPSortHalf()
Create the half-precision (16-bit) FloatingPoint sort.
IntExpr MkReal2Int(RealExpr t)
Coerce a real to an integer.
static Z3_ast Z3_mk_bvneg(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_set_complement(Z3_context a0, Z3_ast a1)
static Z3_tactic Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2)
BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
Two's complement subtraction.
void Dispose()
Disposes of the context.
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
static Z3_ast Z3_mk_fpa_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
Creates a new function declaration.
static uint Z3_get_smtlib_num_assumptions(Z3_context a0)
FPSort MkFPSort64()
Create the double-precision (64-bit) FloatingPoint sort.
static Z3_ast Z3_mk_fpa_rne(Z3_context a0)
Context(Dictionary< string, string > settings)
Constructor.
Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create a Quantifier.
FPRMNum MkFPRNA()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
Bitwise NAND.
Symbols are used to name several term and type constructors.
static Z3_ast Z3_mk_concat(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_fpa_numeral_int(Z3_context a0, int a1, Z3_sort a2)
static Z3_solver Z3_mk_solver_for_logic(Z3_context a0, IntPtr a1)
static Z3_ast Z3_mk_fpa_to_fp_bv(Z3_context a0, Z3_ast a1, Z3_sort a2)
Solver MkSimpleSolver()
Creates a new (incremental) solver.
BitVecExpr MkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint s...
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
Two's complement multiplication.
BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
Floating-point greater than or equal.
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
static Z3_ast Z3_mk_div(Z3_context a0, Z3_ast a1, Z3_ast a2)
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
An Entry object represents an element in the finite map used to encode a function interpretation...
IntExpr MkMod(IntExpr t1, IntExpr t2)
Create an expression representing t1 mod t2.
static Z3_ast Z3_get_smtlib_assumption(Z3_context a0, uint a1)
static Z3_ast Z3_parse_smtlib2_file(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
static Z3_ast Z3_mk_fpa_rna(Z3_context a0)
static Z3_sort Z3_mk_fpa_sort_32(Z3_context a0)
BoolExpr MkFPIsPositive(FPExpr t)
Predicate indicating whether t is a positive floating-point number.
BoolExpr MkBool(bool value)
Creates a Boolean value.
BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
Rotate Left.
IntSort MkIntSort()
Create a new integer sort.
static Z3_ast Z3_mk_extract(Z3_context a0, uint a1, uint a2, Z3_ast a3)
static Z3_ast Z3_mk_bvsub_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
BitVecExpr MkZeroExt(uint i, BitVecExpr t)
Bit-vector zero extension.
static Z3_ast Z3_mk_bvor(Z3_context a0, Z3_ast a1, Z3_ast a2)
RatNum MkReal(uint v)
Create a real numeral.
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit...
BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
Parse the given file using the SMT-LIB2 parser.
Expr MkConst(FuncDecl f)
Creates a fresh constant from the FuncDecl f .
static void Z3_set_param_value(Z3_config a0, string a1, string a2)
static Z3_sort Z3_mk_fpa_sort_single(Z3_context a0)
static Z3_sort Z3_mk_fpa_sort_double(Z3_context a0)
static Z3_probe Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2)
static Z3_ast Z3_mk_map(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3)