Z3
 
Loading...
Searching...
No Matches
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.Collections.Generic;
22using System.Diagnostics;
23using System.Linq;
24using System.Runtime.InteropServices;
25
26namespace Microsoft.Z3
27{
28
29 using Z3_context = System.IntPtr;
33 public class Context : IDisposable
34 {
35 #region Constructors
39 public Context()
40 : base()
41 {
42 lock (creation_lock)
43 {
44 m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
45 Native.Z3_enable_concurrent_dec_ref(m_ctx);
46 InitContext();
47 }
48 }
49
68 public Context(Dictionary<string, string> settings)
69 : base()
70 {
71 Debug.Assert(settings != null);
72
73 lock (creation_lock)
74 {
75 IntPtr cfg = Native.Z3_mk_config();
76 foreach (KeyValuePair<string, string> kv in settings)
77 Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
78 m_ctx = Native.Z3_mk_context_rc(cfg);
79 Native.Z3_enable_concurrent_dec_ref(m_ctx);
80 Native.Z3_del_config(cfg);
81 InitContext();
82 }
83 }
84
88 internal Context(Z3_context ctx)
89 : base()
90 {
91 lock (creation_lock)
92 {
93 is_external = true;
94 m_ctx = ctx;
95 InitContext();
96 }
97 }
98
99 bool is_external = false;
100
101 #endregion
102
103 #region Symbols
111 public IntSymbol MkSymbol(int i)
112 {
113 return new IntSymbol(this, i);
114 }
115
119 public StringSymbol MkSymbol(string name)
120 {
121 return new StringSymbol(this, name);
122 }
123
127 internal Symbol[] MkSymbols(string[] names)
128 {
129 if (names == null) return new Symbol[0];
130 Symbol[] result = new Symbol[names.Length];
131 for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
132 return result;
133 }
134 #endregion
135
136 #region Sorts
137 private BoolSort m_boolSort = null;
138 private IntSort m_intSort = null;
139 private RealSort m_realSort = null;
140 private SeqSort m_stringSort = null;
141 private CharSort m_charSort = null;
142
146 public BoolSort BoolSort
147 {
148 get
149 {
150 if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
151 }
152 }
153
157 public IntSort IntSort
158 {
159 get
160 {
161 if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
162 }
163 }
164
165
169 public RealSort RealSort
170 {
171 get
172 {
173 if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
174 }
175 }
176
180 public CharSort CharSort
181 {
182 get
183 {
184 if (m_charSort == null) m_charSort = new CharSort(this); return m_charSort;
185 }
186 }
187
188
192 public SeqSort StringSort
193 {
194 get
195 {
196 if (m_stringSort == null) m_stringSort = new SeqSort(this, Native.Z3_mk_string_sort(nCtx));
197 return m_stringSort;
198 }
199 }
200
201
205 public BoolSort MkBoolSort()
206 {
207 return new BoolSort(this);
208 }
209
213 public UninterpretedSort MkUninterpretedSort(Symbol s)
214 {
215 Debug.Assert(s != null);
216
217 CheckContextMatch(s);
218 return new UninterpretedSort(this, s);
219 }
220
224 public UninterpretedSort MkUninterpretedSort(string str)
225 {
226 using var sym = MkSymbol(str);
227 return MkUninterpretedSort(sym);
228 }
229
233 public IntSort MkIntSort()
234 {
235
236 return new IntSort(this);
237 }
238
242 public RealSort MkRealSort()
243 {
244 return new RealSort(this);
245 }
246
250 public BitVecSort MkBitVecSort(uint size)
251 {
252 return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
253 }
254
258 public SeqSort MkSeqSort(Sort s)
259 {
260 Debug.Assert(s != null);
261 return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
262 }
263
267 public ReSort MkReSort(SeqSort s)
268 {
269 Debug.Assert(s != null);
270 return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
271 }
272
276 public ArraySort MkArraySort(Sort domain, Sort range)
277 {
278 Debug.Assert(domain != null);
279 Debug.Assert(range != null);
280
281 CheckContextMatch(domain);
282 CheckContextMatch(range);
283 return new ArraySort(this, domain, range);
284 }
285
289 public ArraySort MkArraySort(Sort[] domain, Sort range)
290 {
291 Debug.Assert(domain != null);
292 Debug.Assert(range != null);
293
294 CheckContextMatch<Sort>(domain);
295 CheckContextMatch(range);
296 return new ArraySort(this, domain, range);
297 }
298
302 public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
303 {
304 Debug.Assert(name != null);
305 Debug.Assert(fieldNames != null);
306 Debug.Assert(fieldNames.All(fn => fn != null));
307 Debug.Assert(fieldSorts == null || fieldSorts.All(fs => fs != null));
308
309 CheckContextMatch(name);
310 CheckContextMatch<Symbol>(fieldNames);
311 CheckContextMatch<Sort>(fieldSorts);
312 return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
313 }
314
318 public EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
319 {
320 Debug.Assert(name != null);
321 Debug.Assert(enumNames != null);
322 Debug.Assert(enumNames.All(f => f != null));
323
324
325 CheckContextMatch(name);
326 CheckContextMatch<Symbol>(enumNames);
327 return new EnumSort(this, name, enumNames);
328 }
329
333 public EnumSort MkEnumSort(string name, params string[] enumNames)
334 {
335 Debug.Assert(enumNames != null);
336
337 var enumSymbols = MkSymbols(enumNames);
338 try
339 {
340 using var symbol = MkSymbol(name);
341 return new EnumSort(this, symbol, enumSymbols);
342 }
343 finally
344 {
345 foreach (var enumSymbol in enumSymbols)
346 enumSymbol.Dispose();
347 }
348 }
349
353 public ListSort MkListSort(Symbol name, Sort elemSort)
354 {
355 Debug.Assert(name != null);
356 Debug.Assert(elemSort != null);
357
358 CheckContextMatch(name);
359 CheckContextMatch(elemSort);
360 return new ListSort(this, name, elemSort);
361 }
362
366 public ListSort MkListSort(string name, Sort elemSort)
367 {
368 Debug.Assert(elemSort != null);
369
370 CheckContextMatch(elemSort);
371 using var symbol = MkSymbol(name);
372 return new ListSort(this, symbol, elemSort);
373 }
374
381 public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
382 {
383 Debug.Assert(name != null);
384
385 CheckContextMatch(name);
386 return new FiniteDomainSort(this, name, size);
387 }
388
397 public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
398 {
399 using var symbol = MkSymbol(name);
400 return new FiniteDomainSort(this, symbol, size);
401 }
402
403
404 #region Datatypes
415 public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
416 {
417 Debug.Assert(name != null);
418 Debug.Assert(recognizer != null);
419
420 return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
421 }
422
432 public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
433 {
434
435 using var nameSymbol = MkSymbol(name);
436 using var recognizerSymbol = MkSymbol(recognizer);
437 var fieldSymbols = MkSymbols(fieldNames);
438 try
439 {
440 return new Constructor(this, nameSymbol, recognizerSymbol, fieldSymbols, sorts, sortRefs);
441 }
442 finally
443 {
444 foreach (var fieldSymbol in fieldSymbols)
445 fieldSymbol.Dispose();
446 }
447 }
448
452 public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
453 {
454 Debug.Assert(name != null);
455 Debug.Assert(constructors != null);
456 Debug.Assert(constructors.All(c => c != null));
457
458
459 CheckContextMatch(name);
460 CheckContextMatch<Constructor>(constructors);
461 return new DatatypeSort(this, name, constructors);
462 }
463
467 public DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
468 {
469 Debug.Assert(constructors != null);
470 Debug.Assert(constructors.All(c => c != null));
471
472 CheckContextMatch<Constructor>(constructors);
473 using var symbol = MkSymbol(name);
474 return new DatatypeSort(this, symbol, constructors);
475 }
476
483 public DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters = null)
484 {
485 Debug.Assert(name != null);
486 CheckContextMatch(name);
487 if (parameters != null)
488 CheckContextMatch<Sort>(parameters);
489
490 var numParams = (parameters == null) ? 0 : (uint)parameters.Length;
491 var paramsNative = (parameters == null) ? null : AST.ArrayToNative(parameters);
492 return new DatatypeSort(this, Native.Z3_mk_datatype_sort(nCtx, name.NativeObject, numParams, paramsNative));
493 }
494
501 public DatatypeSort MkDatatypeSortRef(string name, Sort[] parameters = null)
502 {
503 using var symbol = MkSymbol(name);
504 return MkDatatypeSortRef(symbol, parameters);
505 }
506
512 public DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
513 {
514 Debug.Assert(names != null);
515 Debug.Assert(c != null);
516 Debug.Assert(names.Length == c.Length);
517 //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
518 Debug.Assert(names.All(name => name != null));
519
520 CheckContextMatch<Symbol>(names);
521 uint n = (uint)names.Length;
522 ConstructorList[] cla = new ConstructorList[n];
523 IntPtr[] n_constr = new IntPtr[n];
524 for (uint i = 0; i < n; i++)
525 {
526 Constructor[] constructor = c[i];
527 CheckContextMatch<Constructor>(constructor);
528 cla[i] = new ConstructorList(this, constructor);
529 n_constr[i] = cla[i].NativeObject;
530 }
531 IntPtr[] n_res = new IntPtr[n];
532 Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
533 DatatypeSort[] res = new DatatypeSort[n];
534 for (uint i = 0; i < n; i++)
535 res[i] = new DatatypeSort(this, n_res[i]);
536 return res;
537 }
538
545 public DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
546 {
547 Debug.Assert(names != null);
548 Debug.Assert(c != null);
549 Debug.Assert(names.Length == c.Length);
550 //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
551 //Debug.Assert(names.All(name => name != null));
552
553 var symbols = MkSymbols(names);
554 try
555 {
556 return MkDatatypeSorts(symbols, c);
557 }
558 finally
559 {
560 foreach (var symbol in symbols)
561 symbol.Dispose();
562 }
563 }
564
571 public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
572 {
573 return Expr.Create(this, Native.Z3_datatype_update_field(
574 nCtx, field.NativeObject,
575 t.NativeObject, v.NativeObject));
576 }
577
578 #endregion
579 #endregion
580
581 #region Function Declarations
585 public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
586 {
587 Debug.Assert(name != null);
588 Debug.Assert(range != null);
589 Debug.Assert(domain.All(d => d != null));
590
591 CheckContextMatch(name);
592 CheckContextMatch<Sort>(domain);
593 CheckContextMatch(range);
594 return new FuncDecl(this, name, domain, range);
595 }
596
600 public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
601 {
602 Debug.Assert(name != null);
603 Debug.Assert(domain != null);
604 Debug.Assert(range != null);
605
606 CheckContextMatch(name);
607 CheckContextMatch(domain);
608 CheckContextMatch(range);
609 Sort[] q = new Sort[] { domain };
610 return new FuncDecl(this, name, q, range);
611 }
612
616 public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
617 {
618 Debug.Assert(range != null);
619 Debug.Assert(domain.All(d => d != null));
620
621 CheckContextMatch<Sort>(domain);
622 CheckContextMatch(range);
623 using var symbol = MkSymbol(name);
624 return new FuncDecl(this, symbol, domain, range);
625 }
626
630 public FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
631 {
632 Debug.Assert(range != null);
633 Debug.Assert(domain.All(d => d != null));
634
635 CheckContextMatch<Sort>(domain);
636 CheckContextMatch(range);
637 using var symbol = MkSymbol(name);
638 return new FuncDecl(this, symbol, domain, range, true);
639 }
640
647 public void AddRecDef(FuncDecl f, Expr[] args, Expr body)
648 {
649 CheckContextMatch(f);
650 CheckContextMatch<Expr>(args);
651 CheckContextMatch(body);
652 IntPtr[] argsNative = AST.ArrayToNative(args);
653 Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
654 }
655
659 public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
660 {
661 Debug.Assert(range != null);
662 Debug.Assert(domain != null);
663
664 CheckContextMatch(domain);
665 CheckContextMatch(range);
666 using var symbol = MkSymbol(name);
667 Sort[] q = new Sort[] { domain };
668 return new FuncDecl(this, symbol, q, range);
669 }
670
676 public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
677 {
678 Debug.Assert(range != null);
679 Debug.Assert(domain.All(d => d != null));
680
681 CheckContextMatch<Sort>(domain);
682 CheckContextMatch(range);
683 return new FuncDecl(this, prefix, domain, range);
684 }
685
689 public FuncDecl MkConstDecl(Symbol name, Sort range)
690 {
691 Debug.Assert(name != null);
692 Debug.Assert(range != null);
693
694 CheckContextMatch(name);
695 CheckContextMatch(range);
696 return new FuncDecl(this, name, null, range);
697 }
698
702 public FuncDecl MkConstDecl(string name, Sort range)
703 {
704 Debug.Assert(range != null);
705
706 CheckContextMatch(range);
707 using var symbol = MkSymbol(name);
708 return new FuncDecl(this, symbol, null, range);
709 }
710
716 public FuncDecl MkFreshConstDecl(string prefix, Sort range)
717 {
718 Debug.Assert(range != null);
719
720 CheckContextMatch(range);
721 return new FuncDecl(this, prefix, null, range);
722 }
723
727 public FuncDecl MkUserPropagatorFuncDecl(string name, Sort[] domain, Sort range)
728 {
729 using var _name = MkSymbol(name);
730 var fn = Native.Z3_solver_propagate_declare(nCtx, _name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject);
731 return new FuncDecl(this, fn);
732 }
733 #endregion
734
735 #region Bound Variables
741 public Expr MkBound(uint index, Sort ty)
742 {
743 Debug.Assert(ty != null);
744
745 return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
746 }
747 #endregion
748
749 #region Quantifier Patterns
753 public Pattern MkPattern(params Expr[] terms)
754 {
755 Debug.Assert(terms != null);
756 if (terms.Length == 0)
757 throw new Z3Exception("Cannot create a pattern from zero terms");
758
759 IntPtr[] termsNative = AST.ArrayToNative(terms);
760 return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
761 }
762 #endregion
763
764 #region Constants
768 public Expr MkConst(Symbol name, Sort range)
769 {
770 Debug.Assert(name != null);
771 Debug.Assert(range != null);
772
773 CheckContextMatch(name);
774 CheckContextMatch(range);
775
776 return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
777 }
778
782 public Expr MkConst(string name, Sort range)
783 {
784 Debug.Assert(range != null);
785
786 using var symbol = MkSymbol(name);
787 return MkConst(symbol, range);
788 }
789
794 public Expr MkFreshConst(string prefix, Sort range)
795 {
796 Debug.Assert(range != null);
797
798 CheckContextMatch(range);
799 return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
800 }
801
806 public Expr MkConst(FuncDecl f)
807 {
808 Debug.Assert(f != null);
809
810 return MkApp(f);
811 }
812
816 public BoolExpr MkBoolConst(Symbol name)
817 {
818 Debug.Assert(name != null);
819
820 return (BoolExpr)MkConst(name, BoolSort);
821 }
822
826 public BoolExpr MkBoolConst(string name)
827 {
828 using var symbol = MkSymbol(name);
829 return (BoolExpr)MkConst(symbol, BoolSort);
830 }
831
835 public IntExpr MkIntConst(Symbol name)
836 {
837 Debug.Assert(name != null);
838
839 return (IntExpr)MkConst(name, IntSort);
840 }
841
845 public IntExpr MkIntConst(string name)
846 {
847 Debug.Assert(name != null);
848
849 return (IntExpr)MkConst(name, IntSort);
850 }
851
855 public RealExpr MkRealConst(Symbol name)
856 {
857 Debug.Assert(name != null);
858
859 return (RealExpr)MkConst(name, RealSort);
860 }
861
865 public RealExpr MkRealConst(string name)
866 {
867
868 return (RealExpr)MkConst(name, RealSort);
869 }
870
874 public BitVecExpr MkBVConst(Symbol name, uint size)
875 {
876 Debug.Assert(name != null);
877
878 using var sort = MkBitVecSort(size);
879 return (BitVecExpr)MkConst(name, sort);
880 }
881
885 public BitVecExpr MkBVConst(string name, uint size)
886 {
887 using var sort = MkBitVecSort(size);
888 return (BitVecExpr)MkConst(name, sort);
889 }
890 #endregion
891
892 #region Terms
896 public Expr MkApp(FuncDecl f, params Expr[] args)
897 {
898 Debug.Assert(f != null);
899 Debug.Assert(args == null || args.All(a => a != null));
900 CheckContextMatch(f);
901 CheckContextMatch<Expr>(args);
902 return Expr.Create(this, f, args);
903 }
904
908 public Expr MkApp(FuncDecl f, IEnumerable<Expr> args)
909 {
910 Debug.Assert(f != null);
911 return MkApp(f, args?.ToArray());
912 }
913
914 #region Propositional
918 public BoolExpr MkTrue()
919 {
920 return new BoolExpr(this, Native.Z3_mk_true(nCtx));
921 }
922
926 public BoolExpr MkFalse()
927 {
928 return new BoolExpr(this, Native.Z3_mk_false(nCtx));
929 }
930
934 public BoolExpr MkBool(bool value)
935 {
936 return value ? MkTrue() : MkFalse();
937 }
938
942 public BoolExpr MkEq(Expr x, Expr y)
943 {
944 Debug.Assert(x != null);
945 Debug.Assert(y != null);
946
947 CheckContextMatch(x);
948 CheckContextMatch(y);
949 return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
950 }
951
955 public BoolExpr MkDistinct(params Expr[] args)
956 {
957 Debug.Assert(args != null);
958 Debug.Assert(args.All(a => a != null));
959
960 CheckContextMatch<Expr>(args);
961 return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
962 }
963
967 public BoolExpr MkDistinct(IEnumerable<Expr> args)
968 {
969 Debug.Assert(args != null);
970 return MkDistinct(args.ToArray());
971 }
972
976 public BoolExpr MkNot(BoolExpr a)
977 {
978 Debug.Assert(a != null);
979 CheckContextMatch(a);
980 return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
981 }
982
989 public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
990 {
991 Debug.Assert(t1 != null);
992 Debug.Assert(t2 != null);
993 Debug.Assert(t3 != null);
994
995 CheckContextMatch(t1);
996 CheckContextMatch(t2);
997 CheckContextMatch(t3);
998 return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
999 }
1000
1004 public BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
1005 {
1006 Debug.Assert(t1 != null);
1007 Debug.Assert(t2 != null);
1008
1009 CheckContextMatch(t1);
1010 CheckContextMatch(t2);
1011 return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
1012 }
1013
1017 public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
1018 {
1019 Debug.Assert(t1 != null);
1020 Debug.Assert(t2 != null);
1021
1022 CheckContextMatch(t1);
1023 CheckContextMatch(t2);
1024 return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
1025 }
1026
1030 public BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
1031 {
1032 Debug.Assert(t1 != null);
1033 Debug.Assert(t2 != null);
1034
1035 CheckContextMatch(t1);
1036 CheckContextMatch(t2);
1037 return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
1038 }
1039
1043 public BoolExpr MkXor(IEnumerable<BoolExpr> args)
1044 {
1045 Debug.Assert(args != null);
1046 var ts = args.ToArray();
1047 Debug.Assert(ts.All(a => a != null));
1048 CheckContextMatch<BoolExpr>(ts);
1049
1050 return ts.Aggregate(MkFalse(), (r, t) =>
1051 {
1052 using (r)
1053 return MkXor(r, t);
1054 });
1055 }
1056
1060 public BoolExpr MkAnd(params BoolExpr[] ts)
1061 {
1062 Debug.Assert(ts != null);
1063 Debug.Assert(ts.All(a => a != null));
1064
1065 CheckContextMatch<BoolExpr>(ts);
1066 return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1067 }
1068
1072 public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
1073 {
1074 Debug.Assert(t != null);
1075 return MkAnd(t.ToArray());
1076 }
1077
1081 public BoolExpr MkOr(params BoolExpr[] ts)
1082 {
1083 Debug.Assert(ts != null);
1084 Debug.Assert(ts.All(a => a != null));
1085
1086 CheckContextMatch<BoolExpr>(ts);
1087 return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1088 }
1089
1090
1094 public BoolExpr MkOr(IEnumerable<BoolExpr> ts)
1095 {
1096 Debug.Assert(ts != null);
1097 return MkOr(ts.ToArray());
1098 }
1099
1100 #endregion
1101
1102 #region Arithmetic
1106 public ArithExpr MkAdd(params ArithExpr[] ts)
1107 {
1108 Debug.Assert(ts != null);
1109 Debug.Assert(ts.All(a => a != null));
1110
1111 CheckContextMatch<ArithExpr>(ts);
1112 return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1113 }
1114
1118 public ArithExpr MkAdd(IEnumerable<ArithExpr> ts)
1119 {
1120 Debug.Assert(ts != null);
1121 return MkAdd(ts.ToArray());
1122 }
1123
1127 public ArithExpr MkMul(params ArithExpr[] ts)
1128 {
1129 Debug.Assert(ts != null);
1130 Debug.Assert(ts.All(a => a != null));
1131
1132 CheckContextMatch<ArithExpr>(ts);
1133 return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1134 }
1135
1139 public ArithExpr MkMul(IEnumerable<ArithExpr> ts)
1140 {
1141 Debug.Assert(ts != null);
1142 return MkMul(ts.ToArray());
1143 }
1144
1148 public ArithExpr MkSub(params ArithExpr[] ts)
1149 {
1150 Debug.Assert(ts != null);
1151 Debug.Assert(ts.All(a => a != null));
1152
1153 CheckContextMatch<ArithExpr>(ts);
1154 return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1155 }
1156
1160 public ArithExpr MkUnaryMinus(ArithExpr t)
1161 {
1162 Debug.Assert(t != null);
1163
1164 CheckContextMatch(t);
1165 return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
1166 }
1167
1171 public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
1172 {
1173 Debug.Assert(t1 != null);
1174 Debug.Assert(t2 != null);
1175
1176 CheckContextMatch(t1);
1177 CheckContextMatch(t2);
1178 return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1179 }
1180
1185 public IntExpr MkMod(IntExpr t1, IntExpr t2)
1186 {
1187 Debug.Assert(t1 != null);
1188 Debug.Assert(t2 != null);
1189
1190 CheckContextMatch(t1);
1191 CheckContextMatch(t2);
1192 return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1193 }
1194
1199 public IntExpr MkRem(IntExpr t1, IntExpr t2)
1200 {
1201 Debug.Assert(t1 != null);
1202 Debug.Assert(t2 != null);
1203
1204 CheckContextMatch(t1);
1205 CheckContextMatch(t2);
1206 return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1207 }
1208
1212 public ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
1213 {
1214 Debug.Assert(t1 != null);
1215 Debug.Assert(t2 != null);
1216
1217 CheckContextMatch(t1);
1218 CheckContextMatch(t2);
1219 return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1220 }
1221
1225 public BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
1226 {
1227 Debug.Assert(t1 != null);
1228 Debug.Assert(t2 != null);
1229
1230 CheckContextMatch(t1);
1231 CheckContextMatch(t2);
1232 return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1233 }
1234
1238 public BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
1239 {
1240 Debug.Assert(t1 != null);
1241 Debug.Assert(t2 != null);
1242
1243 CheckContextMatch(t1);
1244 CheckContextMatch(t2);
1245 return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1246 }
1247
1251 public BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
1252 {
1253 Debug.Assert(t1 != null);
1254 Debug.Assert(t2 != null);
1255
1256 CheckContextMatch(t1);
1257 CheckContextMatch(t2);
1258 return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1259 }
1260
1264 public BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
1265 {
1266 Debug.Assert(t1 != null);
1267 Debug.Assert(t2 != null);
1268
1269 CheckContextMatch(t1);
1270 CheckContextMatch(t2);
1271 return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1272 }
1273
1284 public RealExpr MkInt2Real(IntExpr t)
1285 {
1286 Debug.Assert(t != null);
1287
1288 CheckContextMatch(t);
1289 return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1290 }
1291
1299 public IntExpr MkReal2Int(RealExpr t)
1300 {
1301 Debug.Assert(t != null);
1302
1303 CheckContextMatch(t);
1304 return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1305 }
1306
1310 public BoolExpr MkIsInteger(RealExpr t)
1311 {
1312 Debug.Assert(t != null);
1313
1314 CheckContextMatch(t);
1315 return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1316 }
1317 #endregion
1318
1319 #region Bit-vectors
1324 public BitVecExpr MkBVNot(BitVecExpr t)
1325 {
1326 Debug.Assert(t != null);
1327
1328 CheckContextMatch(t);
1329 return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1330 }
1331
1336 public BitVecExpr MkBVRedAND(BitVecExpr t)
1337 {
1338 Debug.Assert(t != null);
1339
1340 CheckContextMatch(t);
1341 return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1342 }
1343
1348 public BitVecExpr MkBVRedOR(BitVecExpr t)
1349 {
1350 Debug.Assert(t != null);
1351
1352 CheckContextMatch(t);
1353 return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1354 }
1355
1360 public BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
1361 {
1362 Debug.Assert(t1 != null);
1363 Debug.Assert(t2 != null);
1364
1365 CheckContextMatch(t1);
1366 CheckContextMatch(t2);
1367 return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1368 }
1369
1374 public BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
1375 {
1376 Debug.Assert(t1 != null);
1377 Debug.Assert(t2 != null);
1378
1379 CheckContextMatch(t1);
1380 CheckContextMatch(t2);
1381 return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1382 }
1383
1388 public BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
1389 {
1390 Debug.Assert(t1 != null);
1391 Debug.Assert(t2 != null);
1392
1393 CheckContextMatch(t1);
1394 CheckContextMatch(t2);
1395 return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1396 }
1397
1402 public BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
1403 {
1404 Debug.Assert(t1 != null);
1405 Debug.Assert(t2 != null);
1406
1407 CheckContextMatch(t1);
1408 CheckContextMatch(t2);
1409 return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1410 }
1411
1416 public BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
1417 {
1418 Debug.Assert(t1 != null);
1419 Debug.Assert(t2 != null);
1420
1421 CheckContextMatch(t1);
1422 CheckContextMatch(t2);
1423 return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1424 }
1425
1430 public BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
1431 {
1432 Debug.Assert(t1 != null);
1433 Debug.Assert(t2 != null);
1434
1435 CheckContextMatch(t1);
1436 CheckContextMatch(t2);
1437 return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1438 }
1439
1444 public BitVecExpr MkBVNeg(BitVecExpr t)
1445 {
1446 Debug.Assert(t != null);
1447
1448 CheckContextMatch(t);
1449 return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1450 }
1451
1456 public BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
1457 {
1458 Debug.Assert(t1 != null);
1459 Debug.Assert(t2 != null);
1460
1461 CheckContextMatch(t1);
1462 CheckContextMatch(t2);
1463 return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1464 }
1465
1470 public BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
1471 {
1472 Debug.Assert(t1 != null);
1473 Debug.Assert(t2 != null);
1474
1475 CheckContextMatch(t1);
1476 CheckContextMatch(t2);
1477 return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1478 }
1479
1484 public BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
1485 {
1486 Debug.Assert(t1 != null);
1487 Debug.Assert(t2 != null);
1488
1489 CheckContextMatch(t1);
1490 CheckContextMatch(t2);
1491 return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1492 }
1493
1503 public BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
1504 {
1505 Debug.Assert(t1 != null);
1506 Debug.Assert(t2 != null);
1507
1508 CheckContextMatch(t1);
1509 CheckContextMatch(t2);
1510 return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1511 }
1512
1526 public BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
1527 {
1528 Debug.Assert(t1 != null);
1529 Debug.Assert(t2 != null);
1530
1531 CheckContextMatch(t1);
1532 CheckContextMatch(t2);
1533 return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1534 }
1535
1544 public BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
1545 {
1546 Debug.Assert(t1 != null);
1547 Debug.Assert(t2 != null);
1548
1549 CheckContextMatch(t1);
1550 CheckContextMatch(t2);
1551 return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1552 }
1553
1564 public BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
1565 {
1566 Debug.Assert(t1 != null);
1567 Debug.Assert(t2 != null);
1568
1569 CheckContextMatch(t1);
1570 CheckContextMatch(t2);
1571 return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1572 }
1573
1581 public BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
1582 {
1583 Debug.Assert(t1 != null);
1584 Debug.Assert(t2 != null);
1585
1586 CheckContextMatch(t1);
1587 CheckContextMatch(t2);
1588 return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1589 }
1590
1597 public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
1598 {
1599 Debug.Assert(t1 != null);
1600 Debug.Assert(t2 != null);
1601
1602 CheckContextMatch(t1);
1603 CheckContextMatch(t2);
1604 return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1605 }
1606
1613 public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
1614 {
1615 Debug.Assert(t1 != null);
1616 Debug.Assert(t2 != null);
1617
1618 CheckContextMatch(t1);
1619 CheckContextMatch(t2);
1620 return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1621 }
1622
1629 public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
1630 {
1631 Debug.Assert(t1 != null);
1632 Debug.Assert(t2 != null);
1633
1634 CheckContextMatch(t1);
1635 CheckContextMatch(t2);
1636 return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1637 }
1638
1645 public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
1646 {
1647 Debug.Assert(t1 != null);
1648 Debug.Assert(t2 != null);
1649
1650 CheckContextMatch(t1);
1651 CheckContextMatch(t2);
1652 return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1653 }
1654
1661 public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
1662 {
1663 Debug.Assert(t1 != null);
1664 Debug.Assert(t2 != null);
1665
1666 CheckContextMatch(t1);
1667 CheckContextMatch(t2);
1668 return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1669 }
1670
1677 public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
1678 {
1679 Debug.Assert(t1 != null);
1680 Debug.Assert(t2 != null);
1681
1682 CheckContextMatch(t1);
1683 CheckContextMatch(t2);
1684 return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1685 }
1686
1693 public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
1694 {
1695 Debug.Assert(t1 != null);
1696 Debug.Assert(t2 != null);
1697
1698 CheckContextMatch(t1);
1699 CheckContextMatch(t2);
1700 return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1701 }
1702
1709 public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
1710 {
1711 Debug.Assert(t1 != null);
1712 Debug.Assert(t2 != null);
1713
1714 CheckContextMatch(t1);
1715 CheckContextMatch(t2);
1716 return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1717 }
1718
1729 public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
1730 {
1731 Debug.Assert(t1 != null);
1732 Debug.Assert(t2 != null);
1733
1734 CheckContextMatch(t1);
1735 CheckContextMatch(t2);
1736 return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1737 }
1738
1748 public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
1749 {
1750 Debug.Assert(t != null);
1751
1752 CheckContextMatch(t);
1753 return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1754 }
1755
1764 public BitVecExpr MkSignExt(uint i, BitVecExpr t)
1765 {
1766 Debug.Assert(t != null);
1767
1768 CheckContextMatch(t);
1769 return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1770 }
1771
1781 public BitVecExpr MkZeroExt(uint i, BitVecExpr t)
1782 {
1783 Debug.Assert(t != null);
1784
1785 CheckContextMatch(t);
1786 return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1787 }
1788
1795 public BitVecExpr MkRepeat(uint i, BitVecExpr t)
1796 {
1797 Debug.Assert(t != null);
1798
1799 CheckContextMatch(t);
1800 return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1801 }
1802
1815 public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
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_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1823 }
1824
1837 public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
1838 {
1839 Debug.Assert(t1 != null);
1840 Debug.Assert(t2 != null);
1841
1842 CheckContextMatch(t1);
1843 CheckContextMatch(t2);
1844 return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1845 }
1846
1861 public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
1862 {
1863 Debug.Assert(t1 != null);
1864 Debug.Assert(t2 != null);
1865
1866 CheckContextMatch(t1);
1867 CheckContextMatch(t2);
1868 return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1869 }
1870
1878 public BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
1879 {
1880 Debug.Assert(t != null);
1881
1882 CheckContextMatch(t);
1883 return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1884 }
1885
1893 public BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
1894 {
1895 Debug.Assert(t != null);
1896
1897 CheckContextMatch(t);
1898 return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1899 }
1900
1908 public BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
1909 {
1910 Debug.Assert(t1 != null);
1911 Debug.Assert(t2 != null);
1912
1913 CheckContextMatch(t1);
1914 CheckContextMatch(t2);
1915 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1916 }
1917
1925 public BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
1926 {
1927 Debug.Assert(t1 != null);
1928 Debug.Assert(t2 != null);
1929
1930 CheckContextMatch(t1);
1931 CheckContextMatch(t2);
1932 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1933 }
1934
1945 public BitVecExpr MkInt2BV(uint n, IntExpr t)
1946 {
1947 Debug.Assert(t != null);
1948
1949 CheckContextMatch(t);
1950 return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1951 }
1952
1968 public IntExpr MkBV2Int(BitVecExpr t, bool signed)
1969 {
1970 Debug.Assert(t != null);
1971
1972 CheckContextMatch(t);
1973 return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (byte)(signed ? 1 : 0)));
1974 }
1975
1982 public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1983 {
1984 Debug.Assert(t1 != null);
1985 Debug.Assert(t2 != null);
1986
1987 CheckContextMatch(t1);
1988 CheckContextMatch(t2);
1989 return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
1990 }
1991
1998 public BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
1999 {
2000 Debug.Assert(t1 != null);
2001 Debug.Assert(t2 != null);
2002
2003 CheckContextMatch(t1);
2004 CheckContextMatch(t2);
2005 return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2006 }
2007
2014 public BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
2015 {
2016 Debug.Assert(t1 != null);
2017 Debug.Assert(t2 != null);
2018
2019 CheckContextMatch(t1);
2020 CheckContextMatch(t2);
2021 return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2022 }
2023
2030 public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
2031 {
2032 Debug.Assert(t1 != null);
2033 Debug.Assert(t2 != null);
2034
2035 CheckContextMatch(t1);
2036 CheckContextMatch(t2);
2037 return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
2038 }
2039
2046 public BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
2047 {
2048 Debug.Assert(t1 != null);
2049 Debug.Assert(t2 != null);
2050
2051 CheckContextMatch(t1);
2052 CheckContextMatch(t2);
2053 return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2054 }
2055
2062 public BoolExpr MkBVNegNoOverflow(BitVecExpr t)
2063 {
2064 Debug.Assert(t != null);
2065
2066 CheckContextMatch(t);
2067 return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
2068 }
2069
2076 public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
2077 {
2078 Debug.Assert(t1 != null);
2079 Debug.Assert(t2 != null);
2080
2081 CheckContextMatch(t1);
2082 CheckContextMatch(t2);
2083 return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
2084 }
2085
2092 public BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
2093 {
2094 Debug.Assert(t1 != null);
2095 Debug.Assert(t2 != null);
2096
2097 CheckContextMatch(t1);
2098 CheckContextMatch(t2);
2099 return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2100 }
2101 #endregion
2102
2103 #region Arrays
2107 public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
2108 {
2109 Debug.Assert(name != null);
2110 Debug.Assert(domain != null);
2111 Debug.Assert(range != null);
2112
2113 using var sort = MkArraySort(domain, range);
2114 return (ArrayExpr)MkConst(name, sort);
2115 }
2116
2120 public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
2121 {
2122 Debug.Assert(domain != null);
2123 Debug.Assert(range != null);
2124
2125 using var symbol = MkSymbol(name);
2126 using var sort = MkArraySort(domain, range);
2127 return (ArrayExpr)MkConst(symbol, sort);
2128 }
2129
2130
2144 public Expr MkSelect(ArrayExpr a, Expr i)
2145 {
2146 Debug.Assert(a != null);
2147 Debug.Assert(i != null);
2148
2149 CheckContextMatch(a);
2150 CheckContextMatch(i);
2151 return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2152 }
2153
2167 public Expr MkSelect(ArrayExpr a, params Expr[] args)
2168 {
2169 Debug.Assert(a != null);
2170 Debug.Assert(args != null && args.All(n => n != null));
2171
2172 CheckContextMatch(a);
2173 CheckContextMatch<Expr>(args);
2174 return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2175 }
2176
2177
2196 public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
2197 {
2198 Debug.Assert(a != null);
2199 Debug.Assert(i != null);
2200 Debug.Assert(v != null);
2201
2202 CheckContextMatch(a);
2203 CheckContextMatch(i);
2204 CheckContextMatch(v);
2205 return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2206 }
2207
2226 public ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
2227 {
2228 Debug.Assert(a != null);
2229 Debug.Assert(args != null);
2230 Debug.Assert(v != null);
2231
2232 CheckContextMatch<Expr>(args);
2233 CheckContextMatch(a);
2234 CheckContextMatch(v);
2235 return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
2236 }
2237
2247 public ArrayExpr MkConstArray(Sort domain, Expr v)
2248 {
2249 Debug.Assert(domain != null);
2250 Debug.Assert(v != null);
2251
2252 CheckContextMatch(domain);
2253 CheckContextMatch(v);
2254 return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2255 }
2256
2268 public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
2269 {
2270 Debug.Assert(f != null);
2271 Debug.Assert(args == null || args.All(a => a != null));
2272
2273 CheckContextMatch(f);
2274 CheckContextMatch<ArrayExpr>(args);
2275 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2276 }
2277
2285 public Expr MkTermArray(ArrayExpr array)
2286 {
2287 Debug.Assert(array != null);
2288
2289 CheckContextMatch(array);
2290 return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2291 }
2292
2296 public Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
2297 {
2298 Debug.Assert(arg1 != null);
2299 Debug.Assert(arg2 != null);
2300
2301 CheckContextMatch(arg1);
2302 CheckContextMatch(arg2);
2303 return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
2304 }
2305
2306 #endregion
2307
2308 #region Sets
2312 public SetSort MkSetSort(Sort ty)
2313 {
2314 Debug.Assert(ty != null);
2315
2316 CheckContextMatch(ty);
2317 return new SetSort(this, ty);
2318 }
2319
2323 public ArrayExpr MkEmptySet(Sort domain)
2324 {
2325 Debug.Assert(domain != null);
2326
2327 CheckContextMatch(domain);
2328 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2329 }
2330
2334 public ArrayExpr MkFullSet(Sort domain)
2335 {
2336 Debug.Assert(domain != null);
2337
2338 CheckContextMatch(domain);
2339 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2340 }
2341
2345 public ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
2346 {
2347 Debug.Assert(set != null);
2348 Debug.Assert(element != null);
2349
2350 CheckContextMatch(set);
2351 CheckContextMatch(element);
2352 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2353 }
2354
2355
2359 public ArrayExpr MkSetDel(ArrayExpr set, Expr element)
2360 {
2361 Debug.Assert(set != null);
2362 Debug.Assert(element != null);
2363
2364 CheckContextMatch(set);
2365 CheckContextMatch(element);
2366 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2367 }
2368
2372 public ArrayExpr MkSetUnion(params ArrayExpr[] args)
2373 {
2374 Debug.Assert(args != null);
2375 Debug.Assert(args.All(a => a != null));
2376
2377 CheckContextMatch<ArrayExpr>(args);
2378 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2379 }
2380
2384 public ArrayExpr MkSetIntersection(params ArrayExpr[] args)
2385 {
2386 Debug.Assert(args != null);
2387 Debug.Assert(args.All(a => a != null));
2388
2389 CheckContextMatch<ArrayExpr>(args);
2390 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2391 }
2392
2396 public ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
2397 {
2398 Debug.Assert(arg1 != null);
2399 Debug.Assert(arg2 != null);
2400
2401 CheckContextMatch(arg1);
2402 CheckContextMatch(arg2);
2403 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2404 }
2405
2409 public ArrayExpr MkSetComplement(ArrayExpr arg)
2410 {
2411 Debug.Assert(arg != null);
2412
2413 CheckContextMatch(arg);
2414 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2415 }
2416
2420 public BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
2421 {
2422 Debug.Assert(elem != null);
2423 Debug.Assert(set != null);
2424
2425 CheckContextMatch(elem);
2426 CheckContextMatch(set);
2427 return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2428 }
2429
2433 public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
2434 {
2435 Debug.Assert(arg1 != null);
2436 Debug.Assert(arg2 != null);
2437
2438 CheckContextMatch(arg1);
2439 CheckContextMatch(arg2);
2440 return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2441 }
2442
2443 #endregion
2444
2445 #region Sequence, string and regular expressions
2446
2450 public SeqExpr MkEmptySeq(Sort s)
2451 {
2452 Debug.Assert(s != null);
2453 return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
2454 }
2455
2459 public SeqExpr MkUnit(Expr elem)
2460 {
2461 Debug.Assert(elem != null);
2462 return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
2463 }
2464
2468 public SeqExpr MkString(string s)
2469 {
2470 Debug.Assert(s != null);
2471 return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
2472 }
2473
2477 public SeqExpr IntToString(Expr e)
2478 {
2479 Debug.Assert(e != null);
2480 Debug.Assert(e is ArithExpr);
2481 return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
2482 }
2483
2487 public SeqExpr UbvToString(Expr e)
2488 {
2489 Debug.Assert(e != null);
2490 Debug.Assert(e is ArithExpr);
2491 return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject));
2492 }
2493
2497 public SeqExpr SbvToString(Expr e)
2498 {
2499 Debug.Assert(e != null);
2500 Debug.Assert(e is ArithExpr);
2501 return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject));
2502 }
2503
2507 public IntExpr StringToInt(Expr e)
2508 {
2509 Debug.Assert(e != null);
2510 Debug.Assert(e is SeqExpr);
2511 return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject));
2512 }
2513
2514
2518 public SeqExpr MkConcat(params SeqExpr[] t)
2519 {
2520 Debug.Assert(t != null);
2521 Debug.Assert(t.All(a => a != null));
2522
2523 CheckContextMatch<SeqExpr>(t);
2524 return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2525 }
2526
2527
2531 public IntExpr MkLength(SeqExpr s)
2532 {
2533 Debug.Assert(s != null);
2534 return (IntExpr)Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
2535 }
2536
2540 public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
2541 {
2542 Debug.Assert(s1 != null);
2543 Debug.Assert(s2 != null);
2544 CheckContextMatch(s1, s2);
2545 return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
2546 }
2547
2551 public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
2552 {
2553 Debug.Assert(s1 != null);
2554 Debug.Assert(s2 != null);
2555 CheckContextMatch(s1, s2);
2556 return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
2557 }
2558
2562 public BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
2563 {
2564 Debug.Assert(s1 != null);
2565 Debug.Assert(s2 != null);
2566 CheckContextMatch(s1, s2);
2567 return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
2568 }
2569
2573 public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
2574 {
2575 Debug.Assert(s1 != null);
2576 Debug.Assert(s2 != null);
2577 CheckContextMatch(s1, s2);
2578 return new BoolExpr(this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject));
2579 }
2580
2584 public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2)
2585 {
2586 Debug.Assert(s1 != null);
2587 Debug.Assert(s2 != null);
2588 CheckContextMatch(s1, s2);
2589 return new BoolExpr(this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject));
2590 }
2591
2595 public SeqExpr MkAt(SeqExpr s, Expr index)
2596 {
2597 Debug.Assert(s != null);
2598 Debug.Assert(index != null);
2599 CheckContextMatch(s, index);
2600 return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
2601 }
2602
2606 public Expr MkNth(SeqExpr s, Expr index)
2607 {
2608 Debug.Assert(s != null);
2609 Debug.Assert(index != null);
2610 CheckContextMatch(s, index);
2611 return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
2612 }
2613
2617 public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
2618 {
2619 Debug.Assert(s != null);
2620 Debug.Assert(offset != null);
2621 Debug.Assert(length != null);
2622 CheckContextMatch(s, offset, length);
2623 return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
2624 }
2625
2629 public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
2630 {
2631 Debug.Assert(s != null);
2632 Debug.Assert(offset != null);
2633 Debug.Assert(substr != null);
2634 CheckContextMatch(s, substr, offset);
2635 return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
2636 }
2637
2641 public SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
2642 {
2643 Debug.Assert(s != null);
2644 Debug.Assert(src != null);
2645 Debug.Assert(dst != null);
2646 CheckContextMatch(s, src, dst);
2647 return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
2648 }
2649
2653 public Expr MkSeqMap(Expr f, SeqExpr s)
2654 {
2655 Debug.Assert(f != null);
2656 Debug.Assert(s != null);
2657 CheckContextMatch(f, s);
2658 return Expr.Create(this, Native.Z3_mk_seq_map(nCtx, f.NativeObject, s.NativeObject));
2659 }
2660
2664 public Expr MkSeqMapi(Expr f, Expr i, SeqExpr s)
2665 {
2666 Debug.Assert(f != null);
2667 Debug.Assert(i != null);
2668 Debug.Assert(s != null);
2669 CheckContextMatch(f, i, s);
2670 return Expr.Create(this, Native.Z3_mk_seq_mapi(nCtx, f.NativeObject, i.NativeObject, s.NativeObject));
2671 }
2672
2676 public Expr MkSeqFoldLeft(Expr f, Expr a, SeqExpr s)
2677 {
2678 Debug.Assert(f != null);
2679 Debug.Assert(a != null);
2680 Debug.Assert(s != null);
2681 CheckContextMatch(f, a, s);
2682 return Expr.Create(this, Native.Z3_mk_seq_foldl(nCtx, f.NativeObject, a.NativeObject, s.NativeObject));
2683 }
2684
2688 public Expr MkSeqFoldLeftI(Expr f, Expr i, Expr a, SeqExpr s)
2689 {
2690 Debug.Assert(f != null);
2691 Debug.Assert(i != null);
2692 Debug.Assert(a != null);
2693 Debug.Assert(s != null);
2694 CheckContextMatch(f, i, a);
2695 CheckContextMatch(s, a);
2696 return Expr.Create(this, Native.Z3_mk_seq_foldli(nCtx, f.NativeObject, i.NativeObject, a.NativeObject, s.NativeObject));
2697 }
2698
2702 public ReExpr MkToRe(SeqExpr s)
2703 {
2704 Debug.Assert(s != null);
2705 return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));
2706 }
2707
2708
2712 public BoolExpr MkInRe(SeqExpr s, ReExpr re)
2713 {
2714 Debug.Assert(s != null);
2715 Debug.Assert(re != null);
2716 CheckContextMatch(s, re);
2717 return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
2718 }
2719
2723 public ReExpr MkStar(ReExpr re)
2724 {
2725 Debug.Assert(re != null);
2726 return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
2727 }
2728
2732 public ReExpr MkLoop(ReExpr re, uint lo, uint hi = 0)
2733 {
2734 Debug.Assert(re != null);
2735 return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi));
2736 }
2737
2741 public ReExpr MkPlus(ReExpr re)
2742 {
2743 Debug.Assert(re != null);
2744 return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));
2745 }
2746
2750 public ReExpr MkOption(ReExpr re)
2751 {
2752 Debug.Assert(re != null);
2753 return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
2754 }
2755
2759 public ReExpr MkComplement(ReExpr re)
2760 {
2761 Debug.Assert(re != null);
2762 return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject));
2763 }
2764
2768 public ReExpr MkConcat(params ReExpr[] t)
2769 {
2770 Debug.Assert(t != null);
2771 Debug.Assert(t.All(a => a != null));
2772
2773 CheckContextMatch<ReExpr>(t);
2774 return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2775 }
2776
2780 public ReExpr MkUnion(params ReExpr[] t)
2781 {
2782 Debug.Assert(t != null);
2783 Debug.Assert(t.All(a => a != null));
2784
2785 CheckContextMatch<ReExpr>(t);
2786 return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2787 }
2788
2792 public ReExpr MkIntersect(params ReExpr[] t)
2793 {
2794 Debug.Assert(t != null);
2795 Debug.Assert(t.All(a => a != null));
2796
2797 CheckContextMatch<ReExpr>(t);
2798 return new ReExpr(this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2799 }
2800
2804 public ReExpr MkDiff(ReExpr a, ReExpr b)
2805 {
2806 Debug.Assert(a != null);
2807 Debug.Assert(b != null);
2808 CheckContextMatch(a, b);
2809 return new ReExpr(this, Native.Z3_mk_re_diff(nCtx, a.NativeObject, b.NativeObject));
2810 }
2811
2816 public ReExpr MkEmptyRe(Sort s)
2817 {
2818 Debug.Assert(s != null);
2819 return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject));
2820 }
2821
2826 public ReExpr MkFullRe(Sort s)
2827 {
2828 Debug.Assert(s != null);
2829 return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject));
2830 }
2831
2832
2836 public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
2837 {
2838 Debug.Assert(lo != null);
2839 Debug.Assert(hi != null);
2840 CheckContextMatch(lo, hi);
2841 return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
2842 }
2843
2847 public BoolExpr MkCharLe(Expr ch1, Expr ch2)
2848 {
2849 Debug.Assert(ch1 != null);
2850 Debug.Assert(ch2 != null);
2851 return new BoolExpr(this, Native.Z3_mk_char_le(nCtx, ch1.NativeObject, ch2.NativeObject));
2852 }
2853
2857 public IntExpr CharToInt(Expr ch)
2858 {
2859 Debug.Assert(ch != null);
2860 return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject));
2861 }
2862
2866 public BitVecExpr CharToBV(Expr ch)
2867 {
2868 Debug.Assert(ch != null);
2869 return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject));
2870 }
2871
2875 public Expr CharFromBV(BitVecExpr bv)
2876 {
2877 Debug.Assert(bv != null);
2878 return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject));
2879 }
2880
2884 public BoolExpr MkIsDigit(Expr ch)
2885 {
2886 Debug.Assert(ch != null);
2887 return new BoolExpr(this, Native.Z3_mk_char_is_digit(nCtx, ch.NativeObject));
2888 }
2889
2890 #endregion
2891
2892 #region Pseudo-Boolean constraints
2893
2897 public BoolExpr MkAtMost(IEnumerable<BoolExpr> args, uint k)
2898 {
2899 Debug.Assert(args != null);
2900 var ts = args.ToArray();
2901 CheckContextMatch<BoolExpr>(ts);
2902 return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint)ts.Length,
2903 AST.ArrayToNative(ts), k));
2904 }
2905
2909 public BoolExpr MkAtLeast(IEnumerable<BoolExpr> args, uint k)
2910 {
2911 Debug.Assert(args != null);
2912 var ts = args.ToArray();
2913 CheckContextMatch<BoolExpr>(ts);
2914 return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint)ts.Length,
2915 AST.ArrayToNative(ts), k));
2916 }
2917
2921 public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
2922 {
2923 Debug.Assert(args != null);
2924 Debug.Assert(coeffs != null);
2925 Debug.Assert(args.Length == coeffs.Length);
2926 CheckContextMatch<BoolExpr>(args);
2927 return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint)args.Length,
2928 AST.ArrayToNative(args),
2929 coeffs, k));
2930 }
2931
2935 public BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k)
2936 {
2937 Debug.Assert(args != null);
2938 Debug.Assert(coeffs != null);
2939 Debug.Assert(args.Length == coeffs.Length);
2940 CheckContextMatch<BoolExpr>(args);
2941 return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint)args.Length,
2942 AST.ArrayToNative(args),
2943 coeffs, k));
2944 }
2948 public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
2949 {
2950 Debug.Assert(args != null);
2951 Debug.Assert(coeffs != null);
2952 Debug.Assert(args.Length == coeffs.Length);
2953 CheckContextMatch<BoolExpr>(args);
2954 return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint)args.Length,
2955 AST.ArrayToNative(args),
2956 coeffs, k));
2957 }
2958 #endregion
2959
2960 #region Numerals
2961
2962 #region General Numerals
2969 public Expr MkNumeral(string v, Sort ty)
2970 {
2971 Debug.Assert(ty != null);
2972
2973 CheckContextMatch(ty);
2974 return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2975 }
2976
2984 public Expr MkNumeral(int v, Sort ty)
2985 {
2986 Debug.Assert(ty != null);
2987
2988 CheckContextMatch(ty);
2989 return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2990 }
2991
2999 public Expr MkNumeral(uint v, Sort ty)
3000 {
3001 Debug.Assert(ty != null);
3002
3003 CheckContextMatch(ty);
3004 return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
3005 }
3006
3014 public Expr MkNumeral(long v, Sort ty)
3015 {
3016 Debug.Assert(ty != null);
3017
3018 CheckContextMatch(ty);
3019 return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
3020 }
3021
3029 public Expr MkNumeral(ulong v, Sort ty)
3030 {
3031 Debug.Assert(ty != null);
3032
3033 CheckContextMatch(ty);
3034 return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
3035 }
3036 #endregion
3037
3038 #region Reals
3046 public RatNum MkReal(int num, int den)
3047 {
3048 if (den == 0)
3049 throw new Z3Exception("Denominator is zero");
3050
3051 return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
3052 }
3053
3059 public RatNum MkReal(string v)
3060 {
3061
3062 return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
3063 }
3064
3070 public RatNum MkReal(int v)
3071 {
3072
3073 return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
3074 }
3075
3081 public RatNum MkReal(uint v)
3082 {
3083
3084 return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
3085 }
3086
3092 public RatNum MkReal(long v)
3093 {
3094
3095 return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
3096 }
3097
3103 public RatNum MkReal(ulong v)
3104 {
3105
3106 return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
3107 }
3108 #endregion
3109
3110 #region Integers
3115 public IntNum MkInt(string v)
3116 {
3117
3118 return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
3119 }
3120
3126 public IntNum MkInt(int v)
3127 {
3128
3129 return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
3130 }
3131
3137 public IntNum MkInt(uint v)
3138 {
3139
3140 return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
3141 }
3142
3148 public IntNum MkInt(long v)
3149 {
3150
3151 return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
3152 }
3153
3159 public IntNum MkInt(ulong v)
3160 {
3161
3162 return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
3163 }
3164 #endregion
3165
3166 #region Bit-vectors
3172 public BitVecNum MkBV(string v, uint size)
3173 {
3174 using var sort = MkBitVecSort(size);
3175 return (BitVecNum)MkNumeral(v, sort);
3176 }
3177
3183 public BitVecNum MkBV(int v, uint size)
3184 {
3185 using var sort = MkBitVecSort(size);
3186 return (BitVecNum)MkNumeral(v, sort);
3187 }
3188
3194 public BitVecNum MkBV(uint v, uint size)
3195 {
3196 using var sort = MkBitVecSort(size);
3197 return (BitVecNum)MkNumeral(v, sort);
3198 }
3199
3205 public BitVecNum MkBV(long v, uint size)
3206 {
3207 using var sort = MkBitVecSort(size);
3208 return (BitVecNum)MkNumeral(v, sort);
3209 }
3210
3216 public BitVecNum MkBV(ulong v, uint size)
3217 {
3218 using var sort = MkBitVecSort(size);
3219 return (BitVecNum)MkNumeral(v, sort);
3220 }
3221
3226 public BitVecNum MkBV(bool[] bits)
3227 {
3228 byte[] _bits = new byte[bits.Length];
3229 for (int i = 0; i < bits.Length; ++i) _bits[i] = (byte)(bits[i] ? 1 : 0);
3230 return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
3231 }
3232
3233
3234 #endregion
3235
3236 #endregion // Numerals
3237
3238 #region Quantifiers
3263 public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3264 {
3265 Debug.Assert(sorts != null);
3266 Debug.Assert(names != null);
3267 Debug.Assert(body != null);
3268 Debug.Assert(sorts.Length == names.Length);
3269 Debug.Assert(sorts.All(s => s != null));
3270 Debug.Assert(names.All(n => n != null));
3271 Debug.Assert(patterns == null || patterns.All(p => p != null));
3272 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3273
3274
3275 return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3276 }
3277
3278
3287 public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3288 {
3289 Debug.Assert(body != null);
3290 Debug.Assert(boundConstants == null || boundConstants.All(b => b != null));
3291 Debug.Assert(patterns == null || patterns.All(p => p != null));
3292 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3293
3294
3295 return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3296 }
3297
3305 public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3306 {
3307 Debug.Assert(sorts != null);
3308 Debug.Assert(names != null);
3309 Debug.Assert(body != null);
3310 Debug.Assert(sorts.Length == names.Length);
3311 Debug.Assert(sorts.All(s => s != null));
3312 Debug.Assert(names.All(n => n != null));
3313 Debug.Assert(patterns == null || patterns.All(p => p != null));
3314 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3315
3316 return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3317 }
3318
3327 public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3328 {
3329 Debug.Assert(body != null);
3330 Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3331 Debug.Assert(patterns == null || patterns.All(p => p != null));
3332 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3333
3334 return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3335 }
3336
3337
3342 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)
3343 {
3344 Debug.Assert(body != null);
3345 Debug.Assert(names != null);
3346 Debug.Assert(sorts != null);
3347 Debug.Assert(sorts.Length == names.Length);
3348 Debug.Assert(sorts.All(s => s != null));
3349 Debug.Assert(names.All(n => n != null));
3350 Debug.Assert(patterns == null || patterns.All(p => p != null));
3351 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3352
3353
3354 if (universal)
3355 return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3356 else
3357 return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3358 }
3359
3360
3365 public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3366 {
3367 Debug.Assert(body != null);
3368 Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3369 Debug.Assert(patterns == null || patterns.All(p => p != null));
3370 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3371
3372
3373 if (universal)
3374 return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3375 else
3376 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3377 }
3378
3397 public Lambda MkLambda(Sort[] sorts, Symbol[] names, Expr body)
3398 {
3399 Debug.Assert(sorts != null);
3400 Debug.Assert(names != null);
3401 Debug.Assert(body != null);
3402 Debug.Assert(sorts.Length == names.Length);
3403 Debug.Assert(sorts.All(s => s != null));
3404 Debug.Assert(names.All(n => n != null));
3405 return new Lambda(this, sorts, names, body);
3406 }
3407
3416 public Lambda MkLambda(Expr[] boundConstants, Expr body)
3417 {
3418 Debug.Assert(body != null);
3419 Debug.Assert(boundConstants != null && boundConstants.All(b => b != null));
3420 return new Lambda(this, boundConstants, body);
3421 }
3422
3423
3424 #endregion
3425
3426 #endregion // Expr
3427
3428 #region Options
3445 public Z3_ast_print_mode PrintMode
3446 {
3447 get { return m_print_mode; }
3448 set
3449 {
3450 Native.Z3_set_ast_print_mode(nCtx, (uint)value);
3451 m_print_mode = value;
3452 }
3453 }
3454 #endregion
3455
3456 #region SMT Files & Strings
3457
3462 public BoolExpr[] ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
3463 {
3464
3465 uint csn = Symbol.ArrayLength(sortNames);
3466 uint cs = Sort.ArrayLength(sorts);
3467 uint cdn = Symbol.ArrayLength(declNames);
3468 uint cd = AST.ArrayLength(decls);
3469 if (csn != cs || cdn != cd)
3470 throw new Z3Exception("Argument size mismatch");
3471 using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str,
3472 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3473 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3474 return assertions.ToBoolExprArray();
3475 }
3476
3481 public BoolExpr[] ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
3482 {
3483
3484 uint csn = Symbol.ArrayLength(sortNames);
3485 uint cs = Sort.ArrayLength(sorts);
3486 uint cdn = Symbol.ArrayLength(declNames);
3487 uint cd = AST.ArrayLength(decls);
3488 if (csn != cs || cdn != cd)
3489 throw new Z3Exception("Argument size mismatch");
3490 using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
3491 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3492 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3493 return assertions.ToBoolExprArray();
3494 }
3495
3506 public string BenchmarkToSmtlibString(string name, string logic, string status, string attributes, BoolExpr[] assumptions, BoolExpr formula)
3507 {
3508 Debug.Assert(assumptions != null);
3509 Debug.Assert(formula != null);
3510
3511 return Native.Z3_benchmark_to_smtlib_string(
3512 nCtx,
3513 name,
3514 logic,
3515 status,
3516 attributes,
3517 (uint)(assumptions?.Length ?? 0),
3518 AST.ArrayToNative(assumptions),
3519 formula.NativeObject);
3520 }
3521 #endregion
3522
3523 #region Goals
3534 public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
3535 {
3536
3537 return new Goal(this, models, unsatCores, proofs);
3538 }
3539 #endregion
3540
3541 #region ParameterSets
3545 public Params MkParams()
3546 {
3547
3548 return new Params(this);
3549 }
3550 #endregion
3551
3552 #region Tactics
3556 public uint NumTactics
3557 {
3558 get { return Native.Z3_get_num_tactics(nCtx); }
3559 }
3560
3564 public string[] TacticNames
3565 {
3566 get
3567 {
3568
3569 uint n = NumTactics;
3570 string[] res = new string[n];
3571 for (uint i = 0; i < n; i++)
3572 res[i] = Native.Z3_get_tactic_name(nCtx, i);
3573 return res;
3574 }
3575 }
3576
3580 public string TacticDescription(string name)
3581 {
3582
3583 return Native.Z3_tactic_get_descr(nCtx, name);
3584 }
3585
3589 public Tactic MkTactic(string name)
3590 {
3591
3592 return new Tactic(this, name);
3593 }
3594
3599 public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
3600 {
3601 Debug.Assert(t1 != null);
3602 Debug.Assert(t2 != null);
3603 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3604
3605
3606 CheckContextMatch(t1);
3607 CheckContextMatch(t2);
3608 CheckContextMatch<Tactic>(ts);
3609
3610 IntPtr last = IntPtr.Zero;
3611 if (ts != null && ts.Length > 0)
3612 {
3613 last = ts[ts.Length - 1].NativeObject;
3614 for (int i = ts.Length - 2; i >= 0; i--)
3615 last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3616 }
3617 if (last != IntPtr.Zero)
3618 {
3619 last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3620 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3621 }
3622 else
3623 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3624 }
3625
3633 public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
3634 {
3635 Debug.Assert(t1 != null);
3636 Debug.Assert(t2 != null);
3637 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3638
3639 return AndThen(t1, t2, ts);
3640 }
3641
3646 public Tactic OrElse(Tactic t1, Tactic t2)
3647 {
3648 Debug.Assert(t1 != null);
3649 Debug.Assert(t2 != null);
3650
3651 CheckContextMatch(t1);
3652 CheckContextMatch(t2);
3653 return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3654 }
3655
3662 public Tactic TryFor(Tactic t, uint ms)
3663 {
3664 Debug.Assert(t != null);
3665
3666 CheckContextMatch(t);
3667 return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3668 }
3669
3677 public Tactic When(Probe p, Tactic t)
3678 {
3679 Debug.Assert(p != null);
3680 Debug.Assert(t != null);
3681
3682 CheckContextMatch(t);
3683 CheckContextMatch(p);
3684 return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3685 }
3686
3691 public Tactic Cond(Probe p, Tactic t1, Tactic t2)
3692 {
3693 Debug.Assert(p != null);
3694 Debug.Assert(t1 != null);
3695 Debug.Assert(t2 != null);
3696
3697 CheckContextMatch(p);
3698 CheckContextMatch(t1);
3699 CheckContextMatch(t2);
3700 return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3701 }
3702
3707 public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
3708 {
3709 Debug.Assert(t != null);
3710
3711 CheckContextMatch(t);
3712 return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3713 }
3714
3718 public Tactic Skip()
3719 {
3720
3721 return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3722 }
3723
3727 public Tactic Fail()
3728 {
3729
3730 return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3731 }
3732
3736 public Tactic FailIf(Probe p)
3737 {
3738 Debug.Assert(p != null);
3739
3740 CheckContextMatch(p);
3741 return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3742 }
3743
3748 public Tactic FailIfNotDecided()
3749 {
3750
3751 return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3752 }
3753
3757 public Tactic UsingParams(Tactic t, Params p)
3758 {
3759 Debug.Assert(t != null);
3760 Debug.Assert(p != null);
3761
3762 CheckContextMatch(t);
3763 CheckContextMatch(p);
3764 return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3765 }
3766
3771 public Tactic With(Tactic t, Params p)
3772 {
3773 Debug.Assert(t != null);
3774 Debug.Assert(p != null);
3775
3776 return UsingParams(t, p);
3777 }
3778
3782 public Tactic ParOr(params Tactic[] t)
3783 {
3784 Debug.Assert(t == null || t.All(tactic => tactic != null));
3785
3786 CheckContextMatch<Tactic>(t);
3787 return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
3788 }
3789
3794 public Tactic ParAndThen(Tactic t1, Tactic t2)
3795 {
3796 Debug.Assert(t1 != null);
3797 Debug.Assert(t2 != null);
3798
3799 CheckContextMatch(t1);
3800 CheckContextMatch(t2);
3801 return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3802 }
3803
3808 public void Interrupt()
3809 {
3810 Native.Z3_interrupt(nCtx);
3811 }
3812 #endregion
3813
3814 #region Simplifiers
3818 public uint NumSimplifiers
3819 {
3820 get { return Native.Z3_get_num_simplifiers(nCtx); }
3821 }
3822
3826 public string[] SimplifierNames
3827 {
3828 get
3829 {
3830
3831 uint n = NumSimplifiers;
3832 string[] res = new string[n];
3833 for (uint i = 0; i < n; i++)
3834 res[i] = Native.Z3_get_simplifier_name(nCtx, i);
3835 return res;
3836 }
3837 }
3838
3842 public string SimplifierDescription(string name)
3843 {
3844
3845 return Native.Z3_simplifier_get_descr(nCtx, name);
3846 }
3847
3851 public Simplifier MkSimplifier(string name)
3852 {
3853
3854 return new Simplifier(this, name);
3855 }
3856
3861 public Simplifier AndThen(Simplifier t1, Simplifier t2, params Simplifier[] ts)
3862 {
3863 Debug.Assert(t1 != null);
3864 Debug.Assert(t2 != null);
3865 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3866
3867
3868 CheckContextMatch(t1);
3869 CheckContextMatch(t2);
3870 CheckContextMatch<Simplifier>(ts);
3871
3872 IntPtr last = IntPtr.Zero;
3873 if (ts != null && ts.Length > 0)
3874 {
3875 last = ts[ts.Length - 1].NativeObject;
3876 for (int i = ts.Length - 2; i >= 0; i--)
3877 last = Native.Z3_simplifier_and_then(nCtx, ts[i].NativeObject, last);
3878 }
3879 if (last != IntPtr.Zero)
3880 {
3881 last = Native.Z3_simplifier_and_then(nCtx, t2.NativeObject, last);
3882 return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, last));
3883 }
3884 else
3885 return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3886 }
3887
3895 public Simplifier Then(Simplifier t1, Simplifier t2, params Simplifier[] ts)
3896 {
3897 Debug.Assert(t1 != null);
3898 Debug.Assert(t2 != null);
3899 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3900
3901 return AndThen(t1, t2, ts);
3902 }
3903
3907 public Simplifier UsingParams(Simplifier t, Params p)
3908 {
3909 Debug.Assert(t != null);
3910 Debug.Assert(p != null);
3911
3912 CheckContextMatch(t);
3913 CheckContextMatch(p);
3914 return new Simplifier(this, Native.Z3_simplifier_using_params(nCtx, t.NativeObject, p.NativeObject));
3915 }
3916 #endregion
3917
3918 #region Probes
3922 public uint NumProbes
3923 {
3924 get { return Native.Z3_get_num_probes(nCtx); }
3925 }
3926
3930 public string[] ProbeNames
3931 {
3932 get
3933 {
3934
3935 uint n = NumProbes;
3936 string[] res = new string[n];
3937 for (uint i = 0; i < n; i++)
3938 res[i] = Native.Z3_get_probe_name(nCtx, i);
3939 return res;
3940 }
3941 }
3942
3946 public string ProbeDescription(string name)
3947 {
3948
3949 return Native.Z3_probe_get_descr(nCtx, name);
3950 }
3951
3955 public Probe MkProbe(string name)
3956 {
3957
3958 return new Probe(this, name);
3959 }
3960
3964 public Probe ConstProbe(double val)
3965 {
3966
3967 return new Probe(this, Native.Z3_probe_const(nCtx, val));
3968 }
3969
3974 public Probe Lt(Probe p1, Probe p2)
3975 {
3976 Debug.Assert(p1 != null);
3977 Debug.Assert(p2 != null);
3978
3979 CheckContextMatch(p1);
3980 CheckContextMatch(p2);
3981 return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3982 }
3983
3988 public Probe Gt(Probe p1, Probe p2)
3989 {
3990 Debug.Assert(p1 != null);
3991 Debug.Assert(p2 != null);
3992
3993 CheckContextMatch(p1);
3994 CheckContextMatch(p2);
3995 return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3996 }
3997
4002 public Probe Le(Probe p1, Probe p2)
4003 {
4004 Debug.Assert(p1 != null);
4005 Debug.Assert(p2 != null);
4006
4007 CheckContextMatch(p1);
4008 CheckContextMatch(p2);
4009 return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
4010 }
4011
4016 public Probe Ge(Probe p1, Probe p2)
4017 {
4018 Debug.Assert(p1 != null);
4019 Debug.Assert(p2 != null);
4020
4021 CheckContextMatch(p1);
4022 CheckContextMatch(p2);
4023 return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
4024 }
4025
4030 public Probe Eq(Probe p1, Probe p2)
4031 {
4032 Debug.Assert(p1 != null);
4033 Debug.Assert(p2 != null);
4034
4035 CheckContextMatch(p1);
4036 CheckContextMatch(p2);
4037 return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
4038 }
4039
4044 public Probe And(Probe p1, Probe p2)
4045 {
4046 Debug.Assert(p1 != null);
4047 Debug.Assert(p2 != null);
4048
4049 CheckContextMatch(p1);
4050 CheckContextMatch(p2);
4051 return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
4052 }
4053
4058 public Probe Or(Probe p1, Probe p2)
4059 {
4060 Debug.Assert(p1 != null);
4061 Debug.Assert(p2 != null);
4062
4063 CheckContextMatch(p1);
4064 CheckContextMatch(p2);
4065 return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
4066 }
4067
4072 public Probe Not(Probe p)
4073 {
4074 Debug.Assert(p != null);
4075
4076 CheckContextMatch(p);
4077 return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
4078 }
4079 #endregion
4080
4081 #region Solvers
4090 public Solver MkSolver(Symbol logic = null)
4091 {
4092
4093 if (logic == null)
4094 return new Solver(this, Native.Z3_mk_solver(nCtx));
4095 else
4096 return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
4097 }
4098
4103 public Solver MkSolver(string logic)
4104 {
4105 using var symbol = MkSymbol(logic);
4106 return MkSolver(symbol);
4107 }
4108
4112 public Solver MkSimpleSolver()
4113 {
4114
4115 return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
4116 }
4117
4121 public Solver MkSolver(Solver s, Simplifier t)
4122 {
4123 Debug.Assert(t != null);
4124 Debug.Assert(s != null);
4125 return new Solver(this, Native.Z3_solver_add_simplifier(nCtx, s.NativeObject, t.NativeObject));
4126 }
4127
4135 public Solver MkSolver(Tactic t)
4136 {
4137 Debug.Assert(t != null);
4138
4139 return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
4140 }
4141
4142
4143 #endregion
4144
4145 #region Fixedpoints
4149 public Fixedpoint MkFixedpoint()
4150 {
4151
4152 return new Fixedpoint(this);
4153 }
4154 #endregion
4155
4156 #region Optimization
4160 public Optimize MkOptimize()
4161 {
4162
4163 return new Optimize(this);
4164 }
4165 #endregion
4166
4167 #region Floating-Point Arithmetic
4168
4169 #region Rounding Modes
4170 #region RoundingMode Sort
4174 public FPRMSort MkFPRoundingModeSort()
4175 {
4176 return new FPRMSort(this);
4177 }
4178 #endregion
4179
4180 #region Numerals
4184 public FPRMExpr MkFPRoundNearestTiesToEven()
4185 {
4186 return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
4187 }
4188
4192 public FPRMNum MkFPRNE()
4193 {
4194 return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
4195 }
4196
4200 public FPRMNum MkFPRoundNearestTiesToAway()
4201 {
4202 return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
4203 }
4204
4208 public FPRMNum MkFPRNA()
4209 {
4210 return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
4211 }
4212
4216 public FPRMNum MkFPRoundTowardPositive()
4217 {
4218 return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
4219 }
4220
4224 public FPRMNum MkFPRTP()
4225 {
4226 return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
4227 }
4228
4232 public FPRMNum MkFPRoundTowardNegative()
4233 {
4234 return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
4235 }
4236
4240 public FPRMNum MkFPRTN()
4241 {
4242 return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
4243 }
4244
4248 public FPRMNum MkFPRoundTowardZero()
4249 {
4250 return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
4251 }
4252
4256 public FPRMNum MkFPRTZ()
4257 {
4258 return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
4259 }
4260 #endregion
4261 #endregion
4262
4263 #region FloatingPoint Sorts
4269 public FPSort MkFPSort(uint ebits, uint sbits)
4270 {
4271 return new FPSort(this, ebits, sbits);
4272 }
4273
4277 public FPSort MkFPSortHalf()
4278 {
4279 return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
4280 }
4281
4285 public FPSort MkFPSort16()
4286 {
4287 return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
4288 }
4289
4293 public FPSort MkFPSortSingle()
4294 {
4295 return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
4296 }
4297
4301 public FPSort MkFPSort32()
4302 {
4303 return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx));
4304 }
4305
4309 public FPSort MkFPSortDouble()
4310 {
4311 return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
4312 }
4313
4317 public FPSort MkFPSort64()
4318 {
4319 return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
4320 }
4321
4325 public FPSort MkFPSortQuadruple()
4326 {
4327 return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
4328 }
4329
4333 public FPSort MkFPSort128()
4334 {
4335 return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
4336 }
4337 #endregion
4338
4339 #region Numerals
4344 public FPNum MkFPNaN(FPSort s)
4345 {
4346 return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
4347 }
4348
4354 public FPNum MkFPInf(FPSort s, bool negative)
4355 {
4356 return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
4357 }
4358
4364 public FPNum MkFPZero(FPSort s, bool negative)
4365 {
4366 return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
4367 }
4368
4374 public FPNum MkFPNumeral(float v, FPSort s)
4375 {
4376 return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
4377 }
4378
4384 public FPNum MkFPNumeral(double v, FPSort s)
4385 {
4386 return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
4387 }
4388
4394 public FPNum MkFPNumeral(int v, FPSort s)
4395 {
4396 return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
4397 }
4398
4406 public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
4407 {
4408 return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
4409 }
4410
4418 public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
4419 {
4420 return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
4421 }
4422
4428 public FPNum MkFP(float v, FPSort s)
4429 {
4430 return MkFPNumeral(v, s);
4431 }
4432
4438 public FPNum MkFP(double v, FPSort s)
4439 {
4440 return MkFPNumeral(v, s);
4441 }
4442
4448 public FPNum MkFP(int v, FPSort s)
4449 {
4450 return MkFPNumeral(v, s);
4451 }
4452
4460 public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
4461 {
4462 return MkFPNumeral(sgn, exp, sig, s);
4463 }
4464
4472 public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
4473 {
4474 return MkFPNumeral(sgn, exp, sig, s);
4475 }
4476
4477 #endregion
4478
4479 #region Operators
4484 public FPExpr MkFPAbs(FPExpr t)
4485 {
4486 return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
4487 }
4488
4493 public FPExpr MkFPNeg(FPExpr t)
4494 {
4495 return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
4496 }
4497
4504 public FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
4505 {
4506 return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4507 }
4508
4515 public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
4516 {
4517 return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4518 }
4519
4526 public FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
4527 {
4528 return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4529 }
4530
4537 public FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
4538 {
4539 return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4540 }
4541
4552 public FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
4553 {
4554 return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
4555 }
4556
4562 public FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
4563 {
4564 return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
4565 }
4566
4572 public FPExpr MkFPRem(FPExpr t1, FPExpr t2)
4573 {
4574 return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
4575 }
4576
4583 public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
4584 {
4585 return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
4586 }
4587
4593 public FPExpr MkFPMin(FPExpr t1, FPExpr t2)
4594 {
4595 return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
4596 }
4597
4603 public FPExpr MkFPMax(FPExpr t1, FPExpr t2)
4604 {
4605 return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
4606 }
4607
4613 public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
4614 {
4615 return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
4616 }
4617
4623 public BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
4624 {
4625 return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
4626 }
4627
4633 public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
4634 {
4635 return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
4636 }
4637
4643 public BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
4644 {
4645 return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
4646 }
4647
4656 public BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
4657 {
4658 return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
4659 }
4660
4665 public BoolExpr MkFPIsNormal(FPExpr t)
4666 {
4667 return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
4668 }
4669
4674 public BoolExpr MkFPIsSubnormal(FPExpr t)
4675 {
4676 return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
4677 }
4678
4683 public BoolExpr MkFPIsZero(FPExpr t)
4684 {
4685 return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
4686 }
4687
4692 public BoolExpr MkFPIsInfinite(FPExpr t)
4693 {
4694 return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
4695 }
4696
4701 public BoolExpr MkFPIsNaN(FPExpr t)
4702 {
4703 return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
4704 }
4705
4710 public BoolExpr MkFPIsNegative(FPExpr t)
4711 {
4712 return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
4713 }
4714
4719 public BoolExpr MkFPIsPositive(FPExpr t)
4720 {
4721 return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
4722 }
4723 #endregion
4724
4725 #region Conversions to FloatingPoint terms
4739 public FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
4740 {
4741 return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
4742 }
4743
4755 public FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
4756 {
4757 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
4758 }
4759
4771 public FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
4772 {
4773 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4774 }
4775
4787 public FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
4788 {
4789 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4790 }
4791
4805 public FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
4806 {
4807 if (signed)
4808 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4809 else
4810 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4811 }
4812
4823 public FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
4824 {
4825 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
4826 }
4827 #endregion
4828
4829 #region Conversions from FloatingPoint terms
4842 public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool sign)
4843 {
4844 if (sign)
4845 return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4846 else
4847 return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4848 }
4849
4859 public RealExpr MkFPToReal(FPExpr t)
4860 {
4861 return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
4862 }
4863 #endregion
4864
4865 #region Z3-specific extensions
4876 public BitVecExpr MkFPToIEEEBV(FPExpr t)
4877 {
4878 return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
4879 }
4880
4893 public BitVecExpr MkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
4894 {
4895 return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
4896 }
4897 #endregion
4898 #endregion // Floating-point Arithmetic
4899
4900 #region Miscellaneous
4911 public AST WrapAST(IntPtr nativeObject)
4912 {
4913 return AST.Create(this, nativeObject);
4914 }
4915
4927 public IntPtr UnwrapAST(AST a)
4928 {
4929 return a.NativeObject;
4930 }
4931
4937 public FuncDecl MkPartialOrder(Sort a, uint index)
4938 {
4939 return new FuncDecl(this, Native.Z3_mk_partial_order(this.nCtx, a.NativeObject, index));
4940 }
4941
4947 public FuncDecl MkTransitiveClosure(FuncDecl f)
4948 {
4949 return new FuncDecl(this, Native.Z3_mk_transitive_closure(this.nCtx, f.NativeObject));
4950 }
4951
4962 public ASTVector PolynomialSubresultants(Expr p, Expr q, Expr x)
4963 {
4964 CheckContextMatch(p);
4965 CheckContextMatch(q);
4966 CheckContextMatch(x);
4967 return new ASTVector(this, Native.Z3_polynomial_subresultants(this.nCtx, p.NativeObject, q.NativeObject, x.NativeObject));
4968 }
4969
4973 public string SimplifyHelp()
4974 {
4975
4976 return Native.Z3_simplify_get_help(nCtx);
4977 }
4978
4982 public ParamDescrs SimplifyParameterDescriptions
4983 {
4984 get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
4985 }
4986 #endregion
4987
4988 #region Error Handling
4996 //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
4997
5001 //public event ErrorHandler OnError = null;
5002 #endregion
5003
5004 #region Parameters
5014 public void UpdateParamValue(string id, string value)
5015 {
5016 Native.Z3_update_param_value(nCtx, id, value);
5017 }
5018
5019 #endregion
5020
5021 #region Internal
5022 internal IntPtr m_ctx = IntPtr.Zero;
5023 internal Native.Z3_error_handler m_n_err_handler = null;
5024 internal static Object creation_lock = new Object();
5025 internal IntPtr nCtx { get { return m_ctx; } }
5026 private Z3_ast_print_mode m_print_mode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
5027
5028 internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
5029 {
5030 // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
5031 }
5032
5033 internal void InitContext()
5034 {
5035 PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
5036 m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
5037 Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
5038 }
5039
5040 internal void CheckContextMatch(Z3Object other)
5041 {
5042 Debug.Assert(other != null);
5043
5044 if (!ReferenceEquals(this, other.Context))
5045 throw new Z3Exception("Context mismatch");
5046 }
5047
5048 internal void CheckContextMatch(Z3Object other1, Z3Object other2)
5049 {
5050 Debug.Assert(other1 != null);
5051 Debug.Assert(other2 != null);
5052 CheckContextMatch(other1);
5053 CheckContextMatch(other2);
5054 }
5055
5056 internal void CheckContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
5057 {
5058 Debug.Assert(other1 != null);
5059 Debug.Assert(other2 != null);
5060 Debug.Assert(other3 != null);
5061 CheckContextMatch(other1);
5062 CheckContextMatch(other2);
5063 CheckContextMatch(other3);
5064 }
5065
5066 internal void CheckContextMatch(Z3Object[] arr)
5067 {
5068 Debug.Assert(arr == null || arr.All(a => a != null));
5069
5070 if (arr != null)
5071 {
5072 foreach (Z3Object a in arr)
5073 {
5074 Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
5075 CheckContextMatch(a);
5076 }
5077 }
5078 }
5079
5080 internal void CheckContextMatch<T>(IEnumerable<T> arr) where T : Z3Object
5081 {
5082 Debug.Assert(arr == null || arr.All(a => a != null));
5083
5084 if (arr != null)
5085 {
5086 foreach (Z3Object a in arr)
5087 {
5088 Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
5089 CheckContextMatch(a);
5090 }
5091 }
5092 }
5093
5094 private void ObjectInvariant()
5095 {
5096 // none
5097 }
5098
5102 ~Context()
5103 {
5104 // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
5105 Dispose();
5106 }
5107
5111 public void Dispose()
5112 {
5113 // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
5114
5115 if (m_boolSort != null) m_boolSort.Dispose();
5116 if (m_intSort != null) m_intSort.Dispose();
5117 if (m_realSort != null) m_realSort.Dispose();
5118 if (m_stringSort != null) m_stringSort.Dispose();
5119 if (m_charSort != null) m_charSort.Dispose();
5120 m_boolSort = null;
5121 m_intSort = null;
5122 m_realSort = null;
5123 m_stringSort = null;
5124 m_charSort = null;
5125 if (m_ctx != IntPtr.Zero)
5126 {
5127 IntPtr ctx = m_ctx;
5128 lock (this)
5129 {
5130 m_n_err_handler = null;
5131 m_ctx = IntPtr.Zero;
5132 }
5133 if (!is_external)
5134 Native.Z3_del_context(ctx);
5135 }
5136
5137 GC.SuppressFinalize(this);
5138 }
5139
5140
5141 #endregion
5142 }
5143}
Microsoft.Z3.AST
The abstract syntax tree (AST) class.
Definition AST.cs:31
Microsoft.Z3.ASTVector
Vectors of ASTs.
Definition ASTVector.cs:29
Microsoft.Z3.ArithExpr
Arithmetic expressions (int/real)
Definition ArithExpr.cs:31
Microsoft.Z3.ArrayExpr
Array expressions.
Definition ArrayExpr.cs:32
Microsoft.Z3.BitVecExpr
Bit-vector expressions.
Definition BitVecExpr.cs:32
Microsoft.Z3.BitVecNum
Bit-vector numerals.
Definition BitVecNum.cs:32
Microsoft.Z3.BitVecSort
Bit-vector sorts.
Definition BitVecSort.cs:29
Microsoft.Z3.BoolExpr
Boolean expressions.
Definition BoolExpr.cs:32
Microsoft.Z3.BoolSort
A Boolean sort.
Definition BoolSort.cs:29
Microsoft.Z3.CharSort
A Character sort.
Definition CharSort.cs:29
Microsoft.Z3.Constructor
Constructors are used for datatype sorts.
Definition Constructor.cs:29
Microsoft.Z3.ConstructorList
Lists of constructors.
Definition ConstructorList.cs:33
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition Context.cs:34
Microsoft.Z3.Context.MkFPToFP
FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
Definition Context.cs:4787
Microsoft.Z3.Context.MkBVNAND
BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
Bitwise NAND.
Definition Context.cs:1402
Microsoft.Z3.Context.MkFP
FPNum MkFP(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition Context.cs:4428
Microsoft.Z3.Context.MkInt2Real
RealExpr MkInt2Real(IntExpr t)
Coerce an integer to a real.
Definition Context.cs:1284
Microsoft.Z3.Context.MkFPSort16
FPSort MkFPSort16()
Create the half-precision (16-bit) FloatingPoint sort.
Definition Context.cs:4285
Microsoft.Z3.Context.MkAdd
ArithExpr MkAdd(IEnumerable< ArithExpr > ts)
Create an expression representing t[0] + t[1] + ....
Definition Context.cs:1118
Microsoft.Z3.Context.MkCharLe
BoolExpr MkCharLe(Expr ch1, Expr ch2)
Create less than or equal to between two characters.
Definition Context.cs:2847
Microsoft.Z3.Context.MkNumeral
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:2999
Microsoft.Z3.Context.MkArrayConst
ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
Create an array constant.
Definition Context.cs:2120
Microsoft.Z3.Context.MkAtLeast
BoolExpr MkAtLeast(IEnumerable< BoolExpr > args, uint k)
Create an at-least-k constraint.
Definition Context.cs:2909
Microsoft.Z3.Context.MkBVSHL
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
Shift left.
Definition Context.cs:1815
Microsoft.Z3.Context.Skip
Tactic Skip()
Create a tactic that just returns the given goal.
Definition Context.cs:3718
Microsoft.Z3.Context.MkConstructor
Constructor MkConstructor(string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
Create a datatype constructor.
Definition Context.cs:432
Microsoft.Z3.Context.Then
Simplifier Then(Simplifier t1, Simplifier t2, params Simplifier[] ts)
Create a simplifier that applies t1 and then then t2 .
Definition Context.cs:3895
Microsoft.Z3.Context.BoolSort
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition Context.cs:147
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(bool[] bits)
Create a bit-vector numeral.
Definition Context.cs:3226
Microsoft.Z3.Context.MkFiniteDomainSort
FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
Create a new finite domain sort. The result is a sort
Definition Context.cs:381
Microsoft.Z3.Context.MkStringLe
BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2)
Check if the string s1 is lexicographically less or equal to s2.
Definition Context.cs:2584
Microsoft.Z3.Context.MkFPSort
FPSort MkFPSort(uint ebits, uint sbits)
Create a FloatingPoint sort.
Definition Context.cs:4269
Microsoft.Z3.Context.With
Tactic With(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition Context.cs:3771
Microsoft.Z3.Context.TacticNames
string[] TacticNames
The names of all supported tactics.
Definition Context.cs:3565
Microsoft.Z3.Context.MkIsDigit
BoolExpr MkIsDigit(Expr ch)
Create a check if the character is a digit.
Definition Context.cs:2884
Microsoft.Z3.Context.MkAdd
ArithExpr MkAdd(params ArithExpr[] ts)
Create an expression representing t[0] + t[1] + ....
Definition Context.cs:1106
Microsoft.Z3.Context.MkFPAdd
FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point addition.
Definition Context.cs:4504
Microsoft.Z3.Context.MkBVRotateLeft
BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Rotate Left.
Definition Context.cs:1908
Microsoft.Z3.Context.MkRealConst
RealExpr MkRealConst(string name)
Creates a real constant.
Definition Context.cs:865
Microsoft.Z3.Context.MkReal
RatNum MkReal(uint v)
Create a real numeral.
Definition Context.cs:3081
Microsoft.Z3.Context.Gt
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:3988
Microsoft.Z3.Context.MkBVLSHR
BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Logical shift right.
Definition Context.cs:1837
Microsoft.Z3.Context.MkFPRoundingModeSort
FPRMSort MkFPRoundingModeSort()
Create the floating-point RoundingMode sort.
Definition Context.cs:4174
Microsoft.Z3.Context.MkFPToReal
RealExpr MkFPToReal(FPExpr t)
Conversion of a floating-point term into a real-numbered term.
Definition Context.cs:4859
Microsoft.Z3.Context.MkTupleSort
TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Create a new tuple sort.
Definition Context.cs:302
Microsoft.Z3.Context.MkLambda
Lambda MkLambda(Expr[] boundConstants, Expr body)
Create a lambda expression.
Definition Context.cs:3416
Microsoft.Z3.Context.MkBitVecSort
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition Context.cs:250
Microsoft.Z3.Context.MkBVMulNoUnderflow
BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise multiplication does not underflow.
Definition Context.cs:2092
Microsoft.Z3.Context.MkDiff
ReExpr MkDiff(ReExpr a, ReExpr b)
Create a difference regular expression.
Definition Context.cs:2804
Microsoft.Z3.Context.MkFullSet
ArrayExpr MkFullSet(Sort domain)
Create the full set.
Definition Context.cs:2334
Microsoft.Z3.Context.MkFPSortQuadruple
FPSort MkFPSortQuadruple()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition Context.cs:4325
Microsoft.Z3.Context.MkLe
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
Definition Context.cs:1238
Microsoft.Z3.Context.ConstProbe
Probe ConstProbe(double val)
Create a probe that always evaluates to val .
Definition Context.cs:3964
Microsoft.Z3.Context.MkFreshConst
Expr MkFreshConst(string prefix, Sort range)
Creates a fresh Constant of sort range and a name prefixed with prefix .
Definition Context.cs:794
Microsoft.Z3.Context.MkOr
BoolExpr MkOr(params BoolExpr[] ts)
Create an expression representing t[0] or t[1] or ....
Definition Context.cs:1081
Microsoft.Z3.Context.MkReal2Int
IntExpr MkReal2Int(RealExpr t)
Coerce a real to an integer.
Definition Context.cs:1299
Microsoft.Z3.Context.MkUninterpretedSort
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
Definition Context.cs:213
Microsoft.Z3.Context.MkFPSortHalf
FPSort MkFPSortHalf()
Create the half-precision (16-bit) FloatingPoint sort.
Definition Context.cs:4277
Microsoft.Z3.Context.MkForall
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:3287
Microsoft.Z3.Context.MkSetDifference
ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Take the difference between two sets.
Definition Context.cs:2396
Microsoft.Z3.Context.MkXor
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition Context.cs:1030
Microsoft.Z3.Context.MkNumeral
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:3014
Microsoft.Z3.Context.MkITE
Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
Create an expression representing an if-then-else: ite(t1, t2, t3).
Definition Context.cs:989
Microsoft.Z3.Context.MkInt
IntNum MkInt(uint v)
Create an integer numeral.
Definition Context.cs:3137
Microsoft.Z3.Context.MkIntConst
IntExpr MkIntConst(Symbol name)
Creates an integer constant.
Definition Context.cs:835
Microsoft.Z3.Context.WrapAST
AST WrapAST(IntPtr nativeObject)
Wraps an AST.
Definition Context.cs:4911
Microsoft.Z3.Context.MkPartialOrder
FuncDecl MkPartialOrder(Sort a, uint index)
Create a partial order relation over a sort.
Definition Context.cs:4937
Microsoft.Z3.Context.IntToString
SeqExpr IntToString(Expr e)
Convert an integer expression to a string.
Definition Context.cs:2477
Microsoft.Z3.Context.MkFPMax
FPExpr MkFPMax(FPExpr t1, FPExpr t2)
Maximum of floating-point numbers.
Definition Context.cs:4603
Microsoft.Z3.Context.MkUnaryMinus
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
Definition Context.cs:1160
Microsoft.Z3.Context.MkFPToIEEEBV
BitVecExpr MkFPToIEEEBV(FPExpr t)
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
Definition Context.cs:4876
Microsoft.Z3.Context.MkConstructor
Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
Create a datatype constructor.
Definition Context.cs:415
Microsoft.Z3.Context.IntSort
IntSort IntSort
Retrieves the Integer sort of the context.
Definition Context.cs:158
Microsoft.Z3.Context.MkSuffixOf
BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
Check for sequence suffix.
Definition Context.cs:2551
Microsoft.Z3.Context.MkConcat
SeqExpr MkConcat(params SeqExpr[] t)
Concatenate sequences.
Definition Context.cs:2518
Microsoft.Z3.Context.MkFuncDecl
FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
Creates a new function declaration.
Definition Context.cs:659
Microsoft.Z3.Context.MkNot
BoolExpr MkNot(BoolExpr a)
Mk an expression representing not(a).
Definition Context.cs:976
Microsoft.Z3.Context.MkFuncDecl
FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
Creates a new function declaration.
Definition Context.cs:616
Microsoft.Z3.Context.MkUserPropagatorFuncDecl
FuncDecl MkUserPropagatorFuncDecl(string name, Sort[] domain, Sort range)
Declare a function to be processed by the user propagator plugin.
Definition Context.cs:727
Microsoft.Z3.Context.MkTermArray
Expr MkTermArray(ArrayExpr array)
Access the array default value.
Definition Context.cs:2285
Microsoft.Z3.Context.MkBVSRem
BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
Signed remainder.
Definition Context.cs:1564
Microsoft.Z3.Context.UsingParams
Simplifier UsingParams(Simplifier t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition Context.cs:3907
Microsoft.Z3.Context.MkBVRedOR
BitVecExpr MkBVRedOR(BitVecExpr t)
Take disjunction of bits in a vector, return vector of length 1.
Definition Context.cs:1348
Microsoft.Z3.Context.MkTactic
Tactic MkTactic(string name)
Creates a new Tactic.
Definition Context.cs:3589
Microsoft.Z3.Context.MkFPLEq
BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
Floating-point less than or equal.
Definition Context.cs:4613
Microsoft.Z3.Context.BenchmarkToSmtlibString
string BenchmarkToSmtlibString(string name, string logic, string status, string attributes, BoolExpr[] assumptions, BoolExpr formula)
Convert a benchmark into SMT-LIB2 formatted string.
Definition Context.cs:3506
Microsoft.Z3.Context.MkOption
ReExpr MkOption(ReExpr re)
Create the optional regular expression.
Definition Context.cs:2750
Microsoft.Z3.Context.MkFPEq
BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
Floating-point equality.
Definition Context.cs:4656
Microsoft.Z3.Context.MkDatatypeSorts
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition Context.cs:512
Microsoft.Z3.Context.MkExtract
SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
Extract subsequence.
Definition Context.cs:2617
Microsoft.Z3.Context.MkReal
RatNum MkReal(string v)
Create a real numeral.
Definition Context.cs:3059
Microsoft.Z3.Context.MkFPToFP
FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Definition Context.cs:4771
Microsoft.Z3.Context.MkDatatypeSort
DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
Create a new datatype sort.
Definition Context.cs:467
Microsoft.Z3.Context.MkFPToFP
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:4805
Microsoft.Z3.Context.UsingParams
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition Context.cs:3757
Microsoft.Z3.Context.SimplifierNames
string[] SimplifierNames
The names of all supported tactics.
Definition Context.cs:3827
Microsoft.Z3.Context.MkBVNegNoOverflow
BoolExpr MkBVNegNoOverflow(BitVecExpr t)
Create a predicate that checks that the bit-wise negation does not overflow.
Definition Context.cs:2062
Microsoft.Z3.Context.MkListSort
ListSort MkListSort(string name, Sort elemSort)
Create a new list sort.
Definition Context.cs:366
Microsoft.Z3.Context.NumTactics
uint NumTactics
The number of supported tactics.
Definition Context.cs:3557
Microsoft.Z3.Context.UbvToString
SeqExpr UbvToString(Expr e)
Convert a bit-vector expression, represented as an unsigned number, to a string.
Definition Context.cs:2487
Microsoft.Z3.Context.MkConcat
ReExpr MkConcat(params ReExpr[] t)
Create the concatenation of regular languages.
Definition Context.cs:2768
Microsoft.Z3.Context.MkBVULT
BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than.
Definition Context.cs:1597
Microsoft.Z3.Context.MkBVMulNoOverflow
BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise multiplication does not overflow.
Definition Context.cs:2076
Microsoft.Z3.Context.MkConstDecl
FuncDecl MkConstDecl(Symbol name, Sort range)
Creates a new constant function declaration.
Definition Context.cs:689
Microsoft.Z3.Context.MkXor
BoolExpr MkXor(IEnumerable< BoolExpr > args)
Create an expression representing t1 xor t2 xor t3 ... .
Definition Context.cs:1043
Microsoft.Z3.Context.MkBVSDiv
BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Signed division.
Definition Context.cs:1526
Microsoft.Z3.Context.SimplifyParameterDescriptions
ParamDescrs SimplifyParameterDescriptions
Retrieves parameter descriptions for simplifier.
Definition Context.cs:4983
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(ulong v, uint size)
Create a bit-vector numeral.
Definition Context.cs:3216
Microsoft.Z3.Context.MkFPFMA
FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Floating-point fused multiply-add.
Definition Context.cs:4552
Microsoft.Z3.Context.MkFPIsInfinite
BoolExpr MkFPIsInfinite(FPExpr t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.
Definition Context.cs:4692
Microsoft.Z3.Context.MkInt2BV
BitVecExpr MkInt2BV(uint n, IntExpr t)
Create an n bit bit-vector from the integer argument t .
Definition Context.cs:1945
Microsoft.Z3.Context.MkTrue
BoolExpr MkTrue()
The true Term.
Definition Context.cs:918
Microsoft.Z3.Context.MkFPSub
FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point subtraction.
Definition Context.cs:4515
Microsoft.Z3.Context.MkFPNumeral
FPNum MkFPNumeral(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition Context.cs:4384
Microsoft.Z3.Context.MkFPToFP
FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Definition Context.cs:4755
Microsoft.Z3.Context.MkUnion
ReExpr MkUnion(params ReExpr[] t)
Create the union of regular languages.
Definition Context.cs:2780
Microsoft.Z3.Context.MkReal
RatNum MkReal(ulong v)
Create a real numeral.
Definition Context.cs:3103
Microsoft.Z3.Context.MkBoolConst
BoolExpr MkBoolConst(Symbol name)
Create a Boolean constant.
Definition Context.cs:816
Microsoft.Z3.Context.MkEmptyRe
ReExpr MkEmptyRe(Sort s)
Create the empty regular expression. The sort s should be a regular expression.
Definition Context.cs:2816
Microsoft.Z3.Context.MkTransitiveClosure
FuncDecl MkTransitiveClosure(FuncDecl f)
Create the transitive closure of a binary relation.
Definition Context.cs:4947
Microsoft.Z3.Context.MkNth
Expr MkNth(SeqExpr s, Expr index)
Retrieve element at index.
Definition Context.cs:2606
Microsoft.Z3.Context.MkSeqMap
Expr MkSeqMap(Expr f, SeqExpr s)
Map function f over the sequence s.
Definition Context.cs:2653
Microsoft.Z3.Context.MkFPSortSingle
FPSort MkFPSortSingle()
Create the single-precision (32-bit) FloatingPoint sort.
Definition Context.cs:4293
Microsoft.Z3.Context.UnwrapAST
IntPtr UnwrapAST(AST a)
Unwraps an AST.
Definition Context.cs:4927
Microsoft.Z3.Context.MkMod
IntExpr MkMod(IntExpr t1, IntExpr t2)
Create an expression representing t1 mod t2.
Definition Context.cs:1185
Microsoft.Z3.Context.MkPBLe
BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean less-or-equal constraint.
Definition Context.cs:2921
Microsoft.Z3.Context.MkInt
IntNum MkInt(string v)
Create an integer numeral.
Definition Context.cs:3115
Microsoft.Z3.Context.MkConst
Expr MkConst(FuncDecl f)
Creates a fresh constant from the FuncDecl f .
Definition Context.cs:806
Microsoft.Z3.Context.MkFPRTZ
FPRMNum MkFPRTZ()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Definition Context.cs:4256
Microsoft.Z3.Context.TryFor
Tactic TryFor(Tactic t, uint ms)
Create a tactic that applies t to a goal for ms milliseconds.
Definition Context.cs:3662
Microsoft.Z3.Context.MkImplies
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 -> t2.
Definition Context.cs:1017
Microsoft.Z3.Context.MkBVSubNoUnderflow
BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise subtraction does not underflow.
Definition Context.cs:2030
Microsoft.Z3.Context.MkSelect
Expr MkSelect(ArrayExpr a, Expr i)
Array read.
Definition Context.cs:2144
Microsoft.Z3.Context.MkSetUnion
ArrayExpr MkSetUnion(params ArrayExpr[] args)
Take the union of a list of sets.
Definition Context.cs:2372
Microsoft.Z3.Context.MkIndexOf
IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Extract index of sub-string starting at offset.
Definition Context.cs:2629
Microsoft.Z3.Context.MkBoolConst
BoolExpr MkBoolConst(string name)
Create a Boolean constant.
Definition Context.cs:826
Microsoft.Z3.Context.MkApp
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition Context.cs:896
Microsoft.Z3.Context.MkBVSMod
BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
Two's complement signed remainder (sign follows divisor).
Definition Context.cs:1581
Microsoft.Z3.Context.Or
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:4058
Microsoft.Z3.Context.MkRepeat
BitVecExpr MkRepeat(uint i, BitVecExpr t)
Bit-vector repetition.
Definition Context.cs:1795
Microsoft.Z3.Context.MkDistinct
BoolExpr MkDistinct(IEnumerable< Expr > args)
Creates a distinct term.
Definition Context.cs:967
Microsoft.Z3.Context.MkFuncDecl
FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
Creates a new function declaration.
Definition Context.cs:600
Microsoft.Z3.Context.MkFPGt
BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
Floating-point greater than.
Definition Context.cs:4643
Microsoft.Z3.Context.MkAtMost
BoolExpr MkAtMost(IEnumerable< BoolExpr > args, uint k)
Create an at-most-k constraint.
Definition Context.cs:2897
Microsoft.Z3.Context.ParAndThen
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:3794
Microsoft.Z3.Context.MkSolver
Solver MkSolver(string logic)
Creates a new (incremental) solver.
Definition Context.cs:4103
Microsoft.Z3.Context.MkQuantifier
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:3365
Microsoft.Z3.Context.MkSetDel
ArrayExpr MkSetDel(ArrayExpr set, Expr element)
Remove an element from a set.
Definition Context.cs:2359
Microsoft.Z3.Context.MkUpdateField
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:571
Microsoft.Z3.Context.Lt
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:3974
Microsoft.Z3.Context.MkRange
ReExpr MkRange(SeqExpr lo, SeqExpr hi)
Create a range expression.
Definition Context.cs:2836
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(long v, uint size)
Create a bit-vector numeral.
Definition Context.cs:3205
Microsoft.Z3.Context.MkBVSGT
BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater-than.
Definition Context.cs:1709
Microsoft.Z3.Context.MkParams
Params MkParams()
Creates a new ParameterSet.
Definition Context.cs:3545
Microsoft.Z3.Context.MkSetIntersection
ArrayExpr MkSetIntersection(params ArrayExpr[] args)
Take the intersection of a list of sets.
Definition Context.cs:2384
Microsoft.Z3.Context.MkFPNaN
FPNum MkFPNaN(FPSort s)
Create a NaN of sort s.
Definition Context.cs:4344
Microsoft.Z3.Context.MkFP
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:4472
Microsoft.Z3.Context.ParseSMTLIB2String
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:3462
Microsoft.Z3.Context.MkBVNOR
BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise NOR.
Definition Context.cs:1416
Microsoft.Z3.Context.CharToInt
IntExpr CharToInt(Expr ch)
Create an integer (code point) from character.
Definition Context.cs:2857
Microsoft.Z3.Context.MkDistinct
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
Definition Context.cs:955
Microsoft.Z3.Context.MkFPRoundToIntegral
FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...
Definition Context.cs:4583
Microsoft.Z3.Context.MkFixedpoint
Fixedpoint MkFixedpoint()
Create a Fixedpoint context.
Definition Context.cs:4149
Microsoft.Z3.Context.MkSeqMapi
Expr MkSeqMapi(Expr f, Expr i, SeqExpr s)
Map function f over the sequence s at index i.
Definition Context.cs:2664
Microsoft.Z3.Context.UpdateParamValue
void UpdateParamValue(string id, string value)
Update a mutable configuration parameter.
Definition Context.cs:5014
Microsoft.Z3.Context.MkDatatypeSort
DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
Create a new datatype sort.
Definition Context.cs:452
Microsoft.Z3.Context.AddRecDef
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:647
Microsoft.Z3.Context.MkFPNumeral
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition Context.cs:4374
Microsoft.Z3.Context.MkConstArray
ArrayExpr MkConstArray(Sort domain, Expr v)
Create a constant array.
Definition Context.cs:2247
Microsoft.Z3.Context.MkSetComplement
ArrayExpr MkSetComplement(ArrayExpr arg)
Take the complement of a set.
Definition Context.cs:2409
Microsoft.Z3.Context.MkSetSubset
BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Check for subsetness of sets.
Definition Context.cs:2433
Microsoft.Z3.Context.Eq
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:4030
Microsoft.Z3.Context.MkFPRoundNearestTiesToAway
FPRMNum MkFPRoundNearestTiesToAway()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Definition Context.cs:4200
Microsoft.Z3.Context.ProbeNames
string[] ProbeNames
The names of all supported Probes.
Definition Context.cs:3931
Microsoft.Z3.Context.AndThen
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:3599
Microsoft.Z3.Context.MkZeroExt
BitVecExpr MkZeroExt(uint i, BitVecExpr t)
Bit-vector zero extension.
Definition Context.cs:1781
Microsoft.Z3.Context.PrintMode
Z3_ast_print_mode PrintMode
Selects the format used for pretty-printing expressions.
Definition Context.cs:3446
Microsoft.Z3.Context.Dispose
void Dispose()
Disposes of the context.
Definition Context.cs:5111
Microsoft.Z3.Context.CharToBV
BitVecExpr CharToBV(Expr ch)
Create a bit-vector (code point) from character.
Definition Context.cs:2866
Microsoft.Z3.Context.SbvToString
SeqExpr SbvToString(Expr e)
Convert a bit-vector expression, represented as an signed number, to a string.
Definition Context.cs:2497
Microsoft.Z3.Context.MkMul
ArithExpr MkMul(IEnumerable< ArithExpr > ts)
Create an expression representing t[0] * t[1] * ....
Definition Context.cs:1139
Microsoft.Z3.Context.MkEmptySet
ArrayExpr MkEmptySet(Sort domain)
Create an empty set.
Definition Context.cs:2323
Microsoft.Z3.Context.MkExists
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:3305
Microsoft.Z3.Context.MkUninterpretedSort
UninterpretedSort MkUninterpretedSort(string str)
Create a new uninterpreted sort.
Definition Context.cs:224
Microsoft.Z3.Context.MkNumeral
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:3029
Microsoft.Z3.Context.MkStar
ReExpr MkStar(ReExpr re)
Take the Kleene star of a regular expression.
Definition Context.cs:2723
Microsoft.Z3.Context.Context
Context()
Constructor.
Definition Context.cs:39
Microsoft.Z3.Context.MkBVConst
BitVecExpr MkBVConst(string name, uint size)
Creates a bit-vector constant.
Definition Context.cs:885
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(uint v, uint size)
Create a bit-vector numeral.
Definition Context.cs:3194
Microsoft.Z3.Context.MkOptimize
Optimize MkOptimize()
Create an Optimization context.
Definition Context.cs:4160
Microsoft.Z3.Context.MkQuantifier
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:3342
Microsoft.Z3.Context.CharFromBV
Expr CharFromBV(BitVecExpr bv)
Create a character from a bit-vector (code point).
Definition Context.cs:2875
Microsoft.Z3.Context.MkArrayExt
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:2296
Microsoft.Z3.Context.CharSort
CharSort CharSort
Retrieves the String sort of the context.
Definition Context.cs:181
Microsoft.Z3.Context.MkFPInf
FPNum MkFPInf(FPSort s, bool negative)
Create a floating-point infinity of sort s.
Definition Context.cs:4354
Microsoft.Z3.Context.MkConstDecl
FuncDecl MkConstDecl(string name, Sort range)
Creates a new constant function declaration.
Definition Context.cs:702
Microsoft.Z3.Context.MkMap
ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
Maps f on the argument arrays.
Definition Context.cs:2268
Microsoft.Z3.Context.MkIntersect
ReExpr MkIntersect(params ReExpr[] t)
Create the intersection of regular languages.
Definition Context.cs:2792
Microsoft.Z3.Context.Repeat
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:3707
Microsoft.Z3.Context.MkBVSLE
BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than or equal to.
Definition Context.cs:1645
Microsoft.Z3.Context.MkFP
FPNum MkFP(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition Context.cs:4448
Microsoft.Z3.Context.NumSimplifiers
uint NumSimplifiers
The number of supported simplifiers.
Definition Context.cs:3819
Microsoft.Z3.Context.MkLt
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
Definition Context.cs:1225
Microsoft.Z3.Context.MkFP
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:4460
Microsoft.Z3.Context.MkListSort
ListSort MkListSort(Symbol name, Sort elemSort)
Create a new list sort.
Definition Context.cs:353
Microsoft.Z3.Context.MkAt
SeqExpr MkAt(SeqExpr s, Expr index)
Retrieve sequence of length one at index.
Definition Context.cs:2595
Microsoft.Z3.Context.MkFPToFP
FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Conversion of a floating-point number to another FloatingPoint sort s.
Definition Context.cs:4823
Microsoft.Z3.Context.MkSetMembership
BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
Check for set membership.
Definition Context.cs:2420
Microsoft.Z3.Context.MkBVRotateRight
BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Rotate Right.
Definition Context.cs:1925
Microsoft.Z3.Context.MkReplace
SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
Replace the first occurrence of src by dst in s.
Definition Context.cs:2641
Microsoft.Z3.Context.MkFPRoundNearestTiesToEven
FPRMExpr MkFPRoundNearestTiesToEven()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Definition Context.cs:4184
Microsoft.Z3.Context.ProbeDescription
string ProbeDescription(string name)
Returns a string containing a description of the probe with the given name.
Definition Context.cs:3946
Microsoft.Z3.Context.MkPattern
Pattern MkPattern(params Expr[] terms)
Create a quantifier pattern.
Definition Context.cs:753
Microsoft.Z3.Context.And
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:4044
Microsoft.Z3.Context.Le
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:4002
Microsoft.Z3.Context.MkFPNeg
FPExpr MkFPNeg(FPExpr t)
Floating-point negation.
Definition Context.cs:4493
Microsoft.Z3.Context.MkFPSort32
FPSort MkFPSort32()
Create the single-precision (32-bit) FloatingPoint sort.
Definition Context.cs:4301
Microsoft.Z3.Context.MkConst
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition Context.cs:768
Microsoft.Z3.Context.MkAnd
BoolExpr MkAnd(params BoolExpr[] ts)
Create an expression representing t[0] and t[1] and ....
Definition Context.cs:1060
Microsoft.Z3.Context.RealSort
RealSort RealSort
Retrieves the Real sort of the context.
Definition Context.cs:170
Microsoft.Z3.Context.MkIsInteger
BoolExpr MkIsInteger(RealExpr t)
Creates an expression that checks whether a real number is an integer.
Definition Context.cs:1310
Microsoft.Z3.Context.MkBVXNOR
BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XNOR.
Definition Context.cs:1430
Microsoft.Z3.Context.MkBVULE
BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than or equal to.
Definition Context.cs:1629
Microsoft.Z3.Context.MkGe
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
Definition Context.cs:1264
Microsoft.Z3.Context.PolynomialSubresultants
ASTVector PolynomialSubresultants(Expr p, Expr q, Expr x)
Return the nonzero subresultants of p and q with respect to the "variable" x.
Definition Context.cs:4962
Microsoft.Z3.Context.MkFPNumeral
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:4418
Microsoft.Z3.Context.MkFPToBV
BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool sign)
Conversion of a floating-point term into a bit-vector.
Definition Context.cs:4842
Microsoft.Z3.Context.MkBVAddNoUnderflow
BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise addition does not underflow.
Definition Context.cs:1998
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(string v, uint size)
Create a bit-vector numeral.
Definition Context.cs:3172
Microsoft.Z3.Context.MkFullRe
ReExpr MkFullRe(Sort s)
Create the full regular expression. The sort s should be a regular expression.
Definition Context.cs:2826
Microsoft.Z3.Context.MkSeqFoldLeft
Expr MkSeqFoldLeft(Expr f, Expr a, SeqExpr s)
Fold left the function f over the sequence s with initial value a.
Definition Context.cs:2676
Microsoft.Z3.Context.MkFPIsSubnormal
BoolExpr MkFPIsSubnormal(FPExpr t)
Predicate indicating whether t is a subnormal floating-point number.
Definition Context.cs:4674
Microsoft.Z3.Context.MkArrayConst
ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
Create an array constant.
Definition Context.cs:2107
Microsoft.Z3.Context.MkFPIsZero
BoolExpr MkFPIsZero(FPExpr t)
Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
Definition Context.cs:4683
Microsoft.Z3.Context.MkReSort
ReSort MkReSort(SeqSort s)
Create a new regular expression sort.
Definition Context.cs:267
Microsoft.Z3.Context.MkFPSortDouble
FPSort MkFPSortDouble()
Create the double-precision (64-bit) FloatingPoint sort.
Definition Context.cs:4309
Microsoft.Z3.Context.SimplifierDescription
string SimplifierDescription(string name)
Returns a string containing a description of the simplifier with the given name.
Definition Context.cs:3842
Microsoft.Z3.Context.MkFPRoundTowardZero
FPRMNum MkFPRoundTowardZero()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Definition Context.cs:4248
Microsoft.Z3.Context.MkSub
ArithExpr MkSub(params ArithExpr[] ts)
Create an expression representing t[0] - t[1] - ....
Definition Context.cs:1148
Microsoft.Z3.Context.MkGoal
Goal MkGoal(bool models=true, bool unsatCores=false, bool proofs=false)
Creates a new Goal.
Definition Context.cs:3534
Microsoft.Z3.Context.MkBV2Int
IntExpr MkBV2Int(BitVecExpr t, bool signed)
Create an integer from the bit-vector argument t .
Definition Context.cs:1968
Microsoft.Z3.Context.MkInRe
BoolExpr MkInRe(SeqExpr s, ReExpr re)
Check for regular expression membership.
Definition Context.cs:2712
Microsoft.Z3.Context.MkSetAdd
ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
Add an element to the set.
Definition Context.cs:2345
Microsoft.Z3.Context.MkBVRedAND
BitVecExpr MkBVRedAND(BitVecExpr t)
Take conjunction of bits in a vector, return vector of length 1.
Definition Context.cs:1336
Microsoft.Z3.Context.Ge
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:4016
Microsoft.Z3.Context.MkDatatypeSortRef
DatatypeSort MkDatatypeSortRef(string name, Sort[] parameters=null)
Create a forward reference to a datatype sort. This is useful for creating recursive datatypes or par...
Definition Context.cs:501
Microsoft.Z3.Context.MkLoop
ReExpr MkLoop(ReExpr re, uint lo, uint hi=0)
Take the bounded Kleene star of a regular expression.
Definition Context.cs:2732
Microsoft.Z3.Context.MkFPRoundTowardNegative
FPRMNum MkFPRoundTowardNegative()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Definition Context.cs:4232
Microsoft.Z3.Context.MkProbe
Probe MkProbe(string name)
Creates a new Probe.
Definition Context.cs:3955
Microsoft.Z3.Context.MkFPNumeral
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:4406
Microsoft.Z3.Context.MkSeqSort
SeqSort MkSeqSort(Sort s)
Create a new sequence sort.
Definition Context.cs:258
Microsoft.Z3.Context.MkDatatypeSorts
DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
Create mutually recursive data-types.
Definition Context.cs:545
Microsoft.Z3.Context.FailIf
Tactic FailIf(Probe p)
Create a tactic that fails if the probe p evaluates to false.
Definition Context.cs:3736
Microsoft.Z3.Context.MkBound
Expr MkBound(uint index, Sort ty)
Creates a new bound variable.
Definition Context.cs:741
Microsoft.Z3.Context.MkFPRTN
FPRMNum MkFPRTN()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Definition Context.cs:4240
Microsoft.Z3.Context.MkFPSort128
FPSort MkFPSort128()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition Context.cs:4333
Microsoft.Z3.Context.MkBVUGE
BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
Unsigned greater than or equal to.
Definition Context.cs:1661
Microsoft.Z3.Context.MkNumeral
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:2984
Microsoft.Z3.Context.MkFPRTP
FPRMNum MkFPRTP()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Definition Context.cs:4224
Microsoft.Z3.Context.MkBoolSort
BoolSort MkBoolSort()
Create a new Boolean sort.
Definition Context.cs:205
Microsoft.Z3.Context.MkConcat
BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
Bit-vector concatenation.
Definition Context.cs:1729
Microsoft.Z3.Context.MkPower
ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 ^ t2.
Definition Context.cs:1212
Microsoft.Z3.Context.MkEmptySeq
SeqExpr MkEmptySeq(Sort s)
Create the empty sequence.
Definition Context.cs:2450
Microsoft.Z3.Context.MkBVNot
BitVecExpr MkBVNot(BitVecExpr t)
Bitwise negation.
Definition Context.cs:1324
Microsoft.Z3.Context.MkFPRem
FPExpr MkFPRem(FPExpr t1, FPExpr t2)
Floating-point remainder.
Definition Context.cs:4572
Microsoft.Z3.Context.MkRealSort
RealSort MkRealSort()
Create a real sort.
Definition Context.cs:242
Microsoft.Z3.Context.MkBVAddNoOverflow
BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise addition does not overflow.
Definition Context.cs:1982
Microsoft.Z3.Context.MkDiv
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
Definition Context.cs:1171
Microsoft.Z3.Context.MkSelect
Expr MkSelect(ArrayExpr a, params Expr[] args)
Array read.
Definition Context.cs:2167
Microsoft.Z3.Context.MkFPNumeral
FPNum MkFPNumeral(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition Context.cs:4394
Microsoft.Z3.Context.ParseSMTLIB2File
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:3481
Microsoft.Z3.Context.MkFPLt
BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
Floating-point less than.
Definition Context.cs:4623
Microsoft.Z3.Context.MkSimplifier
Simplifier MkSimplifier(string name)
Creates a new Tactic.
Definition Context.cs:3851
Microsoft.Z3.Context.MkFPGEq
BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
Floating-point greater than or equal.
Definition Context.cs:4633
Microsoft.Z3.Context.MkSignExt
BitVecExpr MkSignExt(uint i, BitVecExpr t)
Bit-vector sign extension.
Definition Context.cs:1764
Microsoft.Z3.Context.ParOr
Tactic ParOr(params Tactic[] t)
Create a tactic that applies the given tactics in parallel until one of them succeeds (i....
Definition Context.cs:3782
Microsoft.Z3.Context.MkIntSort
IntSort MkIntSort()
Create a new integer sort.
Definition Context.cs:233
Microsoft.Z3.Context.MkAnd
BoolExpr MkAnd(IEnumerable< BoolExpr > t)
Create an expression representing t[0] and t[1] and ....
Definition Context.cs:1072
Microsoft.Z3.Context.MkBVMul
BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
Two's complement multiplication.
Definition Context.cs:1484
Microsoft.Z3.Context.StringToInt
IntExpr StringToInt(Expr e)
Convert an integer expression to a string.
Definition Context.cs:2507
Microsoft.Z3.Context.MkBVSDivNoOverflow
BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise signed division does not overflow.
Definition Context.cs:2046
Microsoft.Z3.Context.MkContains
BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
Check for sequence containment of s2 in s1.
Definition Context.cs:2562
Microsoft.Z3.Context.OrElse
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:3646
Microsoft.Z3.Context.StringSort
SeqSort StringSort
Retrieves the String sort of the context.
Definition Context.cs:193
Microsoft.Z3.Context.MkEq
BoolExpr MkEq(Expr x, Expr y)
Creates the equality x = y .
Definition Context.cs:942
Microsoft.Z3.Context.Cond
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:3691
Microsoft.Z3.Context.MkBVSub
BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
Two's complement subtraction.
Definition Context.cs:1470
Microsoft.Z3.Context.MkBVUDiv
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Unsigned division.
Definition Context.cs:1503
Microsoft.Z3.Context.Interrupt
void Interrupt()
Interrupt the execution of a Z3 procedure.
Definition Context.cs:3808
Microsoft.Z3.Context.MkBVUGT
BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
Unsigned greater-than.
Definition Context.cs:1693
Microsoft.Z3.Context.MkArraySort
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition Context.cs:276
Microsoft.Z3.Context.MkBVConst
BitVecExpr MkBVConst(Symbol name, uint size)
Creates a bit-vector constant.
Definition Context.cs:874
Microsoft.Z3.Context.MkBVASHR
BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
Arithmetic shift right.
Definition Context.cs:1861
Microsoft.Z3.Context.Then
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:3633
Microsoft.Z3.Context.MkFPZero
FPNum MkFPZero(FPSort s, bool negative)
Create a floating-point zero of sort s.
Definition Context.cs:4364
Microsoft.Z3.Context.MkPBGe
BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean greater-or-equal constraint.
Definition Context.cs:2935
Microsoft.Z3.Context.MkInt
IntNum MkInt(long v)
Create an integer numeral.
Definition Context.cs:3148
Microsoft.Z3.Context.MkReal
RatNum MkReal(long v)
Create a real numeral.
Definition Context.cs:3092
Microsoft.Z3.Context.MkPlus
ReExpr MkPlus(ReExpr re)
Take the Kleene plus of a regular expression.
Definition Context.cs:2741
Microsoft.Z3.Context.MkFPSqrt
FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
Floating-point square root.
Definition Context.cs:4562
Microsoft.Z3.Context.MkIff
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 iff t2.
Definition Context.cs:1004
Microsoft.Z3.Context.MkFiniteDomainSort
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:397
Microsoft.Z3.Context.MkNumeral
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition Context.cs:2969
Microsoft.Z3.Context.MkRecFuncDecl
FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
Creates a new recursive function declaration.
Definition Context.cs:630
Microsoft.Z3.Context.MkBVAdd
BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
Two's complement addition.
Definition Context.cs:1456
Microsoft.Z3.Context.MkGt
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
Definition Context.cs:1251
Microsoft.Z3.Context.MkSimpleSolver
Solver MkSimpleSolver()
Creates a new (incremental) solver.
Definition Context.cs:4112
Microsoft.Z3.Context.MkArraySort
ArraySort MkArraySort(Sort[] domain, Sort range)
Create a new n-ary array sort.
Definition Context.cs:289
Microsoft.Z3.Context.MkDatatypeSortRef
DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters=null)
Create a forward reference to a datatype sort. This is useful for creating recursive datatypes or par...
Definition Context.cs:483
Microsoft.Z3.Context.Not
Probe Not(Probe p)
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
Definition Context.cs:4072
Microsoft.Z3.Context.MkBool
BoolExpr MkBool(bool value)
Creates a Boolean value.
Definition Context.cs:934
Microsoft.Z3.Context.MkBVAND
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
Bitwise conjunction.
Definition Context.cs:1360
Microsoft.Z3.Context.MkSolver
Solver MkSolver(Tactic t)
Creates a solver that is implemented using the given tactic.
Definition Context.cs:4135
Microsoft.Z3.Context.MkRealConst
RealExpr MkRealConst(Symbol name)
Creates a real constant.
Definition Context.cs:855
Microsoft.Z3.Context.MkInt
IntNum MkInt(ulong v)
Create an integer numeral.
Definition Context.cs:3159
Microsoft.Z3.Context.MkApp
Expr MkApp(FuncDecl f, IEnumerable< Expr > args)
Create a new function application.
Definition Context.cs:908
Microsoft.Z3.Context.MkToRe
ReExpr MkToRe(SeqExpr s)
Convert a regular expression that accepts sequence s.
Definition Context.cs:2702
Microsoft.Z3.Context.MkFPIsNaN
BoolExpr MkFPIsNaN(FPExpr t)
Predicate indicating whether t is a NaN.
Definition Context.cs:4701
Microsoft.Z3.Context.MkBVRotateRight
BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
Rotate Right.
Definition Context.cs:1893
Microsoft.Z3.Context.SimplifyHelp
string SimplifyHelp()
Return a string describing all available parameters to Expr.Simplify.
Definition Context.cs:4973
Microsoft.Z3.Context.MkExists
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:3327
Microsoft.Z3.Context.MkLambda
Lambda MkLambda(Sort[] sorts, Symbol[] names, Expr body)
Create a lambda expression.
Definition Context.cs:3397
Microsoft.Z3.Context.MkFuncDecl
FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
Creates a new function declaration.
Definition Context.cs:585
Microsoft.Z3.Context.MkBVSLT
BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than.
Definition Context.cs:1613
Microsoft.Z3.Context.MkSetSort
SetSort MkSetSort(Sort ty)
Create a set type.
Definition Context.cs:2312
Microsoft.Z3.Context.MkEnumSort
EnumSort MkEnumSort(string name, params string[] enumNames)
Create a new enumeration sort.
Definition Context.cs:333
Microsoft.Z3.Context.AndThen
Simplifier AndThen(Simplifier t1, Simplifier t2, params Simplifier[] ts)
Create a simplifier that applies t1 and then t2 .
Definition Context.cs:3861
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(int v, uint size)
Create a bit-vector numeral.
Definition Context.cs:3183
Microsoft.Z3.Context.MkReal
RatNum MkReal(int num, int den)
Create a real from a fraction.
Definition Context.cs:3046
Microsoft.Z3.Context.MkEnumSort
EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
Create a new enumeration sort.
Definition Context.cs:318
Microsoft.Z3.Context.MkSolver
Solver MkSolver(Solver s, Simplifier t)
Creates a solver that uses an incremental simplifier.
Definition Context.cs:4121
Microsoft.Z3.Context.MkFPIsNegative
BoolExpr MkFPIsNegative(FPExpr t)
Predicate indicating whether t is a negative floating-point number.
Definition Context.cs:4710
Microsoft.Z3.Context.MkFreshFuncDecl
FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
Creates a fresh function declaration with a name prefixed with prefix .
Definition Context.cs:676
Microsoft.Z3.Context.MkIntConst
IntExpr MkIntConst(string name)
Creates an integer constant.
Definition Context.cs:845
Microsoft.Z3.Context.When
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:3677
Microsoft.Z3.Context.MkBVNeg
BitVecExpr MkBVNeg(BitVecExpr t)
Standard two's complement unary minus.
Definition Context.cs:1444
Microsoft.Z3.Context.MkFreshConstDecl
FuncDecl MkFreshConstDecl(string prefix, Sort range)
Creates a fresh constant function declaration with a name prefixed with prefix .
Definition Context.cs:716
Microsoft.Z3.Context.Fail
Tactic Fail()
Create a tactic always fails.
Definition Context.cs:3727
Microsoft.Z3.Context.FailIfNotDecided
Tactic FailIfNotDecided()
Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsati...
Definition Context.cs:3748
Microsoft.Z3.Context.MkFPRoundTowardPositive
FPRMNum MkFPRoundTowardPositive()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Definition Context.cs:4216
Microsoft.Z3.Context.MkBVOR
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
Bitwise disjunction.
Definition Context.cs:1374
Microsoft.Z3.Context.MkConst
Expr MkConst(string name, Sort range)
Creates a new Constant of sort range and named name .
Definition Context.cs:782
Microsoft.Z3.Context.MkRem
IntExpr MkRem(IntExpr t1, IntExpr t2)
Create an expression representing t1 rem t2.
Definition Context.cs:1199
Microsoft.Z3.Context.MkFPMul
FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point multiplication.
Definition Context.cs:4526
Microsoft.Z3.Context.MkStringLt
BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
Check if the string s1 is lexicographically strictly less than s2.
Definition Context.cs:2573
Microsoft.Z3.Context.MkBVSubNoOverflow
BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise subtraction does not overflow.
Definition Context.cs:2014
Microsoft.Z3.Context.MkFPToFP
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:4893
Microsoft.Z3.Context.MkFPSort64
FPSort MkFPSort64()
Create the double-precision (64-bit) FloatingPoint sort.
Definition Context.cs:4317
Microsoft.Z3.Context.MkOr
BoolExpr MkOr(IEnumerable< BoolExpr > ts)
Create an expression representing t[0] or t[1] or ....
Definition Context.cs:1094
Microsoft.Z3.Context.MkFPRNA
FPRMNum MkFPRNA()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Definition Context.cs:4208
Microsoft.Z3.Context.Context
Context(Dictionary< string, string > settings)
Constructor.
Definition Context.cs:68
Microsoft.Z3.Context.MkBVRotateLeft
BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
Rotate Left.
Definition Context.cs:1878
Microsoft.Z3.Context.TacticDescription
string TacticDescription(string name)
Returns a string containing a description of the tactic with the given name.
Definition Context.cs:3580
Microsoft.Z3.Context.MkFPRNE
FPRMNum MkFPRNE()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Definition Context.cs:4192
Microsoft.Z3.Context.MkUnit
SeqExpr MkUnit(Expr elem)
Create the singleton sequence.
Definition Context.cs:2459
Microsoft.Z3.Context.NumProbes
uint NumProbes
The number of supported Probes.
Definition Context.cs:3923
Microsoft.Z3.Context.MkPBEq
BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean equal constraint.
Definition Context.cs:2948
Microsoft.Z3.Context.MkInt
IntNum MkInt(int v)
Create an integer numeral.
Definition Context.cs:3126
Microsoft.Z3.Context.MkBVXOR
BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XOR.
Definition Context.cs:1388
Microsoft.Z3.Context.MkStore
ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
Array update.
Definition Context.cs:2226
Microsoft.Z3.Context.MkSolver
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition Context.cs:4090
Microsoft.Z3.Context.MkFPAbs
FPExpr MkFPAbs(FPExpr t)
Floating-point absolute value.
Definition Context.cs:4484
Microsoft.Z3.Context.MkFPMin
FPExpr MkFPMin(FPExpr t1, FPExpr t2)
Minimum of floating-point numbers.
Definition Context.cs:4593
Microsoft.Z3.Context.MkFPDiv
FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point division.
Definition Context.cs:4537
Microsoft.Z3.Context.MkComplement
ReExpr MkComplement(ReExpr re)
Create the complement regular expression.
Definition Context.cs:2759
Microsoft.Z3.Context.MkExtract
BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
Bit-vector extraction.
Definition Context.cs:1748
Microsoft.Z3.Context.MkSymbol
StringSymbol MkSymbol(string name)
Create a symbol using a string.
Definition Context.cs:119
Microsoft.Z3.Context.MkBVURem
BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
Unsigned remainder.
Definition Context.cs:1544
Microsoft.Z3.Context.MkFalse
BoolExpr MkFalse()
The false Term.
Definition Context.cs:926
Microsoft.Z3.Context.MkLength
IntExpr MkLength(SeqExpr s)
Retrieve the length of a given sequence.
Definition Context.cs:2531
Microsoft.Z3.Context.MkReal
RatNum MkReal(int v)
Create a real numeral.
Definition Context.cs:3070
Microsoft.Z3.Context.MkSymbol
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition Context.cs:111
Microsoft.Z3.Context.MkString
SeqExpr MkString(string s)
Create a string constant.
Definition Context.cs:2468
Microsoft.Z3.Context.MkStore
ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
Array update.
Definition Context.cs:2196
Microsoft.Z3.Context.MkFP
FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
Create an expression of FloatingPoint sort from three bit-vector expressions.
Definition Context.cs:4739
Microsoft.Z3.Context.MkSeqFoldLeftI
Expr MkSeqFoldLeftI(Expr f, Expr i, Expr a, SeqExpr s)
Fold left with index the function f over the sequence s with initial value a starting at index i.
Definition Context.cs:2688
Microsoft.Z3.Context.MkMul
ArithExpr MkMul(params ArithExpr[] ts)
Create an expression representing t[0] * t[1] * ....
Definition Context.cs:1127
Microsoft.Z3.Context.MkBVSGE
BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater than or equal to.
Definition Context.cs:1677
Microsoft.Z3.Context.MkForall
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:3263
Microsoft.Z3.Context.MkFP
FPNum MkFP(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition Context.cs:4438
Microsoft.Z3.Context.MkFPIsNormal
BoolExpr MkFPIsNormal(FPExpr t)
Predicate indicating whether t is a normal floating-point number.
Definition Context.cs:4665
Microsoft.Z3.Context.MkPrefixOf
BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
Check for sequence prefix.
Definition Context.cs:2540
Microsoft.Z3.Context.MkFPIsPositive
BoolExpr MkFPIsPositive(FPExpr t)
Predicate indicating whether t is a positive floating-point number.
Definition Context.cs:4719
Microsoft.Z3.EnumSort
Enumeration sorts.
Definition EnumSort.cs:29
Microsoft.Z3.Expr
Expressions are terms.
Definition Expr.cs:31
Microsoft.Z3.FPExpr
FloatingPoint Expressions.
Definition FPExpr.cs:32
Microsoft.Z3.FPNum
FloatiungPoint Numerals.
Definition FPNum.cs:28
Microsoft.Z3.FPRMExpr
FloatingPoint RoundingMode Expressions.
Definition FPRMExpr.cs:32
Microsoft.Z3.FPRMNum
Floating-point rounding mode numerals.
Definition FPRMNum.cs:32
Microsoft.Z3.FPRMSort
The FloatingPoint RoundingMode sort.
Definition FPRMSort.cs:29
Microsoft.Z3.FPSort
FloatingPoint sort.
Definition FPSort.cs:28
Microsoft.Z3.Fixedpoint
Object for managing fixedpoints.
Definition Fixedpoint.cs:30
Microsoft.Z3.FuncDecl
Function declarations.
Definition FuncDecl.cs:31
Microsoft.Z3.Goal
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition Goal.cs:32
Microsoft.Z3.IntExpr
Int expressions.
Definition IntExpr.cs:32
Microsoft.Z3.IntNum
Integer Numerals.
Definition IntNum.cs:32
Microsoft.Z3.IntSort
An Integer sort.
Definition IntSort.cs:29
Microsoft.Z3.IntSymbol
Numbered symbols.
Definition IntSymbol.cs:30
Microsoft.Z3.Lambda
Lambda expressions.
Definition Lambda.cs:30
Microsoft.Z3.Optimize
Object for managing optimization context.
Definition Optimize.cs:31
Microsoft.Z3.ParamDescrs
A ParamDescrs describes a set of parameters.
Definition ParamDescrs.cs:29
Microsoft.Z3.Params
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition Params.cs:29
Microsoft.Z3.Pattern
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
Definition Pattern.cs:32
Microsoft.Z3.Probe
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
Definition Probe.cs:34
Microsoft.Z3.Quantifier
Quantifier expressions.
Definition Quantifier.cs:30
Microsoft.Z3.RatNum
Rational Numerals.
Definition RatNum.cs:32
Microsoft.Z3.ReExpr
Regular expression expressions.
Definition ReExpr.cs:32
Microsoft.Z3.ReSort
A regular expression sort.
Definition ReSort.cs:29
Microsoft.Z3.RealExpr
Real expressions.
Definition RealExpr.cs:32
Microsoft.Z3.SeqExpr
Sequence expressions.
Definition SeqExpr.cs:32
Microsoft.Z3.SeqSort
A Sequence sort.
Definition SeqSort.cs:29
Microsoft.Z3.Simplifier
Simplifiers are the basic building block for creating custom solvers with incremental pre-processing....
Definition Simplifiers.cs:30
Microsoft.Z3.Solver.Assert
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
Definition Solver.cs:200
Microsoft.Z3.Sort
The Sort class implements type information for ASTs.
Definition Sort.cs:29
Microsoft.Z3.Symbol
Symbols are used to name several term and type constructors.
Definition Symbol.cs:30
Microsoft.Z3.Tactic
Tactics are the basic building block for creating custom solvers for specific problem domains....
Definition Tactic.cs:32
Microsoft.Z3.Z3Exception
The exception base class for error reporting from Z3.
Definition Z3Exception.cs:32
Z3_ast_print_mode
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition z3_api.h:1322
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition z3_api.h:1347
Microsoft.Z3.Z3_context
System.IntPtr Z3_context
Definition Context.cs:29
Generated on Thu Feb 19 2026 05:10:46 for Z3 by doxygen 1.9.8