21using System.Diagnostics;
22using System.Collections.Generic;
23using System.Runtime.InteropServices;
42 m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
65 public Context(Dictionary<string, string> settings)
68 Debug.Assert(settings !=
null);
72 IntPtr cfg = Native.Z3_mk_config();
73 foreach (KeyValuePair<string, string> kv
in settings)
74 Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
75 m_ctx = Native.Z3_mk_context_rc(cfg);
76 Native.Z3_del_config(cfg);
108 internal Symbol[] MkSymbols(
string[] names)
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;
122 private SeqSort m_stringSort =
null;
131 if (m_boolSort ==
null) m_boolSort =
new BoolSort(
this);
return m_boolSort;
142 if (m_intSort ==
null) m_intSort =
new IntSort(
this);
return m_intSort;
154 if (m_realSort ==
null) m_realSort =
new RealSort(
this);
return m_realSort;
165 if (m_stringSort ==
null) m_stringSort =
new SeqSort(
this, Native.Z3_mk_string_sort(nCtx));
184 Debug.Assert(s !=
null);
186 CheckContextMatch(s);
221 return new BitVecSort(
this, Native.Z3_mk_bv_sort(nCtx, size));
230 Debug.Assert(s !=
null);
231 return new SeqSort(
this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
239 Debug.Assert(s !=
null);
240 return new ReSort(
this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
248 Debug.Assert(domain !=
null);
249 Debug.Assert(
range !=
null);
251 CheckContextMatch(domain);
252 CheckContextMatch(
range);
261 Debug.Assert(domain !=
null);
262 Debug.Assert(
range !=
null);
264 CheckContextMatch<Sort>(domain);
265 CheckContextMatch(
range);
274 Debug.Assert(name !=
null);
275 Debug.Assert(fieldNames !=
null);
276 Debug.Assert(fieldNames.All(fn => fn !=
null));
277 Debug.Assert(fieldSorts ==
null || fieldSorts.All(fs => fs !=
null));
279 CheckContextMatch(name);
280 CheckContextMatch<Symbol>(fieldNames);
281 CheckContextMatch<Sort>(fieldSorts);
282 return new TupleSort(
this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
290 Debug.Assert(name !=
null);
291 Debug.Assert(enumNames !=
null);
292 Debug.Assert(enumNames.All(f => f !=
null));
295 CheckContextMatch(name);
296 CheckContextMatch<Symbol>(enumNames);
297 return new EnumSort(
this, name, enumNames);
305 Debug.Assert(enumNames !=
null);
315 Debug.Assert(name !=
null);
316 Debug.Assert(elemSort !=
null);
318 CheckContextMatch(name);
319 CheckContextMatch(elemSort);
320 return new ListSort(
this, name, elemSort);
328 Debug.Assert(elemSort !=
null);
330 CheckContextMatch(elemSort);
342 Debug.Assert(name !=
null);
344 CheckContextMatch(name);
376 Debug.Assert(name !=
null);
377 Debug.Assert(recognizer !=
null);
379 return new Constructor(
this, name, recognizer, fieldNames, sorts, sortRefs);
402 Debug.Assert(name !=
null);
403 Debug.Assert(constructors !=
null);
404 Debug.Assert(constructors.All(c => c !=
null));
407 CheckContextMatch(name);
408 CheckContextMatch<Constructor>(constructors);
417 Debug.Assert(constructors !=
null);
418 Debug.Assert(constructors.All(c => c !=
null));
420 CheckContextMatch<Constructor>(constructors);
431 Debug.Assert(names !=
null);
432 Debug.Assert(c !=
null);
433 Debug.Assert(names.Length == c.Length);
435 Debug.Assert(names.All(name => name !=
null));
437 CheckContextMatch<Symbol>(names);
438 uint n = (uint)names.Length;
440 IntPtr[] n_constr =
new IntPtr[n];
441 for (uint i = 0; i < n; i++)
444 CheckContextMatch<Constructor>(constructor);
446 n_constr[i] = cla[i].NativeObject;
448 IntPtr[] n_res =
new IntPtr[n];
449 Native.Z3_mk_datatypes(nCtx, n,
Symbol.ArrayToNative(names), n_res, n_constr);
451 for (uint i = 0; i < n; i++)
464 Debug.Assert(names !=
null);
465 Debug.Assert(c !=
null);
466 Debug.Assert(names.Length == c.Length);
481 return Expr.Create(
this, Native.Z3_datatype_update_field(
482 nCtx, field.NativeObject,
483 t.NativeObject, v.NativeObject));
489 #region Function Declarations
495 Debug.Assert(name !=
null);
496 Debug.Assert(
range !=
null);
497 Debug.Assert(domain.All(d => d !=
null));
499 CheckContextMatch(name);
500 CheckContextMatch<Sort>(domain);
501 CheckContextMatch(
range);
510 Debug.Assert(name !=
null);
511 Debug.Assert(domain !=
null);
512 Debug.Assert(
range !=
null);
514 CheckContextMatch(name);
515 CheckContextMatch(domain);
516 CheckContextMatch(
range);
526 Debug.Assert(
range !=
null);
527 Debug.Assert(domain.All(d => d !=
null));
529 CheckContextMatch<Sort>(domain);
530 CheckContextMatch(
range);
539 Debug.Assert(
range !=
null);
540 Debug.Assert(domain.All(d => d !=
null));
542 CheckContextMatch<Sort>(domain);
543 CheckContextMatch(
range);
555 CheckContextMatch(f);
556 CheckContextMatch<Expr>(args);
557 CheckContextMatch(body);
558 IntPtr[] argsNative =
AST.ArrayToNative(args);
559 Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
567 Debug.Assert(
range !=
null);
568 Debug.Assert(domain !=
null);
570 CheckContextMatch(domain);
571 CheckContextMatch(
range);
583 Debug.Assert(
range !=
null);
584 Debug.Assert(domain.All(d => d !=
null));
586 CheckContextMatch<Sort>(domain);
587 CheckContextMatch(
range);
596 Debug.Assert(name !=
null);
597 Debug.Assert(
range !=
null);
599 CheckContextMatch(name);
600 CheckContextMatch(
range);
609 Debug.Assert(
range !=
null);
611 CheckContextMatch(
range);
622 Debug.Assert(
range !=
null);
624 CheckContextMatch(
range);
629 #region Bound Variables
637 Debug.Assert(ty !=
null);
639 return Expr.Create(
this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
643 #region Quantifier Patterns
649 Debug.Assert(terms !=
null);
650 if (terms.Length == 0)
651 throw new Z3Exception(
"Cannot create a pattern from zero terms");
653 IntPtr[] termsNative =
AST.ArrayToNative(terms);
654 return new Pattern(
this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
664 Debug.Assert(name !=
null);
665 Debug.Assert(
range !=
null);
667 CheckContextMatch(name);
668 CheckContextMatch(
range);
670 return Expr.Create(
this, Native.Z3_mk_const(nCtx, name.NativeObject,
range.NativeObject));
678 Debug.Assert(
range !=
null);
689 Debug.Assert(
range !=
null);
691 CheckContextMatch(
range);
692 return Expr.Create(
this, Native.Z3_mk_fresh_const(nCtx, prefix,
range.NativeObject));
701 Debug.Assert(f !=
null);
711 Debug.Assert(name !=
null);
730 Debug.Assert(name !=
null);
740 Debug.Assert(name !=
null);
750 Debug.Assert(name !=
null);
769 Debug.Assert(name !=
null);
790 Debug.Assert(f !=
null);
791 Debug.Assert(args ==
null || args.All(a => a !=
null));
793 CheckContextMatch(f);
794 CheckContextMatch<Expr>(args);
795 return Expr.Create(
this, f, args);
803 Debug.Assert(f !=
null);
804 Debug.Assert(args ==
null || args.All( a => a !=
null));
806 CheckContextMatch(f);
807 CheckContextMatch(args);
808 return Expr.Create(
this, f, args.ToArray());
811 #region Propositional
818 return new BoolExpr(
this, Native.Z3_mk_true(nCtx));
827 return new BoolExpr(
this, Native.Z3_mk_false(nCtx));
844 Debug.Assert(x !=
null);
845 Debug.Assert(y !=
null);
847 CheckContextMatch(x);
848 CheckContextMatch(y);
849 return new BoolExpr(
this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
857 Debug.Assert(args !=
null);
858 Debug.Assert(args.All(a => a !=
null));
861 CheckContextMatch<Expr>(args);
862 return new BoolExpr(
this, Native.Z3_mk_distinct(nCtx, (uint)args.Length,
AST.ArrayToNative(args)));
870 Debug.Assert(a !=
null);
872 CheckContextMatch(a);
873 return new BoolExpr(
this, Native.Z3_mk_not(nCtx, a.NativeObject));
884 Debug.Assert(t1 !=
null);
885 Debug.Assert(t2 !=
null);
886 Debug.Assert(t3 !=
null);
888 CheckContextMatch(t1);
889 CheckContextMatch(t2);
890 CheckContextMatch(t3);
891 return Expr.Create(
this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
899 Debug.Assert(t1 !=
null);
900 Debug.Assert(t2 !=
null);
902 CheckContextMatch(t1);
903 CheckContextMatch(t2);
904 return new BoolExpr(
this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
912 Debug.Assert(t1 !=
null);
913 Debug.Assert(t2 !=
null);
915 CheckContextMatch(t1);
916 CheckContextMatch(t2);
917 return new BoolExpr(
this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
925 Debug.Assert(t1 !=
null);
926 Debug.Assert(t2 !=
null);
928 CheckContextMatch(t1);
929 CheckContextMatch(t2);
930 return new BoolExpr(
this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
938 Debug.Assert(ts !=
null);
939 Debug.Assert(ts.All(a => a !=
null));
940 CheckContextMatch<BoolExpr>(ts);
942 foreach (var t
in ts) {
958 Debug.Assert(t !=
null);
959 Debug.Assert(t.All(a => a !=
null));
961 CheckContextMatch<BoolExpr>(t);
962 return new BoolExpr(
this, Native.Z3_mk_and(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
970 Debug.Assert(t !=
null);
971 Debug.Assert(t.All(a => a !=
null));
972 CheckContextMatch<BoolExpr>(t);
973 return new BoolExpr(
this, Native.Z3_mk_and(nCtx, (uint)t.Count(),
AST.EnumToNative(t)));
981 Debug.Assert(t !=
null);
982 Debug.Assert(t.All(a => a !=
null));
984 CheckContextMatch<BoolExpr>(t);
985 return new BoolExpr(
this, Native.Z3_mk_or(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
994 Debug.Assert(t !=
null);
995 Debug.Assert(t.All(a => a !=
null));
997 CheckContextMatch(t);
998 return new BoolExpr(
this, Native.Z3_mk_or(nCtx, (uint)t.Count(),
AST.EnumToNative(t)));
1009 Debug.Assert(t !=
null);
1010 Debug.Assert(t.All(a => a !=
null));
1012 CheckContextMatch<ArithExpr>(t);
1013 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_add(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
1021 Debug.Assert(t !=
null);
1022 Debug.Assert(t.All(a => a !=
null));
1024 CheckContextMatch(t);
1025 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_add(nCtx, (uint)t.Count(),
AST.EnumToNative(t)));
1033 Debug.Assert(t !=
null);
1034 Debug.Assert(t.All(a => a !=
null));
1036 CheckContextMatch<ArithExpr>(t);
1037 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_mul(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
1045 Debug.Assert(t !=
null);
1046 Debug.Assert(t.All(a => a !=
null));
1048 CheckContextMatch<ArithExpr>(t);
1049 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_mul(nCtx, (uint)t.Count(),
AST.EnumToNative(t)));
1057 Debug.Assert(t !=
null);
1058 Debug.Assert(t.All(a => a !=
null));
1060 CheckContextMatch<ArithExpr>(t);
1061 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_sub(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
1069 Debug.Assert(t !=
null);
1071 CheckContextMatch(t);
1072 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
1080 Debug.Assert(t1 !=
null);
1081 Debug.Assert(t2 !=
null);
1083 CheckContextMatch(t1);
1084 CheckContextMatch(t2);
1085 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1094 Debug.Assert(t1 !=
null);
1095 Debug.Assert(t2 !=
null);
1097 CheckContextMatch(t1);
1098 CheckContextMatch(t2);
1099 return new IntExpr(
this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1108 Debug.Assert(t1 !=
null);
1109 Debug.Assert(t2 !=
null);
1111 CheckContextMatch(t1);
1112 CheckContextMatch(t2);
1113 return new IntExpr(
this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1121 Debug.Assert(t1 !=
null);
1122 Debug.Assert(t2 !=
null);
1124 CheckContextMatch(t1);
1125 CheckContextMatch(t2);
1126 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1134 Debug.Assert(t1 !=
null);
1135 Debug.Assert(t2 !=
null);
1137 CheckContextMatch(t1);
1138 CheckContextMatch(t2);
1139 return new BoolExpr(
this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1147 Debug.Assert(t1 !=
null);
1148 Debug.Assert(t2 !=
null);
1150 CheckContextMatch(t1);
1151 CheckContextMatch(t2);
1152 return new BoolExpr(
this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1160 Debug.Assert(t1 !=
null);
1161 Debug.Assert(t2 !=
null);
1163 CheckContextMatch(t1);
1164 CheckContextMatch(t2);
1165 return new BoolExpr(
this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1173 Debug.Assert(t1 !=
null);
1174 Debug.Assert(t2 !=
null);
1176 CheckContextMatch(t1);
1177 CheckContextMatch(t2);
1178 return new BoolExpr(
this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1193 Debug.Assert(t !=
null);
1195 CheckContextMatch(t);
1196 return new RealExpr(
this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1208 Debug.Assert(t !=
null);
1210 CheckContextMatch(t);
1211 return new IntExpr(
this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1219 Debug.Assert(t !=
null);
1221 CheckContextMatch(t);
1222 return new BoolExpr(
this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1233 Debug.Assert(t !=
null);
1235 CheckContextMatch(t);
1236 return new BitVecExpr(
this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1245 Debug.Assert(t !=
null);
1247 CheckContextMatch(t);
1248 return new BitVecExpr(
this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1257 Debug.Assert(t !=
null);
1259 CheckContextMatch(t);
1260 return new BitVecExpr(
this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1269 Debug.Assert(t1 !=
null);
1270 Debug.Assert(t2 !=
null);
1272 CheckContextMatch(t1);
1273 CheckContextMatch(t2);
1274 return new BitVecExpr(
this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1283 Debug.Assert(t1 !=
null);
1284 Debug.Assert(t2 !=
null);
1286 CheckContextMatch(t1);
1287 CheckContextMatch(t2);
1288 return new BitVecExpr(
this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1297 Debug.Assert(t1 !=
null);
1298 Debug.Assert(t2 !=
null);
1300 CheckContextMatch(t1);
1301 CheckContextMatch(t2);
1302 return new BitVecExpr(
this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1311 Debug.Assert(t1 !=
null);
1312 Debug.Assert(t2 !=
null);
1314 CheckContextMatch(t1);
1315 CheckContextMatch(t2);
1316 return new BitVecExpr(
this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1325 Debug.Assert(t1 !=
null);
1326 Debug.Assert(t2 !=
null);
1328 CheckContextMatch(t1);
1329 CheckContextMatch(t2);
1330 return new BitVecExpr(
this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1339 Debug.Assert(t1 !=
null);
1340 Debug.Assert(t2 !=
null);
1342 CheckContextMatch(t1);
1343 CheckContextMatch(t2);
1344 return new BitVecExpr(
this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1353 Debug.Assert(t !=
null);
1355 CheckContextMatch(t);
1356 return new BitVecExpr(
this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1365 Debug.Assert(t1 !=
null);
1366 Debug.Assert(t2 !=
null);
1368 CheckContextMatch(t1);
1369 CheckContextMatch(t2);
1370 return new BitVecExpr(
this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1379 Debug.Assert(t1 !=
null);
1380 Debug.Assert(t2 !=
null);
1382 CheckContextMatch(t1);
1383 CheckContextMatch(t2);
1384 return new BitVecExpr(
this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1393 Debug.Assert(t1 !=
null);
1394 Debug.Assert(t2 !=
null);
1396 CheckContextMatch(t1);
1397 CheckContextMatch(t2);
1398 return new BitVecExpr(
this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1412 Debug.Assert(t1 !=
null);
1413 Debug.Assert(t2 !=
null);
1415 CheckContextMatch(t1);
1416 CheckContextMatch(t2);
1417 return new BitVecExpr(
this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1435 Debug.Assert(t1 !=
null);
1436 Debug.Assert(t2 !=
null);
1438 CheckContextMatch(t1);
1439 CheckContextMatch(t2);
1440 return new BitVecExpr(
this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1453 Debug.Assert(t1 !=
null);
1454 Debug.Assert(t2 !=
null);
1456 CheckContextMatch(t1);
1457 CheckContextMatch(t2);
1458 return new BitVecExpr(
this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1473 Debug.Assert(t1 !=
null);
1474 Debug.Assert(t2 !=
null);
1476 CheckContextMatch(t1);
1477 CheckContextMatch(t2);
1478 return new BitVecExpr(
this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1490 Debug.Assert(t1 !=
null);
1491 Debug.Assert(t2 !=
null);
1493 CheckContextMatch(t1);
1494 CheckContextMatch(t2);
1495 return new BitVecExpr(
this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1506 Debug.Assert(t1 !=
null);
1507 Debug.Assert(t2 !=
null);
1509 CheckContextMatch(t1);
1510 CheckContextMatch(t2);
1511 return new BoolExpr(
this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1522 Debug.Assert(t1 !=
null);
1523 Debug.Assert(t2 !=
null);
1525 CheckContextMatch(t1);
1526 CheckContextMatch(t2);
1527 return new BoolExpr(
this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1538 Debug.Assert(t1 !=
null);
1539 Debug.Assert(t2 !=
null);
1541 CheckContextMatch(t1);
1542 CheckContextMatch(t2);
1543 return new BoolExpr(
this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1554 Debug.Assert(t1 !=
null);
1555 Debug.Assert(t2 !=
null);
1557 CheckContextMatch(t1);
1558 CheckContextMatch(t2);
1559 return new BoolExpr(
this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1570 Debug.Assert(t1 !=
null);
1571 Debug.Assert(t2 !=
null);
1573 CheckContextMatch(t1);
1574 CheckContextMatch(t2);
1575 return new BoolExpr(
this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1586 Debug.Assert(t1 !=
null);
1587 Debug.Assert(t2 !=
null);
1589 CheckContextMatch(t1);
1590 CheckContextMatch(t2);
1591 return new BoolExpr(
this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1602 Debug.Assert(t1 !=
null);
1603 Debug.Assert(t2 !=
null);
1605 CheckContextMatch(t1);
1606 CheckContextMatch(t2);
1607 return new BoolExpr(
this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1618 Debug.Assert(t1 !=
null);
1619 Debug.Assert(t2 !=
null);
1621 CheckContextMatch(t1);
1622 CheckContextMatch(t2);
1623 return new BoolExpr(
this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1638 Debug.Assert(t1 !=
null);
1639 Debug.Assert(t2 !=
null);
1641 CheckContextMatch(t1);
1642 CheckContextMatch(t2);
1643 return new BitVecExpr(
this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1657 Debug.Assert(t !=
null);
1659 CheckContextMatch(t);
1660 return new BitVecExpr(
this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1673 Debug.Assert(t !=
null);
1675 CheckContextMatch(t);
1676 return new BitVecExpr(
this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1690 Debug.Assert(t !=
null);
1692 CheckContextMatch(t);
1693 return new BitVecExpr(
this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1704 Debug.Assert(t !=
null);
1706 CheckContextMatch(t);
1707 return new BitVecExpr(
this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1724 Debug.Assert(t1 !=
null);
1725 Debug.Assert(t2 !=
null);
1727 CheckContextMatch(t1);
1728 CheckContextMatch(t2);
1729 return new BitVecExpr(
this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1746 Debug.Assert(t1 !=
null);
1747 Debug.Assert(t2 !=
null);
1749 CheckContextMatch(t1);
1750 CheckContextMatch(t2);
1751 return new BitVecExpr(
this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1770 Debug.Assert(t1 !=
null);
1771 Debug.Assert(t2 !=
null);
1773 CheckContextMatch(t1);
1774 CheckContextMatch(t2);
1775 return new BitVecExpr(
this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1787 Debug.Assert(t !=
null);
1789 CheckContextMatch(t);
1790 return new BitVecExpr(
this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1802 Debug.Assert(t !=
null);
1804 CheckContextMatch(t);
1805 return new BitVecExpr(
this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1817 Debug.Assert(t1 !=
null);
1818 Debug.Assert(t2 !=
null);
1820 CheckContextMatch(t1);
1821 CheckContextMatch(t2);
1822 return new BitVecExpr(
this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1834 Debug.Assert(t1 !=
null);
1835 Debug.Assert(t2 !=
null);
1837 CheckContextMatch(t1);
1838 CheckContextMatch(t2);
1839 return new BitVecExpr(
this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1854 Debug.Assert(t !=
null);
1856 CheckContextMatch(t);
1857 return new BitVecExpr(
this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1877 Debug.Assert(t !=
null);
1879 CheckContextMatch(t);
1880 return new IntExpr(
this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (
byte)(
signed ? 1 : 0)));
1891 Debug.Assert(t1 !=
null);
1892 Debug.Assert(t2 !=
null);
1894 CheckContextMatch(t1);
1895 CheckContextMatch(t2);
1896 return new BoolExpr(
this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (
byte)(isSigned ? 1 : 0)));
1907 Debug.Assert(t1 !=
null);
1908 Debug.Assert(t2 !=
null);
1910 CheckContextMatch(t1);
1911 CheckContextMatch(t2);
1912 return new BoolExpr(
this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1923 Debug.Assert(t1 !=
null);
1924 Debug.Assert(t2 !=
null);
1926 CheckContextMatch(t1);
1927 CheckContextMatch(t2);
1928 return new BoolExpr(
this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1939 Debug.Assert(t1 !=
null);
1940 Debug.Assert(t2 !=
null);
1942 CheckContextMatch(t1);
1943 CheckContextMatch(t2);
1944 return new BoolExpr(
this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (
byte)(isSigned ? 1 : 0)));
1955 Debug.Assert(t1 !=
null);
1956 Debug.Assert(t2 !=
null);
1958 CheckContextMatch(t1);
1959 CheckContextMatch(t2);
1960 return new BoolExpr(
this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1971 Debug.Assert(t !=
null);
1973 CheckContextMatch(t);
1974 return new BoolExpr(
this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
1985 Debug.Assert(t1 !=
null);
1986 Debug.Assert(t2 !=
null);
1988 CheckContextMatch(t1);
1989 CheckContextMatch(t2);
1990 return new BoolExpr(
this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (
byte)(isSigned ? 1 : 0)));
2001 Debug.Assert(t1 !=
null);
2002 Debug.Assert(t2 !=
null);
2004 CheckContextMatch(t1);
2005 CheckContextMatch(t2);
2006 return new BoolExpr(
this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2016 Debug.Assert(name !=
null);
2017 Debug.Assert(domain !=
null);
2018 Debug.Assert(
range !=
null);
2028 Debug.Assert(domain !=
null);
2029 Debug.Assert(
range !=
null);
2050 Debug.Assert(a !=
null);
2051 Debug.Assert(i !=
null);
2053 CheckContextMatch(a);
2054 CheckContextMatch(i);
2055 return Expr.Create(
this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2073 Debug.Assert(a !=
null);
2074 Debug.Assert(args !=
null && args.All(n => n !=
null));
2076 CheckContextMatch(a);
2077 CheckContextMatch<Expr>(args);
2078 return Expr.Create(
this, Native.Z3_mk_select_n(nCtx, a.NativeObject,
AST.ArrayLength(args),
AST.ArrayToNative(args)));
2102 Debug.Assert(a !=
null);
2103 Debug.Assert(i !=
null);
2104 Debug.Assert(v !=
null);
2106 CheckContextMatch(a);
2107 CheckContextMatch(i);
2108 CheckContextMatch(v);
2109 return new ArrayExpr(
this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2132 Debug.Assert(a !=
null);
2133 Debug.Assert(args !=
null);
2134 Debug.Assert(v !=
null);
2136 CheckContextMatch<Expr>(args);
2137 CheckContextMatch(a);
2138 CheckContextMatch(v);
2139 return new ArrayExpr(
this, Native.Z3_mk_store_n(nCtx, a.NativeObject,
AST.ArrayLength(args),
AST.ArrayToNative(args), v.NativeObject));
2153 Debug.Assert(domain !=
null);
2154 Debug.Assert(v !=
null);
2156 CheckContextMatch(domain);
2157 CheckContextMatch(v);
2158 return new ArrayExpr(
this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2174 Debug.Assert(f !=
null);
2175 Debug.Assert(args ==
null || args.All(a => a !=
null));
2177 CheckContextMatch(f);
2178 CheckContextMatch<ArrayExpr>(args);
2179 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_map(nCtx, f.NativeObject,
AST.ArrayLength(args),
AST.ArrayToNative(args)));
2191 Debug.Assert(array !=
null);
2193 CheckContextMatch(array);
2194 return Expr.Create(
this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2202 Debug.Assert(arg1 !=
null);
2203 Debug.Assert(arg2 !=
null);
2205 CheckContextMatch(arg1);
2206 CheckContextMatch(arg2);
2207 return Expr.Create(
this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
2218 Debug.Assert(ty !=
null);
2220 CheckContextMatch(ty);
2229 Debug.Assert(domain !=
null);
2231 CheckContextMatch(domain);
2232 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2240 Debug.Assert(domain !=
null);
2242 CheckContextMatch(domain);
2243 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2251 Debug.Assert(
set !=
null);
2252 Debug.Assert(element !=
null);
2254 CheckContextMatch(
set);
2255 CheckContextMatch(element);
2256 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_add(nCtx,
set.NativeObject, element.NativeObject));
2265 Debug.Assert(
set !=
null);
2266 Debug.Assert(element !=
null);
2268 CheckContextMatch(
set);
2269 CheckContextMatch(element);
2270 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_del(nCtx,
set.NativeObject, element.NativeObject));
2278 Debug.Assert(args !=
null);
2279 Debug.Assert(args.All(a => a !=
null));
2281 CheckContextMatch<ArrayExpr>(args);
2282 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_union(nCtx, (uint)args.Length,
AST.ArrayToNative(args)));
2290 Debug.Assert(args !=
null);
2291 Debug.Assert(args.All(a => a !=
null));
2293 CheckContextMatch<ArrayExpr>(args);
2294 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length,
AST.ArrayToNative(args)));
2302 Debug.Assert(arg1 !=
null);
2303 Debug.Assert(arg2 !=
null);
2305 CheckContextMatch(arg1);
2306 CheckContextMatch(arg2);
2307 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2315 Debug.Assert(arg !=
null);
2317 CheckContextMatch(arg);
2318 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2326 Debug.Assert(elem !=
null);
2327 Debug.Assert(
set !=
null);
2329 CheckContextMatch(elem);
2330 CheckContextMatch(
set);
2331 return (
BoolExpr)
Expr.Create(
this, Native.Z3_mk_set_member(nCtx, elem.NativeObject,
set.NativeObject));
2339 Debug.Assert(arg1 !=
null);
2340 Debug.Assert(arg2 !=
null);
2342 CheckContextMatch(arg1);
2343 CheckContextMatch(arg2);
2344 return (
BoolExpr)
Expr.Create(
this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2349 #region Sequence, string and regular expressions
2356 Debug.Assert(s !=
null);
2357 return new SeqExpr(
this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
2365 Debug.Assert(elem !=
null);
2366 return new SeqExpr(
this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
2374 Debug.Assert(s !=
null);
2375 return new SeqExpr(
this, Native.Z3_mk_string(nCtx, s));
2383 Debug.Assert(e !=
null);
2385 return new SeqExpr(
this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
2393 Debug.Assert(e !=
null);
2395 return new IntExpr(
this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject));
2404 Debug.Assert(t !=
null);
2405 Debug.Assert(t.All(a => a !=
null));
2407 CheckContextMatch<SeqExpr>(t);
2408 return new SeqExpr(
this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
2417 Debug.Assert(s !=
null);
2418 return (
IntExpr)
Expr.Create(
this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
2426 Debug.Assert(s1 !=
null);
2427 Debug.Assert(s2 !=
null);
2428 CheckContextMatch(s1, s2);
2429 return new BoolExpr(
this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
2437 Debug.Assert(s1 !=
null);
2438 Debug.Assert(s2 !=
null);
2439 CheckContextMatch(s1, s2);
2440 return new BoolExpr(
this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
2448 Debug.Assert(s1 !=
null);
2449 Debug.Assert(s2 !=
null);
2450 CheckContextMatch(s1, s2);
2451 return new BoolExpr(
this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
2459 Debug.Assert(s1 !=
null);
2460 Debug.Assert(s2 !=
null);
2461 CheckContextMatch(s1, s2);
2462 return new BoolExpr(
this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject));
2470 Debug.Assert(s1 !=
null);
2471 Debug.Assert(s2 !=
null);
2472 CheckContextMatch(s1, s2);
2473 return new BoolExpr(
this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject));
2481 Debug.Assert(s !=
null);
2482 Debug.Assert(index !=
null);
2483 CheckContextMatch(s, index);
2484 return new SeqExpr(
this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
2492 Debug.Assert(s !=
null);
2493 Debug.Assert(index !=
null);
2494 CheckContextMatch(s, index);
2495 return Expr.Create(
this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
2503 Debug.Assert(s !=
null);
2504 Debug.Assert(offset !=
null);
2505 Debug.Assert(length !=
null);
2506 CheckContextMatch(s, offset, length);
2507 return new SeqExpr(
this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
2515 Debug.Assert(s !=
null);
2516 Debug.Assert(offset !=
null);
2517 Debug.Assert(substr !=
null);
2518 CheckContextMatch(s, substr, offset);
2519 return new IntExpr(
this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
2527 Debug.Assert(s !=
null);
2528 Debug.Assert(src !=
null);
2529 Debug.Assert(dst !=
null);
2530 CheckContextMatch(s, src, dst);
2531 return new SeqExpr(
this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
2539 Debug.Assert(s !=
null);
2540 return new ReExpr(
this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));
2549 Debug.Assert(s !=
null);
2550 Debug.Assert(re !=
null);
2551 CheckContextMatch(s, re);
2552 return new BoolExpr(
this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
2560 Debug.Assert(re !=
null);
2561 return new ReExpr(
this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
2569 Debug.Assert(re !=
null);
2570 return new ReExpr(
this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi));
2578 Debug.Assert(re !=
null);
2579 return new ReExpr(
this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));
2587 Debug.Assert(re !=
null);
2588 return new ReExpr(
this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
2596 Debug.Assert(re !=
null);
2597 return new ReExpr(
this, Native.Z3_mk_re_complement(nCtx, re.NativeObject));
2605 Debug.Assert(t !=
null);
2606 Debug.Assert(t.All(a => a !=
null));
2608 CheckContextMatch<ReExpr>(t);
2609 return new ReExpr(
this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
2617 Debug.Assert(t !=
null);
2618 Debug.Assert(t.All(a => a !=
null));
2620 CheckContextMatch<ReExpr>(t);
2621 return new ReExpr(
this, Native.Z3_mk_re_union(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
2629 Debug.Assert(t !=
null);
2630 Debug.Assert(t.All(a => a !=
null));
2632 CheckContextMatch<ReExpr>(t);
2633 return new ReExpr(
this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
2642 Debug.Assert(s !=
null);
2643 return new ReExpr(
this, Native.Z3_mk_re_empty(nCtx, s.NativeObject));
2652 Debug.Assert(s !=
null);
2653 return new ReExpr(
this, Native.Z3_mk_re_full(nCtx, s.NativeObject));
2662 Debug.Assert(lo !=
null);
2663 Debug.Assert(hi !=
null);
2664 CheckContextMatch(lo, hi);
2665 return new ReExpr(
this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
2670 #region Pseudo-Boolean constraints
2677 Debug.Assert(args !=
null);
2678 CheckContextMatch<BoolExpr>(args);
2679 return new BoolExpr(
this, Native.Z3_mk_atmost(nCtx, (uint) args.Count(),
2680 AST.EnumToNative(args), k));
2688 Debug.Assert(args !=
null);
2689 CheckContextMatch<BoolExpr>(args);
2690 return new BoolExpr(
this, Native.Z3_mk_atleast(nCtx, (uint) args.Count(),
2691 AST.EnumToNative(args), k));
2699 Debug.Assert(args !=
null);
2700 Debug.Assert(coeffs !=
null);
2701 Debug.Assert(args.Length == coeffs.Length);
2702 CheckContextMatch<BoolExpr>(args);
2703 return new BoolExpr(
this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
2704 AST.ArrayToNative(args),
2713 Debug.Assert(args !=
null);
2714 Debug.Assert(coeffs !=
null);
2715 Debug.Assert(args.Length == coeffs.Length);
2716 CheckContextMatch<BoolExpr>(args);
2717 return new BoolExpr(
this, Native.Z3_mk_pbge(nCtx, (uint) args.Length,
2718 AST.ArrayToNative(args),
2726 Debug.Assert(args !=
null);
2727 Debug.Assert(coeffs !=
null);
2728 Debug.Assert(args.Length == coeffs.Length);
2729 CheckContextMatch<BoolExpr>(args);
2730 return new BoolExpr(
this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length,
2731 AST.ArrayToNative(args),
2738 #region General Numerals
2747 Debug.Assert(ty !=
null);
2749 CheckContextMatch(ty);
2750 return Expr.Create(
this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2762 Debug.Assert(ty !=
null);
2764 CheckContextMatch(ty);
2765 return Expr.Create(
this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2777 Debug.Assert(ty !=
null);
2779 CheckContextMatch(ty);
2780 return Expr.Create(
this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2792 Debug.Assert(ty !=
null);
2794 CheckContextMatch(ty);
2795 return Expr.Create(
this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2807 Debug.Assert(ty !=
null);
2809 CheckContextMatch(ty);
2810 return Expr.Create(
this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2827 return new RatNum(
this, Native.Z3_mk_real(nCtx, num, den));
2838 return new RatNum(
this, Native.Z3_mk_numeral(nCtx, v,
RealSort.NativeObject));
2849 return new RatNum(
this, Native.Z3_mk_int(nCtx, v,
RealSort.NativeObject));
2860 return new RatNum(
this, Native.Z3_mk_unsigned_int(nCtx, v,
RealSort.NativeObject));
2871 return new RatNum(
this, Native.Z3_mk_int64(nCtx, v,
RealSort.NativeObject));
2882 return new RatNum(
this, Native.Z3_mk_unsigned_int64(nCtx, v,
RealSort.NativeObject));
2894 return new IntNum(
this, Native.Z3_mk_numeral(nCtx, v,
IntSort.NativeObject));
2905 return new IntNum(
this, Native.Z3_mk_int(nCtx, v,
IntSort.NativeObject));
2916 return new IntNum(
this, Native.Z3_mk_unsigned_int(nCtx, v,
IntSort.NativeObject));
2927 return new IntNum(
this, Native.Z3_mk_int64(nCtx, v,
IntSort.NativeObject));
2938 return new IntNum(
this, Native.Z3_mk_unsigned_int64(nCtx, v,
IntSort.NativeObject));
3004 byte[] _bits =
new byte[bits.Length];
3005 for (
int i = 0; i < bits.Length; ++i) _bits[i] = (
byte)(bits[i] ? 1 : 0);
3006 return (
BitVecNum)
Expr.Create(
this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
3041 Debug.Assert(sorts !=
null);
3042 Debug.Assert(names !=
null);
3043 Debug.Assert(body !=
null);
3044 Debug.Assert(sorts.Length == names.Length);
3045 Debug.Assert(sorts.All(s => s !=
null));
3046 Debug.Assert(names.All(n => n !=
null));
3047 Debug.Assert(patterns ==
null || patterns.All(p => p !=
null));
3048 Debug.Assert(noPatterns ==
null || noPatterns.All(np => np !=
null));
3051 return new Quantifier(
this,
true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3065 Debug.Assert(body !=
null);
3066 Debug.Assert(boundConstants ==
null || boundConstants.All(b => b !=
null));
3067 Debug.Assert(patterns ==
null || patterns.All(p => p !=
null));
3068 Debug.Assert(noPatterns ==
null || noPatterns.All(np => np !=
null));
3071 return new Quantifier(
this,
true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3083 Debug.Assert(sorts !=
null);
3084 Debug.Assert(names !=
null);
3085 Debug.Assert(body !=
null);
3086 Debug.Assert(sorts.Length == names.Length);
3087 Debug.Assert(sorts.All(s => s !=
null));
3088 Debug.Assert(names.All(n => n !=
null));
3089 Debug.Assert(patterns ==
null || patterns.All(p => p !=
null));
3090 Debug.Assert(noPatterns ==
null || noPatterns.All(np => np !=
null));
3092 return new Quantifier(
this,
false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3105 Debug.Assert(body !=
null);
3106 Debug.Assert(boundConstants ==
null || boundConstants.All(n => n !=
null));
3107 Debug.Assert(patterns ==
null || patterns.All(p => p !=
null));
3108 Debug.Assert(noPatterns ==
null || noPatterns.All(np => np !=
null));
3110 return new Quantifier(
this,
false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3120 Debug.Assert(body !=
null);
3121 Debug.Assert(names !=
null);
3122 Debug.Assert(sorts !=
null);
3123 Debug.Assert(sorts.Length == names.Length);
3124 Debug.Assert(sorts.All(s => s !=
null));
3125 Debug.Assert(names.All(n => n !=
null));
3126 Debug.Assert(patterns ==
null || patterns.All(p => p !=
null));
3127 Debug.Assert(noPatterns ==
null || noPatterns.All(np => np !=
null));
3131 return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3133 return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3143 Debug.Assert(body !=
null);
3144 Debug.Assert(boundConstants ==
null || boundConstants.All(n => n !=
null));
3145 Debug.Assert(patterns ==
null || patterns.All(p => p !=
null));
3146 Debug.Assert(noPatterns ==
null || noPatterns.All(np => np !=
null));
3150 return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3152 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3175 Debug.Assert(sorts !=
null);
3176 Debug.Assert(names !=
null);
3177 Debug.Assert(body !=
null);
3178 Debug.Assert(sorts.Length == names.Length);
3179 Debug.Assert(sorts.All(s => s !=
null));
3180 Debug.Assert(names.All(n => n !=
null));
3181 return new Lambda(
this, sorts, names, body);
3194 Debug.Assert(body !=
null);
3195 Debug.Assert(boundConstants !=
null && boundConstants.All(b => b !=
null));
3196 return new Lambda(
this, boundConstants, body);
3223 set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
3227 #region SMT Files & Strings
3236 uint csn =
Symbol.ArrayLength(sortNames);
3237 uint cs =
Sort.ArrayLength(sorts);
3238 uint cdn =
Symbol.ArrayLength(declNames);
3239 uint cd =
AST.ArrayLength(decls);
3240 if (csn != cs || cdn != cd)
3243 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
3244 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls)));
3255 uint csn =
Symbol.ArrayLength(sortNames);
3256 uint cs =
Sort.ArrayLength(sorts);
3257 uint cdn =
Symbol.ArrayLength(declNames);
3258 uint cd =
AST.ArrayLength(decls);
3259 if (csn != cs || cdn != cd)
3261 ASTVector assertions =
new ASTVector(
this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
3262 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
3263 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls)));
3279 public Goal MkGoal(
bool models =
true,
bool unsatCores =
false,
bool proofs =
false)
3282 return new Goal(
this, models, unsatCores, proofs);
3286 #region ParameterSets
3303 get {
return Native.Z3_get_num_tactics(nCtx); }
3315 string[] res =
new string[n];
3316 for (uint i = 0; i < n; i++)
3317 res[i] = Native.Z3_get_tactic_name(nCtx, i);
3328 return Native.Z3_tactic_get_descr(nCtx, name);
3337 return new Tactic(
this, name);
3346 Debug.Assert(t1 !=
null);
3347 Debug.Assert(t2 !=
null);
3351 CheckContextMatch(t1);
3352 CheckContextMatch(t2);
3353 CheckContextMatch<Tactic>(ts);
3355 IntPtr last = IntPtr.Zero;
3356 if (ts !=
null && ts.Length > 0)
3358 last = ts[ts.Length - 1].NativeObject;
3359 for (
int i = ts.Length - 2; i >= 0; i--)
3360 last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3362 if (last != IntPtr.Zero)
3364 last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3365 return new Tactic(
this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3368 return new Tactic(
this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3380 Debug.Assert(t1 !=
null);
3381 Debug.Assert(t2 !=
null);
3393 Debug.Assert(t1 !=
null);
3394 Debug.Assert(t2 !=
null);
3396 CheckContextMatch(t1);
3397 CheckContextMatch(t2);
3398 return new Tactic(
this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3409 Debug.Assert(t !=
null);
3411 CheckContextMatch(t);
3412 return new Tactic(
this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3424 Debug.Assert(p !=
null);
3425 Debug.Assert(t !=
null);
3427 CheckContextMatch(t);
3428 CheckContextMatch(p);
3429 return new Tactic(
this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3438 Debug.Assert(p !=
null);
3439 Debug.Assert(t1 !=
null);
3440 Debug.Assert(t2 !=
null);
3442 CheckContextMatch(p);
3443 CheckContextMatch(t1);
3444 CheckContextMatch(t2);
3445 return new Tactic(
this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3454 Debug.Assert(t !=
null);
3456 CheckContextMatch(t);
3457 return new Tactic(
this, Native.Z3_tactic_repeat(nCtx, t.NativeObject,
max));
3466 return new Tactic(
this, Native.Z3_tactic_skip(nCtx));
3475 return new Tactic(
this, Native.Z3_tactic_fail(nCtx));
3483 Debug.Assert(p !=
null);
3485 CheckContextMatch(p);
3486 return new Tactic(
this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3496 return new Tactic(
this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3504 Debug.Assert(t !=
null);
3505 Debug.Assert(p !=
null);
3507 CheckContextMatch(t);
3508 CheckContextMatch(p);
3509 return new Tactic(
this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3518 Debug.Assert(t !=
null);
3519 Debug.Assert(p !=
null);
3529 Debug.Assert(t ==
null || t.All(tactic => tactic !=
null));
3531 CheckContextMatch<Tactic>(t);
3532 return new Tactic(
this, Native.Z3_tactic_par_or(nCtx,
Tactic.ArrayLength(t),
Tactic.ArrayToNative(t)));
3541 Debug.Assert(t1 !=
null);
3542 Debug.Assert(t2 !=
null);
3544 CheckContextMatch(t1);
3545 CheckContextMatch(t2);
3546 return new Tactic(
this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3555 Native.Z3_interrupt(nCtx);
3565 get {
return Native.Z3_get_num_probes(nCtx); }
3577 string[] res =
new string[n];
3578 for (uint i = 0; i < n; i++)
3579 res[i] = Native.Z3_get_probe_name(nCtx, i);
3590 return Native.Z3_probe_get_descr(nCtx, name);
3599 return new Probe(
this, name);
3608 return new Probe(
this, Native.Z3_probe_const(nCtx, val));
3617 Debug.Assert(p1 !=
null);
3618 Debug.Assert(p2 !=
null);
3620 CheckContextMatch(p1);
3621 CheckContextMatch(p2);
3622 return new Probe(
this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3631 Debug.Assert(p1 !=
null);
3632 Debug.Assert(p2 !=
null);
3634 CheckContextMatch(p1);
3635 CheckContextMatch(p2);
3636 return new Probe(
this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3645 Debug.Assert(p1 !=
null);
3646 Debug.Assert(p2 !=
null);
3648 CheckContextMatch(p1);
3649 CheckContextMatch(p2);
3650 return new Probe(
this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3659 Debug.Assert(p1 !=
null);
3660 Debug.Assert(p2 !=
null);
3662 CheckContextMatch(p1);
3663 CheckContextMatch(p2);
3664 return new Probe(
this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3673 Debug.Assert(p1 !=
null);
3674 Debug.Assert(p2 !=
null);
3676 CheckContextMatch(p1);
3677 CheckContextMatch(p2);
3678 return new Probe(
this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3687 Debug.Assert(p1 !=
null);
3688 Debug.Assert(p2 !=
null);
3690 CheckContextMatch(p1);
3691 CheckContextMatch(p2);
3692 return new Probe(
this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3701 Debug.Assert(p1 !=
null);
3702 Debug.Assert(p2 !=
null);
3704 CheckContextMatch(p1);
3705 CheckContextMatch(p2);
3706 return new Probe(
this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3715 Debug.Assert(p !=
null);
3717 CheckContextMatch(p);
3718 return new Probe(
this, Native.Z3_probe_not(nCtx, p.NativeObject));
3735 return new Solver(
this, Native.Z3_mk_solver(nCtx));
3737 return new Solver(
this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3756 return new Solver(
this, Native.Z3_mk_simple_solver(nCtx));
3770 return new Solver(
this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3785 #region Optimization
3796 #region Floating-Point Arithmetic
3798 #region Rounding Modes
3799 #region RoundingMode Sort
3815 return new FPRMExpr(
this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
3823 return new FPRMNum(
this, Native.Z3_mk_fpa_rne(nCtx));
3831 return new FPRMNum(
this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
3839 return new FPRMNum(
this, Native.Z3_mk_fpa_rna(nCtx));
3847 return new FPRMNum(
this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
3855 return new FPRMNum(
this, Native.Z3_mk_fpa_rtp(nCtx));
3863 return new FPRMNum(
this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
3871 return new FPRMNum(
this, Native.Z3_mk_fpa_rtn(nCtx));
3879 return new FPRMNum(
this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
3887 return new FPRMNum(
this, Native.Z3_mk_fpa_rtz(nCtx));
3892 #region FloatingPoint Sorts
3900 return new FPSort(
this, ebits, sbits);
3908 return new FPSort(
this, Native.Z3_mk_fpa_sort_half(nCtx));
3916 return new FPSort(
this, Native.Z3_mk_fpa_sort_16(nCtx));
3924 return new FPSort(
this, Native.Z3_mk_fpa_sort_single(nCtx));
3932 return new FPSort(
this, Native.Z3_mk_fpa_sort_32(nCtx));
3940 return new FPSort(
this, Native.Z3_mk_fpa_sort_double(nCtx));
3948 return new FPSort(
this, Native.Z3_mk_fpa_sort_64(nCtx));
3956 return new FPSort(
this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
3964 return new FPSort(
this, Native.Z3_mk_fpa_sort_128(nCtx));
3975 return new FPNum(
this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
3985 return new FPNum(
this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, (
byte)(negative ? 1 : 0)));
3995 return new FPNum(
this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (
byte)(negative ? 1 : 0)));
4005 return new FPNum(
this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
4015 return new FPNum(
this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
4025 return new FPNum(
this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
4037 return new FPNum(
this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (
byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
4049 return new FPNum(
this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (
byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
4115 return new FPExpr(
this, Native.Z3_mk_fpa_abs(
this.nCtx, t.NativeObject));
4124 return new FPExpr(
this, Native.Z3_mk_fpa_neg(
this.nCtx, t.NativeObject));
4135 return new FPExpr(
this, Native.Z3_mk_fpa_add(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4146 return new FPExpr(
this, Native.Z3_mk_fpa_sub(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4157 return new FPExpr(
this, Native.Z3_mk_fpa_mul(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4168 return new FPExpr(
this, Native.Z3_mk_fpa_div(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4183 return new FPExpr(
this, Native.Z3_mk_fpa_fma(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
4193 return new FPExpr(
this, Native.Z3_mk_fpa_sqrt(
this.nCtx, rm.NativeObject, t.NativeObject));
4203 return new FPExpr(
this, Native.Z3_mk_fpa_rem(
this.nCtx, t1.NativeObject, t2.NativeObject));
4214 return new FPExpr(
this, Native.Z3_mk_fpa_round_to_integral(
this.nCtx, rm.NativeObject, t.NativeObject));
4224 return new FPExpr(
this, Native.Z3_mk_fpa_min(
this.nCtx, t1.NativeObject, t2.NativeObject));
4234 return new FPExpr(
this, Native.Z3_mk_fpa_max(
this.nCtx, t1.NativeObject, t2.NativeObject));
4244 return new BoolExpr(
this, Native.Z3_mk_fpa_leq(
this.nCtx, t1.NativeObject, t2.NativeObject));
4254 return new BoolExpr(
this, Native.Z3_mk_fpa_lt(
this.nCtx, t1.NativeObject, t2.NativeObject));
4264 return new BoolExpr(
this, Native.Z3_mk_fpa_geq(
this.nCtx, t1.NativeObject, t2.NativeObject));
4274 return new BoolExpr(
this, Native.Z3_mk_fpa_gt(
this.nCtx, t1.NativeObject, t2.NativeObject));
4287 return new BoolExpr(
this, Native.Z3_mk_fpa_eq(
this.nCtx, t1.NativeObject, t2.NativeObject));
4296 return new BoolExpr(
this, Native.Z3_mk_fpa_is_normal(
this.nCtx, t.NativeObject));
4305 return new BoolExpr(
this, Native.Z3_mk_fpa_is_subnormal(
this.nCtx, t.NativeObject));
4314 return new BoolExpr(
this, Native.Z3_mk_fpa_is_zero(
this.nCtx, t.NativeObject));
4323 return new BoolExpr(
this, Native.Z3_mk_fpa_is_infinite(
this.nCtx, t.NativeObject));
4332 return new BoolExpr(
this, Native.Z3_mk_fpa_is_nan(
this.nCtx, t.NativeObject));
4341 return new BoolExpr(
this, Native.Z3_mk_fpa_is_negative(
this.nCtx, t.NativeObject));
4350 return new BoolExpr(
this, Native.Z3_mk_fpa_is_positive(
this.nCtx, t.NativeObject));
4354 #region Conversions to FloatingPoint terms
4370 return new FPExpr(
this, Native.Z3_mk_fpa_fp(
this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
4386 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_bv(
this.nCtx, bv.NativeObject, s.NativeObject));
4402 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_float(
this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4418 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_real(
this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4437 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_signed(
this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4439 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_unsigned(
this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4454 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_float(
this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
4458 #region Conversions from FloatingPoint terms
4474 return new BitVecExpr(
this, Native.Z3_mk_fpa_to_sbv(
this.nCtx, rm.NativeObject, t.NativeObject, sz));
4476 return new BitVecExpr(
this, Native.Z3_mk_fpa_to_ubv(
this.nCtx, rm.NativeObject, t.NativeObject, sz));
4490 return new RealExpr(
this, Native.Z3_mk_fpa_to_real(
this.nCtx, t.NativeObject));
4494 #region Z3-specific extensions
4507 return new BitVecExpr(
this, Native.Z3_mk_fpa_to_ieee_bv(
this.nCtx, t.NativeObject));
4524 return new BitVecExpr(
this, Native.Z3_mk_fpa_to_fp_int_real(
this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
4529 #region Miscellaneous
4542 return AST.Create(
this, nativeObject);
4558 return a.NativeObject;
4567 return Native.Z3_simplify_get_help(nCtx);
4575 get {
return new ParamDescrs(
this, Native.Z3_simplify_get_param_descrs(nCtx)); }
4579 #region Error Handling
4607 Native.Z3_update_param_value(nCtx,
id, value);
4613 internal IntPtr m_ctx = IntPtr.Zero;
4614 internal Native.Z3_error_handler m_n_err_handler =
null;
4615 internal static Object creation_lock =
new Object();
4616 internal IntPtr nCtx {
get {
return m_ctx; } }
4618 internal void NativeErrorHandler(IntPtr ctx,
Z3_error_code errorCode)
4623 internal void InitContext()
4626 m_n_err_handler =
new Native.Z3_error_handler(NativeErrorHandler);
4627 Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
4628 GC.SuppressFinalize(
this);
4631 internal void CheckContextMatch(Z3Object other)
4633 Debug.Assert(other !=
null);
4635 if (!ReferenceEquals(
this, other.Context))
4636 throw new Z3Exception(
"Context mismatch");
4639 internal void CheckContextMatch(Z3Object other1, Z3Object other2)
4641 Debug.Assert(other1 !=
null);
4642 Debug.Assert(other2 !=
null);
4643 CheckContextMatch(other1);
4644 CheckContextMatch(other2);
4647 internal void CheckContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
4649 Debug.Assert(other1 !=
null);
4650 Debug.Assert(other2 !=
null);
4651 Debug.Assert(other3 !=
null);
4652 CheckContextMatch(other1);
4653 CheckContextMatch(other2);
4654 CheckContextMatch(other3);
4657 internal void CheckContextMatch(Z3Object[] arr)
4659 Debug.Assert(arr ==
null || arr.All(a => a !=
null));
4663 foreach (Z3Object a
in arr)
4665 Debug.Assert(a !=
null);
4666 CheckContextMatch(a);
4671 internal void CheckContextMatch<T>(IEnumerable<T> arr) where T : Z3Object
4673 Debug.Assert(arr ==
null || arr.All(a => a !=
null));
4677 foreach (Z3Object a
in arr)
4679 Debug.Assert(a !=
null);
4680 CheckContextMatch(a);
4685 private void ObjectInvariant()
4687 Debug.Assert(m_AST_DRQ !=
null);
4688 Debug.Assert(m_ASTMap_DRQ !=
null);
4689 Debug.Assert(m_ASTVector_DRQ !=
null);
4690 Debug.Assert(m_ApplyResult_DRQ !=
null);
4691 Debug.Assert(m_FuncEntry_DRQ !=
null);
4692 Debug.Assert(m_FuncInterp_DRQ !=
null);
4693 Debug.Assert(m_Goal_DRQ !=
null);
4694 Debug.Assert(m_Model_DRQ !=
null);
4695 Debug.Assert(m_Params_DRQ !=
null);
4696 Debug.Assert(m_ParamDescrs_DRQ !=
null);
4697 Debug.Assert(m_Probe_DRQ !=
null);
4698 Debug.Assert(m_Solver_DRQ !=
null);
4699 Debug.Assert(m_Statistics_DRQ !=
null);
4700 Debug.Assert(m_Tactic_DRQ !=
null);
4701 Debug.Assert(m_Fixedpoint_DRQ !=
null);
4702 Debug.Assert(m_Optimize_DRQ !=
null);
4705 readonly
private AST.DecRefQueue m_AST_DRQ =
new AST.DecRefQueue();
4706 readonly
private ASTMap.DecRefQueue m_ASTMap_DRQ =
new ASTMap.DecRefQueue(10);
4707 readonly
private ASTVector.DecRefQueue m_ASTVector_DRQ =
new ASTVector.DecRefQueue(10);
4708 readonly
private ApplyResult.DecRefQueue m_ApplyResult_DRQ =
new ApplyResult.DecRefQueue(10);
4709 readonly
private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ =
new FuncInterp.Entry.DecRefQueue(10);
4710 readonly
private FuncInterp.DecRefQueue m_FuncInterp_DRQ =
new FuncInterp.DecRefQueue(10);
4711 readonly
private Goal.DecRefQueue m_Goal_DRQ =
new Goal.DecRefQueue(10);
4712 readonly
private Model.DecRefQueue m_Model_DRQ =
new Model.DecRefQueue(10);
4713 readonly
private Params.DecRefQueue m_Params_DRQ =
new Params.DecRefQueue(10);
4714 readonly
private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ =
new ParamDescrs.DecRefQueue(10);
4715 readonly
private Probe.DecRefQueue m_Probe_DRQ =
new Probe.DecRefQueue(10);
4716 readonly
private Solver.DecRefQueue m_Solver_DRQ =
new Solver.DecRefQueue(10);
4717 readonly
private Statistics.DecRefQueue m_Statistics_DRQ =
new Statistics.DecRefQueue(10);
4718 readonly
private Tactic.DecRefQueue m_Tactic_DRQ =
new Tactic.DecRefQueue(10);
4719 readonly
private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ =
new Fixedpoint.DecRefQueue(10);
4720 readonly
private Optimize.DecRefQueue m_Optimize_DRQ =
new Optimize.DecRefQueue(10);
4802 internal long refCount = 0;
4839 m_stringSort =
null;
4840 if (refCount == 0 && m_ctx != IntPtr.Zero)
4842 m_n_err_handler =
null;
4844 m_ctx = IntPtr.Zero;
4845 Native.Z3_del_context(ctx);
4848 GC.ReRegisterForFinalize(
this);
The abstract syntax tree (AST) class.
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Arithmetic expressions (int/real)
Constructors are used for datatype sorts.
The main interaction with Z3 happens via the Context.
FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
Bitwise NAND.
FPNum MkFP(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
RealExpr MkInt2Real(IntExpr t)
Coerce an integer to a real.
FPSort MkFPSort16()
Create the half-precision (16-bit) FloatingPoint sort.
Expr MkNumeral(uint v, Sort ty)
Create a Term of a given sort. This function can be used to create numerals that fit in a machine int...
ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
Create an array constant.
BoolExpr MkAtLeast(IEnumerable< BoolExpr > args, uint k)
Create an at-least-k constraint.
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
Shift left.
IDecRefQueue ParamDescrs_DRQ
ParamDescrs DRQ
Tactic Skip()
Create a tactic that just returns the given goal.
Constructor MkConstructor(string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
Create a datatype constructor.
BoolSort BoolSort
Retrieves the Boolean sort of the context.
BitVecNum MkBV(bool[] bits)
Create a bit-vector numeral.
FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
Create a new finite domain sort. The result is a sort
BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2)
Check if the string s1 is lexicographically strictly less than s2.
FPSort MkFPSort(uint ebits, uint sbits)
Create a FloatingPoint sort.
Tactic With(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
string[] TacticNames
The names of all supported tactics.
FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point addition
BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Rotate Left.
RealExpr MkRealConst(string name)
Creates a real constant.
RatNum MkReal(uint v)
Create a real numeral.
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...
BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Logical shift right
FPRMSort MkFPRoundingModeSort()
Create the floating-point RoundingMode sort.
RealExpr MkFPToReal(FPExpr t)
Conversion of a floating-point term into a real-numbered term.
TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Create a new tuple sort.
Lambda MkLambda(Expr[] boundConstants, Expr body)
Create a lambda expression.
IDecRefQueue Params_DRQ
Params DRQ
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise multiplication does not underflow.
ArrayExpr MkFullSet(Sort domain)
Create the full set.
FPSort MkFPSortQuadruple()
Create the quadruple-precision (128-bit) FloatingPoint sort.
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
Probe ConstProbe(double val)
Create a probe that always evaluates to val .
Expr MkFreshConst(string prefix, Sort range)
Creates a fresh Constant of sort range and a name prefixed with prefix .
IntExpr MkReal2Int(RealExpr t)
Coerce a real to an integer.
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
FPSort MkFPSortHalf()
Create the half-precision (16-bit) FloatingPoint sort.
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.
ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Take the difference between two sets.
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Expr MkNumeral(long v, Sort ty)
Create a Term of a given sort. This function can be used to create numerals that fit in a machine int...
Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
Create an expression representing an if-then-else: ite(t1, t2, t3).
IntNum MkInt(uint v)
Create an integer numeral.
IntExpr MkIntConst(Symbol name)
Creates an integer constant.
AST WrapAST(IntPtr nativeObject)
Wraps an AST.
SeqExpr IntToString(Expr e)
Convert an integer expression to a string.
FPExpr MkFPMax(FPExpr t1, FPExpr t2)
Maximum of floating-point numbers.
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
BitVecExpr MkFPToIEEEBV(FPExpr t)
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
Create a datatype constructor.
IntSort IntSort
Retrieves the Integer sort of the context.
BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
Check for sequence suffix.
SeqExpr MkConcat(params SeqExpr[] t)
Concatenate sequences.
FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
Creates a new function declaration.
BoolExpr MkNot(BoolExpr a)
Mk an expression representing not(a).
FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
Creates a new function declaration.
Expr MkTermArray(ArrayExpr array)
Access the array default value.
BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
Signed remainder.
BitVecExpr MkBVRedOR(BitVecExpr t)
Take disjunction of bits in a vector, return vector of length 1.
Tactic MkTactic(string name)
Creates a new Tactic.
BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
Floating-point less than or equal.
ReExpr MkOption(ReExpr re)
Create the optional regular expression.
BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
Floating-point equality.
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
Extract subsequence.
RatNum MkReal(string v)
Create a real numeral.
FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
Create a new datatype sort.
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.
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
BoolExpr MkBVNegNoOverflow(BitVecExpr t)
Create a predicate that checks that the bit-wise negation does not overflow.
ListSort MkListSort(string name, Sort elemSort)
Create a new list sort.
uint NumTactics
The number of supported tactics.
ReExpr MkConcat(params ReExpr[] t)
Create the concatenation of regular languages.
BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than
BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise multiplication does not overflow.
FuncDecl MkConstDecl(Symbol name, Sort range)
Creates a new constant function declaration.
BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Signed division.
ParamDescrs SimplifyParameterDescriptions
Retrieves parameter descriptions for simplifier.
BitVecNum MkBV(ulong v, uint size)
Create a bit-vector numeral.
FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Floating-point fused multiply-add
BoolExpr MkFPIsInfinite(FPExpr t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.
BitVecExpr MkInt2BV(uint n, IntExpr t)
Create an n bit bit-vector from the integer argument t .
BoolExpr MkTrue()
The true Term.
FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point subtraction
FPNum MkFPNumeral(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
ReExpr MkUnion(params ReExpr[] t)
Create the union of regular languages.
RatNum MkReal(ulong v)
Create a real numeral.
BoolExpr MkBoolConst(Symbol name)
Create a Boolean constant.
IDecRefQueue Model_DRQ
Model DRQ
ReExpr MkEmptyRe(Sort s)
Create the empty regular expression. The sort s should be a regular expression.
Expr MkNth(SeqExpr s, Expr index)
Retrieve element at index.
FPSort MkFPSortSingle()
Create the single-precision (32-bit) FloatingPoint sort.
IntPtr UnwrapAST(AST a)
Unwraps an AST.
IntExpr MkMod(IntExpr t1, IntExpr t2)
Create an expression representing t1 mod t2.
BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean less-or-equal constraint.
IntNum MkInt(string v)
Create an integer numeral.
Expr MkConst(FuncDecl f)
Creates a fresh constant from the FuncDecl f .
FPRMNum MkFPRTZ()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
IDecRefQueue Optimize_DRQ
Optimize DRQ
Tactic TryFor(Tactic t, uint ms)
Create a tactic that applies t to a goal for ms milliseconds.
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 -> t2.
BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise subtraction does not underflow.
Expr MkSelect(ArrayExpr a, Expr i)
Array read.
ArrayExpr MkSetUnion(params ArrayExpr[] args)
Take the union of a list of sets.
IDecRefQueue ApplyResult_DRQ
ApplyResult DRQ
IDecRefQueue ASTVector_DRQ
ASTVector DRQ
IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Extract index of sub-string starting at offset.
BoolExpr MkBoolConst(string name)
Create a Boolean constant.
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
Two's complement signed remainder (sign follows divisor).
IDecRefQueue Goal_DRQ
Goal DRQ
Probe Or(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".
BitVecExpr MkRepeat(uint i, BitVecExpr t)
Bit-vector repetition.
FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
Creates a new function declaration.
BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
Floating-point greater than.
BoolExpr MkAtMost(IEnumerable< BoolExpr > args, uint k)
Create an at-most-k constraint.
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 ....
Solver MkSolver(string logic)
Creates a new (incremental) solver.
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.
ArrayExpr MkSetDel(ArrayExpr set, Expr element)
Remove an element from a set.
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....
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...
ReExpr MkRange(SeqExpr lo, SeqExpr hi)
Create a range expression.
BitVecNum MkBV(long v, uint size)
Create a bit-vector numeral.
BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater-than.
Params MkParams()
Creates a new ParameterSet.
ArrayExpr MkSetIntersection(params ArrayExpr[] args)
Take the intersection of a list of sets.
FPNum MkFPNaN(FPSort s)
Create a NaN of sort s.
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.
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.
BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise NOR.
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...
Fixedpoint MkFixedpoint()
Create a Fixedpoint context.
BoolExpr MkXor(IEnumerable< BoolExpr > ts)
Create an expression representing t1 xor t2 xor t3 ... .
void UpdateParamValue(string id, string value)
Update a mutable configuration parameter.
DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
Create a new datatype sort.
IDecRefQueue Statistics_DRQ
Statistics DRQ
void AddRecDef(FuncDecl f, Expr[] args, Expr body)
Bind a definition to a recursive function declaration. The function must have previously been created...
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
ArrayExpr MkConstArray(Sort domain, Expr v)
Create a constant array.
ArrayExpr MkSetComplement(ArrayExpr arg)
Take the complement of a set.
BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Check for subsetness of sets.
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...
FPRMNum MkFPRoundNearestTiesToAway()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
string[] ProbeNames
The names of all supported Probes.
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 .
BitVecExpr MkZeroExt(uint i, BitVecExpr t)
Bit-vector zero extension.
Z3_ast_print_mode PrintMode
Selects the format used for pretty-printing expressions.
IDecRefQueue FuncEntry_DRQ
FuncEntry DRQ
void Dispose()
Disposes of the context.
IDecRefQueue Solver_DRQ
Solver DRQ
ArrayExpr MkEmptySet(Sort domain)
Create an empty set.
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.
UninterpretedSort MkUninterpretedSort(string str)
Create a new uninterpreted sort.
IDecRefQueue FuncInterp_DRQ
FuncInterp DRQ
Expr MkNumeral(ulong v, Sort ty)
Create a Term of a given sort. This function can be used to create numerals that fit in a machine int...
ReExpr MkStar(ReExpr re)
Take the Kleene star of a regular expression.
BitVecExpr MkBVConst(string name, uint size)
Creates a bit-vector constant.
BitVecNum MkBV(uint v, uint size)
Create a bit-vector numeral.
Optimize MkOptimize()
Create an Optimization context.
IDecRefQueue AST_DRQ
AST DRQ
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.
Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned...
FPNum MkFPInf(FPSort s, bool negative)
Create a floating-point infinity of sort s.
FuncDecl MkConstDecl(string name, Sort range)
Creates a new constant function declaration.
ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
Maps f on the argument arrays.
ReExpr MkIntersect(params ReExpr[] t)
Create the intersection of regular languages.
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 MkBVSLE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than or equal to.
FPNum MkFP(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
IDecRefQueue Fixedpoint_DRQ
FixedPoint DRQ
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two integers.
ListSort MkListSort(Symbol name, Sort elemSort)
Create a new list sort.
SeqExpr MkAt(SeqExpr s, Expr index)
Retrieve sequence of length one at index.
FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Conversion of a floating-point number to another FloatingPoint sort s.
BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
Check for set membership.
BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Rotate Right.
SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
Replace the first occurrence of src by dst in s.
FPRMExpr MkFPRoundNearestTiesToEven()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
string ProbeDescription(string name)
Returns a string containing a description of the probe with the given name.
Pattern MkPattern(params Expr[] terms)
Create a quantifier pattern.
Probe And(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".
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...
FPExpr MkFPNeg(FPExpr t)
Floating-point negation
FPSort MkFPSort32()
Create the single-precision (32-bit) FloatingPoint sort.
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
RealSort RealSort
Retrieves the Real sort of the context.
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
BoolExpr MkIsInteger(RealExpr t)
Creates an expression that checks whether a real number is an integer.
BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XNOR.
BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than or equal to.
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
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.
BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise addition does not underflow.
BitVecNum MkBV(string v, uint size)
Create a bit-vector numeral.
ReExpr MkFullRe(Sort s)
Create the full regular expression. The sort s should be a regular expression.
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
BoolExpr MkFPIsSubnormal(FPExpr t)
Predicate indicating whether t is a subnormal floating-point number.
ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
Create an array constant.
BoolExpr MkFPIsZero(FPExpr t)
Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
ReSort MkReSort(SeqSort s)
Create a new regular expression sort.
FPSort MkFPSortDouble()
Create the double-precision (64-bit) FloatingPoint sort.
FPRMNum MkFPRoundTowardZero()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Goal MkGoal(bool models=true, bool unsatCores=false, bool proofs=false)
Creates a new Goal.
IntExpr MkBV2Int(BitVecExpr t, bool signed)
Create an integer from the bit-vector argument t .
ArithExpr MkAdd(params ArithExpr[] t)
Create an expression representing t[0] + t[1] + ....
BoolExpr MkInRe(SeqExpr s, ReExpr re)
Check for regular expression membership.
ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
Add an element to the set.
BitVecExpr MkBVRedAND(BitVecExpr t)
Take conjunction of bits in a vector, return vector of length 1.
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...
ReExpr MkLoop(ReExpr re, uint lo, uint hi=0)
Take the bounded Kleene star of a regular expression.
FPRMNum MkFPRoundTowardNegative()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Probe MkProbe(string name)
Creates a new Probe.
FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two integers.
SeqSort MkSeqSort(Sort s)
Create a new sequence sort.
DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
Create mutually recursive data-types.
Tactic FailIf(Probe p)
Create a tactic that fails if the probe p evaluates to false.
Expr MkBound(uint index, Sort ty)
Creates a new bound variable.
FPRMNum MkFPRTN()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed)
Conversion of a floating-point term into a bit-vector.
FPSort MkFPSort128()
Create the quadruple-precision (128-bit) FloatingPoint sort.
BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
Unsigned greater than or equal to.
Expr MkNumeral(int v, Sort ty)
Create a Term of a given sort. This function can be used to create numerals that fit in a machine int...
FPRMNum MkFPRTP()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
BoolSort MkBoolSort()
Create a new Boolean sort.
BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
Bit-vector concatenation.
ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 ^ t2.
SeqExpr MkEmptySeq(Sort s)
Create the empty sequence.
BitVecExpr MkBVNot(BitVecExpr t)
Bitwise negation.
FPExpr MkFPRem(FPExpr t1, FPExpr t2)
Floating-point remainder
RealSort MkRealSort()
Create a real sort.
BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise addition does not overflow.
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
Expr MkSelect(ArrayExpr a, params Expr[] args)
Array read.
FPNum MkFPNumeral(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
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.
BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
Floating-point less than.
BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
Floating-point greater than or equal.
BitVecExpr MkSignExt(uint i, BitVecExpr t)
Bit-vector sign extension.
Tactic ParOr(params Tactic[] t)
Create a tactic that applies the given tactics in parallel until one of them succeeds (i....
IntSort MkIntSort()
Create a new integer sort.
BoolExpr MkAnd(IEnumerable< BoolExpr > t)
Create an expression representing t[0] and t[1] and ....
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
Two's complement multiplication.
IntExpr StringToInt(Expr e)
Convert an integer expression to a string.
BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise signed division does not overflow.
BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
Check for sequence containment of s2 in s1.
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...
SeqSort StringSort
Retrieves the String sort of the context.
BoolExpr MkEq(Expr x, Expr y)
Creates the equality x = y .
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.
BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
Two's complement subtraction.
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Unsigned division.
void Interrupt()
Interrupt the execution of a Z3 procedure.
BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
Unsigned greater-than.
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
BitVecExpr MkBVConst(Symbol name, uint size)
Creates a bit-vector constant.
BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
Arithmetic shift right
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 .
FPNum MkFPZero(FPSort s, bool negative)
Create a floating-point zero of sort s.
BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean greater-or-equal constraint.
IntNum MkInt(long v)
Create an integer numeral.
RatNum MkReal(long v)
Create a real numeral.
ReExpr MkPlus(ReExpr re)
Take the Kleene plus of a regular expression.
FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
Floating-point square root
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 iff t2.
FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
Create a new finite domain sort. The result is a sortElements of the sort are created using MkNumeral...
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
ArithExpr MkAdd(IEnumerable< ArithExpr > t)
Create an expression representing t[0] + t[1] + ....
FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
Creates a new recursive function declaration.
BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
Two's complement addition.
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
Solver MkSimpleSolver()
Creates a new (incremental) solver.
ArraySort MkArraySort(Sort[] domain, Sort range)
Create a new n-ary array sort.
Probe Not(Probe p)
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
BoolExpr MkBool(bool value)
Creates a Boolean value.
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
Bitwise conjunction.
Solver MkSolver(Tactic t)
Creates a solver that is implemented using the given tactic.
RealExpr MkRealConst(Symbol name)
Creates a real constant.
IntNum MkInt(ulong v)
Create an integer numeral.
Expr MkApp(FuncDecl f, IEnumerable< Expr > args)
Create a new function application.
ReExpr MkToRe(SeqExpr s)
Convert a regular expression that accepts sequence s.
BoolExpr MkFPIsNaN(FPExpr t)
Predicate indicating whether t is a NaN.
BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
Rotate Right.
string SimplifyHelp()
Return a string describing all available parameters to Expr.Simplify.
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.
Lambda MkLambda(Sort[] sorts, Symbol[] names, Expr body)
Create a lambda expression.
FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
Creates a new function declaration.
BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than
IDecRefQueue Tactic_DRQ
Tactic DRQ
SetSort MkSetSort(Sort ty)
Create a set type.
EnumSort MkEnumSort(string name, params string[] enumNames)
Create a new enumeration sort.
BitVecNum MkBV(int v, uint size)
Create a bit-vector numeral.
RatNum MkReal(int num, int den)
Create a real from a fraction.
IDecRefQueue Probe_DRQ
Probe DRQ
EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
Create a new enumeration sort.
BoolExpr MkFPIsNegative(FPExpr t)
Predicate indicating whether t is a negative floating-point number.
FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
Creates a fresh function declaration with a name prefixed with prefix .
IntExpr MkIntConst(string name)
Creates an integer constant.
Tactic When(Probe p, Tactic t)
Create a tactic that applies t to a given goal if the probe p evaluates to true.
BitVecExpr MkBVNeg(BitVecExpr t)
Standard two's complement unary minus.
FuncDecl MkFreshConstDecl(string prefix, Sort range)
Creates a fresh constant function declaration with a name prefixed with prefix .
Tactic Fail()
Create a tactic always fails.
Tactic FailIfNotDecided()
Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsati...
FPRMNum MkFPRoundTowardPositive()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
Bitwise disjunction.
Expr MkConst(string name, Sort range)
Creates a new Constant of sort range and named name .
IntExpr MkRem(IntExpr t1, IntExpr t2)
Create an expression representing t1 rem t2.
FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point multiplication
BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
Check if the string s1 is lexicographically strictly less than s2.
BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise subtraction does not overflow.
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...
FPSort MkFPSort64()
Create the double-precision (64-bit) FloatingPoint sort.
FPRMNum MkFPRNA()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Context(Dictionary< string, string > settings)
Constructor.
BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
Rotate Left.
string TacticDescription(string name)
Returns a string containing a description of the tactic with the given name.
FPRMNum MkFPRNE()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
IDecRefQueue ASTMap_DRQ
ASTMap DRQ
SeqExpr MkUnit(Expr elem)
Create the singleton sequence.
uint NumProbes
The number of supported Probes.
BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean equal constraint.
IntNum MkInt(int v)
Create an integer numeral.
BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XOR.
ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
Array update.
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
FPExpr MkFPAbs(FPExpr t)
Floating-point absolute value
FPExpr MkFPMin(FPExpr t1, FPExpr t2)
Minimum of floating-point numbers.
FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point division
BoolExpr MkOr(IEnumerable< BoolExpr > t)
Create an expression representing t[0] or t[1] or ....
ReExpr MkComplement(ReExpr re)
Create the complement regular expression.
BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
Bit-vector extraction.
ArithExpr MkMul(IEnumerable< ArithExpr > t)
Create an expression representing t[0] * t[1] * ....
StringSymbol MkSymbol(string name)
Create a symbol using a string.
BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
Unsigned remainder.
BoolExpr MkFalse()
The false Term.
IntExpr MkLength(SeqExpr s)
Retrieve the length of a given sequence.
RatNum MkReal(int v)
Create a real numeral.
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
SeqExpr MkString(string s)
Create a string constant.
ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
Array update.
FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
Create an expression of FloatingPoint sort from three bit-vector expressions.
BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater than or equal to.
Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create a universal Quantifier.
FPNum MkFP(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
BoolExpr MkFPIsNormal(FPExpr t)
Predicate indicating whether t is a normal floating-point number.
BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
Check for sequence prefix.
BoolExpr MkFPIsPositive(FPExpr t)
Predicate indicating whether t is a positive floating-point number.
FloatingPoint Expressions
FloatingPoint RoundingMode Expressions
Floating-point rounding mode numerals
The FloatingPoint RoundingMode sort
Object for managing fixedpoints
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Object for managing optimization context
A ParamDescrs describes a set of parameters.
A Params objects represents a configuration in the form of Symbol/value pairs.
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
Regular expression expressions
A regular expression sort
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
The Sort class implements type information for ASTs.
Symbols are used to name several term and type constructors.
Tactics are the basic building block for creating custom solvers for specific problem domains....
The exception base class for error reporting from Z3
expr range(expr const &lo, expr const &hi)
expr max(expr const &a, expr const &b)
def EnumSort(name, values, ctx=None)
def FiniteDomainSort(name, sz, ctx=None)
def FPSort(ebits, sbits, ctx=None)
def TupleSort(name, sorts, ctx=None)
def BitVecSort(sz, ctx=None)
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Z3_error_code
Z3 error codes (See Z3_get_error_code).