Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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  public Context()
38  : base()
39  {
40  m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
41  InitContext();
42  }
43 
62  public Context(Dictionary<string, string> settings)
63  : base()
64  {
65  Contract.Requires(settings != null);
66 
67  IntPtr cfg = Native.Z3_mk_config();
68  foreach (KeyValuePair<string, string> kv in settings)
69  Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
70  m_ctx = Native.Z3_mk_context_rc(cfg);
71  Native.Z3_del_config(cfg);
72  InitContext();
73  }
74  #endregion
75 
76  #region Symbols
77  public IntSymbol MkSymbol(int i)
85  {
86  Contract.Ensures(Contract.Result<IntSymbol>() != null);
87 
88  return new IntSymbol(this, i);
89  }
90 
94  public StringSymbol MkSymbol(string name)
95  {
96  Contract.Ensures(Contract.Result<StringSymbol>() != null);
97 
98  return new StringSymbol(this, name);
99  }
100 
104  internal Symbol[] MkSymbols(string[] names)
105  {
106  Contract.Ensures(names == null || Contract.Result<Symbol[]>() != null);
107  Contract.Ensures(names != null || Contract.Result<Symbol[]>() == null);
108  Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.Result<Symbol[]>().Length == names.Length);
109  Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.ForAll(Contract.Result<Symbol[]>(), s => s != null));
110 
111  if (names == null) return null;
112  Symbol[] result = new Symbol[names.Length];
113  for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
114  return result;
115  }
116  #endregion
117 
118  #region Sorts
119  private BoolSort m_boolSort = null;
120  private IntSort m_intSort = null;
121  private RealSort m_realSort = null;
122 
126  public BoolSort BoolSort
127  {
128  get
129  {
130  Contract.Ensures(Contract.Result<BoolSort>() != null);
131  if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
132  }
133  }
134 
138  public IntSort IntSort
139  {
140  get
141  {
142  Contract.Ensures(Contract.Result<IntSort>() != null);
143  if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
144  }
145  }
146 
147 
151  public RealSort RealSort
152  {
153  get
154  {
155  Contract.Ensures(Contract.Result<RealSort>() != null);
156  if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
157  }
158  }
159 
164  {
165  Contract.Ensures(Contract.Result<BoolSort>() != null);
166  return new BoolSort(this);
167  }
168 
172  public UninterpretedSort MkUninterpretedSort(Symbol s)
173  {
174  Contract.Requires(s != null);
175  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
176 
177  CheckContextMatch(s);
178  return new UninterpretedSort(this, s);
179  }
180 
184  public UninterpretedSort MkUninterpretedSort(string str)
185  {
186  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
187 
188  return MkUninterpretedSort(MkSymbol(str));
189  }
190 
195  {
196  Contract.Ensures(Contract.Result<IntSort>() != null);
197 
198  return new IntSort(this);
199  }
200 
205  {
206  Contract.Ensures(Contract.Result<RealSort>() != null);
207  return new RealSort(this);
208  }
209 
213  public BitVecSort MkBitVecSort(uint size)
214  {
215  Contract.Ensures(Contract.Result<BitVecSort>() != null);
216 
217  return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
218  }
219 
223  public ArraySort MkArraySort(Sort domain, Sort range)
224  {
225  Contract.Requires(domain != null);
226  Contract.Requires(range != null);
227  Contract.Ensures(Contract.Result<ArraySort>() != null);
228 
229  CheckContextMatch(domain);
230  CheckContextMatch(range);
231  return new ArraySort(this, domain, range);
232  }
233 
237  public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
238  {
239  Contract.Requires(name != null);
240  Contract.Requires(fieldNames != null);
241  Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
242  Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
243  Contract.Ensures(Contract.Result<TupleSort>() != null);
244 
245  CheckContextMatch(name);
246  CheckContextMatch(fieldNames);
247  CheckContextMatch(fieldSorts);
248  return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
249  }
250 
254  public EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
255  {
256  Contract.Requires(name != null);
257  Contract.Requires(enumNames != null);
258  Contract.Requires(Contract.ForAll(enumNames, f => f != null));
259 
260  Contract.Ensures(Contract.Result<EnumSort>() != null);
261 
262  CheckContextMatch(name);
263  CheckContextMatch(enumNames);
264  return new EnumSort(this, name, enumNames);
265  }
266 
270  public EnumSort MkEnumSort(string name, params string[] enumNames)
271  {
272  Contract.Requires(enumNames != null);
273  Contract.Ensures(Contract.Result<EnumSort>() != null);
274 
275  return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
276  }
277 
281  public ListSort MkListSort(Symbol name, Sort elemSort)
282  {
283  Contract.Requires(name != null);
284  Contract.Requires(elemSort != null);
285  Contract.Ensures(Contract.Result<ListSort>() != null);
286 
287  CheckContextMatch(name);
288  CheckContextMatch(elemSort);
289  return new ListSort(this, name, elemSort);
290  }
291 
295  public ListSort MkListSort(string name, Sort elemSort)
296  {
297  Contract.Requires(elemSort != null);
298  Contract.Ensures(Contract.Result<ListSort>() != null);
299 
300  CheckContextMatch(elemSort);
301  return new ListSort(this, MkSymbol(name), elemSort);
302  }
303 
310  public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
311  {
312  Contract.Requires(name != null);
313  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
314 
315  CheckContextMatch(name);
316  return new FiniteDomainSort(this, name, size);
317  }
318 
327  public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
328  {
329  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
330 
331  return new FiniteDomainSort(this, MkSymbol(name), size);
332  }
333 
334 
335  #region Datatypes
336  public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
347  {
348  Contract.Requires(name != null);
349  Contract.Requires(recognizer != null);
350  Contract.Ensures(Contract.Result<Constructor>() != null);
351 
352  return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
353  }
354 
364  public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
365  {
366  Contract.Ensures(Contract.Result<Constructor>() != null);
367 
368  return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
369  }
370 
374  public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
375  {
376  Contract.Requires(name != null);
377  Contract.Requires(constructors != null);
378  Contract.Requires(Contract.ForAll(constructors, c => c != null));
379 
380  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
381 
382  CheckContextMatch(name);
383  CheckContextMatch(constructors);
384  return new DatatypeSort(this, name, constructors);
385  }
386 
390  public DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
391  {
392  Contract.Requires(constructors != null);
393  Contract.Requires(Contract.ForAll(constructors, c => c != null));
394  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
395 
396  CheckContextMatch(constructors);
397  return new DatatypeSort(this, MkSymbol(name), constructors);
398  }
399 
405  public DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
406  {
407  Contract.Requires(names != null);
408  Contract.Requires(c != null);
409  Contract.Requires(names.Length == c.Length);
410  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
411  Contract.Requires(Contract.ForAll(names, name => name != null));
412  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
413 
414  CheckContextMatch(names);
415  uint n = (uint)names.Length;
416  ConstructorList[] cla = new ConstructorList[n];
417  IntPtr[] n_constr = new IntPtr[n];
418  for (uint i = 0; i < n; i++)
419  {
420  Constructor[] constructor = c[i];
421  Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
422  CheckContextMatch(constructor);
423  cla[i] = new ConstructorList(this, constructor);
424  n_constr[i] = cla[i].NativeObject;
425  }
426  IntPtr[] n_res = new IntPtr[n];
427  Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
428  DatatypeSort[] res = new DatatypeSort[n];
429  for (uint i = 0; i < n; i++)
430  res[i] = new DatatypeSort(this, n_res[i]);
431  return res;
432  }
433 
440  public DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
441  {
442  Contract.Requires(names != null);
443  Contract.Requires(c != null);
444  Contract.Requires(names.Length == c.Length);
445  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
446  Contract.Requires(Contract.ForAll(names, name => name != null));
447  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
448 
449  return MkDatatypeSorts(MkSymbols(names), c);
450  }
451 
452  #endregion
453  #endregion
454 
455  #region Function Declarations
456  public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
460  {
461  Contract.Requires(name != null);
462  Contract.Requires(range != null);
463  Contract.Requires(Contract.ForAll(domain, d => d != null));
464  Contract.Ensures(Contract.Result<FuncDecl>() != null);
465 
466  CheckContextMatch(name);
467  CheckContextMatch(domain);
468  CheckContextMatch(range);
469  return new FuncDecl(this, name, domain, range);
470  }
471 
475  public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
476  {
477  Contract.Requires(name != null);
478  Contract.Requires(domain != null);
479  Contract.Requires(range != null);
480  Contract.Ensures(Contract.Result<FuncDecl>() != null);
481 
482  CheckContextMatch(name);
483  CheckContextMatch(domain);
484  CheckContextMatch(range);
485  Sort[] q = new Sort[] { domain };
486  return new FuncDecl(this, name, q, range);
487  }
488 
492  public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
493  {
494  Contract.Requires(range != null);
495  Contract.Requires(Contract.ForAll(domain, d => d != null));
496  Contract.Ensures(Contract.Result<FuncDecl>() != null);
497 
498  CheckContextMatch(domain);
499  CheckContextMatch(range);
500  return new FuncDecl(this, MkSymbol(name), domain, range);
501  }
502 
506  public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
507  {
508  Contract.Requires(range != null);
509  Contract.Requires(domain != null);
510  Contract.Ensures(Contract.Result<FuncDecl>() != null);
511 
512  CheckContextMatch(domain);
513  CheckContextMatch(range);
514  Sort[] q = new Sort[] { domain };
515  return new FuncDecl(this, MkSymbol(name), q, range);
516  }
517 
523  public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
524  {
525  Contract.Requires(range != null);
526  Contract.Requires(Contract.ForAll(domain, d => d != null));
527  Contract.Ensures(Contract.Result<FuncDecl>() != null);
528 
529  CheckContextMatch(domain);
530  CheckContextMatch(range);
531  return new FuncDecl(this, prefix, domain, range);
532  }
533 
537  public FuncDecl MkConstDecl(Symbol name, Sort range)
538  {
539  Contract.Requires(name != null);
540  Contract.Requires(range != null);
541  Contract.Ensures(Contract.Result<FuncDecl>() != null);
542 
543  CheckContextMatch(name);
544  CheckContextMatch(range);
545  return new FuncDecl(this, name, null, range);
546  }
547 
551  public FuncDecl MkConstDecl(string name, Sort range)
552  {
553  Contract.Requires(range != null);
554  Contract.Ensures(Contract.Result<FuncDecl>() != null);
555 
556  CheckContextMatch(range);
557  return new FuncDecl(this, MkSymbol(name), null, range);
558  }
559 
565  public FuncDecl MkFreshConstDecl(string prefix, Sort range)
566  {
567  Contract.Requires(range != null);
568  Contract.Ensures(Contract.Result<FuncDecl>() != null);
569 
570  CheckContextMatch(range);
571  return new FuncDecl(this, prefix, null, range);
572  }
573  #endregion
574 
575  #region Bound Variables
576  public Expr MkBound(uint index, Sort ty)
582  {
583  Contract.Requires(ty != null);
584  Contract.Ensures(Contract.Result<Expr>() != null);
585 
586  return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
587  }
588  #endregion
589 
590  #region Quantifier Patterns
591  public Pattern MkPattern(params Expr[] terms)
595  {
596  Contract.Requires(terms != null);
597  if (terms.Length == 0)
598  throw new Z3Exception("Cannot create a pattern from zero terms");
599 
600  Contract.Ensures(Contract.Result<Pattern>() != null);
601 
602  Contract.EndContractBlock();
603 
604  IntPtr[] termsNative = AST.ArrayToNative(terms);
605  return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
606  }
607  #endregion
608 
609  #region Constants
610  public Expr MkConst(Symbol name, Sort range)
614  {
615  Contract.Requires(name != null);
616  Contract.Requires(range != null);
617  Contract.Ensures(Contract.Result<Expr>() != null);
618 
619  CheckContextMatch(name);
620  CheckContextMatch(range);
621 
622  return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
623  }
624 
628  public Expr MkConst(string name, Sort range)
629  {
630  Contract.Requires(range != null);
631  Contract.Ensures(Contract.Result<Expr>() != null);
632 
633  return MkConst(MkSymbol(name), range);
634  }
635 
640  public Expr MkFreshConst(string prefix, Sort range)
641  {
642  Contract.Requires(range != null);
643  Contract.Ensures(Contract.Result<Expr>() != null);
644 
645  CheckContextMatch(range);
646  return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
647  }
648 
654  {
655  Contract.Requires(f != null);
656  Contract.Ensures(Contract.Result<Expr>() != null);
657 
658  return MkApp(f);
659  }
660 
665  {
666  Contract.Requires(name != null);
667  Contract.Ensures(Contract.Result<BoolExpr>() != null);
668 
669  return (BoolExpr)MkConst(name, BoolSort);
670  }
671 
675  public BoolExpr MkBoolConst(string name)
676  {
677  Contract.Ensures(Contract.Result<BoolExpr>() != null);
678 
679  return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
680  }
681 
685  public IntExpr MkIntConst(Symbol name)
686  {
687  Contract.Requires(name != null);
688  Contract.Ensures(Contract.Result<IntExpr>() != null);
689 
690  return (IntExpr)MkConst(name, IntSort);
691  }
692 
696  public IntExpr MkIntConst(string name)
697  {
698  Contract.Requires(name != null);
699  Contract.Ensures(Contract.Result<IntExpr>() != null);
700 
701  return (IntExpr)MkConst(name, IntSort);
702  }
703 
707  public RealExpr MkRealConst(Symbol name)
708  {
709  Contract.Requires(name != null);
710  Contract.Ensures(Contract.Result<RealExpr>() != null);
711 
712  return (RealExpr)MkConst(name, RealSort);
713  }
714 
718  public RealExpr MkRealConst(string name)
719  {
720  Contract.Ensures(Contract.Result<RealExpr>() != null);
721 
722  return (RealExpr)MkConst(name, RealSort);
723  }
724 
728  public BitVecExpr MkBVConst(Symbol name, uint size)
729  {
730  Contract.Requires(name != null);
731  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
732 
733  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
734  }
735 
739  public BitVecExpr MkBVConst(string name, uint size)
740  {
741  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
742 
743  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
744  }
745  #endregion
746 
747  #region Terms
748  public Expr MkApp(FuncDecl f, params Expr[] args)
752  {
753  Contract.Requires(f != null);
754  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
755  Contract.Ensures(Contract.Result<Expr>() != null);
756 
757  CheckContextMatch(f);
758  CheckContextMatch(args);
759  return Expr.Create(this, f, args);
760  }
761 
762  #region Propositional
763  public BoolExpr MkTrue()
767  {
768  Contract.Ensures(Contract.Result<BoolExpr>() != null);
769 
770  return new BoolExpr(this, Native.Z3_mk_true(nCtx));
771  }
772 
776  public BoolExpr MkFalse()
777  {
778  Contract.Ensures(Contract.Result<BoolExpr>() != null);
779 
780  return new BoolExpr(this, Native.Z3_mk_false(nCtx));
781  }
782 
786  public BoolExpr MkBool(bool value)
787  {
788  Contract.Ensures(Contract.Result<BoolExpr>() != null);
789 
790  return value ? MkTrue() : MkFalse();
791  }
792 
796  public BoolExpr MkEq(Expr x, Expr y)
797  {
798  Contract.Requires(x != null);
799  Contract.Requires(y != null);
800  Contract.Ensures(Contract.Result<BoolExpr>() != null);
801 
802  CheckContextMatch(x);
803  CheckContextMatch(y);
804  return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
805  }
806 
810  public BoolExpr MkDistinct(params Expr[] args)
811  {
812  Contract.Requires(args != null);
813  Contract.Requires(Contract.ForAll(args, a => a != null));
814 
815  Contract.Ensures(Contract.Result<BoolExpr>() != null);
816 
817  CheckContextMatch(args);
818  return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
819  }
820 
825  {
826  Contract.Requires(a != null);
827  Contract.Ensures(Contract.Result<BoolExpr>() != null);
828 
829  CheckContextMatch(a);
830  return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
831  }
832 
839  public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
840  {
841  Contract.Requires(t1 != null);
842  Contract.Requires(t2 != null);
843  Contract.Requires(t3 != null);
844  Contract.Ensures(Contract.Result<Expr>() != null);
845 
846  CheckContextMatch(t1);
847  CheckContextMatch(t2);
848  CheckContextMatch(t3);
849  return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
850  }
851 
856  {
857  Contract.Requires(t1 != null);
858  Contract.Requires(t2 != null);
859  Contract.Ensures(Contract.Result<BoolExpr>() != null);
860 
861  CheckContextMatch(t1);
862  CheckContextMatch(t2);
863  return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
864  }
865 
870  {
871  Contract.Requires(t1 != null);
872  Contract.Requires(t2 != null);
873  Contract.Ensures(Contract.Result<BoolExpr>() != null);
874 
875  CheckContextMatch(t1);
876  CheckContextMatch(t2);
877  return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
878  }
879 
884  {
885  Contract.Requires(t1 != null);
886  Contract.Requires(t2 != null);
887  Contract.Ensures(Contract.Result<BoolExpr>() != null);
888 
889  CheckContextMatch(t1);
890  CheckContextMatch(t2);
891  return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
892  }
893 
897  public BoolExpr MkAnd(params BoolExpr[] t)
898  {
899  Contract.Requires(t != null);
900  Contract.Requires(Contract.ForAll(t, a => a != null));
901  Contract.Ensures(Contract.Result<BoolExpr>() != null);
902 
903  CheckContextMatch(t);
904  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
905  }
906 
910  public BoolExpr MkOr(params BoolExpr[] t)
911  {
912  Contract.Requires(t != null);
913  Contract.Requires(Contract.ForAll(t, a => a != null));
914  Contract.Ensures(Contract.Result<BoolExpr>() != null);
915 
916  CheckContextMatch(t);
917  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
918  }
919 
920 
921  #endregion
922 
923  #region Arithmetic
924  public ArithExpr MkAdd(params ArithExpr[] t)
928  {
929  Contract.Requires(t != null);
930  Contract.Requires(Contract.ForAll(t, a => a != null));
931  Contract.Ensures(Contract.Result<ArithExpr>() != null);
932 
933  CheckContextMatch(t);
934  return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
935  }
936 
940  public ArithExpr MkMul(params ArithExpr[] t)
941  {
942  Contract.Requires(t != null);
943  Contract.Requires(Contract.ForAll(t, a => a != null));
944  Contract.Ensures(Contract.Result<ArithExpr>() != null);
945 
946  CheckContextMatch(t);
947  return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
948  }
949 
953  public ArithExpr MkSub(params ArithExpr[] t)
954  {
955  Contract.Requires(t != null);
956  Contract.Requires(Contract.ForAll(t, a => a != null));
957  Contract.Ensures(Contract.Result<ArithExpr>() != null);
958 
959  CheckContextMatch(t);
960  return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
961  }
962 
966  public ArithExpr MkUnaryMinus(ArithExpr t)
967  {
968  Contract.Requires(t != null);
969  Contract.Ensures(Contract.Result<ArithExpr>() != null);
970 
971  CheckContextMatch(t);
972  return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
973  }
974 
978  public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
979  {
980  Contract.Requires(t1 != null);
981  Contract.Requires(t2 != null);
982  Contract.Ensures(Contract.Result<ArithExpr>() != null);
983 
984  CheckContextMatch(t1);
985  CheckContextMatch(t2);
986  return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
987  }
988 
993  public IntExpr MkMod(IntExpr t1, IntExpr t2)
994  {
995  Contract.Requires(t1 != null);
996  Contract.Requires(t2 != null);
997  Contract.Ensures(Contract.Result<IntExpr>() != null);
998 
999  CheckContextMatch(t1);
1000  CheckContextMatch(t2);
1001  return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1002  }
1003 
1008  public IntExpr MkRem(IntExpr t1, IntExpr t2)
1009  {
1010  Contract.Requires(t1 != null);
1011  Contract.Requires(t2 != null);
1012  Contract.Ensures(Contract.Result<IntExpr>() != null);
1013 
1014  CheckContextMatch(t1);
1015  CheckContextMatch(t2);
1016  return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1017  }
1018 
1022  public ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
1023  {
1024  Contract.Requires(t1 != null);
1025  Contract.Requires(t2 != null);
1026  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1027 
1028  CheckContextMatch(t1);
1029  CheckContextMatch(t2);
1030  return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1031  }
1032 
1036  public BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
1037  {
1038  Contract.Requires(t1 != null);
1039  Contract.Requires(t2 != null);
1040  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1041 
1042  CheckContextMatch(t1);
1043  CheckContextMatch(t2);
1044  return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1045  }
1046 
1050  public BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
1051  {
1052  Contract.Requires(t1 != null);
1053  Contract.Requires(t2 != null);
1054  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1055 
1056  CheckContextMatch(t1);
1057  CheckContextMatch(t2);
1058  return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1059  }
1060 
1064  public BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
1065  {
1066  Contract.Requires(t1 != null);
1067  Contract.Requires(t2 != null);
1068  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1069 
1070  CheckContextMatch(t1);
1071  CheckContextMatch(t2);
1072  return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1073  }
1074 
1078  public BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
1079  {
1080  Contract.Requires(t1 != null);
1081  Contract.Requires(t2 != null);
1082  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1083 
1084  CheckContextMatch(t1);
1085  CheckContextMatch(t2);
1086  return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1087  }
1088 
1099  public RealExpr MkInt2Real(IntExpr t)
1100  {
1101  Contract.Requires(t != null);
1102  Contract.Ensures(Contract.Result<RealExpr>() != null);
1103 
1104  CheckContextMatch(t);
1105  return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1106  }
1107 
1115  public IntExpr MkReal2Int(RealExpr t)
1116  {
1117  Contract.Requires(t != null);
1118  Contract.Ensures(Contract.Result<IntExpr>() != null);
1119 
1120  CheckContextMatch(t);
1121  return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1122  }
1123 
1127  public BoolExpr MkIsInteger(RealExpr t)
1128  {
1129  Contract.Requires(t != null);
1130  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1131 
1132  CheckContextMatch(t);
1133  return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1134  }
1135  #endregion
1136 
1137  #region Bit-vectors
1138  public BitVecExpr MkBVNot(BitVecExpr t)
1143  {
1144  Contract.Requires(t != null);
1145  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1146 
1147  CheckContextMatch(t);
1148  return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1149  }
1150 
1155  public BitVecExpr MkBVRedAND(BitVecExpr t)
1156  {
1157  Contract.Requires(t != null);
1158  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1159 
1160  CheckContextMatch(t);
1161  return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1162  }
1163 
1168  public BitVecExpr MkBVRedOR(BitVecExpr t)
1169  {
1170  Contract.Requires(t != null);
1171  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1172 
1173  CheckContextMatch(t);
1174  return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1175  }
1176 
1181  public BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
1182  {
1183  Contract.Requires(t1 != null);
1184  Contract.Requires(t2 != null);
1185  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1186 
1187  CheckContextMatch(t1);
1188  CheckContextMatch(t2);
1189  return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1190  }
1191 
1196  public BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
1197  {
1198  Contract.Requires(t1 != null);
1199  Contract.Requires(t2 != null);
1200  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1201 
1202  CheckContextMatch(t1);
1203  CheckContextMatch(t2);
1204  return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1205  }
1206 
1211  public BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
1212  {
1213  Contract.Requires(t1 != null);
1214  Contract.Requires(t2 != null);
1215  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1216 
1217  CheckContextMatch(t1);
1218  CheckContextMatch(t2);
1219  return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1220  }
1221 
1226  public BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
1227  {
1228  Contract.Requires(t1 != null);
1229  Contract.Requires(t2 != null);
1230  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1231 
1232  CheckContextMatch(t1);
1233  CheckContextMatch(t2);
1234  return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1235  }
1236 
1241  public BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
1242  {
1243  Contract.Requires(t1 != null);
1244  Contract.Requires(t2 != null);
1245  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1246 
1247  CheckContextMatch(t1);
1248  CheckContextMatch(t2);
1249  return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1250  }
1251 
1256  public BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
1257  {
1258  Contract.Requires(t1 != null);
1259  Contract.Requires(t2 != null);
1260  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1261 
1262  CheckContextMatch(t1);
1263  CheckContextMatch(t2);
1264  return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1265  }
1266 
1271  public BitVecExpr MkBVNeg(BitVecExpr t)
1272  {
1273  Contract.Requires(t != null);
1274  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1275 
1276  CheckContextMatch(t);
1277  return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1278  }
1279 
1284  public BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
1285  {
1286  Contract.Requires(t1 != null);
1287  Contract.Requires(t2 != null);
1288  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1289 
1290  CheckContextMatch(t1);
1291  CheckContextMatch(t2);
1292  return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1293  }
1294 
1299  public BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
1300  {
1301  Contract.Requires(t1 != null);
1302  Contract.Requires(t2 != null);
1303  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1304 
1305  CheckContextMatch(t1);
1306  CheckContextMatch(t2);
1307  return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1308  }
1309 
1314  public BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
1315  {
1316  Contract.Requires(t1 != null);
1317  Contract.Requires(t2 != null);
1318  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1319 
1320  CheckContextMatch(t1);
1321  CheckContextMatch(t2);
1322  return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1323  }
1324 
1334  public BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
1335  {
1336  Contract.Requires(t1 != null);
1337  Contract.Requires(t2 != null);
1338  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1339 
1340  CheckContextMatch(t1);
1341  CheckContextMatch(t2);
1342  return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1343  }
1344 
1358  public BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
1359  {
1360  Contract.Requires(t1 != null);
1361  Contract.Requires(t2 != null);
1362  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1363 
1364  CheckContextMatch(t1);
1365  CheckContextMatch(t2);
1366  return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1367  }
1368 
1377  public BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
1378  {
1379  Contract.Requires(t1 != null);
1380  Contract.Requires(t2 != null);
1381  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1382 
1383  CheckContextMatch(t1);
1384  CheckContextMatch(t2);
1385  return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1386  }
1387 
1398  public BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
1399  {
1400  Contract.Requires(t1 != null);
1401  Contract.Requires(t2 != null);
1402  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1403 
1404  CheckContextMatch(t1);
1405  CheckContextMatch(t2);
1406  return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1407  }
1408 
1416  public BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
1417  {
1418  Contract.Requires(t1 != null);
1419  Contract.Requires(t2 != null);
1420  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1421 
1422  CheckContextMatch(t1);
1423  CheckContextMatch(t2);
1424  return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1425  }
1426 
1433  public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
1434  {
1435  Contract.Requires(t1 != null);
1436  Contract.Requires(t2 != null);
1437  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1438 
1439  CheckContextMatch(t1);
1440  CheckContextMatch(t2);
1441  return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1442  }
1443 
1450  public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
1451  {
1452  Contract.Requires(t1 != null);
1453  Contract.Requires(t2 != null);
1454  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1455 
1456  CheckContextMatch(t1);
1457  CheckContextMatch(t2);
1458  return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1459  }
1460 
1467  public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
1468  {
1469  Contract.Requires(t1 != null);
1470  Contract.Requires(t2 != null);
1471  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1472 
1473  CheckContextMatch(t1);
1474  CheckContextMatch(t2);
1475  return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1476  }
1477 
1484  public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
1485  {
1486  Contract.Requires(t1 != null);
1487  Contract.Requires(t2 != null);
1488  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1489 
1490  CheckContextMatch(t1);
1491  CheckContextMatch(t2);
1492  return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1493  }
1494 
1501  public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
1502  {
1503  Contract.Requires(t1 != null);
1504  Contract.Requires(t2 != null);
1505  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1506 
1507  CheckContextMatch(t1);
1508  CheckContextMatch(t2);
1509  return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1510  }
1511 
1518  public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
1519  {
1520  Contract.Requires(t1 != null);
1521  Contract.Requires(t2 != null);
1522  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1523 
1524  CheckContextMatch(t1);
1525  CheckContextMatch(t2);
1526  return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1527  }
1528 
1535  public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
1536  {
1537  Contract.Requires(t1 != null);
1538  Contract.Requires(t2 != null);
1539  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1540 
1541  CheckContextMatch(t1);
1542  CheckContextMatch(t2);
1543  return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1544  }
1545 
1552  public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
1553  {
1554  Contract.Requires(t1 != null);
1555  Contract.Requires(t2 != null);
1556  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1557 
1558  CheckContextMatch(t1);
1559  CheckContextMatch(t2);
1560  return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1561  }
1562 
1573  public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
1574  {
1575  Contract.Requires(t1 != null);
1576  Contract.Requires(t2 != null);
1577  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1578 
1579  CheckContextMatch(t1);
1580  CheckContextMatch(t2);
1581  return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1582  }
1583 
1593  public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
1594  {
1595  Contract.Requires(t != null);
1596  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1597 
1598  CheckContextMatch(t);
1599  return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1600  }
1601 
1610  public BitVecExpr MkSignExt(uint i, BitVecExpr t)
1611  {
1612  Contract.Requires(t != null);
1613  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1614 
1615  CheckContextMatch(t);
1616  return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1617  }
1618 
1628  public BitVecExpr MkZeroExt(uint i, BitVecExpr t)
1629  {
1630  Contract.Requires(t != null);
1631  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1632 
1633  CheckContextMatch(t);
1634  return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1635  }
1636 
1643  public BitVecExpr MkRepeat(uint i, BitVecExpr t)
1644  {
1645  Contract.Requires(t != null);
1646  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1647 
1648  CheckContextMatch(t);
1649  return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1650  }
1651 
1664  public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
1665  {
1666  Contract.Requires(t1 != null);
1667  Contract.Requires(t2 != null);
1668  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1669 
1670  CheckContextMatch(t1);
1671  CheckContextMatch(t2);
1672  return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1673  }
1674 
1687  public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
1688  {
1689  Contract.Requires(t1 != null);
1690  Contract.Requires(t2 != null);
1691  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1692 
1693  CheckContextMatch(t1);
1694  CheckContextMatch(t2);
1695  return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1696  }
1697 
1712  public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
1713  {
1714  Contract.Requires(t1 != null);
1715  Contract.Requires(t2 != null);
1716  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1717 
1718  CheckContextMatch(t1);
1719  CheckContextMatch(t2);
1720  return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1721  }
1722 
1730  public BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
1731  {
1732  Contract.Requires(t != null);
1733  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1734 
1735  CheckContextMatch(t);
1736  return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1737  }
1738 
1746  public BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
1747  {
1748  Contract.Requires(t != null);
1749  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1750 
1751  CheckContextMatch(t);
1752  return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1753  }
1754 
1762  public BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
1763  {
1764  Contract.Requires(t1 != null);
1765  Contract.Requires(t2 != null);
1766  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1767 
1768  CheckContextMatch(t1);
1769  CheckContextMatch(t2);
1770  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1771  }
1772 
1780  public BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
1781  {
1782  Contract.Requires(t1 != null);
1783  Contract.Requires(t2 != null);
1784  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1785 
1786  CheckContextMatch(t1);
1787  CheckContextMatch(t2);
1788  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1789  }
1790 
1801  public BitVecExpr MkInt2BV(uint n, IntExpr t)
1802  {
1803  Contract.Requires(t != null);
1804  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1805 
1806  CheckContextMatch(t);
1807  return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1808  }
1809 
1825  public IntExpr MkBV2Int(BitVecExpr t, bool signed)
1826  {
1827  Contract.Requires(t != null);
1828  Contract.Ensures(Contract.Result<IntExpr>() != null);
1829 
1830  CheckContextMatch(t);
1831  return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
1832  }
1833 
1840  public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1841  {
1842  Contract.Requires(t1 != null);
1843  Contract.Requires(t2 != null);
1844  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1845 
1846  CheckContextMatch(t1);
1847  CheckContextMatch(t2);
1848  return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1849  }
1850 
1857  public BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
1858  {
1859  Contract.Requires(t1 != null);
1860  Contract.Requires(t2 != null);
1861  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1862 
1863  CheckContextMatch(t1);
1864  CheckContextMatch(t2);
1865  return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1866  }
1867 
1874  public BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
1875  {
1876  Contract.Requires(t1 != null);
1877  Contract.Requires(t2 != null);
1878  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1879 
1880  CheckContextMatch(t1);
1881  CheckContextMatch(t2);
1882  return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1883  }
1884 
1891  public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1892  {
1893  Contract.Requires(t1 != null);
1894  Contract.Requires(t2 != null);
1895  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1896 
1897  CheckContextMatch(t1);
1898  CheckContextMatch(t2);
1899  return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1900  }
1901 
1908  public BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
1909  {
1910  Contract.Requires(t1 != null);
1911  Contract.Requires(t2 != null);
1912  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1913 
1914  CheckContextMatch(t1);
1915  CheckContextMatch(t2);
1916  return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1917  }
1918 
1925  public BoolExpr MkBVNegNoOverflow(BitVecExpr t)
1926  {
1927  Contract.Requires(t != null);
1928  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1929 
1930  CheckContextMatch(t);
1931  return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
1932  }
1933 
1940  public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1941  {
1942  Contract.Requires(t1 != null);
1943  Contract.Requires(t2 != null);
1944  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1945 
1946  CheckContextMatch(t1);
1947  CheckContextMatch(t2);
1948  return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1949  }
1950 
1957  public BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
1958  {
1959  Contract.Requires(t1 != null);
1960  Contract.Requires(t2 != null);
1961  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1962 
1963  CheckContextMatch(t1);
1964  CheckContextMatch(t2);
1965  return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1966  }
1967  #endregion
1968 
1969  #region Arrays
1970  public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
1974  {
1975  Contract.Requires(name != null);
1976  Contract.Requires(domain != null);
1977  Contract.Requires(range != null);
1978  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
1979 
1980  return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
1981  }
1982 
1986  public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
1987  {
1988  Contract.Requires(domain != null);
1989  Contract.Requires(range != null);
1990  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
1991 
1992  return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
1993  }
1994 
2008  public Expr MkSelect(ArrayExpr a, Expr i)
2009  {
2010  Contract.Requires(a != null);
2011  Contract.Requires(i != null);
2012  Contract.Ensures(Contract.Result<Expr>() != null);
2013 
2014  CheckContextMatch(a);
2015  CheckContextMatch(i);
2016  return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2017  }
2018 
2036  public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
2037  {
2038  Contract.Requires(a != null);
2039  Contract.Requires(i != null);
2040  Contract.Requires(v != null);
2041  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2042 
2043  CheckContextMatch(a);
2044  CheckContextMatch(i);
2045  CheckContextMatch(v);
2046  return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2047  }
2048 
2058  public ArrayExpr MkConstArray(Sort domain, Expr v)
2059  {
2060  Contract.Requires(domain != null);
2061  Contract.Requires(v != null);
2062  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2063 
2064  CheckContextMatch(domain);
2065  CheckContextMatch(v);
2066  return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2067  }
2068 
2080  public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
2081  {
2082  Contract.Requires(f != null);
2083  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2084  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2085 
2086  CheckContextMatch(f);
2087  CheckContextMatch(args);
2088  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2089  }
2090 
2098  public Expr MkTermArray(ArrayExpr array)
2099  {
2100  Contract.Requires(array != null);
2101  Contract.Ensures(Contract.Result<Expr>() != null);
2102 
2103  CheckContextMatch(array);
2104  return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2105  }
2106  #endregion
2107 
2108  #region Sets
2109  public SetSort MkSetSort(Sort ty)
2113  {
2114  Contract.Requires(ty != null);
2115  Contract.Ensures(Contract.Result<SetSort>() != null);
2116 
2117  CheckContextMatch(ty);
2118  return new SetSort(this, ty);
2119  }
2120 
2124  public Expr MkEmptySet(Sort domain)
2125  {
2126  Contract.Requires(domain != null);
2127  Contract.Ensures(Contract.Result<Expr>() != null);
2128 
2129  CheckContextMatch(domain);
2130  return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2131  }
2132 
2136  public Expr MkFullSet(Sort domain)
2137  {
2138  Contract.Requires(domain != null);
2139  Contract.Ensures(Contract.Result<Expr>() != null);
2140 
2141  CheckContextMatch(domain);
2142  return Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2143  }
2144 
2148  public Expr MkSetAdd(Expr set, Expr element)
2149  {
2150  Contract.Requires(set != null);
2151  Contract.Requires(element != null);
2152  Contract.Ensures(Contract.Result<Expr>() != null);
2153 
2154  CheckContextMatch(set);
2155  CheckContextMatch(element);
2156  return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2157  }
2158 
2159 
2163  public Expr MkSetDel(Expr set, Expr element)
2164  {
2165  Contract.Requires(set != null);
2166  Contract.Requires(element != null);
2167  Contract.Ensures(Contract.Result<Expr>() != null);
2168 
2169  CheckContextMatch(set);
2170  CheckContextMatch(element);
2171  return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2172  }
2173 
2177  public Expr MkSetUnion(params Expr[] args)
2178  {
2179  Contract.Requires(args != null);
2180  Contract.Requires(Contract.ForAll(args, a => a != null));
2181 
2182  CheckContextMatch(args);
2183  return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2184  }
2185 
2189  public Expr MkSetIntersection(params Expr[] args)
2190  {
2191  Contract.Requires(args != null);
2192  Contract.Requires(Contract.ForAll(args, a => a != null));
2193  Contract.Ensures(Contract.Result<Expr>() != null);
2194 
2195  CheckContextMatch(args);
2196  return Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2197  }
2198 
2202  public Expr MkSetDifference(Expr arg1, Expr arg2)
2203  {
2204  Contract.Requires(arg1 != null);
2205  Contract.Requires(arg2 != null);
2206  Contract.Ensures(Contract.Result<Expr>() != null);
2207 
2208  CheckContextMatch(arg1);
2209  CheckContextMatch(arg2);
2210  return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2211  }
2212 
2217  {
2218  Contract.Requires(arg != null);
2219  Contract.Ensures(Contract.Result<Expr>() != null);
2220 
2221  CheckContextMatch(arg);
2222  return Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2223  }
2224 
2228  public Expr MkSetMembership(Expr elem, Expr set)
2229  {
2230  Contract.Requires(elem != null);
2231  Contract.Requires(set != null);
2232  Contract.Ensures(Contract.Result<Expr>() != null);
2233 
2234  CheckContextMatch(elem);
2235  CheckContextMatch(set);
2236  return Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2237  }
2238 
2242  public Expr MkSetSubset(Expr arg1, Expr arg2)
2243  {
2244  Contract.Requires(arg1 != null);
2245  Contract.Requires(arg2 != null);
2246  Contract.Ensures(Contract.Result<Expr>() != null);
2247 
2248  CheckContextMatch(arg1);
2249  CheckContextMatch(arg2);
2250  return Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2251  }
2252  #endregion
2253 
2254  #region Numerals
2255 
2256  #region General Numerals
2257  public Expr MkNumeral(string v, Sort ty)
2264  {
2265  Contract.Requires(ty != null);
2266  Contract.Ensures(Contract.Result<Expr>() != null);
2267 
2268  CheckContextMatch(ty);
2269  return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2270  }
2271 
2279  public Expr MkNumeral(int v, Sort ty)
2280  {
2281  Contract.Requires(ty != null);
2282  Contract.Ensures(Contract.Result<Expr>() != null);
2283 
2284  CheckContextMatch(ty);
2285  return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2286  }
2287 
2295  public Expr MkNumeral(uint v, Sort ty)
2296  {
2297  Contract.Requires(ty != null);
2298  Contract.Ensures(Contract.Result<Expr>() != null);
2299 
2300  CheckContextMatch(ty);
2301  return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2302  }
2303 
2311  public Expr MkNumeral(long v, Sort ty)
2312  {
2313  Contract.Requires(ty != null);
2314  Contract.Ensures(Contract.Result<Expr>() != null);
2315 
2316  CheckContextMatch(ty);
2317  return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2318  }
2319 
2327  public Expr MkNumeral(ulong v, Sort ty)
2328  {
2329  Contract.Requires(ty != null);
2330  Contract.Ensures(Contract.Result<Expr>() != null);
2331 
2332  CheckContextMatch(ty);
2333  return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2334  }
2335  #endregion
2336 
2337  #region Reals
2338  public RatNum MkReal(int num, int den)
2346  {
2347  if (den == 0)
2348  throw new Z3Exception("Denominator is zero");
2349 
2350  Contract.Ensures(Contract.Result<RatNum>() != null);
2351  Contract.EndContractBlock();
2352 
2353  return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
2354  }
2355 
2361  public RatNum MkReal(string v)
2362  {
2363  Contract.Ensures(Contract.Result<RatNum>() != null);
2364 
2365  return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
2366  }
2367 
2373  public RatNum MkReal(int v)
2374  {
2375  Contract.Ensures(Contract.Result<RatNum>() != null);
2376 
2377  return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
2378  }
2379 
2385  public RatNum MkReal(uint v)
2386  {
2387  Contract.Ensures(Contract.Result<RatNum>() != null);
2388 
2389  return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
2390  }
2391 
2397  public RatNum MkReal(long v)
2398  {
2399  Contract.Ensures(Contract.Result<RatNum>() != null);
2400 
2401  return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
2402  }
2403 
2409  public RatNum MkReal(ulong v)
2410  {
2411  Contract.Ensures(Contract.Result<RatNum>() != null);
2412 
2413  return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
2414  }
2415  #endregion
2416 
2417  #region Integers
2418  public IntNum MkInt(string v)
2423  {
2424  Contract.Ensures(Contract.Result<IntNum>() != null);
2425 
2426  return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
2427  }
2428 
2434  public IntNum MkInt(int v)
2435  {
2436  Contract.Ensures(Contract.Result<IntNum>() != null);
2437 
2438  return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
2439  }
2440 
2446  public IntNum MkInt(uint v)
2447  {
2448  Contract.Ensures(Contract.Result<IntNum>() != null);
2449 
2450  return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
2451  }
2452 
2458  public IntNum MkInt(long v)
2459  {
2460  Contract.Ensures(Contract.Result<IntNum>() != null);
2461 
2462  return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
2463  }
2464 
2470  public IntNum MkInt(ulong v)
2471  {
2472  Contract.Ensures(Contract.Result<IntNum>() != null);
2473 
2474  return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
2475  }
2476  #endregion
2477 
2478  #region Bit-vectors
2479  public BitVecNum MkBV(string v, uint size)
2485  {
2486  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2487 
2488  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2489  }
2490 
2496  public BitVecNum MkBV(int v, uint size)
2497  {
2498  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2499 
2500  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2501  }
2502 
2508  public BitVecNum MkBV(uint v, uint size)
2509  {
2510  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2511 
2512  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2513  }
2514 
2520  public BitVecNum MkBV(long v, uint size)
2521  {
2522  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2523 
2524  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2525  }
2526 
2532  public BitVecNum MkBV(ulong v, uint size)
2533  {
2534  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2535 
2536  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2537  }
2538  #endregion
2539 
2540  #endregion // Numerals
2541 
2542  #region Quantifiers
2543  public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2563  {
2564  Contract.Requires(sorts != null);
2565  Contract.Requires(names != null);
2566  Contract.Requires(body != null);
2567  Contract.Requires(sorts.Length == names.Length);
2568  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2569  Contract.Requires(Contract.ForAll(names, n => n != null));
2570  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2571  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2572 
2573  Contract.Ensures(Contract.Result<Quantifier>() != null);
2574 
2575  return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2576  }
2577 
2578 
2582  public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2583  {
2584  Contract.Requires(body != null);
2585  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
2586  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2587  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2588 
2589  Contract.Ensures(Contract.Result<Quantifier>() != null);
2590 
2591  return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2592  }
2593 
2598  public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2599  {
2600  Contract.Requires(sorts != null);
2601  Contract.Requires(names != null);
2602  Contract.Requires(body != null);
2603  Contract.Requires(sorts.Length == names.Length);
2604  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2605  Contract.Requires(Contract.ForAll(names, n => n != null));
2606  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2607  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2608  Contract.Ensures(Contract.Result<Quantifier>() != null);
2609 
2610  return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2611  }
2612 
2616  public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2617  {
2618  Contract.Requires(body != null);
2619  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2620  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2621  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2622  Contract.Ensures(Contract.Result<Quantifier>() != null);
2623 
2624  return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2625  }
2626 
2627 
2631  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)
2632  {
2633  Contract.Requires(body != null);
2634  Contract.Requires(names != null);
2635  Contract.Requires(sorts != null);
2636  Contract.Requires(sorts.Length == names.Length);
2637  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2638  Contract.Requires(Contract.ForAll(names, n => n != null));
2639  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2640  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2641 
2642  Contract.Ensures(Contract.Result<Quantifier>() != null);
2643 
2644  if (universal)
2645  return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2646  else
2647  return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2648  }
2649 
2650 
2654  public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2655  {
2656  Contract.Requires(body != null);
2657  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2658  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2659  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2660 
2661  Contract.Ensures(Contract.Result<Quantifier>() != null);
2662 
2663  if (universal)
2664  return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2665  else
2666  return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2667  }
2668 
2669  #endregion
2670 
2671  #endregion // Expr
2672 
2673  #region Options
2674  public Z3_ast_print_mode PrintMode
2691  {
2692  set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
2693  }
2694  #endregion
2695 
2696  #region SMT Files & Strings
2697  public string BenchmarkToSMTString(string name, string logic, string status, string attributes,
2708  BoolExpr[] assumptions, BoolExpr formula)
2709  {
2710  Contract.Requires(assumptions != null);
2711  Contract.Requires(formula != null);
2712  Contract.Ensures(Contract.Result<string>() != null);
2713 
2714  return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
2715  (uint)assumptions.Length, AST.ArrayToNative(assumptions),
2716  formula.NativeObject);
2717  }
2718 
2729  public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2730  {
2731  uint csn = Symbol.ArrayLength(sortNames);
2732  uint cs = Sort.ArrayLength(sorts);
2733  uint cdn = Symbol.ArrayLength(declNames);
2734  uint cd = AST.ArrayLength(decls);
2735  if (csn != cs || cdn != cd)
2736  throw new Z3Exception("Argument size mismatch");
2737  Native.Z3_parse_smtlib_string(nCtx, str,
2738  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2739  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2740  }
2741 
2746  public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2747  {
2748  uint csn = Symbol.ArrayLength(sortNames);
2749  uint cs = Sort.ArrayLength(sorts);
2750  uint cdn = Symbol.ArrayLength(declNames);
2751  uint cd = AST.ArrayLength(decls);
2752  if (csn != cs || cdn != cd)
2753  throw new Z3Exception("Argument size mismatch");
2754  Native.Z3_parse_smtlib_file(nCtx, fileName,
2755  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2756  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2757  }
2758 
2762  public uint NumSMTLIBFormulas { get { return Native.Z3_get_smtlib_num_formulas(nCtx); } }
2763 
2767  public BoolExpr[] SMTLIBFormulas
2768  {
2769  get
2770  {
2771  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
2772 
2773  uint n = NumSMTLIBFormulas;
2774  BoolExpr[] res = new BoolExpr[n];
2775  for (uint i = 0; i < n; i++)
2776  res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_formula(nCtx, i));
2777  return res;
2778  }
2779  }
2780 
2784  public uint NumSMTLIBAssumptions { get { return Native.Z3_get_smtlib_num_assumptions(nCtx); } }
2785 
2789  public BoolExpr[] SMTLIBAssumptions
2790  {
2791  get
2792  {
2793  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
2794 
2795  uint n = NumSMTLIBAssumptions;
2796  BoolExpr[] res = new BoolExpr[n];
2797  for (uint i = 0; i < n; i++)
2798  res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_assumption(nCtx, i));
2799  return res;
2800  }
2801  }
2802 
2806  public uint NumSMTLIBDecls { get { return Native.Z3_get_smtlib_num_decls(nCtx); } }
2807 
2811  public FuncDecl[] SMTLIBDecls
2812  {
2813  get
2814  {
2815  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
2816 
2817  uint n = NumSMTLIBDecls;
2818  FuncDecl[] res = new FuncDecl[n];
2819  for (uint i = 0; i < n; i++)
2820  res[i] = new FuncDecl(this, Native.Z3_get_smtlib_decl(nCtx, i));
2821  return res;
2822  }
2823  }
2824 
2828  public uint NumSMTLIBSorts { get { return Native.Z3_get_smtlib_num_sorts(nCtx); } }
2829 
2833  public Sort[] SMTLIBSorts
2834  {
2835  get
2836  {
2837  Contract.Ensures(Contract.Result<Sort[]>() != null);
2838 
2839  uint n = NumSMTLIBSorts;
2840  Sort[] res = new Sort[n];
2841  for (uint i = 0; i < n; i++)
2842  res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i));
2843  return res;
2844  }
2845  }
2846 
2852  public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2853  {
2854  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2855 
2856  uint csn = Symbol.ArrayLength(sortNames);
2857  uint cs = Sort.ArrayLength(sorts);
2858  uint cdn = Symbol.ArrayLength(declNames);
2859  uint cd = AST.ArrayLength(decls);
2860  if (csn != cs || cdn != cd)
2861  throw new Z3Exception("Argument size mismatch");
2862  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
2863  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2864  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2865  }
2866 
2871  public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2872  {
2873  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2874 
2875  uint csn = Symbol.ArrayLength(sortNames);
2876  uint cs = Sort.ArrayLength(sorts);
2877  uint cdn = Symbol.ArrayLength(declNames);
2878  uint cd = AST.ArrayLength(decls);
2879  if (csn != cs || cdn != cd)
2880  throw new Z3Exception("Argument size mismatch");
2881  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
2882  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2883  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2884  }
2885  #endregion
2886 
2887  #region Goals
2888  public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
2899  {
2900  Contract.Ensures(Contract.Result<Goal>() != null);
2901 
2902  return new Goal(this, models, unsatCores, proofs);
2903  }
2904  #endregion
2905 
2906  #region ParameterSets
2907  public Params MkParams()
2911  {
2912  Contract.Ensures(Contract.Result<Params>() != null);
2913 
2914  return new Params(this);
2915  }
2916  #endregion
2917 
2918  #region Tactics
2919  public uint NumTactics
2923  {
2924  get { return Native.Z3_get_num_tactics(nCtx); }
2925  }
2926 
2930  public string[] TacticNames
2931  {
2932  get
2933  {
2934  Contract.Ensures(Contract.Result<string[]>() != null);
2935 
2936  uint n = NumTactics;
2937  string[] res = new string[n];
2938  for (uint i = 0; i < n; i++)
2939  res[i] = Native.Z3_get_tactic_name(nCtx, i);
2940  return res;
2941  }
2942  }
2943 
2947  public string TacticDescription(string name)
2948  {
2949  Contract.Ensures(Contract.Result<string>() != null);
2950 
2951  return Native.Z3_tactic_get_descr(nCtx, name);
2952  }
2953 
2957  public Tactic MkTactic(string name)
2958  {
2959  Contract.Ensures(Contract.Result<Tactic>() != null);
2960 
2961  return new Tactic(this, name);
2962  }
2963 
2968  public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
2969  {
2970  Contract.Requires(t1 != null);
2971  Contract.Requires(t2 != null);
2972  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
2973  Contract.Ensures(Contract.Result<Tactic>() != null);
2974 
2975 
2976  CheckContextMatch(t1);
2977  CheckContextMatch(t2);
2978  CheckContextMatch(ts);
2979 
2980  IntPtr last = IntPtr.Zero;
2981  if (ts != null && ts.Length > 0)
2982  {
2983  last = ts[ts.Length - 1].NativeObject;
2984  for (int i = ts.Length - 2; i >= 0; i--)
2985  last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
2986  }
2987  if (last != IntPtr.Zero)
2988  {
2989  last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
2990  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
2991  }
2992  else
2993  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
2994  }
2995 
3003  public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
3004  {
3005  Contract.Requires(t1 != null);
3006  Contract.Requires(t2 != null);
3007  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3008  Contract.Ensures(Contract.Result<Tactic>() != null);
3009 
3010  return AndThen(t1, t2, ts);
3011  }
3012 
3017  public Tactic OrElse(Tactic t1, Tactic t2)
3018  {
3019  Contract.Requires(t1 != null);
3020  Contract.Requires(t2 != null);
3021  Contract.Ensures(Contract.Result<Tactic>() != null);
3022 
3023  CheckContextMatch(t1);
3024  CheckContextMatch(t2);
3025  return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3026  }
3027 
3034  public Tactic TryFor(Tactic t, uint ms)
3035  {
3036  Contract.Requires(t != null);
3037  Contract.Ensures(Contract.Result<Tactic>() != null);
3038 
3039  CheckContextMatch(t);
3040  return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3041  }
3042 
3050  public Tactic When(Probe p, Tactic t)
3051  {
3052  Contract.Requires(p != null);
3053  Contract.Requires(t != null);
3054  Contract.Ensures(Contract.Result<Tactic>() != null);
3055 
3056  CheckContextMatch(t);
3057  CheckContextMatch(p);
3058  return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3059  }
3060 
3065  public Tactic Cond(Probe p, Tactic t1, Tactic t2)
3066  {
3067  Contract.Requires(p != null);
3068  Contract.Requires(t1 != null);
3069  Contract.Requires(t2 != null);
3070  Contract.Ensures(Contract.Result<Tactic>() != null);
3071 
3072  CheckContextMatch(p);
3073  CheckContextMatch(t1);
3074  CheckContextMatch(t2);
3075  return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3076  }
3077 
3082  public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
3083  {
3084  Contract.Requires(t != null);
3085  Contract.Ensures(Contract.Result<Tactic>() != null);
3086 
3087  CheckContextMatch(t);
3088  return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3089  }
3090 
3094  public Tactic Skip()
3095  {
3096  Contract.Ensures(Contract.Result<Tactic>() != null);
3097 
3098  return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3099  }
3100 
3104  public Tactic Fail()
3105  {
3106  Contract.Ensures(Contract.Result<Tactic>() != null);
3107 
3108  return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3109  }
3110 
3114  public Tactic FailIf(Probe p)
3115  {
3116  Contract.Requires(p != null);
3117  Contract.Ensures(Contract.Result<Tactic>() != null);
3118 
3119  CheckContextMatch(p);
3120  return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3121  }
3122 
3128  {
3129  Contract.Ensures(Contract.Result<Tactic>() != null);
3130 
3131  return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3132  }
3133 
3138  {
3139  Contract.Requires(t != null);
3140  Contract.Requires(p != null);
3141  Contract.Ensures(Contract.Result<Tactic>() != null);
3142 
3143  CheckContextMatch(t);
3144  CheckContextMatch(p);
3145  return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3146  }
3147 
3152  public Tactic With(Tactic t, Params p)
3153  {
3154  Contract.Requires(t != null);
3155  Contract.Requires(p != null);
3156  Contract.Ensures(Contract.Result<Tactic>() != null);
3157 
3158  return UsingParams(t, p);
3159  }
3160 
3164  public Tactic ParOr(params Tactic[] t)
3165  {
3166  Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3167  Contract.Ensures(Contract.Result<Tactic>() != null);
3168 
3169  CheckContextMatch(t);
3170  return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
3171  }
3172 
3178  {
3179  Contract.Requires(t1 != null);
3180  Contract.Requires(t2 != null);
3181  Contract.Ensures(Contract.Result<Tactic>() != null);
3182 
3183  CheckContextMatch(t1);
3184  CheckContextMatch(t2);
3185  return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3186  }
3187 
3192  public void Interrupt()
3193  {
3194  Native.Z3_interrupt(nCtx);
3195  }
3196  #endregion
3197 
3198  #region Probes
3199  public uint NumProbes
3203  {
3204  get { return Native.Z3_get_num_probes(nCtx); }
3205  }
3206 
3210  public string[] ProbeNames
3211  {
3212  get
3213  {
3214  Contract.Ensures(Contract.Result<string[]>() != null);
3215 
3216  uint n = NumProbes;
3217  string[] res = new string[n];
3218  for (uint i = 0; i < n; i++)
3219  res[i] = Native.Z3_get_probe_name(nCtx, i);
3220  return res;
3221  }
3222  }
3223 
3227  public string ProbeDescription(string name)
3228  {
3229  Contract.Ensures(Contract.Result<string>() != null);
3230 
3231  return Native.Z3_probe_get_descr(nCtx, name);
3232  }
3233 
3237  public Probe MkProbe(string name)
3238  {
3239  Contract.Ensures(Contract.Result<Probe>() != null);
3240 
3241  return new Probe(this, name);
3242  }
3243 
3247  public Probe ConstProbe(double val)
3248  {
3249  Contract.Ensures(Contract.Result<Probe>() != null);
3250 
3251  return new Probe(this, Native.Z3_probe_const(nCtx, val));
3252  }
3253 
3258  public Probe Lt(Probe p1, Probe p2)
3259  {
3260  Contract.Requires(p1 != null);
3261  Contract.Requires(p2 != null);
3262  Contract.Ensures(Contract.Result<Probe>() != null);
3263 
3264  CheckContextMatch(p1);
3265  CheckContextMatch(p2);
3266  return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3267  }
3268 
3273  public Probe Gt(Probe p1, Probe p2)
3274  {
3275  Contract.Requires(p1 != null);
3276  Contract.Requires(p2 != null);
3277  Contract.Ensures(Contract.Result<Probe>() != null);
3278 
3279  CheckContextMatch(p1);
3280  CheckContextMatch(p2);
3281  return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3282  }
3283 
3288  public Probe Le(Probe p1, Probe p2)
3289  {
3290  Contract.Requires(p1 != null);
3291  Contract.Requires(p2 != null);
3292  Contract.Ensures(Contract.Result<Probe>() != null);
3293 
3294  CheckContextMatch(p1);
3295  CheckContextMatch(p2);
3296  return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3297  }
3298 
3303  public Probe Ge(Probe p1, Probe p2)
3304  {
3305  Contract.Requires(p1 != null);
3306  Contract.Requires(p2 != null);
3307  Contract.Ensures(Contract.Result<Probe>() != null);
3308 
3309  CheckContextMatch(p1);
3310  CheckContextMatch(p2);
3311  return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3312  }
3313 
3318  public Probe Eq(Probe p1, Probe p2)
3319  {
3320  Contract.Requires(p1 != null);
3321  Contract.Requires(p2 != null);
3322  Contract.Ensures(Contract.Result<Probe>() != null);
3323 
3324  CheckContextMatch(p1);
3325  CheckContextMatch(p2);
3326  return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3327  }
3328 
3333  public Probe And(Probe p1, Probe p2)
3334  {
3335  Contract.Requires(p1 != null);
3336  Contract.Requires(p2 != null);
3337  Contract.Ensures(Contract.Result<Probe>() != null);
3338 
3339  CheckContextMatch(p1);
3340  CheckContextMatch(p2);
3341  return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3342  }
3343 
3348  public Probe Or(Probe p1, Probe p2)
3349  {
3350  Contract.Requires(p1 != null);
3351  Contract.Requires(p2 != null);
3352  Contract.Ensures(Contract.Result<Probe>() != null);
3353 
3354  CheckContextMatch(p1);
3355  CheckContextMatch(p2);
3356  return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3357  }
3358 
3363  public Probe Not(Probe p)
3364  {
3365  Contract.Requires(p != null);
3366  Contract.Ensures(Contract.Result<Probe>() != null);
3367 
3368  CheckContextMatch(p);
3369  return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3370  }
3371  #endregion
3372 
3373  #region Solvers
3374  public Solver MkSolver(Symbol logic = null)
3383  {
3384  Contract.Ensures(Contract.Result<Solver>() != null);
3385 
3386  if (logic == null)
3387  return new Solver(this, Native.Z3_mk_solver(nCtx));
3388  else
3389  return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3390  }
3391 
3396  public Solver MkSolver(string logic)
3397  {
3398  Contract.Ensures(Contract.Result<Solver>() != null);
3399 
3400  return MkSolver(MkSymbol(logic));
3401  }
3402 
3407  {
3408  Contract.Ensures(Contract.Result<Solver>() != null);
3409 
3410  return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3411  }
3412 
3421  {
3422  Contract.Requires(t != null);
3423  Contract.Ensures(Contract.Result<Solver>() != null);
3424 
3425  return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3426  }
3427  #endregion
3428 
3429  #region Fixedpoints
3430  public Fixedpoint MkFixedpoint()
3434  {
3435  Contract.Ensures(Contract.Result<Fixedpoint>() != null);
3436 
3437  return new Fixedpoint(this);
3438  }
3439  #endregion
3440 
3441 
3442  #region Miscellaneous
3443  public AST WrapAST(IntPtr nativeObject)
3454  {
3455  Contract.Ensures(Contract.Result<AST>() != null);
3456  return AST.Create(this, nativeObject);
3457  }
3458 
3470  public IntPtr UnwrapAST(AST a)
3471  {
3472  return a.NativeObject;
3473  }
3474 
3478  public string SimplifyHelp()
3479  {
3480  Contract.Ensures(Contract.Result<string>() != null);
3481 
3482  return Native.Z3_simplify_get_help(nCtx);
3483  }
3484 
3488  public ParamDescrs SimplifyParameterDescriptions
3489  {
3490  get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
3491  }
3492 
3498  public static void ToggleWarningMessages(bool enabled)
3499  {
3500  Native.Z3_toggle_warning_messages((enabled) ? 1 : 0);
3501  }
3502  #endregion
3503 
3504  #region Error Handling
3505  //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
3513 
3517  //public event ErrorHandler OnError = null;
3518  #endregion
3519 
3520  #region Parameters
3521  public void UpdateParamValue(string id, string value)
3531  {
3532  Native.Z3_update_param_value(nCtx, id, value);
3533  }
3534 
3535  #endregion
3536 
3537  #region Internal
3538  internal IntPtr m_ctx = IntPtr.Zero;
3539  internal Native.Z3_error_handler m_n_err_handler = null;
3540  internal IntPtr nCtx { get { return m_ctx; } }
3541 
3542  internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
3543  {
3544  // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
3545  }
3546 
3547  internal void InitContext()
3548  {
3549  PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
3550  m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
3551  Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
3552  GC.SuppressFinalize(this);
3553  }
3554 
3555  [Pure]
3556  internal void CheckContextMatch(Z3Object other)
3557  {
3558  Contract.Requires(other != null);
3559 
3560  if (!ReferenceEquals(this, other.Context))
3561  throw new Z3Exception("Context mismatch");
3562  }
3563 
3564  [Pure]
3565  internal void CheckContextMatch(Z3Object[] arr)
3566  {
3567  Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
3568 
3569  if (arr != null)
3570  {
3571  foreach (Z3Object a in arr)
3572  {
3573  Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
3574  CheckContextMatch(a);
3575  }
3576  }
3577  }
3578 
3579  [ContractInvariantMethod]
3580  private void ObjectInvariant()
3581  {
3582  Contract.Invariant(m_AST_DRQ != null);
3583  Contract.Invariant(m_ASTMap_DRQ != null);
3584  Contract.Invariant(m_ASTVector_DRQ != null);
3585  Contract.Invariant(m_ApplyResult_DRQ != null);
3586  Contract.Invariant(m_FuncEntry_DRQ != null);
3587  Contract.Invariant(m_FuncInterp_DRQ != null);
3588  Contract.Invariant(m_Goal_DRQ != null);
3589  Contract.Invariant(m_Model_DRQ != null);
3590  Contract.Invariant(m_Params_DRQ != null);
3591  Contract.Invariant(m_ParamDescrs_DRQ != null);
3592  Contract.Invariant(m_Probe_DRQ != null);
3593  Contract.Invariant(m_Solver_DRQ != null);
3594  Contract.Invariant(m_Statistics_DRQ != null);
3595  Contract.Invariant(m_Tactic_DRQ != null);
3596  Contract.Invariant(m_Fixedpoint_DRQ != null);
3597  }
3598 
3599  readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
3600  readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue();
3601  readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue();
3602  readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue();
3603  readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue();
3604  readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue();
3605  readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue();
3606  readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue();
3607  readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue();
3608  readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue();
3609  readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue();
3610  readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue();
3611  readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue();
3612  readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue();
3613  readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue();
3614 
3615  internal AST.DecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result<AST.DecRefQueue>() != null); return m_AST_DRQ; } }
3616  internal ASTMap.DecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null); return m_ASTMap_DRQ; } }
3617  internal ASTVector.DecRefQueue ASTVector_DRQ { get { Contract.Ensures(Contract.Result<ASTVector.DecRefQueue>() != null); return m_ASTVector_DRQ; } }
3618  internal ApplyResult.DecRefQueue ApplyResult_DRQ { get { Contract.Ensures(Contract.Result<ApplyResult.DecRefQueue>() != null); return m_ApplyResult_DRQ; } }
3619  internal FuncInterp.Entry.DecRefQueue FuncEntry_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.Entry.DecRefQueue>() != null); return m_FuncEntry_DRQ; } }
3620  internal FuncInterp.DecRefQueue FuncInterp_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.DecRefQueue>() != null); return m_FuncInterp_DRQ; } }
3621  internal Goal.DecRefQueue Goal_DRQ { get { Contract.Ensures(Contract.Result<Goal.DecRefQueue>() != null); return m_Goal_DRQ; } }
3622  internal Model.DecRefQueue Model_DRQ { get { Contract.Ensures(Contract.Result<Model.DecRefQueue>() != null); return m_Model_DRQ; } }
3623  internal Params.DecRefQueue Params_DRQ { get { Contract.Ensures(Contract.Result<Params.DecRefQueue>() != null); return m_Params_DRQ; } }
3624  internal ParamDescrs.DecRefQueue ParamDescrs_DRQ { get { Contract.Ensures(Contract.Result<ParamDescrs.DecRefQueue>() != null); return m_ParamDescrs_DRQ; } }
3625  internal Probe.DecRefQueue Probe_DRQ { get { Contract.Ensures(Contract.Result<Probe.DecRefQueue>() != null); return m_Probe_DRQ; } }
3626  internal Solver.DecRefQueue Solver_DRQ { get { Contract.Ensures(Contract.Result<Solver.DecRefQueue>() != null); return m_Solver_DRQ; } }
3627  internal Statistics.DecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result<Statistics.DecRefQueue>() != null); return m_Statistics_DRQ; } }
3628  internal Tactic.DecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result<Tactic.DecRefQueue>() != null); return m_Tactic_DRQ; } }
3629  internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
3630 
3631 
3632  internal long refCount = 0;
3633 
3637  ~Context()
3638  {
3639  // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
3640  Dispose();
3641 
3642  if (refCount == 0)
3643  {
3644  m_n_err_handler = null;
3645  Native.Z3_del_context(m_ctx);
3646  m_ctx = IntPtr.Zero;
3647  }
3648  else
3649  GC.ReRegisterForFinalize(this);
3650  }
3651 
3655  public void Dispose()
3656  {
3657  // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
3658  AST_DRQ.Clear(this);
3659  ASTMap_DRQ.Clear(this);
3660  ASTVector_DRQ.Clear(this);
3661  ApplyResult_DRQ.Clear(this);
3662  FuncEntry_DRQ.Clear(this);
3663  FuncInterp_DRQ.Clear(this);
3664  Goal_DRQ.Clear(this);
3665  Model_DRQ.Clear(this);
3666  Params_DRQ.Clear(this);
3667  ParamDescrs_DRQ.Clear(this);
3668  Probe_DRQ.Clear(this);
3669  Solver_DRQ.Clear(this);
3670  Statistics_DRQ.Clear(this);
3671  Tactic_DRQ.Clear(this);
3672  Fixedpoint_DRQ.Clear(this);
3673 
3674  m_boolSort = null;
3675  m_intSort = null;
3676  m_realSort = null;
3677  }
3678  #endregion
3679  }
3680 }
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:897
static Z3_ast Z3_mk_bvmul(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2350
static Z3_solver Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1)
Definition: Native.cs:4879
BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
Two's complement signed remainder (sign follows divisor).
Definition: Context.cs:1416
string SimplifyHelp()
Return a string describing all available parameters to Expr.Simplify.
Definition: Context.cs:3478
static Z3_ast Z3_mk_bvadd_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Definition: Native.cs:2574
static string Z3_get_tactic_name(Z3_context a0, uint a1)
Definition: Native.cs:4729
def RealSort
Definition: z3py.py:2630
static Z3_tactic Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Definition: Native.cs:4553
static Z3_ast Z3_get_smtlib_formula(Z3_context a0, uint a1)
Definition: Native.cs:3918
static Z3_ast Z3_mk_bvneg_no_overflow(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2614
BoolExpr MkIsInteger(RealExpr t)
Creates an expression that checks whether a real number is an integer.
Definition: Context.cs:1127
static Z3_tactic Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Definition: Native.cs:4569
Expr MkSetMembership(Expr elem, Expr set)
Check for set membership.
Definition: Context.cs:2228
static Z3_ast Z3_mk_real2int(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2238
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
Bitwise conjunction.
Definition: Context.cs:1181
static Z3_ast Z3_mk_set_intersect(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2726
static Z3_ast Z3_mk_bvuge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2430
DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
Create a new datatype sort.
Definition: Context.cs:374
Expr MkNumeral(uint v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
Definition: Context.cs:2295
static Z3_ast Z3_mk_mul(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2142
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:2957
static Z3_ast Z3_mk_mod(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2174
UninterpretedSort MkUninterpretedSort(string str)
Create a new uninterpreted sort.
Definition: Context.cs:184
FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
Create a new finite domain sort.
Definition: Context.cs:310
def IntSort
Definition: z3py.py:2614
static Z3_ast Z3_mk_empty_set(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2686
def BoolSort
Definition: z3py.py:1325
ArrayExpr MkConstArray(Sort domain, Expr v)
Create a constant array.
Definition: Context.cs:2058
string ProbeDescription(string name)
Returns a string containing a description of the probe with the given name.
Definition: Context.cs:3227
BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
Unsigned greater than or equal to.
Definition: Context.cs:1501
RatNum MkReal(string v)
Create a real numeral.
Definition: Context.cs:2361
Expr MkFreshConst(string prefix, Sort range)
Creates a fresh Constant of sort range and a name prefixed with prefix .
Definition: Context.cs:640
static Z3_tactic Z3_tactic_par_or(Z3_context a0, uint a1, [In] Z3_tactic[] a2)
Definition: Native.cs:4561
static Z3_ast Z3_mk_bvashr(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2518
static void Z3_parse_smtlib_string(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
Definition: Native.cs:3896
def BitVecSort
Definition: z3py.py:3435
static Z3_ast Z3_mk_bv2int(Z3_context a0, Z3_ast a1, int a2)
Definition: Native.cs:2566
static string Z3_tactic_get_descr(Z3_context a0, string a1)
Definition: Native.cs:4769
BitVecNum MkBV(long v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2520
Probe Not(Probe p)
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
Definition: Context.cs:3363
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Unsigned division.
Definition: Context.cs:1334
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:3050
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:3082
BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater than or equal to.
Definition: Context.cs:1518
static Z3_probe Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4705
BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
Bit-vector extraction.
Definition: Context.cs:1593
static Z3_ast Z3_mk_fresh_const(Z3_context a0, string a1, Z3_sort a2)
Definition: Native.cs:2038
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:3303
IntExpr MkIntConst(Symbol name)
Creates an integer constant.
Definition: Context.cs:685
static uint Z3_get_num_probes(Z3_context a0)
Definition: Native.cs:4737
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:2852
static Z3_ast Z3_mk_bvmul_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2630
static Z3_ast Z3_mk_bvshl(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2502
IntNum MkInt(int v)
Create an integer numeral.
Definition: Context.cs:2434
Tactic ParOr(params Tactic[] t)
Create a tactic that applies the given tactics in parallel.
Definition: Context.cs:3164
BitVecExpr MkBVNeg(BitVecExpr t)
Standard two's complement unary minus.
Definition: Context.cs:1271
static Z3_probe Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4673
def ArraySort
Definition: z3py.py:3955
ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
Maps f on the argument arrays.
Definition: Context.cs:2080
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_mk_real(Z3_context a0, int a1, int a2)
Definition: Native.cs:2774
void Interrupt()
Interrupt the execution of a Z3 procedure.
Definition: Context.cs:3192
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:3288
static Z3_tactic Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3)
Definition: Native.cs:4593
Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
Create an expression representing an if-then-else: ite(t1, t2, t3).
Definition: Context.cs:839
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:2598
Expr MkNumeral(ulong v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
Definition: Context.cs:2327
static Z3_ast Z3_mk_or(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2126
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
Definition: Probe.cs:34
FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
Create a new finite domain sort.
Definition: Context.cs:327
Expr MkConst(string name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:628
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
Definition: Context.cs:978
FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:506
BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
Unsigned greater-than.
Definition: Context.cs:1535
static Z3_probe Z3_probe_eq(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4689
BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than or equal to.
Definition: Context.cs:1467
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
Definition: Context.cs:1036
static Z3_ast Z3_mk_bvredand(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2262
BoolExpr MkBoolConst(Symbol name)
Create a Boolean constant.
Definition: Context.cs:664
IntNum MkInt(uint v)
Create an integer numeral.
Definition: Context.cs:2446
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:2968
void ParseSMTLIBString(string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
Parse the given string using the SMT-LIB parser.
Definition: Context.cs:2729
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:2616
BoolExpr MkEq(Expr x, Expr y)
Creates the equality x = y .
Definition: Context.cs:796
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:3333
static Z3_tactic Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, uint a2)
Definition: Native.cs:4577
Expr MkSetAdd(Expr set, Expr element)
Add an element to the set.
Definition: Context.cs:2148
static Z3_tactic Z3_tactic_fail(Z3_context a0)
Definition: Native.cs:4617
Expr MkEmptySet(Sort domain)
Create an empty set.
Definition: Context.cs:2124
static Z3_ast Z3_mk_implies(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2102
ListSort MkListSort(Symbol name, Sort elemSort)
Create a new list sort.
Definition: Context.cs:281
static Z3_solver Z3_mk_solver(Z3_context a0)
Definition: Native.cs:4855
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
Definition: Context.cs:1050
DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
Create mutually recursive data-types.
Definition: Context.cs:440
static string Z3_simplify_get_help(Z3_context a0)
Definition: Native.cs:3558
static Z3_ast Z3_mk_set_add(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2702
Tactics are the basic building block for creating custom solvers for specific problem domains...
Definition: Tactic.cs:32
Expr MkSetDifference(Expr arg1, Expr arg2)
Take the difference between two sets.
Definition: Context.cs:2202
static Z3_ast Z3_mk_zero_ext(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2486
static Z3_ast Z3_mk_le(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2206
static Z3_probe Z3_probe_const(Z3_context a0, double a1)
Definition: Native.cs:4649
static Z3_ast Z3_mk_set_subset(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2758
FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
Creates a fresh function declaration with a name prefixed with prefix .
Definition: Context.cs:523
BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise subtraction does not overflow.
Definition: Context.cs:1874
BoolExpr MkBoolConst(string name)
Create a Boolean constant.
Definition: Context.cs:675
BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise signed division does not overflow.
Definition: Context.cs:1908
FuncDecl MkFreshConstDecl(string prefix, Sort range)
Creates a fresh constant function declaration with a name prefixed with prefix .
Definition: Context.cs:565
FuncDecl MkConstDecl(Symbol name, Sort range)
Creates a new constant function declaration.
Definition: Context.cs:537
static Z3_ast Z3_mk_bvudiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2358
Solver MkSolver(string logic)
Creates a new (incremental) solver.
Definition: Context.cs:3396
BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Rotate Right.
Definition: Context.cs:1780
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:3258
Expr MkNumeral(long v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
Definition: Context.cs:2311
static Z3_ast Z3_mk_is_int(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2246
RatNum MkReal(int v)
Create a real numeral.
Definition: Context.cs:2373
static Z3_ast Z3_mk_not(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2078
FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:475
Expr MkSetComplement(Expr arg)
Take the complement of a set.
Definition: Context.cs:2216
static Z3_ast Z3_mk_bvredor(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2270
DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
Create a new datatype sort.
Definition: Context.cs:390
static void Z3_interrupt(Z3_context a0)
Definition: Native.cs:1740
BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XNOR.
Definition: Context.cs:1256
BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Rotate Left.
Definition: Context.cs:1762
BitVecExpr MkBVRedAND(BitVecExpr t)
Take conjunction of bits in a vector, return vector of length 1.
Definition: Context.cs:1155
static Z3_ast Z3_mk_bvand(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2278
BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than
Definition: Context.cs:1450
static Z3_ast Z3_mk_sub(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2150
Expressions are terms.
Definition: Expr.cs:29
static Z3_func_decl Z3_get_smtlib_decl(Z3_context a0, uint a1)
Definition: Native.cs:3950
RealExpr MkRealConst(string name)
Creates a real constant.
Definition: Context.cs:718
static Z3_sort Z3_mk_bv_sort(Z3_context a0, uint a1)
Definition: Native.cs:1906
Expr MkSetIntersection(params Expr[] args)
Take the intersection of a list of sets.
Definition: Context.cs:2189
RealSort MkRealSort()
Create a real sort.
Definition: Context.cs:204
Expr MkSetUnion(params Expr[] args)
Take the union of a list of sets.
Definition: Context.cs:2177
static string Z3_probe_get_descr(Z3_context a0, string a1)
Definition: Native.cs:4777
def AndThen
Definition: z3py.py:6537
BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise NOR.
Definition: Context.cs:1241
static void Z3_set_ast_print_mode(Z3_context a0, uint a1)
Definition: Native.cs:3825
string TacticDescription(string name)
Returns a string containing a description of the tactic with the given name.
Definition: Context.cs:2947
Expr MkNumeral(int v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
Definition: Context.cs:2279
Expr MkSetDel(Expr set, Expr element)
Remove an element from a set.
Definition: Context.cs:2163
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3137
static string Z3_get_probe_name(Z3_context a0, uint a1)
Definition: Native.cs:4745
static Z3_ast Z3_mk_sign_ext(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2478
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
Definition: Context.cs:953
FuncDecl MkConstDecl(string name, Sort range)
Creates a new constant function declaration.
Definition: Context.cs:551
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:3177
BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
Two's complement addition.
Definition: Context.cs:1284
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:213
BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Signed division.
Definition: Context.cs:1358
Solver MkSolver(Tactic t)
Creates a solver that is implemented using the given tactic.
Definition: Context.cs:3420
ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
Create an array constant.
Definition: Context.cs:1986
static Z3_ast Z3_mk_bvsrem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2382
StringSymbol MkSymbol(string name)
Create a symbol using a string.
Definition: Context.cs:94
static Z3_ast Z3_parse_smtlib2_string(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
Definition: Native.cs:3880
static Z3_ast Z3_mk_repeat(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2494
BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XOR.
Definition: Context.cs:1211
BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Logical shift right
Definition: Context.cs:1687
BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise subtraction does not underflow.
Definition: Context.cs:1891
BitVecExpr MkSignExt(uint i, BitVecExpr t)
Bit-vector sign extension.
Definition: Context.cs:1610
static Z3_ast Z3_mk_unsigned_int(Z3_context a0, uint a1, Z3_sort a2)
Definition: Native.cs:2790
static Z3_ast Z3_mk_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2062
static Z3_ast Z3_mk_bvxnor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2318
static Z3_context Z3_mk_context_rc(Z3_config a0)
Definition: Native.cs:1708
static Z3_ast Z3_mk_bvadd_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2582
static Z3_ast Z3_mk_set_del(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2710
static Z3_ast Z3_mk_ext_rotate_left(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2542
static string Z3_benchmark_to_smtlib_string(Z3_context a0, string a1, string a2, string a3, string a4, uint a5, [In] Z3_ast[] a6, Z3_ast a7)
Definition: Native.cs:3872
static Z3_ast Z3_mk_bvsdiv_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2606
BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise addition does not underflow.
Definition: Context.cs:1857
static Z3_ast Z3_mk_bvule(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2414
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
Definition: Context.cs:910
static Z3_ast Z3_mk_bvslt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2406
static Z3_ast Z3_mk_power(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2190
static Z3_ast Z3_mk_bvmul_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Definition: Native.cs:2622
BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater-than.
Definition: Context.cs:1552
static Z3_ast Z3_mk_const_array(Z3_context a0, Z3_sort a1, Z3_ast a2)
Definition: Native.cs:2654
static Z3_ast Z3_mk_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2214
BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise multiplication does not overflow.
Definition: Context.cs:1940
static Z3_ast Z3_mk_xor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2110
Constructors are used for datatype sorts.
Definition: Constructor.cs:29
Probe MkProbe(string name)
Creates a new Probe.
Definition: Context.cs:3237
static Z3_ast Z3_mk_ite(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:2086
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
Shift left.
Definition: Context.cs:1664
static Z3_ast Z3_mk_bvadd(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2334
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
Bitwise disjunction.
Definition: Context.cs:1196
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition: z3_api.h:1121
static void Z3_parse_smtlib_file(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
Definition: Native.cs:3903
BitVecExpr MkBVConst(Symbol name, uint size)
Creates a bit-vector constant.
Definition: Context.cs:728
static Z3_ast Z3_mk_iff(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2094
static Z3_ast Z3_mk_and(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2118
static Z3_ast Z3_mk_unsigned_int64(Z3_context a0, UInt64 a1, Z3_sort a2)
Definition: Native.cs:2806
static Z3_ast Z3_mk_distinct(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2070
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:3017
static Z3_ast Z3_mk_select(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2638
static Z3_ast Z3_mk_int2bv(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2558
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition: Context.cs:223
static Z3_param_descrs Z3_simplify_get_param_descrs(Z3_context a0)
Definition: Native.cs:3566
static Z3_tactic Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Definition: Native.cs:4545
BoolSort MkBoolSort()
Create a new Boolean sort.
Definition: Context.cs:163
BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
Arithmetic shift right
Definition: Context.cs:1712
BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than or equal to.
Definition: Context.cs:1484
static Z3_ast Z3_mk_false(Z3_context a0)
Definition: Native.cs:2054
BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
Rotate Right.
Definition: Context.cs:1746
static Z3_ast Z3_mk_bound(Z3_context a0, uint a1, Z3_sort a2)
Definition: Native.cs:2822
EnumSort MkEnumSort(string name, params string[] enumNames)
Create a new enumeration sort.
Definition: Context.cs:270
static Z3_ast Z3_mk_bvnor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2310
static Z3_probe Z3_probe_not(Z3_context a0, Z3_probe a1)
Definition: Native.cs:4713
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 -> t2.
Definition: Context.cs:869
static Z3_tactic Z3_tactic_fail_if(Z3_context a0, Z3_probe a1)
Definition: Native.cs:4625
static Z3_ast Z3_mk_bvsgt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2454
static Z3_probe Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4681
BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise multiplication does not underflow.
Definition: Context.cs:1957
static Z3_ast Z3_mk_bvxor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2294
def EnumSort
Definition: z3py.py:4398
static uint Z3_get_smtlib_num_decls(Z3_context a0)
Definition: Native.cs:3942
BitVecExpr MkRepeat(uint i, BitVecExpr t)
Bit-vector repetition.
Definition: Context.cs:1643
Constructor MkConstructor(string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
Create a datatype constructor.
Definition: Context.cs:364
static Z3_ast Z3_mk_unary_minus(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2158
Expr MkSetSubset(Expr arg1, Expr arg2)
Check for subsetness of sets.
Definition: Context.cs:2242
static Z3_ast Z3_mk_set_member(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2750
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:3348
static Z3_ast Z3_mk_bvlshr(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2510
static Z3_ast Z3_mk_add(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2134
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
Definition: Context.cs:940
static void Z3_mk_datatypes(Z3_context a0, uint a1, [In] IntPtr[] a2, [Out] Z3_sort[] a3, [In, Out] Z3_constructor_list[] a4)
Definition: Native.cs:1992
A ParameterSet represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
ListSort MkListSort(string name, Sort elemSort)
Create a new list sort.
Definition: Context.cs:295
static Z3_ast Z3_mk_full_set(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2694
BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise addition does not overflow.
Definition: Context.cs:1840
static Z3_tactic Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2)
Definition: Native.cs:4585
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:2654
static Z3_ast Z3_mk_set_difference(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2734
Quantifier expressions.
Definition: Quantifier.cs:29
static Z3_ast Z3_mk_bvnot(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2254
BitVecNum MkBV(int v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2496
static void Z3_del_config(Z3_config a0)
Definition: Native.cs:1693
static Z3_config Z3_mk_config()
Definition: Native.cs:1688
static Z3_ast Z3_mk_bvsub(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2342
static Z3_ast Z3_mk_bvsge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2438
BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than
Definition: Context.cs:1433
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition: Context.cs:883
static Z3_ast Z3_mk_store(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:2646
BoolExpr MkBVNegNoOverflow(BitVecExpr t)
Create a predicate that checks that the bit-wise negation does not overflow.
Definition: Context.cs:1925
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:3318
BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
Bit-vector concatenation.
Definition: Context.cs:1573
static Z3_ast Z3_mk_ext_rotate_right(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2550
RealExpr MkInt2Real(IntExpr t)
Coerce an integer to a real.
Definition: Context.cs:1099
static void ToggleWarningMessages(bool enabled)
Enable/disable printing of warning messages to the console.
Definition: Context.cs:3498
IntExpr MkIntConst(string name)
Creates an integer constant.
Definition: Context.cs:696
static Z3_ast Z3_mk_rem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2182
static Z3_ast Z3_mk_ge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2222
static Z3_tactic Z3_tactic_fail_if_not_decided(Z3_context a0)
Definition: Native.cs:4633
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
Definition: Pattern.cs:32
EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
Create a new enumeration sort.
Definition: Context.cs:254
static Z3_solver Z3_mk_simple_solver(Z3_context a0)
Definition: Native.cs:4863
Tactic FailIf(Probe p)
Create a tactic that fails if the probe p evaluates to false.
Definition: Context.cs:3114
BitVecNum MkBV(uint v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2508
BitVecExpr MkBVRedOR(BitVecExpr t)
Take disjunction of bits in a vector, return vector of length 1.
Definition: Context.cs:1168
TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Create a new tuple sort.
Definition: Context.cs:237
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:2582
static Z3_sort Z3_get_smtlib_sort(Z3_context a0, uint a1)
Definition: Native.cs:3966
static Z3_ast Z3_mk_bvult(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2398
static Z3_tactic Z3_tactic_skip(Z3_context a0)
Definition: Native.cs:4609
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 iff t2.
Definition: Context.cs:855
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
static uint Z3_get_num_tactics(Z3_context a0)
Definition: Native.cs:4721
static Z3_ast Z3_mk_bvsub_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Definition: Native.cs:2598
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:3003
static Z3_ast Z3_mk_bvurem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2374
static Z3_ast Z3_mk_bvsdiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2366
BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
Signed remainder.
Definition: Context.cs:1398
static Z3_probe Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4697
Tactic Fail()
Create a tactic always fails.
Definition: Context.cs:3104
BitVecExpr MkInt2BV(uint n, IntExpr t)
Create an n bit bit-vector from the integer argument t .
Definition: Context.cs:1801
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
BoolExpr MkNot(BoolExpr a)
Mk an expression representing not(a).
Definition: Context.cs:824
static uint Z3_get_smtlib_num_formulas(Z3_context a0)
Definition: Native.cs:3910
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
Definition: Context.cs:966
static Z3_ast Z3_mk_bvsmod(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2390
static Z3_ast Z3_mk_rotate_right(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2534
ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 ^ t2.
Definition: Context.cs:1022
static Z3_ast Z3_mk_bvsle(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2422
static Z3_ast Z3_mk_int2real(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2230
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
static Z3_ast Z3_mk_rotate_left(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2526
static Z3_probe Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4665
Expr MkTermArray(ArrayExpr array)
Access the array default value.
Definition: Context.cs:2098
RatNum MkReal(ulong v)
Create a real numeral.
Definition: Context.cs:2409
ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
Array update.
Definition: Context.cs:2036
Tactic With(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3152
The abstract syntax tree (AST) class.
Definition: AST.cs:31
static uint Z3_get_smtlib_num_sorts(Z3_context a0)
Definition: Native.cs:3958
static Z3_ast Z3_mk_bvugt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2446
RealExpr MkRealConst(Symbol name)
Creates a real constant.
Definition: Context.cs:707
static Z3_ast Z3_mk_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2198
IntNum MkInt(ulong v)
Create an integer numeral.
Definition: Context.cs:2470
IntPtr UnwrapAST(AST a)
Unwraps an AST.
Definition: Context.cs:3470
static Z3_ast Z3_mk_int(Z3_context a0, int a1, Z3_sort a2)
Definition: Native.cs:2782
Probe ConstProbe(double val)
Create a probe that always evaluates to val .
Definition: Context.cs:3247
static void Z3_update_param_value(Z3_context a0, string a1, string a2)
Definition: Native.cs:1733
IntExpr MkBV2Int(BitVecExpr t, bool signed)
Create an integer from the bit-vector argument t .
Definition: Context.cs:1825
BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
Unsigned remainder.
Definition: Context.cs:1377
RatNum MkReal(long v)
Create a real numeral.
Definition: Context.cs:2397
Expr MkFullSet(Sort domain)
Create the full set.
Definition: Context.cs:2136
IntNum MkInt(long v)
Create an integer numeral.
Definition: Context.cs:2458
Expr MkSelect(ArrayExpr a, Expr i)
Array read.
Definition: Context.cs:2008
static Z3_tactic Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, uint a2)
Definition: Native.cs:4601
void ParseSMTLIBFile(string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
Parse the given file using the SMT-LIB parser.
Definition: Context.cs:2746
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:3065
static Z3_ast Z3_mk_set_union(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2718
Tactic FailIfNotDecided()
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatis...
Definition: Context.cs:3127
Z3_ast_print_mode
Z3_ast_print_mode
static Z3_ast Z3_mk_array_default(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2670
static Z3_ast Z3_mk_bvnand(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2302
BoolExpr MkFalse()
The false Term.
Definition: Context.cs:776
Tactic TryFor(Tactic t, uint ms)
Create a tactic that applies t to a goal for ms milliseconds.
Definition: Context.cs:3034
BitVecExpr MkBVConst(string name, uint size)
Creates a bit-vector constant.
Definition: Context.cs:739
BitVecNum MkBV(ulong v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2532
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:3273
IntExpr MkRem(IntExpr t1, IntExpr t2)
Create an expression representing t1 rem t2.
Definition: Context.cs:1008
static Z3_ast Z3_mk_int64(Z3_context a0, Int64 a1, Z3_sort a2)
Definition: Native.cs:2798
Tactic Skip()
Create a tactic that just returns the given goal.
Definition: Context.cs:3094
static Z3_ast Z3_mk_numeral(Z3_context a0, string a1, Z3_sort a2)
Definition: Native.cs:2766
static void Z3_toggle_warning_messages(int a0)
Definition: Native.cs:3821
IntExpr MkReal2Int(RealExpr t)
Coerce a real to an integer.
Definition: Context.cs:1115
static Z3_ast Z3_mk_bvneg(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2326
static Z3_ast Z3_mk_set_complement(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2742
static Z3_tactic Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2)
Definition: Native.cs:4641
BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
Two's complement subtraction.
Definition: Context.cs:1299
void Dispose()
Disposes of the context.
Definition: Context.cs:3655
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
Definition: Context.cs:810
FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:492
static uint Z3_get_smtlib_num_assumptions(Z3_context a0)
Definition: Native.cs:3926
Context(Dictionary< string, string > settings)
Constructor.
Definition: Context.cs:62
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:2631
BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
Bitwise NAND.
Definition: Context.cs:1226
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
static Z3_ast Z3_mk_concat(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2462
static Z3_solver Z3_mk_solver_for_logic(Z3_context a0, IntPtr a1)
Definition: Native.cs:4871
Function declarations.
Definition: FuncDecl.cs:29
Solver MkSimpleSolver()
Creates a new (incremental) solver.
Definition: Context.cs:3406
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition: Context.cs:405
BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
Two's complement multiplication.
Definition: Context.cs:1314
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
Definition: Context.cs:1078
static Z3_ast Z3_mk_div(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2166
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
Definition: Context.cs:172
Solvers.
Definition: Solver.cs:29
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
Definition: Context.cs:1064
IntExpr MkMod(IntExpr t1, IntExpr t2)
Create an expression representing t1 mod t2.
Definition: Context.cs:993
static Z3_ast Z3_get_smtlib_assumption(Z3_context a0, uint a1)
Definition: Native.cs:3934
static Z3_ast Z3_parse_smtlib2_file(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
Definition: Native.cs:3888
BoolExpr MkBool(bool value)
Creates a Boolean value.
Definition: Context.cs:786
BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
Rotate Left.
Definition: Context.cs:1730
IntSort MkIntSort()
Create a new integer sort.
Definition: Context.cs:194
static Z3_ast Z3_mk_extract(Z3_context a0, uint a1, uint a2, Z3_ast a3)
Definition: Native.cs:2470
static Z3_ast Z3_mk_bvsub_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2590
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:31
BitVecExpr MkZeroExt(uint i, BitVecExpr t)
Bit-vector zero extension.
Definition: Context.cs:1628
static Z3_ast Z3_mk_bvor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2286
RatNum MkReal(uint v)
Create a real numeral.
Definition: Context.cs:2385
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:2871
Expr MkConst(FuncDecl f)
Creates a fresh constant from the FuncDecl f .
Definition: Context.cs:653
static void Z3_set_param_value(Z3_config a0, string a1, string a2)
Definition: Native.cs:1697
static Z3_probe Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4657
static Z3_ast Z3_mk_map(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3)
Definition: Native.cs:2662