Z3
Context.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Context.cs
7
8Abstract:
9
10 Z3 Managed API: Context
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-15
15
16Notes:
17
18--*/
19
20using System;
21using System.Diagnostics;
22using System.Collections.Generic;
23using System.Runtime.InteropServices;
24using System.Linq;
25
26namespace Microsoft.Z3
27{
31 public class Context : IDisposable
32 {
33 #region Constructors
37 public Context()
38 : base()
39 {
40 lock (creation_lock)
41 {
42 m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
43 InitContext();
44 }
45 }
46
65 public Context(Dictionary<string, string> settings)
66 : base()
67 {
68 Debug.Assert(settings != null);
69
70 lock (creation_lock)
71 {
72 IntPtr cfg = Native.Z3_mk_config();
73 foreach (KeyValuePair<string, string> kv in settings)
74 Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
75 m_ctx = Native.Z3_mk_context_rc(cfg);
76 Native.Z3_del_config(cfg);
77 InitContext();
78 }
79 }
80 #endregion
81
82 #region Symbols
90 public IntSymbol MkSymbol(int i)
91 {
92
93 return new IntSymbol(this, i);
94 }
95
99 public StringSymbol MkSymbol(string name)
100 {
101
102 return new StringSymbol(this, name);
103 }
104
108 internal Symbol[] MkSymbols(string[] names)
109 {
110
111 if (names == null) return null;
112 Symbol[] result = new Symbol[names.Length];
113 for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
114 return result;
115 }
116 #endregion
117
118 #region Sorts
119 private BoolSort m_boolSort = null;
120 private IntSort m_intSort = null;
121 private RealSort m_realSort = null;
122 private SeqSort m_stringSort = null;
123
128 {
129 get
130 {
131 if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
132 }
133 }
134
139 {
140 get
141 {
142 if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
143 }
144 }
145
146
151 {
152 get
153 {
154 if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
155 }
156 }
157
162 {
163 get
164 {
165 if (m_stringSort == null) m_stringSort = new SeqSort(this, Native.Z3_mk_string_sort(nCtx));
166 return m_stringSort;
167 }
168 }
169
170
175 {
176 return new BoolSort(this);
177 }
178
183 {
184 Debug.Assert(s != null);
185
186 CheckContextMatch(s);
187 return new UninterpretedSort(this, s);
188 }
189
194 {
195
196 return MkUninterpretedSort(MkSymbol(str));
197 }
198
203 {
204
205 return new IntSort(this);
206 }
207
212 {
213 return new RealSort(this);
214 }
215
219 public BitVecSort MkBitVecSort(uint size)
220 {
221 return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
222 }
223
224
229 {
230 Debug.Assert(s != null);
231 return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
232 }
233
238 {
239 Debug.Assert(s != null);
240 return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
241 }
242
247 {
248 Debug.Assert(domain != null);
249 Debug.Assert(range != null);
250
251 CheckContextMatch(domain);
252 CheckContextMatch(range);
253 return new ArraySort(this, domain, range);
254 }
255
260 {
261 Debug.Assert(domain != null);
262 Debug.Assert(range != null);
263
264 CheckContextMatch<Sort>(domain);
265 CheckContextMatch(range);
266 return new ArraySort(this, domain, range);
267 }
268
272 public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
273 {
274 Debug.Assert(name != null);
275 Debug.Assert(fieldNames != null);
276 Debug.Assert(fieldNames.All(fn => fn != null));
277 Debug.Assert(fieldSorts == null || fieldSorts.All(fs => fs != null));
278
279 CheckContextMatch(name);
280 CheckContextMatch<Symbol>(fieldNames);
281 CheckContextMatch<Sort>(fieldSorts);
282 return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
283 }
284
288 public EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
289 {
290 Debug.Assert(name != null);
291 Debug.Assert(enumNames != null);
292 Debug.Assert(enumNames.All(f => f != null));
293
294
295 CheckContextMatch(name);
296 CheckContextMatch<Symbol>(enumNames);
297 return new EnumSort(this, name, enumNames);
298 }
299
303 public EnumSort MkEnumSort(string name, params string[] enumNames)
304 {
305 Debug.Assert(enumNames != null);
306
307 return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
308 }
309
313 public ListSort MkListSort(Symbol name, Sort elemSort)
314 {
315 Debug.Assert(name != null);
316 Debug.Assert(elemSort != null);
317
318 CheckContextMatch(name);
319 CheckContextMatch(elemSort);
320 return new ListSort(this, name, elemSort);
321 }
322
326 public ListSort MkListSort(string name, Sort elemSort)
327 {
328 Debug.Assert(elemSort != null);
329
330 CheckContextMatch(elemSort);
331 return new ListSort(this, MkSymbol(name), elemSort);
332 }
333
341 {
342 Debug.Assert(name != null);
343
344 CheckContextMatch(name);
345 return new FiniteDomainSort(this, name, size);
346 }
347
356 public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
357 {
358
359 return new FiniteDomainSort(this, MkSymbol(name), size);
360 }
361
362
363 #region Datatypes
374 public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
375 {
376 Debug.Assert(name != null);
377 Debug.Assert(recognizer != null);
378
379 return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
380 }
381
391 public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
392 {
393
394 return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
395 }
396
400 public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
401 {
402 Debug.Assert(name != null);
403 Debug.Assert(constructors != null);
404 Debug.Assert(constructors.All(c => c != null));
405
406
407 CheckContextMatch(name);
408 CheckContextMatch<Constructor>(constructors);
409 return new DatatypeSort(this, name, constructors);
410 }
411
415 public DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
416 {
417 Debug.Assert(constructors != null);
418 Debug.Assert(constructors.All(c => c != null));
419
420 CheckContextMatch<Constructor>(constructors);
421 return new DatatypeSort(this, MkSymbol(name), constructors);
422 }
423
430 {
431 Debug.Assert(names != null);
432 Debug.Assert(c != null);
433 Debug.Assert(names.Length == c.Length);
434 //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
435 Debug.Assert(names.All(name => name != null));
436
437 CheckContextMatch<Symbol>(names);
438 uint n = (uint)names.Length;
439 ConstructorList[] cla = new ConstructorList[n];
440 IntPtr[] n_constr = new IntPtr[n];
441 for (uint i = 0; i < n; i++)
442 {
443 Constructor[] constructor = c[i];
444 CheckContextMatch<Constructor>(constructor);
445 cla[i] = new ConstructorList(this, constructor);
446 n_constr[i] = cla[i].NativeObject;
447 }
448 IntPtr[] n_res = new IntPtr[n];
449 Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
450 DatatypeSort[] res = new DatatypeSort[n];
451 for (uint i = 0; i < n; i++)
452 res[i] = new DatatypeSort(this, n_res[i]);
453 return res;
454 }
455
462 public DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
463 {
464 Debug.Assert(names != null);
465 Debug.Assert(c != null);
466 Debug.Assert(names.Length == c.Length);
467 //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
468 //Debug.Assert(names.All(name => name != null));
469
470 return MkDatatypeSorts(MkSymbols(names), c);
471 }
472
479 public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
480 {
481 return Expr.Create(this, Native.Z3_datatype_update_field(
482 nCtx, field.NativeObject,
483 t.NativeObject, v.NativeObject));
484 }
485
486 #endregion
487 #endregion
488
489 #region Function Declarations
493 public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
494 {
495 Debug.Assert(name != null);
496 Debug.Assert(range != null);
497 Debug.Assert(domain.All(d => d != null));
498
499 CheckContextMatch(name);
500 CheckContextMatch<Sort>(domain);
501 CheckContextMatch(range);
502 return new FuncDecl(this, name, domain, range);
503 }
504
508 public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
509 {
510 Debug.Assert(name != null);
511 Debug.Assert(domain != null);
512 Debug.Assert(range != null);
513
514 CheckContextMatch(name);
515 CheckContextMatch(domain);
516 CheckContextMatch(range);
517 Sort[] q = new Sort[] { domain };
518 return new FuncDecl(this, name, q, range);
519 }
520
524 public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
525 {
526 Debug.Assert(range != null);
527 Debug.Assert(domain.All(d => d != null));
528
529 CheckContextMatch<Sort>(domain);
530 CheckContextMatch(range);
531 return new FuncDecl(this, MkSymbol(name), domain, range);
532 }
533
537 public FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
538 {
539 Debug.Assert(range != null);
540 Debug.Assert(domain.All(d => d != null));
541
542 CheckContextMatch<Sort>(domain);
543 CheckContextMatch(range);
544 return new FuncDecl(this, MkSymbol(name), domain, range, true);
545 }
546
553 public void AddRecDef(FuncDecl f, Expr[] args, Expr body)
554 {
555 CheckContextMatch(f);
556 CheckContextMatch<Expr>(args);
557 CheckContextMatch(body);
558 IntPtr[] argsNative = AST.ArrayToNative(args);
559 Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
560 }
561
565 public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
566 {
567 Debug.Assert(range != null);
568 Debug.Assert(domain != null);
569
570 CheckContextMatch(domain);
571 CheckContextMatch(range);
572 Sort[] q = new Sort[] { domain };
573 return new FuncDecl(this, MkSymbol(name), q, range);
574 }
575
581 public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
582 {
583 Debug.Assert(range != null);
584 Debug.Assert(domain.All(d => d != null));
585
586 CheckContextMatch<Sort>(domain);
587 CheckContextMatch(range);
588 return new FuncDecl(this, prefix, domain, range);
589 }
590
595 {
596 Debug.Assert(name != null);
597 Debug.Assert(range != null);
598
599 CheckContextMatch(name);
600 CheckContextMatch(range);
601 return new FuncDecl(this, name, null, range);
602 }
603
607 public FuncDecl MkConstDecl(string name, Sort range)
608 {
609 Debug.Assert(range != null);
610
611 CheckContextMatch(range);
612 return new FuncDecl(this, MkSymbol(name), null, range);
613 }
614
620 public FuncDecl MkFreshConstDecl(string prefix, Sort range)
621 {
622 Debug.Assert(range != null);
623
624 CheckContextMatch(range);
625 return new FuncDecl(this, prefix, null, range);
626 }
627 #endregion
628
629 #region Bound Variables
635 public Expr MkBound(uint index, Sort ty)
636 {
637 Debug.Assert(ty != null);
638
639 return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
640 }
641 #endregion
642
643 #region Quantifier Patterns
647 public Pattern MkPattern(params Expr[] terms)
648 {
649 Debug.Assert(terms != null);
650 if (terms.Length == 0)
651 throw new Z3Exception("Cannot create a pattern from zero terms");
652
653 IntPtr[] termsNative = AST.ArrayToNative(terms);
654 return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
655 }
656 #endregion
657
658 #region Constants
663 {
664 Debug.Assert(name != null);
665 Debug.Assert(range != null);
666
667 CheckContextMatch(name);
668 CheckContextMatch(range);
669
670 return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
671 }
672
676 public Expr MkConst(string name, Sort range)
677 {
678 Debug.Assert(range != null);
679
680 return MkConst(MkSymbol(name), range);
681 }
682
687 public Expr MkFreshConst(string prefix, Sort range)
688 {
689 Debug.Assert(range != null);
690
691 CheckContextMatch(range);
692 return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
693 }
694
700 {
701 Debug.Assert(f != null);
702
703 return MkApp(f);
704 }
705
710 {
711 Debug.Assert(name != null);
712
713 return (BoolExpr)MkConst(name, BoolSort);
714 }
715
719 public BoolExpr MkBoolConst(string name)
720 {
721
722 return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
723 }
724
729 {
730 Debug.Assert(name != null);
731
732 return (IntExpr)MkConst(name, IntSort);
733 }
734
738 public IntExpr MkIntConst(string name)
739 {
740 Debug.Assert(name != null);
741
742 return (IntExpr)MkConst(name, IntSort);
743 }
744
749 {
750 Debug.Assert(name != null);
751
752 return (RealExpr)MkConst(name, RealSort);
753 }
754
758 public RealExpr MkRealConst(string name)
759 {
760
761 return (RealExpr)MkConst(name, RealSort);
762 }
763
767 public BitVecExpr MkBVConst(Symbol name, uint size)
768 {
769 Debug.Assert(name != null);
770
771 return (BitVecExpr)MkConst(name, MkBitVecSort(size));
772 }
773
777 public BitVecExpr MkBVConst(string name, uint size)
778 {
779
780 return (BitVecExpr)MkConst(name, MkBitVecSort(size));
781 }
782 #endregion
783
784 #region Terms
788 public Expr MkApp(FuncDecl f, params Expr[] args)
789 {
790 Debug.Assert(f != null);
791 Debug.Assert(args == null || args.All(a => a != null));
792
793 CheckContextMatch(f);
794 CheckContextMatch<Expr>(args);
795 return Expr.Create(this, f, args);
796 }
797
801 public Expr MkApp(FuncDecl f, IEnumerable<Expr> args)
802 {
803 Debug.Assert(f != null);
804 Debug.Assert(args == null || args.All( a => a != null));
805
806 CheckContextMatch(f);
807 CheckContextMatch(args);
808 return Expr.Create(this, f, args.ToArray());
809 }
810
811 #region Propositional
816 {
817
818 return new BoolExpr(this, Native.Z3_mk_true(nCtx));
819 }
820
825 {
826
827 return new BoolExpr(this, Native.Z3_mk_false(nCtx));
828 }
829
833 public BoolExpr MkBool(bool value)
834 {
835
836 return value ? MkTrue() : MkFalse();
837 }
838
842 public BoolExpr MkEq(Expr x, Expr y)
843 {
844 Debug.Assert(x != null);
845 Debug.Assert(y != null);
846
847 CheckContextMatch(x);
848 CheckContextMatch(y);
849 return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
850 }
851
855 public BoolExpr MkDistinct(params Expr[] args)
856 {
857 Debug.Assert(args != null);
858 Debug.Assert(args.All(a => a != null));
859
860
861 CheckContextMatch<Expr>(args);
862 return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
863 }
864
869 {
870 Debug.Assert(a != null);
871
872 CheckContextMatch(a);
873 return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
874 }
875
882 public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
883 {
884 Debug.Assert(t1 != null);
885 Debug.Assert(t2 != null);
886 Debug.Assert(t3 != null);
887
888 CheckContextMatch(t1);
889 CheckContextMatch(t2);
890 CheckContextMatch(t3);
891 return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
892 }
893
898 {
899 Debug.Assert(t1 != null);
900 Debug.Assert(t2 != null);
901
902 CheckContextMatch(t1);
903 CheckContextMatch(t2);
904 return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
905 }
906
911 {
912 Debug.Assert(t1 != null);
913 Debug.Assert(t2 != null);
914
915 CheckContextMatch(t1);
916 CheckContextMatch(t2);
917 return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
918 }
919
924 {
925 Debug.Assert(t1 != null);
926 Debug.Assert(t2 != null);
927
928 CheckContextMatch(t1);
929 CheckContextMatch(t2);
930 return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
931 }
932
936 public BoolExpr MkXor(IEnumerable<BoolExpr> ts)
937 {
938 Debug.Assert(ts != null);
939 Debug.Assert(ts.All(a => a != null));
940 CheckContextMatch<BoolExpr>(ts);
941 BoolExpr r = null;
942 foreach (var t in ts) {
943 if (r == null)
944 r = t;
945 else
946 r = MkXor(r, t);
947 }
948 if (r == null)
949 r = MkTrue();
950 return r;
951 }
952
956 public BoolExpr MkAnd(params BoolExpr[] t)
957 {
958 Debug.Assert(t != null);
959 Debug.Assert(t.All(a => a != null));
960
961 CheckContextMatch<BoolExpr>(t);
962 return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
963 }
964
968 public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
969 {
970 Debug.Assert(t != null);
971 Debug.Assert(t.All(a => a != null));
972 CheckContextMatch<BoolExpr>(t);
973 return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
974 }
975
979 public BoolExpr MkOr(params BoolExpr[] t)
980 {
981 Debug.Assert(t != null);
982 Debug.Assert(t.All(a => a != null));
983
984 CheckContextMatch<BoolExpr>(t);
985 return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
986 }
987
988
992 public BoolExpr MkOr(IEnumerable<BoolExpr> t)
993 {
994 Debug.Assert(t != null);
995 Debug.Assert(t.All(a => a != null));
996
997 CheckContextMatch(t);
998 return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
999 }
1000
1001 #endregion
1002
1003 #region Arithmetic
1007 public ArithExpr MkAdd(params ArithExpr[] t)
1008 {
1009 Debug.Assert(t != null);
1010 Debug.Assert(t.All(a => a != null));
1011
1012 CheckContextMatch<ArithExpr>(t);
1013 return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1014 }
1015
1019 public ArithExpr MkAdd(IEnumerable<ArithExpr> t)
1020 {
1021 Debug.Assert(t != null);
1022 Debug.Assert(t.All(a => a != null));
1023
1024 CheckContextMatch(t);
1025 return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
1026 }
1027
1031 public ArithExpr MkMul(params ArithExpr[] t)
1032 {
1033 Debug.Assert(t != null);
1034 Debug.Assert(t.All(a => a != null));
1035
1036 CheckContextMatch<ArithExpr>(t);
1037 return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1038 }
1039
1043 public ArithExpr MkMul(IEnumerable<ArithExpr> t)
1044 {
1045 Debug.Assert(t != null);
1046 Debug.Assert(t.All(a => a != null));
1047
1048 CheckContextMatch<ArithExpr>(t);
1049 return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
1050 }
1051
1055 public ArithExpr MkSub(params ArithExpr[] t)
1056 {
1057 Debug.Assert(t != null);
1058 Debug.Assert(t.All(a => a != null));
1059
1060 CheckContextMatch<ArithExpr>(t);
1061 return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1062 }
1063
1068 {
1069 Debug.Assert(t != null);
1070
1071 CheckContextMatch(t);
1072 return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
1073 }
1074
1079 {
1080 Debug.Assert(t1 != null);
1081 Debug.Assert(t2 != null);
1082
1083 CheckContextMatch(t1);
1084 CheckContextMatch(t2);
1085 return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1086 }
1087
1093 {
1094 Debug.Assert(t1 != null);
1095 Debug.Assert(t2 != null);
1096
1097 CheckContextMatch(t1);
1098 CheckContextMatch(t2);
1099 return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1100 }
1101
1107 {
1108 Debug.Assert(t1 != null);
1109 Debug.Assert(t2 != null);
1110
1111 CheckContextMatch(t1);
1112 CheckContextMatch(t2);
1113 return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1114 }
1115
1120 {
1121 Debug.Assert(t1 != null);
1122 Debug.Assert(t2 != null);
1123
1124 CheckContextMatch(t1);
1125 CheckContextMatch(t2);
1126 return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1127 }
1128
1133 {
1134 Debug.Assert(t1 != null);
1135 Debug.Assert(t2 != null);
1136
1137 CheckContextMatch(t1);
1138 CheckContextMatch(t2);
1139 return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1140 }
1141
1146 {
1147 Debug.Assert(t1 != null);
1148 Debug.Assert(t2 != null);
1149
1150 CheckContextMatch(t1);
1151 CheckContextMatch(t2);
1152 return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1153 }
1154
1159 {
1160 Debug.Assert(t1 != null);
1161 Debug.Assert(t2 != null);
1162
1163 CheckContextMatch(t1);
1164 CheckContextMatch(t2);
1165 return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1166 }
1167
1172 {
1173 Debug.Assert(t1 != null);
1174 Debug.Assert(t2 != null);
1175
1176 CheckContextMatch(t1);
1177 CheckContextMatch(t2);
1178 return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1179 }
1180
1192 {
1193 Debug.Assert(t != null);
1194
1195 CheckContextMatch(t);
1196 return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1197 }
1198
1207 {
1208 Debug.Assert(t != null);
1209
1210 CheckContextMatch(t);
1211 return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1212 }
1213
1218 {
1219 Debug.Assert(t != null);
1220
1221 CheckContextMatch(t);
1222 return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1223 }
1224 #endregion
1225
1226 #region Bit-vectors
1232 {
1233 Debug.Assert(t != null);
1234
1235 CheckContextMatch(t);
1236 return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1237 }
1238
1244 {
1245 Debug.Assert(t != null);
1246
1247 CheckContextMatch(t);
1248 return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1249 }
1250
1256 {
1257 Debug.Assert(t != null);
1258
1259 CheckContextMatch(t);
1260 return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1261 }
1262
1268 {
1269 Debug.Assert(t1 != null);
1270 Debug.Assert(t2 != null);
1271
1272 CheckContextMatch(t1);
1273 CheckContextMatch(t2);
1274 return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1275 }
1276
1282 {
1283 Debug.Assert(t1 != null);
1284 Debug.Assert(t2 != null);
1285
1286 CheckContextMatch(t1);
1287 CheckContextMatch(t2);
1288 return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1289 }
1290
1296 {
1297 Debug.Assert(t1 != null);
1298 Debug.Assert(t2 != null);
1299
1300 CheckContextMatch(t1);
1301 CheckContextMatch(t2);
1302 return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1303 }
1304
1310 {
1311 Debug.Assert(t1 != null);
1312 Debug.Assert(t2 != null);
1313
1314 CheckContextMatch(t1);
1315 CheckContextMatch(t2);
1316 return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1317 }
1318
1324 {
1325 Debug.Assert(t1 != null);
1326 Debug.Assert(t2 != null);
1327
1328 CheckContextMatch(t1);
1329 CheckContextMatch(t2);
1330 return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1331 }
1332
1338 {
1339 Debug.Assert(t1 != null);
1340 Debug.Assert(t2 != null);
1341
1342 CheckContextMatch(t1);
1343 CheckContextMatch(t2);
1344 return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1345 }
1346
1352 {
1353 Debug.Assert(t != null);
1354
1355 CheckContextMatch(t);
1356 return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1357 }
1358
1364 {
1365 Debug.Assert(t1 != null);
1366 Debug.Assert(t2 != null);
1367
1368 CheckContextMatch(t1);
1369 CheckContextMatch(t2);
1370 return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1371 }
1372
1378 {
1379 Debug.Assert(t1 != null);
1380 Debug.Assert(t2 != null);
1381
1382 CheckContextMatch(t1);
1383 CheckContextMatch(t2);
1384 return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1385 }
1386
1392 {
1393 Debug.Assert(t1 != null);
1394 Debug.Assert(t2 != null);
1395
1396 CheckContextMatch(t1);
1397 CheckContextMatch(t2);
1398 return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1399 }
1400
1411 {
1412 Debug.Assert(t1 != null);
1413 Debug.Assert(t2 != null);
1414
1415 CheckContextMatch(t1);
1416 CheckContextMatch(t2);
1417 return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1418 }
1419
1434 {
1435 Debug.Assert(t1 != null);
1436 Debug.Assert(t2 != null);
1437
1438 CheckContextMatch(t1);
1439 CheckContextMatch(t2);
1440 return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1441 }
1442
1452 {
1453 Debug.Assert(t1 != null);
1454 Debug.Assert(t2 != null);
1455
1456 CheckContextMatch(t1);
1457 CheckContextMatch(t2);
1458 return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1459 }
1460
1472 {
1473 Debug.Assert(t1 != null);
1474 Debug.Assert(t2 != null);
1475
1476 CheckContextMatch(t1);
1477 CheckContextMatch(t2);
1478 return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1479 }
1480
1489 {
1490 Debug.Assert(t1 != null);
1491 Debug.Assert(t2 != null);
1492
1493 CheckContextMatch(t1);
1494 CheckContextMatch(t2);
1495 return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1496 }
1497
1505 {
1506 Debug.Assert(t1 != null);
1507 Debug.Assert(t2 != null);
1508
1509 CheckContextMatch(t1);
1510 CheckContextMatch(t2);
1511 return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1512 }
1513
1521 {
1522 Debug.Assert(t1 != null);
1523 Debug.Assert(t2 != null);
1524
1525 CheckContextMatch(t1);
1526 CheckContextMatch(t2);
1527 return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1528 }
1529
1537 {
1538 Debug.Assert(t1 != null);
1539 Debug.Assert(t2 != null);
1540
1541 CheckContextMatch(t1);
1542 CheckContextMatch(t2);
1543 return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1544 }
1545
1553 {
1554 Debug.Assert(t1 != null);
1555 Debug.Assert(t2 != null);
1556
1557 CheckContextMatch(t1);
1558 CheckContextMatch(t2);
1559 return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1560 }
1561
1569 {
1570 Debug.Assert(t1 != null);
1571 Debug.Assert(t2 != null);
1572
1573 CheckContextMatch(t1);
1574 CheckContextMatch(t2);
1575 return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1576 }
1577
1585 {
1586 Debug.Assert(t1 != null);
1587 Debug.Assert(t2 != null);
1588
1589 CheckContextMatch(t1);
1590 CheckContextMatch(t2);
1591 return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1592 }
1593
1601 {
1602 Debug.Assert(t1 != null);
1603 Debug.Assert(t2 != null);
1604
1605 CheckContextMatch(t1);
1606 CheckContextMatch(t2);
1607 return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1608 }
1609
1617 {
1618 Debug.Assert(t1 != null);
1619 Debug.Assert(t2 != null);
1620
1621 CheckContextMatch(t1);
1622 CheckContextMatch(t2);
1623 return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1624 }
1625
1637 {
1638 Debug.Assert(t1 != null);
1639 Debug.Assert(t2 != null);
1640
1641 CheckContextMatch(t1);
1642 CheckContextMatch(t2);
1643 return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1644 }
1645
1655 public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
1656 {
1657 Debug.Assert(t != null);
1658
1659 CheckContextMatch(t);
1660 return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1661 }
1662
1672 {
1673 Debug.Assert(t != null);
1674
1675 CheckContextMatch(t);
1676 return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1677 }
1678
1689 {
1690 Debug.Assert(t != null);
1691
1692 CheckContextMatch(t);
1693 return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1694 }
1695
1703 {
1704 Debug.Assert(t != null);
1705
1706 CheckContextMatch(t);
1707 return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1708 }
1709
1723 {
1724 Debug.Assert(t1 != null);
1725 Debug.Assert(t2 != null);
1726
1727 CheckContextMatch(t1);
1728 CheckContextMatch(t2);
1729 return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1730 }
1731
1745 {
1746 Debug.Assert(t1 != null);
1747 Debug.Assert(t2 != null);
1748
1749 CheckContextMatch(t1);
1750 CheckContextMatch(t2);
1751 return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1752 }
1753
1769 {
1770 Debug.Assert(t1 != null);
1771 Debug.Assert(t2 != null);
1772
1773 CheckContextMatch(t1);
1774 CheckContextMatch(t2);
1775 return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1776 }
1777
1786 {
1787 Debug.Assert(t != null);
1788
1789 CheckContextMatch(t);
1790 return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1791 }
1792
1801 {
1802 Debug.Assert(t != null);
1803
1804 CheckContextMatch(t);
1805 return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1806 }
1807
1816 {
1817 Debug.Assert(t1 != null);
1818 Debug.Assert(t2 != null);
1819
1820 CheckContextMatch(t1);
1821 CheckContextMatch(t2);
1822 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1823 }
1824
1833 {
1834 Debug.Assert(t1 != null);
1835 Debug.Assert(t2 != null);
1836
1837 CheckContextMatch(t1);
1838 CheckContextMatch(t2);
1839 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1840 }
1841
1852 public BitVecExpr MkInt2BV(uint n, IntExpr t)
1853 {
1854 Debug.Assert(t != null);
1855
1856 CheckContextMatch(t);
1857 return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1858 }
1859
1875 public IntExpr MkBV2Int(BitVecExpr t, bool signed)
1876 {
1877 Debug.Assert(t != null);
1878
1879 CheckContextMatch(t);
1880 return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (byte)(signed ? 1 : 0)));
1881 }
1882
1889 public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1890 {
1891 Debug.Assert(t1 != null);
1892 Debug.Assert(t2 != null);
1893
1894 CheckContextMatch(t1);
1895 CheckContextMatch(t2);
1896 return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
1897 }
1898
1906 {
1907 Debug.Assert(t1 != null);
1908 Debug.Assert(t2 != null);
1909
1910 CheckContextMatch(t1);
1911 CheckContextMatch(t2);
1912 return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1913 }
1914
1922 {
1923 Debug.Assert(t1 != null);
1924 Debug.Assert(t2 != null);
1925
1926 CheckContextMatch(t1);
1927 CheckContextMatch(t2);
1928 return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1929 }
1930
1937 public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1938 {
1939 Debug.Assert(t1 != null);
1940 Debug.Assert(t2 != null);
1941
1942 CheckContextMatch(t1);
1943 CheckContextMatch(t2);
1944 return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
1945 }
1946
1954 {
1955 Debug.Assert(t1 != null);
1956 Debug.Assert(t2 != null);
1957
1958 CheckContextMatch(t1);
1959 CheckContextMatch(t2);
1960 return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1961 }
1962
1970 {
1971 Debug.Assert(t != null);
1972
1973 CheckContextMatch(t);
1974 return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
1975 }
1976
1983 public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1984 {
1985 Debug.Assert(t1 != null);
1986 Debug.Assert(t2 != null);
1987
1988 CheckContextMatch(t1);
1989 CheckContextMatch(t2);
1990 return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
1991 }
1992
2000 {
2001 Debug.Assert(t1 != null);
2002 Debug.Assert(t2 != null);
2003
2004 CheckContextMatch(t1);
2005 CheckContextMatch(t2);
2006 return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2007 }
2008 #endregion
2009
2010 #region Arrays
2015 {
2016 Debug.Assert(name != null);
2017 Debug.Assert(domain != null);
2018 Debug.Assert(range != null);
2019
2020 return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
2021 }
2022
2026 public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
2027 {
2028 Debug.Assert(domain != null);
2029 Debug.Assert(range != null);
2030
2031 return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
2032 }
2033
2034
2049 {
2050 Debug.Assert(a != null);
2051 Debug.Assert(i != null);
2052
2053 CheckContextMatch(a);
2054 CheckContextMatch(i);
2055 return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2056 }
2057
2071 public Expr MkSelect(ArrayExpr a, params Expr[] args)
2072 {
2073 Debug.Assert(a != null);
2074 Debug.Assert(args != null && args.All(n => n != null));
2075
2076 CheckContextMatch(a);
2077 CheckContextMatch<Expr>(args);
2078 return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2079 }
2080
2081
2101 {
2102 Debug.Assert(a != null);
2103 Debug.Assert(i != null);
2104 Debug.Assert(v != null);
2105
2106 CheckContextMatch(a);
2107 CheckContextMatch(i);
2108 CheckContextMatch(v);
2109 return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2110 }
2111
2130 public ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
2131 {
2132 Debug.Assert(a != null);
2133 Debug.Assert(args != null);
2134 Debug.Assert(v != null);
2135
2136 CheckContextMatch<Expr>(args);
2137 CheckContextMatch(a);
2138 CheckContextMatch(v);
2139 return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
2140 }
2141
2152 {
2153 Debug.Assert(domain != null);
2154 Debug.Assert(v != null);
2155
2156 CheckContextMatch(domain);
2157 CheckContextMatch(v);
2158 return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2159 }
2160
2172 public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
2173 {
2174 Debug.Assert(f != null);
2175 Debug.Assert(args == null || args.All(a => a != null));
2176
2177 CheckContextMatch(f);
2178 CheckContextMatch<ArrayExpr>(args);
2179 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2180 }
2181
2190 {
2191 Debug.Assert(array != null);
2192
2193 CheckContextMatch(array);
2194 return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2195 }
2196
2201 {
2202 Debug.Assert(arg1 != null);
2203 Debug.Assert(arg2 != null);
2204
2205 CheckContextMatch(arg1);
2206 CheckContextMatch(arg2);
2207 return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
2208 }
2209
2210 #endregion
2211
2212 #region Sets
2217 {
2218 Debug.Assert(ty != null);
2219
2220 CheckContextMatch(ty);
2221 return new SetSort(this, ty);
2222 }
2223
2228 {
2229 Debug.Assert(domain != null);
2230
2231 CheckContextMatch(domain);
2232 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2233 }
2234
2238 public ArrayExpr MkFullSet(Sort domain)
2239 {
2240 Debug.Assert(domain != null);
2241
2242 CheckContextMatch(domain);
2243 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2244 }
2245
2249 public ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
2250 {
2251 Debug.Assert(set != null);
2252 Debug.Assert(element != null);
2253
2254 CheckContextMatch(set);
2255 CheckContextMatch(element);
2256 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2257 }
2258
2259
2263 public ArrayExpr MkSetDel(ArrayExpr set, Expr element)
2264 {
2265 Debug.Assert(set != null);
2266 Debug.Assert(element != null);
2267
2268 CheckContextMatch(set);
2269 CheckContextMatch(element);
2270 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2271 }
2272
2276 public ArrayExpr MkSetUnion(params ArrayExpr[] args)
2277 {
2278 Debug.Assert(args != null);
2279 Debug.Assert(args.All(a => a != null));
2280
2281 CheckContextMatch<ArrayExpr>(args);
2282 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2283 }
2284
2289 {
2290 Debug.Assert(args != null);
2291 Debug.Assert(args.All(a => a != null));
2292
2293 CheckContextMatch<ArrayExpr>(args);
2294 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2295 }
2296
2301 {
2302 Debug.Assert(arg1 != null);
2303 Debug.Assert(arg2 != null);
2304
2305 CheckContextMatch(arg1);
2306 CheckContextMatch(arg2);
2307 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2308 }
2309
2314 {
2315 Debug.Assert(arg != null);
2316
2317 CheckContextMatch(arg);
2318 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2319 }
2320
2325 {
2326 Debug.Assert(elem != null);
2327 Debug.Assert(set != null);
2328
2329 CheckContextMatch(elem);
2330 CheckContextMatch(set);
2331 return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2332 }
2333
2338 {
2339 Debug.Assert(arg1 != null);
2340 Debug.Assert(arg2 != null);
2341
2342 CheckContextMatch(arg1);
2343 CheckContextMatch(arg2);
2344 return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2345 }
2346
2347 #endregion
2348
2349 #region Sequence, string and regular expressions
2350
2355 {
2356 Debug.Assert(s != null);
2357 return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
2358 }
2359
2363 public SeqExpr MkUnit(Expr elem)
2364 {
2365 Debug.Assert(elem != null);
2366 return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
2367 }
2368
2372 public SeqExpr MkString(string s)
2373 {
2374 Debug.Assert(s != null);
2375 return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
2376 }
2377
2382 {
2383 Debug.Assert(e != null);
2384 Debug.Assert(e is ArithExpr);
2385 return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
2386 }
2387
2392 {
2393 Debug.Assert(e != null);
2394 Debug.Assert(e is SeqExpr);
2395 return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject));
2396 }
2397
2398
2402 public SeqExpr MkConcat(params SeqExpr[] t)
2403 {
2404 Debug.Assert(t != null);
2405 Debug.Assert(t.All(a => a != null));
2406
2407 CheckContextMatch<SeqExpr>(t);
2408 return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2409 }
2410
2411
2416 {
2417 Debug.Assert(s != null);
2418 return (IntExpr) Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
2419 }
2420
2425 {
2426 Debug.Assert(s1 != null);
2427 Debug.Assert(s2 != null);
2428 CheckContextMatch(s1, s2);
2429 return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
2430 }
2431
2436 {
2437 Debug.Assert(s1 != null);
2438 Debug.Assert(s2 != null);
2439 CheckContextMatch(s1, s2);
2440 return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
2441 }
2442
2447 {
2448 Debug.Assert(s1 != null);
2449 Debug.Assert(s2 != null);
2450 CheckContextMatch(s1, s2);
2451 return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
2452 }
2453
2458 {
2459 Debug.Assert(s1 != null);
2460 Debug.Assert(s2 != null);
2461 CheckContextMatch(s1, s2);
2462 return new BoolExpr(this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject));
2463 }
2464
2469 {
2470 Debug.Assert(s1 != null);
2471 Debug.Assert(s2 != null);
2472 CheckContextMatch(s1, s2);
2473 return new BoolExpr(this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject));
2474 }
2475
2479 public SeqExpr MkAt(SeqExpr s, Expr index)
2480 {
2481 Debug.Assert(s != null);
2482 Debug.Assert(index != null);
2483 CheckContextMatch(s, index);
2484 return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
2485 }
2486
2490 public Expr MkNth(SeqExpr s, Expr index)
2491 {
2492 Debug.Assert(s != null);
2493 Debug.Assert(index != null);
2494 CheckContextMatch(s, index);
2495 return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
2496 }
2497
2501 public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
2502 {
2503 Debug.Assert(s != null);
2504 Debug.Assert(offset != null);
2505 Debug.Assert(length != null);
2506 CheckContextMatch(s, offset, length);
2507 return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
2508 }
2509
2513 public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
2514 {
2515 Debug.Assert(s != null);
2516 Debug.Assert(offset != null);
2517 Debug.Assert(substr != null);
2518 CheckContextMatch(s, substr, offset);
2519 return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
2520 }
2521
2526 {
2527 Debug.Assert(s != null);
2528 Debug.Assert(src != null);
2529 Debug.Assert(dst != null);
2530 CheckContextMatch(s, src, dst);
2531 return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
2532 }
2533
2538 {
2539 Debug.Assert(s != null);
2540 return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));
2541 }
2542
2543
2548 {
2549 Debug.Assert(s != null);
2550 Debug.Assert(re != null);
2551 CheckContextMatch(s, re);
2552 return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
2553 }
2554
2559 {
2560 Debug.Assert(re != null);
2561 return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
2562 }
2563
2567 public ReExpr MkLoop(ReExpr re, uint lo, uint hi = 0)
2568 {
2569 Debug.Assert(re != null);
2570 return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi));
2571 }
2572
2577 {
2578 Debug.Assert(re != null);
2579 return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));
2580 }
2581
2586 {
2587 Debug.Assert(re != null);
2588 return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
2589 }
2590
2595 {
2596 Debug.Assert(re != null);
2597 return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject));
2598 }
2599
2603 public ReExpr MkConcat(params ReExpr[] t)
2604 {
2605 Debug.Assert(t != null);
2606 Debug.Assert(t.All(a => a != null));
2607
2608 CheckContextMatch<ReExpr>(t);
2609 return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2610 }
2611
2615 public ReExpr MkUnion(params ReExpr[] t)
2616 {
2617 Debug.Assert(t != null);
2618 Debug.Assert(t.All(a => a != null));
2619
2620 CheckContextMatch<ReExpr>(t);
2621 return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2622 }
2623
2627 public ReExpr MkIntersect(params ReExpr[] t)
2628 {
2629 Debug.Assert(t != null);
2630 Debug.Assert(t.All(a => a != null));
2631
2632 CheckContextMatch<ReExpr>(t);
2633 return new ReExpr(this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2634 }
2635
2641 {
2642 Debug.Assert(s != null);
2643 return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject));
2644 }
2645
2651 {
2652 Debug.Assert(s != null);
2653 return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject));
2654 }
2655
2656
2661 {
2662 Debug.Assert(lo != null);
2663 Debug.Assert(hi != null);
2664 CheckContextMatch(lo, hi);
2665 return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
2666 }
2667
2668 #endregion
2669
2670 #region Pseudo-Boolean constraints
2671
2675 public BoolExpr MkAtMost(IEnumerable<BoolExpr> args, uint k)
2676 {
2677 Debug.Assert(args != null);
2678 CheckContextMatch<BoolExpr>(args);
2679 return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Count(),
2680 AST.EnumToNative(args), k));
2681 }
2682
2686 public BoolExpr MkAtLeast(IEnumerable<BoolExpr> args, uint k)
2687 {
2688 Debug.Assert(args != null);
2689 CheckContextMatch<BoolExpr>(args);
2690 return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) args.Count(),
2691 AST.EnumToNative(args), k));
2692 }
2693
2697 public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
2698 {
2699 Debug.Assert(args != null);
2700 Debug.Assert(coeffs != null);
2701 Debug.Assert(args.Length == coeffs.Length);
2702 CheckContextMatch<BoolExpr>(args);
2703 return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
2704 AST.ArrayToNative(args),
2705 coeffs, k));
2706 }
2707
2711 public BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k)
2712 {
2713 Debug.Assert(args != null);
2714 Debug.Assert(coeffs != null);
2715 Debug.Assert(args.Length == coeffs.Length);
2716 CheckContextMatch<BoolExpr>(args);
2717 return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint) args.Length,
2718 AST.ArrayToNative(args),
2719 coeffs, k));
2720 }
2724 public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
2725 {
2726 Debug.Assert(args != null);
2727 Debug.Assert(coeffs != null);
2728 Debug.Assert(args.Length == coeffs.Length);
2729 CheckContextMatch<BoolExpr>(args);
2730 return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length,
2731 AST.ArrayToNative(args),
2732 coeffs, k));
2733 }
2734 #endregion
2735
2736 #region Numerals
2737
2738 #region General Numerals
2745 public Expr MkNumeral(string v, Sort ty)
2746 {
2747 Debug.Assert(ty != null);
2748
2749 CheckContextMatch(ty);
2750 return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2751 }
2752
2760 public Expr MkNumeral(int v, Sort ty)
2761 {
2762 Debug.Assert(ty != null);
2763
2764 CheckContextMatch(ty);
2765 return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2766 }
2767
2775 public Expr MkNumeral(uint v, Sort ty)
2776 {
2777 Debug.Assert(ty != null);
2778
2779 CheckContextMatch(ty);
2780 return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2781 }
2782
2790 public Expr MkNumeral(long v, Sort ty)
2791 {
2792 Debug.Assert(ty != null);
2793
2794 CheckContextMatch(ty);
2795 return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2796 }
2797
2805 public Expr MkNumeral(ulong v, Sort ty)
2806 {
2807 Debug.Assert(ty != null);
2808
2809 CheckContextMatch(ty);
2810 return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2811 }
2812 #endregion
2813
2814 #region Reals
2822 public RatNum MkReal(int num, int den)
2823 {
2824 if (den == 0)
2825 throw new Z3Exception("Denominator is zero");
2826
2827 return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
2828 }
2829
2835 public RatNum MkReal(string v)
2836 {
2837
2838 return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
2839 }
2840
2846 public RatNum MkReal(int v)
2847 {
2848
2849 return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
2850 }
2851
2857 public RatNum MkReal(uint v)
2858 {
2859
2860 return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
2861 }
2862
2868 public RatNum MkReal(long v)
2869 {
2870
2871 return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
2872 }
2873
2879 public RatNum MkReal(ulong v)
2880 {
2881
2882 return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
2883 }
2884 #endregion
2885
2886 #region Integers
2891 public IntNum MkInt(string v)
2892 {
2893
2894 return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
2895 }
2896
2902 public IntNum MkInt(int v)
2903 {
2904
2905 return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
2906 }
2907
2913 public IntNum MkInt(uint v)
2914 {
2915
2916 return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
2917 }
2918
2924 public IntNum MkInt(long v)
2925 {
2926
2927 return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
2928 }
2929
2935 public IntNum MkInt(ulong v)
2936 {
2937
2938 return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
2939 }
2940 #endregion
2941
2942 #region Bit-vectors
2948 public BitVecNum MkBV(string v, uint size)
2949 {
2950
2951 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2952 }
2953
2959 public BitVecNum MkBV(int v, uint size)
2960 {
2961
2962 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2963 }
2964
2970 public BitVecNum MkBV(uint v, uint size)
2971 {
2972
2973 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2974 }
2975
2981 public BitVecNum MkBV(long v, uint size)
2982 {
2983
2984 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2985 }
2986
2992 public BitVecNum MkBV(ulong v, uint size)
2993 {
2994
2995 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2996 }
2997
3002 public BitVecNum MkBV(bool[] bits)
3003 {
3004 byte[] _bits = new byte[bits.Length];
3005 for (int i = 0; i < bits.Length; ++i) _bits[i] = (byte)(bits[i] ? 1 : 0);
3006 return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
3007 }
3008
3009
3010 #endregion
3011
3012 #endregion // Numerals
3013
3014 #region Quantifiers
3039 public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3040 {
3041 Debug.Assert(sorts != null);
3042 Debug.Assert(names != null);
3043 Debug.Assert(body != null);
3044 Debug.Assert(sorts.Length == names.Length);
3045 Debug.Assert(sorts.All(s => s != null));
3046 Debug.Assert(names.All(n => n != null));
3047 Debug.Assert(patterns == null || patterns.All(p => p != null));
3048 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3049
3050
3051 return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3052 }
3053
3054
3063 public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3064 {
3065 Debug.Assert(body != null);
3066 Debug.Assert(boundConstants == null || boundConstants.All(b => b != null));
3067 Debug.Assert(patterns == null || patterns.All(p => p != null));
3068 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3069
3070
3071 return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3072 }
3073
3081 public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3082 {
3083 Debug.Assert(sorts != null);
3084 Debug.Assert(names != null);
3085 Debug.Assert(body != null);
3086 Debug.Assert(sorts.Length == names.Length);
3087 Debug.Assert(sorts.All(s => s != null));
3088 Debug.Assert(names.All(n => n != null));
3089 Debug.Assert(patterns == null || patterns.All(p => p != null));
3090 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3091
3092 return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3093 }
3094
3103 public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3104 {
3105 Debug.Assert(body != null);
3106 Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3107 Debug.Assert(patterns == null || patterns.All(p => p != null));
3108 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3109
3110 return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3111 }
3112
3113
3118 public 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)
3119 {
3120 Debug.Assert(body != null);
3121 Debug.Assert(names != null);
3122 Debug.Assert(sorts != null);
3123 Debug.Assert(sorts.Length == names.Length);
3124 Debug.Assert(sorts.All(s => s != null));
3125 Debug.Assert(names.All(n => n != null));
3126 Debug.Assert(patterns == null || patterns.All(p => p != null));
3127 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3128
3129
3130 if (universal)
3131 return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3132 else
3133 return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3134 }
3135
3136
3141 public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3142 {
3143 Debug.Assert(body != null);
3144 Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3145 Debug.Assert(patterns == null || patterns.All(p => p != null));
3146 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3147
3148
3149 if (universal)
3150 return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3151 else
3152 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3153 }
3154
3173 public Lambda MkLambda(Sort[] sorts, Symbol[] names, Expr body)
3174 {
3175 Debug.Assert(sorts != null);
3176 Debug.Assert(names != null);
3177 Debug.Assert(body != null);
3178 Debug.Assert(sorts.Length == names.Length);
3179 Debug.Assert(sorts.All(s => s != null));
3180 Debug.Assert(names.All(n => n != null));
3181 return new Lambda(this, sorts, names, body);
3182 }
3183
3192 public Lambda MkLambda(Expr[] boundConstants, Expr body)
3193 {
3194 Debug.Assert(body != null);
3195 Debug.Assert(boundConstants != null && boundConstants.All(b => b != null));
3196 return new Lambda(this, boundConstants, body);
3197 }
3198
3199
3200 #endregion
3201
3202 #endregion // Expr
3203
3204 #region Options
3222 {
3223 set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
3224 }
3225 #endregion
3226
3227 #region SMT Files & Strings
3228
3233 public BoolExpr[] ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
3234 {
3235
3236 uint csn = Symbol.ArrayLength(sortNames);
3237 uint cs = Sort.ArrayLength(sorts);
3238 uint cdn = Symbol.ArrayLength(declNames);
3239 uint cd = AST.ArrayLength(decls);
3240 if (csn != cs || cdn != cd)
3241 throw new Z3Exception("Argument size mismatch");
3242 ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str,
3243 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3244 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3245 return assertions.ToBoolExprArray();
3246 }
3247
3252 public BoolExpr[] ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
3253 {
3254
3255 uint csn = Symbol.ArrayLength(sortNames);
3256 uint cs = Sort.ArrayLength(sorts);
3257 uint cdn = Symbol.ArrayLength(declNames);
3258 uint cd = AST.ArrayLength(decls);
3259 if (csn != cs || cdn != cd)
3260 throw new Z3Exception("Argument size mismatch");
3261 ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
3262 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3263 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3264 return assertions.ToBoolExprArray();
3265 }
3266 #endregion
3267
3268 #region Goals
3279 public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
3280 {
3281
3282 return new Goal(this, models, unsatCores, proofs);
3283 }
3284 #endregion
3285
3286 #region ParameterSets
3291 {
3292
3293 return new Params(this);
3294 }
3295 #endregion
3296
3297 #region Tactics
3301 public uint NumTactics
3302 {
3303 get { return Native.Z3_get_num_tactics(nCtx); }
3304 }
3305
3309 public string[] TacticNames
3310 {
3311 get
3312 {
3313
3314 uint n = NumTactics;
3315 string[] res = new string[n];
3316 for (uint i = 0; i < n; i++)
3317 res[i] = Native.Z3_get_tactic_name(nCtx, i);
3318 return res;
3319 }
3320 }
3321
3325 public string TacticDescription(string name)
3326 {
3327
3328 return Native.Z3_tactic_get_descr(nCtx, name);
3329 }
3330
3334 public Tactic MkTactic(string name)
3335 {
3336
3337 return new Tactic(this, name);
3338 }
3339
3344 public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
3345 {
3346 Debug.Assert(t1 != null);
3347 Debug.Assert(t2 != null);
3348 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3349
3350
3351 CheckContextMatch(t1);
3352 CheckContextMatch(t2);
3353 CheckContextMatch<Tactic>(ts);
3354
3355 IntPtr last = IntPtr.Zero;
3356 if (ts != null && ts.Length > 0)
3357 {
3358 last = ts[ts.Length - 1].NativeObject;
3359 for (int i = ts.Length - 2; i >= 0; i--)
3360 last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3361 }
3362 if (last != IntPtr.Zero)
3363 {
3364 last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3365 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3366 }
3367 else
3368 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3369 }
3370
3378 public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
3379 {
3380 Debug.Assert(t1 != null);
3381 Debug.Assert(t2 != null);
3382 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3383
3384 return AndThen(t1, t2, ts);
3385 }
3386
3392 {
3393 Debug.Assert(t1 != null);
3394 Debug.Assert(t2 != null);
3395
3396 CheckContextMatch(t1);
3397 CheckContextMatch(t2);
3398 return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3399 }
3400
3407 public Tactic TryFor(Tactic t, uint ms)
3408 {
3409 Debug.Assert(t != null);
3410
3411 CheckContextMatch(t);
3412 return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3413 }
3414
3423 {
3424 Debug.Assert(p != null);
3425 Debug.Assert(t != null);
3426
3427 CheckContextMatch(t);
3428 CheckContextMatch(p);
3429 return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3430 }
3431
3436 public Tactic Cond(Probe p, Tactic t1, Tactic t2)
3437 {
3438 Debug.Assert(p != null);
3439 Debug.Assert(t1 != null);
3440 Debug.Assert(t2 != null);
3441
3442 CheckContextMatch(p);
3443 CheckContextMatch(t1);
3444 CheckContextMatch(t2);
3445 return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3446 }
3447
3452 public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
3453 {
3454 Debug.Assert(t != null);
3455
3456 CheckContextMatch(t);
3457 return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3458 }
3459
3463 public Tactic Skip()
3464 {
3465
3466 return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3467 }
3468
3472 public Tactic Fail()
3473 {
3474
3475 return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3476 }
3477
3482 {
3483 Debug.Assert(p != null);
3484
3485 CheckContextMatch(p);
3486 return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3487 }
3488
3494 {
3495
3496 return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3497 }
3498
3503 {
3504 Debug.Assert(t != null);
3505 Debug.Assert(p != null);
3506
3507 CheckContextMatch(t);
3508 CheckContextMatch(p);
3509 return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3510 }
3511
3517 {
3518 Debug.Assert(t != null);
3519 Debug.Assert(p != null);
3520
3521 return UsingParams(t, p);
3522 }
3523
3527 public Tactic ParOr(params Tactic[] t)
3528 {
3529 Debug.Assert(t == null || t.All(tactic => tactic != null));
3530
3531 CheckContextMatch<Tactic>(t);
3532 return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
3533 }
3534
3540 {
3541 Debug.Assert(t1 != null);
3542 Debug.Assert(t2 != null);
3543
3544 CheckContextMatch(t1);
3545 CheckContextMatch(t2);
3546 return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3547 }
3548
3553 public void Interrupt()
3554 {
3555 Native.Z3_interrupt(nCtx);
3556 }
3557 #endregion
3558
3559 #region Probes
3563 public uint NumProbes
3564 {
3565 get { return Native.Z3_get_num_probes(nCtx); }
3566 }
3567
3571 public string[] ProbeNames
3572 {
3573 get
3574 {
3575
3576 uint n = NumProbes;
3577 string[] res = new string[n];
3578 for (uint i = 0; i < n; i++)
3579 res[i] = Native.Z3_get_probe_name(nCtx, i);
3580 return res;
3581 }
3582 }
3583
3587 public string ProbeDescription(string name)
3588 {
3589
3590 return Native.Z3_probe_get_descr(nCtx, name);
3591 }
3592
3596 public Probe MkProbe(string name)
3597 {
3598
3599 return new Probe(this, name);
3600 }
3601
3605 public Probe ConstProbe(double val)
3606 {
3607
3608 return new Probe(this, Native.Z3_probe_const(nCtx, val));
3609 }
3610
3615 public Probe Lt(Probe p1, Probe p2)
3616 {
3617 Debug.Assert(p1 != null);
3618 Debug.Assert(p2 != null);
3619
3620 CheckContextMatch(p1);
3621 CheckContextMatch(p2);
3622 return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3623 }
3624
3629 public Probe Gt(Probe p1, Probe p2)
3630 {
3631 Debug.Assert(p1 != null);
3632 Debug.Assert(p2 != null);
3633
3634 CheckContextMatch(p1);
3635 CheckContextMatch(p2);
3636 return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3637 }
3638
3643 public Probe Le(Probe p1, Probe p2)
3644 {
3645 Debug.Assert(p1 != null);
3646 Debug.Assert(p2 != null);
3647
3648 CheckContextMatch(p1);
3649 CheckContextMatch(p2);
3650 return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3651 }
3652
3657 public Probe Ge(Probe p1, Probe p2)
3658 {
3659 Debug.Assert(p1 != null);
3660 Debug.Assert(p2 != null);
3661
3662 CheckContextMatch(p1);
3663 CheckContextMatch(p2);
3664 return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3665 }
3666
3671 public Probe Eq(Probe p1, Probe p2)
3672 {
3673 Debug.Assert(p1 != null);
3674 Debug.Assert(p2 != null);
3675
3676 CheckContextMatch(p1);
3677 CheckContextMatch(p2);
3678 return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3679 }
3680
3685 public Probe And(Probe p1, Probe p2)
3686 {
3687 Debug.Assert(p1 != null);
3688 Debug.Assert(p2 != null);
3689
3690 CheckContextMatch(p1);
3691 CheckContextMatch(p2);
3692 return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3693 }
3694
3699 public Probe Or(Probe p1, Probe p2)
3700 {
3701 Debug.Assert(p1 != null);
3702 Debug.Assert(p2 != null);
3703
3704 CheckContextMatch(p1);
3705 CheckContextMatch(p2);
3706 return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3707 }
3708
3713 public Probe Not(Probe p)
3714 {
3715 Debug.Assert(p != null);
3716
3717 CheckContextMatch(p);
3718 return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3719 }
3720 #endregion
3721
3722 #region Solvers
3731 public Solver MkSolver(Symbol logic = null)
3732 {
3733
3734 if (logic == null)
3735 return new Solver(this, Native.Z3_mk_solver(nCtx));
3736 else
3737 return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3738 }
3739
3744 public Solver MkSolver(string logic)
3745 {
3746
3747 return MkSolver(MkSymbol(logic));
3748 }
3749
3754 {
3755
3756 return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3757 }
3758
3767 {
3768 Debug.Assert(t != null);
3769
3770 return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3771 }
3772 #endregion
3773
3774 #region Fixedpoints
3779 {
3780
3781 return new Fixedpoint(this);
3782 }
3783 #endregion
3784
3785 #region Optimization
3790 {
3791
3792 return new Optimize(this);
3793 }
3794 #endregion
3795
3796 #region Floating-Point Arithmetic
3797
3798 #region Rounding Modes
3799 #region RoundingMode Sort
3804 {
3805 return new FPRMSort(this);
3806 }
3807 #endregion
3808
3809 #region Numerals
3814 {
3815 return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
3816 }
3817
3822 {
3823 return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
3824 }
3825
3830 {
3831 return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
3832 }
3833
3838 {
3839 return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
3840 }
3841
3846 {
3847 return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
3848 }
3849
3854 {
3855 return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
3856 }
3857
3862 {
3863 return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
3864 }
3865
3870 {
3871 return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
3872 }
3873
3878 {
3879 return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
3880 }
3881
3886 {
3887 return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
3888 }
3889 #endregion
3890 #endregion
3891
3892 #region FloatingPoint Sorts
3898 public FPSort MkFPSort(uint ebits, uint sbits)
3899 {
3900 return new FPSort(this, ebits, sbits);
3901 }
3902
3907 {
3908 return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
3909 }
3910
3915 {
3916 return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
3917 }
3918
3923 {
3924 return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
3925 }
3926
3931 {
3932 return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx));
3933 }
3934
3939 {
3940 return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
3941 }
3942
3947 {
3948 return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
3949 }
3950
3955 {
3956 return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
3957 }
3958
3963 {
3964 return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
3965 }
3966 #endregion
3967
3968 #region Numerals
3974 {
3975 return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
3976 }
3977
3983 public FPNum MkFPInf(FPSort s, bool negative)
3984 {
3985 return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
3986 }
3987
3993 public FPNum MkFPZero(FPSort s, bool negative)
3994 {
3995 return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
3996 }
3997
4003 public FPNum MkFPNumeral(float v, FPSort s)
4004 {
4005 return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
4006 }
4007
4013 public FPNum MkFPNumeral(double v, FPSort s)
4014 {
4015 return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
4016 }
4017
4023 public FPNum MkFPNumeral(int v, FPSort s)
4024 {
4025 return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
4026 }
4027
4035 public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
4036 {
4037 return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
4038 }
4039
4047 public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
4048 {
4049 return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
4050 }
4051
4057 public FPNum MkFP(float v, FPSort s)
4058 {
4059 return MkFPNumeral(v, s);
4060 }
4061
4067 public FPNum MkFP(double v, FPSort s)
4068 {
4069 return MkFPNumeral(v, s);
4070 }
4071
4077 public FPNum MkFP(int v, FPSort s)
4078 {
4079 return MkFPNumeral(v, s);
4080 }
4081
4089 public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
4090 {
4091 return MkFPNumeral(sgn, exp, sig, s);
4092 }
4093
4101 public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
4102 {
4103 return MkFPNumeral(sgn, exp, sig, s);
4104 }
4105
4106 #endregion
4107
4108 #region Operators
4114 {
4115 return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
4116 }
4117
4123 {
4124 return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
4125 }
4126
4134 {
4135 return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4136 }
4137
4145 {
4146 return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4147 }
4148
4156 {
4157 return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4158 }
4159
4167 {
4168 return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4169 }
4170
4182 {
4183 return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
4184 }
4185
4192 {
4193 return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
4194 }
4195
4202 {
4203 return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
4204 }
4205
4213 {
4214 return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
4215 }
4216
4223 {
4224 return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
4225 }
4226
4233 {
4234 return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
4235 }
4236
4243 {
4244 return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
4245 }
4246
4253 {
4254 return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
4255 }
4256
4263 {
4264 return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
4265 }
4266
4273 {
4274 return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
4275 }
4276
4286 {
4287 return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
4288 }
4289
4295 {
4296 return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
4297 }
4298
4304 {
4305 return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
4306 }
4307
4313 {
4314 return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
4315 }
4316
4322 {
4323 return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
4324 }
4325
4331 {
4332 return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
4333 }
4334
4340 {
4341 return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
4342 }
4343
4349 {
4350 return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
4351 }
4352 #endregion
4353
4354 #region Conversions to FloatingPoint terms
4369 {
4370 return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
4371 }
4372
4385 {
4386 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
4387 }
4388
4401 {
4402 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4403 }
4404
4417 {
4418 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4419 }
4420
4434 public FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
4435 {
4436 if (signed)
4437 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4438 else
4439 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4440 }
4441
4453 {
4454 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
4455 }
4456 #endregion
4457
4458 #region Conversions from FloatingPoint terms
4471 public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed)
4472 {
4473 if (signed)
4474 return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4475 else
4476 return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4477 }
4478
4489 {
4490 return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
4491 }
4492 #endregion
4493
4494 #region Z3-specific extensions
4506 {
4507 return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
4508 }
4509
4523 {
4524 return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
4525 }
4526 #endregion
4527 #endregion // Floating-point Arithmetic
4528
4529 #region Miscellaneous
4540 public AST WrapAST(IntPtr nativeObject)
4541 {
4542 return AST.Create(this, nativeObject);
4543 }
4544
4556 public IntPtr UnwrapAST(AST a)
4557 {
4558 return a.NativeObject;
4559 }
4560
4564 public string SimplifyHelp()
4565 {
4566
4567 return Native.Z3_simplify_get_help(nCtx);
4568 }
4569
4574 {
4575 get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
4576 }
4577 #endregion
4578
4579 #region Error Handling
4587 //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
4588
4592 //public event ErrorHandler OnError = null;
4593 #endregion
4594
4595 #region Parameters
4605 public void UpdateParamValue(string id, string value)
4606 {
4607 Native.Z3_update_param_value(nCtx, id, value);
4608 }
4609
4610 #endregion
4611
4612 #region Internal
4613 internal IntPtr m_ctx = IntPtr.Zero;
4614 internal Native.Z3_error_handler m_n_err_handler = null;
4615 internal static Object creation_lock = new Object();
4616 internal IntPtr nCtx { get { return m_ctx; } }
4617
4618 internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
4619 {
4620 // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
4621 }
4622
4623 internal void InitContext()
4624 {
4625 PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
4626 m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
4627 Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
4628 GC.SuppressFinalize(this);
4629 }
4630
4631 internal void CheckContextMatch(Z3Object other)
4632 {
4633 Debug.Assert(other != null);
4634
4635 if (!ReferenceEquals(this, other.Context))
4636 throw new Z3Exception("Context mismatch");
4637 }
4638
4639 internal void CheckContextMatch(Z3Object other1, Z3Object other2)
4640 {
4641 Debug.Assert(other1 != null);
4642 Debug.Assert(other2 != null);
4643 CheckContextMatch(other1);
4644 CheckContextMatch(other2);
4645 }
4646
4647 internal void CheckContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
4648 {
4649 Debug.Assert(other1 != null);
4650 Debug.Assert(other2 != null);
4651 Debug.Assert(other3 != null);
4652 CheckContextMatch(other1);
4653 CheckContextMatch(other2);
4654 CheckContextMatch(other3);
4655 }
4656
4657 internal void CheckContextMatch(Z3Object[] arr)
4658 {
4659 Debug.Assert(arr == null || arr.All(a => a != null));
4660
4661 if (arr != null)
4662 {
4663 foreach (Z3Object a in arr)
4664 {
4665 Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
4666 CheckContextMatch(a);
4667 }
4668 }
4669 }
4670
4671 internal void CheckContextMatch<T>(IEnumerable<T> arr) where T : Z3Object
4672 {
4673 Debug.Assert(arr == null || arr.All(a => a != null));
4674
4675 if (arr != null)
4676 {
4677 foreach (Z3Object a in arr)
4678 {
4679 Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
4680 CheckContextMatch(a);
4681 }
4682 }
4683 }
4684
4685 private void ObjectInvariant()
4686 {
4687 Debug.Assert(m_AST_DRQ != null);
4688 Debug.Assert(m_ASTMap_DRQ != null);
4689 Debug.Assert(m_ASTVector_DRQ != null);
4690 Debug.Assert(m_ApplyResult_DRQ != null);
4691 Debug.Assert(m_FuncEntry_DRQ != null);
4692 Debug.Assert(m_FuncInterp_DRQ != null);
4693 Debug.Assert(m_Goal_DRQ != null);
4694 Debug.Assert(m_Model_DRQ != null);
4695 Debug.Assert(m_Params_DRQ != null);
4696 Debug.Assert(m_ParamDescrs_DRQ != null);
4697 Debug.Assert(m_Probe_DRQ != null);
4698 Debug.Assert(m_Solver_DRQ != null);
4699 Debug.Assert(m_Statistics_DRQ != null);
4700 Debug.Assert(m_Tactic_DRQ != null);
4701 Debug.Assert(m_Fixedpoint_DRQ != null);
4702 Debug.Assert(m_Optimize_DRQ != null);
4703 }
4704
4705 readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
4706 readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue(10);
4707 readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue(10);
4708 readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue(10);
4709 readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue(10);
4710 readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue(10);
4711 readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue(10);
4712 readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue(10);
4713 readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue(10);
4714 readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue(10);
4715 readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue(10);
4716 readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue(10);
4717 readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10);
4718 readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
4719 readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
4720 readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10);
4721
4725 public IDecRefQueue AST_DRQ { get { return m_AST_DRQ; } }
4726
4730 public IDecRefQueue ASTMap_DRQ { get { return m_ASTMap_DRQ; } }
4731
4735 public IDecRefQueue ASTVector_DRQ { get { return m_ASTVector_DRQ; } }
4736
4740 public IDecRefQueue ApplyResult_DRQ { get { return m_ApplyResult_DRQ; } }
4741
4745 public IDecRefQueue FuncEntry_DRQ { get { return m_FuncEntry_DRQ; } }
4746
4750 public IDecRefQueue FuncInterp_DRQ { get { return m_FuncInterp_DRQ; } }
4751
4755 public IDecRefQueue Goal_DRQ { get { return m_Goal_DRQ; } }
4756
4760 public IDecRefQueue Model_DRQ { get { return m_Model_DRQ; } }
4761
4765 public IDecRefQueue Params_DRQ { get { return m_Params_DRQ; } }
4766
4770 public IDecRefQueue ParamDescrs_DRQ { get { return m_ParamDescrs_DRQ; } }
4771
4775 public IDecRefQueue Probe_DRQ { get { return m_Probe_DRQ; } }
4776
4780 public IDecRefQueue Solver_DRQ { get { return m_Solver_DRQ; } }
4781
4785 public IDecRefQueue Statistics_DRQ { get { return m_Statistics_DRQ; } }
4786
4790 public IDecRefQueue Tactic_DRQ { get { return m_Tactic_DRQ; } }
4791
4795 public IDecRefQueue Fixedpoint_DRQ { get { return m_Fixedpoint_DRQ; } }
4796
4800 public IDecRefQueue Optimize_DRQ { get { return m_Fixedpoint_DRQ; } }
4801
4802 internal long refCount = 0;
4803
4807 ~Context()
4808 {
4809 // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4810 Dispose();
4811 }
4812
4816 public void Dispose()
4817 {
4818 // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4819 AST_DRQ.Clear(this);
4820 ASTMap_DRQ.Clear(this);
4821 ASTVector_DRQ.Clear(this);
4822 ApplyResult_DRQ.Clear(this);
4823 FuncEntry_DRQ.Clear(this);
4824 FuncInterp_DRQ.Clear(this);
4825 Goal_DRQ.Clear(this);
4826 Model_DRQ.Clear(this);
4827 Params_DRQ.Clear(this);
4828 ParamDescrs_DRQ.Clear(this);
4829 Probe_DRQ.Clear(this);
4830 Solver_DRQ.Clear(this);
4831 Statistics_DRQ.Clear(this);
4832 Tactic_DRQ.Clear(this);
4833 Fixedpoint_DRQ.Clear(this);
4834 Optimize_DRQ.Clear(this);
4835
4836 m_boolSort = null;
4837 m_intSort = null;
4838 m_realSort = null;
4839 m_stringSort = null;
4840 if (refCount == 0 && m_ctx != IntPtr.Zero)
4841 {
4842 m_n_err_handler = null;
4843 IntPtr ctx = m_ctx;
4844 m_ctx = IntPtr.Zero;
4845 Native.Z3_del_context(ctx);
4846 }
4847 else
4848 GC.ReRegisterForFinalize(this);
4849 }
4850 #endregion
4851 }
4852}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Vectors of ASTs.
Definition: ASTVector.cs:29
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:127
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:32
Array expressions
Definition: ArrayExpr.cs:32
Bit-vector expressions
Definition: BitVecExpr.cs:32
Bit-vector numerals
Definition: BitVecNum.cs:32
Bit-vector sorts.
Definition: BitVecSort.cs:29
Boolean expressions
Definition: BoolExpr.cs:32
A Boolean sort.
Definition: BoolSort.cs:29
Constructors are used for datatype sorts.
Definition: Constructor.cs:29
Lists of constructors
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
Definition: Context.cs:4416
BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
Bitwise NAND.
Definition: Context.cs:1309
FPNum MkFP(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4057
RealExpr MkInt2Real(IntExpr t)
Coerce an integer to a real.
Definition: Context.cs:1191
FPSort MkFPSort16()
Create the half-precision (16-bit) FloatingPoint sort.
Definition: Context.cs:3914
Expr MkNumeral(uint v, Sort ty)
Create a Term of a given sort. This function can be used to create numerals that fit in a machine int...
Definition: Context.cs:2775
ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
Create an array constant.
Definition: Context.cs:2026
BoolExpr MkAtLeast(IEnumerable< BoolExpr > args, uint k)
Create an at-least-k constraint.
Definition: Context.cs:2686
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
Shift left.
Definition: Context.cs:1722
IDecRefQueue ParamDescrs_DRQ
ParamDescrs DRQ
Definition: Context.cs:4770
Tactic Skip()
Create a tactic that just returns the given goal.
Definition: Context.cs:3463
Constructor MkConstructor(string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
Create a datatype constructor.
Definition: Context.cs:391
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition: Context.cs:128
BitVecNum MkBV(bool[] bits)
Create a bit-vector numeral.
Definition: Context.cs:3002
FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
Create a new finite domain sort. The result is a sort
Definition: Context.cs:340
BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2)
Check if the string s1 is lexicographically strictly less than s2.
Definition: Context.cs:2468
FPSort MkFPSort(uint ebits, uint sbits)
Create a FloatingPoint sort.
Definition: Context.cs:3898
Tactic With(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3516
string[] TacticNames
The names of all supported tactics.
Definition: Context.cs:3310
FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point addition
Definition: Context.cs:4133
BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Rotate Left.
Definition: Context.cs:1815
RealExpr MkRealConst(string name)
Creates a real constant.
Definition: Context.cs:758
RatNum MkReal(uint v)
Create a real numeral.
Definition: Context.cs:2857
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...
Definition: Context.cs:3629
BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Logical shift right
Definition: Context.cs:1744
FPRMSort MkFPRoundingModeSort()
Create the floating-point RoundingMode sort.
Definition: Context.cs:3803
RealExpr MkFPToReal(FPExpr t)
Conversion of a floating-point term into a real-numbered term.
Definition: Context.cs:4488
TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Create a new tuple sort.
Definition: Context.cs:272
Lambda MkLambda(Expr[] boundConstants, Expr body)
Create a lambda expression.
Definition: Context.cs:3192
IDecRefQueue Params_DRQ
Params DRQ
Definition: Context.cs:4765
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:219
BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise multiplication does not underflow.
Definition: Context.cs:1999
ArrayExpr MkFullSet(Sort domain)
Create the full set.
Definition: Context.cs:2238
FPSort MkFPSortQuadruple()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition: Context.cs:3954
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
Definition: Context.cs:1145
Probe ConstProbe(double val)
Create a probe that always evaluates to val .
Definition: Context.cs:3605
Expr MkFreshConst(string prefix, Sort range)
Creates a fresh Constant of sort range and a name prefixed with prefix .
Definition: Context.cs:687
IntExpr MkReal2Int(RealExpr t)
Coerce a real to an integer.
Definition: Context.cs:1206
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
Definition: Context.cs:182
FPSort MkFPSortHalf()
Create the half-precision (16-bit) FloatingPoint sort.
Definition: Context.cs:3906
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.
Definition: Context.cs:3063
ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Take the difference between two sets.
Definition: Context.cs:2300
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition: Context.cs:923
Expr MkNumeral(long v, Sort ty)
Create a Term of a given sort. This function can be used to create numerals that fit in a machine int...
Definition: Context.cs:2790
Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
Create an expression representing an if-then-else: ite(t1, t2, t3).
Definition: Context.cs:882
IntNum MkInt(uint v)
Create an integer numeral.
Definition: Context.cs:2913
IntExpr MkIntConst(Symbol name)
Creates an integer constant.
Definition: Context.cs:728
AST WrapAST(IntPtr nativeObject)
Wraps an AST.
Definition: Context.cs:4540
SeqExpr IntToString(Expr e)
Convert an integer expression to a string.
Definition: Context.cs:2381
FPExpr MkFPMax(FPExpr t1, FPExpr t2)
Maximum of floating-point numbers.
Definition: Context.cs:4232
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
Definition: Context.cs:1067
BitVecExpr MkFPToIEEEBV(FPExpr t)
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
Definition: Context.cs:4505
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
Definition: Context.cs:1055
Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
Create a datatype constructor.
Definition: Context.cs:374
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:139
BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
Check for sequence suffix.
Definition: Context.cs:2435
SeqExpr MkConcat(params SeqExpr[] t)
Concatenate sequences.
Definition: Context.cs:2402
FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:565
BoolExpr MkNot(BoolExpr a)
Mk an expression representing not(a).
Definition: Context.cs:868
FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:524
Expr MkTermArray(ArrayExpr array)
Access the array default value.
Definition: Context.cs:2189
BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
Signed remainder.
Definition: Context.cs:1471
BitVecExpr MkBVRedOR(BitVecExpr t)
Take disjunction of bits in a vector, return vector of length 1.
Definition: Context.cs:1255
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:3334
BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
Floating-point less than or equal.
Definition: Context.cs:4242
ReExpr MkOption(ReExpr re)
Create the optional regular expression.
Definition: Context.cs:2585
BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
Floating-point equality.
Definition: Context.cs:4285
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition: Context.cs:429
SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
Extract subsequence.
Definition: Context.cs:2501
RatNum MkReal(string v)
Create a real numeral.
Definition: Context.cs:2835
FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Definition: Context.cs:4400
DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
Create a new datatype sort.
Definition: Context.cs:415
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.
Definition: Context.cs:4434
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3502
BoolExpr MkBVNegNoOverflow(BitVecExpr t)
Create a predicate that checks that the bit-wise negation does not overflow.
Definition: Context.cs:1969
ListSort MkListSort(string name, Sort elemSort)
Create a new list sort.
Definition: Context.cs:326
uint NumTactics
The number of supported tactics.
Definition: Context.cs:3302
ReExpr MkConcat(params ReExpr[] t)
Create the concatenation of regular languages.
Definition: Context.cs:2603
BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than
Definition: Context.cs:1504
BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise multiplication does not overflow.
Definition: Context.cs:1983
FuncDecl MkConstDecl(Symbol name, Sort range)
Creates a new constant function declaration.
Definition: Context.cs:594
BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Signed division.
Definition: Context.cs:1433
ParamDescrs SimplifyParameterDescriptions
Retrieves parameter descriptions for simplifier.
Definition: Context.cs:4574
BitVecNum MkBV(ulong v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2992
FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Floating-point fused multiply-add
Definition: Context.cs:4181
BoolExpr MkFPIsInfinite(FPExpr t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.
Definition: Context.cs:4321
BitVecExpr MkInt2BV(uint n, IntExpr t)
Create an n bit bit-vector from the integer argument t .
Definition: Context.cs:1852
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:815
FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point subtraction
Definition: Context.cs:4144
FPNum MkFPNumeral(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4013
FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Definition: Context.cs:4384
ReExpr MkUnion(params ReExpr[] t)
Create the union of regular languages.
Definition: Context.cs:2615
RatNum MkReal(ulong v)
Create a real numeral.
Definition: Context.cs:2879
BoolExpr MkBoolConst(Symbol name)
Create a Boolean constant.
Definition: Context.cs:709
IDecRefQueue Model_DRQ
Model DRQ
Definition: Context.cs:4760
ReExpr MkEmptyRe(Sort s)
Create the empty regular expression. The sort s should be a regular expression.
Definition: Context.cs:2640
Expr MkNth(SeqExpr s, Expr index)
Retrieve element at index.
Definition: Context.cs:2490
FPSort MkFPSortSingle()
Create the single-precision (32-bit) FloatingPoint sort.
Definition: Context.cs:3922
IntPtr UnwrapAST(AST a)
Unwraps an AST.
Definition: Context.cs:4556
IntExpr MkMod(IntExpr t1, IntExpr t2)
Create an expression representing t1 mod t2.
Definition: Context.cs:1092
BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean less-or-equal constraint.
Definition: Context.cs:2697
IntNum MkInt(string v)
Create an integer numeral.
Definition: Context.cs:2891
Expr MkConst(FuncDecl f)
Creates a fresh constant from the FuncDecl f .
Definition: Context.cs:699
FPRMNum MkFPRTZ()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Definition: Context.cs:3885
IDecRefQueue Optimize_DRQ
Optimize DRQ
Definition: Context.cs:4800
Tactic TryFor(Tactic t, uint ms)
Create a tactic that applies t to a goal for ms milliseconds.
Definition: Context.cs:3407
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 -> t2.
Definition: Context.cs:910
BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise subtraction does not underflow.
Definition: Context.cs:1937
Expr MkSelect(ArrayExpr a, Expr i)
Array read.
Definition: Context.cs:2048
ArrayExpr MkSetUnion(params ArrayExpr[] args)
Take the union of a list of sets.
Definition: Context.cs:2276
IDecRefQueue ApplyResult_DRQ
ApplyResult DRQ
Definition: Context.cs:4740
IDecRefQueue ASTVector_DRQ
ASTVector DRQ
Definition: Context.cs:4735
IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Extract index of sub-string starting at offset.
Definition: Context.cs:2513
BoolExpr MkBoolConst(string name)
Create a Boolean constant.
Definition: Context.cs:719
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:788
BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
Two's complement signed remainder (sign follows divisor).
Definition: Context.cs:1488
IDecRefQueue Goal_DRQ
Goal DRQ
Definition: Context.cs:4755
Probe Or(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".
Definition: Context.cs:3699
BitVecExpr MkRepeat(uint i, BitVecExpr t)
Bit-vector repetition.
Definition: Context.cs:1702
FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:508
BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
Floating-point greater than.
Definition: Context.cs:4272
BoolExpr MkAtMost(IEnumerable< BoolExpr > args, uint k)
Create an at-most-k constraint.
Definition: Context.cs:2675
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 ....
Definition: Context.cs:3539
Solver MkSolver(string logic)
Creates a new (incremental) solver.
Definition: Context.cs:3744
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.
Definition: Context.cs:3141
ArrayExpr MkSetDel(ArrayExpr set, Expr element)
Remove an element from a set.
Definition: Context.cs:2263
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....
Definition: Context.cs:479
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...
Definition: Context.cs:3615
ReExpr MkRange(SeqExpr lo, SeqExpr hi)
Create a range expression.
Definition: Context.cs:2660
BitVecNum MkBV(long v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2981
BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater-than.
Definition: Context.cs:1616
Params MkParams()
Creates a new ParameterSet.
Definition: Context.cs:3290
ArrayExpr MkSetIntersection(params ArrayExpr[] args)
Take the intersection of a list of sets.
Definition: Context.cs:2288
FPNum MkFPNaN(FPSort s)
Create a NaN of sort s.
Definition: Context.cs:3973
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.
Definition: Context.cs:4101
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.
Definition: Context.cs:3233
BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise NOR.
Definition: Context.cs:1323
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
Definition: Context.cs:855
FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...
Definition: Context.cs:4212
Fixedpoint MkFixedpoint()
Create a Fixedpoint context.
Definition: Context.cs:3778
BoolExpr MkXor(IEnumerable< BoolExpr > ts)
Create an expression representing t1 xor t2 xor t3 ... .
Definition: Context.cs:936
void UpdateParamValue(string id, string value)
Update a mutable configuration parameter.
Definition: Context.cs:4605
DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
Create a new datatype sort.
Definition: Context.cs:400
IDecRefQueue Statistics_DRQ
Statistics DRQ
Definition: Context.cs:4785
void AddRecDef(FuncDecl f, Expr[] args, Expr body)
Bind a definition to a recursive function declaration. The function must have previously been created...
Definition: Context.cs:553
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4003
ArrayExpr MkConstArray(Sort domain, Expr v)
Create a constant array.
Definition: Context.cs:2151
ArrayExpr MkSetComplement(ArrayExpr arg)
Take the complement of a set.
Definition: Context.cs:2313
BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Check for subsetness of sets.
Definition: Context.cs:2337
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...
Definition: Context.cs:3671
FPRMNum MkFPRoundNearestTiesToAway()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Definition: Context.cs:3829
string[] ProbeNames
The names of all supported Probes.
Definition: Context.cs:3572
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 .
Definition: Context.cs:3344
BitVecExpr MkZeroExt(uint i, BitVecExpr t)
Bit-vector zero extension.
Definition: Context.cs:1688
Z3_ast_print_mode PrintMode
Selects the format used for pretty-printing expressions.
Definition: Context.cs:3222
IDecRefQueue FuncEntry_DRQ
FuncEntry DRQ
Definition: Context.cs:4745
void Dispose()
Disposes of the context.
Definition: Context.cs:4816
IDecRefQueue Solver_DRQ
Solver DRQ
Definition: Context.cs:4780
ArrayExpr MkEmptySet(Sort domain)
Create an empty set.
Definition: Context.cs:2227
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.
Definition: Context.cs:3081
UninterpretedSort MkUninterpretedSort(string str)
Create a new uninterpreted sort.
Definition: Context.cs:193
IDecRefQueue FuncInterp_DRQ
FuncInterp DRQ
Definition: Context.cs:4750
Expr MkNumeral(ulong v, Sort ty)
Create a Term of a given sort. This function can be used to create numerals that fit in a machine int...
Definition: Context.cs:2805
ReExpr MkStar(ReExpr re)
Take the Kleene star of a regular expression.
Definition: Context.cs:2558
Context()
Constructor.
Definition: Context.cs:37
BitVecExpr MkBVConst(string name, uint size)
Creates a bit-vector constant.
Definition: Context.cs:777
BitVecNum MkBV(uint v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2970
Optimize MkOptimize()
Create an Optimization context.
Definition: Context.cs:3789
IDecRefQueue AST_DRQ
AST DRQ
Definition: Context.cs:4725
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.
Definition: Context.cs:3118
Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned...
Definition: Context.cs:2200
FPNum MkFPInf(FPSort s, bool negative)
Create a floating-point infinity of sort s.
Definition: Context.cs:3983
FuncDecl MkConstDecl(string name, Sort range)
Creates a new constant function declaration.
Definition: Context.cs:607
ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
Maps f on the argument arrays.
Definition: Context.cs:2172
ReExpr MkIntersect(params ReExpr[] t)
Create the intersection of regular languages.
Definition: Context.cs:2627
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...
Definition: Context.cs:3452
BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than or equal to.
Definition: Context.cs:1552
FPNum MkFP(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition: Context.cs:4077
IDecRefQueue Fixedpoint_DRQ
FixedPoint DRQ
Definition: Context.cs:4795
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
Definition: Context.cs:1132
FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two integers.
Definition: Context.cs:4089
ListSort MkListSort(Symbol name, Sort elemSort)
Create a new list sort.
Definition: Context.cs:313
SeqExpr MkAt(SeqExpr s, Expr index)
Retrieve sequence of length one at index.
Definition: Context.cs:2479
FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Conversion of a floating-point number to another FloatingPoint sort s.
Definition: Context.cs:4452
BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
Check for set membership.
Definition: Context.cs:2324
BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Rotate Right.
Definition: Context.cs:1832
SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
Replace the first occurrence of src by dst in s.
Definition: Context.cs:2525
FPRMExpr MkFPRoundNearestTiesToEven()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Definition: Context.cs:3813
string ProbeDescription(string name)
Returns a string containing a description of the probe with the given name.
Definition: Context.cs:3587
Pattern MkPattern(params Expr[] terms)
Create a quantifier pattern.
Definition: Context.cs:647
Probe And(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".
Definition: Context.cs:3685
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...
Definition: Context.cs:3643
FPExpr MkFPNeg(FPExpr t)
Floating-point negation
Definition: Context.cs:4122
FPSort MkFPSort32()
Create the single-precision (32-bit) FloatingPoint sort.
Definition: Context.cs:3930
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:662
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:151
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:956
BoolExpr MkIsInteger(RealExpr t)
Creates an expression that checks whether a real number is an integer.
Definition: Context.cs:1217
BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XNOR.
Definition: Context.cs:1337
BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than or equal to.
Definition: Context.cs:1536
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
Definition: Context.cs:1171
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.
Definition: Context.cs:4047
BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise addition does not underflow.
Definition: Context.cs:1905
BitVecNum MkBV(string v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2948
ReExpr MkFullRe(Sort s)
Create the full regular expression. The sort s should be a regular expression.
Definition: Context.cs:2650
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
Definition: Context.cs:1031
BoolExpr MkFPIsSubnormal(FPExpr t)
Predicate indicating whether t is a subnormal floating-point number.
Definition: Context.cs:4303
ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
Create an array constant.
Definition: Context.cs:2014
BoolExpr MkFPIsZero(FPExpr t)
Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
Definition: Context.cs:4312
ReSort MkReSort(SeqSort s)
Create a new regular expression sort.
Definition: Context.cs:237
FPSort MkFPSortDouble()
Create the double-precision (64-bit) FloatingPoint sort.
Definition: Context.cs:3938
FPRMNum MkFPRoundTowardZero()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Definition: Context.cs:3877
Goal MkGoal(bool models=true, bool unsatCores=false, bool proofs=false)
Creates a new Goal.
Definition: Context.cs:3279
IntExpr MkBV2Int(BitVecExpr t, bool signed)
Create an integer from the bit-vector argument t .
Definition: Context.cs:1875
ArithExpr MkAdd(params ArithExpr[] t)
Create an expression representing t[0] + t[1] + ....
Definition: Context.cs:1007
BoolExpr MkInRe(SeqExpr s, ReExpr re)
Check for regular expression membership.
Definition: Context.cs:2547
ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
Add an element to the set.
Definition: Context.cs:2249
BitVecExpr MkBVRedAND(BitVecExpr t)
Take conjunction of bits in a vector, return vector of length 1.
Definition: Context.cs:1243
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...
Definition: Context.cs:3657
ReExpr MkLoop(ReExpr re, uint lo, uint hi=0)
Take the bounded Kleene star of a regular expression.
Definition: Context.cs:2567
FPRMNum MkFPRoundTowardNegative()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Definition: Context.cs:3861
Probe MkProbe(string name)
Creates a new Probe.
Definition: Context.cs:3596
FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two integers.
Definition: Context.cs:4035
SeqSort MkSeqSort(Sort s)
Create a new sequence sort.
Definition: Context.cs:228
DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
Create mutually recursive data-types.
Definition: Context.cs:462
Tactic FailIf(Probe p)
Create a tactic that fails if the probe p evaluates to false.
Definition: Context.cs:3481
Expr MkBound(uint index, Sort ty)
Creates a new bound variable.
Definition: Context.cs:635
FPRMNum MkFPRTN()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Definition: Context.cs:3869
BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed)
Conversion of a floating-point term into a bit-vector.
Definition: Context.cs:4471
FPSort MkFPSort128()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition: Context.cs:3962
BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
Unsigned greater than or equal to.
Definition: Context.cs:1568
Expr MkNumeral(int v, Sort ty)
Create a Term of a given sort. This function can be used to create numerals that fit in a machine int...
Definition: Context.cs:2760
FPRMNum MkFPRTP()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Definition: Context.cs:3853
BoolSort MkBoolSort()
Create a new Boolean sort.
Definition: Context.cs:174
BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
Bit-vector concatenation.
Definition: Context.cs:1636
ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 ^ t2.
Definition: Context.cs:1119
SeqExpr MkEmptySeq(Sort s)
Create the empty sequence.
Definition: Context.cs:2354
BitVecExpr MkBVNot(BitVecExpr t)
Bitwise negation.
Definition: Context.cs:1231
FPExpr MkFPRem(FPExpr t1, FPExpr t2)
Floating-point remainder
Definition: Context.cs:4201
RealSort MkRealSort()
Create a real sort.
Definition: Context.cs:211
BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise addition does not overflow.
Definition: Context.cs:1889
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
Definition: Context.cs:1078
Expr MkSelect(ArrayExpr a, params Expr[] args)
Array read.
Definition: Context.cs:2071
FPNum MkFPNumeral(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition: Context.cs:4023
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.
Definition: Context.cs:3252
BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
Floating-point less than.
Definition: Context.cs:4252
BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
Floating-point greater than or equal.
Definition: Context.cs:4262
BitVecExpr MkSignExt(uint i, BitVecExpr t)
Bit-vector sign extension.
Definition: Context.cs:1671
Tactic ParOr(params Tactic[] t)
Create a tactic that applies the given tactics in parallel until one of them succeeds (i....
Definition: Context.cs:3527
IntSort MkIntSort()
Create a new integer sort.
Definition: Context.cs:202
BoolExpr MkAnd(IEnumerable< BoolExpr > t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:968
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
Definition: Context.cs:979
BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
Two's complement multiplication.
Definition: Context.cs:1391
IntExpr StringToInt(Expr e)
Convert an integer expression to a string.
Definition: Context.cs:2391
BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise signed division does not overflow.
Definition: Context.cs:1953
BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
Check for sequence containment of s2 in s1.
Definition: Context.cs:2446
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...
Definition: Context.cs:3391
SeqSort StringSort
Retrieves the String sort of the context.
Definition: Context.cs:162
BoolExpr MkEq(Expr x, Expr y)
Creates the equality x = y .
Definition: Context.cs:842
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.
Definition: Context.cs:3436
BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
Two's complement subtraction.
Definition: Context.cs:1377
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Unsigned division.
Definition: Context.cs:1410
void Interrupt()
Interrupt the execution of a Z3 procedure.
Definition: Context.cs:3553
BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
Unsigned greater-than.
Definition: Context.cs:1600
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition: Context.cs:246
BitVecExpr MkBVConst(Symbol name, uint size)
Creates a bit-vector constant.
Definition: Context.cs:767
BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
Arithmetic shift right
Definition: Context.cs:1768
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 .
Definition: Context.cs:3378
FPNum MkFPZero(FPSort s, bool negative)
Create a floating-point zero of sort s.
Definition: Context.cs:3993
BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean greater-or-equal constraint.
Definition: Context.cs:2711
IntNum MkInt(long v)
Create an integer numeral.
Definition: Context.cs:2924
RatNum MkReal(long v)
Create a real numeral.
Definition: Context.cs:2868
ReExpr MkPlus(ReExpr re)
Take the Kleene plus of a regular expression.
Definition: Context.cs:2576
FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
Floating-point square root
Definition: Context.cs:4191
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 iff t2.
Definition: Context.cs:897
FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
Create a new finite domain sort. The result is a sortElements of the sort are created using MkNumeral...
Definition: Context.cs:356
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2745
ArithExpr MkAdd(IEnumerable< ArithExpr > t)
Create an expression representing t[0] + t[1] + ....
Definition: Context.cs:1019
FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
Creates a new recursive function declaration.
Definition: Context.cs:537
BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
Two's complement addition.
Definition: Context.cs:1363
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
Definition: Context.cs:1158
Solver MkSimpleSolver()
Creates a new (incremental) solver.
Definition: Context.cs:3753
ArraySort MkArraySort(Sort[] domain, Sort range)
Create a new n-ary array sort.
Definition: Context.cs:259
Probe Not(Probe p)
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
Definition: Context.cs:3713
BoolExpr MkBool(bool value)
Creates a Boolean value.
Definition: Context.cs:833
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
Bitwise conjunction.
Definition: Context.cs:1267
Solver MkSolver(Tactic t)
Creates a solver that is implemented using the given tactic.
Definition: Context.cs:3766
RealExpr MkRealConst(Symbol name)
Creates a real constant.
Definition: Context.cs:748
IntNum MkInt(ulong v)
Create an integer numeral.
Definition: Context.cs:2935
Expr MkApp(FuncDecl f, IEnumerable< Expr > args)
Create a new function application.
Definition: Context.cs:801
ReExpr MkToRe(SeqExpr s)
Convert a regular expression that accepts sequence s.
Definition: Context.cs:2537
BoolExpr MkFPIsNaN(FPExpr t)
Predicate indicating whether t is a NaN.
Definition: Context.cs:4330
BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
Rotate Right.
Definition: Context.cs:1800
string SimplifyHelp()
Return a string describing all available parameters to Expr.Simplify.
Definition: Context.cs:4564
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.
Definition: Context.cs:3103
Lambda MkLambda(Sort[] sorts, Symbol[] names, Expr body)
Create a lambda expression.
Definition: Context.cs:3173
FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:493
BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than
Definition: Context.cs:1520
IDecRefQueue Tactic_DRQ
Tactic DRQ
Definition: Context.cs:4790
SetSort MkSetSort(Sort ty)
Create a set type.
Definition: Context.cs:2216
EnumSort MkEnumSort(string name, params string[] enumNames)
Create a new enumeration sort.
Definition: Context.cs:303
BitVecNum MkBV(int v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2959
RatNum MkReal(int num, int den)
Create a real from a fraction.
Definition: Context.cs:2822
IDecRefQueue Probe_DRQ
Probe DRQ
Definition: Context.cs:4775
EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
Create a new enumeration sort.
Definition: Context.cs:288
BoolExpr MkFPIsNegative(FPExpr t)
Predicate indicating whether t is a negative floating-point number.
Definition: Context.cs:4339
FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
Creates a fresh function declaration with a name prefixed with prefix .
Definition: Context.cs:581
IntExpr MkIntConst(string name)
Creates an integer constant.
Definition: Context.cs:738
Tactic When(Probe p, Tactic t)
Create a tactic that applies t to a given goal if the probe p evaluates to true.
Definition: Context.cs:3422
BitVecExpr MkBVNeg(BitVecExpr t)
Standard two's complement unary minus.
Definition: Context.cs:1351
FuncDecl MkFreshConstDecl(string prefix, Sort range)
Creates a fresh constant function declaration with a name prefixed with prefix .
Definition: Context.cs:620
Tactic Fail()
Create a tactic always fails.
Definition: Context.cs:3472
Tactic FailIfNotDecided()
Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsati...
Definition: Context.cs:3493
FPRMNum MkFPRoundTowardPositive()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Definition: Context.cs:3845
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
Bitwise disjunction.
Definition: Context.cs:1281
Expr MkConst(string name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:676
IntExpr MkRem(IntExpr t1, IntExpr t2)
Create an expression representing t1 rem t2.
Definition: Context.cs:1106
FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point multiplication
Definition: Context.cs:4155
BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
Check if the string s1 is lexicographically strictly less than s2.
Definition: Context.cs:2457
BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise subtraction does not overflow.
Definition: Context.cs:1921
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...
Definition: Context.cs:4522
FPSort MkFPSort64()
Create the double-precision (64-bit) FloatingPoint sort.
Definition: Context.cs:3946
FPRMNum MkFPRNA()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Definition: Context.cs:3837
Context(Dictionary< string, string > settings)
Constructor.
Definition: Context.cs:65
BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
Rotate Left.
Definition: Context.cs:1785
string TacticDescription(string name)
Returns a string containing a description of the tactic with the given name.
Definition: Context.cs:3325
FPRMNum MkFPRNE()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Definition: Context.cs:3821
IDecRefQueue ASTMap_DRQ
ASTMap DRQ
Definition: Context.cs:4730
SeqExpr MkUnit(Expr elem)
Create the singleton sequence.
Definition: Context.cs:2363
uint NumProbes
The number of supported Probes.
Definition: Context.cs:3564
BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean equal constraint.
Definition: Context.cs:2724
IntNum MkInt(int v)
Create an integer numeral.
Definition: Context.cs:2902
BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XOR.
Definition: Context.cs:1295
ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
Array update.
Definition: Context.cs:2130
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3731
FPExpr MkFPAbs(FPExpr t)
Floating-point absolute value
Definition: Context.cs:4113
FPExpr MkFPMin(FPExpr t1, FPExpr t2)
Minimum of floating-point numbers.
Definition: Context.cs:4222
FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point division
Definition: Context.cs:4166
BoolExpr MkOr(IEnumerable< BoolExpr > t)
Create an expression representing t[0] or t[1] or ....
Definition: Context.cs:992
ReExpr MkComplement(ReExpr re)
Create the complement regular expression.
Definition: Context.cs:2594
BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
Bit-vector extraction.
Definition: Context.cs:1655
ArithExpr MkMul(IEnumerable< ArithExpr > t)
Create an expression representing t[0] * t[1] * ....
Definition: Context.cs:1043
StringSymbol MkSymbol(string name)
Create a symbol using a string.
Definition: Context.cs:99
BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
Unsigned remainder.
Definition: Context.cs:1451
BoolExpr MkFalse()
The false Term.
Definition: Context.cs:824
IntExpr MkLength(SeqExpr s)
Retrieve the length of a given sequence.
Definition: Context.cs:2415
RatNum MkReal(int v)
Create a real numeral.
Definition: Context.cs:2846
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:90
SeqExpr MkString(string s)
Create a string constant.
Definition: Context.cs:2372
ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
Array update.
Definition: Context.cs:2100
FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
Create an expression of FloatingPoint sort from three bit-vector expressions.
Definition: Context.cs:4368
BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater than or equal to.
Definition: Context.cs:1584
Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create a universal Quantifier.
Definition: Context.cs:3039
FPNum MkFP(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4067
BoolExpr MkFPIsNormal(FPExpr t)
Predicate indicating whether t is a normal floating-point number.
Definition: Context.cs:4294
BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
Check for sequence prefix.
Definition: Context.cs:2424
BoolExpr MkFPIsPositive(FPExpr t)
Predicate indicating whether t is a positive floating-point number.
Definition: Context.cs:4348
Enumeration sorts.
Definition: EnumSort.cs:29
Expressions are terms.
Definition: Expr.cs:31
FloatingPoint Expressions
Definition: FPExpr.cs:32
FloatiungPoint Numerals
Definition: FPNum.cs:28
FloatingPoint RoundingMode Expressions
Definition: FPRMExpr.cs:32
Floating-point rounding mode numerals
Definition: FPRMNum.cs:32
The FloatingPoint RoundingMode sort
Definition: FPRMSort.cs:29
FloatingPoint sort
Definition: FPSort.cs:28
Object for managing fixedpoints
Definition: Fixedpoint.cs:30
Function declarations.
Definition: FuncDecl.cs:31
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:32
DecRefQueue interface
Definition: IDecRefQueue.cs:32
Int expressions
Definition: IntExpr.cs:32
Integer Numerals
Definition: IntNum.cs:32
An Integer sort
Definition: IntSort.cs:29
Numbered symbols
Definition: IntSymbol.cs:30
Lambda expressions.
Definition: Lambda.cs:30
Object for managing optimization context
Definition: Optimize.cs:31
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
Definition: Pattern.cs:32
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
Definition: Probe.cs:34
Quantifier expressions.
Definition: Quantifier.cs:30
Rational Numerals
Definition: RatNum.cs:32
Regular expression expressions
Definition: ReExpr.cs:32
A regular expression sort
Definition: ReSort.cs:29
Real expressions
Definition: RealExpr.cs:32
Sequence expressions
Definition: SeqExpr.cs:32
A Sequence sort
Definition: SeqSort.cs:29
Set sorts.
Definition: SetSort.cs:29
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
Definition: Solver.cs:151
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Tactics are the basic building block for creating custom solvers for specific problem domains....
Definition: Tactic.cs:32
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
expr max(expr const &a, expr const &b)
Definition: z3++.h:1836
def Lambda(vs, body)
Definition: z3py.py:2226
def SeqSort(s)
Definition: z3py.py:10579
def SetSort(s)
Sets.
Definition: z3py.py:4851
def ArraySort(*sig)
Definition: z3py.py:4645
def EnumSort(name, values, ctx=None)
Definition: z3py.py:5317
def ReSort(s)
Definition: z3py.py:10904
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7590
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9727
def TupleSort(name, sorts, ctx=None)
Definition: z3py.py:5293
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3967
def Model(ctx=None)
Definition: z3py.py:6579
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition: z3_api.h:1334
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1359