Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Context.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Context.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Context
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-15
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Collections.Generic;
22 using System.Runtime.InteropServices;
23 using System.Diagnostics.Contracts;
24 
25 namespace Microsoft.Z3
26 {
30  [ContractVerification(true)]
31  public class Context : IDisposable
32  {
33  #region Constructors
34 
35 
36 
37  public Context()
38  : base()
39  {
40  m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
41  InitContext();
42  }
43 
47  public Context(Dictionary<string, string> settings)
48  : base()
49  {
50  Contract.Requires(settings != null);
51 
52  IntPtr cfg = Native.Z3_mk_config();
53  foreach (KeyValuePair<string, string> kv in settings)
54  Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
55  m_ctx = Native.Z3_mk_context_rc(cfg);
56  Native.Z3_del_config(cfg);
57  InitContext();
58  }
59  #endregion
60 
61  #region Symbols
62 
63 
64 
65 
66 
67 
68 
69  public IntSymbol MkSymbol(int i)
70  {
71  Contract.Ensures(Contract.Result<IntSymbol>() != null);
72 
73  return new IntSymbol(this, i);
74  }
75 
79  public StringSymbol MkSymbol(string name)
80  {
81  Contract.Ensures(Contract.Result<StringSymbol>() != null);
82 
83  return new StringSymbol(this, name);
84  }
85 
89  internal Symbol[] MkSymbols(string[] names)
90  {
91  Contract.Ensures(names == null || Contract.Result<Symbol[]>() != null);
92  Contract.Ensures(names != null || Contract.Result<Symbol[]>() == null);
93  Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.Result<Symbol[]>().Length == names.Length);
94  Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.ForAll(Contract.Result<Symbol[]>(), s => s != null));
95 
96  if (names == null) return null;
97  Symbol[] result = new Symbol[names.Length];
98  for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
99  return result;
100  }
101  #endregion
102 
103  #region Sorts
104  private BoolSort m_boolSort = null;
105  private IntSort m_intSort = null;
106  private RealSort m_realSort = null;
107 
111  public BoolSort BoolSort
112  {
113  get
114  {
115  Contract.Ensures(Contract.Result<BoolSort>() != null);
116 
117  if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
118  }
119  }
120 
124  public IntSort IntSort
125  {
126  get
127  {
128  Contract.Ensures(Contract.Result<IntSort>() != null);
129  if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
130  }
131  }
132 
133 
137  public RealSort RealSort { get { Contract.Ensures(Contract.Result<RealSort>() != null); if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort; } }
138 
142  public BoolSort MkBoolSort()
143  {
144  Contract.Ensures(Contract.Result<BoolSort>() != null);
145  return new BoolSort(this);
146  }
147 
151  public UninterpretedSort MkUninterpretedSort(Symbol s)
152  {
153  Contract.Requires(s != null);
154  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
155 
156  CheckContextMatch(s);
157  return new UninterpretedSort(this, s);
158  }
159 
163  public UninterpretedSort MkUninterpretedSort(string str)
164  {
165  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
166 
167  return MkUninterpretedSort(MkSymbol(str));
168  }
169 
173  public IntSort MkIntSort()
174  {
175  Contract.Ensures(Contract.Result<IntSort>() != null);
176 
177  return new IntSort(this);
178  }
179 
183  public RealSort MkRealSort()
184  {
185  Contract.Ensures(Contract.Result<RealSort>() != null);
186  return new RealSort(this);
187  }
188 
192  public BitVecSort MkBitVecSort(uint size)
193  {
194  Contract.Ensures(Contract.Result<BitVecSort>() != null);
195 
196  return new BitVecSort(this, size);
197  }
198 
202  public ArraySort MkArraySort(Sort domain, Sort range)
203  {
204  Contract.Requires(domain != null);
205  Contract.Requires(range != null);
206  Contract.Ensures(Contract.Result<ArraySort>() != null);
207 
208  CheckContextMatch(domain);
209  CheckContextMatch(range);
210  return new ArraySort(this, domain, range);
211  }
212 
216  public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
217  {
218  Contract.Requires(name != null);
219  Contract.Requires(fieldNames != null);
220  Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
221  Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
222  Contract.Ensures(Contract.Result<TupleSort>() != null);
223 
224  CheckContextMatch(name);
225  CheckContextMatch(fieldNames);
226  CheckContextMatch(fieldSorts);
227  return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
228  }
229 
233  public EnumSort MkEnumSort(Symbol name, Symbol[] enumNames)
234  {
235  Contract.Requires(name != null);
236  Contract.Requires(enumNames != null);
237  Contract.Requires(Contract.ForAll(enumNames, f => f != null));
238 
239  Contract.Ensures(Contract.Result<EnumSort>() != null);
240 
241  CheckContextMatch(name);
242  CheckContextMatch(enumNames);
243  return new EnumSort(this, name, enumNames);
244  }
245 
249  public EnumSort MkEnumSort(string name, string[] enumNames)
250  {
251  Contract.Requires(enumNames != null);
252  Contract.Ensures(Contract.Result<EnumSort>() != null);
253 
254  return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
255  }
256 
260  public ListSort MkListSort(Symbol name, Sort elemSort)
261  {
262  Contract.Requires(name != null);
263  Contract.Requires(elemSort != null);
264  Contract.Ensures(Contract.Result<ListSort>() != null);
265 
266  CheckContextMatch(name);
267  CheckContextMatch(elemSort);
268  return new ListSort(this, name, elemSort);
269  }
270 
274  public ListSort MkListSort(string name, Sort elemSort)
275  {
276  Contract.Requires(elemSort != null);
277  Contract.Ensures(Contract.Result<ListSort>() != null);
278 
279  CheckContextMatch(elemSort);
280  return new ListSort(this, MkSymbol(name), elemSort);
281  }
282 
286  public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
287  {
288  Contract.Requires(name != null);
289  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
290 
291  CheckContextMatch(name);
292  return new FiniteDomainSort(this, name, size);
293  }
294 
298  public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
299  {
300  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
301 
302  return new FiniteDomainSort(this, MkSymbol(name), size);
303  }
304 
305 
306  #region Datatypes
307 
308 
309 
310 
311 
312 
313 
314 
315 
316 
317  public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
318  {
319  Contract.Requires(name != null);
320  Contract.Requires(recognizer != null);
321  Contract.Ensures(Contract.Result<Constructor>() != null);
322 
323  return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
324  }
325 
335  public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
336  {
337  Contract.Ensures(Contract.Result<Constructor>() != null);
338 
339  return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
340  }
341 
345  public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
346  {
347  Contract.Requires(name != null);
348  Contract.Requires(constructors != null);
349  Contract.Requires(Contract.ForAll(constructors, c => c != null));
350 
351  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
352 
353  CheckContextMatch(name);
354  CheckContextMatch(constructors);
355  return new DatatypeSort(this, name, constructors);
356  }
357 
361  public DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
362  {
363  Contract.Requires(constructors != null);
364  Contract.Requires(Contract.ForAll(constructors, c => c != null));
365  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
366 
367  CheckContextMatch(constructors);
368  return new DatatypeSort(this, MkSymbol(name), constructors);
369  }
370 
376  public DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
377  {
378  Contract.Requires(names != null);
379  Contract.Requires(c != null);
380  Contract.Requires(names.Length == c.Length);
381  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
382  Contract.Requires(Contract.ForAll(names, name => name != null));
383  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
384 
385  CheckContextMatch(names);
386  uint n = (uint)names.Length;
387  ConstructorList[] cla = new ConstructorList[n];
388  IntPtr[] n_constr = new IntPtr[n];
389  for (uint i = 0; i < n; i++)
390  {
391  var constructor = c[i];
392  Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
393  CheckContextMatch(constructor);
394  cla[i] = new ConstructorList(this, constructor);
395  n_constr[i] = cla[i].NativeObject;
396  }
397  IntPtr[] n_res = new IntPtr[n];
398  Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
399  DatatypeSort[] res = new DatatypeSort[n];
400  for (uint i = 0; i < n; i++)
401  res[i] = new DatatypeSort(this, n_res[i]);
402  return res;
403  }
404 
411  public DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
412  {
413  Contract.Requires(names != null);
414  Contract.Requires(c != null);
415  Contract.Requires(names.Length == c.Length);
416  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
417  Contract.Requires(Contract.ForAll(names, name => name != null));
418  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
419 
420  return MkDatatypeSorts(MkSymbols(names), c);
421  }
422 
423  #endregion
424  #endregion
425 
426  #region Function Declarations
427 
428 
429 
430  public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
431  {
432  Contract.Requires(name != null);
433  Contract.Requires(range != null);
434  Contract.Requires(Contract.ForAll(domain, d => d != null));
435  Contract.Ensures(Contract.Result<FuncDecl>() != null);
436 
437  CheckContextMatch(name);
438  CheckContextMatch(domain);
439  CheckContextMatch(range);
440  return new FuncDecl(this, name, domain, range);
441  }
442 
446  public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
447  {
448  Contract.Requires(name != null);
449  Contract.Requires(domain != null);
450  Contract.Requires(range != null);
451  Contract.Ensures(Contract.Result<FuncDecl>() != null);
452 
453  CheckContextMatch(name);
454  CheckContextMatch(domain);
455  CheckContextMatch(range);
456  Sort[] q = new Sort[] { domain };
457  return new FuncDecl(this, name, q, range);
458  }
459 
463  public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
464  {
465  Contract.Requires(range != null);
466  Contract.Requires(Contract.ForAll(domain, d => d != null));
467  Contract.Ensures(Contract.Result<FuncDecl>() != null);
468 
469  CheckContextMatch(domain);
470  CheckContextMatch(range);
471  return new FuncDecl(this, MkSymbol(name), domain, range);
472  }
473 
477  public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
478  {
479  Contract.Requires(range != null);
480  Contract.Requires(domain != null);
481  Contract.Ensures(Contract.Result<FuncDecl>() != null);
482 
483  CheckContextMatch(domain);
484  CheckContextMatch(range);
485  Sort[] q = new Sort[] { domain };
486  return new FuncDecl(this, MkSymbol(name), q, range);
487  }
488 
494  public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
495  {
496  Contract.Requires(range != null);
497  Contract.Requires(Contract.ForAll(domain, d => d != null));
498  Contract.Ensures(Contract.Result<FuncDecl>() != null);
499 
500  CheckContextMatch(domain);
501  CheckContextMatch(range);
502  return new FuncDecl(this, prefix, domain, range);
503  }
504 
508  public FuncDecl MkConstDecl(Symbol name, Sort range)
509  {
510  Contract.Requires(name != null);
511  Contract.Requires(range != null);
512  Contract.Ensures(Contract.Result<FuncDecl>() != null);
513 
514  CheckContextMatch(name);
515  CheckContextMatch(range);
516  return new FuncDecl(this, name, null, range);
517  }
518 
522  public FuncDecl MkConstDecl(string name, Sort range)
523  {
524  Contract.Requires(range != null);
525  Contract.Ensures(Contract.Result<FuncDecl>() != null);
526 
527  CheckContextMatch(range);
528  return new FuncDecl(this, MkSymbol(name), null, range);
529  }
530 
536  public FuncDecl MkFreshConstDecl(string prefix, Sort range)
537  {
538  Contract.Requires(range != null);
539  Contract.Ensures(Contract.Result<FuncDecl>() != null);
540 
541  CheckContextMatch(range);
542  return new FuncDecl(this, prefix, null, range);
543  }
544  #endregion
545 
546  #region Bound Variables
547 
548 
549 
550 
551 
552  public Expr MkBound(uint index, Sort ty)
553  {
554  Contract.Requires(ty != null);
555  Contract.Ensures(Contract.Result<Expr>() != null);
556 
557  return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
558  }
559  #endregion
560 
561  #region Quantifier Patterns
562 
563 
564 
565  public Pattern MkPattern(params Expr[] terms)
566  {
567  Contract.Requires(terms != null);
568  if (terms.Length == 0)
569  throw new Z3Exception("Cannot create a pattern from zero terms");
570 
571  Contract.Ensures(Contract.Result<Pattern>() != null);
572 
573  Contract.EndContractBlock();
574 
575  IntPtr[] termsNative = AST.ArrayToNative(terms);
576  return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
577  }
578  #endregion
579 
580  #region Constants
581 
582 
583 
584  public Expr MkConst(Symbol name, Sort range)
585  {
586  Contract.Requires(name != null);
587  Contract.Requires(range != null);
588  Contract.Ensures(Contract.Result<Expr>() != null);
589 
590  CheckContextMatch(name);
591  CheckContextMatch(range);
592 
593  return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
594  }
595 
599  public Expr MkConst(string name, Sort range)
600  {
601  Contract.Requires(range != null);
602  Contract.Ensures(Contract.Result<Expr>() != null);
603 
604  return MkConst(MkSymbol(name), range);
605  }
606 
611  public Expr MkFreshConst(string prefix, Sort range)
612  {
613  Contract.Requires(range != null);
614  Contract.Ensures(Contract.Result<Expr>() != null);
615 
616  CheckContextMatch(range);
617  return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
618  }
619 
624  public Expr MkConst(FuncDecl f)
625  {
626  Contract.Requires(f != null);
627  Contract.Ensures(Contract.Result<Expr>() != null);
628 
629  return MkApp(f);
630  }
631 
635  public BoolExpr MkBoolConst(Symbol name)
636  {
637  Contract.Requires(name != null);
638  Contract.Ensures(Contract.Result<BoolExpr>() != null);
639 
640  return (BoolExpr)MkConst(name, BoolSort);
641  }
642 
646  public BoolExpr MkBoolConst(string name)
647  {
648  Contract.Ensures(Contract.Result<BoolExpr>() != null);
649 
650  return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
651  }
652 
656  public IntExpr MkIntConst(Symbol name)
657  {
658  Contract.Requires(name != null);
659  Contract.Ensures(Contract.Result<IntExpr>() != null);
660 
661  return (IntExpr)MkConst(name, IntSort);
662  }
663 
667  public IntExpr MkIntConst(string name)
668  {
669  Contract.Requires(name != null);
670  Contract.Ensures(Contract.Result<IntExpr>() != null);
671 
672  return (IntExpr)MkConst(name, IntSort);
673  }
674 
678  public RealExpr MkRealConst(Symbol name)
679  {
680  Contract.Requires(name != null);
681  Contract.Ensures(Contract.Result<RealExpr>() != null);
682 
683  return (RealExpr)MkConst(name, RealSort);
684  }
685 
689  public RealExpr MkRealConst(string name)
690  {
691  Contract.Ensures(Contract.Result<RealExpr>() != null);
692 
693  return (RealExpr)MkConst(name, RealSort);
694  }
695 
699  public BitVecExpr MkBVConst(Symbol name, uint size)
700  {
701  Contract.Requires(name != null);
702  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
703 
704  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
705  }
706 
710  public BitVecExpr MkBVConst(string name, uint size)
711  {
712  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
713 
714  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
715  }
716  #endregion
717 
718  #region Terms
719 
720 
721 
722  public Expr MkApp(FuncDecl f, params Expr[] args)
723  {
724  Contract.Requires(f != null);
725  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
726  Contract.Ensures(Contract.Result<Expr>() != null);
727 
728  CheckContextMatch(f);
729  CheckContextMatch(args);
730  return Expr.Create(this, f, args);
731  }
732 
733  #region Propositional
734 
735 
736 
737  public BoolExpr MkTrue()
738  {
739  Contract.Ensures(Contract.Result<BoolExpr>() != null);
740 
741  return new BoolExpr(this, Native.Z3_mk_true(nCtx));
742  }
743 
747  public BoolExpr MkFalse()
748  {
749  Contract.Ensures(Contract.Result<BoolExpr>() != null);
750 
751  return new BoolExpr(this, Native.Z3_mk_false(nCtx));
752  }
753 
757  public BoolExpr MkBool(bool value)
758  {
759  Contract.Ensures(Contract.Result<BoolExpr>() != null);
760 
761  return value ? MkTrue() : MkFalse();
762  }
763 
767  public BoolExpr MkEq(Expr x, Expr y)
768  {
769  Contract.Requires(x != null);
770  Contract.Requires(y != null);
771  Contract.Ensures(Contract.Result<BoolExpr>() != null);
772 
773  CheckContextMatch(x);
774  CheckContextMatch(y);
775  return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
776  }
777 
781  public BoolExpr MkDistinct(params Expr[] args)
782  {
783  Contract.Requires(args != null);
784  Contract.Requires(Contract.ForAll(args, a => a != null));
785 
786  Contract.Ensures(Contract.Result<BoolExpr>() != null);
787 
788  CheckContextMatch(args);
789  return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
790  }
791 
795  public BoolExpr MkNot(BoolExpr a)
796  {
797  Contract.Requires(a != null);
798  Contract.Ensures(Contract.Result<BoolExpr>() != null);
799 
800  CheckContextMatch(a);
801  return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
802  }
803 
810  public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
811  {
812  Contract.Requires(t1 != null);
813  Contract.Requires(t2 != null);
814  Contract.Requires(t3 != null);
815  Contract.Ensures(Contract.Result<Expr>() != null);
816 
817  CheckContextMatch(t1);
818  CheckContextMatch(t2);
819  CheckContextMatch(t3);
820  return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
821  }
822 
826  public BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
827  {
828  Contract.Requires(t1 != null);
829  Contract.Requires(t2 != null);
830  Contract.Ensures(Contract.Result<BoolExpr>() != null);
831 
832  CheckContextMatch(t1);
833  CheckContextMatch(t2);
834  return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
835  }
836 
840  public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
841  {
842  Contract.Requires(t1 != null);
843  Contract.Requires(t2 != null);
844  Contract.Ensures(Contract.Result<BoolExpr>() != null);
845 
846  CheckContextMatch(t1);
847  CheckContextMatch(t2);
848  return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
849  }
850 
854  public BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
855  {
856  Contract.Requires(t1 != null);
857  Contract.Requires(t2 != null);
858  Contract.Ensures(Contract.Result<BoolExpr>() != null);
859 
860  CheckContextMatch(t1);
861  CheckContextMatch(t2);
862  return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
863  }
864 
868  public BoolExpr MkAnd(params BoolExpr[] t)
869  {
870  Contract.Requires(t != null);
871  Contract.Requires(Contract.ForAll(t, a => a != null));
872  Contract.Ensures(Contract.Result<BoolExpr>() != null);
873 
874  CheckContextMatch(t);
875  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
876  }
877 
881  public BoolExpr MkOr(params BoolExpr[] t)
882  {
883  Contract.Requires(t != null);
884  Contract.Requires(Contract.ForAll(t, a => a != null));
885  Contract.Ensures(Contract.Result<BoolExpr>() != null);
886 
887  CheckContextMatch(t);
888  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
889  }
890  #endregion
891 
892  #region Arithmetic
893 
894 
895 
896  public ArithExpr MkAdd(params ArithExpr[] t)
897  {
898  Contract.Requires(t != null);
899  Contract.Requires(Contract.ForAll(t, a => a != null));
900  Contract.Ensures(Contract.Result<ArithExpr>() != null);
901 
902  CheckContextMatch(t);
903  return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
904  }
905 
909  public ArithExpr MkMul(params ArithExpr[] t)
910  {
911  Contract.Requires(t != null);
912  Contract.Requires(Contract.ForAll(t, a => a != null));
913  Contract.Ensures(Contract.Result<ArithExpr>() != null);
914 
915  CheckContextMatch(t);
916  return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
917  }
918 
922  public ArithExpr MkSub(params ArithExpr[] t)
923  {
924  Contract.Requires(t != null);
925  Contract.Requires(Contract.ForAll(t, a => a != null));
926  Contract.Ensures(Contract.Result<ArithExpr>() != null);
927 
928  CheckContextMatch(t);
929  return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
930  }
931 
935  public ArithExpr MkUnaryMinus(ArithExpr t)
936  {
937  Contract.Requires(t != null);
938  Contract.Ensures(Contract.Result<ArithExpr>() != null);
939 
940  CheckContextMatch(t);
941  return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
942  }
943 
947  public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
948  {
949  Contract.Requires(t1 != null);
950  Contract.Requires(t2 != null);
951  Contract.Ensures(Contract.Result<ArithExpr>() != null);
952 
953  CheckContextMatch(t1);
954  CheckContextMatch(t2);
955  return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
956  }
957 
962  public IntExpr MkMod(IntExpr t1, IntExpr t2)
963  {
964  Contract.Requires(t1 != null);
965  Contract.Requires(t2 != null);
966  Contract.Ensures(Contract.Result<IntExpr>() != null);
967 
968  CheckContextMatch(t1);
969  CheckContextMatch(t2);
970  return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
971  }
972 
977  public IntExpr MkRem(IntExpr t1, IntExpr t2)
978  {
979  Contract.Requires(t1 != null);
980  Contract.Requires(t2 != null);
981  Contract.Ensures(Contract.Result<IntExpr>() != null);
982 
983  CheckContextMatch(t1);
984  CheckContextMatch(t2);
985  return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
986  }
987 
991  public ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
992  {
993  Contract.Requires(t1 != null);
994  Contract.Requires(t2 != null);
995  Contract.Ensures(Contract.Result<ArithExpr>() != null);
996 
997  CheckContextMatch(t1);
998  CheckContextMatch(t2);
999  return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1000  }
1001 
1005  public BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
1006  {
1007  Contract.Requires(t1 != null);
1008  Contract.Requires(t2 != null);
1009  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1010 
1011  CheckContextMatch(t1);
1012  CheckContextMatch(t2);
1013  return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1014  }
1015 
1019  public BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
1020  {
1021  Contract.Requires(t1 != null);
1022  Contract.Requires(t2 != null);
1023  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1024 
1025  CheckContextMatch(t1);
1026  CheckContextMatch(t2);
1027  return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1028  }
1029 
1033  public BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
1034  {
1035  Contract.Requires(t1 != null);
1036  Contract.Requires(t2 != null);
1037  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1038 
1039  CheckContextMatch(t1);
1040  CheckContextMatch(t2);
1041  return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1042  }
1043 
1047  public BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
1048  {
1049  Contract.Requires(t1 != null);
1050  Contract.Requires(t2 != null);
1051  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1052 
1053  CheckContextMatch(t1);
1054  CheckContextMatch(t2);
1055  return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1056  }
1057 
1068  public RealExpr MkInt2Real(IntExpr t)
1069  {
1070  Contract.Requires(t != null);
1071  Contract.Ensures(Contract.Result<RealExpr>() != null);
1072 
1073  CheckContextMatch(t);
1074  return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1075  }
1076 
1084  public IntExpr MkReal2Int(RealExpr t)
1085  {
1086  Contract.Requires(t != null);
1087  Contract.Ensures(Contract.Result<IntExpr>() != null);
1088 
1089  CheckContextMatch(t);
1090  return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1091  }
1092 
1096  public BoolExpr MkIsInteger(RealExpr t)
1097  {
1098  Contract.Requires(t != null);
1099  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1100 
1101  CheckContextMatch(t);
1102  return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1103  }
1104  #endregion
1105 
1106  #region Bit-vectors
1107 
1108 
1109 
1110 
1111  public BitVecExpr MkBVNot(BitVecExpr t)
1112  {
1113  Contract.Requires(t != null);
1114  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1115 
1116  CheckContextMatch(t);
1117  return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1118  }
1119 
1124  public BitVecExpr MkBVRedAND(BitVecExpr t)
1125  {
1126  Contract.Requires(t != null);
1127  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1128 
1129  CheckContextMatch(t);
1130  return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1131  }
1132 
1137  public BitVecExpr MkBVRedOR(BitVecExpr t)
1138  {
1139  Contract.Requires(t != null);
1140  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1141 
1142  CheckContextMatch(t);
1143  return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1144  }
1145 
1150  public BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
1151  {
1152  Contract.Requires(t1 != null);
1153  Contract.Requires(t2 != null);
1154  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1155 
1156  CheckContextMatch(t1);
1157  CheckContextMatch(t2);
1158  return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1159  }
1160 
1165  public BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
1166  {
1167  Contract.Requires(t1 != null);
1168  Contract.Requires(t2 != null);
1169  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1170 
1171  CheckContextMatch(t1);
1172  CheckContextMatch(t2);
1173  return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1174  }
1175 
1180  public BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
1181  {
1182  Contract.Requires(t1 != null);
1183  Contract.Requires(t2 != null);
1184  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1185 
1186  CheckContextMatch(t1);
1187  CheckContextMatch(t2);
1188  return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1189  }
1190 
1195  public BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
1196  {
1197  Contract.Requires(t1 != null);
1198  Contract.Requires(t2 != null);
1199  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1200 
1201  CheckContextMatch(t1);
1202  CheckContextMatch(t2);
1203  return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1204  }
1205 
1210  public BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
1211  {
1212  Contract.Requires(t1 != null);
1213  Contract.Requires(t2 != null);
1214  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1215 
1216  CheckContextMatch(t1);
1217  CheckContextMatch(t2);
1218  return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1219  }
1220 
1225  public BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
1226  {
1227  Contract.Requires(t1 != null);
1228  Contract.Requires(t2 != null);
1229  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1230 
1231  CheckContextMatch(t1);
1232  CheckContextMatch(t2);
1233  return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1234  }
1235 
1240  public BitVecExpr MkBVNeg(BitVecExpr t)
1241  {
1242  Contract.Requires(t != null);
1243  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1244 
1245  CheckContextMatch(t);
1246  return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1247  }
1248 
1253  public BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
1254  {
1255  Contract.Requires(t1 != null);
1256  Contract.Requires(t2 != null);
1257  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1258 
1259  CheckContextMatch(t1);
1260  CheckContextMatch(t2);
1261  return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1262  }
1263 
1268  public BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
1269  {
1270  Contract.Requires(t1 != null);
1271  Contract.Requires(t2 != null);
1272  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1273 
1274  CheckContextMatch(t1);
1275  CheckContextMatch(t2);
1276  return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1277  }
1278 
1283  public BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
1284  {
1285  Contract.Requires(t1 != null);
1286  Contract.Requires(t2 != null);
1287  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1288 
1289  CheckContextMatch(t1);
1290  CheckContextMatch(t2);
1291  return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1292  }
1293 
1303  public BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
1304  {
1305  Contract.Requires(t1 != null);
1306  Contract.Requires(t2 != null);
1307  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1308 
1309  CheckContextMatch(t1);
1310  CheckContextMatch(t2);
1311  return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1312  }
1313 
1327  public BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
1328  {
1329  Contract.Requires(t1 != null);
1330  Contract.Requires(t2 != null);
1331  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1332 
1333  CheckContextMatch(t1);
1334  CheckContextMatch(t2);
1335  return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1336  }
1337 
1346  public BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
1347  {
1348  Contract.Requires(t1 != null);
1349  Contract.Requires(t2 != null);
1350  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1351 
1352  CheckContextMatch(t1);
1353  CheckContextMatch(t2);
1354  return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1355  }
1356 
1367  public BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
1368  {
1369  Contract.Requires(t1 != null);
1370  Contract.Requires(t2 != null);
1371  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1372 
1373  CheckContextMatch(t1);
1374  CheckContextMatch(t2);
1375  return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1376  }
1377 
1385  public BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
1386  {
1387  Contract.Requires(t1 != null);
1388  Contract.Requires(t2 != null);
1389  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1390 
1391  CheckContextMatch(t1);
1392  CheckContextMatch(t2);
1393  return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1394  }
1395 
1402  public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
1403  {
1404  Contract.Requires(t1 != null);
1405  Contract.Requires(t2 != null);
1406  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1407 
1408  CheckContextMatch(t1);
1409  CheckContextMatch(t2);
1410  return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1411  }
1412 
1419  public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
1420  {
1421  Contract.Requires(t1 != null);
1422  Contract.Requires(t2 != null);
1423  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1424 
1425  CheckContextMatch(t1);
1426  CheckContextMatch(t2);
1427  return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1428  }
1429 
1436  public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
1437  {
1438  Contract.Requires(t1 != null);
1439  Contract.Requires(t2 != null);
1440  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1441 
1442  CheckContextMatch(t1);
1443  CheckContextMatch(t2);
1444  return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1445  }
1446 
1453  public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
1454  {
1455  Contract.Requires(t1 != null);
1456  Contract.Requires(t2 != null);
1457  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1458 
1459  CheckContextMatch(t1);
1460  CheckContextMatch(t2);
1461  return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1462  }
1463 
1470  public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
1471  {
1472  Contract.Requires(t1 != null);
1473  Contract.Requires(t2 != null);
1474  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1475 
1476  CheckContextMatch(t1);
1477  CheckContextMatch(t2);
1478  return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1479  }
1480 
1487  public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
1488  {
1489  Contract.Requires(t1 != null);
1490  Contract.Requires(t2 != null);
1491  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1492 
1493  CheckContextMatch(t1);
1494  CheckContextMatch(t2);
1495  return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1496  }
1497 
1504  public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
1505  {
1506  Contract.Requires(t1 != null);
1507  Contract.Requires(t2 != null);
1508  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1509 
1510  CheckContextMatch(t1);
1511  CheckContextMatch(t2);
1512  return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1513  }
1514 
1521  public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
1522  {
1523  Contract.Requires(t1 != null);
1524  Contract.Requires(t2 != null);
1525  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1526 
1527  CheckContextMatch(t1);
1528  CheckContextMatch(t2);
1529  return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1530  }
1531 
1542  public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
1543  {
1544  Contract.Requires(t1 != null);
1545  Contract.Requires(t2 != null);
1546  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1547 
1548  CheckContextMatch(t1);
1549  CheckContextMatch(t2);
1550  return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1551  }
1552 
1562  public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
1563  {
1564  Contract.Requires(t != null);
1565  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1566 
1567  CheckContextMatch(t);
1568  return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1569  }
1570 
1579  public BitVecExpr MkSignExt(uint i, BitVecExpr t)
1580  {
1581  Contract.Requires(t != null);
1582  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1583 
1584  CheckContextMatch(t);
1585  return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1586  }
1587 
1597  public BitVecExpr MkZeroExt(uint i, BitVecExpr t)
1598  {
1599  Contract.Requires(t != null);
1600  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1601 
1602  CheckContextMatch(t);
1603  return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1604  }
1605 
1612  public BitVecExpr MkRepeat(uint i, BitVecExpr t)
1613  {
1614  Contract.Requires(t != null);
1615  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1616 
1617  CheckContextMatch(t);
1618  return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1619  }
1620 
1633  public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
1634  {
1635  Contract.Requires(t1 != null);
1636  Contract.Requires(t2 != null);
1637  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1638 
1639  CheckContextMatch(t1);
1640  CheckContextMatch(t2);
1641  return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1642  }
1643 
1656  public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
1657  {
1658  Contract.Requires(t1 != null);
1659  Contract.Requires(t2 != null);
1660  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1661 
1662  CheckContextMatch(t1);
1663  CheckContextMatch(t2);
1664  return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1665  }
1666 
1681  public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
1682  {
1683  Contract.Requires(t1 != null);
1684  Contract.Requires(t2 != null);
1685  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1686 
1687  CheckContextMatch(t1);
1688  CheckContextMatch(t2);
1689  return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1690  }
1691 
1699  public BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
1700  {
1701  Contract.Requires(t != null);
1702  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1703 
1704  CheckContextMatch(t);
1705  return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1706  }
1707 
1715  public BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
1716  {
1717  Contract.Requires(t != null);
1718  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1719 
1720  CheckContextMatch(t);
1721  return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1722  }
1723 
1731  public BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
1732  {
1733  Contract.Requires(t1 != null);
1734  Contract.Requires(t2 != null);
1735  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1736 
1737  CheckContextMatch(t1);
1738  CheckContextMatch(t2);
1739  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1740  }
1741 
1749  public BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
1750  {
1751  Contract.Requires(t1 != null);
1752  Contract.Requires(t2 != null);
1753  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1754 
1755  CheckContextMatch(t1);
1756  CheckContextMatch(t2);
1757  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1758  }
1759 
1770  public BitVecExpr MkInt2BV(uint n, IntExpr t)
1771  {
1772  Contract.Requires(t != null);
1773  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1774 
1775  CheckContextMatch(t);
1776  return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1777  }
1778 
1794  public IntExpr MkBV2Int(BitVecExpr t, bool signed)
1795  {
1796  Contract.Requires(t != null);
1797  Contract.Ensures(Contract.Result<IntExpr>() != null);
1798 
1799  CheckContextMatch(t);
1800  return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
1801  }
1802 
1809  public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1810  {
1811  Contract.Requires(t1 != null);
1812  Contract.Requires(t2 != null);
1813  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1814 
1815  CheckContextMatch(t1);
1816  CheckContextMatch(t2);
1817  return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1818  }
1819 
1826  public BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
1827  {
1828  Contract.Requires(t1 != null);
1829  Contract.Requires(t2 != null);
1830  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1831 
1832  CheckContextMatch(t1);
1833  CheckContextMatch(t2);
1834  return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1835  }
1836 
1843  public BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
1844  {
1845  Contract.Requires(t1 != null);
1846  Contract.Requires(t2 != null);
1847  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1848 
1849  CheckContextMatch(t1);
1850  CheckContextMatch(t2);
1851  return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1852  }
1853 
1860  public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1861  {
1862  Contract.Requires(t1 != null);
1863  Contract.Requires(t2 != null);
1864  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1865 
1866  CheckContextMatch(t1);
1867  CheckContextMatch(t2);
1868  return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1869  }
1870 
1877  public BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
1878  {
1879  Contract.Requires(t1 != null);
1880  Contract.Requires(t2 != null);
1881  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1882 
1883  CheckContextMatch(t1);
1884  CheckContextMatch(t2);
1885  return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1886  }
1887 
1894  public BoolExpr MkBVNegNoOverflow(BitVecExpr t)
1895  {
1896  Contract.Requires(t != null);
1897  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1898 
1899  CheckContextMatch(t);
1900  return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
1901  }
1902 
1909  public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1910  {
1911  Contract.Requires(t1 != null);
1912  Contract.Requires(t2 != null);
1913  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1914 
1915  CheckContextMatch(t1);
1916  CheckContextMatch(t2);
1917  return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1918  }
1919 
1926  public BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
1927  {
1928  Contract.Requires(t1 != null);
1929  Contract.Requires(t2 != null);
1930  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1931 
1932  CheckContextMatch(t1);
1933  CheckContextMatch(t2);
1934  return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1935  }
1936  #endregion
1937 
1938  #region Arrays
1939 
1940 
1941 
1942  public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
1943  {
1944  Contract.Requires(name != null);
1945  Contract.Requires(domain != null);
1946  Contract.Requires(range != null);
1947  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
1948 
1949  return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
1950  }
1951 
1955  public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
1956  {
1957  Contract.Requires(domain != null);
1958  Contract.Requires(range != null);
1959  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
1960 
1961  return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
1962  }
1963 
1977  public Expr MkSelect(ArrayExpr a, Expr i)
1978  {
1979  Contract.Requires(a != null);
1980  Contract.Requires(i != null);
1981  Contract.Ensures(Contract.Result<Expr>() != null);
1982 
1983  CheckContextMatch(a);
1984  CheckContextMatch(i);
1985  return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
1986  }
1987 
2005  public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
2006  {
2007  Contract.Requires(a != null);
2008  Contract.Requires(i != null);
2009  Contract.Requires(v != null);
2010  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2011 
2012  CheckContextMatch(a);
2013  CheckContextMatch(i);
2014  CheckContextMatch(v);
2015  return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2016  }
2017 
2027  public ArrayExpr MkConstArray(Sort domain, Expr v)
2028  {
2029  Contract.Requires(domain != null);
2030  Contract.Requires(v != null);
2031  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2032 
2033  CheckContextMatch(domain);
2034  CheckContextMatch(v);
2035  return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2036  }
2037 
2049  public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
2050  {
2051  Contract.Requires(f != null);
2052  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2053  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2054 
2055  CheckContextMatch(f);
2056  CheckContextMatch(args);
2057  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2058  }
2059 
2067  public Expr MkTermArray(ArrayExpr array)
2068  {
2069  Contract.Requires(array != null);
2070  Contract.Ensures(Contract.Result<Expr>() != null);
2071 
2072  CheckContextMatch(array);
2073  return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2074  }
2075  #endregion
2076 
2077  #region Sets
2078 
2079 
2080 
2081  public SetSort MkSetSort(Sort ty)
2082  {
2083  Contract.Requires(ty != null);
2084  Contract.Ensures(Contract.Result<SetSort>() != null);
2085 
2086  CheckContextMatch(ty);
2087  return new SetSort(this, ty);
2088  }
2089 
2093  public Expr MkEmptySet(Sort domain)
2094  {
2095  Contract.Requires(domain != null);
2096  Contract.Ensures(Contract.Result<Expr>() != null);
2097 
2098  CheckContextMatch(domain);
2099  return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2100  }
2101 
2105  public Expr MkFullSet(Sort domain)
2106  {
2107  Contract.Requires(domain != null);
2108  Contract.Ensures(Contract.Result<Expr>() != null);
2109 
2110  CheckContextMatch(domain);
2111  return Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2112  }
2113 
2117  public Expr MkSetAdd(Expr set, Expr element)
2118  {
2119  Contract.Requires(set != null);
2120  Contract.Requires(element != null);
2121  Contract.Ensures(Contract.Result<Expr>() != null);
2122 
2123  CheckContextMatch(set);
2124  CheckContextMatch(element);
2125  return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2126  }
2127 
2128 
2132  public Expr MkSetDel(Expr set, Expr element)
2133  {
2134  Contract.Requires(set != null);
2135  Contract.Requires(element != null);
2136  Contract.Ensures(Contract.Result<Expr>() != null);
2137 
2138  CheckContextMatch(set);
2139  CheckContextMatch(element);
2140  return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2141  }
2142 
2146  public Expr MkSetUnion(params Expr[] args)
2147  {
2148  Contract.Requires(args != null);
2149  Contract.Requires(Contract.ForAll(args, a => a != null));
2150 
2151  CheckContextMatch(args);
2152  return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2153  }
2154 
2158  public Expr MkSetIntersection(params Expr[] args)
2159  {
2160  Contract.Requires(args != null);
2161  Contract.Requires(Contract.ForAll(args, a => a != null));
2162  Contract.Ensures(Contract.Result<Expr>() != null);
2163 
2164  CheckContextMatch(args);
2165  return Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2166  }
2167 
2171  public Expr MkSetDifference(Expr arg1, Expr arg2)
2172  {
2173  Contract.Requires(arg1 != null);
2174  Contract.Requires(arg2 != null);
2175  Contract.Ensures(Contract.Result<Expr>() != null);
2176 
2177  CheckContextMatch(arg1);
2178  CheckContextMatch(arg2);
2179  return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2180  }
2181 
2185  public Expr MkSetComplement(Expr arg)
2186  {
2187  Contract.Requires(arg != null);
2188  Contract.Ensures(Contract.Result<Expr>() != null);
2189 
2190  CheckContextMatch(arg);
2191  return Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2192  }
2193 
2197  public Expr MkSetMembership(Expr elem, Expr set)
2198  {
2199  Contract.Requires(elem != null);
2200  Contract.Requires(set != null);
2201  Contract.Ensures(Contract.Result<Expr>() != null);
2202 
2203  CheckContextMatch(elem);
2204  CheckContextMatch(set);
2205  return Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2206  }
2207 
2211  public Expr MkSetSubset(Expr arg1, Expr arg2)
2212  {
2213  Contract.Requires(arg1 != null);
2214  Contract.Requires(arg2 != null);
2215  Contract.Ensures(Contract.Result<Expr>() != null);
2216 
2217  CheckContextMatch(arg1);
2218  CheckContextMatch(arg2);
2219  return Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2220  }
2221  #endregion
2222 
2223  #region Numerals
2224 
2225  #region General Numerals
2226 
2227 
2228 
2229 
2230 
2231 
2232  public Expr MkNumeral(string v, Sort ty)
2233  {
2234  Contract.Requires(ty != null);
2235  Contract.Ensures(Contract.Result<Expr>() != null);
2236 
2237  CheckContextMatch(ty);
2238  return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2239  }
2240 
2248  public Expr MkNumeral(int v, Sort ty)
2249  {
2250  Contract.Requires(ty != null);
2251  Contract.Ensures(Contract.Result<Expr>() != null);
2252 
2253  CheckContextMatch(ty);
2254  return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2255  }
2256 
2264  public Expr MkNumeral(uint v, Sort ty)
2265  {
2266  Contract.Requires(ty != null);
2267  Contract.Ensures(Contract.Result<Expr>() != null);
2268 
2269  CheckContextMatch(ty);
2270  return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2271  }
2272 
2280  public Expr MkNumeral(long v, Sort ty)
2281  {
2282  Contract.Requires(ty != null);
2283  Contract.Ensures(Contract.Result<Expr>() != null);
2284 
2285  CheckContextMatch(ty);
2286  return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2287  }
2288 
2296  public Expr MkNumeral(ulong v, Sort ty)
2297  {
2298  Contract.Requires(ty != null);
2299  Contract.Ensures(Contract.Result<Expr>() != null);
2300 
2301  CheckContextMatch(ty);
2302  return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2303  }
2304  #endregion
2305 
2306  #region Reals
2307 
2308 
2309 
2310 
2311 
2312 
2313 
2314  public RatNum MkReal(int num, int den)
2315  {
2316  if (den == 0)
2317  throw new Z3Exception("Denominator is zero");
2318 
2319  Contract.Ensures(Contract.Result<RatNum>() != null);
2320  Contract.EndContractBlock();
2321 
2322  return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
2323  }
2324 
2330  public RatNum MkReal(string v)
2331  {
2332  Contract.Ensures(Contract.Result<RatNum>() != null);
2333 
2334  return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
2335  }
2336 
2342  public RatNum MkReal(int v)
2343  {
2344  Contract.Ensures(Contract.Result<RatNum>() != null);
2345 
2346  return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
2347  }
2348 
2354  public RatNum MkReal(uint v)
2355  {
2356  Contract.Ensures(Contract.Result<RatNum>() != null);
2357 
2358  return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
2359  }
2360 
2366  public RatNum MkReal(long v)
2367  {
2368  Contract.Ensures(Contract.Result<RatNum>() != null);
2369 
2370  return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
2371  }
2372 
2378  public RatNum MkReal(ulong v)
2379  {
2380  Contract.Ensures(Contract.Result<RatNum>() != null);
2381 
2382  return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
2383  }
2384  #endregion
2385 
2386  #region Integers
2387 
2388 
2389 
2390 
2391  public IntNum MkInt(string v)
2392  {
2393  Contract.Ensures(Contract.Result<IntNum>() != null);
2394 
2395  return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
2396  }
2397 
2403  public IntNum MkInt(int v)
2404  {
2405  Contract.Ensures(Contract.Result<IntNum>() != null);
2406 
2407  return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
2408  }
2409 
2415  public IntNum MkInt(uint v)
2416  {
2417  Contract.Ensures(Contract.Result<IntNum>() != null);
2418 
2419  return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
2420  }
2421 
2427  public IntNum MkInt(long v)
2428  {
2429  Contract.Ensures(Contract.Result<IntNum>() != null);
2430 
2431  return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
2432  }
2433 
2439  public IntNum MkInt(ulong v)
2440  {
2441  Contract.Ensures(Contract.Result<IntNum>() != null);
2442 
2443  return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
2444  }
2445  #endregion
2446 
2447  #region Bit-vectors
2448 
2449 
2450 
2451 
2452 
2453  public BitVecNum MkBV(string v, uint size)
2454  {
2455  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2456 
2457  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2458  }
2459 
2465  public BitVecNum MkBV(int v, uint size)
2466  {
2467  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2468 
2469  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2470  }
2471 
2477  public BitVecNum MkBV(uint v, uint size)
2478  {
2479  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2480 
2481  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2482  }
2483 
2489  public BitVecNum MkBV(long v, uint size)
2490  {
2491  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2492 
2493  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2494  }
2495 
2501  public BitVecNum MkBV(ulong v, uint size)
2502  {
2503  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2504 
2505  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2506  }
2507  #endregion
2508 
2509  #endregion // Numerals
2510 
2511  #region Quantifiers
2512 
2513 
2514 
2515 
2516 
2517 
2518 
2519 
2520 
2521 
2522 
2523 
2524 
2525 
2526 
2527 
2528 
2529 
2530 
2531  public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2532  {
2533  Contract.Requires(sorts != null);
2534  Contract.Requires(names != null);
2535  Contract.Requires(body != null);
2536  Contract.Requires(sorts.Length == names.Length);
2537  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2538  Contract.Requires(Contract.ForAll(names, n => n != null));
2539  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2540  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2541 
2542  Contract.Ensures(Contract.Result<Quantifier>() != null);
2543 
2544  return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2545  }
2546 
2547 
2551  public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2552  {
2553  Contract.Requires(body != null);
2554  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
2555  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2556  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2557 
2558  Contract.Ensures(Contract.Result<Quantifier>() != null);
2559 
2560  return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2561  }
2562 
2567  public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2568  {
2569  Contract.Requires(sorts != null);
2570  Contract.Requires(names != null);
2571  Contract.Requires(body != null);
2572  Contract.Requires(sorts.Length == names.Length);
2573  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2574  Contract.Requires(Contract.ForAll(names, n => n != null));
2575  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2576  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2577  Contract.Ensures(Contract.Result<Quantifier>() != null);
2578 
2579  return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2580  }
2581 
2585  public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2586  {
2587  Contract.Requires(body != null);
2588  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2589  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2590  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2591  Contract.Ensures(Contract.Result<Quantifier>() != null);
2592 
2593  return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2594  }
2595 
2596 
2600  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)
2601  {
2602  Contract.Requires(body != null);
2603  Contract.Requires(names != null);
2604  Contract.Requires(sorts != null);
2605  Contract.Requires(sorts.Length == names.Length);
2606  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2607  Contract.Requires(Contract.ForAll(names, n => n != null));
2608  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2609  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2610 
2611  Contract.Ensures(Contract.Result<Quantifier>() != null);
2612 
2613  if (universal)
2614  return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2615  else
2616  return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2617  }
2618 
2619 
2623  public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2624  {
2625  Contract.Requires(body != null);
2626  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2627  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2628  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2629 
2630  Contract.Ensures(Contract.Result<Quantifier>() != null);
2631 
2632  if (universal)
2633  return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2634  else
2635  return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2636  }
2637 
2638  #endregion
2639 
2640  #endregion // Expr
2641 
2642  #region Options
2643 
2644 
2645 
2646 
2647 
2648 
2649 
2650 
2651 
2652 
2653 
2654 
2655 
2656 
2657 
2658 
2659  public Z3_ast_print_mode PrintMode
2660  {
2661  set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
2662  }
2663  #endregion
2664 
2665  #region SMT Files & Strings
2666 
2667 
2668 
2669 
2670 
2671 
2672 
2673 
2674 
2675 
2676  public string BenchmarkToSMTString(string name, string logic, string status, string attributes,
2677  BoolExpr[] assumptions, BoolExpr formula)
2678  {
2679  Contract.Requires(assumptions != null);
2680  Contract.Requires(formula != null);
2681  Contract.Ensures(Contract.Result<string>() != null);
2682 
2683  return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
2684  (uint)assumptions.Length, AST.ArrayToNative(assumptions),
2685  formula.NativeObject);
2686  }
2687 
2698  public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2699  {
2700  uint csn = Symbol.ArrayLength(sortNames);
2701  uint cs = Sort.ArrayLength(sorts);
2702  uint cdn = Symbol.ArrayLength(declNames);
2703  uint cd = AST.ArrayLength(decls);
2704  if (csn != cs || cdn != cd)
2705  throw new Z3Exception("Argument size mismatch");
2706  Native.Z3_parse_smtlib_string(nCtx, str,
2707  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2708  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2709  }
2710 
2715  public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2716  {
2717  uint csn = Symbol.ArrayLength(sortNames);
2718  uint cs = Sort.ArrayLength(sorts);
2719  uint cdn = Symbol.ArrayLength(declNames);
2720  uint cd = AST.ArrayLength(decls);
2721  if (csn != cs || cdn != cd)
2722  throw new Z3Exception("Argument size mismatch");
2723  Native.Z3_parse_smtlib_file(nCtx, fileName,
2724  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2725  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2726  }
2727 
2731  public uint NumSMTLIBFormulas { get { return Native.Z3_get_smtlib_num_formulas(nCtx); } }
2732 
2736  public BoolExpr[] SMTLIBFormulas
2737  {
2738  get
2739  {
2740  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
2741 
2742  uint n = NumSMTLIBFormulas;
2743  BoolExpr[] res = new BoolExpr[n];
2744  for (uint i = 0; i < n; i++)
2745  res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_formula(nCtx, i));
2746  return res;
2747  }
2748  }
2749 
2753  public uint NumSMTLIBAssumptions { get { return Native.Z3_get_smtlib_num_assumptions(nCtx); } }
2754 
2758  public BoolExpr[] SMTLIBAssumptions
2759  {
2760  get
2761  {
2762  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
2763 
2764  uint n = NumSMTLIBAssumptions;
2765  BoolExpr[] res = new BoolExpr[n];
2766  for (uint i = 0; i < n; i++)
2767  res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_assumption(nCtx, i));
2768  return res;
2769  }
2770  }
2771 
2775  public uint NumSMTLIBDecls { get { return Native.Z3_get_smtlib_num_decls(nCtx); } }
2776 
2780  public FuncDecl[] SMTLIBDecls
2781  {
2782  get
2783  {
2784  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
2785 
2786  uint n = NumSMTLIBDecls;
2787  FuncDecl[] res = new FuncDecl[n];
2788  for (uint i = 0; i < n; i++)
2789  res[i] = new FuncDecl(this, Native.Z3_get_smtlib_decl(nCtx, i));
2790  return res;
2791  }
2792  }
2793 
2797  public uint NumSMTLIBSorts { get { return Native.Z3_get_smtlib_num_sorts(nCtx); } }
2798 
2802  public Sort[] SMTLIBSorts
2803  {
2804  get
2805  {
2806  Contract.Ensures(Contract.Result<Sort[]>() != null);
2807 
2808  uint n = NumSMTLIBSorts;
2809  Sort[] res = new Sort[n];
2810  for (uint i = 0; i < n; i++)
2811  res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i));
2812  return res;
2813  }
2814  }
2815 
2821  public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2822  {
2823  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2824 
2825  uint csn = Symbol.ArrayLength(sortNames);
2826  uint cs = Sort.ArrayLength(sorts);
2827  uint cdn = Symbol.ArrayLength(declNames);
2828  uint cd = AST.ArrayLength(decls);
2829  if (csn != cs || cdn != cd)
2830  throw new Z3Exception("Argument size mismatch");
2831  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
2832  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2833  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2834  }
2835 
2840  public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2841  {
2842  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2843 
2844  uint csn = Symbol.ArrayLength(sortNames);
2845  uint cs = Sort.ArrayLength(sorts);
2846  uint cdn = Symbol.ArrayLength(declNames);
2847  uint cd = AST.ArrayLength(decls);
2848  if (csn != cs || cdn != cd)
2849  throw new Z3Exception("Argument size mismatch");
2850  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
2851  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2852  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2853  }
2854  #endregion
2855 
2856  #region Goals
2857 
2858 
2859 
2860 
2861 
2862 
2863 
2864 
2865 
2866 
2867  public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
2868  {
2869  Contract.Ensures(Contract.Result<Goal>() != null);
2870 
2871  return new Goal(this, models, unsatCores, proofs);
2872  }
2873  #endregion
2874 
2875  #region ParameterSets
2876 
2877 
2878 
2879  public Params MkParams()
2880  {
2881  Contract.Ensures(Contract.Result<Params>() != null);
2882 
2883  return new Params(this);
2884  }
2885  #endregion
2886 
2887  #region Tactics
2888 
2889 
2890 
2891  public uint NumTactics
2892  {
2893  get { return Native.Z3_get_num_tactics(nCtx); }
2894  }
2895 
2899  public string[] TacticNames
2900  {
2901  get
2902  {
2903  Contract.Ensures(Contract.Result<string[]>() != null);
2904 
2905  uint n = NumTactics;
2906  string[] res = new string[n];
2907  for (uint i = 0; i < n; i++)
2908  res[i] = Native.Z3_get_tactic_name(nCtx, i);
2909  return res;
2910  }
2911  }
2912 
2916  public string TacticDescription(string name)
2917  {
2918  Contract.Ensures(Contract.Result<string>() != null);
2919 
2920  return Native.Z3_tactic_get_descr(nCtx, name);
2921  }
2922 
2926  public Tactic MkTactic(string name)
2927  {
2928  Contract.Ensures(Contract.Result<Tactic>() != null);
2929 
2930  return new Tactic(this, name);
2931  }
2932 
2937  public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
2938  {
2939  Contract.Requires(t1 != null);
2940  Contract.Requires(t2 != null);
2941  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
2942  Contract.Ensures(Contract.Result<Tactic>() != null);
2943 
2944 
2945  CheckContextMatch(t1);
2946  CheckContextMatch(t2);
2947  CheckContextMatch(ts);
2948 
2949  IntPtr last = IntPtr.Zero;
2950  if (ts != null && ts.Length > 0)
2951  {
2952  last = ts[ts.Length - 1].NativeObject;
2953  for (int i = ts.Length - 2; i >= 0; i--)
2954  last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
2955  }
2956  if (last != IntPtr.Zero)
2957  {
2958  last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
2959  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
2960  }
2961  else
2962  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
2963  }
2964 
2972  public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
2973  {
2974  Contract.Requires(t1 != null);
2975  Contract.Requires(t2 != null);
2976  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
2977  Contract.Ensures(Contract.Result<Tactic>() != null);
2978 
2979  return AndThen(t1, t2, ts);
2980  }
2981 
2986  public Tactic OrElse(Tactic t1, Tactic t2)
2987  {
2988  Contract.Requires(t1 != null);
2989  Contract.Requires(t2 != null);
2990  Contract.Ensures(Contract.Result<Tactic>() != null);
2991 
2992  CheckContextMatch(t1);
2993  CheckContextMatch(t2);
2994  return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
2995  }
2996 
3003  public Tactic TryFor(Tactic t, uint ms)
3004  {
3005  Contract.Requires(t != null);
3006  Contract.Ensures(Contract.Result<Tactic>() != null);
3007 
3008  CheckContextMatch(t);
3009  return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3010  }
3011 
3019  public Tactic When(Probe p, Tactic t)
3020  {
3021  Contract.Requires(p != null);
3022  Contract.Requires(t != null);
3023  Contract.Ensures(Contract.Result<Tactic>() != null);
3024 
3025  CheckContextMatch(t);
3026  CheckContextMatch(p);
3027  return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3028  }
3029 
3034  public Tactic Cond(Probe p, Tactic t1, Tactic t2)
3035  {
3036  Contract.Requires(p != null);
3037  Contract.Requires(t1 != null);
3038  Contract.Requires(t2 != null);
3039  Contract.Ensures(Contract.Result<Tactic>() != null);
3040 
3041  CheckContextMatch(p);
3042  CheckContextMatch(t1);
3043  CheckContextMatch(t2);
3044  return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3045  }
3046 
3051  public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
3052  {
3053  Contract.Requires(t != null);
3054  Contract.Ensures(Contract.Result<Tactic>() != null);
3055 
3056  CheckContextMatch(t);
3057  return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3058  }
3059 
3063  public Tactic Skip()
3064  {
3065  Contract.Ensures(Contract.Result<Tactic>() != null);
3066 
3067  return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3068  }
3069 
3073  public Tactic Fail()
3074  {
3075  Contract.Ensures(Contract.Result<Tactic>() != null);
3076 
3077  return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3078  }
3079 
3083  public Tactic FailIf(Probe p)
3084  {
3085  Contract.Requires(p != null);
3086  Contract.Ensures(Contract.Result<Tactic>() != null);
3087 
3088  CheckContextMatch(p);
3089  return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3090  }
3091 
3096  public Tactic FailIfNotDecided()
3097  {
3098  Contract.Ensures(Contract.Result<Tactic>() != null);
3099 
3100  return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3101  }
3102 
3106  public Tactic UsingParams(Tactic t, Params p)
3107  {
3108  Contract.Requires(t != null);
3109  Contract.Requires(p != null);
3110  Contract.Ensures(Contract.Result<Tactic>() != null);
3111 
3112  CheckContextMatch(t);
3113  CheckContextMatch(p);
3114  return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3115  }
3116 
3121  public Tactic With(Tactic t, Params p)
3122  {
3123  Contract.Requires(t != null);
3124  Contract.Requires(p != null);
3125  Contract.Ensures(Contract.Result<Tactic>() != null);
3126 
3127  return UsingParams(t, p);
3128  }
3129 
3133  public Tactic ParOr(params Tactic[] t)
3134  {
3135  Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3136  Contract.Ensures(Contract.Result<Tactic>() != null);
3137 
3138  CheckContextMatch(t);
3139  return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
3140  }
3141 
3146  public Tactic ParAndThen(Tactic t1, Tactic t2)
3147  {
3148  Contract.Requires(t1 != null);
3149  Contract.Requires(t2 != null);
3150  Contract.Ensures(Contract.Result<Tactic>() != null);
3151 
3152  CheckContextMatch(t1);
3153  CheckContextMatch(t2);
3154  return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3155  }
3156 
3161  public void Interrupt()
3162  {
3163  Native.Z3_interrupt(nCtx);
3164  }
3165  #endregion
3166 
3167  #region Probes
3168 
3169 
3170 
3171  public uint NumProbes
3172  {
3173  get { return Native.Z3_get_num_probes(nCtx); }
3174  }
3175 
3179  public string[] ProbeNames
3180  {
3181  get
3182  {
3183  Contract.Ensures(Contract.Result<string[]>() != null);
3184 
3185  uint n = NumProbes;
3186  string[] res = new string[n];
3187  for (uint i = 0; i < n; i++)
3188  res[i] = Native.Z3_get_probe_name(nCtx, i);
3189  return res;
3190  }
3191  }
3192 
3196  public string ProbeDescription(string name)
3197  {
3198  Contract.Ensures(Contract.Result<string>() != null);
3199 
3200  return Native.Z3_probe_get_descr(nCtx, name);
3201  }
3202 
3206  public Probe MkProbe(string name)
3207  {
3208  Contract.Ensures(Contract.Result<Probe>() != null);
3209 
3210  return new Probe(this, name);
3211  }
3212 
3216  public Probe Const(double val)
3217  {
3218  Contract.Ensures(Contract.Result<Probe>() != null);
3219 
3220  return new Probe(this, Native.Z3_probe_const(nCtx, val));
3221  }
3222 
3227  public Probe Lt(Probe p1, Probe p2)
3228  {
3229  Contract.Requires(p1 != null);
3230  Contract.Requires(p2 != null);
3231  Contract.Ensures(Contract.Result<Probe>() != null);
3232 
3233  CheckContextMatch(p1);
3234  CheckContextMatch(p2);
3235  return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3236  }
3237 
3242  public Probe Gt(Probe p1, Probe p2)
3243  {
3244  Contract.Requires(p1 != null);
3245  Contract.Requires(p2 != null);
3246  Contract.Ensures(Contract.Result<Probe>() != null);
3247 
3248  CheckContextMatch(p1);
3249  CheckContextMatch(p2);
3250  return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3251  }
3252 
3257  public Probe Le(Probe p1, Probe p2)
3258  {
3259  Contract.Requires(p1 != null);
3260  Contract.Requires(p2 != null);
3261  Contract.Ensures(Contract.Result<Probe>() != null);
3262 
3263  CheckContextMatch(p1);
3264  CheckContextMatch(p2);
3265  return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3266  }
3267 
3272  public Probe Ge(Probe p1, Probe p2)
3273  {
3274  Contract.Requires(p1 != null);
3275  Contract.Requires(p2 != null);
3276  Contract.Ensures(Contract.Result<Probe>() != null);
3277 
3278  CheckContextMatch(p1);
3279  CheckContextMatch(p2);
3280  return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3281  }
3282 
3287  public Probe Eq(Probe p1, Probe p2)
3288  {
3289  Contract.Requires(p1 != null);
3290  Contract.Requires(p2 != null);
3291  Contract.Ensures(Contract.Result<Probe>() != null);
3292 
3293  CheckContextMatch(p1);
3294  CheckContextMatch(p2);
3295  return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3296  }
3297 
3302  public Probe And(Probe p1, Probe p2)
3303  {
3304  Contract.Requires(p1 != null);
3305  Contract.Requires(p2 != null);
3306  Contract.Ensures(Contract.Result<Probe>() != null);
3307 
3308  CheckContextMatch(p1);
3309  CheckContextMatch(p2);
3310  return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3311  }
3312 
3317  public Probe Or(Probe p1, Probe p2)
3318  {
3319  Contract.Requires(p1 != null);
3320  Contract.Requires(p2 != null);
3321  Contract.Ensures(Contract.Result<Probe>() != null);
3322 
3323  CheckContextMatch(p1);
3324  CheckContextMatch(p2);
3325  return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3326  }
3327 
3332  public Probe Not(Probe p)
3333  {
3334  Contract.Requires(p != null);
3335  Contract.Ensures(Contract.Result<Probe>() != null);
3336 
3337  CheckContextMatch(p);
3338  return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3339  }
3340  #endregion
3341 
3342  #region Solvers
3343 
3344 
3345 
3346 
3347 
3348 
3349 
3350 
3351  public Solver MkSolver(Symbol logic = null)
3352  {
3353  Contract.Ensures(Contract.Result<Solver>() != null);
3354 
3355  if (logic == null)
3356  return new Solver(this, Native.Z3_mk_solver(nCtx));
3357  else
3358  return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3359  }
3360 
3365  public Solver MkSolver(string logic)
3366  {
3367  Contract.Ensures(Contract.Result<Solver>() != null);
3368 
3369  return MkSolver(MkSymbol(logic));
3370  }
3371 
3375  public Solver MkSimpleSolver()
3376  {
3377  Contract.Ensures(Contract.Result<Solver>() != null);
3378 
3379  return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3380  }
3381 
3389  public Solver MkSolver(Tactic t)
3390  {
3391  Contract.Requires(t != null);
3392  Contract.Ensures(Contract.Result<Solver>() != null);
3393 
3394  return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3395  }
3396  #endregion
3397 
3398  #region Fixedpoints
3399 
3400 
3401 
3402  public Fixedpoint MkFixedpoint()
3403  {
3404  Contract.Ensures(Contract.Result<Fixedpoint>() != null);
3405 
3406  return new Fixedpoint(this);
3407  }
3408  #endregion
3409 
3410 
3411  #region Miscellaneous
3412 
3413 
3414 
3415 
3416 
3417 
3418 
3419 
3420 
3421 
3422  public AST WrapAST(IntPtr nativeObject)
3423  {
3424  Contract.Ensures(Contract.Result<AST>() != null);
3425  return AST.Create(this, nativeObject);
3426  }
3427 
3439  public IntPtr UnwrapAST(AST a)
3440  {
3441  return a.NativeObject;
3442  }
3443 
3447  public string SimplifyHelp()
3448  {
3449  Contract.Ensures(Contract.Result<string>() != null);
3450 
3451  return Native.Z3_simplify_get_help(nCtx);
3452  }
3453 
3457  public ParamDescrs SimplifyParameterDescriptions
3458  {
3459  get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
3460  }
3461 
3467  public static void ToggleWarningMessages(bool enabled)
3468  {
3469  Native.Z3_toggle_warning_messages((enabled) ? 1 : 0);
3470  }
3471  #endregion
3472 
3473  #region Error Handling
3474 
3475 
3476 
3477 
3478 
3479 
3480 
3481  //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
3482 
3486  //public event ErrorHandler OnError = null;
3487  #endregion
3488 
3489  #region Parameters
3490 
3491 
3492 
3493 
3494 
3495 
3496 
3497 
3498 
3499 
3500  public void UpdateParamValue(string id, string value)
3501  {
3502  Native.Z3_update_param_value(nCtx, id, value);
3503  }
3504 
3512  public string GetParamValue(string id)
3513  {
3514  IntPtr res = IntPtr.Zero;
3515  int r = Native.Z3_get_param_value(nCtx, id, out res);
3516  if (r == (int)Z3_lbool.Z3_L_FALSE)
3517  return null;
3518  else
3519  return Marshal.PtrToStringAnsi(res);
3520  }
3521 
3522  #endregion
3523 
3524  #region Internal
3525  internal IntPtr m_ctx = IntPtr.Zero;
3526  internal Native.Z3_error_handler m_n_err_handler = null;
3527  internal IntPtr nCtx { get { return m_ctx; } }
3528 
3529  internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
3530  {
3531  // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
3532  }
3533 
3534  internal void InitContext()
3535  {
3536  PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
3537  m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
3538  Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
3539  GC.SuppressFinalize(this);
3540  }
3541 
3542  [Pure]
3543  internal void CheckContextMatch(Z3Object other)
3544  {
3545  Contract.Requires(other != null);
3546 
3547  if (!ReferenceEquals(this, other.Context))
3548  throw new Z3Exception("Context mismatch");
3549  }
3550 
3551  [Pure]
3552  internal void CheckContextMatch(Z3Object[] arr)
3553  {
3554  Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
3555 
3556  if (arr != null)
3557  {
3558  foreach (Z3Object a in arr)
3559  {
3560  Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
3561  CheckContextMatch(a);
3562  }
3563  }
3564  }
3565 
3566  [ContractInvariantMethod]
3567  private void ObjectInvariant()
3568  {
3569  Contract.Invariant(m_AST_DRQ != null);
3570  Contract.Invariant(m_ASTMap_DRQ != null);
3571  Contract.Invariant(m_ASTVector_DRQ != null);
3572  Contract.Invariant(m_ApplyResult_DRQ != null);
3573  Contract.Invariant(m_FuncEntry_DRQ != null);
3574  Contract.Invariant(m_FuncInterp_DRQ != null);
3575  Contract.Invariant(m_Goal_DRQ != null);
3576  Contract.Invariant(m_Model_DRQ != null);
3577  Contract.Invariant(m_Params_DRQ != null);
3578  Contract.Invariant(m_ParamDescrs_DRQ != null);
3579  Contract.Invariant(m_Probe_DRQ != null);
3580  Contract.Invariant(m_Solver_DRQ != null);
3581  Contract.Invariant(m_Statistics_DRQ != null);
3582  Contract.Invariant(m_Tactic_DRQ != null);
3583  Contract.Invariant(m_Fixedpoint_DRQ != null);
3584  }
3585 
3586  readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
3587  readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue();
3588  readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue();
3589  readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue();
3590  readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue();
3591  readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue();
3592  readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue();
3593  readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue();
3594  readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue();
3595  readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue();
3596  readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue();
3597  readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue();
3598  readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue();
3599  readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue();
3600  readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue();
3601 
3602  internal AST.DecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result<AST.DecRefQueue>() != null); return m_AST_DRQ; } }
3603  internal ASTMap.DecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null); return m_ASTMap_DRQ; } }
3604  internal ASTVector.DecRefQueue ASTVector_DRQ { get { Contract.Ensures(Contract.Result<ASTVector.DecRefQueue>() != null); return m_ASTVector_DRQ; } }
3605  internal ApplyResult.DecRefQueue ApplyResult_DRQ { get { Contract.Ensures(Contract.Result<ApplyResult.DecRefQueue>() != null); return m_ApplyResult_DRQ; } }
3606  internal FuncInterp.Entry.DecRefQueue FuncEntry_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.Entry.DecRefQueue>() != null); return m_FuncEntry_DRQ; } }
3607  internal FuncInterp.DecRefQueue FuncInterp_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.DecRefQueue>() != null); return m_FuncInterp_DRQ; } }
3608  internal Goal.DecRefQueue Goal_DRQ { get { Contract.Ensures(Contract.Result<Goal.DecRefQueue>() != null); return m_Goal_DRQ; } }
3609  internal Model.DecRefQueue Model_DRQ { get { Contract.Ensures(Contract.Result<Model.DecRefQueue>() != null); return m_Model_DRQ; } }
3610  internal Params.DecRefQueue Params_DRQ { get { Contract.Ensures(Contract.Result<Params.DecRefQueue>() != null); return m_Params_DRQ; } }
3611  internal ParamDescrs.DecRefQueue ParamDescrs_DRQ { get { Contract.Ensures(Contract.Result<ParamDescrs.DecRefQueue>() != null); return m_ParamDescrs_DRQ; } }
3612  internal Probe.DecRefQueue Probe_DRQ { get { Contract.Ensures(Contract.Result<Probe.DecRefQueue>() != null); return m_Probe_DRQ; } }
3613  internal Solver.DecRefQueue Solver_DRQ { get { Contract.Ensures(Contract.Result<Solver.DecRefQueue>() != null); return m_Solver_DRQ; } }
3614  internal Statistics.DecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result<Statistics.DecRefQueue>() != null); return m_Statistics_DRQ; } }
3615  internal Tactic.DecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result<Tactic.DecRefQueue>() != null); return m_Tactic_DRQ; } }
3616  internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
3617 
3618 
3619  internal uint refCount = 0;
3620 
3624  ~Context()
3625  {
3626  // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
3627  Dispose();
3628 
3629  if (refCount == 0)
3630  {
3631  m_n_err_handler = null;
3632  Native.Z3_del_context(m_ctx);
3633  m_ctx = IntPtr.Zero;
3634  }
3635  else
3636  GC.ReRegisterForFinalize(this);
3637  }
3638 
3642  public void Dispose()
3643  {
3644  // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
3645  AST_DRQ.Clear(this);
3646  ASTMap_DRQ.Clear(this);
3647  ASTVector_DRQ.Clear(this);
3648  ApplyResult_DRQ.Clear(this);
3649  FuncEntry_DRQ.Clear(this);
3650  FuncInterp_DRQ.Clear(this);
3651  Goal_DRQ.Clear(this);
3652  Model_DRQ.Clear(this);
3653  Params_DRQ.Clear(this);
3654  Probe_DRQ.Clear(this);
3655  Solver_DRQ.Clear(this);
3656  Statistics_DRQ.Clear(this);
3657  Tactic_DRQ.Clear(this);
3658  Fixedpoint_DRQ.Clear(this);
3659 
3660  m_boolSort = null;
3661  m_intSort = null;
3662  m_realSort = null;
3663  }
3664  #endregion
3665  }
3666 }
Generated on Thu Nov 22 2012 18:37:18 for Z3 by   doxygen 1.8.2