21 using System.Collections.Generic;
22 using System.Runtime.InteropServices;
43 m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
66 public Context(Dictionary<string, string> settings)
69 Contract.Requires(settings != null);
73 IntPtr cfg = Native.Z3_mk_config();
74 foreach (KeyValuePair<string, string> kv
in settings)
75 Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
76 m_ctx = Native.Z3_mk_context_rc(cfg);
77 Native.Z3_del_config(cfg);
93 Contract.Ensures(Contract.Result<
IntSymbol>() != null);
103 Contract.Ensures(Contract.Result<
StringSymbol>() != null);
111 internal Symbol[] MkSymbols(
string[] names)
113 Contract.Ensures(names == null || Contract.Result<
Symbol[]>() != null);
114 Contract.Ensures(names != null || Contract.Result<
Symbol[]>() == null);
115 Contract.Ensures(Contract.Result<
Symbol[]>() == null || Contract.Result<
Symbol[]>().Length == names.Length);
116 Contract.Ensures(Contract.Result<
Symbol[]>() == null || Contract.ForAll(Contract.Result<
Symbol[]>(), s => s != null));
118 if (names == null)
return null;
120 for (
int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
127 private IntSort m_intSort = null;
129 private SeqSort m_stringSort = null;
138 Contract.Ensures(Contract.Result<
BoolSort>() != null);
139 if (m_boolSort == null) m_boolSort =
new BoolSort(
this);
return m_boolSort;
150 Contract.Ensures(Contract.Result<
IntSort>() != null);
151 if (m_intSort == null) m_intSort =
new IntSort(
this);
return m_intSort;
163 Contract.Ensures(Contract.Result<
RealSort>() != null);
164 if (m_realSort == null) m_realSort =
new RealSort(
this);
return m_realSort;
175 Contract.Ensures(Contract.Result<
SeqSort>() != null);
176 if (m_stringSort == null) m_stringSort =
new SeqSort(
this, Native.Z3_mk_string_sort(nCtx));
187 Contract.Ensures(Contract.Result<
BoolSort>() != null);
196 Contract.Requires(s != null);
199 CheckContextMatch(s);
210 return MkUninterpretedSort(MkSymbol(str));
218 Contract.Ensures(Contract.Result<
IntSort>() != null);
228 Contract.Ensures(Contract.Result<
RealSort>() != null);
237 Contract.Ensures(Contract.Result<
BitVecSort>() != null);
239 return new BitVecSort(
this, Native.Z3_mk_bv_sort(nCtx, size));
248 Contract.Requires(s != null);
249 Contract.Ensures(Contract.Result<
SeqSort>() != null);
250 return new SeqSort(
this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
258 Contract.Requires(s != null);
259 Contract.Ensures(Contract.Result<
ReSort>() != null);
260 return new ReSort(
this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
268 Contract.Requires(domain != null);
269 Contract.Requires(range != null);
270 Contract.Ensures(Contract.Result<
ArraySort>() != null);
272 CheckContextMatch(domain);
273 CheckContextMatch(range);
274 return new ArraySort(
this, domain, range);
282 Contract.Requires(name != null);
283 Contract.Requires(fieldNames != null);
284 Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
285 Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
286 Contract.Ensures(Contract.Result<
TupleSort>() != null);
288 CheckContextMatch(name);
289 CheckContextMatch<Symbol>(fieldNames);
290 CheckContextMatch<Sort>(fieldSorts);
291 return new TupleSort(
this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
299 Contract.Requires(name != null);
300 Contract.Requires(enumNames != null);
301 Contract.Requires(Contract.ForAll(enumNames, f => f != null));
303 Contract.Ensures(Contract.Result<
EnumSort>() != null);
305 CheckContextMatch(name);
306 CheckContextMatch<Symbol>(enumNames);
307 return new EnumSort(
this, name, enumNames);
315 Contract.Requires(enumNames != null);
316 Contract.Ensures(Contract.Result<
EnumSort>() != null);
318 return new EnumSort(
this, MkSymbol(name), MkSymbols(enumNames));
326 Contract.Requires(name != null);
327 Contract.Requires(elemSort != null);
328 Contract.Ensures(Contract.Result<
ListSort>() != null);
330 CheckContextMatch(name);
331 CheckContextMatch(elemSort);
332 return new ListSort(
this, name, elemSort);
340 Contract.Requires(elemSort != null);
341 Contract.Ensures(Contract.Result<
ListSort>() != null);
343 CheckContextMatch(elemSort);
344 return new ListSort(
this, MkSymbol(name), elemSort);
355 Contract.Requires(name != null);
358 CheckContextMatch(name);
391 Contract.Requires(name != null);
392 Contract.Requires(recognizer != null);
393 Contract.Ensures(Contract.Result<
Constructor>() != null);
395 return new Constructor(
this, name, recognizer, fieldNames, sorts, sortRefs);
409 Contract.Ensures(Contract.Result<
Constructor>() != null);
411 return new Constructor(
this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
419 Contract.Requires(name != null);
420 Contract.Requires(constructors != null);
421 Contract.Requires(Contract.ForAll(constructors, c => c != null));
423 Contract.Ensures(Contract.Result<
DatatypeSort>() != null);
425 CheckContextMatch(name);
426 CheckContextMatch<Constructor>(constructors);
435 Contract.Requires(constructors != null);
436 Contract.Requires(Contract.ForAll(constructors, c => c != null));
437 Contract.Ensures(Contract.Result<
DatatypeSort>() != null);
439 CheckContextMatch<Constructor>(constructors);
440 return new DatatypeSort(
this, MkSymbol(name), constructors);
450 Contract.Requires(names != null);
451 Contract.Requires(c != null);
452 Contract.Requires(names.Length == c.Length);
453 Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
454 Contract.Requires(Contract.ForAll(names, name => name != null));
455 Contract.Ensures(Contract.Result<
DatatypeSort[]>() != null);
457 CheckContextMatch<Symbol>(names);
458 uint n = (uint)names.Length;
460 IntPtr[] n_constr =
new IntPtr[n];
461 for (uint i = 0; i < n; i++)
464 Contract.Assume(Contract.ForAll(constructor, arr => arr != null),
"Clousot does not support yet quantified formula on multidimensional arrays");
465 CheckContextMatch<Constructor>(constructor);
467 n_constr[i] = cla[i].NativeObject;
469 IntPtr[] n_res =
new IntPtr[n];
470 Native.Z3_mk_datatypes(nCtx, n,
Symbol.ArrayToNative(names), n_res, n_constr);
472 for (uint i = 0; i < n; i++)
485 Contract.Requires(names != null);
486 Contract.Requires(c != null);
487 Contract.Requires(names.Length == c.Length);
488 Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
489 Contract.Requires(Contract.ForAll(names, name => name != null));
490 Contract.Ensures(Contract.Result<
DatatypeSort[]>() != null);
492 return MkDatatypeSorts(MkSymbols(names), c);
503 return Expr.Create(
this, Native.Z3_datatype_update_field(
504 nCtx, field.NativeObject,
505 t.NativeObject, v.NativeObject));
511 #region Function Declarations 517 Contract.Requires(name != null);
518 Contract.Requires(range != null);
519 Contract.Requires(Contract.ForAll(domain, d => d != null));
520 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
522 CheckContextMatch(name);
523 CheckContextMatch<Sort>(domain);
524 CheckContextMatch(range);
525 return new FuncDecl(
this, name, domain, range);
533 Contract.Requires(name != null);
534 Contract.Requires(domain != null);
535 Contract.Requires(range != null);
536 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
538 CheckContextMatch(name);
539 CheckContextMatch(domain);
540 CheckContextMatch(range);
542 return new FuncDecl(
this, name, q, range);
550 Contract.Requires(range != null);
551 Contract.Requires(Contract.ForAll(domain, d => d != null));
552 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
554 CheckContextMatch<Sort>(domain);
555 CheckContextMatch(range);
556 return new FuncDecl(
this, MkSymbol(name), domain, range);
564 Contract.Requires(range != null);
565 Contract.Requires(domain != null);
566 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
568 CheckContextMatch(domain);
569 CheckContextMatch(range);
571 return new FuncDecl(
this, MkSymbol(name), q, range);
581 Contract.Requires(range != null);
582 Contract.Requires(Contract.ForAll(domain, d => d != null));
583 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
585 CheckContextMatch<Sort>(domain);
586 CheckContextMatch(range);
587 return new FuncDecl(
this, prefix, domain, range);
595 Contract.Requires(name != null);
596 Contract.Requires(range != null);
597 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
599 CheckContextMatch(name);
600 CheckContextMatch(range);
601 return new FuncDecl(
this, name, null, range);
609 Contract.Requires(range != null);
610 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
612 CheckContextMatch(range);
613 return new FuncDecl(
this, MkSymbol(name), null, range);
623 Contract.Requires(range != null);
624 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
626 CheckContextMatch(range);
627 return new FuncDecl(
this, prefix, null, range);
631 #region Bound Variables 632 public Expr MkBound(uint index,
Sort ty)
639 Contract.Requires(ty != null);
640 Contract.Ensures(Contract.Result<
Expr>() != null);
642 return Expr.Create(
this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
646 #region Quantifier Patterns 652 Contract.Requires(terms != null);
653 if (terms.Length == 0)
654 throw new Z3Exception(
"Cannot create a pattern from zero terms");
656 Contract.Ensures(Contract.Result<
Pattern>() != null);
658 Contract.EndContractBlock();
660 IntPtr[] termsNative =
AST.ArrayToNative(terms);
661 return new Pattern(
this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
671 Contract.Requires(name != null);
672 Contract.Requires(range != null);
673 Contract.Ensures(Contract.Result<
Expr>() != null);
675 CheckContextMatch(name);
676 CheckContextMatch(range);
678 return Expr.Create(
this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
686 Contract.Requires(range != null);
687 Contract.Ensures(Contract.Result<
Expr>() != null);
689 return MkConst(MkSymbol(name), range);
698 Contract.Requires(range != null);
699 Contract.Ensures(Contract.Result<
Expr>() != null);
701 CheckContextMatch(range);
702 return Expr.Create(
this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
711 Contract.Requires(f != null);
712 Contract.Ensures(Contract.Result<
Expr>() != null);
722 Contract.Requires(name != null);
723 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
733 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
743 Contract.Requires(name != null);
744 Contract.Ensures(Contract.Result<
IntExpr>() != null);
754 Contract.Requires(name != null);
755 Contract.Ensures(Contract.Result<
IntExpr>() != null);
765 Contract.Requires(name != null);
766 Contract.Ensures(Contract.Result<
RealExpr>() != null);
776 Contract.Ensures(Contract.Result<
RealExpr>() != null);
786 Contract.Requires(name != null);
787 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
789 return (
BitVecExpr)MkConst(name, MkBitVecSort(size));
797 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
799 return (
BitVecExpr)MkConst(name, MkBitVecSort(size));
809 Contract.Requires(f != null);
810 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
811 Contract.Ensures(Contract.Result<
Expr>() != null);
813 CheckContextMatch(f);
814 CheckContextMatch<Expr>(args);
815 return Expr.Create(
this, f, args);
823 Contract.Requires(f != null);
824 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
825 Contract.Ensures(Contract.Result<
Expr>() != null);
827 CheckContextMatch(f);
828 CheckContextMatch(args);
829 return Expr.Create(
this, f, args.ToArray());
832 #region Propositional 838 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
840 return new BoolExpr(
this, Native.Z3_mk_true(nCtx));
848 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
850 return new BoolExpr(
this, Native.Z3_mk_false(nCtx));
858 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
860 return value ? MkTrue() : MkFalse();
868 Contract.Requires(x != null);
869 Contract.Requires(y != null);
870 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
872 CheckContextMatch(x);
873 CheckContextMatch(y);
874 return new BoolExpr(
this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
882 Contract.Requires(args != null);
883 Contract.Requires(Contract.ForAll(args, a => a != null));
885 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
887 CheckContextMatch<Expr>(args);
888 return new BoolExpr(
this, Native.Z3_mk_distinct(nCtx, (uint)args.Length,
AST.ArrayToNative(args)));
896 Contract.Requires(a != null);
897 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
899 CheckContextMatch(a);
900 return new BoolExpr(
this, Native.Z3_mk_not(nCtx, a.NativeObject));
911 Contract.Requires(t1 != null);
912 Contract.Requires(t2 != null);
913 Contract.Requires(t3 != null);
914 Contract.Ensures(Contract.Result<
Expr>() != null);
916 CheckContextMatch(t1);
917 CheckContextMatch(t2);
918 CheckContextMatch(t3);
919 return Expr.Create(
this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
927 Contract.Requires(t1 != null);
928 Contract.Requires(t2 != null);
929 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
931 CheckContextMatch(t1);
932 CheckContextMatch(t2);
933 return new BoolExpr(
this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
941 Contract.Requires(t1 != null);
942 Contract.Requires(t2 != null);
943 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
945 CheckContextMatch(t1);
946 CheckContextMatch(t2);
947 return new BoolExpr(
this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
955 Contract.Requires(t1 != null);
956 Contract.Requires(t2 != null);
957 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
959 CheckContextMatch(t1);
960 CheckContextMatch(t2);
961 return new BoolExpr(
this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
969 Contract.Requires(t != null);
970 Contract.Requires(Contract.ForAll(t, a => a != null));
971 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
973 CheckContextMatch<BoolExpr>(t);
974 return new BoolExpr(
this, Native.Z3_mk_and(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
982 Contract.Requires(t != null);
983 Contract.Requires(Contract.ForAll(t, a => a != null));
984 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
985 CheckContextMatch<BoolExpr>(t);
986 return new BoolExpr(
this, Native.Z3_mk_and(nCtx, (uint)t.Count(),
AST.EnumToNative(t)));
994 Contract.Requires(t != null);
995 Contract.Requires(Contract.ForAll(t, a => a != null));
996 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
998 CheckContextMatch<BoolExpr>(t);
999 return new BoolExpr(
this, Native.Z3_mk_or(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
1008 Contract.Requires(t != null);
1009 Contract.Requires(Contract.ForAll(t, a => a != null));
1010 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1012 CheckContextMatch(t);
1013 return new BoolExpr(
this, Native.Z3_mk_or(nCtx, (uint)t.Count(),
AST.EnumToNative(t)));
1024 Contract.Requires(t != null);
1025 Contract.Requires(Contract.ForAll(t, a => a != null));
1026 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
1028 CheckContextMatch<ArithExpr>(t);
1029 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_add(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
1037 Contract.Requires(t != null);
1038 Contract.Requires(Contract.ForAll(t, a => a != null));
1039 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
1041 CheckContextMatch(t);
1042 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_add(nCtx, (uint)t.Count(),
AST.EnumToNative(t)));
1050 Contract.Requires(t != null);
1051 Contract.Requires(Contract.ForAll(t, a => a != null));
1052 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
1054 CheckContextMatch<ArithExpr>(t);
1055 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_mul(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
1063 Contract.Requires(t != null);
1064 Contract.Requires(Contract.ForAll(t, a => a != null));
1065 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
1067 CheckContextMatch<ArithExpr>(t);
1068 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_mul(nCtx, (uint)t.Count(),
AST.EnumToNative(t)));
1076 Contract.Requires(t != null);
1077 Contract.Requires(Contract.ForAll(t, a => a != null));
1078 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
1080 CheckContextMatch<ArithExpr>(t);
1081 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_sub(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
1089 Contract.Requires(t != null);
1090 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
1092 CheckContextMatch(t);
1093 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
1101 Contract.Requires(t1 != null);
1102 Contract.Requires(t2 != null);
1103 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
1105 CheckContextMatch(t1);
1106 CheckContextMatch(t2);
1107 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1116 Contract.Requires(t1 != null);
1117 Contract.Requires(t2 != null);
1118 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1120 CheckContextMatch(t1);
1121 CheckContextMatch(t2);
1122 return new IntExpr(
this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1131 Contract.Requires(t1 != null);
1132 Contract.Requires(t2 != null);
1133 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1135 CheckContextMatch(t1);
1136 CheckContextMatch(t2);
1137 return new IntExpr(
this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1145 Contract.Requires(t1 != null);
1146 Contract.Requires(t2 != null);
1147 Contract.Ensures(Contract.Result<
ArithExpr>() != null);
1149 CheckContextMatch(t1);
1150 CheckContextMatch(t2);
1151 return (
ArithExpr)
Expr.Create(
this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1159 Contract.Requires(t1 != null);
1160 Contract.Requires(t2 != null);
1161 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1163 CheckContextMatch(t1);
1164 CheckContextMatch(t2);
1165 return new BoolExpr(
this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1173 Contract.Requires(t1 != null);
1174 Contract.Requires(t2 != null);
1175 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1177 CheckContextMatch(t1);
1178 CheckContextMatch(t2);
1179 return new BoolExpr(
this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1187 Contract.Requires(t1 != null);
1188 Contract.Requires(t2 != null);
1189 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1191 CheckContextMatch(t1);
1192 CheckContextMatch(t2);
1193 return new BoolExpr(
this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1201 Contract.Requires(t1 != null);
1202 Contract.Requires(t2 != null);
1203 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1205 CheckContextMatch(t1);
1206 CheckContextMatch(t2);
1207 return new BoolExpr(
this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1222 Contract.Requires(t != null);
1223 Contract.Ensures(Contract.Result<
RealExpr>() != null);
1225 CheckContextMatch(t);
1226 return new RealExpr(
this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1238 Contract.Requires(t != null);
1239 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1241 CheckContextMatch(t);
1242 return new IntExpr(
this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1250 Contract.Requires(t != null);
1251 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1253 CheckContextMatch(t);
1254 return new BoolExpr(
this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1265 Contract.Requires(t != null);
1266 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1268 CheckContextMatch(t);
1269 return new BitVecExpr(
this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1278 Contract.Requires(t != null);
1279 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1281 CheckContextMatch(t);
1282 return new BitVecExpr(
this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1291 Contract.Requires(t != null);
1292 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1294 CheckContextMatch(t);
1295 return new BitVecExpr(
this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1304 Contract.Requires(t1 != null);
1305 Contract.Requires(t2 != null);
1306 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1308 CheckContextMatch(t1);
1309 CheckContextMatch(t2);
1310 return new BitVecExpr(
this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1319 Contract.Requires(t1 != null);
1320 Contract.Requires(t2 != null);
1321 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1323 CheckContextMatch(t1);
1324 CheckContextMatch(t2);
1325 return new BitVecExpr(
this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1334 Contract.Requires(t1 != null);
1335 Contract.Requires(t2 != null);
1336 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1338 CheckContextMatch(t1);
1339 CheckContextMatch(t2);
1340 return new BitVecExpr(
this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1349 Contract.Requires(t1 != null);
1350 Contract.Requires(t2 != null);
1351 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1353 CheckContextMatch(t1);
1354 CheckContextMatch(t2);
1355 return new BitVecExpr(
this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1364 Contract.Requires(t1 != null);
1365 Contract.Requires(t2 != null);
1366 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1368 CheckContextMatch(t1);
1369 CheckContextMatch(t2);
1370 return new BitVecExpr(
this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1379 Contract.Requires(t1 != null);
1380 Contract.Requires(t2 != null);
1381 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1383 CheckContextMatch(t1);
1384 CheckContextMatch(t2);
1385 return new BitVecExpr(
this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1394 Contract.Requires(t != null);
1395 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1397 CheckContextMatch(t);
1398 return new BitVecExpr(
this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1407 Contract.Requires(t1 != null);
1408 Contract.Requires(t2 != null);
1409 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1411 CheckContextMatch(t1);
1412 CheckContextMatch(t2);
1413 return new BitVecExpr(
this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1422 Contract.Requires(t1 != null);
1423 Contract.Requires(t2 != null);
1424 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1426 CheckContextMatch(t1);
1427 CheckContextMatch(t2);
1428 return new BitVecExpr(
this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1437 Contract.Requires(t1 != null);
1438 Contract.Requires(t2 != null);
1439 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1441 CheckContextMatch(t1);
1442 CheckContextMatch(t2);
1443 return new BitVecExpr(
this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1457 Contract.Requires(t1 != null);
1458 Contract.Requires(t2 != null);
1459 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1461 CheckContextMatch(t1);
1462 CheckContextMatch(t2);
1463 return new BitVecExpr(
this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1481 Contract.Requires(t1 != null);
1482 Contract.Requires(t2 != null);
1483 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1485 CheckContextMatch(t1);
1486 CheckContextMatch(t2);
1487 return new BitVecExpr(
this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1500 Contract.Requires(t1 != null);
1501 Contract.Requires(t2 != null);
1502 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1504 CheckContextMatch(t1);
1505 CheckContextMatch(t2);
1506 return new BitVecExpr(
this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1521 Contract.Requires(t1 != null);
1522 Contract.Requires(t2 != null);
1523 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1525 CheckContextMatch(t1);
1526 CheckContextMatch(t2);
1527 return new BitVecExpr(
this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1539 Contract.Requires(t1 != null);
1540 Contract.Requires(t2 != null);
1541 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1543 CheckContextMatch(t1);
1544 CheckContextMatch(t2);
1545 return new BitVecExpr(
this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1556 Contract.Requires(t1 != null);
1557 Contract.Requires(t2 != null);
1558 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1560 CheckContextMatch(t1);
1561 CheckContextMatch(t2);
1562 return new BoolExpr(
this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1573 Contract.Requires(t1 != null);
1574 Contract.Requires(t2 != null);
1575 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1577 CheckContextMatch(t1);
1578 CheckContextMatch(t2);
1579 return new BoolExpr(
this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1590 Contract.Requires(t1 != null);
1591 Contract.Requires(t2 != null);
1592 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1594 CheckContextMatch(t1);
1595 CheckContextMatch(t2);
1596 return new BoolExpr(
this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1607 Contract.Requires(t1 != null);
1608 Contract.Requires(t2 != null);
1609 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1611 CheckContextMatch(t1);
1612 CheckContextMatch(t2);
1613 return new BoolExpr(
this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1624 Contract.Requires(t1 != null);
1625 Contract.Requires(t2 != null);
1626 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1628 CheckContextMatch(t1);
1629 CheckContextMatch(t2);
1630 return new BoolExpr(
this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1641 Contract.Requires(t1 != null);
1642 Contract.Requires(t2 != null);
1643 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1645 CheckContextMatch(t1);
1646 CheckContextMatch(t2);
1647 return new BoolExpr(
this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1658 Contract.Requires(t1 != null);
1659 Contract.Requires(t2 != null);
1660 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1662 CheckContextMatch(t1);
1663 CheckContextMatch(t2);
1664 return new BoolExpr(
this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1675 Contract.Requires(t1 != null);
1676 Contract.Requires(t2 != null);
1677 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1679 CheckContextMatch(t1);
1680 CheckContextMatch(t2);
1681 return new BoolExpr(
this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1696 Contract.Requires(t1 != null);
1697 Contract.Requires(t2 != null);
1698 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1700 CheckContextMatch(t1);
1701 CheckContextMatch(t2);
1702 return new BitVecExpr(
this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1716 Contract.Requires(t != null);
1717 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1719 CheckContextMatch(t);
1720 return new BitVecExpr(
this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1733 Contract.Requires(t != null);
1734 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1736 CheckContextMatch(t);
1737 return new BitVecExpr(
this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1751 Contract.Requires(t != null);
1752 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1754 CheckContextMatch(t);
1755 return new BitVecExpr(
this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1766 Contract.Requires(t != null);
1767 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1769 CheckContextMatch(t);
1770 return new BitVecExpr(
this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1787 Contract.Requires(t1 != null);
1788 Contract.Requires(t2 != null);
1789 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1791 CheckContextMatch(t1);
1792 CheckContextMatch(t2);
1793 return new BitVecExpr(
this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1810 Contract.Requires(t1 != null);
1811 Contract.Requires(t2 != null);
1812 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1814 CheckContextMatch(t1);
1815 CheckContextMatch(t2);
1816 return new BitVecExpr(
this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1835 Contract.Requires(t1 != null);
1836 Contract.Requires(t2 != null);
1837 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1839 CheckContextMatch(t1);
1840 CheckContextMatch(t2);
1841 return new BitVecExpr(
this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1853 Contract.Requires(t != null);
1854 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1856 CheckContextMatch(t);
1857 return new BitVecExpr(
this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1869 Contract.Requires(t != null);
1870 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1872 CheckContextMatch(t);
1873 return new BitVecExpr(
this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1885 Contract.Requires(t1 != null);
1886 Contract.Requires(t2 != null);
1887 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1889 CheckContextMatch(t1);
1890 CheckContextMatch(t2);
1891 return new BitVecExpr(
this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1903 Contract.Requires(t1 != null);
1904 Contract.Requires(t2 != null);
1905 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1907 CheckContextMatch(t1);
1908 CheckContextMatch(t2);
1909 return new BitVecExpr(
this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1924 Contract.Requires(t != null);
1925 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
1927 CheckContextMatch(t);
1928 return new BitVecExpr(
this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1948 Contract.Requires(t != null);
1949 Contract.Ensures(Contract.Result<
IntExpr>() != null);
1951 CheckContextMatch(t);
1952 return new IntExpr(
this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (
signed) ? 1 : 0));
1963 Contract.Requires(t1 != null);
1964 Contract.Requires(t2 != null);
1965 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1967 CheckContextMatch(t1);
1968 CheckContextMatch(t2);
1969 return new BoolExpr(
this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1980 Contract.Requires(t1 != null);
1981 Contract.Requires(t2 != null);
1982 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
1984 CheckContextMatch(t1);
1985 CheckContextMatch(t2);
1986 return new BoolExpr(
this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1997 Contract.Requires(t1 != null);
1998 Contract.Requires(t2 != null);
1999 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2001 CheckContextMatch(t1);
2002 CheckContextMatch(t2);
2003 return new BoolExpr(
this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2014 Contract.Requires(t1 != null);
2015 Contract.Requires(t2 != null);
2016 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2018 CheckContextMatch(t1);
2019 CheckContextMatch(t2);
2020 return new BoolExpr(
this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
2031 Contract.Requires(t1 != null);
2032 Contract.Requires(t2 != null);
2033 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2035 CheckContextMatch(t1);
2036 CheckContextMatch(t2);
2037 return new BoolExpr(
this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2048 Contract.Requires(t != null);
2049 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2051 CheckContextMatch(t);
2052 return new BoolExpr(
this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
2063 Contract.Requires(t1 != null);
2064 Contract.Requires(t2 != null);
2065 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2067 CheckContextMatch(t1);
2068 CheckContextMatch(t2);
2069 return new BoolExpr(
this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
2080 Contract.Requires(t1 != null);
2081 Contract.Requires(t2 != null);
2082 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2084 CheckContextMatch(t1);
2085 CheckContextMatch(t2);
2086 return new BoolExpr(
this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2096 Contract.Requires(name != null);
2097 Contract.Requires(domain != null);
2098 Contract.Requires(range != null);
2099 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2101 return (
ArrayExpr)MkConst(name, MkArraySort(domain, range));
2109 Contract.Requires(domain != null);
2110 Contract.Requires(range != null);
2111 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2113 return (
ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
2131 Contract.Requires(a != null);
2132 Contract.Requires(i != null);
2133 Contract.Ensures(Contract.Result<
Expr>() != null);
2135 CheckContextMatch(a);
2136 CheckContextMatch(i);
2137 return Expr.Create(
this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2159 Contract.Requires(a != null);
2160 Contract.Requires(i != null);
2161 Contract.Requires(v != null);
2162 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2164 CheckContextMatch(a);
2165 CheckContextMatch(i);
2166 CheckContextMatch(v);
2167 return new ArrayExpr(
this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2181 Contract.Requires(domain != null);
2182 Contract.Requires(v != null);
2183 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2185 CheckContextMatch(domain);
2186 CheckContextMatch(v);
2187 return new ArrayExpr(
this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2203 Contract.Requires(f != null);
2204 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2205 Contract.Ensures(Contract.Result<
ArrayExpr>() != null);
2207 CheckContextMatch(f);
2208 CheckContextMatch<ArrayExpr>(args);
2209 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_map(nCtx, f.NativeObject,
AST.ArrayLength(args),
AST.ArrayToNative(args)));
2221 Contract.Requires(array != null);
2222 Contract.Ensures(Contract.Result<
Expr>() != null);
2224 CheckContextMatch(array);
2225 return Expr.Create(
this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2233 Contract.Requires(arg1 != null);
2234 Contract.Requires(arg2 != null);
2235 Contract.Ensures(Contract.Result<
Expr>() != null);
2237 CheckContextMatch(arg1);
2238 CheckContextMatch(arg2);
2239 return Expr.Create(
this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
2250 Contract.Requires(ty != null);
2251 Contract.Ensures(Contract.Result<
SetSort>() != null);
2253 CheckContextMatch(ty);
2262 Contract.Requires(domain != null);
2263 Contract.Ensures(Contract.Result<
Expr>() != null);
2265 CheckContextMatch(domain);
2266 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2274 Contract.Requires(domain != null);
2275 Contract.Ensures(Contract.Result<
Expr>() != null);
2277 CheckContextMatch(domain);
2278 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2286 Contract.Requires(
set != null);
2287 Contract.Requires(element != null);
2288 Contract.Ensures(Contract.Result<
Expr>() != null);
2290 CheckContextMatch(
set);
2291 CheckContextMatch(element);
2292 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_add(nCtx,
set.NativeObject, element.NativeObject));
2301 Contract.Requires(
set != null);
2302 Contract.Requires(element != null);
2303 Contract.Ensures(Contract.Result<
Expr>() != null);
2305 CheckContextMatch(
set);
2306 CheckContextMatch(element);
2307 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_del(nCtx,
set.NativeObject, element.NativeObject));
2315 Contract.Requires(args != null);
2316 Contract.Requires(Contract.ForAll(args, a => a != null));
2318 CheckContextMatch<ArrayExpr>(args);
2319 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_union(nCtx, (uint)args.Length,
AST.ArrayToNative(args)));
2327 Contract.Requires(args != null);
2328 Contract.Requires(Contract.ForAll(args, a => a != null));
2329 Contract.Ensures(Contract.Result<
Expr>() != null);
2331 CheckContextMatch<ArrayExpr>(args);
2332 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length,
AST.ArrayToNative(args)));
2340 Contract.Requires(arg1 != null);
2341 Contract.Requires(arg2 != null);
2342 Contract.Ensures(Contract.Result<
Expr>() != null);
2344 CheckContextMatch(arg1);
2345 CheckContextMatch(arg2);
2346 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2354 Contract.Requires(arg != null);
2355 Contract.Ensures(Contract.Result<
Expr>() != null);
2357 CheckContextMatch(arg);
2358 return (
ArrayExpr)
Expr.Create(
this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2366 Contract.Requires(elem != null);
2367 Contract.Requires(
set != null);
2368 Contract.Ensures(Contract.Result<
Expr>() != null);
2370 CheckContextMatch(elem);
2371 CheckContextMatch(
set);
2372 return (
BoolExpr)
Expr.Create(
this, Native.Z3_mk_set_member(nCtx, elem.NativeObject,
set.NativeObject));
2380 Contract.Requires(arg1 != null);
2381 Contract.Requires(arg2 != null);
2382 Contract.Ensures(Contract.Result<
Expr>() != null);
2384 CheckContextMatch(arg1);
2385 CheckContextMatch(arg2);
2386 return (
BoolExpr)
Expr.Create(
this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2391 #region Sequence, string and regular expresions 2398 Contract.Requires(s != null);
2399 Contract.Ensures(Contract.Result<
SeqExpr>() != null);
2400 return new SeqExpr(
this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
2408 Contract.Requires(elem != null);
2409 Contract.Ensures(Contract.Result<
SeqExpr>() != null);
2410 return new SeqExpr(
this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
2418 Contract.Requires(s != null);
2419 Contract.Ensures(Contract.Result<
SeqExpr>() != null);
2420 return new SeqExpr(
this, Native.Z3_mk_string(nCtx, s));
2428 Contract.Requires(t != null);
2429 Contract.Requires(Contract.ForAll(t, a => a != null));
2430 Contract.Ensures(Contract.Result<
SeqExpr>() != null);
2432 CheckContextMatch<SeqExpr>(t);
2433 return new SeqExpr(
this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
2442 Contract.Requires(s != null);
2443 Contract.Ensures(Contract.Result<
IntExpr>() != null);
2444 return (
IntExpr)
Expr.Create(
this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
2452 Contract.Requires(s1 != null);
2453 Contract.Requires(s2 != null);
2454 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2455 CheckContextMatch(s1, s2);
2456 return new BoolExpr(
this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
2464 Contract.Requires(s1 != null);
2465 Contract.Requires(s2 != null);
2466 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2467 CheckContextMatch(s1, s2);
2468 return new BoolExpr(
this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
2476 Contract.Requires(s1 != null);
2477 Contract.Requires(s2 != null);
2478 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2479 CheckContextMatch(s1, s2);
2480 return new BoolExpr(
this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
2488 Contract.Requires(s != null);
2489 Contract.Requires(index != null);
2490 Contract.Ensures(Contract.Result<
SeqExpr>() != null);
2491 CheckContextMatch(s, index);
2492 return new SeqExpr(
this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
2500 Contract.Requires(s != null);
2501 Contract.Requires(offset != null);
2502 Contract.Requires(length != null);
2503 Contract.Ensures(Contract.Result<
SeqExpr>() != null);
2504 CheckContextMatch(s, offset, length);
2505 return new SeqExpr(
this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
2513 Contract.Requires(s != null);
2514 Contract.Requires(offset != null);
2515 Contract.Requires(substr != null);
2516 Contract.Ensures(Contract.Result<
IntExpr>() != null);
2517 CheckContextMatch(s, substr, offset);
2518 return new IntExpr(
this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
2526 Contract.Requires(s != null);
2527 Contract.Requires(src != null);
2528 Contract.Requires(dst != null);
2529 Contract.Ensures(Contract.Result<
SeqExpr>() != null);
2530 CheckContextMatch(s, src, dst);
2531 return new SeqExpr(
this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
2539 Contract.Requires(s != null);
2540 Contract.Ensures(Contract.Result<
ReExpr>() != null);
2541 return new ReExpr(
this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));
2550 Contract.Requires(s != null);
2551 Contract.Requires(re != null);
2552 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
2553 CheckContextMatch(s, re);
2554 return new BoolExpr(
this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
2562 Contract.Requires(re != null);
2563 Contract.Ensures(Contract.Result<
ReExpr>() != null);
2564 return new ReExpr(
this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
2572 Contract.Requires(re != null);
2573 Contract.Ensures(Contract.Result<
ReExpr>() != null);
2574 return new ReExpr(
this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));
2582 Contract.Requires(re != null);
2583 Contract.Ensures(Contract.Result<
ReExpr>() != null);
2584 return new ReExpr(
this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
2592 Contract.Requires(t != null);
2593 Contract.Requires(Contract.ForAll(t, a => a != null));
2594 Contract.Ensures(Contract.Result<
ReExpr>() != null);
2596 CheckContextMatch<ReExpr>(t);
2597 return new ReExpr(
this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
2605 Contract.Requires(t != null);
2606 Contract.Requires(Contract.ForAll(t, a => a != null));
2607 Contract.Ensures(Contract.Result<
ReExpr>() != null);
2609 CheckContextMatch<ReExpr>(t);
2610 return new ReExpr(
this, Native.Z3_mk_re_union(nCtx, (uint)t.Length,
AST.ArrayToNative(t)));
2615 #region Pseudo-Boolean constraints 2622 Contract.Requires(args != null);
2623 Contract.Requires(Contract.Result<
BoolExpr[]>() != null);
2624 CheckContextMatch<BoolExpr>(args);
2625 return new BoolExpr(
this, Native.Z3_mk_atmost(nCtx, (uint) args.Length,
2626 AST.ArrayToNative(args), k));
2634 Contract.Requires(args != null);
2635 Contract.Requires(coeffs != null);
2636 Contract.Requires(args.Length == coeffs.Length);
2637 Contract.Requires(Contract.Result<
BoolExpr[]>() != null);
2638 CheckContextMatch<BoolExpr>(args);
2639 return new BoolExpr(
this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
2640 AST.ArrayToNative(args),
2649 Contract.Requires(args != null);
2650 Contract.Requires(coeffs != null);
2651 Contract.Requires(args.Length == coeffs.Length);
2652 Contract.Requires(Contract.Result<
BoolExpr[]>() != null);
2653 CheckContextMatch<BoolExpr>(args);
2654 return new BoolExpr(
this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length,
2655 AST.ArrayToNative(args),
2662 #region General Numerals 2663 public Expr MkNumeral(
string v,
Sort ty)
2671 Contract.Requires(ty != null);
2672 Contract.Ensures(Contract.Result<
Expr>() != null);
2674 CheckContextMatch(ty);
2675 return Expr.Create(
this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2687 Contract.Requires(ty != null);
2688 Contract.Ensures(Contract.Result<
Expr>() != null);
2690 CheckContextMatch(ty);
2691 return Expr.Create(
this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2703 Contract.Requires(ty != null);
2704 Contract.Ensures(Contract.Result<
Expr>() != null);
2706 CheckContextMatch(ty);
2707 return Expr.Create(
this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2719 Contract.Requires(ty != null);
2720 Contract.Ensures(Contract.Result<
Expr>() != null);
2722 CheckContextMatch(ty);
2723 return Expr.Create(
this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2735 Contract.Requires(ty != null);
2736 Contract.Ensures(Contract.Result<
Expr>() != null);
2738 CheckContextMatch(ty);
2739 return Expr.Create(
this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2744 public RatNum MkReal(
int num,
int den)
2756 Contract.Ensures(Contract.Result<
RatNum>() != null);
2757 Contract.EndContractBlock();
2759 return new RatNum(
this, Native.Z3_mk_real(nCtx, num, den));
2769 Contract.Ensures(Contract.Result<
RatNum>() != null);
2771 return new RatNum(
this, Native.Z3_mk_numeral(nCtx, v,
RealSort.NativeObject));
2781 Contract.Ensures(Contract.Result<
RatNum>() != null);
2783 return new RatNum(
this, Native.Z3_mk_int(nCtx, v,
RealSort.NativeObject));
2793 Contract.Ensures(Contract.Result<
RatNum>() != null);
2795 return new RatNum(
this, Native.Z3_mk_unsigned_int(nCtx, v,
RealSort.NativeObject));
2805 Contract.Ensures(Contract.Result<
RatNum>() != null);
2807 return new RatNum(
this, Native.Z3_mk_int64(nCtx, v,
RealSort.NativeObject));
2817 Contract.Ensures(Contract.Result<
RatNum>() != null);
2819 return new RatNum(
this, Native.Z3_mk_unsigned_int64(nCtx, v,
RealSort.NativeObject));
2824 public IntNum MkInt(
string v)
2830 Contract.Ensures(Contract.Result<
IntNum>() != null);
2832 return new IntNum(
this, Native.Z3_mk_numeral(nCtx, v,
IntSort.NativeObject));
2842 Contract.Ensures(Contract.Result<
IntNum>() != null);
2844 return new IntNum(
this, Native.Z3_mk_int(nCtx, v,
IntSort.NativeObject));
2854 Contract.Ensures(Contract.Result<
IntNum>() != null);
2856 return new IntNum(
this, Native.Z3_mk_unsigned_int(nCtx, v,
IntSort.NativeObject));
2866 Contract.Ensures(Contract.Result<
IntNum>() != null);
2868 return new IntNum(
this, Native.Z3_mk_int64(nCtx, v,
IntSort.NativeObject));
2878 Contract.Ensures(Contract.Result<
IntNum>() != null);
2880 return new IntNum(
this, Native.Z3_mk_unsigned_int64(nCtx, v,
IntSort.NativeObject));
2885 public BitVecNum MkBV(
string v, uint size)
2892 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2894 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2904 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2906 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2916 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2918 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2928 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2930 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2940 Contract.Ensures(Contract.Result<
BitVecNum>() != null);
2942 return (
BitVecNum)MkNumeral(v, MkBitVecSort(size));
2946 #endregion // Numerals 2975 Contract.Requires(sorts != null);
2976 Contract.Requires(names != null);
2977 Contract.Requires(body != null);
2978 Contract.Requires(sorts.Length == names.Length);
2979 Contract.Requires(Contract.ForAll(sorts, s => s != null));
2980 Contract.Requires(Contract.ForAll(names, n => n != null));
2981 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2982 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2984 Contract.Ensures(Contract.Result<
Quantifier>() != null);
2986 return new Quantifier(
this,
true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3000 Contract.Requires(body != null);
3001 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
3002 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3003 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3005 Contract.Ensures(Contract.Result<
Quantifier>() != null);
3007 return new Quantifier(
this,
true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3019 Contract.Requires(sorts != null);
3020 Contract.Requires(names != null);
3021 Contract.Requires(body != null);
3022 Contract.Requires(sorts.Length == names.Length);
3023 Contract.Requires(Contract.ForAll(sorts, s => s != null));
3024 Contract.Requires(Contract.ForAll(names, n => n != null));
3025 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3026 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3027 Contract.Ensures(Contract.Result<
Quantifier>() != null);
3029 return new Quantifier(
this,
false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3042 Contract.Requires(body != null);
3043 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
3044 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3045 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3046 Contract.Ensures(Contract.Result<
Quantifier>() != null);
3048 return new Quantifier(
this,
false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3058 Contract.Requires(body != null);
3059 Contract.Requires(names != null);
3060 Contract.Requires(sorts != null);
3061 Contract.Requires(sorts.Length == names.Length);
3062 Contract.Requires(Contract.ForAll(sorts, s => s != null));
3063 Contract.Requires(Contract.ForAll(names, n => n != null));
3064 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3065 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3067 Contract.Ensures(Contract.Result<
Quantifier>() != null);
3070 return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3072 return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3082 Contract.Requires(body != null);
3083 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
3084 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3085 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3087 Contract.Ensures(Contract.Result<
Quantifier>() != null);
3090 return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3092 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3118 set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
3122 #region SMT Files & Strings 3123 public string BenchmarkToSMTString(
string name,
string logic,
string status,
string attributes,
3136 Contract.Requires(assumptions != null);
3137 Contract.Requires(formula != null);
3138 Contract.Ensures(Contract.Result<
string>() != null);
3140 return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
3141 (uint)assumptions.Length,
AST.ArrayToNative(assumptions),
3142 formula.NativeObject);
3157 uint csn =
Symbol.ArrayLength(sortNames);
3158 uint cs =
Sort.ArrayLength(sorts);
3159 uint cdn =
Symbol.ArrayLength(declNames);
3160 uint cd =
AST.ArrayLength(decls);
3161 if (csn != cs || cdn != cd)
3163 Native.Z3_parse_smtlib_string(nCtx, str,
3164 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
3165 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls));
3174 uint csn =
Symbol.ArrayLength(sortNames);
3175 uint cs =
Sort.ArrayLength(sorts);
3176 uint cdn =
Symbol.ArrayLength(declNames);
3177 uint cd =
AST.ArrayLength(decls);
3178 if (csn != cs || cdn != cd)
3180 Native.Z3_parse_smtlib_file(nCtx, fileName,
3181 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
3182 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls));
3188 public uint NumSMTLIBFormulas {
get {
return Native.Z3_get_smtlib_num_formulas(nCtx); } }
3197 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
3199 uint n = NumSMTLIBFormulas;
3201 for (uint i = 0; i < n; i++)
3202 res[i] = (
BoolExpr)
Expr.Create(
this, Native.Z3_get_smtlib_formula(nCtx, i));
3210 public uint NumSMTLIBAssumptions {
get {
return Native.Z3_get_smtlib_num_assumptions(nCtx); } }
3215 public BoolExpr[] SMTLIBAssumptions
3219 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
3221 uint n = NumSMTLIBAssumptions;
3223 for (uint i = 0; i < n; i++)
3224 res[i] = (
BoolExpr)
Expr.Create(
this, Native.Z3_get_smtlib_assumption(nCtx, i));
3232 public uint NumSMTLIBDecls {
get {
return Native.Z3_get_smtlib_num_decls(nCtx); } }
3241 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
3243 uint n = NumSMTLIBDecls;
3245 for (uint i = 0; i < n; i++)
3246 res[i] =
new FuncDecl(
this, Native.Z3_get_smtlib_decl(nCtx, i));
3254 public uint NumSMTLIBSorts {
get {
return Native.Z3_get_smtlib_num_sorts(nCtx); } }
3259 public Sort[] SMTLIBSorts
3263 Contract.Ensures(Contract.Result<
Sort[]>() != null);
3265 uint n = NumSMTLIBSorts;
3267 for (uint i = 0; i < n; i++)
3268 res[i] =
Sort.Create(
this, Native.Z3_get_smtlib_sort(nCtx, i));
3280 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
3282 uint csn =
Symbol.ArrayLength(sortNames);
3283 uint cs =
Sort.ArrayLength(sorts);
3284 uint cdn =
Symbol.ArrayLength(declNames);
3285 uint cd =
AST.ArrayLength(decls);
3286 if (csn != cs || cdn != cd)
3288 return (
BoolExpr)
Expr.Create(
this, Native.Z3_parse_smtlib2_string(nCtx, str,
3289 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
3290 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls)));
3299 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
3301 uint csn =
Symbol.ArrayLength(sortNames);
3302 uint cs =
Sort.ArrayLength(sorts);
3303 uint cdn =
Symbol.ArrayLength(declNames);
3304 uint cd =
AST.ArrayLength(decls);
3305 if (csn != cs || cdn != cd)
3307 return (
BoolExpr)
Expr.Create(
this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
3308 AST.ArrayLength(sorts),
Symbol.ArrayToNative(sortNames),
AST.ArrayToNative(sorts),
3309 AST.ArrayLength(decls),
Symbol.ArrayToNative(declNames),
AST.ArrayToNative(decls)));
3314 public Goal MkGoal(
bool models =
true,
bool unsatCores =
false,
bool proofs =
false)
3326 Contract.Ensures(Contract.Result<
Goal>() != null);
3328 return new Goal(
this, models, unsatCores, proofs);
3332 #region ParameterSets 3338 Contract.Ensures(Contract.Result<
Params>() != null);
3345 public uint NumTactics
3350 get {
return Native.Z3_get_num_tactics(nCtx); }
3356 public string[] TacticNames
3360 Contract.Ensures(Contract.Result<
string[]>() != null);
3362 uint n = NumTactics;
3363 string[] res =
new string[n];
3364 for (uint i = 0; i < n; i++)
3365 res[i] = Native.Z3_get_tactic_name(nCtx, i);
3375 Contract.Ensures(Contract.Result<
string>() != null);
3377 return Native.Z3_tactic_get_descr(nCtx, name);
3385 Contract.Ensures(Contract.Result<
Tactic>() != null);
3387 return new Tactic(
this, name);
3396 Contract.Requires(t1 != null);
3397 Contract.Requires(t2 != null);
3398 Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3399 Contract.Ensures(Contract.Result<
Tactic>() != null);
3402 CheckContextMatch(t1);
3403 CheckContextMatch(t2);
3404 CheckContextMatch<Tactic>(ts);
3406 IntPtr last = IntPtr.Zero;
3407 if (ts != null && ts.Length > 0)
3409 last = ts[ts.Length - 1].NativeObject;
3410 for (
int i = ts.Length - 2; i >= 0; i--)
3411 last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3413 if (last != IntPtr.Zero)
3415 last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3416 return new Tactic(
this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3419 return new Tactic(
this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3431 Contract.Requires(t1 != null);
3432 Contract.Requires(t2 != null);
3433 Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3434 Contract.Ensures(Contract.Result<
Tactic>() != null);
3445 Contract.Requires(t1 != null);
3446 Contract.Requires(t2 != null);
3447 Contract.Ensures(Contract.Result<
Tactic>() != null);
3449 CheckContextMatch(t1);
3450 CheckContextMatch(t2);
3451 return new Tactic(
this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3462 Contract.Requires(t != null);
3463 Contract.Ensures(Contract.Result<
Tactic>() != null);
3465 CheckContextMatch(t);
3466 return new Tactic(
this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3478 Contract.Requires(p != null);
3479 Contract.Requires(t != null);
3480 Contract.Ensures(Contract.Result<
Tactic>() != null);
3482 CheckContextMatch(t);
3483 CheckContextMatch(p);
3484 return new Tactic(
this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3493 Contract.Requires(p != null);
3494 Contract.Requires(t1 != null);
3495 Contract.Requires(t2 != null);
3496 Contract.Ensures(Contract.Result<
Tactic>() != null);
3498 CheckContextMatch(p);
3499 CheckContextMatch(t1);
3500 CheckContextMatch(t2);
3501 return new Tactic(
this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3510 Contract.Requires(t != null);
3511 Contract.Ensures(Contract.Result<
Tactic>() != null);
3513 CheckContextMatch(t);
3514 return new Tactic(
this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3522 Contract.Ensures(Contract.Result<
Tactic>() != null);
3524 return new Tactic(
this, Native.Z3_tactic_skip(nCtx));
3532 Contract.Ensures(Contract.Result<
Tactic>() != null);
3534 return new Tactic(
this, Native.Z3_tactic_fail(nCtx));
3542 Contract.Requires(p != null);
3543 Contract.Ensures(Contract.Result<
Tactic>() != null);
3545 CheckContextMatch(p);
3546 return new Tactic(
this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3555 Contract.Ensures(Contract.Result<
Tactic>() != null);
3557 return new Tactic(
this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3565 Contract.Requires(t != null);
3566 Contract.Requires(p != null);
3567 Contract.Ensures(Contract.Result<
Tactic>() != null);
3569 CheckContextMatch(t);
3570 CheckContextMatch(p);
3571 return new Tactic(
this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3580 Contract.Requires(t != null);
3581 Contract.Requires(p != null);
3582 Contract.Ensures(Contract.Result<
Tactic>() != null);
3584 return UsingParams(t, p);
3592 Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3593 Contract.Ensures(Contract.Result<
Tactic>() != null);
3595 CheckContextMatch<Tactic>(t);
3596 return new Tactic(
this, Native.Z3_tactic_par_or(nCtx,
Tactic.ArrayLength(t),
Tactic.ArrayToNative(t)));
3605 Contract.Requires(t1 != null);
3606 Contract.Requires(t2 != null);
3607 Contract.Ensures(Contract.Result<
Tactic>() != null);
3609 CheckContextMatch(t1);
3610 CheckContextMatch(t2);
3611 return new Tactic(
this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3620 Native.Z3_interrupt(nCtx);
3625 public uint NumProbes
3630 get {
return Native.Z3_get_num_probes(nCtx); }
3636 public string[] ProbeNames
3640 Contract.Ensures(Contract.Result<
string[]>() != null);
3643 string[] res =
new string[n];
3644 for (uint i = 0; i < n; i++)
3645 res[i] = Native.Z3_get_probe_name(nCtx, i);
3655 Contract.Ensures(Contract.Result<
string>() != null);
3657 return Native.Z3_probe_get_descr(nCtx, name);
3665 Contract.Ensures(Contract.Result<
Probe>() != null);
3667 return new Probe(
this, name);
3675 Contract.Ensures(Contract.Result<
Probe>() != null);
3677 return new Probe(
this, Native.Z3_probe_const(nCtx, val));
3686 Contract.Requires(p1 != null);
3687 Contract.Requires(p2 != null);
3688 Contract.Ensures(Contract.Result<
Probe>() != null);
3690 CheckContextMatch(p1);
3691 CheckContextMatch(p2);
3692 return new Probe(
this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3701 Contract.Requires(p1 != null);
3702 Contract.Requires(p2 != null);
3703 Contract.Ensures(Contract.Result<
Probe>() != null);
3705 CheckContextMatch(p1);
3706 CheckContextMatch(p2);
3707 return new Probe(
this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3716 Contract.Requires(p1 != null);
3717 Contract.Requires(p2 != null);
3718 Contract.Ensures(Contract.Result<
Probe>() != null);
3720 CheckContextMatch(p1);
3721 CheckContextMatch(p2);
3722 return new Probe(
this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3731 Contract.Requires(p1 != null);
3732 Contract.Requires(p2 != null);
3733 Contract.Ensures(Contract.Result<
Probe>() != null);
3735 CheckContextMatch(p1);
3736 CheckContextMatch(p2);
3737 return new Probe(
this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3746 Contract.Requires(p1 != null);
3747 Contract.Requires(p2 != null);
3748 Contract.Ensures(Contract.Result<
Probe>() != null);
3750 CheckContextMatch(p1);
3751 CheckContextMatch(p2);
3752 return new Probe(
this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3761 Contract.Requires(p1 != null);
3762 Contract.Requires(p2 != null);
3763 Contract.Ensures(Contract.Result<
Probe>() != null);
3765 CheckContextMatch(p1);
3766 CheckContextMatch(p2);
3767 return new Probe(
this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3776 Contract.Requires(p1 != null);
3777 Contract.Requires(p2 != null);
3778 Contract.Ensures(Contract.Result<
Probe>() != null);
3780 CheckContextMatch(p1);
3781 CheckContextMatch(p2);
3782 return new Probe(
this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3791 Contract.Requires(p != null);
3792 Contract.Ensures(Contract.Result<
Probe>() != null);
3794 CheckContextMatch(p);
3795 return new Probe(
this, Native.Z3_probe_not(nCtx, p.NativeObject));
3810 Contract.Ensures(Contract.Result<
Solver>() != null);
3813 return new Solver(
this, Native.Z3_mk_solver(nCtx));
3815 return new Solver(
this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3824 Contract.Ensures(Contract.Result<
Solver>() != null);
3826 return MkSolver(MkSymbol(logic));
3834 Contract.Ensures(Contract.Result<
Solver>() != null);
3836 return new Solver(
this, Native.Z3_mk_simple_solver(nCtx));
3848 Contract.Requires(t != null);
3849 Contract.Ensures(Contract.Result<
Solver>() != null);
3851 return new Solver(
this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3861 Contract.Ensures(Contract.Result<
Fixedpoint>() != null);
3867 #region Optimization 3873 Contract.Ensures(Contract.Result<
Optimize>() != null);
3879 #region Floating-Point Arithmetic 3881 #region Rounding Modes 3882 #region RoundingMode Sort 3883 public FPRMSort MkFPRoundingModeSort()
3888 Contract.Ensures(Contract.Result<
FPRMSort>() != null);
3894 public FPRMExpr MkFPRoundNearestTiesToEven()
3899 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3900 return new FPRMExpr(
this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
3908 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3909 return new FPRMNum(
this, Native.Z3_mk_fpa_rne(nCtx));
3917 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3918 return new FPRMNum(
this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
3926 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3927 return new FPRMNum(
this, Native.Z3_mk_fpa_rna(nCtx));
3935 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3936 return new FPRMNum(
this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
3944 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3945 return new FPRMNum(
this, Native.Z3_mk_fpa_rtp(nCtx));
3953 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3954 return new FPRMNum(
this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
3962 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3963 return new FPRMNum(
this, Native.Z3_mk_fpa_rtn(nCtx));
3971 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3972 return new FPRMNum(
this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
3980 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
3981 return new FPRMNum(
this, Native.Z3_mk_fpa_rtz(nCtx));
3986 #region FloatingPoint Sorts 3987 public FPSort MkFPSort(uint ebits, uint sbits)
3994 Contract.Ensures(Contract.Result<
FPSort>() != null);
3995 return new FPSort(
this, ebits, sbits);
4003 Contract.Ensures(Contract.Result<
FPSort>() != null);
4004 return new FPSort(
this, Native.Z3_mk_fpa_sort_half(nCtx));
4012 Contract.Ensures(Contract.Result<
FPSort>() != null);
4013 return new FPSort(
this, Native.Z3_mk_fpa_sort_16(nCtx));
4021 Contract.Ensures(Contract.Result<
FPSort>() != null);
4022 return new FPSort(
this, Native.Z3_mk_fpa_sort_single(nCtx));
4030 Contract.Ensures(Contract.Result<
FPSort>() != null);
4031 return new FPSort(
this, Native.Z3_mk_fpa_sort_32(nCtx));
4039 Contract.Ensures(Contract.Result<
FPSort>() != null);
4040 return new FPSort(
this, Native.Z3_mk_fpa_sort_double(nCtx));
4048 Contract.Ensures(Contract.Result<
FPSort>() != null);
4049 return new FPSort(
this, Native.Z3_mk_fpa_sort_64(nCtx));
4057 Contract.Ensures(Contract.Result<
FPSort>() != null);
4058 return new FPSort(
this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
4066 Contract.Ensures(Contract.Result<
FPSort>() != null);
4067 return new FPSort(
this, Native.Z3_mk_fpa_sort_128(nCtx));
4078 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4079 return new FPNum(
this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
4089 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4090 return new FPNum(
this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0));
4100 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4101 return new FPNum(
this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
4111 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4112 return new FPNum(
this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
4122 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4123 return new FPNum(
this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
4133 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4134 return new FPNum(
this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
4146 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4147 return new FPNum(
this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
4159 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4160 return new FPNum(
this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
4170 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4171 return MkFPNumeral(v, s);
4181 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4182 return MkFPNumeral(v, s);
4192 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4193 return MkFPNumeral(v, s);
4205 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4206 return MkFPNumeral(sgn, exp, sig, s);
4218 Contract.Ensures(Contract.Result<
FPRMExpr>() != null);
4219 return MkFPNumeral(sgn, exp, sig, s);
4231 Contract.Ensures(Contract.Result<
FPNum>() != null);
4232 return new FPExpr(
this, Native.Z3_mk_fpa_abs(
this.nCtx, t.NativeObject));
4241 Contract.Ensures(Contract.Result<
FPNum>() != null);
4242 return new FPExpr(
this, Native.Z3_mk_fpa_neg(
this.nCtx, t.NativeObject));
4253 Contract.Ensures(Contract.Result<
FPNum>() != null);
4254 return new FPExpr(
this, Native.Z3_mk_fpa_add(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4265 Contract.Ensures(Contract.Result<
FPNum>() != null);
4266 return new FPExpr(
this, Native.Z3_mk_fpa_sub(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4277 Contract.Ensures(Contract.Result<
FPNum>() != null);
4278 return new FPExpr(
this, Native.Z3_mk_fpa_mul(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4289 Contract.Ensures(Contract.Result<
FPNum>() != null);
4290 return new FPExpr(
this, Native.Z3_mk_fpa_div(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4305 Contract.Ensures(Contract.Result<
FPNum>() != null);
4306 return new FPExpr(
this, Native.Z3_mk_fpa_fma(
this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
4316 Contract.Ensures(Contract.Result<
FPNum>() != null);
4317 return new FPExpr(
this, Native.Z3_mk_fpa_sqrt(
this.nCtx, rm.NativeObject, t.NativeObject));
4327 Contract.Ensures(Contract.Result<
FPNum>() != null);
4328 return new FPExpr(
this, Native.Z3_mk_fpa_rem(
this.nCtx, t1.NativeObject, t2.NativeObject));
4339 Contract.Ensures(Contract.Result<
FPNum>() != null);
4340 return new FPExpr(
this, Native.Z3_mk_fpa_round_to_integral(
this.nCtx, rm.NativeObject, t.NativeObject));
4350 Contract.Ensures(Contract.Result<
FPNum>() != null);
4351 return new FPExpr(
this, Native.Z3_mk_fpa_min(
this.nCtx, t1.NativeObject, t2.NativeObject));
4361 Contract.Ensures(Contract.Result<
FPNum>() != null);
4362 return new FPExpr(
this, Native.Z3_mk_fpa_max(
this.nCtx, t1.NativeObject, t2.NativeObject));
4372 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4373 return new BoolExpr(
this, Native.Z3_mk_fpa_leq(
this.nCtx, t1.NativeObject, t2.NativeObject));
4383 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4384 return new BoolExpr(
this, Native.Z3_mk_fpa_lt(
this.nCtx, t1.NativeObject, t2.NativeObject));
4394 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4395 return new BoolExpr(
this, Native.Z3_mk_fpa_geq(
this.nCtx, t1.NativeObject, t2.NativeObject));
4405 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4406 return new BoolExpr(
this, Native.Z3_mk_fpa_gt(
this.nCtx, t1.NativeObject, t2.NativeObject));
4419 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4420 return new BoolExpr(
this, Native.Z3_mk_fpa_eq(
this.nCtx, t1.NativeObject, t2.NativeObject));
4429 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4430 return new BoolExpr(
this, Native.Z3_mk_fpa_is_normal(
this.nCtx, t.NativeObject));
4439 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4440 return new BoolExpr(
this, Native.Z3_mk_fpa_is_subnormal(
this.nCtx, t.NativeObject));
4449 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4450 return new BoolExpr(
this, Native.Z3_mk_fpa_is_zero(
this.nCtx, t.NativeObject));
4459 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4460 return new BoolExpr(
this, Native.Z3_mk_fpa_is_infinite(
this.nCtx, t.NativeObject));
4469 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4470 return new BoolExpr(
this, Native.Z3_mk_fpa_is_nan(
this.nCtx, t.NativeObject));
4479 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4480 return new BoolExpr(
this, Native.Z3_mk_fpa_is_negative(
this.nCtx, t.NativeObject));
4489 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
4490 return new BoolExpr(
this, Native.Z3_mk_fpa_is_positive(
this.nCtx, t.NativeObject));
4494 #region Conversions to FloatingPoint terms 4510 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4511 return new FPExpr(
this, Native.Z3_mk_fpa_fp(
this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
4527 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4528 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_bv(
this.nCtx, bv.NativeObject, s.NativeObject));
4544 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4545 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_float(
this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4561 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4562 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_real(
this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4580 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4582 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_signed(
this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4584 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_unsigned(
this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4599 Contract.Ensures(Contract.Result<
FPExpr>() != null);
4600 return new FPExpr(
this, Native.Z3_mk_fpa_to_fp_float(
this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
4604 #region Conversions from FloatingPoint terms 4619 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
4621 return new BitVecExpr(
this, Native.Z3_mk_fpa_to_sbv(
this.nCtx, rm.NativeObject, t.NativeObject, sz));
4623 return new BitVecExpr(
this, Native.Z3_mk_fpa_to_ubv(
this.nCtx, rm.NativeObject, t.NativeObject, sz));
4637 Contract.Ensures(Contract.Result<
RealExpr>() != null);
4638 return new RealExpr(
this, Native.Z3_mk_fpa_to_real(
this.nCtx, t.NativeObject));
4642 #region Z3-specific extensions 4655 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
4656 return new BitVecExpr(
this, Native.Z3_mk_fpa_to_ieee_bv(
this.nCtx, t.NativeObject));
4673 Contract.Ensures(Contract.Result<
BitVecExpr>() != null);
4674 return new BitVecExpr(
this, Native.Z3_mk_fpa_to_fp_int_real(
this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
4677 #endregion // Floating-point Arithmetic 4679 #region Miscellaneous 4680 public AST WrapAST(IntPtr nativeObject)
4692 Contract.Ensures(Contract.Result<
AST>() != null);
4693 return AST.Create(
this, nativeObject);
4709 return a.NativeObject;
4717 Contract.Ensures(Contract.Result<
string>() != null);
4719 return Native.Z3_simplify_get_help(nCtx);
4727 get {
return new ParamDescrs(
this, Native.Z3_simplify_get_param_descrs(nCtx)); }
4731 #region Error Handling 4748 public void UpdateParamValue(
string id,
string value)
4759 Native.Z3_update_param_value(nCtx,
id, value);
4765 internal IntPtr m_ctx = IntPtr.Zero;
4766 internal Native.Z3_error_handler m_n_err_handler = null;
4767 internal static Object creation_lock =
new Object();
4768 internal IntPtr nCtx {
get {
return m_ctx; } }
4770 internal void NativeErrorHandler(IntPtr ctx,
Z3_error_code errorCode)
4775 internal void InitContext()
4778 m_n_err_handler =
new Native.Z3_error_handler(NativeErrorHandler);
4779 Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
4780 GC.SuppressFinalize(
this);
4784 internal void CheckContextMatch(
Z3Object other)
4786 Contract.Requires(other != null);
4788 if (!ReferenceEquals(
this, other.Context))
4795 Contract.Requires(other1 != null);
4796 Contract.Requires(other2 != null);
4797 CheckContextMatch(other1);
4798 CheckContextMatch(other2);
4804 Contract.Requires(other1 != null);
4805 Contract.Requires(other2 != null);
4806 Contract.Requires(other3 != null);
4807 CheckContextMatch(other1);
4808 CheckContextMatch(other2);
4809 CheckContextMatch(other3);
4813 internal void CheckContextMatch(
Z3Object[] arr)
4815 Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
4821 Contract.Assert(a != null);
4822 CheckContextMatch(a);
4828 internal void CheckContextMatch<T>(IEnumerable<T> arr) where T :
Z3Object 4830 Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
4836 Contract.Assert(a != null);
4837 CheckContextMatch(a);
4843 private void ObjectInvariant()
4845 Contract.Invariant(m_AST_DRQ != null);
4846 Contract.Invariant(m_ASTMap_DRQ != null);
4847 Contract.Invariant(m_ASTVector_DRQ != null);
4848 Contract.Invariant(m_ApplyResult_DRQ != null);
4849 Contract.Invariant(m_FuncEntry_DRQ != null);
4850 Contract.Invariant(m_FuncInterp_DRQ != null);
4851 Contract.Invariant(m_Goal_DRQ != null);
4852 Contract.Invariant(m_Model_DRQ != null);
4853 Contract.Invariant(m_Params_DRQ != null);
4854 Contract.Invariant(m_ParamDescrs_DRQ != null);
4855 Contract.Invariant(m_Probe_DRQ != null);
4856 Contract.Invariant(m_Solver_DRQ != null);
4857 Contract.Invariant(m_Statistics_DRQ != null);
4858 Contract.Invariant(m_Tactic_DRQ != null);
4859 Contract.Invariant(m_Fixedpoint_DRQ != null);
4860 Contract.Invariant(m_Optimize_DRQ != null);
4864 readonly
private ASTMap.DecRefQueue m_ASTMap_DRQ =
new ASTMap.DecRefQueue(10);
4888 public IDecRefQueue ASTMap_DRQ {
get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null);
return m_ASTMap_DRQ; } }
4961 internal long refCount = 0;
4971 if (refCount == 0 && m_ctx != IntPtr.Zero)
4973 m_n_err_handler = null;
4975 m_ctx = IntPtr.Zero;
4976 Native.Z3_del_context(ctx);
4979 GC.ReRegisterForFinalize(
this);
4988 AST_DRQ.Clear(
this);
4989 ASTMap_DRQ.Clear(
this);
4990 ASTVector_DRQ.Clear(
this);
4991 ApplyResult_DRQ.Clear(
this);
4992 FuncEntry_DRQ.Clear(
this);
4993 FuncInterp_DRQ.Clear(
this);
4994 Goal_DRQ.Clear(
this);
4995 Model_DRQ.Clear(
this);
4996 Params_DRQ.Clear(
this);
4997 ParamDescrs_DRQ.Clear(
this);
4998 Probe_DRQ.Clear(
this);
4999 Solver_DRQ.Clear(
this);
5000 Statistics_DRQ.Clear(
this);
5001 Tactic_DRQ.Clear(
this);
5002 Fixedpoint_DRQ.Clear(
this);
5003 Optimize_DRQ.Clear(
this);
5008 m_stringSort = null;
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
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.
BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
Floating-point less than or equal.
Object for managing optimizization context
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
BoolExpr MkIsInteger(RealExpr t)
Creates an expression that checks whether a real number is an integer.
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...
FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point division
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
Bitwise conjunction.
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...
Tactic MkTactic(string name)
Creates a new Tactic.
BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean less-or-equal constraint.
SeqExpr MkConcat(params SeqExpr[] t)
Concatentate sequences.
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. The result is a sort
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.
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.
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 .
FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two integers.
SeqExpr MkUnit(Expr elem)
Create the singleton sequence.
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.
Probe Not(Probe p)
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Unsigned division.
Tactic When(Probe p, Tactic t)
Create a tactic that applies t to a given goal if the probe p evaluates to true.
Tactic Repeat(Tactic t, uint max=uint.MaxValue)
Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number o...
BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater than or equal to.
BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
Bit-vector extraction.
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.
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.
IntNum MkInt(int v)
Create an integer numeral.
Tactic ParOr(params Tactic[] t)
Create a tactic that applies the given tactics in parallel until one of them succeeds (i...
BitVecExpr MkBVNeg(BitVecExpr t)
Standard two's complement unary minus.
ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
Maps f on the argument arrays.
Z3_error_code
Z3 error codes (See Z3_get_error_code).
ReExpr MOption(ReExpr re)
Create the optional regular expression.
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...
ReSort MkReSort(SeqSort s)
Create a new regular expression sort.
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...
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. The result is a sortElements of the sort are created using MkNumeral...
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.
BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
Unsigned greater-than.
FPSort MkFPSortSingle()
Create the single-precision (32-bit) FloatingPoint sort.
Floating-point rounding mode numerals
BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than or equal to.
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
BoolExpr MkBoolConst(Symbol name)
Create a Boolean constant.
IntNum MkInt(uint v)
Create an integer numeral.
SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
Replace the first occurrence of src by dst in s.
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".
Expr MkApp(FuncDecl f, IEnumerable< Expr > args)
Create a new function application.
ListSort MkListSort(Symbol name, Sort elemSort)
Create a new list sort.
BoolExpr MkFPIsNaN(FPExpr t)
Predicate indicating whether t is a NaN.
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
ArrayExpr MkFullSet(Sort domain)
Create the full set.
DatatypeSort [] MkDatatypeSorts(string[] names, Constructor[][] c)
Create mutually recursive data-types.
ReExpr MPlus(ReExpr re)
Take the Kleene plus of a regular expression.
Tactics are the basic building block for creating custom solvers for specific problem domains...
FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two integers.
FPRMNum MkFPRoundTowardZero()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode...
Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned...
FPSort MkFPSort16()
Create the half-precision (16-bit) FloatingPoint sort.
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.
ArithExpr MkMul(IEnumerable< ArithExpr > t)
Create an expression representing t[0] * t[1] * ....
ReExpr MkToRe(SeqExpr s)
Convert a regular expression that accepts sequence s.
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...
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...
BoolExpr MkAtMost(BoolExpr[] args, uint k)
Create an at-most-k constraint.
RatNum MkReal(int v)
Create a real numeral.
FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
Creates a new function declaration.
FPExpr MkFPNeg(FPExpr t)
Floating-point negation
DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
Create a new datatype sort.
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.
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.
RealExpr MkRealConst(string name)
Creates a real constant.
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.
BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise NOR.
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.
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.
StringSymbol MkSymbol(string name)
Create a symbol using a string.
FPSort MkFPSort128()
Create the quadruple-precision (128-bit) FloatingPoint sort.
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.
FPNum MkFPZero(FPSort s, bool negative)
Create a floating-point zero of sort s.
ArithExpr MkAdd(IEnumerable< ArithExpr > t)
Create an expression representing t[0] + t[1] + ....
BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise addition does not underflow.
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
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.
BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater-than.
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.
BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
Floating-point equality.
Constructors are used for datatype sorts.
A regular expression sort
Probe MkProbe(string name)
Creates a new Probe.
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
Shift left.
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
Bitwise disjunction.
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
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.
IntExpr MkLength(SeqExpr s)
Retrieve the length of a given sequence.
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...
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
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...
BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than or equal to.
BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
Rotate Right.
SeqExpr MkAt(SeqExpr s, IntExpr index)
Retrieve sequence of length one at index.
EnumSort MkEnumSort(string name, params string[] enumNames)
Create a new enumeration sort.
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 -> t2.
BoolExpr MkFPIsNegative(FPExpr t)
Predicate indicating whether t is a negative floating-point number.
BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise multiplication does not underflow.
FPRMNum MkFPRoundTowardPositive()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode...
FPSort MkFPSortDouble()
Create the double-precision (64-bit) FloatingPoint sort.
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.
BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
Check for sequence containment of s2 in s1.
Probe Or(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".
SeqExpr MkEmptySeq(Sort s)
Create the empty sequence.
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
ArrayExpr MkSetDel(ArrayExpr set, Expr element)
Remove an element from a set.
A Params objects represents a configuration in the form of Symbol/value pairs.
ListSort MkListSort(string name, Sort elemSort)
Create a new list sort.
BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise addition does not overflow.
BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
Floating-point less than.
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.
A ParamDescrs describes a set of parameters.
BitVecNum MkBV(int v, uint size)
Create a bit-vector numeral.
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.
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.
RealExpr MkInt2Real(IntExpr t)
Coerce an integer to a real.
FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point multiplication
def EnumSort(name, values, ctx=None)
IntExpr MkIntConst(string name)
Creates an integer constant.
BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
Floating-point greater than.
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.
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.
BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean equal constraint.
SeqSort MkSeqSort(Sort s)
Create a new sequence sort.
BoolExpr MkOr(IEnumerable< BoolExpr > t)
Create an expression representing t[0] or t[1] or ....
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 iff t2.
The main interaction with Z3 happens via the Context.
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 ...
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.
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).
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...
ReExpr MkConcat(params ReExpr[] t)
Create the concatenation of regular languages.
BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Check for subsetness of sets.
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.
The exception base class for error reporting from Z3
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.
ReExpr MkUnion(params ReExpr[] t)
Create the union of regular languages.
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)
RealExpr MkRealConst(Symbol name)
Creates a real constant.
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.
Object for managing fixedpoints
ReExpr MkStar(ReExpr re)
Take the Kleene star of a regular expression.
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 .
IntExpr MkBV2Int(BitVecExpr t, bool signed)
Create an integer from the bit-vector argument t .
BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
Unsigned remainder.
SeqExpr MkString(string s)
Create a string constant.
RatNum MkReal(long v)
Create a real numeral.
IntNum MkInt(long v)
Create an integer numeral.
Expr MkSelect(ArrayExpr a, Expr i)
Array read.
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.
Regular expression expressions
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...
Tactic FailIfNotDecided()
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatis...
SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
Extract subsequence.
BoolExpr MkFalse()
The false Term.
BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
Check for sequence suffix.
ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
Add an element to the set.
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.
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.
FPSort MkFPSort32()
Create the single-precision (32-bit) FloatingPoint sort.
ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Take the difference between two sets.
Tactic Skip()
Create a tactic that just returns the given goal.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
FPSort MkFPSortHalf()
Create the half-precision (16-bit) FloatingPoint sort.
IntExpr MkReal2Int(RealExpr t)
Coerce a real to an integer.
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.
FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
Creates a new function declaration.
FPSort MkFPSort64()
Create the double-precision (64-bit) FloatingPoint sort.
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.
BoolExpr MkAnd(IEnumerable< BoolExpr > t)
Create an expression representing t[0] and t[1] and ....
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.
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
BoolExpr MkInRe(SeqExpr s, ReExpr re)
Check for regular expression membership.
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Extract index of sub-string starting at offset.
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.
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.
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.
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 .
BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
Check for sequence prefix.