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
569 public Sort MkTypeVariable(Symbol name)
570 {
571 Debug.Assert(name != null);
572 CheckContextMatch(name);
573 return new Sort(this, Native.Z3_mk_type_variable(nCtx, name.NativeObject));
574 }
575
580 public Sort MkTypeVariable(string name)
581 {
582 using var symbol = MkSymbol(name);
583 return MkTypeVariable(symbol);
584 }
585
593 public DatatypeSort MkPolymorphicDatatypeSort(Symbol name, Sort[] typeParams, Constructor[] constructors)
594 {
595 Debug.Assert(name != null);
596 Debug.Assert(typeParams != null);
597 Debug.Assert(constructors != null);
598 Debug.Assert(constructors.All(c => c != null));
599
600 CheckContextMatch(name);
601 CheckContextMatch<Sort>(typeParams);
602 CheckContextMatch<Constructor>(constructors);
603 return new DatatypeSort(this,
604 Native.Z3_mk_polymorphic_datatype(nCtx, name.NativeObject,
605 (uint)typeParams.Length, AST.ArrayToNative(typeParams),
606 (uint)constructors.Length, Z3Object.ArrayToNative(constructors)));
607 }
608
616 public DatatypeSort MkPolymorphicDatatypeSort(string name, Sort[] typeParams, Constructor[] constructors)
617 {
618 using var symbol = MkSymbol(name);
619 return MkPolymorphicDatatypeSort(symbol, typeParams, constructors);
620 }
621
628 public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
629 {
630 return Expr.Create(this, Native.Z3_datatype_update_field(
631 nCtx, field.NativeObject,
632 t.NativeObject, v.NativeObject));
633 }
634
635 #endregion
636 #endregion
637
638 #region Function Declarations
642 public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
643 {
644 Debug.Assert(name != null);
645 Debug.Assert(range != null);
646 Debug.Assert(domain.All(d => d != null));
647
648 CheckContextMatch(name);
649 CheckContextMatch<Sort>(domain);
650 CheckContextMatch(range);
651 return new FuncDecl(this, name, domain, range);
652 }
653
657 public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
658 {
659 Debug.Assert(name != null);
660 Debug.Assert(domain != null);
661 Debug.Assert(range != null);
662
663 CheckContextMatch(name);
664 CheckContextMatch(domain);
665 CheckContextMatch(range);
666 Sort[] q = new Sort[] { domain };
667 return new FuncDecl(this, name, q, range);
668 }
669
673 public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
674 {
675 Debug.Assert(range != null);
676 Debug.Assert(domain.All(d => d != null));
677
678 CheckContextMatch<Sort>(domain);
679 CheckContextMatch(range);
680 using var symbol = MkSymbol(name);
681 return new FuncDecl(this, symbol, domain, range);
682 }
683
687 public FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
688 {
689 Debug.Assert(range != null);
690 Debug.Assert(domain.All(d => d != null));
691
692 CheckContextMatch<Sort>(domain);
693 CheckContextMatch(range);
694 using var symbol = MkSymbol(name);
695 return new FuncDecl(this, symbol, domain, range, true);
696 }
697
704 public void AddRecDef(FuncDecl f, Expr[] args, Expr body)
705 {
706 CheckContextMatch(f);
707 CheckContextMatch<Expr>(args);
708 CheckContextMatch(body);
709 IntPtr[] argsNative = AST.ArrayToNative(args);
710 Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
711 }
712
716 public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
717 {
718 Debug.Assert(range != null);
719 Debug.Assert(domain != null);
720
721 CheckContextMatch(domain);
722 CheckContextMatch(range);
723 using var symbol = MkSymbol(name);
724 Sort[] q = new Sort[] { domain };
725 return new FuncDecl(this, symbol, q, range);
726 }
727
733 public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
734 {
735 Debug.Assert(range != null);
736 Debug.Assert(domain.All(d => d != null));
737
738 CheckContextMatch<Sort>(domain);
739 CheckContextMatch(range);
740 return new FuncDecl(this, prefix, domain, range);
741 }
742
746 public FuncDecl MkConstDecl(Symbol name, Sort range)
747 {
748 Debug.Assert(name != null);
749 Debug.Assert(range != null);
750
751 CheckContextMatch(name);
752 CheckContextMatch(range);
753 return new FuncDecl(this, name, null, range);
754 }
755
759 public FuncDecl MkConstDecl(string name, Sort range)
760 {
761 Debug.Assert(range != null);
762
763 CheckContextMatch(range);
764 using var symbol = MkSymbol(name);
765 return new FuncDecl(this, symbol, null, range);
766 }
767
773 public FuncDecl MkFreshConstDecl(string prefix, Sort range)
774 {
775 Debug.Assert(range != null);
776
777 CheckContextMatch(range);
778 return new FuncDecl(this, prefix, null, range);
779 }
780
784 public FuncDecl MkUserPropagatorFuncDecl(string name, Sort[] domain, Sort range)
785 {
786 using var _name = MkSymbol(name);
787 var fn = Native.Z3_solver_propagate_declare(nCtx, _name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject);
788 return new FuncDecl(this, fn);
789 }
790 #endregion
791
792 #region Bound Variables
798 public Expr MkBound(uint index, Sort ty)
799 {
800 Debug.Assert(ty != null);
801
802 return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
803 }
804 #endregion
805
806 #region Quantifier Patterns
810 public Pattern MkPattern(params Expr[] terms)
811 {
812 Debug.Assert(terms != null);
813 if (terms.Length == 0)
814 throw new Z3Exception("Cannot create a pattern from zero terms");
815
816 IntPtr[] termsNative = AST.ArrayToNative(terms);
817 return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
818 }
819 #endregion
820
821 #region Constants
825 public Expr MkConst(Symbol name, Sort range)
826 {
827 Debug.Assert(name != null);
828 Debug.Assert(range != null);
829
830 CheckContextMatch(name);
831 CheckContextMatch(range);
832
833 return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
834 }
835
839 public Expr MkConst(string name, Sort range)
840 {
841 Debug.Assert(range != null);
842
843 using var symbol = MkSymbol(name);
844 return MkConst(symbol, range);
845 }
846
851 public Expr MkFreshConst(string prefix, Sort range)
852 {
853 Debug.Assert(range != null);
854
855 CheckContextMatch(range);
856 return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
857 }
858
863 public Expr MkConst(FuncDecl f)
864 {
865 Debug.Assert(f != null);
866
867 return MkApp(f);
868 }
869
873 public BoolExpr MkBoolConst(Symbol name)
874 {
875 Debug.Assert(name != null);
876
877 return (BoolExpr)MkConst(name, BoolSort);
878 }
879
883 public BoolExpr MkBoolConst(string name)
884 {
885 using var symbol = MkSymbol(name);
886 return (BoolExpr)MkConst(symbol, BoolSort);
887 }
888
892 public IntExpr MkIntConst(Symbol name)
893 {
894 Debug.Assert(name != null);
895
896 return (IntExpr)MkConst(name, IntSort);
897 }
898
902 public IntExpr MkIntConst(string name)
903 {
904 Debug.Assert(name != null);
905
906 return (IntExpr)MkConst(name, IntSort);
907 }
908
912 public RealExpr MkRealConst(Symbol name)
913 {
914 Debug.Assert(name != null);
915
916 return (RealExpr)MkConst(name, RealSort);
917 }
918
922 public RealExpr MkRealConst(string name)
923 {
924
925 return (RealExpr)MkConst(name, RealSort);
926 }
927
931 public BitVecExpr MkBVConst(Symbol name, uint size)
932 {
933 Debug.Assert(name != null);
934
935 using var sort = MkBitVecSort(size);
936 return (BitVecExpr)MkConst(name, sort);
937 }
938
942 public BitVecExpr MkBVConst(string name, uint size)
943 {
944 using var sort = MkBitVecSort(size);
945 return (BitVecExpr)MkConst(name, sort);
946 }
947 #endregion
948
949 #region Terms
953 public Expr MkApp(FuncDecl f, params Expr[] args)
954 {
955 Debug.Assert(f != null);
956 Debug.Assert(args == null || args.All(a => a != null));
957 CheckContextMatch(f);
958 CheckContextMatch<Expr>(args);
959 return Expr.Create(this, f, args);
960 }
961
965 public Expr MkApp(FuncDecl f, IEnumerable<Expr> args)
966 {
967 Debug.Assert(f != null);
968 return MkApp(f, args?.ToArray());
969 }
970
971 #region Propositional
975 public BoolExpr MkTrue()
976 {
977 return new BoolExpr(this, Native.Z3_mk_true(nCtx));
978 }
979
983 public BoolExpr MkFalse()
984 {
985 return new BoolExpr(this, Native.Z3_mk_false(nCtx));
986 }
987
991 public BoolExpr MkBool(bool value)
992 {
993 return value ? MkTrue() : MkFalse();
994 }
995
999 public BoolExpr MkEq(Expr x, Expr y)
1000 {
1001 Debug.Assert(x != null);
1002 Debug.Assert(y != null);
1003
1004 CheckContextMatch(x);
1005 CheckContextMatch(y);
1006 return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
1007 }
1008
1012 public BoolExpr MkDistinct(params Expr[] args)
1013 {
1014 Debug.Assert(args != null);
1015 Debug.Assert(args.All(a => a != null));
1016
1017 CheckContextMatch<Expr>(args);
1018 return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
1019 }
1020
1024 public BoolExpr MkDistinct(IEnumerable<Expr> args)
1025 {
1026 Debug.Assert(args != null);
1027 return MkDistinct(args.ToArray());
1028 }
1029
1033 public BoolExpr MkNot(BoolExpr a)
1034 {
1035 Debug.Assert(a != null);
1036 CheckContextMatch(a);
1037 return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
1038 }
1039
1046 public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
1047 {
1048 Debug.Assert(t1 != null);
1049 Debug.Assert(t2 != null);
1050 Debug.Assert(t3 != null);
1051
1052 CheckContextMatch(t1);
1053 CheckContextMatch(t2);
1054 CheckContextMatch(t3);
1055 return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
1056 }
1057
1061 public BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
1062 {
1063 Debug.Assert(t1 != null);
1064 Debug.Assert(t2 != null);
1065
1066 CheckContextMatch(t1);
1067 CheckContextMatch(t2);
1068 return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
1069 }
1070
1074 public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
1075 {
1076 Debug.Assert(t1 != null);
1077 Debug.Assert(t2 != null);
1078
1079 CheckContextMatch(t1);
1080 CheckContextMatch(t2);
1081 return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
1082 }
1083
1087 public BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
1088 {
1089 Debug.Assert(t1 != null);
1090 Debug.Assert(t2 != null);
1091
1092 CheckContextMatch(t1);
1093 CheckContextMatch(t2);
1094 return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
1095 }
1096
1100 public BoolExpr MkXor(IEnumerable<BoolExpr> args)
1101 {
1102 Debug.Assert(args != null);
1103 var ts = args.ToArray();
1104 Debug.Assert(ts.All(a => a != null));
1105 CheckContextMatch<BoolExpr>(ts);
1106
1107 return ts.Aggregate(MkFalse(), (r, t) =>
1108 {
1109 using (r)
1110 return MkXor(r, t);
1111 });
1112 }
1113
1117 public BoolExpr MkAnd(params BoolExpr[] ts)
1118 {
1119 Debug.Assert(ts != null);
1120 Debug.Assert(ts.All(a => a != null));
1121
1122 CheckContextMatch<BoolExpr>(ts);
1123 return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1124 }
1125
1129 public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
1130 {
1131 Debug.Assert(t != null);
1132 return MkAnd(t.ToArray());
1133 }
1134
1138 public BoolExpr MkOr(params BoolExpr[] ts)
1139 {
1140 Debug.Assert(ts != null);
1141 Debug.Assert(ts.All(a => a != null));
1142
1143 CheckContextMatch<BoolExpr>(ts);
1144 return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1145 }
1146
1147
1151 public BoolExpr MkOr(IEnumerable<BoolExpr> ts)
1152 {
1153 Debug.Assert(ts != null);
1154 return MkOr(ts.ToArray());
1155 }
1156
1157 #endregion
1158
1159 #region Arithmetic
1163 public ArithExpr MkAdd(params ArithExpr[] ts)
1164 {
1165 Debug.Assert(ts != null);
1166 Debug.Assert(ts.All(a => a != null));
1167
1168 CheckContextMatch<ArithExpr>(ts);
1169 return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1170 }
1171
1175 public ArithExpr MkAdd(IEnumerable<ArithExpr> ts)
1176 {
1177 Debug.Assert(ts != null);
1178 return MkAdd(ts.ToArray());
1179 }
1180
1184 public ArithExpr MkMul(params ArithExpr[] ts)
1185 {
1186 Debug.Assert(ts != null);
1187 Debug.Assert(ts.All(a => a != null));
1188
1189 CheckContextMatch<ArithExpr>(ts);
1190 return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1191 }
1192
1196 public ArithExpr MkMul(IEnumerable<ArithExpr> ts)
1197 {
1198 Debug.Assert(ts != null);
1199 return MkMul(ts.ToArray());
1200 }
1201
1205 public ArithExpr MkSub(params ArithExpr[] ts)
1206 {
1207 Debug.Assert(ts != null);
1208 Debug.Assert(ts.All(a => a != null));
1209
1210 CheckContextMatch<ArithExpr>(ts);
1211 return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1212 }
1213
1217 public ArithExpr MkUnaryMinus(ArithExpr t)
1218 {
1219 Debug.Assert(t != null);
1220
1221 CheckContextMatch(t);
1222 return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
1223 }
1224
1228 public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
1229 {
1230 Debug.Assert(t1 != null);
1231 Debug.Assert(t2 != null);
1232
1233 CheckContextMatch(t1);
1234 CheckContextMatch(t2);
1235 return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1236 }
1237
1242 public IntExpr MkMod(IntExpr t1, IntExpr t2)
1243 {
1244 Debug.Assert(t1 != null);
1245 Debug.Assert(t2 != null);
1246
1247 CheckContextMatch(t1);
1248 CheckContextMatch(t2);
1249 return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1250 }
1251
1256 public IntExpr MkRem(IntExpr t1, IntExpr t2)
1257 {
1258 Debug.Assert(t1 != null);
1259 Debug.Assert(t2 != null);
1260
1261 CheckContextMatch(t1);
1262 CheckContextMatch(t2);
1263 return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1264 }
1265
1269 public ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
1270 {
1271 Debug.Assert(t1 != null);
1272 Debug.Assert(t2 != null);
1273
1274 CheckContextMatch(t1);
1275 CheckContextMatch(t2);
1276 return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1277 }
1278
1282 public BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
1283 {
1284 Debug.Assert(t1 != null);
1285 Debug.Assert(t2 != null);
1286
1287 CheckContextMatch(t1);
1288 CheckContextMatch(t2);
1289 return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1290 }
1291
1295 public BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
1296 {
1297 Debug.Assert(t1 != null);
1298 Debug.Assert(t2 != null);
1299
1300 CheckContextMatch(t1);
1301 CheckContextMatch(t2);
1302 return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1303 }
1304
1308 public BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
1309 {
1310 Debug.Assert(t1 != null);
1311 Debug.Assert(t2 != null);
1312
1313 CheckContextMatch(t1);
1314 CheckContextMatch(t2);
1315 return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1316 }
1317
1321 public BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
1322 {
1323 Debug.Assert(t1 != null);
1324 Debug.Assert(t2 != null);
1325
1326 CheckContextMatch(t1);
1327 CheckContextMatch(t2);
1328 return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1329 }
1330
1341 public RealExpr MkInt2Real(IntExpr t)
1342 {
1343 Debug.Assert(t != null);
1344
1345 CheckContextMatch(t);
1346 return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1347 }
1348
1356 public IntExpr MkReal2Int(RealExpr t)
1357 {
1358 Debug.Assert(t != null);
1359
1360 CheckContextMatch(t);
1361 return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1362 }
1363
1367 public BoolExpr MkIsInteger(RealExpr t)
1368 {
1369 Debug.Assert(t != null);
1370
1371 CheckContextMatch(t);
1372 return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1373 }
1374 #endregion
1375
1376 #region Bit-vectors
1381 public BitVecExpr MkBVNot(BitVecExpr t)
1382 {
1383 Debug.Assert(t != null);
1384
1385 CheckContextMatch(t);
1386 return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1387 }
1388
1393 public BitVecExpr MkBVRedAND(BitVecExpr t)
1394 {
1395 Debug.Assert(t != null);
1396
1397 CheckContextMatch(t);
1398 return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1399 }
1400
1405 public BitVecExpr MkBVRedOR(BitVecExpr t)
1406 {
1407 Debug.Assert(t != null);
1408
1409 CheckContextMatch(t);
1410 return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1411 }
1412
1417 public BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
1418 {
1419 Debug.Assert(t1 != null);
1420 Debug.Assert(t2 != null);
1421
1422 CheckContextMatch(t1);
1423 CheckContextMatch(t2);
1424 return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1425 }
1426
1431 public BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
1432 {
1433 Debug.Assert(t1 != null);
1434 Debug.Assert(t2 != null);
1435
1436 CheckContextMatch(t1);
1437 CheckContextMatch(t2);
1438 return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1439 }
1440
1445 public BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
1446 {
1447 Debug.Assert(t1 != null);
1448 Debug.Assert(t2 != null);
1449
1450 CheckContextMatch(t1);
1451 CheckContextMatch(t2);
1452 return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1453 }
1454
1459 public BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
1460 {
1461 Debug.Assert(t1 != null);
1462 Debug.Assert(t2 != null);
1463
1464 CheckContextMatch(t1);
1465 CheckContextMatch(t2);
1466 return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1467 }
1468
1473 public BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
1474 {
1475 Debug.Assert(t1 != null);
1476 Debug.Assert(t2 != null);
1477
1478 CheckContextMatch(t1);
1479 CheckContextMatch(t2);
1480 return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1481 }
1482
1487 public BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
1488 {
1489 Debug.Assert(t1 != null);
1490 Debug.Assert(t2 != null);
1491
1492 CheckContextMatch(t1);
1493 CheckContextMatch(t2);
1494 return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1495 }
1496
1501 public BitVecExpr MkBVNeg(BitVecExpr t)
1502 {
1503 Debug.Assert(t != null);
1504
1505 CheckContextMatch(t);
1506 return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1507 }
1508
1513 public BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
1514 {
1515 Debug.Assert(t1 != null);
1516 Debug.Assert(t2 != null);
1517
1518 CheckContextMatch(t1);
1519 CheckContextMatch(t2);
1520 return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1521 }
1522
1527 public BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
1528 {
1529 Debug.Assert(t1 != null);
1530 Debug.Assert(t2 != null);
1531
1532 CheckContextMatch(t1);
1533 CheckContextMatch(t2);
1534 return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1535 }
1536
1541 public BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
1542 {
1543 Debug.Assert(t1 != null);
1544 Debug.Assert(t2 != null);
1545
1546 CheckContextMatch(t1);
1547 CheckContextMatch(t2);
1548 return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1549 }
1550
1560 public BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
1561 {
1562 Debug.Assert(t1 != null);
1563 Debug.Assert(t2 != null);
1564
1565 CheckContextMatch(t1);
1566 CheckContextMatch(t2);
1567 return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1568 }
1569
1583 public BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
1584 {
1585 Debug.Assert(t1 != null);
1586 Debug.Assert(t2 != null);
1587
1588 CheckContextMatch(t1);
1589 CheckContextMatch(t2);
1590 return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1591 }
1592
1601 public BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
1602 {
1603 Debug.Assert(t1 != null);
1604 Debug.Assert(t2 != null);
1605
1606 CheckContextMatch(t1);
1607 CheckContextMatch(t2);
1608 return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1609 }
1610
1621 public BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
1622 {
1623 Debug.Assert(t1 != null);
1624 Debug.Assert(t2 != null);
1625
1626 CheckContextMatch(t1);
1627 CheckContextMatch(t2);
1628 return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1629 }
1630
1638 public BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
1639 {
1640 Debug.Assert(t1 != null);
1641 Debug.Assert(t2 != null);
1642
1643 CheckContextMatch(t1);
1644 CheckContextMatch(t2);
1645 return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1646 }
1647
1654 public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
1655 {
1656 Debug.Assert(t1 != null);
1657 Debug.Assert(t2 != null);
1658
1659 CheckContextMatch(t1);
1660 CheckContextMatch(t2);
1661 return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1662 }
1663
1670 public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
1671 {
1672 Debug.Assert(t1 != null);
1673 Debug.Assert(t2 != null);
1674
1675 CheckContextMatch(t1);
1676 CheckContextMatch(t2);
1677 return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1678 }
1679
1686 public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
1687 {
1688 Debug.Assert(t1 != null);
1689 Debug.Assert(t2 != null);
1690
1691 CheckContextMatch(t1);
1692 CheckContextMatch(t2);
1693 return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1694 }
1695
1702 public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
1703 {
1704 Debug.Assert(t1 != null);
1705 Debug.Assert(t2 != null);
1706
1707 CheckContextMatch(t1);
1708 CheckContextMatch(t2);
1709 return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1710 }
1711
1718 public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
1719 {
1720 Debug.Assert(t1 != null);
1721 Debug.Assert(t2 != null);
1722
1723 CheckContextMatch(t1);
1724 CheckContextMatch(t2);
1725 return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1726 }
1727
1734 public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
1735 {
1736 Debug.Assert(t1 != null);
1737 Debug.Assert(t2 != null);
1738
1739 CheckContextMatch(t1);
1740 CheckContextMatch(t2);
1741 return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1742 }
1743
1750 public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
1751 {
1752 Debug.Assert(t1 != null);
1753 Debug.Assert(t2 != null);
1754
1755 CheckContextMatch(t1);
1756 CheckContextMatch(t2);
1757 return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1758 }
1759
1766 public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
1767 {
1768 Debug.Assert(t1 != null);
1769 Debug.Assert(t2 != null);
1770
1771 CheckContextMatch(t1);
1772 CheckContextMatch(t2);
1773 return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1774 }
1775
1786 public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
1787 {
1788 Debug.Assert(t1 != null);
1789 Debug.Assert(t2 != null);
1790
1791 CheckContextMatch(t1);
1792 CheckContextMatch(t2);
1793 return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1794 }
1795
1805 public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
1806 {
1807 Debug.Assert(t != null);
1808
1809 CheckContextMatch(t);
1810 return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1811 }
1812
1821 public BitVecExpr MkSignExt(uint i, BitVecExpr t)
1822 {
1823 Debug.Assert(t != null);
1824
1825 CheckContextMatch(t);
1826 return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1827 }
1828
1838 public BitVecExpr MkZeroExt(uint i, BitVecExpr t)
1839 {
1840 Debug.Assert(t != null);
1841
1842 CheckContextMatch(t);
1843 return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1844 }
1845
1852 public BitVecExpr MkRepeat(uint i, BitVecExpr t)
1853 {
1854 Debug.Assert(t != null);
1855
1856 CheckContextMatch(t);
1857 return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1858 }
1859
1872 public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
1873 {
1874 Debug.Assert(t1 != null);
1875 Debug.Assert(t2 != null);
1876
1877 CheckContextMatch(t1);
1878 CheckContextMatch(t2);
1879 return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1880 }
1881
1894 public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
1895 {
1896 Debug.Assert(t1 != null);
1897 Debug.Assert(t2 != null);
1898
1899 CheckContextMatch(t1);
1900 CheckContextMatch(t2);
1901 return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1902 }
1903
1918 public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
1919 {
1920 Debug.Assert(t1 != null);
1921 Debug.Assert(t2 != null);
1922
1923 CheckContextMatch(t1);
1924 CheckContextMatch(t2);
1925 return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1926 }
1927
1935 public BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
1936 {
1937 Debug.Assert(t != null);
1938
1939 CheckContextMatch(t);
1940 return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1941 }
1942
1950 public BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
1951 {
1952 Debug.Assert(t != null);
1953
1954 CheckContextMatch(t);
1955 return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1956 }
1957
1965 public BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
1966 {
1967 Debug.Assert(t1 != null);
1968 Debug.Assert(t2 != null);
1969
1970 CheckContextMatch(t1);
1971 CheckContextMatch(t2);
1972 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1973 }
1974
1982 public BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
1983 {
1984 Debug.Assert(t1 != null);
1985 Debug.Assert(t2 != null);
1986
1987 CheckContextMatch(t1);
1988 CheckContextMatch(t2);
1989 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1990 }
1991
2002 public BitVecExpr MkInt2BV(uint n, IntExpr t)
2003 {
2004 Debug.Assert(t != null);
2005
2006 CheckContextMatch(t);
2007 return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
2008 }
2009
2025 public IntExpr MkBV2Int(BitVecExpr t, bool signed)
2026 {
2027 Debug.Assert(t != null);
2028
2029 CheckContextMatch(t);
2030 return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (byte)(signed ? 1 : 0)));
2031 }
2032
2039 public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
2040 {
2041 Debug.Assert(t1 != null);
2042 Debug.Assert(t2 != null);
2043
2044 CheckContextMatch(t1);
2045 CheckContextMatch(t2);
2046 return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
2047 }
2048
2055 public BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
2056 {
2057 Debug.Assert(t1 != null);
2058 Debug.Assert(t2 != null);
2059
2060 CheckContextMatch(t1);
2061 CheckContextMatch(t2);
2062 return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2063 }
2064
2071 public BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
2072 {
2073 Debug.Assert(t1 != null);
2074 Debug.Assert(t2 != null);
2075
2076 CheckContextMatch(t1);
2077 CheckContextMatch(t2);
2078 return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2079 }
2080
2087 public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
2088 {
2089 Debug.Assert(t1 != null);
2090 Debug.Assert(t2 != null);
2091
2092 CheckContextMatch(t1);
2093 CheckContextMatch(t2);
2094 return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
2095 }
2096
2103 public BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
2104 {
2105 Debug.Assert(t1 != null);
2106 Debug.Assert(t2 != null);
2107
2108 CheckContextMatch(t1);
2109 CheckContextMatch(t2);
2110 return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2111 }
2112
2119 public BoolExpr MkBVNegNoOverflow(BitVecExpr t)
2120 {
2121 Debug.Assert(t != null);
2122
2123 CheckContextMatch(t);
2124 return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
2125 }
2126
2133 public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
2134 {
2135 Debug.Assert(t1 != null);
2136 Debug.Assert(t2 != null);
2137
2138 CheckContextMatch(t1);
2139 CheckContextMatch(t2);
2140 return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
2141 }
2142
2149 public BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
2150 {
2151 Debug.Assert(t1 != null);
2152 Debug.Assert(t2 != null);
2153
2154 CheckContextMatch(t1);
2155 CheckContextMatch(t2);
2156 return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2157 }
2158 #endregion
2159
2160 #region Arrays
2164 public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
2165 {
2166 Debug.Assert(name != null);
2167 Debug.Assert(domain != null);
2168 Debug.Assert(range != null);
2169
2170 using var sort = MkArraySort(domain, range);
2171 return (ArrayExpr)MkConst(name, sort);
2172 }
2173
2177 public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
2178 {
2179 Debug.Assert(domain != null);
2180 Debug.Assert(range != null);
2181
2182 using var symbol = MkSymbol(name);
2183 using var sort = MkArraySort(domain, range);
2184 return (ArrayExpr)MkConst(symbol, sort);
2185 }
2186
2187
2201 public Expr MkSelect(ArrayExpr a, Expr i)
2202 {
2203 Debug.Assert(a != null);
2204 Debug.Assert(i != null);
2205
2206 CheckContextMatch(a);
2207 CheckContextMatch(i);
2208 return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2209 }
2210
2224 public Expr MkSelect(ArrayExpr a, params Expr[] args)
2225 {
2226 Debug.Assert(a != null);
2227 Debug.Assert(args != null && args.All(n => n != null));
2228
2229 CheckContextMatch(a);
2230 CheckContextMatch<Expr>(args);
2231 return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2232 }
2233
2234
2253 public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
2254 {
2255 Debug.Assert(a != null);
2256 Debug.Assert(i != null);
2257 Debug.Assert(v != null);
2258
2259 CheckContextMatch(a);
2260 CheckContextMatch(i);
2261 CheckContextMatch(v);
2262 return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2263 }
2264
2283 public ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
2284 {
2285 Debug.Assert(a != null);
2286 Debug.Assert(args != null);
2287 Debug.Assert(v != null);
2288
2289 CheckContextMatch<Expr>(args);
2290 CheckContextMatch(a);
2291 CheckContextMatch(v);
2292 return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
2293 }
2294
2304 public ArrayExpr MkConstArray(Sort domain, Expr v)
2305 {
2306 Debug.Assert(domain != null);
2307 Debug.Assert(v != null);
2308
2309 CheckContextMatch(domain);
2310 CheckContextMatch(v);
2311 return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2312 }
2313
2325 public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
2326 {
2327 Debug.Assert(f != null);
2328 Debug.Assert(args == null || args.All(a => a != null));
2329
2330 CheckContextMatch(f);
2331 CheckContextMatch<ArrayExpr>(args);
2332 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2333 }
2334
2342 public Expr MkTermArray(ArrayExpr array)
2343 {
2344 Debug.Assert(array != null);
2345
2346 CheckContextMatch(array);
2347 return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2348 }
2349
2353 public Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
2354 {
2355 Debug.Assert(arg1 != null);
2356 Debug.Assert(arg2 != null);
2357
2358 CheckContextMatch(arg1);
2359 CheckContextMatch(arg2);
2360 return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
2361 }
2362
2363 #endregion
2364
2365 #region Sets
2369 public SetSort MkSetSort(Sort ty)
2370 {
2371 Debug.Assert(ty != null);
2372
2373 CheckContextMatch(ty);
2374 return new SetSort(this, ty);
2375 }
2376
2380 public ArrayExpr MkEmptySet(Sort domain)
2381 {
2382 Debug.Assert(domain != null);
2383
2384 CheckContextMatch(domain);
2385 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2386 }
2387
2391 public ArrayExpr MkFullSet(Sort domain)
2392 {
2393 Debug.Assert(domain != null);
2394
2395 CheckContextMatch(domain);
2396 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2397 }
2398
2402 public ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
2403 {
2404 Debug.Assert(set != null);
2405 Debug.Assert(element != null);
2406
2407 CheckContextMatch(set);
2408 CheckContextMatch(element);
2409 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2410 }
2411
2412
2416 public ArrayExpr MkSetDel(ArrayExpr set, Expr element)
2417 {
2418 Debug.Assert(set != null);
2419 Debug.Assert(element != null);
2420
2421 CheckContextMatch(set);
2422 CheckContextMatch(element);
2423 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2424 }
2425
2429 public ArrayExpr MkSetUnion(params ArrayExpr[] args)
2430 {
2431 Debug.Assert(args != null);
2432 Debug.Assert(args.All(a => a != null));
2433
2434 CheckContextMatch<ArrayExpr>(args);
2435 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2436 }
2437
2441 public ArrayExpr MkSetIntersection(params ArrayExpr[] args)
2442 {
2443 Debug.Assert(args != null);
2444 Debug.Assert(args.All(a => a != null));
2445
2446 CheckContextMatch<ArrayExpr>(args);
2447 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2448 }
2449
2453 public ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
2454 {
2455 Debug.Assert(arg1 != null);
2456 Debug.Assert(arg2 != null);
2457
2458 CheckContextMatch(arg1);
2459 CheckContextMatch(arg2);
2460 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2461 }
2462
2466 public ArrayExpr MkSetComplement(ArrayExpr arg)
2467 {
2468 Debug.Assert(arg != null);
2469
2470 CheckContextMatch(arg);
2471 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2472 }
2473
2477 public BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
2478 {
2479 Debug.Assert(elem != null);
2480 Debug.Assert(set != null);
2481
2482 CheckContextMatch(elem);
2483 CheckContextMatch(set);
2484 return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2485 }
2486
2490 public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
2491 {
2492 Debug.Assert(arg1 != null);
2493 Debug.Assert(arg2 != null);
2494
2495 CheckContextMatch(arg1);
2496 CheckContextMatch(arg2);
2497 return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2498 }
2499
2500 #endregion
2501
2502 #region Finite Sets
2503
2507 public FiniteSetSort MkFiniteSetSort(Sort elemSort)
2508 {
2509 Debug.Assert(elemSort != null);
2510
2511 CheckContextMatch(elemSort);
2512 return new FiniteSetSort(this, elemSort);
2513 }
2514
2518 public bool IsFiniteSetSort(Sort s)
2519 {
2520 Debug.Assert(s != null);
2521
2522 CheckContextMatch(s);
2523 return Native.Z3_is_finite_set_sort(nCtx, s.NativeObject) != 0;
2524 }
2525
2529 public Sort GetFiniteSetSortBasis(Sort s)
2530 {
2531 Debug.Assert(s != null);
2532
2533 CheckContextMatch(s);
2534 return Sort.Create(this, Native.Z3_get_finite_set_sort_basis(nCtx, s.NativeObject));
2535 }
2536
2540 public Expr MkFiniteSetEmpty(Sort setSort)
2541 {
2542 Debug.Assert(setSort != null);
2543
2544 CheckContextMatch(setSort);
2545 return Expr.Create(this, Native.Z3_mk_finite_set_empty(nCtx, setSort.NativeObject));
2546 }
2547
2551 public Expr MkFiniteSetSingleton(Expr elem)
2552 {
2553 Debug.Assert(elem != null);
2554
2555 CheckContextMatch(elem);
2556 return Expr.Create(this, Native.Z3_mk_finite_set_singleton(nCtx, elem.NativeObject));
2557 }
2558
2562 public Expr MkFiniteSetUnion(Expr s1, Expr s2)
2563 {
2564 Debug.Assert(s1 != null);
2565 Debug.Assert(s2 != null);
2566
2567 CheckContextMatch(s1);
2568 CheckContextMatch(s2);
2569 return Expr.Create(this, Native.Z3_mk_finite_set_union(nCtx, s1.NativeObject, s2.NativeObject));
2570 }
2571
2575 public Expr MkFiniteSetIntersect(Expr s1, Expr s2)
2576 {
2577 Debug.Assert(s1 != null);
2578 Debug.Assert(s2 != null);
2579
2580 CheckContextMatch(s1);
2581 CheckContextMatch(s2);
2582 return Expr.Create(this, Native.Z3_mk_finite_set_intersect(nCtx, s1.NativeObject, s2.NativeObject));
2583 }
2584
2588 public Expr MkFiniteSetDifference(Expr s1, Expr s2)
2589 {
2590 Debug.Assert(s1 != null);
2591 Debug.Assert(s2 != null);
2592
2593 CheckContextMatch(s1);
2594 CheckContextMatch(s2);
2595 return Expr.Create(this, Native.Z3_mk_finite_set_difference(nCtx, s1.NativeObject, s2.NativeObject));
2596 }
2597
2601 public BoolExpr MkFiniteSetMember(Expr elem, Expr set)
2602 {
2603 Debug.Assert(elem != null);
2604 Debug.Assert(set != null);
2605
2606 CheckContextMatch(elem);
2607 CheckContextMatch(set);
2608 return (BoolExpr)Expr.Create(this, Native.Z3_mk_finite_set_member(nCtx, elem.NativeObject, set.NativeObject));
2609 }
2610
2614 public Expr MkFiniteSetSize(Expr set)
2615 {
2616 Debug.Assert(set != null);
2617
2618 CheckContextMatch(set);
2619 return Expr.Create(this, Native.Z3_mk_finite_set_size(nCtx, set.NativeObject));
2620 }
2621
2625 public BoolExpr MkFiniteSetSubset(Expr s1, Expr s2)
2626 {
2627 Debug.Assert(s1 != null);
2628 Debug.Assert(s2 != null);
2629
2630 CheckContextMatch(s1);
2631 CheckContextMatch(s2);
2632 return (BoolExpr)Expr.Create(this, Native.Z3_mk_finite_set_subset(nCtx, s1.NativeObject, s2.NativeObject));
2633 }
2634
2638 public Expr MkFiniteSetMap(Expr f, Expr set)
2639 {
2640 Debug.Assert(f != null);
2641 Debug.Assert(set != null);
2642
2643 CheckContextMatch(f);
2644 CheckContextMatch(set);
2645 return Expr.Create(this, Native.Z3_mk_finite_set_map(nCtx, f.NativeObject, set.NativeObject));
2646 }
2647
2651 public Expr MkFiniteSetFilter(Expr f, Expr set)
2652 {
2653 Debug.Assert(f != null);
2654 Debug.Assert(set != null);
2655
2656 CheckContextMatch(f);
2657 CheckContextMatch(set);
2658 return Expr.Create(this, Native.Z3_mk_finite_set_filter(nCtx, f.NativeObject, set.NativeObject));
2659 }
2660
2664 public Expr MkFiniteSetRange(Expr low, Expr high)
2665 {
2666 Debug.Assert(low != null);
2667 Debug.Assert(high != null);
2668
2669 CheckContextMatch(low);
2670 CheckContextMatch(high);
2671 return Expr.Create(this, Native.Z3_mk_finite_set_range(nCtx, low.NativeObject, high.NativeObject));
2672 }
2673
2674 #endregion
2675
2676 #region Sequence, string and regular expressions
2677
2681 public SeqExpr MkEmptySeq(Sort s)
2682 {
2683 Debug.Assert(s != null);
2684 return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
2685 }
2686
2690 public SeqExpr MkUnit(Expr elem)
2691 {
2692 Debug.Assert(elem != null);
2693 return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
2694 }
2695
2699 public SeqExpr MkString(string s)
2700 {
2701 Debug.Assert(s != null);
2702 return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
2703 }
2704
2708 public SeqExpr IntToString(Expr e)
2709 {
2710 Debug.Assert(e != null);
2711 Debug.Assert(e is ArithExpr);
2712 return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
2713 }
2714
2718 public SeqExpr UbvToString(Expr e)
2719 {
2720 Debug.Assert(e != null);
2721 Debug.Assert(e is ArithExpr);
2722 return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject));
2723 }
2724
2728 public SeqExpr SbvToString(Expr e)
2729 {
2730 Debug.Assert(e != null);
2731 Debug.Assert(e is ArithExpr);
2732 return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject));
2733 }
2734
2738 public IntExpr StringToInt(Expr e)
2739 {
2740 Debug.Assert(e != null);
2741 Debug.Assert(e is SeqExpr);
2742 return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject));
2743 }
2744
2745
2749 public SeqExpr MkConcat(params SeqExpr[] t)
2750 {
2751 Debug.Assert(t != null);
2752 Debug.Assert(t.All(a => a != null));
2753
2754 CheckContextMatch<SeqExpr>(t);
2755 return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2756 }
2757
2758
2762 public IntExpr MkLength(SeqExpr s)
2763 {
2764 Debug.Assert(s != null);
2765 return (IntExpr)Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
2766 }
2767
2771 public SeqExpr MkSeqPower(SeqExpr s, Expr n)
2772 {
2773 Debug.Assert(s != null);
2774 Debug.Assert(n != null);
2775 CheckContextMatch(s, n);
2776 return new SeqExpr(this, Native.Z3_mk_seq_power(nCtx, s.NativeObject, n.NativeObject));
2777 }
2778
2782 public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
2783 {
2784 Debug.Assert(s1 != null);
2785 Debug.Assert(s2 != null);
2786 CheckContextMatch(s1, s2);
2787 return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
2788 }
2789
2793 public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
2794 {
2795 Debug.Assert(s1 != null);
2796 Debug.Assert(s2 != null);
2797 CheckContextMatch(s1, s2);
2798 return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
2799 }
2800
2804 public BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
2805 {
2806 Debug.Assert(s1 != null);
2807 Debug.Assert(s2 != null);
2808 CheckContextMatch(s1, s2);
2809 return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
2810 }
2811
2815 public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
2816 {
2817 Debug.Assert(s1 != null);
2818 Debug.Assert(s2 != null);
2819 CheckContextMatch(s1, s2);
2820 return new BoolExpr(this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject));
2821 }
2822
2826 public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2)
2827 {
2828 Debug.Assert(s1 != null);
2829 Debug.Assert(s2 != null);
2830 CheckContextMatch(s1, s2);
2831 return new BoolExpr(this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject));
2832 }
2833
2837 public SeqExpr MkAt(SeqExpr s, Expr index)
2838 {
2839 Debug.Assert(s != null);
2840 Debug.Assert(index != null);
2841 CheckContextMatch(s, index);
2842 return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
2843 }
2844
2848 public Expr MkNth(SeqExpr s, Expr index)
2849 {
2850 Debug.Assert(s != null);
2851 Debug.Assert(index != null);
2852 CheckContextMatch(s, index);
2853 return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
2854 }
2855
2859 public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
2860 {
2861 Debug.Assert(s != null);
2862 Debug.Assert(offset != null);
2863 Debug.Assert(length != null);
2864 CheckContextMatch(s, offset, length);
2865 return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
2866 }
2867
2871 public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
2872 {
2873 Debug.Assert(s != null);
2874 Debug.Assert(offset != null);
2875 Debug.Assert(substr != null);
2876 CheckContextMatch(s, substr, offset);
2877 return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
2878 }
2879
2883 public SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
2884 {
2885 Debug.Assert(s != null);
2886 Debug.Assert(src != null);
2887 Debug.Assert(dst != null);
2888 CheckContextMatch(s, src, dst);
2889 return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
2890 }
2891
2895 public Expr MkSeqMap(Expr f, SeqExpr s)
2896 {
2897 Debug.Assert(f != null);
2898 Debug.Assert(s != null);
2899 CheckContextMatch(f, s);
2900 return Expr.Create(this, Native.Z3_mk_seq_map(nCtx, f.NativeObject, s.NativeObject));
2901 }
2902
2906 public Expr MkSeqMapi(Expr f, Expr i, SeqExpr s)
2907 {
2908 Debug.Assert(f != null);
2909 Debug.Assert(i != null);
2910 Debug.Assert(s != null);
2911 CheckContextMatch(f, i, s);
2912 return Expr.Create(this, Native.Z3_mk_seq_mapi(nCtx, f.NativeObject, i.NativeObject, s.NativeObject));
2913 }
2914
2918 public Expr MkSeqFoldLeft(Expr f, Expr a, SeqExpr s)
2919 {
2920 Debug.Assert(f != null);
2921 Debug.Assert(a != null);
2922 Debug.Assert(s != null);
2923 CheckContextMatch(f, a, s);
2924 return Expr.Create(this, Native.Z3_mk_seq_foldl(nCtx, f.NativeObject, a.NativeObject, s.NativeObject));
2925 }
2926
2930 public Expr MkSeqFoldLeftI(Expr f, Expr i, Expr a, SeqExpr s)
2931 {
2932 Debug.Assert(f != null);
2933 Debug.Assert(i != null);
2934 Debug.Assert(a != null);
2935 Debug.Assert(s != null);
2936 CheckContextMatch(f, i, a);
2937 CheckContextMatch(s, a);
2938 return Expr.Create(this, Native.Z3_mk_seq_foldli(nCtx, f.NativeObject, i.NativeObject, a.NativeObject, s.NativeObject));
2939 }
2940
2944 public ReExpr MkToRe(SeqExpr s)
2945 {
2946 Debug.Assert(s != null);
2947 return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));
2948 }
2949
2950
2954 public BoolExpr MkInRe(SeqExpr s, ReExpr re)
2955 {
2956 Debug.Assert(s != null);
2957 Debug.Assert(re != null);
2958 CheckContextMatch(s, re);
2959 return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
2960 }
2961
2965 public ReExpr MkStar(ReExpr re)
2966 {
2967 Debug.Assert(re != null);
2968 return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
2969 }
2970
2974 public ReExpr MkLoop(ReExpr re, uint lo, uint hi = 0)
2975 {
2976 Debug.Assert(re != null);
2977 return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi));
2978 }
2979
2983 public ReExpr MkPlus(ReExpr re)
2984 {
2985 Debug.Assert(re != null);
2986 return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));
2987 }
2988
2992 public ReExpr MkOption(ReExpr re)
2993 {
2994 Debug.Assert(re != null);
2995 return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
2996 }
2997
3001 public ReExpr MkComplement(ReExpr re)
3002 {
3003 Debug.Assert(re != null);
3004 return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject));
3005 }
3006
3010 public ReExpr MkConcat(params ReExpr[] t)
3011 {
3012 Debug.Assert(t != null);
3013 Debug.Assert(t.All(a => a != null));
3014
3015 CheckContextMatch<ReExpr>(t);
3016 return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
3017 }
3018
3022 public ReExpr MkUnion(params ReExpr[] t)
3023 {
3024 Debug.Assert(t != null);
3025 Debug.Assert(t.All(a => a != null));
3026
3027 CheckContextMatch<ReExpr>(t);
3028 return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
3029 }
3030
3034 public ReExpr MkIntersect(params ReExpr[] t)
3035 {
3036 Debug.Assert(t != null);
3037 Debug.Assert(t.All(a => a != null));
3038
3039 CheckContextMatch<ReExpr>(t);
3040 return new ReExpr(this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
3041 }
3042
3046 public ReExpr MkDiff(ReExpr a, ReExpr b)
3047 {
3048 Debug.Assert(a != null);
3049 Debug.Assert(b != null);
3050 CheckContextMatch(a, b);
3051 return new ReExpr(this, Native.Z3_mk_re_diff(nCtx, a.NativeObject, b.NativeObject));
3052 }
3053
3058 public ReExpr MkEmptyRe(Sort s)
3059 {
3060 Debug.Assert(s != null);
3061 return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject));
3062 }
3063
3068 public ReExpr MkFullRe(Sort s)
3069 {
3070 Debug.Assert(s != null);
3071 return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject));
3072 }
3073
3074
3078 public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
3079 {
3080 Debug.Assert(lo != null);
3081 Debug.Assert(hi != null);
3082 CheckContextMatch(lo, hi);
3083 return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
3084 }
3085
3089 public BoolExpr MkCharLe(Expr ch1, Expr ch2)
3090 {
3091 Debug.Assert(ch1 != null);
3092 Debug.Assert(ch2 != null);
3093 return new BoolExpr(this, Native.Z3_mk_char_le(nCtx, ch1.NativeObject, ch2.NativeObject));
3094 }
3095
3099 public IntExpr CharToInt(Expr ch)
3100 {
3101 Debug.Assert(ch != null);
3102 return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject));
3103 }
3104
3108 public BitVecExpr CharToBV(Expr ch)
3109 {
3110 Debug.Assert(ch != null);
3111 return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject));
3112 }
3113
3117 public Expr CharFromBV(BitVecExpr bv)
3118 {
3119 Debug.Assert(bv != null);
3120 return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject));
3121 }
3122
3126 public BoolExpr MkIsDigit(Expr ch)
3127 {
3128 Debug.Assert(ch != null);
3129 return new BoolExpr(this, Native.Z3_mk_char_is_digit(nCtx, ch.NativeObject));
3130 }
3131
3132 #endregion
3133
3134 #region Pseudo-Boolean constraints
3135
3139 public BoolExpr MkAtMost(IEnumerable<BoolExpr> args, uint k)
3140 {
3141 Debug.Assert(args != null);
3142 var ts = args.ToArray();
3143 CheckContextMatch<BoolExpr>(ts);
3144 return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint)ts.Length,
3145 AST.ArrayToNative(ts), k));
3146 }
3147
3151 public BoolExpr MkAtLeast(IEnumerable<BoolExpr> args, uint k)
3152 {
3153 Debug.Assert(args != null);
3154 var ts = args.ToArray();
3155 CheckContextMatch<BoolExpr>(ts);
3156 return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint)ts.Length,
3157 AST.ArrayToNative(ts), k));
3158 }
3159
3163 public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
3164 {
3165 Debug.Assert(args != null);
3166 Debug.Assert(coeffs != null);
3167 Debug.Assert(args.Length == coeffs.Length);
3168 CheckContextMatch<BoolExpr>(args);
3169 return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint)args.Length,
3170 AST.ArrayToNative(args),
3171 coeffs, k));
3172 }
3173
3177 public BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k)
3178 {
3179 Debug.Assert(args != null);
3180 Debug.Assert(coeffs != null);
3181 Debug.Assert(args.Length == coeffs.Length);
3182 CheckContextMatch<BoolExpr>(args);
3183 return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint)args.Length,
3184 AST.ArrayToNative(args),
3185 coeffs, k));
3186 }
3190 public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
3191 {
3192 Debug.Assert(args != null);
3193 Debug.Assert(coeffs != null);
3194 Debug.Assert(args.Length == coeffs.Length);
3195 CheckContextMatch<BoolExpr>(args);
3196 return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint)args.Length,
3197 AST.ArrayToNative(args),
3198 coeffs, k));
3199 }
3200 #endregion
3201
3202 #region Numerals
3203
3204 #region General Numerals
3211 public Expr MkNumeral(string v, Sort ty)
3212 {
3213 Debug.Assert(ty != null);
3214
3215 CheckContextMatch(ty);
3216 return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
3217 }
3218
3226 public Expr MkNumeral(int v, Sort ty)
3227 {
3228 Debug.Assert(ty != null);
3229
3230 CheckContextMatch(ty);
3231 return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
3232 }
3233
3241 public Expr MkNumeral(uint v, Sort ty)
3242 {
3243 Debug.Assert(ty != null);
3244
3245 CheckContextMatch(ty);
3246 return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
3247 }
3248
3256 public Expr MkNumeral(long v, Sort ty)
3257 {
3258 Debug.Assert(ty != null);
3259
3260 CheckContextMatch(ty);
3261 return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
3262 }
3263
3271 public Expr MkNumeral(ulong v, Sort ty)
3272 {
3273 Debug.Assert(ty != null);
3274
3275 CheckContextMatch(ty);
3276 return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
3277 }
3278 #endregion
3279
3280 #region Reals
3288 public RatNum MkReal(int num, int den)
3289 {
3290 if (den == 0)
3291 throw new Z3Exception("Denominator is zero");
3292
3293 return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
3294 }
3295
3301 public RatNum MkReal(string v)
3302 {
3303
3304 return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
3305 }
3306
3312 public RatNum MkReal(int v)
3313 {
3314
3315 return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
3316 }
3317
3323 public RatNum MkReal(uint v)
3324 {
3325
3326 return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
3327 }
3328
3334 public RatNum MkReal(long v)
3335 {
3336
3337 return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
3338 }
3339
3345 public RatNum MkReal(ulong v)
3346 {
3347
3348 return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
3349 }
3350 #endregion
3351
3352 #region Integers
3357 public IntNum MkInt(string v)
3358 {
3359
3360 return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
3361 }
3362
3368 public IntNum MkInt(int v)
3369 {
3370
3371 return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
3372 }
3373
3379 public IntNum MkInt(uint v)
3380 {
3381
3382 return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
3383 }
3384
3390 public IntNum MkInt(long v)
3391 {
3392
3393 return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
3394 }
3395
3401 public IntNum MkInt(ulong v)
3402 {
3403
3404 return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
3405 }
3406 #endregion
3407
3408 #region Bit-vectors
3414 public BitVecNum MkBV(string v, uint size)
3415 {
3416 using var sort = MkBitVecSort(size);
3417 return (BitVecNum)MkNumeral(v, sort);
3418 }
3419
3425 public BitVecNum MkBV(int v, uint size)
3426 {
3427 using var sort = MkBitVecSort(size);
3428 return (BitVecNum)MkNumeral(v, sort);
3429 }
3430
3436 public BitVecNum MkBV(uint v, uint size)
3437 {
3438 using var sort = MkBitVecSort(size);
3439 return (BitVecNum)MkNumeral(v, sort);
3440 }
3441
3447 public BitVecNum MkBV(long v, uint size)
3448 {
3449 using var sort = MkBitVecSort(size);
3450 return (BitVecNum)MkNumeral(v, sort);
3451 }
3452
3458 public BitVecNum MkBV(ulong v, uint size)
3459 {
3460 using var sort = MkBitVecSort(size);
3461 return (BitVecNum)MkNumeral(v, sort);
3462 }
3463
3468 public BitVecNum MkBV(bool[] bits)
3469 {
3470 byte[] _bits = new byte[bits.Length];
3471 for (int i = 0; i < bits.Length; ++i) _bits[i] = (byte)(bits[i] ? 1 : 0);
3472 return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
3473 }
3474
3475
3476 #endregion
3477
3478 #endregion // Numerals
3479
3480 #region Quantifiers
3505 public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3506 {
3507 Debug.Assert(sorts != null);
3508 Debug.Assert(names != null);
3509 Debug.Assert(body != null);
3510 Debug.Assert(sorts.Length == names.Length);
3511 Debug.Assert(sorts.All(s => s != null));
3512 Debug.Assert(names.All(n => n != null));
3513 Debug.Assert(patterns == null || patterns.All(p => p != null));
3514 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3515
3516
3517 return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3518 }
3519
3520
3529 public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3530 {
3531 Debug.Assert(body != null);
3532 Debug.Assert(boundConstants == null || boundConstants.All(b => b != null));
3533 Debug.Assert(patterns == null || patterns.All(p => p != null));
3534 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3535
3536
3537 return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3538 }
3539
3547 public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3548 {
3549 Debug.Assert(sorts != null);
3550 Debug.Assert(names != null);
3551 Debug.Assert(body != null);
3552 Debug.Assert(sorts.Length == names.Length);
3553 Debug.Assert(sorts.All(s => s != null));
3554 Debug.Assert(names.All(n => n != null));
3555 Debug.Assert(patterns == null || patterns.All(p => p != null));
3556 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3557
3558 return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3559 }
3560
3569 public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3570 {
3571 Debug.Assert(body != null);
3572 Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3573 Debug.Assert(patterns == null || patterns.All(p => p != null));
3574 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3575
3576 return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3577 }
3578
3579
3584 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)
3585 {
3586 Debug.Assert(body != null);
3587 Debug.Assert(names != null);
3588 Debug.Assert(sorts != null);
3589 Debug.Assert(sorts.Length == names.Length);
3590 Debug.Assert(sorts.All(s => s != null));
3591 Debug.Assert(names.All(n => n != null));
3592 Debug.Assert(patterns == null || patterns.All(p => p != null));
3593 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3594
3595
3596 if (universal)
3597 return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3598 else
3599 return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3600 }
3601
3602
3607 public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3608 {
3609 Debug.Assert(body != null);
3610 Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3611 Debug.Assert(patterns == null || patterns.All(p => p != null));
3612 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3613
3614
3615 if (universal)
3616 return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3617 else
3618 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3619 }
3620
3639 public Lambda MkLambda(Sort[] sorts, Symbol[] names, Expr body)
3640 {
3641 Debug.Assert(sorts != null);
3642 Debug.Assert(names != null);
3643 Debug.Assert(body != null);
3644 Debug.Assert(sorts.Length == names.Length);
3645 Debug.Assert(sorts.All(s => s != null));
3646 Debug.Assert(names.All(n => n != null));
3647 return new Lambda(this, sorts, names, body);
3648 }
3649
3658 public Lambda MkLambda(Expr[] boundConstants, Expr body)
3659 {
3660 Debug.Assert(body != null);
3661 Debug.Assert(boundConstants != null && boundConstants.All(b => b != null));
3662 return new Lambda(this, boundConstants, body);
3663 }
3664
3665
3666 #endregion
3667
3668 #endregion // Expr
3669
3670 #region Options
3687 public Z3_ast_print_mode PrintMode
3688 {
3689 get { return m_print_mode; }
3690 set
3691 {
3692 Native.Z3_set_ast_print_mode(nCtx, (uint)value);
3693 m_print_mode = value;
3694 }
3695 }
3696 #endregion
3697
3698 #region SMT Files & Strings
3699
3704 public BoolExpr[] ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
3705 {
3706
3707 uint csn = Symbol.ArrayLength(sortNames);
3708 uint cs = Sort.ArrayLength(sorts);
3709 uint cdn = Symbol.ArrayLength(declNames);
3710 uint cd = AST.ArrayLength(decls);
3711 if (csn != cs || cdn != cd)
3712 throw new Z3Exception("Argument size mismatch");
3713 using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str,
3714 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3715 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3716 return assertions.ToBoolExprArray();
3717 }
3718
3723 public BoolExpr[] ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
3724 {
3725
3726 uint csn = Symbol.ArrayLength(sortNames);
3727 uint cs = Sort.ArrayLength(sorts);
3728 uint cdn = Symbol.ArrayLength(declNames);
3729 uint cd = AST.ArrayLength(decls);
3730 if (csn != cs || cdn != cd)
3731 throw new Z3Exception("Argument size mismatch");
3732 using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
3733 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3734 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3735 return assertions.ToBoolExprArray();
3736 }
3737
3748 public string BenchmarkToSmtlibString(string name, string logic, string status, string attributes, BoolExpr[] assumptions, BoolExpr formula)
3749 {
3750 Debug.Assert(assumptions != null);
3751 Debug.Assert(formula != null);
3752
3753 return Native.Z3_benchmark_to_smtlib_string(
3754 nCtx,
3755 name,
3756 logic,
3757 status,
3758 attributes,
3759 (uint)(assumptions?.Length ?? 0),
3760 AST.ArrayToNative(assumptions),
3761 formula.NativeObject);
3762 }
3763 #endregion
3764
3765 #region Goals
3776 public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
3777 {
3778
3779 return new Goal(this, models, unsatCores, proofs);
3780 }
3781 #endregion
3782
3783 #region ParameterSets
3787 public Params MkParams()
3788 {
3789
3790 return new Params(this);
3791 }
3792 #endregion
3793
3794 #region Tactics
3798 public uint NumTactics
3799 {
3800 get { return Native.Z3_get_num_tactics(nCtx); }
3801 }
3802
3806 public string[] TacticNames
3807 {
3808 get
3809 {
3810
3811 uint n = NumTactics;
3812 string[] res = new string[n];
3813 for (uint i = 0; i < n; i++)
3814 res[i] = Native.Z3_get_tactic_name(nCtx, i);
3815 return res;
3816 }
3817 }
3818
3822 public string TacticDescription(string name)
3823 {
3824
3825 return Native.Z3_tactic_get_descr(nCtx, name);
3826 }
3827
3831 public Tactic MkTactic(string name)
3832 {
3833
3834 return new Tactic(this, name);
3835 }
3836
3841 public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
3842 {
3843 Debug.Assert(t1 != null);
3844 Debug.Assert(t2 != null);
3845 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3846
3847
3848 CheckContextMatch(t1);
3849 CheckContextMatch(t2);
3850 CheckContextMatch<Tactic>(ts);
3851
3852 IntPtr last = IntPtr.Zero;
3853 if (ts != null && ts.Length > 0)
3854 {
3855 last = ts[ts.Length - 1].NativeObject;
3856 for (int i = ts.Length - 2; i >= 0; i--)
3857 last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3858 }
3859 if (last != IntPtr.Zero)
3860 {
3861 last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3862 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3863 }
3864 else
3865 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3866 }
3867
3875 public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
3876 {
3877 Debug.Assert(t1 != null);
3878 Debug.Assert(t2 != null);
3879 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3880
3881 return AndThen(t1, t2, ts);
3882 }
3883
3888 public Tactic OrElse(Tactic t1, Tactic t2)
3889 {
3890 Debug.Assert(t1 != null);
3891 Debug.Assert(t2 != null);
3892
3893 CheckContextMatch(t1);
3894 CheckContextMatch(t2);
3895 return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3896 }
3897
3904 public Tactic TryFor(Tactic t, uint ms)
3905 {
3906 Debug.Assert(t != null);
3907
3908 CheckContextMatch(t);
3909 return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3910 }
3911
3919 public Tactic When(Probe p, Tactic t)
3920 {
3921 Debug.Assert(p != null);
3922 Debug.Assert(t != null);
3923
3924 CheckContextMatch(t);
3925 CheckContextMatch(p);
3926 return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3927 }
3928
3933 public Tactic Cond(Probe p, Tactic t1, Tactic t2)
3934 {
3935 Debug.Assert(p != null);
3936 Debug.Assert(t1 != null);
3937 Debug.Assert(t2 != null);
3938
3939 CheckContextMatch(p);
3940 CheckContextMatch(t1);
3941 CheckContextMatch(t2);
3942 return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3943 }
3944
3949 public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
3950 {
3951 Debug.Assert(t != null);
3952
3953 CheckContextMatch(t);
3954 return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3955 }
3956
3960 public Tactic Skip()
3961 {
3962
3963 return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3964 }
3965
3969 public Tactic Fail()
3970 {
3971
3972 return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3973 }
3974
3978 public Tactic FailIf(Probe p)
3979 {
3980 Debug.Assert(p != null);
3981
3982 CheckContextMatch(p);
3983 return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3984 }
3985
3990 public Tactic FailIfNotDecided()
3991 {
3992
3993 return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3994 }
3995
3999 public Tactic UsingParams(Tactic t, Params p)
4000 {
4001 Debug.Assert(t != null);
4002 Debug.Assert(p != null);
4003
4004 CheckContextMatch(t);
4005 CheckContextMatch(p);
4006 return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
4007 }
4008
4013 public Tactic With(Tactic t, Params p)
4014 {
4015 Debug.Assert(t != null);
4016 Debug.Assert(p != null);
4017
4018 return UsingParams(t, p);
4019 }
4020
4024 public Tactic ParOr(params Tactic[] t)
4025 {
4026 Debug.Assert(t == null || t.All(tactic => tactic != null));
4027
4028 CheckContextMatch<Tactic>(t);
4029 return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
4030 }
4031
4036 public Tactic ParAndThen(Tactic t1, Tactic t2)
4037 {
4038 Debug.Assert(t1 != null);
4039 Debug.Assert(t2 != null);
4040
4041 CheckContextMatch(t1);
4042 CheckContextMatch(t2);
4043 return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
4044 }
4045
4050 public void Interrupt()
4051 {
4052 Native.Z3_interrupt(nCtx);
4053 }
4054 #endregion
4055
4056 #region Quantifier Elimination
4060 public ASTMap MkASTMap()
4061 {
4062 return new ASTMap(this);
4063 }
4064
4068 public Expr QeLite(ASTVector vars, Expr body)
4069 {
4070 CheckContextMatch(vars);
4071 CheckContextMatch(body);
4072 return Expr.Create(this, Native.Z3_qe_lite(nCtx, vars.NativeObject, body.NativeObject));
4073 }
4074
4078 public Expr QeModelProject(Model model, Expr[] bounds, Expr body)
4079 {
4080 CheckContextMatch(model);
4081 CheckContextMatch<Expr>(bounds);
4082 CheckContextMatch(body);
4083 return Expr.Create(this, Native.Z3_qe_model_project(nCtx, model.NativeObject,
4084 (uint)bounds.Length, AST.ArrayToNative(bounds), body.NativeObject));
4085 }
4086
4090 public Expr QeModelProjectSkolem(Model model, Expr[] bounds, Expr body, ASTMap map)
4091 {
4092 CheckContextMatch(model);
4093 CheckContextMatch<Expr>(bounds);
4094 CheckContextMatch(body);
4095 CheckContextMatch(map);
4096 return Expr.Create(this, Native.Z3_qe_model_project_skolem(nCtx, model.NativeObject,
4097 (uint)bounds.Length, AST.ArrayToNative(bounds), body.NativeObject, map.NativeObject));
4098 }
4099
4103 public Expr QeModelProjectWithWitness(Model model, Expr[] bounds, Expr body, ASTMap map)
4104 {
4105 CheckContextMatch(model);
4106 CheckContextMatch<Expr>(bounds);
4107 CheckContextMatch(body);
4108 CheckContextMatch(map);
4109 return Expr.Create(this, Native.Z3_qe_model_project_with_witness(nCtx, model.NativeObject,
4110 (uint)bounds.Length, AST.ArrayToNative(bounds), body.NativeObject, map.NativeObject));
4111 }
4112 #endregion
4113
4114 #region Simplifiers
4118 public uint NumSimplifiers
4119 {
4120 get { return Native.Z3_get_num_simplifiers(nCtx); }
4121 }
4122
4126 public string[] SimplifierNames
4127 {
4128 get
4129 {
4130
4131 uint n = NumSimplifiers;
4132 string[] res = new string[n];
4133 for (uint i = 0; i < n; i++)
4134 res[i] = Native.Z3_get_simplifier_name(nCtx, i);
4135 return res;
4136 }
4137 }
4138
4142 public string SimplifierDescription(string name)
4143 {
4144
4145 return Native.Z3_simplifier_get_descr(nCtx, name);
4146 }
4147
4151 public Simplifier MkSimplifier(string name)
4152 {
4153
4154 return new Simplifier(this, name);
4155 }
4156
4161 public Simplifier AndThen(Simplifier t1, Simplifier t2, params Simplifier[] ts)
4162 {
4163 Debug.Assert(t1 != null);
4164 Debug.Assert(t2 != null);
4165 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
4166
4167
4168 CheckContextMatch(t1);
4169 CheckContextMatch(t2);
4170 CheckContextMatch<Simplifier>(ts);
4171
4172 IntPtr last = IntPtr.Zero;
4173 if (ts != null && ts.Length > 0)
4174 {
4175 last = ts[ts.Length - 1].NativeObject;
4176 for (int i = ts.Length - 2; i >= 0; i--)
4177 last = Native.Z3_simplifier_and_then(nCtx, ts[i].NativeObject, last);
4178 }
4179 if (last != IntPtr.Zero)
4180 {
4181 last = Native.Z3_simplifier_and_then(nCtx, t2.NativeObject, last);
4182 return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, last));
4183 }
4184 else
4185 return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, t2.NativeObject));
4186 }
4187
4195 public Simplifier Then(Simplifier t1, Simplifier t2, params Simplifier[] ts)
4196 {
4197 Debug.Assert(t1 != null);
4198 Debug.Assert(t2 != null);
4199 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
4200
4201 return AndThen(t1, t2, ts);
4202 }
4203
4207 public Simplifier UsingParams(Simplifier t, Params p)
4208 {
4209 Debug.Assert(t != null);
4210 Debug.Assert(p != null);
4211
4212 CheckContextMatch(t);
4213 CheckContextMatch(p);
4214 return new Simplifier(this, Native.Z3_simplifier_using_params(nCtx, t.NativeObject, p.NativeObject));
4215 }
4216 #endregion
4217
4218 #region Probes
4222 public uint NumProbes
4223 {
4224 get { return Native.Z3_get_num_probes(nCtx); }
4225 }
4226
4230 public string[] ProbeNames
4231 {
4232 get
4233 {
4234
4235 uint n = NumProbes;
4236 string[] res = new string[n];
4237 for (uint i = 0; i < n; i++)
4238 res[i] = Native.Z3_get_probe_name(nCtx, i);
4239 return res;
4240 }
4241 }
4242
4246 public string ProbeDescription(string name)
4247 {
4248
4249 return Native.Z3_probe_get_descr(nCtx, name);
4250 }
4251
4255 public Probe MkProbe(string name)
4256 {
4257
4258 return new Probe(this, name);
4259 }
4260
4264 public Probe ConstProbe(double val)
4265 {
4266
4267 return new Probe(this, Native.Z3_probe_const(nCtx, val));
4268 }
4269
4274 public Probe Lt(Probe p1, Probe p2)
4275 {
4276 Debug.Assert(p1 != null);
4277 Debug.Assert(p2 != null);
4278
4279 CheckContextMatch(p1);
4280 CheckContextMatch(p2);
4281 return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
4282 }
4283
4288 public Probe Gt(Probe p1, Probe p2)
4289 {
4290 Debug.Assert(p1 != null);
4291 Debug.Assert(p2 != null);
4292
4293 CheckContextMatch(p1);
4294 CheckContextMatch(p2);
4295 return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
4296 }
4297
4302 public Probe Le(Probe p1, Probe p2)
4303 {
4304 Debug.Assert(p1 != null);
4305 Debug.Assert(p2 != null);
4306
4307 CheckContextMatch(p1);
4308 CheckContextMatch(p2);
4309 return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
4310 }
4311
4316 public Probe Ge(Probe p1, Probe p2)
4317 {
4318 Debug.Assert(p1 != null);
4319 Debug.Assert(p2 != null);
4320
4321 CheckContextMatch(p1);
4322 CheckContextMatch(p2);
4323 return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
4324 }
4325
4330 public Probe Eq(Probe p1, Probe p2)
4331 {
4332 Debug.Assert(p1 != null);
4333 Debug.Assert(p2 != null);
4334
4335 CheckContextMatch(p1);
4336 CheckContextMatch(p2);
4337 return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
4338 }
4339
4344 public Probe And(Probe p1, Probe p2)
4345 {
4346 Debug.Assert(p1 != null);
4347 Debug.Assert(p2 != null);
4348
4349 CheckContextMatch(p1);
4350 CheckContextMatch(p2);
4351 return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
4352 }
4353
4358 public Probe Or(Probe p1, Probe p2)
4359 {
4360 Debug.Assert(p1 != null);
4361 Debug.Assert(p2 != null);
4362
4363 CheckContextMatch(p1);
4364 CheckContextMatch(p2);
4365 return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
4366 }
4367
4372 public Probe Not(Probe p)
4373 {
4374 Debug.Assert(p != null);
4375
4376 CheckContextMatch(p);
4377 return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
4378 }
4379 #endregion
4380
4381 #region Solvers
4390 public Solver MkSolver(Symbol logic = null)
4391 {
4392
4393 if (logic == null)
4394 return new Solver(this, Native.Z3_mk_solver(nCtx));
4395 else
4396 return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
4397 }
4398
4403 public Solver MkSolver(string logic)
4404 {
4405 using var symbol = MkSymbol(logic);
4406 return MkSolver(symbol);
4407 }
4408
4412 public Solver MkSimpleSolver()
4413 {
4414
4415 return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
4416 }
4417
4421 public Solver MkSolver(Solver s, Simplifier t)
4422 {
4423 Debug.Assert(t != null);
4424 Debug.Assert(s != null);
4425 return new Solver(this, Native.Z3_solver_add_simplifier(nCtx, s.NativeObject, t.NativeObject));
4426 }
4427
4435 public Solver MkSolver(Tactic t)
4436 {
4437 Debug.Assert(t != null);
4438
4439 return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
4440 }
4441
4442
4443 #endregion
4444
4445 #region Fixedpoints
4449 public Fixedpoint MkFixedpoint()
4450 {
4451
4452 return new Fixedpoint(this);
4453 }
4454 #endregion
4455
4456 #region Optimization
4460 public Optimize MkOptimize()
4461 {
4462
4463 return new Optimize(this);
4464 }
4465 #endregion
4466
4467 #region Floating-Point Arithmetic
4468
4469 #region Rounding Modes
4470 #region RoundingMode Sort
4474 public FPRMSort MkFPRoundingModeSort()
4475 {
4476 return new FPRMSort(this);
4477 }
4478 #endregion
4479
4480 #region Numerals
4484 public FPRMExpr MkFPRoundNearestTiesToEven()
4485 {
4486 return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
4487 }
4488
4492 public FPRMNum MkFPRNE()
4493 {
4494 return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
4495 }
4496
4500 public FPRMNum MkFPRoundNearestTiesToAway()
4501 {
4502 return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
4503 }
4504
4508 public FPRMNum MkFPRNA()
4509 {
4510 return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
4511 }
4512
4516 public FPRMNum MkFPRoundTowardPositive()
4517 {
4518 return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
4519 }
4520
4524 public FPRMNum MkFPRTP()
4525 {
4526 return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
4527 }
4528
4532 public FPRMNum MkFPRoundTowardNegative()
4533 {
4534 return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
4535 }
4536
4540 public FPRMNum MkFPRTN()
4541 {
4542 return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
4543 }
4544
4548 public FPRMNum MkFPRoundTowardZero()
4549 {
4550 return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
4551 }
4552
4556 public FPRMNum MkFPRTZ()
4557 {
4558 return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
4559 }
4560 #endregion
4561 #endregion
4562
4563 #region FloatingPoint Sorts
4569 public FPSort MkFPSort(uint ebits, uint sbits)
4570 {
4571 return new FPSort(this, ebits, sbits);
4572 }
4573
4577 public FPSort MkFPSortHalf()
4578 {
4579 return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
4580 }
4581
4585 public FPSort MkFPSort16()
4586 {
4587 return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
4588 }
4589
4593 public FPSort MkFPSortSingle()
4594 {
4595 return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
4596 }
4597
4601 public FPSort MkFPSort32()
4602 {
4603 return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx));
4604 }
4605
4609 public FPSort MkFPSortDouble()
4610 {
4611 return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
4612 }
4613
4617 public FPSort MkFPSort64()
4618 {
4619 return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
4620 }
4621
4625 public FPSort MkFPSortQuadruple()
4626 {
4627 return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
4628 }
4629
4633 public FPSort MkFPSort128()
4634 {
4635 return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
4636 }
4637 #endregion
4638
4639 #region Numerals
4644 public FPNum MkFPNaN(FPSort s)
4645 {
4646 return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
4647 }
4648
4654 public FPNum MkFPInf(FPSort s, bool negative)
4655 {
4656 return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
4657 }
4658
4664 public FPNum MkFPZero(FPSort s, bool negative)
4665 {
4666 return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
4667 }
4668
4674 public FPNum MkFPNumeral(float v, FPSort s)
4675 {
4676 return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
4677 }
4678
4684 public FPNum MkFPNumeral(double v, FPSort s)
4685 {
4686 return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
4687 }
4688
4694 public FPNum MkFPNumeral(int v, FPSort s)
4695 {
4696 return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
4697 }
4698
4706 public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
4707 {
4708 return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
4709 }
4710
4718 public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
4719 {
4720 return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
4721 }
4722
4728 public FPNum MkFP(float v, FPSort s)
4729 {
4730 return MkFPNumeral(v, s);
4731 }
4732
4738 public FPNum MkFP(double v, FPSort s)
4739 {
4740 return MkFPNumeral(v, s);
4741 }
4742
4748 public FPNum MkFP(int v, FPSort s)
4749 {
4750 return MkFPNumeral(v, s);
4751 }
4752
4760 public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
4761 {
4762 return MkFPNumeral(sgn, exp, sig, s);
4763 }
4764
4772 public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
4773 {
4774 return MkFPNumeral(sgn, exp, sig, s);
4775 }
4776
4777 #endregion
4778
4779 #region Operators
4784 public FPExpr MkFPAbs(FPExpr t)
4785 {
4786 return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
4787 }
4788
4793 public FPExpr MkFPNeg(FPExpr t)
4794 {
4795 return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
4796 }
4797
4804 public FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
4805 {
4806 return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4807 }
4808
4815 public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
4816 {
4817 return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4818 }
4819
4826 public FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
4827 {
4828 return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4829 }
4830
4837 public FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
4838 {
4839 return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4840 }
4841
4852 public FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
4853 {
4854 return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
4855 }
4856
4862 public FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
4863 {
4864 return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
4865 }
4866
4872 public FPExpr MkFPRem(FPExpr t1, FPExpr t2)
4873 {
4874 return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
4875 }
4876
4883 public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
4884 {
4885 return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
4886 }
4887
4893 public FPExpr MkFPMin(FPExpr t1, FPExpr t2)
4894 {
4895 return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
4896 }
4897
4903 public FPExpr MkFPMax(FPExpr t1, FPExpr t2)
4904 {
4905 return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
4906 }
4907
4913 public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
4914 {
4915 return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
4916 }
4917
4923 public BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
4924 {
4925 return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
4926 }
4927
4933 public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
4934 {
4935 return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
4936 }
4937
4943 public BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
4944 {
4945 return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
4946 }
4947
4956 public BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
4957 {
4958 return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
4959 }
4960
4965 public BoolExpr MkFPIsNormal(FPExpr t)
4966 {
4967 return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
4968 }
4969
4974 public BoolExpr MkFPIsSubnormal(FPExpr t)
4975 {
4976 return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
4977 }
4978
4983 public BoolExpr MkFPIsZero(FPExpr t)
4984 {
4985 return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
4986 }
4987
4992 public BoolExpr MkFPIsInfinite(FPExpr t)
4993 {
4994 return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
4995 }
4996
5001 public BoolExpr MkFPIsNaN(FPExpr t)
5002 {
5003 return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
5004 }
5005
5010 public BoolExpr MkFPIsNegative(FPExpr t)
5011 {
5012 return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
5013 }
5014
5019 public BoolExpr MkFPIsPositive(FPExpr t)
5020 {
5021 return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
5022 }
5023 #endregion
5024
5025 #region Conversions to FloatingPoint terms
5039 public FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
5040 {
5041 return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
5042 }
5043
5055 public FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
5056 {
5057 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
5058 }
5059
5071 public FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
5072 {
5073 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
5074 }
5075
5087 public FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
5088 {
5089 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
5090 }
5091
5105 public FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
5106 {
5107 if (signed)
5108 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
5109 else
5110 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
5111 }
5112
5123 public FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
5124 {
5125 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
5126 }
5127 #endregion
5128
5129 #region Conversions from FloatingPoint terms
5142 public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool sign)
5143 {
5144 if (sign)
5145 return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
5146 else
5147 return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
5148 }
5149
5159 public RealExpr MkFPToReal(FPExpr t)
5160 {
5161 return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
5162 }
5163 #endregion
5164
5165 #region Z3-specific extensions
5176 public BitVecExpr MkFPToIEEEBV(FPExpr t)
5177 {
5178 return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
5179 }
5180
5193 public BitVecExpr MkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
5194 {
5195 return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
5196 }
5197 #endregion
5198 #endregion // Floating-point Arithmetic
5199
5200 #region Miscellaneous
5211 public AST WrapAST(IntPtr nativeObject)
5212 {
5213 return AST.Create(this, nativeObject);
5214 }
5215
5227 public IntPtr UnwrapAST(AST a)
5228 {
5229 return a.NativeObject;
5230 }
5231
5237 public FuncDecl MkPartialOrder(Sort a, uint index)
5238 {
5239 return new FuncDecl(this, Native.Z3_mk_partial_order(this.nCtx, a.NativeObject, index));
5240 }
5241
5247 public FuncDecl MkTransitiveClosure(FuncDecl f)
5248 {
5249 return new FuncDecl(this, Native.Z3_mk_transitive_closure(this.nCtx, f.NativeObject));
5250 }
5251
5262 public ASTVector PolynomialSubresultants(Expr p, Expr q, Expr x)
5263 {
5264 CheckContextMatch(p);
5265 CheckContextMatch(q);
5266 CheckContextMatch(x);
5267 return new ASTVector(this, Native.Z3_polynomial_subresultants(this.nCtx, p.NativeObject, q.NativeObject, x.NativeObject));
5268 }
5269
5273 public string SimplifyHelp()
5274 {
5275
5276 return Native.Z3_simplify_get_help(nCtx);
5277 }
5278
5282 public ParamDescrs SimplifyParameterDescriptions
5283 {
5284 get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
5285 }
5286 #endregion
5287
5288 #region Error Handling
5296 //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
5297
5301 //public event ErrorHandler OnError = null;
5302 #endregion
5303
5304 #region Parameters
5314 public void UpdateParamValue(string id, string value)
5315 {
5316 Native.Z3_update_param_value(nCtx, id, value);
5317 }
5318
5319 #endregion
5320
5321 #region Internal
5322 internal IntPtr m_ctx = IntPtr.Zero;
5323 internal Native.Z3_error_handler m_n_err_handler = null;
5324 internal static Object creation_lock = new Object();
5325 internal IntPtr nCtx { get { return m_ctx; } }
5326 private Z3_ast_print_mode m_print_mode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
5327
5328 // Estimated native memory used per context, for GC memory pressure hints.
5329 // The value is a conservative lower bound; actual usage may exceed this.
5330 private const long NativeMemoryPressureEstimate = 8 * 1024 * 1024; // 8 MB
5331 private bool m_memPressureAdded = false;
5332
5333 internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
5334 {
5335 // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
5336 }
5337
5338 internal void InitContext()
5339 {
5340 PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
5341 m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
5342 Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
5343 if (!is_external)
5344 {
5345 GC.AddMemoryPressure(NativeMemoryPressureEstimate);
5346 m_memPressureAdded = true;
5347 }
5348 }
5349
5350 internal void CheckContextMatch(Z3Object other)
5351 {
5352 Debug.Assert(other != null);
5353
5354 if (!ReferenceEquals(this, other.Context))
5355 throw new Z3Exception("Context mismatch");
5356 }
5357
5358 internal void CheckContextMatch(Z3Object other1, Z3Object other2)
5359 {
5360 Debug.Assert(other1 != null);
5361 Debug.Assert(other2 != null);
5362 CheckContextMatch(other1);
5363 CheckContextMatch(other2);
5364 }
5365
5366 internal void CheckContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
5367 {
5368 Debug.Assert(other1 != null);
5369 Debug.Assert(other2 != null);
5370 Debug.Assert(other3 != null);
5371 CheckContextMatch(other1);
5372 CheckContextMatch(other2);
5373 CheckContextMatch(other3);
5374 }
5375
5376 internal void CheckContextMatch(Z3Object[] arr)
5377 {
5378 Debug.Assert(arr == null || arr.All(a => a != null));
5379
5380 if (arr != null)
5381 {
5382 foreach (Z3Object a in arr)
5383 {
5384 Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
5385 CheckContextMatch(a);
5386 }
5387 }
5388 }
5389
5390 internal void CheckContextMatch<T>(IEnumerable<T> arr) where T : Z3Object
5391 {
5392 Debug.Assert(arr == null || arr.All(a => a != null));
5393
5394 if (arr != null)
5395 {
5396 foreach (Z3Object a in arr)
5397 {
5398 Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
5399 CheckContextMatch(a);
5400 }
5401 }
5402 }
5403
5404 private void ObjectInvariant()
5405 {
5406 // none
5407 }
5408
5412 ~Context()
5413 {
5414 // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
5415 Dispose();
5416 }
5417
5421 public void Dispose()
5422 {
5423 // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
5424
5425 if (m_boolSort != null) m_boolSort.Dispose();
5426 if (m_intSort != null) m_intSort.Dispose();
5427 if (m_realSort != null) m_realSort.Dispose();
5428 if (m_stringSort != null) m_stringSort.Dispose();
5429 if (m_charSort != null) m_charSort.Dispose();
5430 m_boolSort = null;
5431 m_intSort = null;
5432 m_realSort = null;
5433 m_stringSort = null;
5434 m_charSort = null;
5435 if (m_ctx != IntPtr.Zero)
5436 {
5437 // Suppress the finalizer before performing cleanup so that it cannot
5438 // run concurrently or redundantly if cleanup raises an exception.
5439 GC.SuppressFinalize(this);
5440 IntPtr ctx;
5441 // Keep a local reference to the error handler delegate to ensure it stays
5442 // alive throughout Z3_del_context. Setting m_n_err_handler = null releases
5443 // the field reference; without the local variable the GC could collect the
5444 // delegate before the native destructor finishes using the handler.
5445 Native.Z3_error_handler errHandler;
5446 lock (this)
5447 {
5448 ctx = m_ctx;
5449 errHandler = m_n_err_handler;
5450 m_n_err_handler = null;
5451 m_ctx = IntPtr.Zero;
5452 }
5453 // ctx is non-zero only for the thread that wins the lock and zeros m_ctx,
5454 // preventing double-free when Dispose() is called concurrently.
5455 if (ctx != IntPtr.Zero)
5456 {
5457 if (!is_external)
5458 {
5459 Native.Z3_del_context(ctx);
5460 GC.KeepAlive(errHandler);
5461 }
5462 if (m_memPressureAdded)
5463 {
5464 GC.RemoveMemoryPressure(NativeMemoryPressureEstimate);
5465 m_memPressureAdded = false;
5466 }
5467 }
5468 }
5469 }
5470
5471
5472 #endregion
5473 }
5474}
Microsoft.Z3.AST
The abstract syntax tree (AST) class.
Definition AST.cs:31
Microsoft.Z3.ASTMap
Map from AST to AST.
Definition ASTMap.cs:29
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:5087
Microsoft.Z3.Context.MkBVNAND
BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
Bitwise NAND.
Definition Context.cs:1459
Microsoft.Z3.Context.MkFP
FPNum MkFP(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition Context.cs:4728
Microsoft.Z3.Context.MkInt2Real
RealExpr MkInt2Real(IntExpr t)
Coerce an integer to a real.
Definition Context.cs:1341
Microsoft.Z3.Context.MkFPSort16
FPSort MkFPSort16()
Create the half-precision (16-bit) FloatingPoint sort.
Definition Context.cs:4585
Microsoft.Z3.Context.MkAdd
ArithExpr MkAdd(IEnumerable< ArithExpr > ts)
Create an expression representing t[0] + t[1] + ....
Definition Context.cs:1175
Microsoft.Z3.Context.MkCharLe
BoolExpr MkCharLe(Expr ch1, Expr ch2)
Create less than or equal to between two characters.
Definition Context.cs:3089
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:3241
Microsoft.Z3.Context.MkArrayConst
ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
Create an array constant.
Definition Context.cs:2177
Microsoft.Z3.Context.MkAtLeast
BoolExpr MkAtLeast(IEnumerable< BoolExpr > args, uint k)
Create an at-least-k constraint.
Definition Context.cs:3151
Microsoft.Z3.Context.MkBVSHL
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
Shift left.
Definition Context.cs:1872
Microsoft.Z3.Context.MkFiniteSetMap
Expr MkFiniteSetMap(Expr f, Expr set)
Map a function over all elements in a finite set.
Definition Context.cs:2638
Microsoft.Z3.Context.Skip
Tactic Skip()
Create a tactic that just returns the given goal.
Definition Context.cs:3960
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:4195
Microsoft.Z3.Context.MkPolymorphicDatatypeSort
DatatypeSort MkPolymorphicDatatypeSort(Symbol name, Sort[] typeParams, Constructor[] constructors)
Create a polymorphic datatype sort with explicit type parameters. Type parameters should be sorts cre...
Definition Context.cs:593
Microsoft.Z3.Context.BoolSort
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition Context.cs:147
Microsoft.Z3.Context.MkFiniteSetUnion
Expr MkFiniteSetUnion(Expr s1, Expr s2)
Create the union of two finite sets.
Definition Context.cs:2562
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(bool[] bits)
Create a bit-vector numeral.
Definition Context.cs:3468
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:2826
Microsoft.Z3.Context.MkFPSort
FPSort MkFPSort(uint ebits, uint sbits)
Create a FloatingPoint sort.
Definition Context.cs:4569
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:4013
Microsoft.Z3.Context.TacticNames
string[] TacticNames
The names of all supported tactics.
Definition Context.cs:3807
Microsoft.Z3.Context.MkIsDigit
BoolExpr MkIsDigit(Expr ch)
Create a check if the character is a digit.
Definition Context.cs:3126
Microsoft.Z3.Context.MkAdd
ArithExpr MkAdd(params ArithExpr[] ts)
Create an expression representing t[0] + t[1] + ....
Definition Context.cs:1163
Microsoft.Z3.Context.MkFPAdd
FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point addition.
Definition Context.cs:4804
Microsoft.Z3.Context.MkBVRotateLeft
BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Rotate Left.
Definition Context.cs:1965
Microsoft.Z3.Context.MkRealConst
RealExpr MkRealConst(string name)
Creates a real constant.
Definition Context.cs:922
Microsoft.Z3.Context.MkReal
RatNum MkReal(uint v)
Create a real numeral.
Definition Context.cs:3323
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:4288
Microsoft.Z3.Context.MkBVLSHR
BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Logical shift right.
Definition Context.cs:1894
Microsoft.Z3.Context.MkFPRoundingModeSort
FPRMSort MkFPRoundingModeSort()
Create the floating-point RoundingMode sort.
Definition Context.cs:4474
Microsoft.Z3.Context.MkFPToReal
RealExpr MkFPToReal(FPExpr t)
Conversion of a floating-point term into a real-numbered term.
Definition Context.cs:5159
Microsoft.Z3.Context.MkFiniteSetSort
FiniteSetSort MkFiniteSetSort(Sort elemSort)
Create a finite set sort over the given element sort.
Definition Context.cs:2507
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:3658
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:2149
Microsoft.Z3.Context.MkFiniteSetSingleton
Expr MkFiniteSetSingleton(Expr elem)
Create a singleton finite set.
Definition Context.cs:2551
Microsoft.Z3.Context.MkDiff
ReExpr MkDiff(ReExpr a, ReExpr b)
Create a difference regular expression.
Definition Context.cs:3046
Microsoft.Z3.Context.MkFullSet
ArrayExpr MkFullSet(Sort domain)
Create the full set.
Definition Context.cs:2391
Microsoft.Z3.Context.MkFPSortQuadruple
FPSort MkFPSortQuadruple()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition Context.cs:4625
Microsoft.Z3.Context.MkLe
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
Definition Context.cs:1295
Microsoft.Z3.Context.ConstProbe
Probe ConstProbe(double val)
Create a probe that always evaluates to val .
Definition Context.cs:4264
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:851
Microsoft.Z3.Context.MkOr
BoolExpr MkOr(params BoolExpr[] ts)
Create an expression representing t[0] or t[1] or ....
Definition Context.cs:1138
Microsoft.Z3.Context.MkReal2Int
IntExpr MkReal2Int(RealExpr t)
Coerce a real to an integer.
Definition Context.cs:1356
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:4577
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:3529
Microsoft.Z3.Context.MkSetDifference
ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Take the difference between two sets.
Definition Context.cs:2453
Microsoft.Z3.Context.MkXor
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition Context.cs:1087
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:3256
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:1046
Microsoft.Z3.Context.MkInt
IntNum MkInt(uint v)
Create an integer numeral.
Definition Context.cs:3379
Microsoft.Z3.Context.QeLite
Expr QeLite(ASTVector vars, Expr body)
Performs best-effort quantifier elimination for the variables in vars .
Definition Context.cs:4068
Microsoft.Z3.Context.MkIntConst
IntExpr MkIntConst(Symbol name)
Creates an integer constant.
Definition Context.cs:892
Microsoft.Z3.Context.WrapAST
AST WrapAST(IntPtr nativeObject)
Wraps an AST.
Definition Context.cs:5211
Microsoft.Z3.Context.MkPartialOrder
FuncDecl MkPartialOrder(Sort a, uint index)
Create a partial order relation over a sort.
Definition Context.cs:5237
Microsoft.Z3.Context.IntToString
SeqExpr IntToString(Expr e)
Convert an integer expression to a string.
Definition Context.cs:2708
Microsoft.Z3.Context.MkFPMax
FPExpr MkFPMax(FPExpr t1, FPExpr t2)
Maximum of floating-point numbers.
Definition Context.cs:4903
Microsoft.Z3.Context.MkUnaryMinus
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
Definition Context.cs:1217
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:5176
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:2793
Microsoft.Z3.Context.MkConcat
SeqExpr MkConcat(params SeqExpr[] t)
Concatenate sequences.
Definition Context.cs:2749
Microsoft.Z3.Context.MkFuncDecl
FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
Creates a new function declaration.
Definition Context.cs:716
Microsoft.Z3.Context.MkNot
BoolExpr MkNot(BoolExpr a)
Mk an expression representing not(a).
Definition Context.cs:1033
Microsoft.Z3.Context.MkFuncDecl
FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
Creates a new function declaration.
Definition Context.cs:673
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:784
Microsoft.Z3.Context.MkTermArray
Expr MkTermArray(ArrayExpr array)
Access the array default value.
Definition Context.cs:2342
Microsoft.Z3.Context.MkBVSRem
BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
Signed remainder.
Definition Context.cs:1621
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:4207
Microsoft.Z3.Context.MkBVRedOR
BitVecExpr MkBVRedOR(BitVecExpr t)
Take disjunction of bits in a vector, return vector of length 1.
Definition Context.cs:1405
Microsoft.Z3.Context.MkTactic
Tactic MkTactic(string name)
Creates a new Tactic.
Definition Context.cs:3831
Microsoft.Z3.Context.MkFPLEq
BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
Floating-point less than or equal.
Definition Context.cs:4913
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:3748
Microsoft.Z3.Context.MkFiniteSetEmpty
Expr MkFiniteSetEmpty(Sort setSort)
Create an empty finite set.
Definition Context.cs:2540
Microsoft.Z3.Context.MkOption
ReExpr MkOption(ReExpr re)
Create the optional regular expression.
Definition Context.cs:2992
Microsoft.Z3.Context.MkFPEq
BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
Floating-point equality.
Definition Context.cs:4956
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:2859
Microsoft.Z3.Context.MkReal
RatNum MkReal(string v)
Create a real numeral.
Definition Context.cs:3301
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:5071
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:5105
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:3999
Microsoft.Z3.Context.SimplifierNames
string[] SimplifierNames
The names of all supported tactics.
Definition Context.cs:4127
Microsoft.Z3.Context.MkBVNegNoOverflow
BoolExpr MkBVNegNoOverflow(BitVecExpr t)
Create a predicate that checks that the bit-wise negation does not overflow.
Definition Context.cs:2119
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:3799
Microsoft.Z3.Context.UbvToString
SeqExpr UbvToString(Expr e)
Convert a bit-vector expression, represented as an unsigned number, to a string.
Definition Context.cs:2718
Microsoft.Z3.Context.MkConcat
ReExpr MkConcat(params ReExpr[] t)
Create the concatenation of regular languages.
Definition Context.cs:3010
Microsoft.Z3.Context.MkBVULT
BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than.
Definition Context.cs:1654
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:2133
Microsoft.Z3.Context.MkConstDecl
FuncDecl MkConstDecl(Symbol name, Sort range)
Creates a new constant function declaration.
Definition Context.cs:746
Microsoft.Z3.Context.MkXor
BoolExpr MkXor(IEnumerable< BoolExpr > args)
Create an expression representing t1 xor t2 xor t3 ... .
Definition Context.cs:1100
Microsoft.Z3.Context.MkBVSDiv
BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Signed division.
Definition Context.cs:1583
Microsoft.Z3.Context.SimplifyParameterDescriptions
ParamDescrs SimplifyParameterDescriptions
Retrieves parameter descriptions for simplifier.
Definition Context.cs:5283
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(ulong v, uint size)
Create a bit-vector numeral.
Definition Context.cs:3458
Microsoft.Z3.Context.MkFPFMA
FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Floating-point fused multiply-add.
Definition Context.cs:4852
Microsoft.Z3.Context.MkFPIsInfinite
BoolExpr MkFPIsInfinite(FPExpr t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.
Definition Context.cs:4992
Microsoft.Z3.Context.MkInt2BV
BitVecExpr MkInt2BV(uint n, IntExpr t)
Create an n bit bit-vector from the integer argument t .
Definition Context.cs:2002
Microsoft.Z3.Context.MkTrue
BoolExpr MkTrue()
The true Term.
Definition Context.cs:975
Microsoft.Z3.Context.MkFPSub
FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point subtraction.
Definition Context.cs:4815
Microsoft.Z3.Context.MkFPNumeral
FPNum MkFPNumeral(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition Context.cs:4684
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:5055
Microsoft.Z3.Context.MkUnion
ReExpr MkUnion(params ReExpr[] t)
Create the union of regular languages.
Definition Context.cs:3022
Microsoft.Z3.Context.MkReal
RatNum MkReal(ulong v)
Create a real numeral.
Definition Context.cs:3345
Microsoft.Z3.Context.MkBoolConst
BoolExpr MkBoolConst(Symbol name)
Create a Boolean constant.
Definition Context.cs:873
Microsoft.Z3.Context.MkEmptyRe
ReExpr MkEmptyRe(Sort s)
Create the empty regular expression. The sort s should be a regular expression.
Definition Context.cs:3058
Microsoft.Z3.Context.MkTransitiveClosure
FuncDecl MkTransitiveClosure(FuncDecl f)
Create the transitive closure of a binary relation.
Definition Context.cs:5247
Microsoft.Z3.Context.MkNth
Expr MkNth(SeqExpr s, Expr index)
Retrieve element at index.
Definition Context.cs:2848
Microsoft.Z3.Context.MkSeqMap
Expr MkSeqMap(Expr f, SeqExpr s)
Map function f over the sequence s.
Definition Context.cs:2895
Microsoft.Z3.Context.MkFPSortSingle
FPSort MkFPSortSingle()
Create the single-precision (32-bit) FloatingPoint sort.
Definition Context.cs:4593
Microsoft.Z3.Context.UnwrapAST
IntPtr UnwrapAST(AST a)
Unwraps an AST.
Definition Context.cs:5227
Microsoft.Z3.Context.MkMod
IntExpr MkMod(IntExpr t1, IntExpr t2)
Create an expression representing t1 mod t2.
Definition Context.cs:1242
Microsoft.Z3.Context.MkPBLe
BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean less-or-equal constraint.
Definition Context.cs:3163
Microsoft.Z3.Context.MkInt
IntNum MkInt(string v)
Create an integer numeral.
Definition Context.cs:3357
Microsoft.Z3.Context.MkConst
Expr MkConst(FuncDecl f)
Creates a fresh constant from the FuncDecl f .
Definition Context.cs:863
Microsoft.Z3.Context.MkFPRTZ
FPRMNum MkFPRTZ()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Definition Context.cs:4556
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:3904
Microsoft.Z3.Context.MkImplies
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 -> t2.
Definition Context.cs:1074
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:2087
Microsoft.Z3.Context.MkSelect
Expr MkSelect(ArrayExpr a, Expr i)
Array read.
Definition Context.cs:2201
Microsoft.Z3.Context.MkSetUnion
ArrayExpr MkSetUnion(params ArrayExpr[] args)
Take the union of a list of sets.
Definition Context.cs:2429
Microsoft.Z3.Context.MkIndexOf
IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Extract index of sub-string starting at offset.
Definition Context.cs:2871
Microsoft.Z3.Context.MkFiniteSetDifference
Expr MkFiniteSetDifference(Expr s1, Expr s2)
Create the difference of two finite sets.
Definition Context.cs:2588
Microsoft.Z3.Context.MkBoolConst
BoolExpr MkBoolConst(string name)
Create a Boolean constant.
Definition Context.cs:883
Microsoft.Z3.Context.MkApp
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition Context.cs:953
Microsoft.Z3.Context.MkBVSMod
BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
Two's complement signed remainder (sign follows divisor).
Definition Context.cs:1638
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:4358
Microsoft.Z3.Context.MkRepeat
BitVecExpr MkRepeat(uint i, BitVecExpr t)
Bit-vector repetition.
Definition Context.cs:1852
Microsoft.Z3.Context.MkDistinct
BoolExpr MkDistinct(IEnumerable< Expr > args)
Creates a distinct term.
Definition Context.cs:1024
Microsoft.Z3.Context.MkFuncDecl
FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
Creates a new function declaration.
Definition Context.cs:657
Microsoft.Z3.Context.MkFPGt
BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
Floating-point greater than.
Definition Context.cs:4943
Microsoft.Z3.Context.MkAtMost
BoolExpr MkAtMost(IEnumerable< BoolExpr > args, uint k)
Create an at-most-k constraint.
Definition Context.cs:3139
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:4036
Microsoft.Z3.Context.MkSolver
Solver MkSolver(string logic)
Creates a new (incremental) solver.
Definition Context.cs:4403
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:3607
Microsoft.Z3.Context.MkSetDel
ArrayExpr MkSetDel(ArrayExpr set, Expr element)
Remove an element from a set.
Definition Context.cs:2416
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:628
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:4274
Microsoft.Z3.Context.MkRange
ReExpr MkRange(SeqExpr lo, SeqExpr hi)
Create a range expression.
Definition Context.cs:3078
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(long v, uint size)
Create a bit-vector numeral.
Definition Context.cs:3447
Microsoft.Z3.Context.QeModelProjectSkolem
Expr QeModelProjectSkolem(Model model, Expr[] bounds, Expr body, ASTMap map)
Projects bound applications and records Skolem terms in map .
Definition Context.cs:4090
Microsoft.Z3.Context.MkBVSGT
BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater-than.
Definition Context.cs:1766
Microsoft.Z3.Context.MkParams
Params MkParams()
Creates a new ParameterSet.
Definition Context.cs:3787
Microsoft.Z3.Context.MkSetIntersection
ArrayExpr MkSetIntersection(params ArrayExpr[] args)
Take the intersection of a list of sets.
Definition Context.cs:2441
Microsoft.Z3.Context.MkFPNaN
FPNum MkFPNaN(FPSort s)
Create a NaN of sort s.
Definition Context.cs:4644
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:4772
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:3704
Microsoft.Z3.Context.MkBVNOR
BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise NOR.
Definition Context.cs:1473
Microsoft.Z3.Context.CharToInt
IntExpr CharToInt(Expr ch)
Create an integer (code point) from character.
Definition Context.cs:3099
Microsoft.Z3.Context.MkDistinct
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
Definition Context.cs:1012
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:4883
Microsoft.Z3.Context.MkFixedpoint
Fixedpoint MkFixedpoint()
Create a Fixedpoint context.
Definition Context.cs:4449
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:2906
Microsoft.Z3.Context.UpdateParamValue
void UpdateParamValue(string id, string value)
Update a mutable configuration parameter.
Definition Context.cs:5314
Microsoft.Z3.Context.MkDatatypeSort
DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
Create a new datatype sort.
Definition Context.cs:452
Microsoft.Z3.Context.QeModelProjectWithWitness
Expr QeModelProjectWithWitness(Model model, Expr[] bounds, Expr body, ASTMap map)
Projects bound applications and records witnesses in map .
Definition Context.cs:4103
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:704
Microsoft.Z3.Context.MkFPNumeral
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition Context.cs:4674
Microsoft.Z3.Context.MkConstArray
ArrayExpr MkConstArray(Sort domain, Expr v)
Create a constant array.
Definition Context.cs:2304
Microsoft.Z3.Context.MkSetComplement
ArrayExpr MkSetComplement(ArrayExpr arg)
Take the complement of a set.
Definition Context.cs:2466
Microsoft.Z3.Context.MkASTMap
ASTMap MkASTMap()
Creates an empty map from ASTs to ASTs.
Definition Context.cs:4060
Microsoft.Z3.Context.MkSetSubset
BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Check for subsetness of sets.
Definition Context.cs:2490
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:4330
Microsoft.Z3.Context.MkFPRoundNearestTiesToAway
FPRMNum MkFPRoundNearestTiesToAway()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Definition Context.cs:4500
Microsoft.Z3.Context.ProbeNames
string[] ProbeNames
The names of all supported Probes.
Definition Context.cs:4231
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:3841
Microsoft.Z3.Context.MkZeroExt
BitVecExpr MkZeroExt(uint i, BitVecExpr t)
Bit-vector zero extension.
Definition Context.cs:1838
Microsoft.Z3.Context.PrintMode
Z3_ast_print_mode PrintMode
Selects the format used for pretty-printing expressions.
Definition Context.cs:3688
Microsoft.Z3.Context.Dispose
void Dispose()
Disposes of the context.
Definition Context.cs:5421
Microsoft.Z3.Context.CharToBV
BitVecExpr CharToBV(Expr ch)
Create a bit-vector (code point) from character.
Definition Context.cs:3108
Microsoft.Z3.Context.SbvToString
SeqExpr SbvToString(Expr e)
Convert a bit-vector expression, represented as an signed number, to a string.
Definition Context.cs:2728
Microsoft.Z3.Context.MkMul
ArithExpr MkMul(IEnumerable< ArithExpr > ts)
Create an expression representing t[0] * t[1] * ....
Definition Context.cs:1196
Microsoft.Z3.Context.MkEmptySet
ArrayExpr MkEmptySet(Sort domain)
Create an empty set.
Definition Context.cs:2380
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:3547
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:3271
Microsoft.Z3.Context.MkStar
ReExpr MkStar(ReExpr re)
Take the Kleene star of a regular expression.
Definition Context.cs:2965
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:942
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(uint v, uint size)
Create a bit-vector numeral.
Definition Context.cs:3436
Microsoft.Z3.Context.MkOptimize
Optimize MkOptimize()
Create an Optimization context.
Definition Context.cs:4460
Microsoft.Z3.Context.MkFiniteSetFilter
Expr MkFiniteSetFilter(Expr f, Expr set)
Filter a finite set with a predicate.
Definition Context.cs:2651
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:3584
Microsoft.Z3.Context.CharFromBV
Expr CharFromBV(BitVecExpr bv)
Create a character from a bit-vector (code point).
Definition Context.cs:3117
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:2353
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:4654
Microsoft.Z3.Context.MkConstDecl
FuncDecl MkConstDecl(string name, Sort range)
Creates a new constant function declaration.
Definition Context.cs:759
Microsoft.Z3.Context.MkMap
ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
Maps f on the argument arrays.
Definition Context.cs:2325
Microsoft.Z3.Context.MkIntersect
ReExpr MkIntersect(params ReExpr[] t)
Create the intersection of regular languages.
Definition Context.cs:3034
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:3949
Microsoft.Z3.Context.MkBVSLE
BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than or equal to.
Definition Context.cs:1702
Microsoft.Z3.Context.MkFP
FPNum MkFP(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition Context.cs:4748
Microsoft.Z3.Context.NumSimplifiers
uint NumSimplifiers
The number of supported simplifiers.
Definition Context.cs:4119
Microsoft.Z3.Context.MkLt
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
Definition Context.cs:1282
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:4760
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:2837
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:5123
Microsoft.Z3.Context.MkSetMembership
BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
Check for set membership.
Definition Context.cs:2477
Microsoft.Z3.Context.MkBVRotateRight
BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Rotate Right.
Definition Context.cs:1982
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:2883
Microsoft.Z3.Context.MkFPRoundNearestTiesToEven
FPRMExpr MkFPRoundNearestTiesToEven()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Definition Context.cs:4484
Microsoft.Z3.Context.ProbeDescription
string ProbeDescription(string name)
Returns a string containing a description of the probe with the given name.
Definition Context.cs:4246
Microsoft.Z3.Context.MkPattern
Pattern MkPattern(params Expr[] terms)
Create a quantifier pattern.
Definition Context.cs:810
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:4344
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:4302
Microsoft.Z3.Context.QeModelProject
Expr QeModelProject(Model model, Expr[] bounds, Expr body)
Projects the bound applications from body using model .
Definition Context.cs:4078
Microsoft.Z3.Context.MkFPNeg
FPExpr MkFPNeg(FPExpr t)
Floating-point negation.
Definition Context.cs:4793
Microsoft.Z3.Context.MkFPSort32
FPSort MkFPSort32()
Create the single-precision (32-bit) FloatingPoint sort.
Definition Context.cs:4601
Microsoft.Z3.Context.MkConst
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition Context.cs:825
Microsoft.Z3.Context.MkAnd
BoolExpr MkAnd(params BoolExpr[] ts)
Create an expression representing t[0] and t[1] and ....
Definition Context.cs:1117
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:1367
Microsoft.Z3.Context.MkBVXNOR
BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XNOR.
Definition Context.cs:1487
Microsoft.Z3.Context.MkBVULE
BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than or equal to.
Definition Context.cs:1686
Microsoft.Z3.Context.MkGe
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
Definition Context.cs:1321
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:5262
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:4718
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:5142
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:2055
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(string v, uint size)
Create a bit-vector numeral.
Definition Context.cs:3414
Microsoft.Z3.Context.MkFullRe
ReExpr MkFullRe(Sort s)
Create the full regular expression. The sort s should be a regular expression.
Definition Context.cs:3068
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:2918
Microsoft.Z3.Context.MkFPIsSubnormal
BoolExpr MkFPIsSubnormal(FPExpr t)
Predicate indicating whether t is a subnormal floating-point number.
Definition Context.cs:4974
Microsoft.Z3.Context.MkArrayConst
ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
Create an array constant.
Definition Context.cs:2164
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:4983
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:4609
Microsoft.Z3.Context.SimplifierDescription
string SimplifierDescription(string name)
Returns a string containing a description of the simplifier with the given name.
Definition Context.cs:4142
Microsoft.Z3.Context.MkFPRoundTowardZero
FPRMNum MkFPRoundTowardZero()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Definition Context.cs:4548
Microsoft.Z3.Context.MkSub
ArithExpr MkSub(params ArithExpr[] ts)
Create an expression representing t[0] - t[1] - ....
Definition Context.cs:1205
Microsoft.Z3.Context.MkGoal
Goal MkGoal(bool models=true, bool unsatCores=false, bool proofs=false)
Creates a new Goal.
Definition Context.cs:3776
Microsoft.Z3.Context.MkBV2Int
IntExpr MkBV2Int(BitVecExpr t, bool signed)
Create an integer from the bit-vector argument t .
Definition Context.cs:2025
Microsoft.Z3.Context.MkInRe
BoolExpr MkInRe(SeqExpr s, ReExpr re)
Check for regular expression membership.
Definition Context.cs:2954
Microsoft.Z3.Context.MkSetAdd
ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
Add an element to the set.
Definition Context.cs:2402
Microsoft.Z3.Context.MkBVRedAND
BitVecExpr MkBVRedAND(BitVecExpr t)
Take conjunction of bits in a vector, return vector of length 1.
Definition Context.cs:1393
Microsoft.Z3.Context.MkSeqPower
SeqExpr MkSeqPower(SeqExpr s, Expr n)
Retrieve the sequence s concatenated n times with itself.
Definition Context.cs:2771
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:4316
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:2974
Microsoft.Z3.Context.MkFPRoundTowardNegative
FPRMNum MkFPRoundTowardNegative()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Definition Context.cs:4532
Microsoft.Z3.Context.MkProbe
Probe MkProbe(string name)
Creates a new Probe.
Definition Context.cs:4255
Microsoft.Z3.Context.MkFiniteSetRange
Expr MkFiniteSetRange(Expr low, Expr high)
Create a finite set containing integers in the range [low, high].
Definition Context.cs:2664
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:4706
Microsoft.Z3.Context.MkSeqSort
SeqSort MkSeqSort(Sort s)
Create a new sequence sort.
Definition Context.cs:258
Microsoft.Z3.Context.MkTypeVariable
Sort MkTypeVariable(Symbol name)
Create a type variable sort for use as a parameter in polymorphic datatypes.
Definition Context.cs:569
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:3978
Microsoft.Z3.Context.MkBound
Expr MkBound(uint index, Sort ty)
Creates a new bound variable.
Definition Context.cs:798
Microsoft.Z3.Context.MkFPRTN
FPRMNum MkFPRTN()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Definition Context.cs:4540
Microsoft.Z3.Context.MkFPSort128
FPSort MkFPSort128()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition Context.cs:4633
Microsoft.Z3.Context.MkBVUGE
BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
Unsigned greater than or equal to.
Definition Context.cs:1718
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:3226
Microsoft.Z3.Context.MkFPRTP
FPRMNum MkFPRTP()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Definition Context.cs:4524
Microsoft.Z3.Context.MkBoolSort
BoolSort MkBoolSort()
Create a new Boolean sort.
Definition Context.cs:205
Microsoft.Z3.Context.MkFiniteSetMember
BoolExpr MkFiniteSetMember(Expr elem, Expr set)
Check for membership in a finite set.
Definition Context.cs:2601
Microsoft.Z3.Context.MkConcat
BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
Bit-vector concatenation.
Definition Context.cs:1786
Microsoft.Z3.Context.MkPower
ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 ^ t2.
Definition Context.cs:1269
Microsoft.Z3.Context.MkEmptySeq
SeqExpr MkEmptySeq(Sort s)
Create the empty sequence.
Definition Context.cs:2681
Microsoft.Z3.Context.MkFiniteSetSize
Expr MkFiniteSetSize(Expr set)
Get the cardinality of a finite set.
Definition Context.cs:2614
Microsoft.Z3.Context.MkBVNot
BitVecExpr MkBVNot(BitVecExpr t)
Bitwise negation.
Definition Context.cs:1381
Microsoft.Z3.Context.MkFPRem
FPExpr MkFPRem(FPExpr t1, FPExpr t2)
Floating-point remainder.
Definition Context.cs:4872
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:2039
Microsoft.Z3.Context.MkDiv
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
Definition Context.cs:1228
Microsoft.Z3.Context.MkSelect
Expr MkSelect(ArrayExpr a, params Expr[] args)
Array read.
Definition Context.cs:2224
Microsoft.Z3.Context.MkFPNumeral
FPNum MkFPNumeral(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition Context.cs:4694
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:3723
Microsoft.Z3.Context.MkFPLt
BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
Floating-point less than.
Definition Context.cs:4923
Microsoft.Z3.Context.MkSimplifier
Simplifier MkSimplifier(string name)
Creates a new Tactic.
Definition Context.cs:4151
Microsoft.Z3.Context.MkFPGEq
BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
Floating-point greater than or equal.
Definition Context.cs:4933
Microsoft.Z3.Context.MkSignExt
BitVecExpr MkSignExt(uint i, BitVecExpr t)
Bit-vector sign extension.
Definition Context.cs:1821
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:4024
Microsoft.Z3.Context.MkIntSort
IntSort MkIntSort()
Create a new integer sort.
Definition Context.cs:233
Microsoft.Z3.Context.MkFiniteSetSubset
BoolExpr MkFiniteSetSubset(Expr s1, Expr s2)
Check if one finite set is a subset of another.
Definition Context.cs:2625
Microsoft.Z3.Context.MkAnd
BoolExpr MkAnd(IEnumerable< BoolExpr > t)
Create an expression representing t[0] and t[1] and ....
Definition Context.cs:1129
Microsoft.Z3.Context.MkBVMul
BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
Two's complement multiplication.
Definition Context.cs:1541
Microsoft.Z3.Context.StringToInt
IntExpr StringToInt(Expr e)
Convert an integer expression to a string.
Definition Context.cs:2738
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:2103
Microsoft.Z3.Context.MkContains
BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
Check for sequence containment of s2 in s1.
Definition Context.cs:2804
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:3888
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:999
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:3933
Microsoft.Z3.Context.MkBVSub
BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
Two's complement subtraction.
Definition Context.cs:1527
Microsoft.Z3.Context.MkBVUDiv
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Unsigned division.
Definition Context.cs:1560
Microsoft.Z3.Context.Interrupt
void Interrupt()
Interrupt the execution of a Z3 procedure.
Definition Context.cs:4050
Microsoft.Z3.Context.MkBVUGT
BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
Unsigned greater-than.
Definition Context.cs:1750
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:931
Microsoft.Z3.Context.MkBVASHR
BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
Arithmetic shift right.
Definition Context.cs:1918
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:3875
Microsoft.Z3.Context.MkFPZero
FPNum MkFPZero(FPSort s, bool negative)
Create a floating-point zero of sort s.
Definition Context.cs:4664
Microsoft.Z3.Context.MkPBGe
BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean greater-or-equal constraint.
Definition Context.cs:3177
Microsoft.Z3.Context.MkInt
IntNum MkInt(long v)
Create an integer numeral.
Definition Context.cs:3390
Microsoft.Z3.Context.MkReal
RatNum MkReal(long v)
Create a real numeral.
Definition Context.cs:3334
Microsoft.Z3.Context.MkPlus
ReExpr MkPlus(ReExpr re)
Take the Kleene plus of a regular expression.
Definition Context.cs:2983
Microsoft.Z3.Context.MkFPSqrt
FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
Floating-point square root.
Definition Context.cs:4862
Microsoft.Z3.Context.MkIff
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 iff t2.
Definition Context.cs:1061
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:3211
Microsoft.Z3.Context.MkRecFuncDecl
FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
Creates a new recursive function declaration.
Definition Context.cs:687
Microsoft.Z3.Context.MkBVAdd
BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
Two's complement addition.
Definition Context.cs:1513
Microsoft.Z3.Context.MkGt
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
Definition Context.cs:1308
Microsoft.Z3.Context.MkSimpleSolver
Solver MkSimpleSolver()
Creates a new (incremental) solver.
Definition Context.cs:4412
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:4372
Microsoft.Z3.Context.MkBool
BoolExpr MkBool(bool value)
Creates a Boolean value.
Definition Context.cs:991
Microsoft.Z3.Context.MkBVAND
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
Bitwise conjunction.
Definition Context.cs:1417
Microsoft.Z3.Context.MkSolver
Solver MkSolver(Tactic t)
Creates a solver that is implemented using the given tactic.
Definition Context.cs:4435
Microsoft.Z3.Context.MkRealConst
RealExpr MkRealConst(Symbol name)
Creates a real constant.
Definition Context.cs:912
Microsoft.Z3.Context.MkInt
IntNum MkInt(ulong v)
Create an integer numeral.
Definition Context.cs:3401
Microsoft.Z3.Context.MkApp
Expr MkApp(FuncDecl f, IEnumerable< Expr > args)
Create a new function application.
Definition Context.cs:965
Microsoft.Z3.Context.MkToRe
ReExpr MkToRe(SeqExpr s)
Convert a regular expression that accepts sequence s.
Definition Context.cs:2944
Microsoft.Z3.Context.MkFPIsNaN
BoolExpr MkFPIsNaN(FPExpr t)
Predicate indicating whether t is a NaN.
Definition Context.cs:5001
Microsoft.Z3.Context.MkBVRotateRight
BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
Rotate Right.
Definition Context.cs:1950
Microsoft.Z3.Context.SimplifyHelp
string SimplifyHelp()
Return a string describing all available parameters to Expr.Simplify.
Definition Context.cs:5273
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:3569
Microsoft.Z3.Context.MkLambda
Lambda MkLambda(Sort[] sorts, Symbol[] names, Expr body)
Create a lambda expression.
Definition Context.cs:3639
Microsoft.Z3.Context.MkFuncDecl
FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
Creates a new function declaration.
Definition Context.cs:642
Microsoft.Z3.Context.MkBVSLT
BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than.
Definition Context.cs:1670
Microsoft.Z3.Context.MkSetSort
SetSort MkSetSort(Sort ty)
Create a set type.
Definition Context.cs:2369
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:4161
Microsoft.Z3.Context.MkTypeVariable
Sort MkTypeVariable(string name)
Create a type variable sort for use as a parameter in polymorphic datatypes.
Definition Context.cs:580
Microsoft.Z3.Context.MkBV
BitVecNum MkBV(int v, uint size)
Create a bit-vector numeral.
Definition Context.cs:3425
Microsoft.Z3.Context.MkReal
RatNum MkReal(int num, int den)
Create a real from a fraction.
Definition Context.cs:3288
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:4421
Microsoft.Z3.Context.MkFPIsNegative
BoolExpr MkFPIsNegative(FPExpr t)
Predicate indicating whether t is a negative floating-point number.
Definition Context.cs:5010
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:733
Microsoft.Z3.Context.MkIntConst
IntExpr MkIntConst(string name)
Creates an integer constant.
Definition Context.cs:902
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:3919
Microsoft.Z3.Context.MkBVNeg
BitVecExpr MkBVNeg(BitVecExpr t)
Standard two's complement unary minus.
Definition Context.cs:1501
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:773
Microsoft.Z3.Context.Fail
Tactic Fail()
Create a tactic always fails.
Definition Context.cs:3969
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:3990
Microsoft.Z3.Context.MkFPRoundTowardPositive
FPRMNum MkFPRoundTowardPositive()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Definition Context.cs:4516
Microsoft.Z3.Context.MkBVOR
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
Bitwise disjunction.
Definition Context.cs:1431
Microsoft.Z3.Context.MkConst
Expr MkConst(string name, Sort range)
Creates a new Constant of sort range and named name .
Definition Context.cs:839
Microsoft.Z3.Context.MkRem
IntExpr MkRem(IntExpr t1, IntExpr t2)
Create an expression representing t1 rem t2.
Definition Context.cs:1256
Microsoft.Z3.Context.MkFPMul
FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point multiplication.
Definition Context.cs:4826
Microsoft.Z3.Context.MkStringLt
BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
Check if the string s1 is lexicographically strictly less than s2.
Definition Context.cs:2815
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:2071
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:5193
Microsoft.Z3.Context.MkPolymorphicDatatypeSort
DatatypeSort MkPolymorphicDatatypeSort(string name, Sort[] typeParams, Constructor[] constructors)
Create a polymorphic datatype sort with explicit type parameters. Type parameters should be sorts cre...
Definition Context.cs:616
Microsoft.Z3.Context.MkFPSort64
FPSort MkFPSort64()
Create the double-precision (64-bit) FloatingPoint sort.
Definition Context.cs:4617
Microsoft.Z3.Context.MkOr
BoolExpr MkOr(IEnumerable< BoolExpr > ts)
Create an expression representing t[0] or t[1] or ....
Definition Context.cs:1151
Microsoft.Z3.Context.IsFiniteSetSort
bool IsFiniteSetSort(Sort s)
Check if a sort is a finite set sort.
Definition Context.cs:2518
Microsoft.Z3.Context.MkFPRNA
FPRMNum MkFPRNA()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Definition Context.cs:4508
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:1935
Microsoft.Z3.Context.TacticDescription
string TacticDescription(string name)
Returns a string containing a description of the tactic with the given name.
Definition Context.cs:3822
Microsoft.Z3.Context.MkFPRNE
FPRMNum MkFPRNE()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Definition Context.cs:4492
Microsoft.Z3.Context.MkUnit
SeqExpr MkUnit(Expr elem)
Create the singleton sequence.
Definition Context.cs:2690
Microsoft.Z3.Context.NumProbes
uint NumProbes
The number of supported Probes.
Definition Context.cs:4223
Microsoft.Z3.Context.GetFiniteSetSortBasis
Sort GetFiniteSetSortBasis(Sort s)
Get the element sort (basis) of a finite set sort.
Definition Context.cs:2529
Microsoft.Z3.Context.MkPBEq
BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean equal constraint.
Definition Context.cs:3190
Microsoft.Z3.Context.MkInt
IntNum MkInt(int v)
Create an integer numeral.
Definition Context.cs:3368
Microsoft.Z3.Context.MkBVXOR
BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XOR.
Definition Context.cs:1445
Microsoft.Z3.Context.MkStore
ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
Array update.
Definition Context.cs:2283
Microsoft.Z3.Context.MkSolver
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition Context.cs:4390
Microsoft.Z3.Context.MkFPAbs
FPExpr MkFPAbs(FPExpr t)
Floating-point absolute value.
Definition Context.cs:4784
Microsoft.Z3.Context.MkFPMin
FPExpr MkFPMin(FPExpr t1, FPExpr t2)
Minimum of floating-point numbers.
Definition Context.cs:4893
Microsoft.Z3.Context.MkFPDiv
FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point division.
Definition Context.cs:4837
Microsoft.Z3.Context.MkComplement
ReExpr MkComplement(ReExpr re)
Create the complement regular expression.
Definition Context.cs:3001
Microsoft.Z3.Context.MkExtract
BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
Bit-vector extraction.
Definition Context.cs:1805
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:1601
Microsoft.Z3.Context.MkFalse
BoolExpr MkFalse()
The false Term.
Definition Context.cs:983
Microsoft.Z3.Context.MkLength
IntExpr MkLength(SeqExpr s)
Retrieve the length of a given sequence.
Definition Context.cs:2762
Microsoft.Z3.Context.MkReal
RatNum MkReal(int v)
Create a real numeral.
Definition Context.cs:3312
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:2699
Microsoft.Z3.Context.MkStore
ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
Array update.
Definition Context.cs:2253
Microsoft.Z3.Context.MkFiniteSetIntersect
Expr MkFiniteSetIntersect(Expr s1, Expr s2)
Create the intersection of two finite sets.
Definition Context.cs:2575
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:5039
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:2930
Microsoft.Z3.Context.MkMul
ArithExpr MkMul(params ArithExpr[] ts)
Create an expression representing t[0] * t[1] * ....
Definition Context.cs:1184
Microsoft.Z3.Context.MkBVSGE
BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater than or equal to.
Definition Context.cs:1734
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:3505
Microsoft.Z3.Context.MkFP
FPNum MkFP(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition Context.cs:4738
Microsoft.Z3.Context.MkFPIsNormal
BoolExpr MkFPIsNormal(FPExpr t)
Predicate indicating whether t is a normal floating-point number.
Definition Context.cs:4965
Microsoft.Z3.Context.MkPrefixOf
BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
Check for sequence prefix.
Definition Context.cs:2782
Microsoft.Z3.Context.MkFPIsPositive
BoolExpr MkFPIsPositive(FPExpr t)
Predicate indicating whether t is a positive floating-point number.
Definition Context.cs:5019
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.Model
A Model contains interpretations (assignments) of constants and functions.
Definition Model.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
Microsoft.Z3.Z3Object
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition Z3Object.cs:33
Z3_ast_print_mode
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition z3_api.h:1364
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition z3_api.h:1389
Microsoft.Z3.Z3_context
System.IntPtr Z3_context
Definition Context.cs:29
Generated on Sun Sep 13 2026 03:38:44 for Z3 by doxygen 1.9.8