Z3
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;
24 using System.Linq;
25 
26 namespace Microsoft.Z3
27 {
31  [ContractVerification(true)]
32  public class Context : IDisposable
33  {
34  #region Constructors
35  public Context()
39  : base()
40  {
41  lock (creation_lock)
42  {
43  m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
44  InitContext();
45  }
46  }
47 
66  public Context(Dictionary<string, string> settings)
67  : base()
68  {
69  Contract.Requires(settings != null);
70 
71  lock (creation_lock)
72  {
73  IntPtr cfg = Native.Z3_mk_config();
74  foreach (KeyValuePair<string, string> kv in settings)
75  Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
76  m_ctx = Native.Z3_mk_context_rc(cfg);
77  Native.Z3_del_config(cfg);
78  InitContext();
79  }
80  }
81  #endregion
82 
83  #region Symbols
84  public IntSymbol MkSymbol(int i)
92  {
93  Contract.Ensures(Contract.Result<IntSymbol>() != null);
94 
95  return new IntSymbol(this, i);
96  }
97 
101  public StringSymbol MkSymbol(string name)
102  {
103  Contract.Ensures(Contract.Result<StringSymbol>() != null);
104 
105  return new StringSymbol(this, name);
106  }
107 
111  internal Symbol[] MkSymbols(string[] names)
112  {
113  Contract.Ensures(names == null || Contract.Result<Symbol[]>() != null);
114  Contract.Ensures(names != null || Contract.Result<Symbol[]>() == null);
115  Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.Result<Symbol[]>().Length == names.Length);
116  Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.ForAll(Contract.Result<Symbol[]>(), s => s != null));
117 
118  if (names == null) return null;
119  Symbol[] result = new Symbol[names.Length];
120  for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
121  return result;
122  }
123  #endregion
124 
125  #region Sorts
126  private BoolSort m_boolSort = null;
127  private IntSort m_intSort = null;
128  private RealSort m_realSort = null;
129  private SeqSort m_stringSort = null;
130 
134  public BoolSort BoolSort
135  {
136  get
137  {
138  Contract.Ensures(Contract.Result<BoolSort>() != null);
139  if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
140  }
141  }
142 
146  public IntSort IntSort
147  {
148  get
149  {
150  Contract.Ensures(Contract.Result<IntSort>() != null);
151  if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
152  }
153  }
154 
155 
159  public RealSort RealSort
160  {
161  get
162  {
163  Contract.Ensures(Contract.Result<RealSort>() != null);
164  if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
165  }
166  }
167 
171  public SeqSort StringSort
172  {
173  get
174  {
175  Contract.Ensures(Contract.Result<SeqSort>() != null);
176  if (m_stringSort == null) m_stringSort = new SeqSort(this, Native.Z3_mk_string_sort(nCtx));
177  return m_stringSort;
178  }
179  }
180 
181 
186  {
187  Contract.Ensures(Contract.Result<BoolSort>() != null);
188  return new BoolSort(this);
189  }
190 
195  {
196  Contract.Requires(s != null);
197  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
198 
199  CheckContextMatch(s);
200  return new UninterpretedSort(this, s);
201  }
202 
207  {
208  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
209 
210  return MkUninterpretedSort(MkSymbol(str));
211  }
212 
217  {
218  Contract.Ensures(Contract.Result<IntSort>() != null);
219 
220  return new IntSort(this);
221  }
222 
227  {
228  Contract.Ensures(Contract.Result<RealSort>() != null);
229  return new RealSort(this);
230  }
231 
235  public BitVecSort MkBitVecSort(uint size)
236  {
237  Contract.Ensures(Contract.Result<BitVecSort>() != null);
238 
239  return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
240  }
241 
242 
247  {
248  Contract.Requires(s != null);
249  Contract.Ensures(Contract.Result<SeqSort>() != null);
250  return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
251  }
252 
257  {
258  Contract.Requires(s != null);
259  Contract.Ensures(Contract.Result<ReSort>() != null);
260  return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
261  }
262 
266  public ArraySort MkArraySort(Sort domain, Sort range)
267  {
268  Contract.Requires(domain != null);
269  Contract.Requires(range != null);
270  Contract.Ensures(Contract.Result<ArraySort>() != null);
271 
272  CheckContextMatch(domain);
273  CheckContextMatch(range);
274  return new ArraySort(this, domain, range);
275  }
276 
280  public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
281  {
282  Contract.Requires(name != null);
283  Contract.Requires(fieldNames != null);
284  Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
285  Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
286  Contract.Ensures(Contract.Result<TupleSort>() != null);
287 
288  CheckContextMatch(name);
289  CheckContextMatch<Symbol>(fieldNames);
290  CheckContextMatch<Sort>(fieldSorts);
291  return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
292  }
293 
297  public EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
298  {
299  Contract.Requires(name != null);
300  Contract.Requires(enumNames != null);
301  Contract.Requires(Contract.ForAll(enumNames, f => f != null));
302 
303  Contract.Ensures(Contract.Result<EnumSort>() != null);
304 
305  CheckContextMatch(name);
306  CheckContextMatch<Symbol>(enumNames);
307  return new EnumSort(this, name, enumNames);
308  }
309 
313  public EnumSort MkEnumSort(string name, params string[] enumNames)
314  {
315  Contract.Requires(enumNames != null);
316  Contract.Ensures(Contract.Result<EnumSort>() != null);
317 
318  return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
319  }
320 
324  public ListSort MkListSort(Symbol name, Sort elemSort)
325  {
326  Contract.Requires(name != null);
327  Contract.Requires(elemSort != null);
328  Contract.Ensures(Contract.Result<ListSort>() != null);
329 
330  CheckContextMatch(name);
331  CheckContextMatch(elemSort);
332  return new ListSort(this, name, elemSort);
333  }
334 
338  public ListSort MkListSort(string name, Sort elemSort)
339  {
340  Contract.Requires(elemSort != null);
341  Contract.Ensures(Contract.Result<ListSort>() != null);
342 
343  CheckContextMatch(elemSort);
344  return new ListSort(this, MkSymbol(name), elemSort);
345  }
346 
353  public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
354  {
355  Contract.Requires(name != null);
356  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
357 
358  CheckContextMatch(name);
359  return new FiniteDomainSort(this, name, size);
360  }
361 
370  public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
371  {
372  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
373 
374  return new FiniteDomainSort(this, MkSymbol(name), size);
375  }
376 
377 
378  #region Datatypes
379  public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
390  {
391  Contract.Requires(name != null);
392  Contract.Requires(recognizer != null);
393  Contract.Ensures(Contract.Result<Constructor>() != null);
394 
395  return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
396  }
397 
407  public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
408  {
409  Contract.Ensures(Contract.Result<Constructor>() != null);
410 
411  return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
412  }
413 
417  public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
418  {
419  Contract.Requires(name != null);
420  Contract.Requires(constructors != null);
421  Contract.Requires(Contract.ForAll(constructors, c => c != null));
422 
423  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
424 
425  CheckContextMatch(name);
426  CheckContextMatch<Constructor>(constructors);
427  return new DatatypeSort(this, name, constructors);
428  }
429 
433  public DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
434  {
435  Contract.Requires(constructors != null);
436  Contract.Requires(Contract.ForAll(constructors, c => c != null));
437  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
438 
439  CheckContextMatch<Constructor>(constructors);
440  return new DatatypeSort(this, MkSymbol(name), constructors);
441  }
442 
449  {
450  Contract.Requires(names != null);
451  Contract.Requires(c != null);
452  Contract.Requires(names.Length == c.Length);
453  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
454  Contract.Requires(Contract.ForAll(names, name => name != null));
455  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
456 
457  CheckContextMatch<Symbol>(names);
458  uint n = (uint)names.Length;
459  ConstructorList[] cla = new ConstructorList[n];
460  IntPtr[] n_constr = new IntPtr[n];
461  for (uint i = 0; i < n; i++)
462  {
463  Constructor[] constructor = c[i];
464  Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
465  CheckContextMatch<Constructor>(constructor);
466  cla[i] = new ConstructorList(this, constructor);
467  n_constr[i] = cla[i].NativeObject;
468  }
469  IntPtr[] n_res = new IntPtr[n];
470  Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
471  DatatypeSort[] res = new DatatypeSort[n];
472  for (uint i = 0; i < n; i++)
473  res[i] = new DatatypeSort(this, n_res[i]);
474  return res;
475  }
476 
483  public DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
484  {
485  Contract.Requires(names != null);
486  Contract.Requires(c != null);
487  Contract.Requires(names.Length == c.Length);
488  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
489  Contract.Requires(Contract.ForAll(names, name => name != null));
490  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
491 
492  return MkDatatypeSorts(MkSymbols(names), c);
493  }
494 
501  public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
502  {
503  return Expr.Create(this, Native.Z3_datatype_update_field(
504  nCtx, field.NativeObject,
505  t.NativeObject, v.NativeObject));
506  }
507 
508  #endregion
509  #endregion
510 
511  #region Function Declarations
512  public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
516  {
517  Contract.Requires(name != null);
518  Contract.Requires(range != null);
519  Contract.Requires(Contract.ForAll(domain, d => d != null));
520  Contract.Ensures(Contract.Result<FuncDecl>() != null);
521 
522  CheckContextMatch(name);
523  CheckContextMatch<Sort>(domain);
524  CheckContextMatch(range);
525  return new FuncDecl(this, name, domain, range);
526  }
527 
531  public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
532  {
533  Contract.Requires(name != null);
534  Contract.Requires(domain != null);
535  Contract.Requires(range != null);
536  Contract.Ensures(Contract.Result<FuncDecl>() != null);
537 
538  CheckContextMatch(name);
539  CheckContextMatch(domain);
540  CheckContextMatch(range);
541  Sort[] q = new Sort[] { domain };
542  return new FuncDecl(this, name, q, range);
543  }
544 
548  public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
549  {
550  Contract.Requires(range != null);
551  Contract.Requires(Contract.ForAll(domain, d => d != null));
552  Contract.Ensures(Contract.Result<FuncDecl>() != null);
553 
554  CheckContextMatch<Sort>(domain);
555  CheckContextMatch(range);
556  return new FuncDecl(this, MkSymbol(name), domain, range);
557  }
558 
562  public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
563  {
564  Contract.Requires(range != null);
565  Contract.Requires(domain != null);
566  Contract.Ensures(Contract.Result<FuncDecl>() != null);
567 
568  CheckContextMatch(domain);
569  CheckContextMatch(range);
570  Sort[] q = new Sort[] { domain };
571  return new FuncDecl(this, MkSymbol(name), q, range);
572  }
573 
579  public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
580  {
581  Contract.Requires(range != null);
582  Contract.Requires(Contract.ForAll(domain, d => d != null));
583  Contract.Ensures(Contract.Result<FuncDecl>() != null);
584 
585  CheckContextMatch<Sort>(domain);
586  CheckContextMatch(range);
587  return new FuncDecl(this, prefix, domain, range);
588  }
589 
593  public FuncDecl MkConstDecl(Symbol name, Sort range)
594  {
595  Contract.Requires(name != null);
596  Contract.Requires(range != null);
597  Contract.Ensures(Contract.Result<FuncDecl>() != null);
598 
599  CheckContextMatch(name);
600  CheckContextMatch(range);
601  return new FuncDecl(this, name, null, range);
602  }
603 
607  public FuncDecl MkConstDecl(string name, Sort range)
608  {
609  Contract.Requires(range != null);
610  Contract.Ensures(Contract.Result<FuncDecl>() != null);
611 
612  CheckContextMatch(range);
613  return new FuncDecl(this, MkSymbol(name), null, range);
614  }
615 
621  public FuncDecl MkFreshConstDecl(string prefix, Sort range)
622  {
623  Contract.Requires(range != null);
624  Contract.Ensures(Contract.Result<FuncDecl>() != null);
625 
626  CheckContextMatch(range);
627  return new FuncDecl(this, prefix, null, range);
628  }
629  #endregion
630 
631  #region Bound Variables
632  public Expr MkBound(uint index, Sort ty)
638  {
639  Contract.Requires(ty != null);
640  Contract.Ensures(Contract.Result<Expr>() != null);
641 
642  return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
643  }
644  #endregion
645 
646  #region Quantifier Patterns
647  public Pattern MkPattern(params Expr[] terms)
651  {
652  Contract.Requires(terms != null);
653  if (terms.Length == 0)
654  throw new Z3Exception("Cannot create a pattern from zero terms");
655 
656  Contract.Ensures(Contract.Result<Pattern>() != null);
657 
658  Contract.EndContractBlock();
659 
660  IntPtr[] termsNative = AST.ArrayToNative(terms);
661  return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
662  }
663  #endregion
664 
665  #region Constants
666  public Expr MkConst(Symbol name, Sort range)
670  {
671  Contract.Requires(name != null);
672  Contract.Requires(range != null);
673  Contract.Ensures(Contract.Result<Expr>() != null);
674 
675  CheckContextMatch(name);
676  CheckContextMatch(range);
677 
678  return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
679  }
680 
684  public Expr MkConst(string name, Sort range)
685  {
686  Contract.Requires(range != null);
687  Contract.Ensures(Contract.Result<Expr>() != null);
688 
689  return MkConst(MkSymbol(name), range);
690  }
691 
696  public Expr MkFreshConst(string prefix, Sort range)
697  {
698  Contract.Requires(range != null);
699  Contract.Ensures(Contract.Result<Expr>() != null);
700 
701  CheckContextMatch(range);
702  return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
703  }
704 
710  {
711  Contract.Requires(f != null);
712  Contract.Ensures(Contract.Result<Expr>() != null);
713 
714  return MkApp(f);
715  }
716 
721  {
722  Contract.Requires(name != null);
723  Contract.Ensures(Contract.Result<BoolExpr>() != null);
724 
725  return (BoolExpr)MkConst(name, BoolSort);
726  }
727 
731  public BoolExpr MkBoolConst(string name)
732  {
733  Contract.Ensures(Contract.Result<BoolExpr>() != null);
734 
735  return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
736  }
737 
741  public IntExpr MkIntConst(Symbol name)
742  {
743  Contract.Requires(name != null);
744  Contract.Ensures(Contract.Result<IntExpr>() != null);
745 
746  return (IntExpr)MkConst(name, IntSort);
747  }
748 
752  public IntExpr MkIntConst(string name)
753  {
754  Contract.Requires(name != null);
755  Contract.Ensures(Contract.Result<IntExpr>() != null);
756 
757  return (IntExpr)MkConst(name, IntSort);
758  }
759 
764  {
765  Contract.Requires(name != null);
766  Contract.Ensures(Contract.Result<RealExpr>() != null);
767 
768  return (RealExpr)MkConst(name, RealSort);
769  }
770 
774  public RealExpr MkRealConst(string name)
775  {
776  Contract.Ensures(Contract.Result<RealExpr>() != null);
777 
778  return (RealExpr)MkConst(name, RealSort);
779  }
780 
784  public BitVecExpr MkBVConst(Symbol name, uint size)
785  {
786  Contract.Requires(name != null);
787  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
788 
789  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
790  }
791 
795  public BitVecExpr MkBVConst(string name, uint size)
796  {
797  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
798 
799  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
800  }
801  #endregion
802 
803  #region Terms
804  public Expr MkApp(FuncDecl f, params Expr[] args)
808  {
809  Contract.Requires(f != null);
810  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
811  Contract.Ensures(Contract.Result<Expr>() != null);
812 
813  CheckContextMatch(f);
814  CheckContextMatch<Expr>(args);
815  return Expr.Create(this, f, args);
816  }
817 
821  public Expr MkApp(FuncDecl f, IEnumerable<Expr> args)
822  {
823  Contract.Requires(f != null);
824  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
825  Contract.Ensures(Contract.Result<Expr>() != null);
826 
827  CheckContextMatch(f);
828  CheckContextMatch(args);
829  return Expr.Create(this, f, args.ToArray());
830  }
831 
832  #region Propositional
833  public BoolExpr MkTrue()
837  {
838  Contract.Ensures(Contract.Result<BoolExpr>() != null);
839 
840  return new BoolExpr(this, Native.Z3_mk_true(nCtx));
841  }
842 
846  public BoolExpr MkFalse()
847  {
848  Contract.Ensures(Contract.Result<BoolExpr>() != null);
849 
850  return new BoolExpr(this, Native.Z3_mk_false(nCtx));
851  }
852 
856  public BoolExpr MkBool(bool value)
857  {
858  Contract.Ensures(Contract.Result<BoolExpr>() != null);
859 
860  return value ? MkTrue() : MkFalse();
861  }
862 
866  public BoolExpr MkEq(Expr x, Expr y)
867  {
868  Contract.Requires(x != null);
869  Contract.Requires(y != null);
870  Contract.Ensures(Contract.Result<BoolExpr>() != null);
871 
872  CheckContextMatch(x);
873  CheckContextMatch(y);
874  return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
875  }
876 
880  public BoolExpr MkDistinct(params Expr[] args)
881  {
882  Contract.Requires(args != null);
883  Contract.Requires(Contract.ForAll(args, a => a != null));
884 
885  Contract.Ensures(Contract.Result<BoolExpr>() != null);
886 
887  CheckContextMatch<Expr>(args);
888  return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
889  }
890 
895  {
896  Contract.Requires(a != null);
897  Contract.Ensures(Contract.Result<BoolExpr>() != null);
898 
899  CheckContextMatch(a);
900  return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
901  }
902 
909  public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
910  {
911  Contract.Requires(t1 != null);
912  Contract.Requires(t2 != null);
913  Contract.Requires(t3 != null);
914  Contract.Ensures(Contract.Result<Expr>() != null);
915 
916  CheckContextMatch(t1);
917  CheckContextMatch(t2);
918  CheckContextMatch(t3);
919  return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
920  }
921 
926  {
927  Contract.Requires(t1 != null);
928  Contract.Requires(t2 != null);
929  Contract.Ensures(Contract.Result<BoolExpr>() != null);
930 
931  CheckContextMatch(t1);
932  CheckContextMatch(t2);
933  return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
934  }
935 
940  {
941  Contract.Requires(t1 != null);
942  Contract.Requires(t2 != null);
943  Contract.Ensures(Contract.Result<BoolExpr>() != null);
944 
945  CheckContextMatch(t1);
946  CheckContextMatch(t2);
947  return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
948  }
949 
954  {
955  Contract.Requires(t1 != null);
956  Contract.Requires(t2 != null);
957  Contract.Ensures(Contract.Result<BoolExpr>() != null);
958 
959  CheckContextMatch(t1);
960  CheckContextMatch(t2);
961  return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
962  }
963 
967  public BoolExpr MkAnd(params BoolExpr[] t)
968  {
969  Contract.Requires(t != null);
970  Contract.Requires(Contract.ForAll(t, a => a != null));
971  Contract.Ensures(Contract.Result<BoolExpr>() != null);
972 
973  CheckContextMatch<BoolExpr>(t);
974  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
975  }
976 
980  public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
981  {
982  Contract.Requires(t != null);
983  Contract.Requires(Contract.ForAll(t, a => a != null));
984  Contract.Ensures(Contract.Result<BoolExpr>() != null);
985  CheckContextMatch<BoolExpr>(t);
986  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
987  }
988 
992  public BoolExpr MkOr(params BoolExpr[] t)
993  {
994  Contract.Requires(t != null);
995  Contract.Requires(Contract.ForAll(t, a => a != null));
996  Contract.Ensures(Contract.Result<BoolExpr>() != null);
997 
998  CheckContextMatch<BoolExpr>(t);
999  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1000  }
1001 
1002 
1006  public BoolExpr MkOr(IEnumerable<BoolExpr> t)
1007  {
1008  Contract.Requires(t != null);
1009  Contract.Requires(Contract.ForAll(t, a => a != null));
1010  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1011 
1012  CheckContextMatch(t);
1013  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
1014  }
1015 
1016  #endregion
1017 
1018  #region Arithmetic
1019  public ArithExpr MkAdd(params ArithExpr[] t)
1023  {
1024  Contract.Requires(t != null);
1025  Contract.Requires(Contract.ForAll(t, a => a != null));
1026  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1027 
1028  CheckContextMatch<ArithExpr>(t);
1029  return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1030  }
1031 
1035  public ArithExpr MkAdd(IEnumerable<ArithExpr> t)
1036  {
1037  Contract.Requires(t != null);
1038  Contract.Requires(Contract.ForAll(t, a => a != null));
1039  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1040 
1041  CheckContextMatch(t);
1042  return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
1043  }
1044 
1048  public ArithExpr MkMul(params ArithExpr[] t)
1049  {
1050  Contract.Requires(t != null);
1051  Contract.Requires(Contract.ForAll(t, a => a != null));
1052  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1053 
1054  CheckContextMatch<ArithExpr>(t);
1055  return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1056  }
1057 
1061  public ArithExpr MkMul(IEnumerable<ArithExpr> t)
1062  {
1063  Contract.Requires(t != null);
1064  Contract.Requires(Contract.ForAll(t, a => a != null));
1065  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1066 
1067  CheckContextMatch<ArithExpr>(t);
1068  return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
1069  }
1070 
1074  public ArithExpr MkSub(params ArithExpr[] t)
1075  {
1076  Contract.Requires(t != null);
1077  Contract.Requires(Contract.ForAll(t, a => a != null));
1078  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1079 
1080  CheckContextMatch<ArithExpr>(t);
1081  return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1082  }
1083 
1088  {
1089  Contract.Requires(t != null);
1090  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1091 
1092  CheckContextMatch(t);
1093  return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
1094  }
1095 
1100  {
1101  Contract.Requires(t1 != null);
1102  Contract.Requires(t2 != null);
1103  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1104 
1105  CheckContextMatch(t1);
1106  CheckContextMatch(t2);
1107  return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1108  }
1109 
1114  public IntExpr MkMod(IntExpr t1, IntExpr t2)
1115  {
1116  Contract.Requires(t1 != null);
1117  Contract.Requires(t2 != null);
1118  Contract.Ensures(Contract.Result<IntExpr>() != null);
1119 
1120  CheckContextMatch(t1);
1121  CheckContextMatch(t2);
1122  return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1123  }
1124 
1129  public IntExpr MkRem(IntExpr t1, IntExpr t2)
1130  {
1131  Contract.Requires(t1 != null);
1132  Contract.Requires(t2 != null);
1133  Contract.Ensures(Contract.Result<IntExpr>() != null);
1134 
1135  CheckContextMatch(t1);
1136  CheckContextMatch(t2);
1137  return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1138  }
1139 
1144  {
1145  Contract.Requires(t1 != null);
1146  Contract.Requires(t2 != null);
1147  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1148 
1149  CheckContextMatch(t1);
1150  CheckContextMatch(t2);
1151  return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1152  }
1153 
1158  {
1159  Contract.Requires(t1 != null);
1160  Contract.Requires(t2 != null);
1161  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1162 
1163  CheckContextMatch(t1);
1164  CheckContextMatch(t2);
1165  return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1166  }
1167 
1172  {
1173  Contract.Requires(t1 != null);
1174  Contract.Requires(t2 != null);
1175  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1176 
1177  CheckContextMatch(t1);
1178  CheckContextMatch(t2);
1179  return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1180  }
1181 
1186  {
1187  Contract.Requires(t1 != null);
1188  Contract.Requires(t2 != null);
1189  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1190 
1191  CheckContextMatch(t1);
1192  CheckContextMatch(t2);
1193  return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1194  }
1195 
1200  {
1201  Contract.Requires(t1 != null);
1202  Contract.Requires(t2 != null);
1203  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1204 
1205  CheckContextMatch(t1);
1206  CheckContextMatch(t2);
1207  return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1208  }
1209 
1221  {
1222  Contract.Requires(t != null);
1223  Contract.Ensures(Contract.Result<RealExpr>() != null);
1224 
1225  CheckContextMatch(t);
1226  return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1227  }
1228 
1237  {
1238  Contract.Requires(t != null);
1239  Contract.Ensures(Contract.Result<IntExpr>() != null);
1240 
1241  CheckContextMatch(t);
1242  return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1243  }
1244 
1249  {
1250  Contract.Requires(t != null);
1251  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1252 
1253  CheckContextMatch(t);
1254  return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1255  }
1256  #endregion
1257 
1258  #region Bit-vectors
1259  public BitVecExpr MkBVNot(BitVecExpr t)
1264  {
1265  Contract.Requires(t != null);
1266  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1267 
1268  CheckContextMatch(t);
1269  return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1270  }
1271 
1277  {
1278  Contract.Requires(t != null);
1279  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1280 
1281  CheckContextMatch(t);
1282  return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1283  }
1284 
1290  {
1291  Contract.Requires(t != null);
1292  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1293 
1294  CheckContextMatch(t);
1295  return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1296  }
1297 
1303  {
1304  Contract.Requires(t1 != null);
1305  Contract.Requires(t2 != null);
1306  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1307 
1308  CheckContextMatch(t1);
1309  CheckContextMatch(t2);
1310  return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1311  }
1312 
1318  {
1319  Contract.Requires(t1 != null);
1320  Contract.Requires(t2 != null);
1321  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1322 
1323  CheckContextMatch(t1);
1324  CheckContextMatch(t2);
1325  return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1326  }
1327 
1333  {
1334  Contract.Requires(t1 != null);
1335  Contract.Requires(t2 != null);
1336  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1337 
1338  CheckContextMatch(t1);
1339  CheckContextMatch(t2);
1340  return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1341  }
1342 
1348  {
1349  Contract.Requires(t1 != null);
1350  Contract.Requires(t2 != null);
1351  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1352 
1353  CheckContextMatch(t1);
1354  CheckContextMatch(t2);
1355  return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1356  }
1357 
1363  {
1364  Contract.Requires(t1 != null);
1365  Contract.Requires(t2 != null);
1366  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1367 
1368  CheckContextMatch(t1);
1369  CheckContextMatch(t2);
1370  return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1371  }
1372 
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_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1386  }
1387 
1393  {
1394  Contract.Requires(t != null);
1395  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1396 
1397  CheckContextMatch(t);
1398  return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1399  }
1400 
1406  {
1407  Contract.Requires(t1 != null);
1408  Contract.Requires(t2 != null);
1409  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1410 
1411  CheckContextMatch(t1);
1412  CheckContextMatch(t2);
1413  return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1414  }
1415 
1421  {
1422  Contract.Requires(t1 != null);
1423  Contract.Requires(t2 != null);
1424  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1425 
1426  CheckContextMatch(t1);
1427  CheckContextMatch(t2);
1428  return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1429  }
1430 
1436  {
1437  Contract.Requires(t1 != null);
1438  Contract.Requires(t2 != null);
1439  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1440 
1441  CheckContextMatch(t1);
1442  CheckContextMatch(t2);
1443  return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1444  }
1445 
1456  {
1457  Contract.Requires(t1 != null);
1458  Contract.Requires(t2 != null);
1459  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1460 
1461  CheckContextMatch(t1);
1462  CheckContextMatch(t2);
1463  return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1464  }
1465 
1480  {
1481  Contract.Requires(t1 != null);
1482  Contract.Requires(t2 != null);
1483  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1484 
1485  CheckContextMatch(t1);
1486  CheckContextMatch(t2);
1487  return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1488  }
1489 
1499  {
1500  Contract.Requires(t1 != null);
1501  Contract.Requires(t2 != null);
1502  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1503 
1504  CheckContextMatch(t1);
1505  CheckContextMatch(t2);
1506  return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1507  }
1508 
1520  {
1521  Contract.Requires(t1 != null);
1522  Contract.Requires(t2 != null);
1523  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1524 
1525  CheckContextMatch(t1);
1526  CheckContextMatch(t2);
1527  return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1528  }
1529 
1538  {
1539  Contract.Requires(t1 != null);
1540  Contract.Requires(t2 != null);
1541  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1542 
1543  CheckContextMatch(t1);
1544  CheckContextMatch(t2);
1545  return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1546  }
1547 
1555  {
1556  Contract.Requires(t1 != null);
1557  Contract.Requires(t2 != null);
1558  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1559 
1560  CheckContextMatch(t1);
1561  CheckContextMatch(t2);
1562  return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1563  }
1564 
1572  {
1573  Contract.Requires(t1 != null);
1574  Contract.Requires(t2 != null);
1575  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1576 
1577  CheckContextMatch(t1);
1578  CheckContextMatch(t2);
1579  return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1580  }
1581 
1589  {
1590  Contract.Requires(t1 != null);
1591  Contract.Requires(t2 != null);
1592  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1593 
1594  CheckContextMatch(t1);
1595  CheckContextMatch(t2);
1596  return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1597  }
1598 
1606  {
1607  Contract.Requires(t1 != null);
1608  Contract.Requires(t2 != null);
1609  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1610 
1611  CheckContextMatch(t1);
1612  CheckContextMatch(t2);
1613  return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1614  }
1615 
1623  {
1624  Contract.Requires(t1 != null);
1625  Contract.Requires(t2 != null);
1626  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1627 
1628  CheckContextMatch(t1);
1629  CheckContextMatch(t2);
1630  return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1631  }
1632 
1640  {
1641  Contract.Requires(t1 != null);
1642  Contract.Requires(t2 != null);
1643  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1644 
1645  CheckContextMatch(t1);
1646  CheckContextMatch(t2);
1647  return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1648  }
1649 
1657  {
1658  Contract.Requires(t1 != null);
1659  Contract.Requires(t2 != null);
1660  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1661 
1662  CheckContextMatch(t1);
1663  CheckContextMatch(t2);
1664  return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1665  }
1666 
1674  {
1675  Contract.Requires(t1 != null);
1676  Contract.Requires(t2 != null);
1677  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1678 
1679  CheckContextMatch(t1);
1680  CheckContextMatch(t2);
1681  return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1682  }
1683 
1695  {
1696  Contract.Requires(t1 != null);
1697  Contract.Requires(t2 != null);
1698  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1699 
1700  CheckContextMatch(t1);
1701  CheckContextMatch(t2);
1702  return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1703  }
1704 
1714  public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
1715  {
1716  Contract.Requires(t != null);
1717  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1718 
1719  CheckContextMatch(t);
1720  return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1721  }
1722 
1731  public BitVecExpr MkSignExt(uint i, BitVecExpr t)
1732  {
1733  Contract.Requires(t != null);
1734  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1735 
1736  CheckContextMatch(t);
1737  return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1738  }
1739 
1749  public BitVecExpr MkZeroExt(uint i, BitVecExpr t)
1750  {
1751  Contract.Requires(t != null);
1752  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1753 
1754  CheckContextMatch(t);
1755  return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1756  }
1757 
1764  public BitVecExpr MkRepeat(uint i, BitVecExpr t)
1765  {
1766  Contract.Requires(t != null);
1767  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1768 
1769  CheckContextMatch(t);
1770  return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1771  }
1772 
1786  {
1787  Contract.Requires(t1 != null);
1788  Contract.Requires(t2 != null);
1789  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1790 
1791  CheckContextMatch(t1);
1792  CheckContextMatch(t2);
1793  return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1794  }
1795 
1809  {
1810  Contract.Requires(t1 != null);
1811  Contract.Requires(t2 != null);
1812  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1813 
1814  CheckContextMatch(t1);
1815  CheckContextMatch(t2);
1816  return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1817  }
1818 
1834  {
1835  Contract.Requires(t1 != null);
1836  Contract.Requires(t2 != null);
1837  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1838 
1839  CheckContextMatch(t1);
1840  CheckContextMatch(t2);
1841  return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1842  }
1843 
1852  {
1853  Contract.Requires(t != null);
1854  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1855 
1856  CheckContextMatch(t);
1857  return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1858  }
1859 
1868  {
1869  Contract.Requires(t != null);
1870  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1871 
1872  CheckContextMatch(t);
1873  return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1874  }
1875 
1884  {
1885  Contract.Requires(t1 != null);
1886  Contract.Requires(t2 != null);
1887  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1888 
1889  CheckContextMatch(t1);
1890  CheckContextMatch(t2);
1891  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1892  }
1893 
1902  {
1903  Contract.Requires(t1 != null);
1904  Contract.Requires(t2 != null);
1905  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1906 
1907  CheckContextMatch(t1);
1908  CheckContextMatch(t2);
1909  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1910  }
1911 
1922  public BitVecExpr MkInt2BV(uint n, IntExpr t)
1923  {
1924  Contract.Requires(t != null);
1925  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1926 
1927  CheckContextMatch(t);
1928  return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1929  }
1930 
1946  public IntExpr MkBV2Int(BitVecExpr t, bool signed)
1947  {
1948  Contract.Requires(t != null);
1949  Contract.Ensures(Contract.Result<IntExpr>() != null);
1950 
1951  CheckContextMatch(t);
1952  return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
1953  }
1954 
1961  public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1962  {
1963  Contract.Requires(t1 != null);
1964  Contract.Requires(t2 != null);
1965  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1966 
1967  CheckContextMatch(t1);
1968  CheckContextMatch(t2);
1969  return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1970  }
1971 
1979  {
1980  Contract.Requires(t1 != null);
1981  Contract.Requires(t2 != null);
1982  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1983 
1984  CheckContextMatch(t1);
1985  CheckContextMatch(t2);
1986  return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1987  }
1988 
1996  {
1997  Contract.Requires(t1 != null);
1998  Contract.Requires(t2 != null);
1999  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2000 
2001  CheckContextMatch(t1);
2002  CheckContextMatch(t2);
2003  return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2004  }
2005 
2012  public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
2013  {
2014  Contract.Requires(t1 != null);
2015  Contract.Requires(t2 != null);
2016  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2017 
2018  CheckContextMatch(t1);
2019  CheckContextMatch(t2);
2020  return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
2021  }
2022 
2030  {
2031  Contract.Requires(t1 != null);
2032  Contract.Requires(t2 != null);
2033  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2034 
2035  CheckContextMatch(t1);
2036  CheckContextMatch(t2);
2037  return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2038  }
2039 
2047  {
2048  Contract.Requires(t != null);
2049  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2050 
2051  CheckContextMatch(t);
2052  return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
2053  }
2054 
2061  public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
2062  {
2063  Contract.Requires(t1 != null);
2064  Contract.Requires(t2 != null);
2065  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2066 
2067  CheckContextMatch(t1);
2068  CheckContextMatch(t2);
2069  return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
2070  }
2071 
2079  {
2080  Contract.Requires(t1 != null);
2081  Contract.Requires(t2 != null);
2082  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2083 
2084  CheckContextMatch(t1);
2085  CheckContextMatch(t2);
2086  return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2087  }
2088  #endregion
2089 
2090  #region Arrays
2091  public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
2095  {
2096  Contract.Requires(name != null);
2097  Contract.Requires(domain != null);
2098  Contract.Requires(range != null);
2099  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2100 
2101  return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
2102  }
2103 
2107  public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
2108  {
2109  Contract.Requires(domain != null);
2110  Contract.Requires(range != null);
2111  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2112 
2113  return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
2114  }
2115 
2130  {
2131  Contract.Requires(a != null);
2132  Contract.Requires(i != null);
2133  Contract.Ensures(Contract.Result<Expr>() != null);
2134 
2135  CheckContextMatch(a);
2136  CheckContextMatch(i);
2137  return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2138  }
2139 
2158  {
2159  Contract.Requires(a != null);
2160  Contract.Requires(i != null);
2161  Contract.Requires(v != null);
2162  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2163 
2164  CheckContextMatch(a);
2165  CheckContextMatch(i);
2166  CheckContextMatch(v);
2167  return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2168  }
2169 
2179  public ArrayExpr MkConstArray(Sort domain, Expr v)
2180  {
2181  Contract.Requires(domain != null);
2182  Contract.Requires(v != null);
2183  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2184 
2185  CheckContextMatch(domain);
2186  CheckContextMatch(v);
2187  return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2188  }
2189 
2201  public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
2202  {
2203  Contract.Requires(f != null);
2204  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2205  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2206 
2207  CheckContextMatch(f);
2208  CheckContextMatch<ArrayExpr>(args);
2209  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2210  }
2211 
2220  {
2221  Contract.Requires(array != null);
2222  Contract.Ensures(Contract.Result<Expr>() != null);
2223 
2224  CheckContextMatch(array);
2225  return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2226  }
2227 
2231  public Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
2232  {
2233  Contract.Requires(arg1 != null);
2234  Contract.Requires(arg2 != null);
2235  Contract.Ensures(Contract.Result<Expr>() != null);
2236 
2237  CheckContextMatch(arg1);
2238  CheckContextMatch(arg2);
2239  return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
2240  }
2241 
2242  #endregion
2243 
2244  #region Sets
2245  public SetSort MkSetSort(Sort ty)
2249  {
2250  Contract.Requires(ty != null);
2251  Contract.Ensures(Contract.Result<SetSort>() != null);
2252 
2253  CheckContextMatch(ty);
2254  return new SetSort(this, ty);
2255  }
2256 
2260  public ArrayExpr MkEmptySet(Sort domain)
2261  {
2262  Contract.Requires(domain != null);
2263  Contract.Ensures(Contract.Result<Expr>() != null);
2264 
2265  CheckContextMatch(domain);
2266  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2267  }
2268 
2272  public ArrayExpr MkFullSet(Sort domain)
2273  {
2274  Contract.Requires(domain != null);
2275  Contract.Ensures(Contract.Result<Expr>() != null);
2276 
2277  CheckContextMatch(domain);
2278  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2279  }
2280 
2284  public ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
2285  {
2286  Contract.Requires(set != null);
2287  Contract.Requires(element != null);
2288  Contract.Ensures(Contract.Result<Expr>() != null);
2289 
2290  CheckContextMatch(set);
2291  CheckContextMatch(element);
2292  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2293  }
2294 
2295 
2299  public ArrayExpr MkSetDel(ArrayExpr set, Expr element)
2300  {
2301  Contract.Requires(set != null);
2302  Contract.Requires(element != null);
2303  Contract.Ensures(Contract.Result<Expr>() != null);
2304 
2305  CheckContextMatch(set);
2306  CheckContextMatch(element);
2307  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2308  }
2309 
2313  public ArrayExpr MkSetUnion(params ArrayExpr[] args)
2314  {
2315  Contract.Requires(args != null);
2316  Contract.Requires(Contract.ForAll(args, a => a != null));
2317 
2318  CheckContextMatch<ArrayExpr>(args);
2319  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2320  }
2321 
2325  public ArrayExpr MkSetIntersection(params ArrayExpr[] args)
2326  {
2327  Contract.Requires(args != null);
2328  Contract.Requires(Contract.ForAll(args, a => a != null));
2329  Contract.Ensures(Contract.Result<Expr>() != null);
2330 
2331  CheckContextMatch<ArrayExpr>(args);
2332  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2333  }
2334 
2339  {
2340  Contract.Requires(arg1 != null);
2341  Contract.Requires(arg2 != null);
2342  Contract.Ensures(Contract.Result<Expr>() != null);
2343 
2344  CheckContextMatch(arg1);
2345  CheckContextMatch(arg2);
2346  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2347  }
2348 
2353  {
2354  Contract.Requires(arg != null);
2355  Contract.Ensures(Contract.Result<Expr>() != null);
2356 
2357  CheckContextMatch(arg);
2358  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2359  }
2360 
2365  {
2366  Contract.Requires(elem != null);
2367  Contract.Requires(set != null);
2368  Contract.Ensures(Contract.Result<Expr>() != null);
2369 
2370  CheckContextMatch(elem);
2371  CheckContextMatch(set);
2372  return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2373  }
2374 
2379  {
2380  Contract.Requires(arg1 != null);
2381  Contract.Requires(arg2 != null);
2382  Contract.Ensures(Contract.Result<Expr>() != null);
2383 
2384  CheckContextMatch(arg1);
2385  CheckContextMatch(arg2);
2386  return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2387  }
2388 
2389  #endregion
2390 
2391  #region Sequence, string and regular expresions
2392 
2397  {
2398  Contract.Requires(s != null);
2399  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2400  return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
2401  }
2402 
2406  public SeqExpr MkUnit(Expr elem)
2407  {
2408  Contract.Requires(elem != null);
2409  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2410  return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
2411  }
2412 
2416  public SeqExpr MkString(string s)
2417  {
2418  Contract.Requires(s != null);
2419  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2420  return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
2421  }
2422 
2426  public SeqExpr MkConcat(params SeqExpr[] t)
2427  {
2428  Contract.Requires(t != null);
2429  Contract.Requires(Contract.ForAll(t, a => a != null));
2430  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2431 
2432  CheckContextMatch<SeqExpr>(t);
2433  return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2434  }
2435 
2436 
2441  {
2442  Contract.Requires(s != null);
2443  Contract.Ensures(Contract.Result<IntExpr>() != null);
2444  return (IntExpr) Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
2445  }
2446 
2451  {
2452  Contract.Requires(s1 != null);
2453  Contract.Requires(s2 != null);
2454  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2455  CheckContextMatch(s1, s2);
2456  return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
2457  }
2458 
2463  {
2464  Contract.Requires(s1 != null);
2465  Contract.Requires(s2 != null);
2466  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2467  CheckContextMatch(s1, s2);
2468  return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
2469  }
2470 
2475  {
2476  Contract.Requires(s1 != null);
2477  Contract.Requires(s2 != null);
2478  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2479  CheckContextMatch(s1, s2);
2480  return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
2481  }
2482 
2486  public SeqExpr MkAt(SeqExpr s, IntExpr index)
2487  {
2488  Contract.Requires(s != null);
2489  Contract.Requires(index != null);
2490  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2491  CheckContextMatch(s, index);
2492  return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
2493  }
2494 
2498  public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
2499  {
2500  Contract.Requires(s != null);
2501  Contract.Requires(offset != null);
2502  Contract.Requires(length != null);
2503  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2504  CheckContextMatch(s, offset, length);
2505  return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
2506  }
2507 
2511  public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
2512  {
2513  Contract.Requires(s != null);
2514  Contract.Requires(offset != null);
2515  Contract.Requires(substr != null);
2516  Contract.Ensures(Contract.Result<IntExpr>() != null);
2517  CheckContextMatch(s, substr, offset);
2518  return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
2519  }
2520 
2525  {
2526  Contract.Requires(s != null);
2527  Contract.Requires(src != null);
2528  Contract.Requires(dst != null);
2529  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2530  CheckContextMatch(s, src, dst);
2531  return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
2532  }
2533 
2537  public ReExpr MkToRe(SeqExpr s)
2538  {
2539  Contract.Requires(s != null);
2540  Contract.Ensures(Contract.Result<ReExpr>() != null);
2541  return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));
2542  }
2543 
2544 
2549  {
2550  Contract.Requires(s != null);
2551  Contract.Requires(re != null);
2552  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2553  CheckContextMatch(s, re);
2554  return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
2555  }
2556 
2560  public ReExpr MkStar(ReExpr re)
2561  {
2562  Contract.Requires(re != null);
2563  Contract.Ensures(Contract.Result<ReExpr>() != null);
2564  return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
2565  }
2566 
2570  public ReExpr MPlus(ReExpr re)
2571  {
2572  Contract.Requires(re != null);
2573  Contract.Ensures(Contract.Result<ReExpr>() != null);
2574  return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));
2575  }
2576 
2580  public ReExpr MOption(ReExpr re)
2581  {
2582  Contract.Requires(re != null);
2583  Contract.Ensures(Contract.Result<ReExpr>() != null);
2584  return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
2585  }
2586 
2590  public ReExpr MkConcat(params ReExpr[] t)
2591  {
2592  Contract.Requires(t != null);
2593  Contract.Requires(Contract.ForAll(t, a => a != null));
2594  Contract.Ensures(Contract.Result<ReExpr>() != null);
2595 
2596  CheckContextMatch<ReExpr>(t);
2597  return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2598  }
2599 
2603  public ReExpr MkUnion(params ReExpr[] t)
2604  {
2605  Contract.Requires(t != null);
2606  Contract.Requires(Contract.ForAll(t, a => a != null));
2607  Contract.Ensures(Contract.Result<ReExpr>() != null);
2608 
2609  CheckContextMatch<ReExpr>(t);
2610  return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2611  }
2612 
2613  #endregion
2614 
2615  #region Pseudo-Boolean constraints
2616 
2620  public BoolExpr MkAtMost(BoolExpr[] args, uint k)
2621  {
2622  Contract.Requires(args != null);
2623  Contract.Requires(Contract.Result<BoolExpr[]>() != null);
2624  CheckContextMatch<BoolExpr>(args);
2625  return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length,
2626  AST.ArrayToNative(args), k));
2627  }
2628 
2632  public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
2633  {
2634  Contract.Requires(args != null);
2635  Contract.Requires(coeffs != null);
2636  Contract.Requires(args.Length == coeffs.Length);
2637  Contract.Requires(Contract.Result<BoolExpr[]>() != null);
2638  CheckContextMatch<BoolExpr>(args);
2639  return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
2640  AST.ArrayToNative(args),
2641  coeffs, k));
2642  }
2643 
2647  public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
2648  {
2649  Contract.Requires(args != null);
2650  Contract.Requires(coeffs != null);
2651  Contract.Requires(args.Length == coeffs.Length);
2652  Contract.Requires(Contract.Result<BoolExpr[]>() != null);
2653  CheckContextMatch<BoolExpr>(args);
2654  return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length,
2655  AST.ArrayToNative(args),
2656  coeffs, k));
2657  }
2658  #endregion
2659 
2660  #region Numerals
2661 
2662  #region General Numerals
2663  public Expr MkNumeral(string v, Sort ty)
2670  {
2671  Contract.Requires(ty != null);
2672  Contract.Ensures(Contract.Result<Expr>() != null);
2673 
2674  CheckContextMatch(ty);
2675  return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2676  }
2677 
2685  public Expr MkNumeral(int v, Sort ty)
2686  {
2687  Contract.Requires(ty != null);
2688  Contract.Ensures(Contract.Result<Expr>() != null);
2689 
2690  CheckContextMatch(ty);
2691  return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2692  }
2693 
2701  public Expr MkNumeral(uint v, Sort ty)
2702  {
2703  Contract.Requires(ty != null);
2704  Contract.Ensures(Contract.Result<Expr>() != null);
2705 
2706  CheckContextMatch(ty);
2707  return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2708  }
2709 
2717  public Expr MkNumeral(long v, Sort ty)
2718  {
2719  Contract.Requires(ty != null);
2720  Contract.Ensures(Contract.Result<Expr>() != null);
2721 
2722  CheckContextMatch(ty);
2723  return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2724  }
2725 
2733  public Expr MkNumeral(ulong v, Sort ty)
2734  {
2735  Contract.Requires(ty != null);
2736  Contract.Ensures(Contract.Result<Expr>() != null);
2737 
2738  CheckContextMatch(ty);
2739  return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2740  }
2741  #endregion
2742 
2743  #region Reals
2744  public RatNum MkReal(int num, int den)
2752  {
2753  if (den == 0)
2754  throw new Z3Exception("Denominator is zero");
2755 
2756  Contract.Ensures(Contract.Result<RatNum>() != null);
2757  Contract.EndContractBlock();
2758 
2759  return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
2760  }
2761 
2767  public RatNum MkReal(string v)
2768  {
2769  Contract.Ensures(Contract.Result<RatNum>() != null);
2770 
2771  return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
2772  }
2773 
2779  public RatNum MkReal(int v)
2780  {
2781  Contract.Ensures(Contract.Result<RatNum>() != null);
2782 
2783  return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
2784  }
2785 
2791  public RatNum MkReal(uint v)
2792  {
2793  Contract.Ensures(Contract.Result<RatNum>() != null);
2794 
2795  return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
2796  }
2797 
2803  public RatNum MkReal(long v)
2804  {
2805  Contract.Ensures(Contract.Result<RatNum>() != null);
2806 
2807  return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
2808  }
2809 
2815  public RatNum MkReal(ulong v)
2816  {
2817  Contract.Ensures(Contract.Result<RatNum>() != null);
2818 
2819  return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
2820  }
2821  #endregion
2822 
2823  #region Integers
2824  public IntNum MkInt(string v)
2829  {
2830  Contract.Ensures(Contract.Result<IntNum>() != null);
2831 
2832  return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
2833  }
2834 
2840  public IntNum MkInt(int v)
2841  {
2842  Contract.Ensures(Contract.Result<IntNum>() != null);
2843 
2844  return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
2845  }
2846 
2852  public IntNum MkInt(uint v)
2853  {
2854  Contract.Ensures(Contract.Result<IntNum>() != null);
2855 
2856  return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
2857  }
2858 
2864  public IntNum MkInt(long v)
2865  {
2866  Contract.Ensures(Contract.Result<IntNum>() != null);
2867 
2868  return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
2869  }
2870 
2876  public IntNum MkInt(ulong v)
2877  {
2878  Contract.Ensures(Contract.Result<IntNum>() != null);
2879 
2880  return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
2881  }
2882  #endregion
2883 
2884  #region Bit-vectors
2885  public BitVecNum MkBV(string v, uint size)
2891  {
2892  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2893 
2894  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2895  }
2896 
2902  public BitVecNum MkBV(int v, uint size)
2903  {
2904  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2905 
2906  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2907  }
2908 
2914  public BitVecNum MkBV(uint v, uint size)
2915  {
2916  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2917 
2918  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2919  }
2920 
2926  public BitVecNum MkBV(long v, uint size)
2927  {
2928  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2929 
2930  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2931  }
2932 
2938  public BitVecNum MkBV(ulong v, uint size)
2939  {
2940  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2941 
2942  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2943  }
2944  #endregion
2945 
2946  #endregion // Numerals
2947 
2948  #region Quantifiers
2949  public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2974  {
2975  Contract.Requires(sorts != null);
2976  Contract.Requires(names != null);
2977  Contract.Requires(body != null);
2978  Contract.Requires(sorts.Length == names.Length);
2979  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2980  Contract.Requires(Contract.ForAll(names, n => n != null));
2981  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2982  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2983 
2984  Contract.Ensures(Contract.Result<Quantifier>() != null);
2985 
2986  return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2987  }
2988 
2989 
2998  public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2999  {
3000  Contract.Requires(body != null);
3001  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
3002  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3003  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3004 
3005  Contract.Ensures(Contract.Result<Quantifier>() != null);
3006 
3007  return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3008  }
3009 
3017  public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3018  {
3019  Contract.Requires(sorts != null);
3020  Contract.Requires(names != null);
3021  Contract.Requires(body != null);
3022  Contract.Requires(sorts.Length == names.Length);
3023  Contract.Requires(Contract.ForAll(sorts, s => s != null));
3024  Contract.Requires(Contract.ForAll(names, n => n != null));
3025  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3026  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3027  Contract.Ensures(Contract.Result<Quantifier>() != null);
3028 
3029  return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3030  }
3031 
3040  public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3041  {
3042  Contract.Requires(body != null);
3043  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
3044  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3045  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3046  Contract.Ensures(Contract.Result<Quantifier>() != null);
3047 
3048  return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3049  }
3050 
3051 
3056  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)
3057  {
3058  Contract.Requires(body != null);
3059  Contract.Requires(names != null);
3060  Contract.Requires(sorts != null);
3061  Contract.Requires(sorts.Length == names.Length);
3062  Contract.Requires(Contract.ForAll(sorts, s => s != null));
3063  Contract.Requires(Contract.ForAll(names, n => n != null));
3064  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3065  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3066 
3067  Contract.Ensures(Contract.Result<Quantifier>() != null);
3068 
3069  if (universal)
3070  return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3071  else
3072  return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3073  }
3074 
3075 
3080  public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
3081  {
3082  Contract.Requires(body != null);
3083  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
3084  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3085  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3086 
3087  Contract.Ensures(Contract.Result<Quantifier>() != null);
3088 
3089  if (universal)
3090  return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3091  else
3092  return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3093  }
3094 
3095  #endregion
3096 
3097  #endregion // Expr
3098 
3099  #region Options
3100  public Z3_ast_print_mode PrintMode
3117  {
3118  set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
3119  }
3120  #endregion
3121 
3122  #region SMT Files & Strings
3123  public string BenchmarkToSMTString(string name, string logic, string status, string attributes,
3134  BoolExpr[] assumptions, BoolExpr formula)
3135  {
3136  Contract.Requires(assumptions != null);
3137  Contract.Requires(formula != null);
3138  Contract.Ensures(Contract.Result<string>() != null);
3139 
3140  return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
3141  (uint)assumptions.Length, AST.ArrayToNative(assumptions),
3142  formula.NativeObject);
3143  }
3144 
3155  public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
3156  {
3157  uint csn = Symbol.ArrayLength(sortNames);
3158  uint cs = Sort.ArrayLength(sorts);
3159  uint cdn = Symbol.ArrayLength(declNames);
3160  uint cd = AST.ArrayLength(decls);
3161  if (csn != cs || cdn != cd)
3162  throw new Z3Exception("Argument size mismatch");
3163  Native.Z3_parse_smtlib_string(nCtx, str,
3164  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3165  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
3166  }
3167 
3172  public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
3173  {
3174  uint csn = Symbol.ArrayLength(sortNames);
3175  uint cs = Sort.ArrayLength(sorts);
3176  uint cdn = Symbol.ArrayLength(declNames);
3177  uint cd = AST.ArrayLength(decls);
3178  if (csn != cs || cdn != cd)
3179  throw new Z3Exception("Argument size mismatch");
3180  Native.Z3_parse_smtlib_file(nCtx, fileName,
3181  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3182  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
3183  }
3184 
3188  public uint NumSMTLIBFormulas { get { return Native.Z3_get_smtlib_num_formulas(nCtx); } }
3189 
3193  public BoolExpr[] SMTLIBFormulas
3194  {
3195  get
3196  {
3197  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
3198 
3199  uint n = NumSMTLIBFormulas;
3200  BoolExpr[] res = new BoolExpr[n];
3201  for (uint i = 0; i < n; i++)
3202  res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_formula(nCtx, i));
3203  return res;
3204  }
3205  }
3206 
3210  public uint NumSMTLIBAssumptions { get { return Native.Z3_get_smtlib_num_assumptions(nCtx); } }
3211 
3215  public BoolExpr[] SMTLIBAssumptions
3216  {
3217  get
3218  {
3219  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
3220 
3221  uint n = NumSMTLIBAssumptions;
3222  BoolExpr[] res = new BoolExpr[n];
3223  for (uint i = 0; i < n; i++)
3224  res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_assumption(nCtx, i));
3225  return res;
3226  }
3227  }
3228 
3232  public uint NumSMTLIBDecls { get { return Native.Z3_get_smtlib_num_decls(nCtx); } }
3233 
3237  public FuncDecl[] SMTLIBDecls
3238  {
3239  get
3240  {
3241  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
3242 
3243  uint n = NumSMTLIBDecls;
3244  FuncDecl[] res = new FuncDecl[n];
3245  for (uint i = 0; i < n; i++)
3246  res[i] = new FuncDecl(this, Native.Z3_get_smtlib_decl(nCtx, i));
3247  return res;
3248  }
3249  }
3250 
3254  public uint NumSMTLIBSorts { get { return Native.Z3_get_smtlib_num_sorts(nCtx); } }
3255 
3259  public Sort[] SMTLIBSorts
3260  {
3261  get
3262  {
3263  Contract.Ensures(Contract.Result<Sort[]>() != null);
3264 
3265  uint n = NumSMTLIBSorts;
3266  Sort[] res = new Sort[n];
3267  for (uint i = 0; i < n; i++)
3268  res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i));
3269  return res;
3270  }
3271  }
3272 
3278  public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
3279  {
3280  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3281 
3282  uint csn = Symbol.ArrayLength(sortNames);
3283  uint cs = Sort.ArrayLength(sorts);
3284  uint cdn = Symbol.ArrayLength(declNames);
3285  uint cd = AST.ArrayLength(decls);
3286  if (csn != cs || cdn != cd)
3287  throw new Z3Exception("Argument size mismatch");
3288  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
3289  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3290  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3291  }
3292 
3297  public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
3298  {
3299  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3300 
3301  uint csn = Symbol.ArrayLength(sortNames);
3302  uint cs = Sort.ArrayLength(sorts);
3303  uint cdn = Symbol.ArrayLength(declNames);
3304  uint cd = AST.ArrayLength(decls);
3305  if (csn != cs || cdn != cd)
3306  throw new Z3Exception("Argument size mismatch");
3307  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
3308  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3309  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3310  }
3311  #endregion
3312 
3313  #region Goals
3314  public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
3325  {
3326  Contract.Ensures(Contract.Result<Goal>() != null);
3327 
3328  return new Goal(this, models, unsatCores, proofs);
3329  }
3330  #endregion
3331 
3332  #region ParameterSets
3333  public Params MkParams()
3337  {
3338  Contract.Ensures(Contract.Result<Params>() != null);
3339 
3340  return new Params(this);
3341  }
3342  #endregion
3343 
3344  #region Tactics
3345  public uint NumTactics
3349  {
3350  get { return Native.Z3_get_num_tactics(nCtx); }
3351  }
3352 
3356  public string[] TacticNames
3357  {
3358  get
3359  {
3360  Contract.Ensures(Contract.Result<string[]>() != null);
3361 
3362  uint n = NumTactics;
3363  string[] res = new string[n];
3364  for (uint i = 0; i < n; i++)
3365  res[i] = Native.Z3_get_tactic_name(nCtx, i);
3366  return res;
3367  }
3368  }
3369 
3373  public string TacticDescription(string name)
3374  {
3375  Contract.Ensures(Contract.Result<string>() != null);
3376 
3377  return Native.Z3_tactic_get_descr(nCtx, name);
3378  }
3379 
3383  public Tactic MkTactic(string name)
3384  {
3385  Contract.Ensures(Contract.Result<Tactic>() != null);
3386 
3387  return new Tactic(this, name);
3388  }
3389 
3394  public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
3395  {
3396  Contract.Requires(t1 != null);
3397  Contract.Requires(t2 != null);
3398  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3399  Contract.Ensures(Contract.Result<Tactic>() != null);
3400 
3401 
3402  CheckContextMatch(t1);
3403  CheckContextMatch(t2);
3404  CheckContextMatch<Tactic>(ts);
3405 
3406  IntPtr last = IntPtr.Zero;
3407  if (ts != null && ts.Length > 0)
3408  {
3409  last = ts[ts.Length - 1].NativeObject;
3410  for (int i = ts.Length - 2; i >= 0; i--)
3411  last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3412  }
3413  if (last != IntPtr.Zero)
3414  {
3415  last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3416  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3417  }
3418  else
3419  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3420  }
3421 
3429  public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
3430  {
3431  Contract.Requires(t1 != null);
3432  Contract.Requires(t2 != null);
3433  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3434  Contract.Ensures(Contract.Result<Tactic>() != null);
3435 
3436  return AndThen(t1, t2, ts);
3437  }
3438 
3443  public Tactic OrElse(Tactic t1, Tactic t2)
3444  {
3445  Contract.Requires(t1 != null);
3446  Contract.Requires(t2 != null);
3447  Contract.Ensures(Contract.Result<Tactic>() != null);
3448 
3449  CheckContextMatch(t1);
3450  CheckContextMatch(t2);
3451  return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3452  }
3453 
3460  public Tactic TryFor(Tactic t, uint ms)
3461  {
3462  Contract.Requires(t != null);
3463  Contract.Ensures(Contract.Result<Tactic>() != null);
3464 
3465  CheckContextMatch(t);
3466  return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3467  }
3468 
3476  public Tactic When(Probe p, Tactic t)
3477  {
3478  Contract.Requires(p != null);
3479  Contract.Requires(t != null);
3480  Contract.Ensures(Contract.Result<Tactic>() != null);
3481 
3482  CheckContextMatch(t);
3483  CheckContextMatch(p);
3484  return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3485  }
3486 
3491  public Tactic Cond(Probe p, Tactic t1, Tactic t2)
3492  {
3493  Contract.Requires(p != null);
3494  Contract.Requires(t1 != null);
3495  Contract.Requires(t2 != null);
3496  Contract.Ensures(Contract.Result<Tactic>() != null);
3497 
3498  CheckContextMatch(p);
3499  CheckContextMatch(t1);
3500  CheckContextMatch(t2);
3501  return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3502  }
3503 
3508  public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
3509  {
3510  Contract.Requires(t != null);
3511  Contract.Ensures(Contract.Result<Tactic>() != null);
3512 
3513  CheckContextMatch(t);
3514  return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3515  }
3516 
3520  public Tactic Skip()
3521  {
3522  Contract.Ensures(Contract.Result<Tactic>() != null);
3523 
3524  return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3525  }
3526 
3530  public Tactic Fail()
3531  {
3532  Contract.Ensures(Contract.Result<Tactic>() != null);
3533 
3534  return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3535  }
3536 
3540  public Tactic FailIf(Probe p)
3541  {
3542  Contract.Requires(p != null);
3543  Contract.Ensures(Contract.Result<Tactic>() != null);
3544 
3545  CheckContextMatch(p);
3546  return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3547  }
3548 
3554  {
3555  Contract.Ensures(Contract.Result<Tactic>() != null);
3556 
3557  return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3558  }
3559 
3564  {
3565  Contract.Requires(t != null);
3566  Contract.Requires(p != null);
3567  Contract.Ensures(Contract.Result<Tactic>() != null);
3568 
3569  CheckContextMatch(t);
3570  CheckContextMatch(p);
3571  return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3572  }
3573 
3578  public Tactic With(Tactic t, Params p)
3579  {
3580  Contract.Requires(t != null);
3581  Contract.Requires(p != null);
3582  Contract.Ensures(Contract.Result<Tactic>() != null);
3583 
3584  return UsingParams(t, p);
3585  }
3586 
3590  public Tactic ParOr(params Tactic[] t)
3591  {
3592  Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3593  Contract.Ensures(Contract.Result<Tactic>() != null);
3594 
3595  CheckContextMatch<Tactic>(t);
3596  return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
3597  }
3598 
3604  {
3605  Contract.Requires(t1 != null);
3606  Contract.Requires(t2 != null);
3607  Contract.Ensures(Contract.Result<Tactic>() != null);
3608 
3609  CheckContextMatch(t1);
3610  CheckContextMatch(t2);
3611  return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3612  }
3613 
3618  public void Interrupt()
3619  {
3620  Native.Z3_interrupt(nCtx);
3621  }
3622  #endregion
3623 
3624  #region Probes
3625  public uint NumProbes
3629  {
3630  get { return Native.Z3_get_num_probes(nCtx); }
3631  }
3632 
3636  public string[] ProbeNames
3637  {
3638  get
3639  {
3640  Contract.Ensures(Contract.Result<string[]>() != null);
3641 
3642  uint n = NumProbes;
3643  string[] res = new string[n];
3644  for (uint i = 0; i < n; i++)
3645  res[i] = Native.Z3_get_probe_name(nCtx, i);
3646  return res;
3647  }
3648  }
3649 
3653  public string ProbeDescription(string name)
3654  {
3655  Contract.Ensures(Contract.Result<string>() != null);
3656 
3657  return Native.Z3_probe_get_descr(nCtx, name);
3658  }
3659 
3663  public Probe MkProbe(string name)
3664  {
3665  Contract.Ensures(Contract.Result<Probe>() != null);
3666 
3667  return new Probe(this, name);
3668  }
3669 
3673  public Probe ConstProbe(double val)
3674  {
3675  Contract.Ensures(Contract.Result<Probe>() != null);
3676 
3677  return new Probe(this, Native.Z3_probe_const(nCtx, val));
3678  }
3679 
3684  public Probe Lt(Probe p1, Probe p2)
3685  {
3686  Contract.Requires(p1 != null);
3687  Contract.Requires(p2 != null);
3688  Contract.Ensures(Contract.Result<Probe>() != null);
3689 
3690  CheckContextMatch(p1);
3691  CheckContextMatch(p2);
3692  return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3693  }
3694 
3699  public Probe Gt(Probe p1, Probe p2)
3700  {
3701  Contract.Requires(p1 != null);
3702  Contract.Requires(p2 != null);
3703  Contract.Ensures(Contract.Result<Probe>() != null);
3704 
3705  CheckContextMatch(p1);
3706  CheckContextMatch(p2);
3707  return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3708  }
3709 
3714  public Probe Le(Probe p1, Probe p2)
3715  {
3716  Contract.Requires(p1 != null);
3717  Contract.Requires(p2 != null);
3718  Contract.Ensures(Contract.Result<Probe>() != null);
3719 
3720  CheckContextMatch(p1);
3721  CheckContextMatch(p2);
3722  return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3723  }
3724 
3729  public Probe Ge(Probe p1, Probe p2)
3730  {
3731  Contract.Requires(p1 != null);
3732  Contract.Requires(p2 != null);
3733  Contract.Ensures(Contract.Result<Probe>() != null);
3734 
3735  CheckContextMatch(p1);
3736  CheckContextMatch(p2);
3737  return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3738  }
3739 
3744  public Probe Eq(Probe p1, Probe p2)
3745  {
3746  Contract.Requires(p1 != null);
3747  Contract.Requires(p2 != null);
3748  Contract.Ensures(Contract.Result<Probe>() != null);
3749 
3750  CheckContextMatch(p1);
3751  CheckContextMatch(p2);
3752  return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3753  }
3754 
3759  public Probe And(Probe p1, Probe p2)
3760  {
3761  Contract.Requires(p1 != null);
3762  Contract.Requires(p2 != null);
3763  Contract.Ensures(Contract.Result<Probe>() != null);
3764 
3765  CheckContextMatch(p1);
3766  CheckContextMatch(p2);
3767  return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3768  }
3769 
3774  public Probe Or(Probe p1, Probe p2)
3775  {
3776  Contract.Requires(p1 != null);
3777  Contract.Requires(p2 != null);
3778  Contract.Ensures(Contract.Result<Probe>() != null);
3779 
3780  CheckContextMatch(p1);
3781  CheckContextMatch(p2);
3782  return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3783  }
3784 
3789  public Probe Not(Probe p)
3790  {
3791  Contract.Requires(p != null);
3792  Contract.Ensures(Contract.Result<Probe>() != null);
3793 
3794  CheckContextMatch(p);
3795  return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3796  }
3797  #endregion
3798 
3799  #region Solvers
3800  public Solver MkSolver(Symbol logic = null)
3809  {
3810  Contract.Ensures(Contract.Result<Solver>() != null);
3811 
3812  if (logic == null)
3813  return new Solver(this, Native.Z3_mk_solver(nCtx));
3814  else
3815  return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3816  }
3817 
3822  public Solver MkSolver(string logic)
3823  {
3824  Contract.Ensures(Contract.Result<Solver>() != null);
3825 
3826  return MkSolver(MkSymbol(logic));
3827  }
3828 
3833  {
3834  Contract.Ensures(Contract.Result<Solver>() != null);
3835 
3836  return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3837  }
3838 
3847  {
3848  Contract.Requires(t != null);
3849  Contract.Ensures(Contract.Result<Solver>() != null);
3850 
3851  return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3852  }
3853  #endregion
3854 
3855  #region Fixedpoints
3856  public Fixedpoint MkFixedpoint()
3860  {
3861  Contract.Ensures(Contract.Result<Fixedpoint>() != null);
3862 
3863  return new Fixedpoint(this);
3864  }
3865  #endregion
3866 
3867  #region Optimization
3868  public Optimize MkOptimize()
3872  {
3873  Contract.Ensures(Contract.Result<Optimize>() != null);
3874 
3875  return new Optimize(this);
3876  }
3877  #endregion
3878 
3879  #region Floating-Point Arithmetic
3880 
3881  #region Rounding Modes
3882  #region RoundingMode Sort
3883  public FPRMSort MkFPRoundingModeSort()
3887  {
3888  Contract.Ensures(Contract.Result<FPRMSort>() != null);
3889  return new FPRMSort(this);
3890  }
3891  #endregion
3892 
3893  #region Numerals
3894  public FPRMExpr MkFPRoundNearestTiesToEven()
3898  {
3899  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3900  return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
3901  }
3902 
3906  public FPRMNum MkFPRNE()
3907  {
3908  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3909  return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
3910  }
3911 
3916  {
3917  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3918  return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
3919  }
3920 
3924  public FPRMNum MkFPRNA()
3925  {
3926  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3927  return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
3928  }
3929 
3934  {
3935  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3936  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
3937  }
3938 
3942  public FPRMNum MkFPRTP()
3943  {
3944  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3945  return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
3946  }
3947 
3952  {
3953  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3954  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
3955  }
3956 
3960  public FPRMNum MkFPRTN()
3961  {
3962  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3963  return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
3964  }
3965 
3970  {
3971  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3972  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
3973  }
3974 
3978  public FPRMNum MkFPRTZ()
3979  {
3980  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3981  return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
3982  }
3983  #endregion
3984  #endregion
3985 
3986  #region FloatingPoint Sorts
3987  public FPSort MkFPSort(uint ebits, uint sbits)
3993  {
3994  Contract.Ensures(Contract.Result<FPSort>() != null);
3995  return new FPSort(this, ebits, sbits);
3996  }
3997 
4002  {
4003  Contract.Ensures(Contract.Result<FPSort>() != null);
4004  return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
4005  }
4006 
4011  {
4012  Contract.Ensures(Contract.Result<FPSort>() != null);
4013  return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
4014  }
4015 
4020  {
4021  Contract.Ensures(Contract.Result<FPSort>() != null);
4022  return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
4023  }
4024 
4029  {
4030  Contract.Ensures(Contract.Result<FPSort>() != null);
4031  return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx));
4032  }
4033 
4038  {
4039  Contract.Ensures(Contract.Result<FPSort>() != null);
4040  return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
4041  }
4042 
4047  {
4048  Contract.Ensures(Contract.Result<FPSort>() != null);
4049  return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
4050  }
4051 
4056  {
4057  Contract.Ensures(Contract.Result<FPSort>() != null);
4058  return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
4059  }
4060 
4065  {
4066  Contract.Ensures(Contract.Result<FPSort>() != null);
4067  return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
4068  }
4069  #endregion
4070 
4071  #region Numerals
4072  public FPNum MkFPNaN(FPSort s)
4077  {
4078  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4079  return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
4080  }
4081 
4087  public FPNum MkFPInf(FPSort s, bool negative)
4088  {
4089  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4090  return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0));
4091  }
4092 
4098  public FPNum MkFPZero(FPSort s, bool negative)
4099  {
4100  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4101  return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
4102  }
4103 
4109  public FPNum MkFPNumeral(float v, FPSort s)
4110  {
4111  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4112  return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
4113  }
4114 
4120  public FPNum MkFPNumeral(double v, FPSort s)
4121  {
4122  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4123  return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
4124  }
4125 
4131  public FPNum MkFPNumeral(int v, FPSort s)
4132  {
4133  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4134  return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
4135  }
4136 
4144  public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
4145  {
4146  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4147  return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
4148  }
4149 
4157  public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
4158  {
4159  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4160  return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
4161  }
4162 
4168  public FPNum MkFP(float v, FPSort s)
4169  {
4170  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4171  return MkFPNumeral(v, s);
4172  }
4173 
4179  public FPNum MkFP(double v, FPSort s)
4180  {
4181  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4182  return MkFPNumeral(v, s);
4183  }
4184 
4190  public FPNum MkFP(int v, FPSort s)
4191  {
4192  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4193  return MkFPNumeral(v, s);
4194  }
4195 
4203  public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
4204  {
4205  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4206  return MkFPNumeral(sgn, exp, sig, s);
4207  }
4208 
4216  public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
4217  {
4218  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4219  return MkFPNumeral(sgn, exp, sig, s);
4220  }
4221 
4222  #endregion
4223 
4224  #region Operators
4225  public FPExpr MkFPAbs(FPExpr t)
4230  {
4231  Contract.Ensures(Contract.Result<FPNum>() != null);
4232  return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
4233  }
4234 
4240  {
4241  Contract.Ensures(Contract.Result<FPNum>() != null);
4242  return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
4243  }
4244 
4251  public FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
4252  {
4253  Contract.Ensures(Contract.Result<FPNum>() != null);
4254  return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4255  }
4256 
4263  public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
4264  {
4265  Contract.Ensures(Contract.Result<FPNum>() != null);
4266  return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4267  }
4268 
4275  public FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
4276  {
4277  Contract.Ensures(Contract.Result<FPNum>() != null);
4278  return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4279  }
4280 
4287  public FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
4288  {
4289  Contract.Ensures(Contract.Result<FPNum>() != null);
4290  return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4291  }
4292 
4303  public FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
4304  {
4305  Contract.Ensures(Contract.Result<FPNum>() != null);
4306  return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
4307  }
4308 
4315  {
4316  Contract.Ensures(Contract.Result<FPNum>() != null);
4317  return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
4318  }
4319 
4325  public FPExpr MkFPRem(FPExpr t1, FPExpr t2)
4326  {
4327  Contract.Ensures(Contract.Result<FPNum>() != null);
4328  return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
4329  }
4330 
4338  {
4339  Contract.Ensures(Contract.Result<FPNum>() != null);
4340  return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
4341  }
4342 
4348  public FPExpr MkFPMin(FPExpr t1, FPExpr t2)
4349  {
4350  Contract.Ensures(Contract.Result<FPNum>() != null);
4351  return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
4352  }
4353 
4359  public FPExpr MkFPMax(FPExpr t1, FPExpr t2)
4360  {
4361  Contract.Ensures(Contract.Result<FPNum>() != null);
4362  return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
4363  }
4364 
4371  {
4372  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4373  return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
4374  }
4375 
4381  public BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
4382  {
4383  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4384  return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
4385  }
4386 
4393  {
4394  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4395  return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
4396  }
4397 
4403  public BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
4404  {
4405  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4406  return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
4407  }
4408 
4417  public BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
4418  {
4419  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4420  return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
4421  }
4422 
4428  {
4429  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4430  return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
4431  }
4432 
4438  {
4439  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4440  return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
4441  }
4442 
4448  {
4449  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4450  return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
4451  }
4452 
4458  {
4459  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4460  return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
4461  }
4462 
4468  {
4469  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4470  return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
4471  }
4472 
4478  {
4479  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4480  return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
4481  }
4482 
4488  {
4489  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4490  return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
4491  }
4492  #endregion
4493 
4494  #region Conversions to FloatingPoint terms
4495  public FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
4509  {
4510  Contract.Ensures(Contract.Result<FPExpr>() != null);
4511  return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
4512  }
4513 
4526  {
4527  Contract.Ensures(Contract.Result<FPExpr>() != null);
4528  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
4529  }
4530 
4543  {
4544  Contract.Ensures(Contract.Result<FPExpr>() != null);
4545  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4546  }
4547 
4560  {
4561  Contract.Ensures(Contract.Result<FPExpr>() != null);
4562  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4563  }
4564 
4578  public FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
4579  {
4580  Contract.Ensures(Contract.Result<FPExpr>() != null);
4581  if (signed)
4582  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4583  else
4584  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4585  }
4586 
4598  {
4599  Contract.Ensures(Contract.Result<FPExpr>() != null);
4600  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
4601  }
4602  #endregion
4603 
4604  #region Conversions from FloatingPoint terms
4605  public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed)
4618  {
4619  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4620  if (signed)
4621  return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4622  else
4623  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4624  }
4625 
4636  {
4637  Contract.Ensures(Contract.Result<RealExpr>() != null);
4638  return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
4639  }
4640  #endregion
4641 
4642  #region Z3-specific extensions
4643  public BitVecExpr MkFPToIEEEBV(FPExpr t)
4654  {
4655  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4656  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
4657  }
4658 
4672  {
4673  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4674  return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
4675  }
4676  #endregion
4677  #endregion // Floating-point Arithmetic
4678 
4679  #region Miscellaneous
4680  public AST WrapAST(IntPtr nativeObject)
4691  {
4692  Contract.Ensures(Contract.Result<AST>() != null);
4693  return AST.Create(this, nativeObject);
4694  }
4695 
4707  public IntPtr UnwrapAST(AST a)
4708  {
4709  return a.NativeObject;
4710  }
4711 
4715  public string SimplifyHelp()
4716  {
4717  Contract.Ensures(Contract.Result<string>() != null);
4718 
4719  return Native.Z3_simplify_get_help(nCtx);
4720  }
4721 
4725  public ParamDescrs SimplifyParameterDescriptions
4726  {
4727  get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
4728  }
4729  #endregion
4730 
4731  #region Error Handling
4732  //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
4740 
4744  //public event ErrorHandler OnError = null;
4745  #endregion
4746 
4747  #region Parameters
4748  public void UpdateParamValue(string id, string value)
4758  {
4759  Native.Z3_update_param_value(nCtx, id, value);
4760  }
4761 
4762  #endregion
4763 
4764  #region Internal
4765  internal IntPtr m_ctx = IntPtr.Zero;
4766  internal Native.Z3_error_handler m_n_err_handler = null;
4767  internal static Object creation_lock = new Object();
4768  internal IntPtr nCtx { get { return m_ctx; } }
4769 
4770  internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
4771  {
4772  // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
4773  }
4774 
4775  internal void InitContext()
4776  {
4777  PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
4778  m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
4779  Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
4780  GC.SuppressFinalize(this);
4781  }
4782 
4783  [Pure]
4784  internal void CheckContextMatch(Z3Object other)
4785  {
4786  Contract.Requires(other != null);
4787 
4788  if (!ReferenceEquals(this, other.Context))
4789  throw new Z3Exception("Context mismatch");
4790  }
4791 
4792  [Pure]
4793  internal void CheckContextMatch(Z3Object other1, Z3Object other2)
4794  {
4795  Contract.Requires(other1 != null);
4796  Contract.Requires(other2 != null);
4797  CheckContextMatch(other1);
4798  CheckContextMatch(other2);
4799  }
4800 
4801  [Pure]
4802  internal void CheckContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
4803  {
4804  Contract.Requires(other1 != null);
4805  Contract.Requires(other2 != null);
4806  Contract.Requires(other3 != null);
4807  CheckContextMatch(other1);
4808  CheckContextMatch(other2);
4809  CheckContextMatch(other3);
4810  }
4811 
4812  [Pure]
4813  internal void CheckContextMatch(Z3Object[] arr)
4814  {
4815  Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
4816 
4817  if (arr != null)
4818  {
4819  foreach (Z3Object a in arr)
4820  {
4821  Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
4822  CheckContextMatch(a);
4823  }
4824  }
4825  }
4826 
4827  [Pure]
4828  internal void CheckContextMatch<T>(IEnumerable<T> arr) where T : Z3Object
4829  {
4830  Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
4831 
4832  if (arr != null)
4833  {
4834  foreach (Z3Object a in arr)
4835  {
4836  Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
4837  CheckContextMatch(a);
4838  }
4839  }
4840  }
4841 
4843  private void ObjectInvariant()
4844  {
4845  Contract.Invariant(m_AST_DRQ != null);
4846  Contract.Invariant(m_ASTMap_DRQ != null);
4847  Contract.Invariant(m_ASTVector_DRQ != null);
4848  Contract.Invariant(m_ApplyResult_DRQ != null);
4849  Contract.Invariant(m_FuncEntry_DRQ != null);
4850  Contract.Invariant(m_FuncInterp_DRQ != null);
4851  Contract.Invariant(m_Goal_DRQ != null);
4852  Contract.Invariant(m_Model_DRQ != null);
4853  Contract.Invariant(m_Params_DRQ != null);
4854  Contract.Invariant(m_ParamDescrs_DRQ != null);
4855  Contract.Invariant(m_Probe_DRQ != null);
4856  Contract.Invariant(m_Solver_DRQ != null);
4857  Contract.Invariant(m_Statistics_DRQ != null);
4858  Contract.Invariant(m_Tactic_DRQ != null);
4859  Contract.Invariant(m_Fixedpoint_DRQ != null);
4860  Contract.Invariant(m_Optimize_DRQ != null);
4861  }
4862 
4863  readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
4864  readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue(10);
4865  readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue(10);
4866  readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue(10);
4867  readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue(10);
4868  readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue(10);
4869  readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue(10);
4870  readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue(10);
4871  readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue(10);
4872  readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue(10);
4873  readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue(10);
4874  readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue(10);
4875  readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10);
4876  readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
4877  readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
4878  readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10);
4879 
4883  public IDecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result<AST.DecRefQueue>() != null); return m_AST_DRQ; } }
4884 
4888  public IDecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null); return m_ASTMap_DRQ; } }
4889 
4893  public IDecRefQueue ASTVector_DRQ { get { Contract.Ensures(Contract.Result<ASTVector.DecRefQueue>() != null); return m_ASTVector_DRQ; } }
4894 
4898  public IDecRefQueue ApplyResult_DRQ { get { Contract.Ensures(Contract.Result<ApplyResult.DecRefQueue>() != null); return m_ApplyResult_DRQ; } }
4899 
4903  public IDecRefQueue FuncEntry_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.Entry.DecRefQueue>() != null); return m_FuncEntry_DRQ; } }
4904 
4908  public IDecRefQueue FuncInterp_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.DecRefQueue>() != null); return m_FuncInterp_DRQ; } }
4909 
4913  public IDecRefQueue Goal_DRQ { get { Contract.Ensures(Contract.Result<Goal.DecRefQueue>() != null); return m_Goal_DRQ; } }
4914 
4918  public IDecRefQueue Model_DRQ { get { Contract.Ensures(Contract.Result<Model.DecRefQueue>() != null); return m_Model_DRQ; } }
4919 
4923  public IDecRefQueue Params_DRQ { get { Contract.Ensures(Contract.Result<Params.DecRefQueue>() != null); return m_Params_DRQ; } }
4924 
4928  public IDecRefQueue ParamDescrs_DRQ { get { Contract.Ensures(Contract.Result<ParamDescrs.DecRefQueue>() != null); return m_ParamDescrs_DRQ; } }
4929 
4933  public IDecRefQueue Probe_DRQ { get { Contract.Ensures(Contract.Result<Probe.DecRefQueue>() != null); return m_Probe_DRQ; } }
4934 
4938  public IDecRefQueue Solver_DRQ { get { Contract.Ensures(Contract.Result<Solver.DecRefQueue>() != null); return m_Solver_DRQ; } }
4939 
4943  public IDecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result<Statistics.DecRefQueue>() != null); return m_Statistics_DRQ; } }
4944 
4948  public IDecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result<Tactic.DecRefQueue>() != null); return m_Tactic_DRQ; } }
4949 
4953  public IDecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
4954 
4958  public IDecRefQueue Optimize_DRQ { get { Contract.Ensures(Contract.Result<Optimize.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
4959 
4960 
4961  internal long refCount = 0;
4962 
4966  ~Context()
4967  {
4968  // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4969  Dispose();
4970 
4971  if (refCount == 0 && m_ctx != IntPtr.Zero)
4972  {
4973  m_n_err_handler = null;
4974  IntPtr ctx = m_ctx;
4975  m_ctx = IntPtr.Zero;
4976  Native.Z3_del_context(ctx);
4977  }
4978  else
4979  GC.ReRegisterForFinalize(this);
4980  }
4981 
4985  public void Dispose()
4986  {
4987  // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4988  AST_DRQ.Clear(this);
4989  ASTMap_DRQ.Clear(this);
4990  ASTVector_DRQ.Clear(this);
4991  ApplyResult_DRQ.Clear(this);
4992  FuncEntry_DRQ.Clear(this);
4993  FuncInterp_DRQ.Clear(this);
4994  Goal_DRQ.Clear(this);
4995  Model_DRQ.Clear(this);
4996  Params_DRQ.Clear(this);
4997  ParamDescrs_DRQ.Clear(this);
4998  Probe_DRQ.Clear(this);
4999  Solver_DRQ.Clear(this);
5000  Statistics_DRQ.Clear(this);
5001  Tactic_DRQ.Clear(this);
5002  Fixedpoint_DRQ.Clear(this);
5003  Optimize_DRQ.Clear(this);
5004 
5005  m_boolSort = null;
5006  m_intSort = null;
5007  m_realSort = null;
5008  m_stringSort = null;
5009  }
5010  #endregion
5011  }
5012 }
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:967
BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement signed remainder (sign follows divisor).
Definition: Context.cs:1537
string SimplifyHelp()
Return a string describing all available parameters to Expr.Simplify.
Definition: Context.cs:4715
BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
Floating-point less than or equal.
Definition: Context.cs:4370
Object for managing optimizization context
Definition: Optimize.cs:30
FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Definition: Context.cs:4542
FPExpr MkFPRem(FPExpr t1, FPExpr t2)
Floating-point remainder
Definition: Context.cs:4325
BoolExpr MkIsInteger(RealExpr t)
Creates an expression that checks whether a real number is an integer.
Definition: Context.cs:1248
FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
Conversion of a 2&#39;s complement signed bit-vector term into a term of FloatingPoint sort...
Definition: Context.cs:4578
def SeqSort(s)
Definition: z3py.py:9357
FPRMNum MkFPRNE()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode...
Definition: Context.cs:3906
FloatiungPoint Numerals
Definition: FPNum.cs:28
FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point division
Definition: Context.cs:4287
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
Bitwise conjunction.
Definition: Context.cs:1302
Lists of constructors
DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
Create a new datatype sort.
Definition: Context.cs:417
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:2701
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:3383
BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean less-or-equal constraint.
Definition: Context.cs:2632
SeqExpr MkConcat(params SeqExpr[] t)
Concatentate sequences.
Definition: Context.cs:2426
UninterpretedSort MkUninterpretedSort(string str)
Create a new uninterpreted sort.
Definition: Context.cs:206
RealExpr MkFPToReal(FPExpr t)
Conversion of a floating-point term into a real-numbered term.
Definition: Context.cs:4635
FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
Definition: Context.cs:4559
FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
Create a new finite domain sort. The result is a sort
Definition: Context.cs:353
FPRMNum MkFPRTN()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode...
Definition: Context.cs:3960
ArrayExpr MkConstArray(Sort domain, Expr v)
Create a constant array.
Definition: Context.cs:2179
string ProbeDescription(string name)
Returns a string containing a description of the probe with the given name.
Definition: Context.cs:3653
FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Floating-point fused multiply-add
Definition: Context.cs:4303
BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
Unsigned greater than or equal to.
Definition: Context.cs:1622
def ReSort(s)
Definition: z3py.py:9584
def RealSort(ctx=None)
Definition: z3py.py:2721
Bit-vector sorts.
Definition: BitVecSort.cs:28
RatNum MkReal(string v)
Create a real numeral.
Definition: Context.cs:2767
Expr MkFreshConst(string prefix, Sort range)
Creates a fresh Constant of sort range and a name prefixed with prefix .
Definition: Context.cs:696
FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two integers.
Definition: Context.cs:4203
SeqExpr MkUnit(Expr elem)
Create the singleton sequence.
Definition: Context.cs:2406
def AndThen(ts, ks)
Definition: z3py.py:7049
BitVecNum MkBV(long v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2926
FPExpr MkFPMax(FPExpr t1, FPExpr t2)
Maximum of floating-point numbers.
Definition: Context.cs:4359
BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
Check for set membership.
Definition: Context.cs:2364
Probe Not(Probe p)
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
Definition: Context.cs:3789
Bit-vector numerals
Definition: BitVecNum.cs:32
Array sorts.
Definition: ArraySort.cs:29
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Unsigned division.
Definition: Context.cs:1455
Definition: FuncInterp.cs:92
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:3476
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:3508
BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement signed greater than or equal to.
Definition: Context.cs:1639
BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
Bit-vector extraction.
Definition: Context.cs:1714
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:3729
IntExpr MkIntConst(Symbol name)
Creates an integer constant.
Definition: Context.cs:741
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:3278
IntNum MkInt(int v)
Create an integer numeral.
Definition: Context.cs:2840
Tactic ParOr(params Tactic[] t)
Create a tactic that applies the given tactics in parallel until one of them succeeds (i...
Definition: Context.cs:3590
BitVecExpr MkBVNeg(BitVecExpr t)
Standard two&#39;s complement unary minus.
Definition: Context.cs:1392
ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
Maps f on the argument arrays.
Definition: Context.cs:2201
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1286
Boolean expressions
Definition: BoolExpr.cs:31
ReExpr MOption(ReExpr re)
Create the optional regular expression.
Definition: Context.cs:2580
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4109
void Interrupt()
Interrupt the execution of a Z3 procedure.
Definition: Context.cs:3618
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:3714
Objects of this class track statistical information about solvers.
Definition: Statistics.cs:29
FPRMNum MkFPRTZ()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode...
Definition: Context.cs:3978
ReSort MkReSort(SeqSort s)
Create a new regular expression sort.
Definition: Context.cs:256
FPNum MkFPInf(FPSort s, bool negative)
Create a floating-point infinity of sort s.
Definition: Context.cs:4087
Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
Create an expression representing an if-then-else: ite(t1, t2, t3).
Definition: Context.cs:909
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:3017
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:2733
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. The result is a sortElements of the sort are created using MkNumeral...
Definition: Context.cs:370
Expr MkConst(string name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:684
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
Definition: Context.cs:1099
FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:562
BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
Unsigned greater-than.
Definition: Context.cs:1656
FPSort MkFPSortSingle()
Create the single-precision (32-bit) FloatingPoint sort.
Definition: Context.cs:4019
Floating-point rounding mode numerals
Definition: FPRMNum.cs:31
BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than or equal to.
Definition: Context.cs:1588
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
Definition: Context.cs:1157
BoolExpr MkBoolConst(Symbol name)
Create a Boolean constant.
Definition: Context.cs:720
IntNum MkInt(uint v)
Create an integer numeral.
Definition: Context.cs:2852
SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
Replace the first occurrence of src by dst in s.
Definition: Context.cs:2524
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:3394
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:3155
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:3040
BoolExpr MkEq(Expr x, Expr y)
Creates the equality x = y .
Definition: Context.cs:866
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:3759
Expr MkApp(FuncDecl f, IEnumerable< Expr > args)
Create a new function application.
Definition: Context.cs:821
def StringSort(ctx=None)
Definition: z3py.py:9347
ListSort MkListSort(Symbol name, Sort elemSort)
Create a new list sort.
Definition: Context.cs:324
BoolExpr MkFPIsNaN(FPExpr t)
Predicate indicating whether t is a NaN.
Definition: Context.cs:4467
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
Definition: Context.cs:1171
ArrayExpr MkFullSet(Sort domain)
Create the full set.
Definition: Context.cs:2272
DatatypeSort [] MkDatatypeSorts(string[] names, Constructor[][] c)
Create mutually recursive data-types.
Definition: Context.cs:483
ReExpr MPlus(ReExpr re)
Take the Kleene plus of a regular expression.
Definition: Context.cs:2570
Tactics are the basic building block for creating custom solvers for specific problem domains...
Definition: Tactic.cs:32
FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two integers.
Definition: Context.cs:4144
FPRMNum MkFPRoundTowardZero()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode...
Definition: Context.cs:3969
Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned...
Definition: Context.cs:2231
FPSort MkFPSort16()
Create the half-precision (16-bit) FloatingPoint sort.
Definition: Context.cs:4010
FPNum MkFP(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition: Context.cs:4190
FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
Creates a fresh function declaration with a name prefixed with prefix .
Definition: Context.cs:579
BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise subtraction does not overflow.
Definition: Context.cs:1995
BoolExpr MkBoolConst(string name)
Create a Boolean constant.
Definition: Context.cs:731
BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise signed division does not overflow.
Definition: Context.cs:2029
List sorts.
Definition: ListSort.cs:29
FuncDecl MkFreshConstDecl(string prefix, Sort range)
Creates a fresh constant function declaration with a name prefixed with prefix .
Definition: Context.cs:621
FuncDecl MkConstDecl(Symbol name, Sort range)
Creates a new constant function declaration.
Definition: Context.cs:593
ArithExpr MkMul(IEnumerable< ArithExpr > t)
Create an expression representing t[0] * t[1] * ....
Definition: Context.cs:1061
ReExpr MkToRe(SeqExpr s)
Convert a regular expression that accepts sequence s.
Definition: Context.cs:2537
Solver MkSolver(string logic)
Creates a new (incremental) solver.
Definition: Context.cs:3822
ArrayExpr MkSetComplement(ArrayExpr arg)
Take the complement of a set.
Definition: Context.cs:2352
BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Rotate Right.
Definition: Context.cs:1901
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:3684
A Boolean sort.
Definition: BoolSort.cs:28
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:2717
BoolExpr MkAtMost(BoolExpr[] args, uint k)
Create an at-most-k constraint.
Definition: Context.cs:2620
RatNum MkReal(int v)
Create a real numeral.
Definition: Context.cs:2779
FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:531
Vectors of ASTs.
Definition: ASTVector.cs:28
FPExpr MkFPNeg(FPExpr t)
Floating-point negation
Definition: Context.cs:4239
DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
Create a new datatype sort.
Definition: Context.cs:433
BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XNOR.
Definition: Context.cs:1377
BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Rotate Left.
Definition: Context.cs:1883
BitVecExpr MkBVRedAND(BitVecExpr t)
Take conjunction of bits in a vector, return vector of length 1.
Definition: Context.cs:1276
BoolExpr MkFPIsInfinite(FPExpr t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.
Definition: Context.cs:4457
BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement signed less-than
Definition: Context.cs:1571
FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Definition: Context.cs:4525
Expressions are terms.
Definition: Expr.cs:29
RealExpr MkRealConst(string name)
Creates a real constant.
Definition: Context.cs:774
RealSort MkRealSort()
Create a real sort.
Definition: Context.cs:226
FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
Definition: Context.cs:4157
BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise NOR.
Definition: Context.cs:1362
string TacticDescription(string name)
Returns a string containing a description of the tactic with the given name.
Definition: Context.cs:3373
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6563
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:2685
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3563
FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Conversion of a floating-point number to another FloatingPoint sort s.
Definition: Context.cs:4597
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
Definition: Context.cs:1074
FuncDecl MkConstDecl(string name, Sort range)
Creates a new constant function declaration.
Definition: Context.cs:607
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:3603
BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement addition.
Definition: Context.cs:1405
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:235
BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Signed division.
Definition: Context.cs:1479
ArrayExpr MkSetUnion(params ArrayExpr[] args)
Take the union of a list of sets.
Definition: Context.cs:2313
Solver MkSolver(Tactic t)
Creates a solver that is implemented using the given tactic.
Definition: Context.cs:3846
A real sort
Definition: RealSort.cs:28
ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
Create an array constant.
Definition: Context.cs:2107
StringSymbol MkSymbol(string name)
Create a symbol using a string.
Definition: Context.cs:101
Integer Numerals
Definition: IntNum.cs:32
FPSort MkFPSort128()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition: Context.cs:4064
BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XOR.
Definition: Context.cs:1332
BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Logical shift right
Definition: Context.cs:1808
BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise subtraction does not underflow.
Definition: Context.cs:2012
BitVecExpr MkSignExt(uint i, BitVecExpr t)
Bit-vector sign extension.
Definition: Context.cs:1731
Bit-vector expressions
Definition: BitVecExpr.cs:31
FPNum MkFPZero(FPSort s, bool negative)
Create a floating-point zero of sort s.
Definition: Context.cs:4098
ArithExpr MkAdd(IEnumerable< ArithExpr > t)
Create an expression representing t[0] + t[1] + ....
Definition: Context.cs:1035
BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise addition does not underflow.
Definition: Context.cs:1978
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
Definition: Context.cs:992
FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point addition
Definition: Context.cs:4251
FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
Definition: Context.cs:4216
BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement signed greater-than.
Definition: Context.cs:1673
ArrayExpr MkEmptySet(Sort domain)
Create an empty set.
Definition: Context.cs:2260
BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise multiplication does not overflow.
Definition: Context.cs:2061
BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
Floating-point equality.
Definition: Context.cs:4417
Constructors are used for datatype sorts.
Definition: Constructor.cs:29
A regular expression sort
Definition: ReSort.cs:28
Probe MkProbe(string name)
Creates a new Probe.
Definition: Context.cs:3663
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
Shift left.
Definition: Context.cs:1785
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
Bitwise disjunction.
Definition: Context.cs:1317
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition: z3_api.h:1261
FloatingPoint Expressions
Definition: FPExpr.cs:31
BitVecExpr MkBVConst(Symbol name, uint size)
Creates a bit-vector constant.
Definition: Context.cs:784
The FloatingPoint RoundingMode sort
Definition: FPRMSort.cs:28
FPNum MkFP(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4179
Array expressions
Definition: ArrayExpr.cs:31
IntExpr MkLength(SeqExpr s)
Retrieve the length of a given sequence.
Definition: Context.cs:2440
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:3443
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition: Context.cs:266
An Integer sort
Definition: IntSort.cs:28
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556
BoolSort MkBoolSort()
Create a new Boolean sort.
Definition: Context.cs:185
BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
Arithmetic shift right
Definition: Context.cs:1833
FPRMNum MkFPRoundNearestTiesToAway()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
Definition: Context.cs:3915
BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement signed less-than or equal to.
Definition: Context.cs:1605
BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
Rotate Right.
Definition: Context.cs:1867
SeqExpr MkAt(SeqExpr s, IntExpr index)
Retrieve sequence of length one at index.
Definition: Context.cs:2486
EnumSort MkEnumSort(string name, params string[] enumNames)
Create a new enumeration sort.
Definition: Context.cs:313
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
Definition: ApplyResult.cs:30
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 -> t2.
Definition: Context.cs:939
BoolExpr MkFPIsNegative(FPExpr t)
Predicate indicating whether t is a negative floating-point number.
Definition: Context.cs:4477
BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise multiplication does not underflow.
Definition: Context.cs:2078
A Sequence sort
Definition: SeqSort.cs:28
Enumeration sorts.
Definition: EnumSort.cs:29
FPRMNum MkFPRoundTowardPositive()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode...
Definition: Context.cs:3933
FPSort MkFPSortDouble()
Create the double-precision (64-bit) FloatingPoint sort.
Definition: Context.cs:4037
BitVecExpr MkRepeat(uint i, BitVecExpr t)
Bit-vector repetition.
Definition: Context.cs:1764
Constructor MkConstructor(string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
Create a datatype constructor.
Definition: Context.cs:407
BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
Check for sequence containment of s2 in s1.
Definition: Context.cs:2474
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:3774
SeqExpr MkEmptySeq(Sort s)
Create the empty sequence.
Definition: Context.cs:2396
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
Definition: Context.cs:1048
ArrayExpr MkSetDel(ArrayExpr set, Expr element)
Remove an element from a set.
Definition: Context.cs:2299
A Params objects 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:338
BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise addition does not overflow.
Definition: Context.cs:1961
BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
Floating-point less than.
Definition: Context.cs:4381
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:3080
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
Quantifier expressions.
Definition: Quantifier.cs:29
BitVecNum MkBV(int v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2902
DecRefQueue interface
Definition: IDecRefQueue.cs:32
def ArraySort(d, r)
Definition: z3py.py:4110
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:29
BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than
Definition: Context.cs:1554
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition: Context.cs:953
def IntSort(ctx=None)
Definition: z3py.py:2705
BoolExpr MkBVNegNoOverflow(BitVecExpr t)
Create a predicate that checks that the bit-wise negation does not overflow.
Definition: Context.cs:2046
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:3744
BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
Bit-vector concatenation.
Definition: Context.cs:1694
RealExpr MkInt2Real(IntExpr t)
Coerce an integer to a real.
Definition: Context.cs:1220
FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point multiplication
Definition: Context.cs:4275
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4574
IntExpr MkIntConst(string name)
Creates an integer constant.
Definition: Context.cs:752
BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
Floating-point greater than.
Definition: Context.cs:4403
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:297
Tactic FailIf(Probe p)
Create a tactic that fails if the probe p evaluates to false.
Definition: Context.cs:3540
BitVecNum MkBV(uint v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2914
BitVecExpr MkBVRedOR(BitVecExpr t)
Take disjunction of bits in a vector, return vector of length 1.
Definition: Context.cs:1289
TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Create a new tuple sort.
Definition: Context.cs:280
FPExpr MkFPMin(FPExpr t1, FPExpr t2)
Minimum of floating-point numbers.
Definition: Context.cs:4348
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:2998
BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean equal constraint.
Definition: Context.cs:2647
SeqSort MkSeqSort(Sort s)
Create a new sequence sort.
Definition: Context.cs:246
BoolExpr MkOr(IEnumerable< BoolExpr > t)
Create an expression representing t[0] or t[1] or ....
Definition: Context.cs:1006
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 iff t2.
Definition: Context.cs:925
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
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:3429
FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.
Definition: Context.cs:4337
BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
Signed remainder.
Definition: Context.cs:1519
Tactic Fail()
Create a tactic always fails.
Definition: Context.cs:3530
BitVecExpr MkInt2BV(uint n, IntExpr t)
Create an n bit bit-vector from the integer argument t .
Definition: Context.cs:1922
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:894
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
Definition: Context.cs:1087
BoolExpr MkFPIsSubnormal(FPExpr t)
Predicate indicating whether t is a subnormal floating-point number.
Definition: Context.cs:4437
FPRMNum MkFPRTP()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode...
Definition: Context.cs:3942
ReExpr MkConcat(params ReExpr[] t)
Create the concatenation of regular languages.
Definition: Context.cs:2590
BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Check for subsetness of sets.
Definition: Context.cs:2378
FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
Floating-point square root
Definition: Context.cs:4314
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:31
ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 ^ t2.
Definition: Context.cs:1143
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:30
Expr MkTermArray(ArrayExpr array)
Access the array default value.
Definition: Context.cs:2219
RatNum MkReal(ulong v)
Create a real numeral.
Definition: Context.cs:2815
ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
Array update.
Definition: Context.cs:2157
ReExpr MkUnion(params ReExpr[] t)
Create the union of regular languages.
Definition: Context.cs:2603
Rational Numerals
Definition: RatNum.cs:32
FPNum MkFPNumeral(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4120
Tactic With(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3578
The abstract syntax tree (AST) class.
Definition: AST.cs:31
FPSort MkFPSortQuadruple()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition: Context.cs:4055
FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point subtraction
Definition: Context.cs:4263
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3530
RealExpr MkRealConst(Symbol name)
Creates a real constant.
Definition: Context.cs:763
IntNum MkInt(ulong v)
Create an integer numeral.
Definition: Context.cs:2876
FloatingPoint RoundingMode Expressions
Definition: FPRMExpr.cs:31
FPRMNum MkFPRoundTowardNegative()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode...
Definition: Context.cs:3951
ArrayExpr MkSetIntersection(params ArrayExpr[] args)
Take the intersection of a list of sets.
Definition: Context.cs:2325
IntPtr UnwrapAST(AST a)
Unwraps an AST.
Definition: Context.cs:4707
Object for managing fixedpoints
Definition: Fixedpoint.cs:29
ReExpr MkStar(ReExpr re)
Take the Kleene star of a regular expression.
Definition: Context.cs:2560
FPNum MkFP(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4168
Probe ConstProbe(double val)
Create a probe that always evaluates to val .
Definition: Context.cs:3673
IntExpr MkBV2Int(BitVecExpr t, bool signed)
Create an integer from the bit-vector argument t .
Definition: Context.cs:1946
BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
Unsigned remainder.
Definition: Context.cs:1498
Sequence expressions
Definition: SeqExpr.cs:31
SeqExpr MkString(string s)
Create a string constant.
Definition: Context.cs:2416
RatNum MkReal(long v)
Create a real numeral.
Definition: Context.cs:2803
IntNum MkInt(long v)
Create an integer numeral.
Definition: Context.cs:2864
Expr MkSelect(ArrayExpr a, Expr i)
Array read.
Definition: Context.cs:2129
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:3172
Regular expression expressions
Definition: ReExpr.cs:31
BoolExpr MkFPIsNormal(FPExpr t)
Predicate indicating whether t is a normal floating-point number.
Definition: Context.cs:4427
FPNum MkFPNumeral(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition: Context.cs:4131
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:3491
Tactic FailIfNotDecided()
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatis...
Definition: Context.cs:3553
SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
Extract subsequence.
Definition: Context.cs:2498
BoolExpr MkFalse()
The false Term.
Definition: Context.cs:846
BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
Check for sequence suffix.
Definition: Context.cs:2462
Set sorts.
Definition: SetSort.cs:29
ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
Add an element to the set.
Definition: Context.cs:2284
BoolExpr MkFPIsZero(FPExpr t)
Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0...
Definition: Context.cs:4447
Tactic TryFor(Tactic t, uint ms)
Create a tactic that applies t to a goal for ms milliseconds.
Definition: Context.cs:3460
BitVecExpr MkBVConst(string name, uint size)
Creates a bit-vector constant.
Definition: Context.cs:795
BitVecNum MkBV(ulong v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2938
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:3699
IntExpr MkRem(IntExpr t1, IntExpr t2)
Create an expression representing t1 rem t2.
Definition: Context.cs:1129
FPSort MkFPSort32()
Create the single-precision (32-bit) FloatingPoint sort.
Definition: Context.cs:4028
ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Take the difference between two sets.
Definition: Context.cs:2338
Tactic Skip()
Create a tactic that just returns the given goal.
Definition: Context.cs:3520
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
FPSort MkFPSortHalf()
Create the half-precision (16-bit) FloatingPoint sort.
Definition: Context.cs:4001
FloatingPoint sort
Definition: FPSort.cs:27
IntExpr MkReal2Int(RealExpr t)
Coerce a real to an integer.
Definition: Context.cs:1236
BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement subtraction.
Definition: Context.cs:1420
void Dispose()
Disposes of the context.
Definition: Context.cs:4985
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
Definition: Context.cs:880
FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:548
FPSort MkFPSort64()
Create the double-precision (64-bit) FloatingPoint sort.
Definition: Context.cs:4046
Int expressions
Definition: IntExpr.cs:31
Context(Dictionary< string, string > settings)
Constructor.
Definition: Context.cs:66
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:3056
BoolExpr MkAnd(IEnumerable< BoolExpr > t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:980
FPRMNum MkFPRNA()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
Definition: Context.cs:3924
BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
Bitwise NAND.
Definition: Context.cs:1347
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Numbered symbols
Definition: IntSymbol.cs:30
Function declarations.
Definition: FuncDecl.cs:29
Solver MkSimpleSolver()
Creates a new (incremental) solver.
Definition: Context.cs:3832
BitVecExpr MkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint s...
Definition: Context.cs:4671
DatatypeSort [] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition: Context.cs:448
BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement multiplication.
Definition: Context.cs:1435
BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
Floating-point greater than or equal.
Definition: Context.cs:4392
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
Definition: Context.cs:1199
BoolExpr MkInRe(SeqExpr s, ReExpr re)
Check for regular expression membership.
Definition: Context.cs:2548
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
Definition: Context.cs:194
Solvers.
Definition: Solver.cs:30
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
Definition: Context.cs:1185
IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Extract index of sub-string starting at offset.
Definition: Context.cs:2511
Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
Update a datatype field at expression t with value v. The function performs a record update at t...
Definition: Context.cs:501
An Entry object represents an element in the finite map used to encode a function interpretation...
Definition: FuncInterp.cs:36
IntExpr MkMod(IntExpr t1, IntExpr t2)
Create an expression representing t1 mod t2.
Definition: Context.cs:1114
Tuple sorts.
Definition: TupleSort.cs:29
BoolExpr MkFPIsPositive(FPExpr t)
Predicate indicating whether t is a positive floating-point number.
Definition: Context.cs:4487
def BoolSort(ctx=None)
Definition: z3py.py:1407
BoolExpr MkBool(bool value)
Creates a Boolean value.
Definition: Context.cs:856
BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
Rotate Left.
Definition: Context.cs:1851
IntSort MkIntSort()
Create a new integer sort.
Definition: Context.cs:216
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:1749
Real expressions
Definition: RealExpr.cs:31
RatNum MkReal(uint v)
Create a real numeral.
Definition: Context.cs:2791
A function interpretation is represented as a finite map and an &#39;else&#39; value. Each entry in the finit...
Definition: FuncInterp.cs:30
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:3297
Expr MkConst(FuncDecl f)
Creates a fresh constant from the FuncDecl f .
Definition: Context.cs:709
BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
Check for sequence prefix.
Definition: Context.cs:2450