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);
461 nCtx, field.NativeObject,
462 t.NativeObject, v.NativeObject));
468 #region Function Declarations 474 Contract.Requires(name != null);
475 Contract.Requires(range != null);
476 Contract.Requires(Contract.ForAll(domain, d => d != null));
477 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
479 CheckContextMatch(name);
480 CheckContextMatch(domain);
481 CheckContextMatch(range);
482 return new FuncDecl(
this, name, domain, range);
490 Contract.Requires(name != null);
491 Contract.Requires(domain != null);
492 Contract.Requires(range != null);
493 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
495 CheckContextMatch(name);
496 CheckContextMatch(domain);
497 CheckContextMatch(range);
499 return new FuncDecl(
this, name, q, range);
507 Contract.Requires(range != null);
508 Contract.Requires(Contract.ForAll(domain, d => d != null));
509 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
511 CheckContextMatch(domain);
512 CheckContextMatch(range);
513 return new FuncDecl(
this, MkSymbol(name), domain, range);
521 Contract.Requires(range != null);
522 Contract.Requires(domain != null);
523 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
525 CheckContextMatch(domain);
526 CheckContextMatch(range);
528 return new FuncDecl(
this, MkSymbol(name), q, range);
538 Contract.Requires(range != null);
539 Contract.Requires(Contract.ForAll(domain, d => d != null));
540 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
542 CheckContextMatch(domain);
543 CheckContextMatch(range);
544 return new FuncDecl(
this, prefix, domain, range);
552 Contract.Requires(name != null);
553 Contract.Requires(range != null);
554 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
556 CheckContextMatch(name);
557 CheckContextMatch(range);
558 return new FuncDecl(
this, name, null, range);
566 Contract.Requires(range != null);
567 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
569 CheckContextMatch(range);
570 return new FuncDecl(
this, MkSymbol(name), null, range);
580 Contract.Requires(range != null);
581 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
583 CheckContextMatch(range);
584 return new FuncDecl(
this, prefix, null, range);
588 #region Bound Variables 589 public Expr MkBound(uint index,
Sort ty)
596 Contract.Requires(ty != null);
597 Contract.Ensures(Contract.Result<
Expr>() != null);
603 #region Quantifier Patterns 609 Contract.Requires(terms != null);
610 if (terms.Length == 0)
611 throw new Z3Exception(
"Cannot create a pattern from zero terms");
613 Contract.Ensures(Contract.Result<
Pattern>() != null);
615 Contract.EndContractBlock();
617 IntPtr[] termsNative =
AST.ArrayToNative(terms);
628 Contract.Requires(name != null);
629 Contract.Requires(range != null);
630 Contract.Ensures(Contract.Result<
Expr>() != null);
632 CheckContextMatch(name);
633 CheckContextMatch(range);
643 Contract.Requires(range != null);
644 Contract.Ensures(Contract.Result<
Expr>() != null);
646 return MkConst(MkSymbol(name), range);
655 Contract.Requires(range != null);
656 Contract.Ensures(Contract.Result<
Expr>() != null);
658 CheckContextMatch(range);
668 Contract.Requires(f != null);
669 Contract.Ensures(Contract.Result<
Expr>() != null);
679 Contract.Requires(name != null);
680 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
690 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
700 Contract.Requires(name != null);
701 Contract.Ensures(Contract.Result<
IntExpr>() != null);
711 Contract.Requires(name != null);
712 Contract.Ensures(Contract.Result<
IntExpr>() != null);
722 Contract.Requires(name != null);
723 Contract.Ensures(Contract.Result<
RealExpr>() != null);
733 Contract.Ensures(Contract.Result<
RealExpr>() != null);
743 Contract.Requires(name != null);
744 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
746 return (
BitVecExpr)MkConst(name, MkBitVecSort(size));
754 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
756 return (
BitVecExpr)MkConst(name, MkBitVecSort(size));
766 Contract.Requires(f != null);
767 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
768 Contract.Ensures(Contract.Result<
Expr>() != null);
770 CheckContextMatch(f);
771 CheckContextMatch(args);
772 return Expr.Create(
this, f, args);
775 #region Propositional 781 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
791 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
801 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
803 return value ? MkTrue() : MkFalse();
811 Contract.Requires(x != null);
812 Contract.Requires(y != null);
813 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
815 CheckContextMatch(x);
816 CheckContextMatch(y);
825 Contract.Requires(args != null);
826 Contract.Requires(Contract.ForAll(args, a => a != null));
828 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
830 CheckContextMatch(args);
839 Contract.Requires(a != null);
840 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
842 CheckContextMatch(a);
854 Contract.Requires(t1 != null);
855 Contract.Requires(t2 != null);
856 Contract.Requires(t3 != null);
857 Contract.Ensures(Contract.Result<
Expr>() != null);
859 CheckContextMatch(t1);
860 CheckContextMatch(t2);
861 CheckContextMatch(t3);
862 return Expr.Create(
this,
Native.
Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
870 Contract.Requires(t1 != null);
871 Contract.Requires(t2 != null);
872 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
874 CheckContextMatch(t1);
875 CheckContextMatch(t2);
884 Contract.Requires(t1 != null);
885 Contract.Requires(t2 != null);
886 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
888 CheckContextMatch(t1);
889 CheckContextMatch(t2);
898 Contract.Requires(t1 != null);
899 Contract.Requires(t2 != null);
900 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
902 CheckContextMatch(t1);
903 CheckContextMatch(t2);
912 Contract.Requires(t != null);
913 Contract.Requires(Contract.ForAll(t, a => a != null));
914 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
916 CheckContextMatch(t);
925 Contract.Requires(t != null);
926 Contract.Requires(Contract.ForAll(t, a => a != null));
927 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
929 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.Requires(Contract.ForAll(t, a => a != null));
970 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
972 CheckContextMatch(t);
981 Contract.Requires(t != null);
982 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
984 CheckContextMatch(t);
993 Contract.Requires(t1 != null);
994 Contract.Requires(t2 != null);
995 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
997 CheckContextMatch(t1);
998 CheckContextMatch(t2);
1008 Contract.Requires(t1 != null);
1009 Contract.Requires(t2 != null);
1010 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1012 CheckContextMatch(t1);
1013 CheckContextMatch(t2);
1023 Contract.Requires(t1 != null);
1024 Contract.Requires(t2 != null);
1025 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1027 CheckContextMatch(t1);
1028 CheckContextMatch(t2);
1037 Contract.Requires(t1 != null);
1038 Contract.Requires(t2 != null);
1039 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
1041 CheckContextMatch(t1);
1042 CheckContextMatch(t2);
1051 Contract.Requires(t1 != null);
1052 Contract.Requires(t2 != null);
1053 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1055 CheckContextMatch(t1);
1056 CheckContextMatch(t2);
1065 Contract.Requires(t1 != null);
1066 Contract.Requires(t2 != null);
1067 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1069 CheckContextMatch(t1);
1070 CheckContextMatch(t2);
1079 Contract.Requires(t1 != null);
1080 Contract.Requires(t2 != null);
1081 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1083 CheckContextMatch(t1);
1084 CheckContextMatch(t2);
1093 Contract.Requires(t1 != null);
1094 Contract.Requires(t2 != null);
1095 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1097 CheckContextMatch(t1);
1098 CheckContextMatch(t2);
1114 Contract.Requires(t != null);
1115 Contract.Ensures(Contract.Result<
RealExpr>() != null);
1117 CheckContextMatch(t);
1130 Contract.Requires(t != null);
1131 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1133 CheckContextMatch(t);
1142 Contract.Requires(t != null);
1143 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1145 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(t != null);
1184 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1186 CheckContextMatch(t);
1196 Contract.Requires(t1 != null);
1197 Contract.Requires(t2 != null);
1198 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1200 CheckContextMatch(t1);
1201 CheckContextMatch(t2);
1211 Contract.Requires(t1 != null);
1212 Contract.Requires(t2 != null);
1213 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1215 CheckContextMatch(t1);
1216 CheckContextMatch(t2);
1226 Contract.Requires(t1 != null);
1227 Contract.Requires(t2 != null);
1228 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1230 CheckContextMatch(t1);
1231 CheckContextMatch(t2);
1241 Contract.Requires(t1 != null);
1242 Contract.Requires(t2 != null);
1243 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1245 CheckContextMatch(t1);
1246 CheckContextMatch(t2);
1256 Contract.Requires(t1 != null);
1257 Contract.Requires(t2 != null);
1258 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1260 CheckContextMatch(t1);
1261 CheckContextMatch(t2);
1271 Contract.Requires(t1 != null);
1272 Contract.Requires(t2 != null);
1273 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1275 CheckContextMatch(t1);
1276 CheckContextMatch(t2);
1286 Contract.Requires(t != null);
1287 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1289 CheckContextMatch(t);
1299 Contract.Requires(t1 != null);
1300 Contract.Requires(t2 != null);
1301 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1303 CheckContextMatch(t1);
1304 CheckContextMatch(t2);
1314 Contract.Requires(t1 != null);
1315 Contract.Requires(t2 != null);
1316 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1318 CheckContextMatch(t1);
1319 CheckContextMatch(t2);
1329 Contract.Requires(t1 != null);
1330 Contract.Requires(t2 != null);
1331 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1333 CheckContextMatch(t1);
1334 CheckContextMatch(t2);
1349 Contract.Requires(t1 != null);
1350 Contract.Requires(t2 != null);
1351 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1353 CheckContextMatch(t1);
1354 CheckContextMatch(t2);
1373 Contract.Requires(t1 != null);
1374 Contract.Requires(t2 != null);
1375 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1377 CheckContextMatch(t1);
1378 CheckContextMatch(t2);
1392 Contract.Requires(t1 != null);
1393 Contract.Requires(t2 != null);
1394 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1396 CheckContextMatch(t1);
1397 CheckContextMatch(t2);
1413 Contract.Requires(t1 != null);
1414 Contract.Requires(t2 != null);
1415 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1417 CheckContextMatch(t1);
1418 CheckContextMatch(t2);
1431 Contract.Requires(t1 != null);
1432 Contract.Requires(t2 != null);
1433 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1435 CheckContextMatch(t1);
1436 CheckContextMatch(t2);
1448 Contract.Requires(t1 != null);
1449 Contract.Requires(t2 != null);
1450 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1452 CheckContextMatch(t1);
1453 CheckContextMatch(t2);
1465 Contract.Requires(t1 != null);
1466 Contract.Requires(t2 != null);
1467 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1469 CheckContextMatch(t1);
1470 CheckContextMatch(t2);
1482 Contract.Requires(t1 != null);
1483 Contract.Requires(t2 != null);
1484 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1486 CheckContextMatch(t1);
1487 CheckContextMatch(t2);
1499 Contract.Requires(t1 != null);
1500 Contract.Requires(t2 != null);
1501 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1503 CheckContextMatch(t1);
1504 CheckContextMatch(t2);
1516 Contract.Requires(t1 != null);
1517 Contract.Requires(t2 != null);
1518 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1520 CheckContextMatch(t1);
1521 CheckContextMatch(t2);
1533 Contract.Requires(t1 != null);
1534 Contract.Requires(t2 != null);
1535 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1537 CheckContextMatch(t1);
1538 CheckContextMatch(t2);
1550 Contract.Requires(t1 != null);
1551 Contract.Requires(t2 != null);
1552 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1554 CheckContextMatch(t1);
1555 CheckContextMatch(t2);
1567 Contract.Requires(t1 != null);
1568 Contract.Requires(t2 != null);
1569 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1571 CheckContextMatch(t1);
1572 CheckContextMatch(t2);
1588 Contract.Requires(t1 != null);
1589 Contract.Requires(t2 != null);
1590 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1592 CheckContextMatch(t1);
1593 CheckContextMatch(t2);
1608 Contract.Requires(t != null);
1609 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1611 CheckContextMatch(t);
1625 Contract.Requires(t != null);
1626 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1628 CheckContextMatch(t);
1643 Contract.Requires(t != null);
1644 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1646 CheckContextMatch(t);
1658 Contract.Requires(t != null);
1659 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1661 CheckContextMatch(t);
1679 Contract.Requires(t1 != null);
1680 Contract.Requires(t2 != null);
1681 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1683 CheckContextMatch(t1);
1684 CheckContextMatch(t2);
1702 Contract.Requires(t1 != null);
1703 Contract.Requires(t2 != null);
1704 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1706 CheckContextMatch(t1);
1707 CheckContextMatch(t2);
1727 Contract.Requires(t1 != null);
1728 Contract.Requires(t2 != null);
1729 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1731 CheckContextMatch(t1);
1732 CheckContextMatch(t2);
1745 Contract.Requires(t != null);
1746 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1748 CheckContextMatch(t);
1761 Contract.Requires(t != null);
1762 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1764 CheckContextMatch(t);
1777 Contract.Requires(t1 != null);
1778 Contract.Requires(t2 != null);
1779 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1781 CheckContextMatch(t1);
1782 CheckContextMatch(t2);
1795 Contract.Requires(t1 != null);
1796 Contract.Requires(t2 != null);
1797 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1799 CheckContextMatch(t1);
1800 CheckContextMatch(t2);
1816 Contract.Requires(t != null);
1817 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1819 CheckContextMatch(t);
1840 Contract.Requires(t != null);
1841 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1843 CheckContextMatch(t);
1855 Contract.Requires(t1 != null);
1856 Contract.Requires(t2 != null);
1857 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1859 CheckContextMatch(t1);
1860 CheckContextMatch(t2);
1872 Contract.Requires(t1 != null);
1873 Contract.Requires(t2 != null);
1874 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1876 CheckContextMatch(t1);
1877 CheckContextMatch(t2);
1889 Contract.Requires(t1 != null);
1890 Contract.Requires(t2 != null);
1891 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1893 CheckContextMatch(t1);
1894 CheckContextMatch(t2);
1906 Contract.Requires(t1 != null);
1907 Contract.Requires(t2 != null);
1908 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1910 CheckContextMatch(t1);
1911 CheckContextMatch(t2);
1923 Contract.Requires(t1 != null);
1924 Contract.Requires(t2 != null);
1925 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1927 CheckContextMatch(t1);
1928 CheckContextMatch(t2);
1940 Contract.Requires(t != null);
1941 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1943 CheckContextMatch(t);
1955 Contract.Requires(t1 != null);
1956 Contract.Requires(t2 != null);
1957 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1959 CheckContextMatch(t1);
1960 CheckContextMatch(t2);
1972 Contract.Requires(t1 != null);
1973 Contract.Requires(t2 != null);
1974 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1976 CheckContextMatch(t1);
1977 CheckContextMatch(t2);
1988 Contract.Requires(name != null);
1989 Contract.Requires(domain != null);
1990 Contract.Requires(range != null);
1991 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
1993 return (
ArrayExpr)MkConst(name, MkArraySort(domain, range));
2001 Contract.Requires(domain != null);
2002 Contract.Requires(range != null);
2003 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2005 return (
ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
2023 Contract.Requires(a != null);
2024 Contract.Requires(i != null);
2025 Contract.Ensures(Contract.Result<
Expr>() != null);
2027 CheckContextMatch(a);
2028 CheckContextMatch(i);
2051 Contract.Requires(a != null);
2052 Contract.Requires(i != null);
2053 Contract.Requires(v != null);
2054 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2056 CheckContextMatch(a);
2057 CheckContextMatch(i);
2058 CheckContextMatch(v);
2073 Contract.Requires(domain != null);
2074 Contract.Requires(v != null);
2075 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2077 CheckContextMatch(domain);
2078 CheckContextMatch(v);
2095 Contract.Requires(f != null);
2096 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2097 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2099 CheckContextMatch(f);
2100 CheckContextMatch(args);
2113 Contract.Requires(array != null);
2114 Contract.Ensures(Contract.Result<
Expr>() != null);
2116 CheckContextMatch(array);
2127 Contract.Requires(ty != null);
2128 Contract.Ensures(Contract.Result<
SetSort>() != null);
2130 CheckContextMatch(ty);
2139 Contract.Requires(domain != null);
2140 Contract.Ensures(Contract.Result<
Expr>() != null);
2142 CheckContextMatch(domain);
2151 Contract.Requires(domain != null);
2152 Contract.Ensures(Contract.Result<
Expr>() != null);
2154 CheckContextMatch(domain);
2163 Contract.Requires(
set != null);
2164 Contract.Requires(element != null);
2165 Contract.Ensures(Contract.Result<
Expr>() != null);
2167 CheckContextMatch(
set);
2168 CheckContextMatch(element);
2178 Contract.Requires(
set != null);
2179 Contract.Requires(element != null);
2180 Contract.Ensures(Contract.Result<
Expr>() != null);
2182 CheckContextMatch(
set);
2183 CheckContextMatch(element);
2192 Contract.Requires(args != null);
2193 Contract.Requires(Contract.ForAll(args, a => a != null));
2195 CheckContextMatch(args);
2204 Contract.Requires(args != null);
2205 Contract.Requires(Contract.ForAll(args, a => a != null));
2206 Contract.Ensures(Contract.Result<
Expr>() != null);
2208 CheckContextMatch(args);
2217 Contract.Requires(arg1 != null);
2218 Contract.Requires(arg2 != null);
2219 Contract.Ensures(Contract.Result<
Expr>() != null);
2221 CheckContextMatch(arg1);
2222 CheckContextMatch(arg2);
2231 Contract.Requires(arg != null);
2232 Contract.Ensures(Contract.Result<
Expr>() != null);
2234 CheckContextMatch(arg);
2243 Contract.Requires(elem != null);
2244 Contract.Requires(
set != null);
2245 Contract.Ensures(Contract.Result<
Expr>() != null);
2247 CheckContextMatch(elem);
2248 CheckContextMatch(
set);
2257 Contract.Requires(arg1 != null);
2258 Contract.Requires(arg2 != null);
2259 Contract.Ensures(Contract.Result<
Expr>() != null);
2261 CheckContextMatch(arg1);
2262 CheckContextMatch(arg2);
2267 #region Pseudo-Boolean constraints 2274 Contract.Requires(args != null);
2275 Contract.Requires(Contract.Result<
BoolExpr[]>() != null);
2276 CheckContextMatch(args);
2278 AST.ArrayToNative(args), k));
2286 Contract.Requires(args != null);
2287 Contract.Requires(coeffs != null);
2288 Contract.Requires(args.Length == coeffs.Length);
2289 Contract.Requires(Contract.Result<
BoolExpr[]>() != null);
2290 CheckContextMatch(args);
2292 AST.ArrayToNative(args),
2299 #region General Numerals 2300 public Expr MkNumeral(
string v,
Sort ty)
2308 Contract.Requires(ty != null);
2309 Contract.Ensures(Contract.Result<
Expr>() != null);
2311 CheckContextMatch(ty);
2324 Contract.Requires(ty != null);
2325 Contract.Ensures(Contract.Result<
Expr>() != null);
2327 CheckContextMatch(ty);
2340 Contract.Requires(ty != null);
2341 Contract.Ensures(Contract.Result<
Expr>() != null);
2343 CheckContextMatch(ty);
2356 Contract.Requires(ty != null);
2357 Contract.Ensures(Contract.Result<
Expr>() != null);
2359 CheckContextMatch(ty);
2372 Contract.Requires(ty != null);
2373 Contract.Ensures(Contract.Result<
Expr>() != null);
2375 CheckContextMatch(ty);
2381 public RatNum MkReal(
int num,
int den)
2393 Contract.Ensures(Contract.Result<
RatNum>() != null);
2394 Contract.EndContractBlock();
2406 Contract.Ensures(Contract.Result<
RatNum>() != null);
2418 Contract.Ensures(Contract.Result<
RatNum>() != null);
2430 Contract.Ensures(Contract.Result<
RatNum>() != null);
2442 Contract.Ensures(Contract.Result<
RatNum>() != null);
2454 Contract.Ensures(Contract.Result<
RatNum>() != null);
2461 public IntNum MkInt(
string v)
2467 Contract.Ensures(Contract.Result<
IntNum>() != null);
2479 Contract.Ensures(Contract.Result<
IntNum>() != null);
2491 Contract.Ensures(Contract.Result<
IntNum>() != null);
2503 Contract.Ensures(Contract.Result<
IntNum>() != null);
2515 Contract.Ensures(Contract.Result<
IntNum>() != null);
2522 public BitVecNum MkBV(
string v, uint size)
2529 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2531 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2541 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2543 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2553 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2555 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2565 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2567 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2577 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2579 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2583 #endregion // Numerals 2607 Contract.Requires(sorts != null);
2608 Contract.Requires(names != null);
2609 Contract.Requires(body != null);
2610 Contract.Requires(sorts.Length == names.Length);
2611 Contract.Requires(Contract.ForAll(sorts, s => s != null));
2612 Contract.Requires(Contract.ForAll(names, n => n != null));
2613 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2614 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2616 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2618 return new Quantifier(
this,
true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2627 Contract.Requires(body != null);
2628 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
2629 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2630 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2632 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2634 return new Quantifier(
this,
true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2643 Contract.Requires(sorts != null);
2644 Contract.Requires(names != null);
2645 Contract.Requires(body != null);
2646 Contract.Requires(sorts.Length == names.Length);
2647 Contract.Requires(Contract.ForAll(sorts, s => s != null));
2648 Contract.Requires(Contract.ForAll(names, n => n != null));
2649 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2650 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2651 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2653 return new Quantifier(
this,
false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2661 Contract.Requires(body != null);
2662 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2663 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2664 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2665 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2667 return new Quantifier(
this,
false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2676 Contract.Requires(body != null);
2677 Contract.Requires(names != null);
2678 Contract.Requires(sorts != null);
2679 Contract.Requires(sorts.Length == names.Length);
2680 Contract.Requires(Contract.ForAll(sorts, s => s != null));
2681 Contract.Requires(Contract.ForAll(names, n => n != null));
2682 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2683 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2685 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2688 return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2690 return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2699 Contract.Requires(body != null);
2700 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2701 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2702 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2704 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2707 return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2709 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2739 #region SMT Files & Strings 2740 public string BenchmarkToSMTString(
string name,
string logic,
string status,
string attributes,
2753 Contract.Requires(assumptions != null);
2754 Contract.Requires(formula != null);
2755 Contract.Ensures(Contract.Result<
string>() != null);
2758 (uint)assumptions.Length,
AST.ArrayToNative(assumptions),
2759 formula.NativeObject);
2774 uint csn =
Symbol.ArrayLength(sortNames);
2775 uint cs =
Sort.ArrayLength(sorts);
2776 uint cdn =
Symbol.ArrayLength(declNames);
2777 uint cd =
AST.ArrayLength(decls);
2778 if (csn != cs || cdn != cd)
2781 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
2782 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls));
2791 uint csn =
Symbol.ArrayLength(sortNames);
2792 uint cs =
Sort.ArrayLength(sorts);
2793 uint cdn =
Symbol.ArrayLength(declNames);
2794 uint cd =
AST.ArrayLength(decls);
2795 if (csn != cs || cdn != cd)
2798 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
2799 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls));
2814 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
2816 uint n = NumSMTLIBFormulas;
2818 for (uint i = 0; i < n; i++)
2832 public BoolExpr[] SMTLIBAssumptions
2836 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
2838 uint n = NumSMTLIBAssumptions;
2840 for (uint i = 0; i < n; i++)
2858 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
2860 uint n = NumSMTLIBDecls;
2862 for (uint i = 0; i < n; i++)
2876 public Sort[] SMTLIBSorts
2880 Contract.Ensures(Contract.Result<
Sort[]>() != null);
2882 uint n = NumSMTLIBSorts;
2884 for (uint i = 0; i < n; i++)
2897 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2899 uint csn =
Symbol.ArrayLength(sortNames);
2900 uint cs =
Sort.ArrayLength(sorts);
2901 uint cdn =
Symbol.ArrayLength(declNames);
2902 uint cd =
AST.ArrayLength(decls);
2903 if (csn != cs || cdn != cd)
2906 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
2907 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls)));
2916 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2918 uint csn =
Symbol.ArrayLength(sortNames);
2919 uint cs =
Sort.ArrayLength(sorts);
2920 uint cdn =
Symbol.ArrayLength(declNames);
2921 uint cd =
AST.ArrayLength(decls);
2922 if (csn != cs || cdn != cd)
2925 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
2926 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls)));
2931 public Goal MkGoal(
bool models =
true,
bool unsatCores =
false,
bool proofs =
false)
2943 Contract.Ensures(Contract.Result<
Goal>() != null);
2945 return new Goal(
this, models, unsatCores, proofs);
2949 #region ParameterSets 2955 Contract.Ensures(Contract.Result<
Params>() != null);
2962 public uint NumTactics
2973 public string[] TacticNames
2977 Contract.Ensures(Contract.Result<
string[]>() != null);
2979 uint n = NumTactics;
2980 string[] res =
new string[n];
2981 for (uint i = 0; i < n; i++)
2992 Contract.Ensures(Contract.Result<
string>() != null);
3002 Contract.Ensures(Contract.Result<
Tactic>() != null);
3004 return new Tactic(
this, name);
3013 Contract.Requires(t1 != null);
3014 Contract.Requires(t2 != null);
3015 Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3016 Contract.Ensures(Contract.Result<
Tactic>() != null);
3019 CheckContextMatch(t1);
3020 CheckContextMatch(t2);
3021 CheckContextMatch(ts);
3023 IntPtr last = IntPtr.Zero;
3024 if (ts != null && ts.Length > 0)
3026 last = ts[ts.Length - 1].NativeObject;
3027 for (
int i = ts.Length - 2; i >= 0; i--)
3030 if (last != IntPtr.Zero)
3048 Contract.Requires(t1 != null);
3049 Contract.Requires(t2 != null);
3050 Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3051 Contract.Ensures(Contract.Result<
Tactic>() != null);
3062 Contract.Requires(t1 != null);
3063 Contract.Requires(t2 != null);
3064 Contract.Ensures(Contract.Result<
Tactic>() != null);
3066 CheckContextMatch(t1);
3067 CheckContextMatch(t2);
3079 Contract.Requires(t != null);
3080 Contract.Ensures(Contract.Result<
Tactic>() != null);
3082 CheckContextMatch(t);
3095 Contract.Requires(p != null);
3096 Contract.Requires(t != null);
3097 Contract.Ensures(Contract.Result<
Tactic>() != null);
3099 CheckContextMatch(t);
3100 CheckContextMatch(p);
3110 Contract.Requires(p != null);
3111 Contract.Requires(t1 != null);
3112 Contract.Requires(t2 != null);
3113 Contract.Ensures(Contract.Result<
Tactic>() != null);
3115 CheckContextMatch(p);
3116 CheckContextMatch(t1);
3117 CheckContextMatch(t2);
3127 Contract.Requires(t != null);
3128 Contract.Ensures(Contract.Result<
Tactic>() != null);
3130 CheckContextMatch(t);
3139 Contract.Ensures(Contract.Result<
Tactic>() != null);
3149 Contract.Ensures(Contract.Result<
Tactic>() != null);
3159 Contract.Requires(p != null);
3160 Contract.Ensures(Contract.Result<
Tactic>() != null);
3162 CheckContextMatch(p);
3172 Contract.Ensures(Contract.Result<
Tactic>() != null);
3182 Contract.Requires(t != null);
3183 Contract.Requires(p != null);
3184 Contract.Ensures(Contract.Result<
Tactic>() != null);
3186 CheckContextMatch(t);
3187 CheckContextMatch(p);
3197 Contract.Requires(t != null);
3198 Contract.Requires(p != null);
3199 Contract.Ensures(Contract.Result<
Tactic>() != null);
3201 return UsingParams(t, p);
3209 Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3210 Contract.Ensures(Contract.Result<
Tactic>() != null);
3212 CheckContextMatch(t);
3222 Contract.Requires(t1 != null);
3223 Contract.Requires(t2 != null);
3224 Contract.Ensures(Contract.Result<
Tactic>() != null);
3226 CheckContextMatch(t1);
3227 CheckContextMatch(t2);
3242 public uint NumProbes
3253 public string[] ProbeNames
3257 Contract.Ensures(Contract.Result<
string[]>() != null);
3260 string[] res =
new string[n];
3261 for (uint i = 0; i < n; i++)
3272 Contract.Ensures(Contract.Result<
string>() != null);
3282 Contract.Ensures(Contract.Result<
Probe>() != null);
3284 return new Probe(
this, name);
3292 Contract.Ensures(Contract.Result<
Probe>() != null);
3303 Contract.Requires(p1 != null);
3304 Contract.Requires(p2 != null);
3305 Contract.Ensures(Contract.Result<
Probe>() != null);
3307 CheckContextMatch(p1);
3308 CheckContextMatch(p2);
3318 Contract.Requires(p1 != null);
3319 Contract.Requires(p2 != null);
3320 Contract.Ensures(Contract.Result<
Probe>() != null);
3322 CheckContextMatch(p1);
3323 CheckContextMatch(p2);
3333 Contract.Requires(p1 != null);
3334 Contract.Requires(p2 != null);
3335 Contract.Ensures(Contract.Result<
Probe>() != null);
3337 CheckContextMatch(p1);
3338 CheckContextMatch(p2);
3348 Contract.Requires(p1 != null);
3349 Contract.Requires(p2 != null);
3350 Contract.Ensures(Contract.Result<
Probe>() != null);
3352 CheckContextMatch(p1);
3353 CheckContextMatch(p2);
3363 Contract.Requires(p1 != null);
3364 Contract.Requires(p2 != null);
3365 Contract.Ensures(Contract.Result<
Probe>() != null);
3367 CheckContextMatch(p1);
3368 CheckContextMatch(p2);
3378 Contract.Requires(p1 != null);
3379 Contract.Requires(p2 != null);
3380 Contract.Ensures(Contract.Result<
Probe>() != null);
3382 CheckContextMatch(p1);
3383 CheckContextMatch(p2);
3393 Contract.Requires(p1 != null);
3394 Contract.Requires(p2 != null);
3395 Contract.Ensures(Contract.Result<
Probe>() != null);
3397 CheckContextMatch(p1);
3398 CheckContextMatch(p2);
3408 Contract.Requires(p != null);
3409 Contract.Ensures(Contract.Result<
Probe>() != null);
3411 CheckContextMatch(p);
3427 Contract.Ensures(Contract.Result<
Solver>() != null);
3441 Contract.Ensures(Contract.Result<
Solver>() != null);
3443 return MkSolver(MkSymbol(logic));
3451 Contract.Ensures(Contract.Result<
Solver>() != null);
3465 Contract.Requires(t != null);
3466 Contract.Ensures(Contract.Result<
Solver>() != null);
3478 Contract.Ensures(Contract.Result<
Fixedpoint>() != null);
3484 #region Optimization 3490 Contract.Ensures(Contract.Result<
Optimize>() != null);
3496 #region Floating-Point Arithmetic 3498 #region Rounding Modes 3499 #region RoundingMode Sort 3500 public FPRMSort MkFPRoundingModeSort()
3505 Contract.Ensures(Contract.Result<
FPRMSort>() != null);
3511 public FPRMExpr MkFPRoundNearestTiesToEven()
3516 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3525 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3534 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3543 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3552 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3561 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3570 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3579 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3588 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3597 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3603 #region FloatingPoint Sorts 3604 public FPSort MkFPSort(uint ebits, uint sbits)
3611 Contract.Ensures(Contract.Result<
FPSort>() != null);
3612 return new FPSort(
this, ebits, sbits);
3620 Contract.Ensures(Contract.Result<
FPSort>() != null);
3629 Contract.Ensures(Contract.Result<
FPSort>() != null);
3638 Contract.Ensures(Contract.Result<
FPSort>() != null);
3647 Contract.Ensures(Contract.Result<
FPSort>() != null);
3656 Contract.Ensures(Contract.Result<
FPSort>() != null);
3665 Contract.Ensures(Contract.Result<
FPSort>() != null);
3674 Contract.Ensures(Contract.Result<
FPSort>() != null);
3683 Contract.Ensures(Contract.Result<
FPSort>() != null);
3695 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3706 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3717 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3728 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3739 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3750 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3763 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3776 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3787 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3788 return MkFPNumeral(v, s);
3798 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3799 return MkFPNumeral(v, s);
3809 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3810 return MkFPNumeral(v, s);
3822 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3823 return MkFPNumeral(sgn, exp, sig, s);
3835 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3836 return MkFPNumeral(sgn, exp, sig, s);
3848 Contract.Ensures(Contract.Result<
FPNum>() != null);
3858 Contract.Ensures(Contract.Result<
FPNum>() != null);
3870 Contract.Ensures(Contract.Result<
FPNum>() != null);
3882 Contract.Ensures(Contract.Result<
FPNum>() != null);
3894 Contract.Ensures(Contract.Result<
FPNum>() != null);
3906 Contract.Ensures(Contract.Result<
FPNum>() != null);
3922 Contract.Ensures(Contract.Result<
FPNum>() != null);
3923 return new FPExpr(
this,
Native.
Z3_mk_fpa_fma(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
3933 Contract.Ensures(Contract.Result<
FPNum>() != null);
3944 Contract.Ensures(Contract.Result<
FPNum>() != null);
3956 Contract.Ensures(Contract.Result<
FPNum>() != null);
3967 Contract.Ensures(Contract.Result<
FPNum>() != null);
3978 Contract.Ensures(Contract.Result<
FPNum>() != null);
3989 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4000 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4011 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4022 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4036 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4046 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4056 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4066 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4076 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4086 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4096 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4106 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4111 #region Conversions to FloatingPoint terms 4127 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4144 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4161 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4178 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4197 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4216 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4221 #region Conversions from FloatingPoint terms 4236 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
4254 Contract.Ensures(Contract.Result<
RealExpr>() != null);
4259 #region Z3-specific extensions 4272 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
4290 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
4294 #endregion // Floating-point Arithmetic 4296 #region Miscellaneous 4297 public AST WrapAST(IntPtr nativeObject)
4309 Contract.Ensures(Contract.Result<
AST>() != null);
4310 return AST.Create(
this, nativeObject);
4326 return a.NativeObject;
4334 Contract.Ensures(Contract.Result<
string>() != null);
4348 #region Error Handling 4365 public void UpdateParamValue(
string id,
string value)
4382 internal IntPtr m_ctx = IntPtr.Zero;
4384 internal IntPtr nCtx {
get {
return m_ctx; } }
4386 internal void NativeErrorHandler(IntPtr ctx,
Z3_error_code errorCode)
4391 internal void InitContext()
4396 GC.SuppressFinalize(
this);
4400 internal void CheckContextMatch(
Z3Object other)
4402 Contract.Requires(other != null);
4404 if (!ReferenceEquals(
this, other.Context))
4409 internal void CheckContextMatch(
Z3Object[] arr)
4411 Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
4417 Contract.Assert(a != null);
4418 CheckContextMatch(a);
4423 [ContractInvariantMethod]
4424 private void ObjectInvariant()
4426 Contract.Invariant(m_AST_DRQ != null);
4427 Contract.Invariant(m_ASTMap_DRQ != null);
4428 Contract.Invariant(m_ASTVector_DRQ != null);
4429 Contract.Invariant(m_ApplyResult_DRQ != null);
4430 Contract.Invariant(m_FuncEntry_DRQ != null);
4431 Contract.Invariant(m_FuncInterp_DRQ != null);
4432 Contract.Invariant(m_Goal_DRQ != null);
4433 Contract.Invariant(m_Model_DRQ != null);
4434 Contract.Invariant(m_Params_DRQ != null);
4435 Contract.Invariant(m_ParamDescrs_DRQ != null);
4436 Contract.Invariant(m_Probe_DRQ != null);
4437 Contract.Invariant(m_Solver_DRQ != null);
4438 Contract.Invariant(m_Statistics_DRQ != null);
4439 Contract.Invariant(m_Tactic_DRQ != null);
4440 Contract.Invariant(m_Fixedpoint_DRQ != null);
4441 Contract.Invariant(m_Optimize_DRQ != null);
4445 readonly
private ASTMap.DecRefQueue m_ASTMap_DRQ =
new ASTMap.DecRefQueue(10);
4469 public IDecRefQueue ASTMap_DRQ {
get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null);
return m_ASTMap_DRQ; } }
4542 internal long refCount = 0;
4554 m_n_err_handler = null;
4556 m_ctx = IntPtr.Zero;
4559 GC.ReRegisterForFinalize(
this);
4568 AST_DRQ.Clear(
this);
4569 ASTMap_DRQ.Clear(
this);
4570 ASTVector_DRQ.Clear(
this);
4571 ApplyResult_DRQ.Clear(
this);
4572 FuncEntry_DRQ.Clear(
this);
4573 FuncInterp_DRQ.Clear(
this);
4574 Goal_DRQ.Clear(
this);
4575 Model_DRQ.Clear(
this);
4576 Params_DRQ.Clear(
this);
4577 ParamDescrs_DRQ.Clear(
this);
4578 Probe_DRQ.Clear(
this);
4579 Solver_DRQ.Clear(
this);
4580 Statistics_DRQ.Clear(
this);
4581 Tactic_DRQ.Clear(
this);
4582 Fixedpoint_DRQ.Clear(
this);
4583 Optimize_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.
Object for managing optimizization context
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_pble(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] int[] a3, int a4)
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...
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)
BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean less-or-equal constraint.
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_round_nearest_ties_to_even(Z3_context a0)
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.
BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
Check for set membership.
static Z3_ast Z3_mk_atmost(Z3_context a0, uint a1, [In] Z3_ast[] a2, uint a3)
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.
Z3_error_code
Z3_error_code
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.
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_ast Z3_mk_true(Z3_context a0)
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)
static Z3_tactic Z3_tactic_fail(Z3_context a0)
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
ArrayExpr MkFullSet(Sort domain)
Create the full set.
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...
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.
ArrayExpr MkSetComplement(ArrayExpr arg)
Take the complement of a set.
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)
BoolExpr MkAtMost(BoolExpr[] args, uint k)
Create an at-most-k constraint.
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.
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)
RealSort MkRealSort()
Create a real sort.
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.
def FiniteDomainSort(name, sz, ctx=None)
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...
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_datatype_update_field(Z3_context a0, Z3_func_decl a1, Z3_ast a2, Z3_ast a3)
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.
ArrayExpr MkSetUnion(params ArrayExpr[] args)
Take the union of a list of sets.
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)
ArrayExpr MkEmptySet(Sort domain)
Create an empty set.
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.
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.
The FloatingPoint RoundingMode sort
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)
def FPSort(ebits, sbits, ctx=None)
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)
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_pattern Z3_mk_pattern(Z3_context a0, uint a1, [In] 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)
ArrayExpr MkSetDel(ArrayExpr set, Expr element)
Remove an element from a set.
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)
def EnumSort(name, values, ctx=None)
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 void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1)
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)
BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Check for subsetness of sets.
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
def BitVecSort(sz, ctx=None)
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...
ArrayExpr MkSetIntersection(params ArrayExpr[] args)
Take the intersection of a list of sets.
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.
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.
ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
Add an element to the set.
delegate void Z3_error_handler(Z3_context c, Z3_error_code e)
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)
ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Take the difference between two sets.
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)
Internal base class for interfacing with native Z3 objects. Should not be used externally.
FPSort MkFPSortHalf()
Create the half-precision (16-bit) FloatingPoint sort.
static Z3_ast Z3_mk_const(Z3_context a0, IntPtr a1, Z3_sort a2)
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
Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
Update a datatype field at expression t with value v. The function performs a record update at t...
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)