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;
23 using System.Diagnostics.Contracts;
24 
25 namespace Microsoft.Z3
26 {
30  [ContractVerification(true)]
31  public class Context : IDisposable
32  {
33  #region Constructors
34  public Context()
38  : base()
39  {
40  m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
41  InitContext();
42  }
43 
62  public Context(Dictionary<string, string> settings)
63  : base()
64  {
65  Contract.Requires(settings != null);
66 
67  IntPtr cfg = Native.Z3_mk_config();
68  foreach (KeyValuePair<string, string> kv in settings)
69  Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
70  m_ctx = Native.Z3_mk_context_rc(cfg);
71  Native.Z3_del_config(cfg);
72  InitContext();
73  }
74  #endregion
75 
76  #region Symbols
77  public IntSymbol MkSymbol(int i)
85  {
86  Contract.Ensures(Contract.Result<IntSymbol>() != null);
87 
88  return new IntSymbol(this, i);
89  }
90 
94  public StringSymbol MkSymbol(string name)
95  {
96  Contract.Ensures(Contract.Result<StringSymbol>() != null);
97 
98  return new StringSymbol(this, name);
99  }
100 
104  internal Symbol[] MkSymbols(string[] names)
105  {
106  Contract.Ensures(names == null || Contract.Result<Symbol[]>() != null);
107  Contract.Ensures(names != null || Contract.Result<Symbol[]>() == null);
108  Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.Result<Symbol[]>().Length == names.Length);
109  Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.ForAll(Contract.Result<Symbol[]>(), s => s != null));
110 
111  if (names == null) return null;
112  Symbol[] result = new Symbol[names.Length];
113  for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
114  return result;
115  }
116  #endregion
117 
118  #region Sorts
119  private BoolSort m_boolSort = null;
120  private IntSort m_intSort = null;
121  private RealSort m_realSort = null;
122 
126  public BoolSort BoolSort
127  {
128  get
129  {
130  Contract.Ensures(Contract.Result<BoolSort>() != null);
131  if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
132  }
133  }
134 
138  public IntSort IntSort
139  {
140  get
141  {
142  Contract.Ensures(Contract.Result<IntSort>() != null);
143  if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
144  }
145  }
146 
147 
151  public RealSort RealSort
152  {
153  get
154  {
155  Contract.Ensures(Contract.Result<RealSort>() != null);
156  if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
157  }
158  }
159 
164  {
165  Contract.Ensures(Contract.Result<BoolSort>() != null);
166  return new BoolSort(this);
167  }
168 
173  {
174  Contract.Requires(s != null);
175  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
176 
177  CheckContextMatch(s);
178  return new UninterpretedSort(this, s);
179  }
180 
185  {
186  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
187 
188  return MkUninterpretedSort(MkSymbol(str));
189  }
190 
195  {
196  Contract.Ensures(Contract.Result<IntSort>() != null);
197 
198  return new IntSort(this);
199  }
200 
205  {
206  Contract.Ensures(Contract.Result<RealSort>() != null);
207  return new RealSort(this);
208  }
209 
213  public BitVecSort MkBitVecSort(uint size)
214  {
215  Contract.Ensures(Contract.Result<BitVecSort>() != null);
216 
217  return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
218  }
219 
223  public ArraySort MkArraySort(Sort domain, Sort range)
224  {
225  Contract.Requires(domain != null);
226  Contract.Requires(range != null);
227  Contract.Ensures(Contract.Result<ArraySort>() != null);
228 
229  CheckContextMatch(domain);
230  CheckContextMatch(range);
231  return new ArraySort(this, domain, range);
232  }
233 
237  public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
238  {
239  Contract.Requires(name != null);
240  Contract.Requires(fieldNames != null);
241  Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
242  Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
243  Contract.Ensures(Contract.Result<TupleSort>() != null);
244 
245  CheckContextMatch(name);
246  CheckContextMatch(fieldNames);
247  CheckContextMatch(fieldSorts);
248  return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
249  }
250 
254  public EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
255  {
256  Contract.Requires(name != null);
257  Contract.Requires(enumNames != null);
258  Contract.Requires(Contract.ForAll(enumNames, f => f != null));
259 
260  Contract.Ensures(Contract.Result<EnumSort>() != null);
261 
262  CheckContextMatch(name);
263  CheckContextMatch(enumNames);
264  return new EnumSort(this, name, enumNames);
265  }
266 
270  public EnumSort MkEnumSort(string name, params string[] enumNames)
271  {
272  Contract.Requires(enumNames != null);
273  Contract.Ensures(Contract.Result<EnumSort>() != null);
274 
275  return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
276  }
277 
281  public ListSort MkListSort(Symbol name, Sort elemSort)
282  {
283  Contract.Requires(name != null);
284  Contract.Requires(elemSort != null);
285  Contract.Ensures(Contract.Result<ListSort>() != null);
286 
287  CheckContextMatch(name);
288  CheckContextMatch(elemSort);
289  return new ListSort(this, name, elemSort);
290  }
291 
295  public ListSort MkListSort(string name, Sort elemSort)
296  {
297  Contract.Requires(elemSort != null);
298  Contract.Ensures(Contract.Result<ListSort>() != null);
299 
300  CheckContextMatch(elemSort);
301  return new ListSort(this, MkSymbol(name), elemSort);
302  }
303 
310  public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
311  {
312  Contract.Requires(name != null);
313  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
314 
315  CheckContextMatch(name);
316  return new FiniteDomainSort(this, name, size);
317  }
318 
327  public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
328  {
329  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
330 
331  return new FiniteDomainSort(this, MkSymbol(name), size);
332  }
333 
334 
335  #region Datatypes
336  public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
347  {
348  Contract.Requires(name != null);
349  Contract.Requires(recognizer != null);
350  Contract.Ensures(Contract.Result<Constructor>() != null);
351 
352  return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
353  }
354 
364  public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
365  {
366  Contract.Ensures(Contract.Result<Constructor>() != null);
367 
368  return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
369  }
370 
374  public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
375  {
376  Contract.Requires(name != null);
377  Contract.Requires(constructors != null);
378  Contract.Requires(Contract.ForAll(constructors, c => c != null));
379 
380  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
381 
382  CheckContextMatch(name);
383  CheckContextMatch(constructors);
384  return new DatatypeSort(this, name, constructors);
385  }
386 
390  public DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
391  {
392  Contract.Requires(constructors != null);
393  Contract.Requires(Contract.ForAll(constructors, c => c != null));
394  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
395 
396  CheckContextMatch(constructors);
397  return new DatatypeSort(this, MkSymbol(name), constructors);
398  }
399 
406  {
407  Contract.Requires(names != null);
408  Contract.Requires(c != null);
409  Contract.Requires(names.Length == c.Length);
410  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
411  Contract.Requires(Contract.ForAll(names, name => name != null));
412  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
413 
414  CheckContextMatch(names);
415  uint n = (uint)names.Length;
416  ConstructorList[] cla = new ConstructorList[n];
417  IntPtr[] n_constr = new IntPtr[n];
418  for (uint i = 0; i < n; i++)
419  {
420  Constructor[] constructor = c[i];
421  Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
422  CheckContextMatch(constructor);
423  cla[i] = new ConstructorList(this, constructor);
424  n_constr[i] = cla[i].NativeObject;
425  }
426  IntPtr[] n_res = new IntPtr[n];
427  Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
428  DatatypeSort[] res = new DatatypeSort[n];
429  for (uint i = 0; i < n; i++)
430  res[i] = new DatatypeSort(this, n_res[i]);
431  return res;
432  }
433 
440  public DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
441  {
442  Contract.Requires(names != null);
443  Contract.Requires(c != null);
444  Contract.Requires(names.Length == c.Length);
445  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
446  Contract.Requires(Contract.ForAll(names, name => name != null));
447  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
448 
449  return MkDatatypeSorts(MkSymbols(names), c);
450  }
451 
452  #endregion
453  #endregion
454 
455  #region Function Declarations
456  public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
460  {
461  Contract.Requires(name != null);
462  Contract.Requires(range != null);
463  Contract.Requires(Contract.ForAll(domain, d => d != null));
464  Contract.Ensures(Contract.Result<FuncDecl>() != null);
465 
466  CheckContextMatch(name);
467  CheckContextMatch(domain);
468  CheckContextMatch(range);
469  return new FuncDecl(this, name, domain, range);
470  }
471 
475  public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
476  {
477  Contract.Requires(name != null);
478  Contract.Requires(domain != null);
479  Contract.Requires(range != null);
480  Contract.Ensures(Contract.Result<FuncDecl>() != null);
481 
482  CheckContextMatch(name);
483  CheckContextMatch(domain);
484  CheckContextMatch(range);
485  Sort[] q = new Sort[] { domain };
486  return new FuncDecl(this, name, q, range);
487  }
488 
492  public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
493  {
494  Contract.Requires(range != null);
495  Contract.Requires(Contract.ForAll(domain, d => d != null));
496  Contract.Ensures(Contract.Result<FuncDecl>() != null);
497 
498  CheckContextMatch(domain);
499  CheckContextMatch(range);
500  return new FuncDecl(this, MkSymbol(name), domain, range);
501  }
502 
506  public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
507  {
508  Contract.Requires(range != null);
509  Contract.Requires(domain != null);
510  Contract.Ensures(Contract.Result<FuncDecl>() != null);
511 
512  CheckContextMatch(domain);
513  CheckContextMatch(range);
514  Sort[] q = new Sort[] { domain };
515  return new FuncDecl(this, MkSymbol(name), q, range);
516  }
517 
523  public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
524  {
525  Contract.Requires(range != null);
526  Contract.Requires(Contract.ForAll(domain, d => d != null));
527  Contract.Ensures(Contract.Result<FuncDecl>() != null);
528 
529  CheckContextMatch(domain);
530  CheckContextMatch(range);
531  return new FuncDecl(this, prefix, domain, range);
532  }
533 
537  public FuncDecl MkConstDecl(Symbol name, Sort range)
538  {
539  Contract.Requires(name != null);
540  Contract.Requires(range != null);
541  Contract.Ensures(Contract.Result<FuncDecl>() != null);
542 
543  CheckContextMatch(name);
544  CheckContextMatch(range);
545  return new FuncDecl(this, name, null, range);
546  }
547 
551  public FuncDecl MkConstDecl(string name, Sort range)
552  {
553  Contract.Requires(range != null);
554  Contract.Ensures(Contract.Result<FuncDecl>() != null);
555 
556  CheckContextMatch(range);
557  return new FuncDecl(this, MkSymbol(name), null, range);
558  }
559 
565  public FuncDecl MkFreshConstDecl(string prefix, Sort range)
566  {
567  Contract.Requires(range != null);
568  Contract.Ensures(Contract.Result<FuncDecl>() != null);
569 
570  CheckContextMatch(range);
571  return new FuncDecl(this, prefix, null, range);
572  }
573  #endregion
574 
575  #region Bound Variables
576  public Expr MkBound(uint index, Sort ty)
582  {
583  Contract.Requires(ty != null);
584  Contract.Ensures(Contract.Result<Expr>() != null);
585 
586  return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
587  }
588  #endregion
589 
590  #region Quantifier Patterns
591  public Pattern MkPattern(params Expr[] terms)
595  {
596  Contract.Requires(terms != null);
597  if (terms.Length == 0)
598  throw new Z3Exception("Cannot create a pattern from zero terms");
599 
600  Contract.Ensures(Contract.Result<Pattern>() != null);
601 
602  Contract.EndContractBlock();
603 
604  IntPtr[] termsNative = AST.ArrayToNative(terms);
605  return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
606  }
607  #endregion
608 
609  #region Constants
610  public Expr MkConst(Symbol name, Sort range)
614  {
615  Contract.Requires(name != null);
616  Contract.Requires(range != null);
617  Contract.Ensures(Contract.Result<Expr>() != null);
618 
619  CheckContextMatch(name);
620  CheckContextMatch(range);
621 
622  return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
623  }
624 
628  public Expr MkConst(string name, Sort range)
629  {
630  Contract.Requires(range != null);
631  Contract.Ensures(Contract.Result<Expr>() != null);
632 
633  return MkConst(MkSymbol(name), range);
634  }
635 
640  public Expr MkFreshConst(string prefix, Sort range)
641  {
642  Contract.Requires(range != null);
643  Contract.Ensures(Contract.Result<Expr>() != null);
644 
645  CheckContextMatch(range);
646  return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
647  }
648 
654  {
655  Contract.Requires(f != null);
656  Contract.Ensures(Contract.Result<Expr>() != null);
657 
658  return MkApp(f);
659  }
660 
665  {
666  Contract.Requires(name != null);
667  Contract.Ensures(Contract.Result<BoolExpr>() != null);
668 
669  return (BoolExpr)MkConst(name, BoolSort);
670  }
671 
675  public BoolExpr MkBoolConst(string name)
676  {
677  Contract.Ensures(Contract.Result<BoolExpr>() != null);
678 
679  return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
680  }
681 
685  public IntExpr MkIntConst(Symbol name)
686  {
687  Contract.Requires(name != null);
688  Contract.Ensures(Contract.Result<IntExpr>() != null);
689 
690  return (IntExpr)MkConst(name, IntSort);
691  }
692 
696  public IntExpr MkIntConst(string name)
697  {
698  Contract.Requires(name != null);
699  Contract.Ensures(Contract.Result<IntExpr>() != null);
700 
701  return (IntExpr)MkConst(name, IntSort);
702  }
703 
708  {
709  Contract.Requires(name != null);
710  Contract.Ensures(Contract.Result<RealExpr>() != null);
711 
712  return (RealExpr)MkConst(name, RealSort);
713  }
714 
718  public RealExpr MkRealConst(string name)
719  {
720  Contract.Ensures(Contract.Result<RealExpr>() != null);
721 
722  return (RealExpr)MkConst(name, RealSort);
723  }
724 
728  public BitVecExpr MkBVConst(Symbol name, uint size)
729  {
730  Contract.Requires(name != null);
731  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
732 
733  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
734  }
735 
739  public BitVecExpr MkBVConst(string name, uint size)
740  {
741  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
742 
743  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
744  }
745  #endregion
746 
747  #region Terms
748  public Expr MkApp(FuncDecl f, params Expr[] args)
752  {
753  Contract.Requires(f != null);
754  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
755  Contract.Ensures(Contract.Result<Expr>() != null);
756 
757  CheckContextMatch(f);
758  CheckContextMatch(args);
759  return Expr.Create(this, f, args);
760  }
761 
762  #region Propositional
763  public BoolExpr MkTrue()
767  {
768  Contract.Ensures(Contract.Result<BoolExpr>() != null);
769 
770  return new BoolExpr(this, Native.Z3_mk_true(nCtx));
771  }
772 
776  public BoolExpr MkFalse()
777  {
778  Contract.Ensures(Contract.Result<BoolExpr>() != null);
779 
780  return new BoolExpr(this, Native.Z3_mk_false(nCtx));
781  }
782 
786  public BoolExpr MkBool(bool value)
787  {
788  Contract.Ensures(Contract.Result<BoolExpr>() != null);
789 
790  return value ? MkTrue() : MkFalse();
791  }
792 
796  public BoolExpr MkEq(Expr x, Expr y)
797  {
798  Contract.Requires(x != null);
799  Contract.Requires(y != null);
800  Contract.Ensures(Contract.Result<BoolExpr>() != null);
801 
802  CheckContextMatch(x);
803  CheckContextMatch(y);
804  return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
805  }
806 
810  public BoolExpr MkDistinct(params Expr[] args)
811  {
812  Contract.Requires(args != null);
813  Contract.Requires(Contract.ForAll(args, a => a != null));
814 
815  Contract.Ensures(Contract.Result<BoolExpr>() != null);
816 
817  CheckContextMatch(args);
818  return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
819  }
820 
825  {
826  Contract.Requires(a != null);
827  Contract.Ensures(Contract.Result<BoolExpr>() != null);
828 
829  CheckContextMatch(a);
830  return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
831  }
832 
839  public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
840  {
841  Contract.Requires(t1 != null);
842  Contract.Requires(t2 != null);
843  Contract.Requires(t3 != null);
844  Contract.Ensures(Contract.Result<Expr>() != null);
845 
846  CheckContextMatch(t1);
847  CheckContextMatch(t2);
848  CheckContextMatch(t3);
849  return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
850  }
851 
856  {
857  Contract.Requires(t1 != null);
858  Contract.Requires(t2 != null);
859  Contract.Ensures(Contract.Result<BoolExpr>() != null);
860 
861  CheckContextMatch(t1);
862  CheckContextMatch(t2);
863  return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
864  }
865 
870  {
871  Contract.Requires(t1 != null);
872  Contract.Requires(t2 != null);
873  Contract.Ensures(Contract.Result<BoolExpr>() != null);
874 
875  CheckContextMatch(t1);
876  CheckContextMatch(t2);
877  return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
878  }
879 
884  {
885  Contract.Requires(t1 != null);
886  Contract.Requires(t2 != null);
887  Contract.Ensures(Contract.Result<BoolExpr>() != null);
888 
889  CheckContextMatch(t1);
890  CheckContextMatch(t2);
891  return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
892  }
893 
897  public BoolExpr MkAnd(params BoolExpr[] t)
898  {
899  Contract.Requires(t != null);
900  Contract.Requires(Contract.ForAll(t, a => a != null));
901  Contract.Ensures(Contract.Result<BoolExpr>() != null);
902 
903  CheckContextMatch(t);
904  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
905  }
906 
910  public BoolExpr MkOr(params BoolExpr[] t)
911  {
912  Contract.Requires(t != null);
913  Contract.Requires(Contract.ForAll(t, a => a != null));
914  Contract.Ensures(Contract.Result<BoolExpr>() != null);
915 
916  CheckContextMatch(t);
917  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
918  }
919 
920 
921  #endregion
922 
923  #region Arithmetic
924  public ArithExpr MkAdd(params ArithExpr[] t)
928  {
929  Contract.Requires(t != null);
930  Contract.Requires(Contract.ForAll(t, a => a != null));
931  Contract.Ensures(Contract.Result<ArithExpr>() != null);
932 
933  CheckContextMatch(t);
934  return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
935  }
936 
940  public ArithExpr MkMul(params ArithExpr[] t)
941  {
942  Contract.Requires(t != null);
943  Contract.Requires(Contract.ForAll(t, a => a != null));
944  Contract.Ensures(Contract.Result<ArithExpr>() != null);
945 
946  CheckContextMatch(t);
947  return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
948  }
949 
953  public ArithExpr MkSub(params ArithExpr[] t)
954  {
955  Contract.Requires(t != null);
956  Contract.Requires(Contract.ForAll(t, a => a != null));
957  Contract.Ensures(Contract.Result<ArithExpr>() != null);
958 
959  CheckContextMatch(t);
960  return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
961  }
962 
967  {
968  Contract.Requires(t != null);
969  Contract.Ensures(Contract.Result<ArithExpr>() != null);
970 
971  CheckContextMatch(t);
972  return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
973  }
974 
979  {
980  Contract.Requires(t1 != null);
981  Contract.Requires(t2 != null);
982  Contract.Ensures(Contract.Result<ArithExpr>() != null);
983 
984  CheckContextMatch(t1);
985  CheckContextMatch(t2);
986  return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
987  }
988 
993  public IntExpr MkMod(IntExpr t1, IntExpr t2)
994  {
995  Contract.Requires(t1 != null);
996  Contract.Requires(t2 != null);
997  Contract.Ensures(Contract.Result<IntExpr>() != null);
998 
999  CheckContextMatch(t1);
1000  CheckContextMatch(t2);
1001  return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1002  }
1003 
1008  public IntExpr MkRem(IntExpr t1, IntExpr t2)
1009  {
1010  Contract.Requires(t1 != null);
1011  Contract.Requires(t2 != null);
1012  Contract.Ensures(Contract.Result<IntExpr>() != null);
1013 
1014  CheckContextMatch(t1);
1015  CheckContextMatch(t2);
1016  return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1017  }
1018 
1023  {
1024  Contract.Requires(t1 != null);
1025  Contract.Requires(t2 != null);
1026  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1027 
1028  CheckContextMatch(t1);
1029  CheckContextMatch(t2);
1030  return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1031  }
1032 
1037  {
1038  Contract.Requires(t1 != null);
1039  Contract.Requires(t2 != null);
1040  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1041 
1042  CheckContextMatch(t1);
1043  CheckContextMatch(t2);
1044  return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1045  }
1046 
1051  {
1052  Contract.Requires(t1 != null);
1053  Contract.Requires(t2 != null);
1054  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1055 
1056  CheckContextMatch(t1);
1057  CheckContextMatch(t2);
1058  return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1059  }
1060 
1065  {
1066  Contract.Requires(t1 != null);
1067  Contract.Requires(t2 != null);
1068  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1069 
1070  CheckContextMatch(t1);
1071  CheckContextMatch(t2);
1072  return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1073  }
1074 
1079  {
1080  Contract.Requires(t1 != null);
1081  Contract.Requires(t2 != null);
1082  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1083 
1084  CheckContextMatch(t1);
1085  CheckContextMatch(t2);
1086  return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1087  }
1088 
1100  {
1101  Contract.Requires(t != null);
1102  Contract.Ensures(Contract.Result<RealExpr>() != null);
1103 
1104  CheckContextMatch(t);
1105  return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1106  }
1107 
1116  {
1117  Contract.Requires(t != null);
1118  Contract.Ensures(Contract.Result<IntExpr>() != null);
1119 
1120  CheckContextMatch(t);
1121  return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1122  }
1123 
1128  {
1129  Contract.Requires(t != null);
1130  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1131 
1132  CheckContextMatch(t);
1133  return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1134  }
1135  #endregion
1136 
1137  #region Bit-vectors
1138  public BitVecExpr MkBVNot(BitVecExpr t)
1143  {
1144  Contract.Requires(t != null);
1145  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1146 
1147  CheckContextMatch(t);
1148  return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1149  }
1150 
1156  {
1157  Contract.Requires(t != null);
1158  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1159 
1160  CheckContextMatch(t);
1161  return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1162  }
1163 
1169  {
1170  Contract.Requires(t != null);
1171  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1172 
1173  CheckContextMatch(t);
1174  return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1175  }
1176 
1182  {
1183  Contract.Requires(t1 != null);
1184  Contract.Requires(t2 != null);
1185  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1186 
1187  CheckContextMatch(t1);
1188  CheckContextMatch(t2);
1189  return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1190  }
1191 
1197  {
1198  Contract.Requires(t1 != null);
1199  Contract.Requires(t2 != null);
1200  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1201 
1202  CheckContextMatch(t1);
1203  CheckContextMatch(t2);
1204  return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1205  }
1206 
1212  {
1213  Contract.Requires(t1 != null);
1214  Contract.Requires(t2 != null);
1215  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1216 
1217  CheckContextMatch(t1);
1218  CheckContextMatch(t2);
1219  return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1220  }
1221 
1227  {
1228  Contract.Requires(t1 != null);
1229  Contract.Requires(t2 != null);
1230  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1231 
1232  CheckContextMatch(t1);
1233  CheckContextMatch(t2);
1234  return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1235  }
1236 
1242  {
1243  Contract.Requires(t1 != null);
1244  Contract.Requires(t2 != null);
1245  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1246 
1247  CheckContextMatch(t1);
1248  CheckContextMatch(t2);
1249  return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1250  }
1251 
1257  {
1258  Contract.Requires(t1 != null);
1259  Contract.Requires(t2 != null);
1260  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1261 
1262  CheckContextMatch(t1);
1263  CheckContextMatch(t2);
1264  return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1265  }
1266 
1272  {
1273  Contract.Requires(t != null);
1274  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1275 
1276  CheckContextMatch(t);
1277  return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1278  }
1279 
1285  {
1286  Contract.Requires(t1 != null);
1287  Contract.Requires(t2 != null);
1288  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1289 
1290  CheckContextMatch(t1);
1291  CheckContextMatch(t2);
1292  return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1293  }
1294 
1300  {
1301  Contract.Requires(t1 != null);
1302  Contract.Requires(t2 != null);
1303  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1304 
1305  CheckContextMatch(t1);
1306  CheckContextMatch(t2);
1307  return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1308  }
1309 
1315  {
1316  Contract.Requires(t1 != null);
1317  Contract.Requires(t2 != null);
1318  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1319 
1320  CheckContextMatch(t1);
1321  CheckContextMatch(t2);
1322  return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1323  }
1324 
1335  {
1336  Contract.Requires(t1 != null);
1337  Contract.Requires(t2 != null);
1338  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1339 
1340  CheckContextMatch(t1);
1341  CheckContextMatch(t2);
1342  return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1343  }
1344 
1359  {
1360  Contract.Requires(t1 != null);
1361  Contract.Requires(t2 != null);
1362  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1363 
1364  CheckContextMatch(t1);
1365  CheckContextMatch(t2);
1366  return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1367  }
1368 
1378  {
1379  Contract.Requires(t1 != null);
1380  Contract.Requires(t2 != null);
1381  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1382 
1383  CheckContextMatch(t1);
1384  CheckContextMatch(t2);
1385  return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1386  }
1387 
1399  {
1400  Contract.Requires(t1 != null);
1401  Contract.Requires(t2 != null);
1402  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1403 
1404  CheckContextMatch(t1);
1405  CheckContextMatch(t2);
1406  return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1407  }
1408 
1417  {
1418  Contract.Requires(t1 != null);
1419  Contract.Requires(t2 != null);
1420  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1421 
1422  CheckContextMatch(t1);
1423  CheckContextMatch(t2);
1424  return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1425  }
1426 
1434  {
1435  Contract.Requires(t1 != null);
1436  Contract.Requires(t2 != null);
1437  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1438 
1439  CheckContextMatch(t1);
1440  CheckContextMatch(t2);
1441  return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1442  }
1443 
1451  {
1452  Contract.Requires(t1 != null);
1453  Contract.Requires(t2 != null);
1454  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1455 
1456  CheckContextMatch(t1);
1457  CheckContextMatch(t2);
1458  return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1459  }
1460 
1468  {
1469  Contract.Requires(t1 != null);
1470  Contract.Requires(t2 != null);
1471  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1472 
1473  CheckContextMatch(t1);
1474  CheckContextMatch(t2);
1475  return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1476  }
1477 
1485  {
1486  Contract.Requires(t1 != null);
1487  Contract.Requires(t2 != null);
1488  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1489 
1490  CheckContextMatch(t1);
1491  CheckContextMatch(t2);
1492  return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1493  }
1494 
1502  {
1503  Contract.Requires(t1 != null);
1504  Contract.Requires(t2 != null);
1505  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1506 
1507  CheckContextMatch(t1);
1508  CheckContextMatch(t2);
1509  return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1510  }
1511 
1519  {
1520  Contract.Requires(t1 != null);
1521  Contract.Requires(t2 != null);
1522  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1523 
1524  CheckContextMatch(t1);
1525  CheckContextMatch(t2);
1526  return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1527  }
1528 
1536  {
1537  Contract.Requires(t1 != null);
1538  Contract.Requires(t2 != null);
1539  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1540 
1541  CheckContextMatch(t1);
1542  CheckContextMatch(t2);
1543  return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1544  }
1545 
1553  {
1554  Contract.Requires(t1 != null);
1555  Contract.Requires(t2 != null);
1556  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1557 
1558  CheckContextMatch(t1);
1559  CheckContextMatch(t2);
1560  return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1561  }
1562 
1574  {
1575  Contract.Requires(t1 != null);
1576  Contract.Requires(t2 != null);
1577  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1578 
1579  CheckContextMatch(t1);
1580  CheckContextMatch(t2);
1581  return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1582  }
1583 
1593  public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
1594  {
1595  Contract.Requires(t != null);
1596  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1597 
1598  CheckContextMatch(t);
1599  return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1600  }
1601 
1610  public BitVecExpr MkSignExt(uint i, BitVecExpr t)
1611  {
1612  Contract.Requires(t != null);
1613  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1614 
1615  CheckContextMatch(t);
1616  return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1617  }
1618 
1628  public BitVecExpr MkZeroExt(uint i, BitVecExpr t)
1629  {
1630  Contract.Requires(t != null);
1631  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1632 
1633  CheckContextMatch(t);
1634  return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1635  }
1636 
1643  public BitVecExpr MkRepeat(uint i, BitVecExpr t)
1644  {
1645  Contract.Requires(t != null);
1646  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1647 
1648  CheckContextMatch(t);
1649  return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1650  }
1651 
1665  {
1666  Contract.Requires(t1 != null);
1667  Contract.Requires(t2 != null);
1668  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1669 
1670  CheckContextMatch(t1);
1671  CheckContextMatch(t2);
1672  return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1673  }
1674 
1688  {
1689  Contract.Requires(t1 != null);
1690  Contract.Requires(t2 != null);
1691  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1692 
1693  CheckContextMatch(t1);
1694  CheckContextMatch(t2);
1695  return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1696  }
1697 
1713  {
1714  Contract.Requires(t1 != null);
1715  Contract.Requires(t2 != null);
1716  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1717 
1718  CheckContextMatch(t1);
1719  CheckContextMatch(t2);
1720  return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1721  }
1722 
1731  {
1732  Contract.Requires(t != null);
1733  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1734 
1735  CheckContextMatch(t);
1736  return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1737  }
1738 
1747  {
1748  Contract.Requires(t != null);
1749  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1750 
1751  CheckContextMatch(t);
1752  return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1753  }
1754 
1763  {
1764  Contract.Requires(t1 != null);
1765  Contract.Requires(t2 != null);
1766  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1767 
1768  CheckContextMatch(t1);
1769  CheckContextMatch(t2);
1770  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1771  }
1772 
1781  {
1782  Contract.Requires(t1 != null);
1783  Contract.Requires(t2 != null);
1784  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1785 
1786  CheckContextMatch(t1);
1787  CheckContextMatch(t2);
1788  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1789  }
1790 
1801  public BitVecExpr MkInt2BV(uint n, IntExpr t)
1802  {
1803  Contract.Requires(t != null);
1804  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1805 
1806  CheckContextMatch(t);
1807  return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1808  }
1809 
1825  public IntExpr MkBV2Int(BitVecExpr t, bool signed)
1826  {
1827  Contract.Requires(t != null);
1828  Contract.Ensures(Contract.Result<IntExpr>() != null);
1829 
1830  CheckContextMatch(t);
1831  return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
1832  }
1833 
1840  public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1841  {
1842  Contract.Requires(t1 != null);
1843  Contract.Requires(t2 != null);
1844  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1845 
1846  CheckContextMatch(t1);
1847  CheckContextMatch(t2);
1848  return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1849  }
1850 
1858  {
1859  Contract.Requires(t1 != null);
1860  Contract.Requires(t2 != null);
1861  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1862 
1863  CheckContextMatch(t1);
1864  CheckContextMatch(t2);
1865  return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1866  }
1867 
1875  {
1876  Contract.Requires(t1 != null);
1877  Contract.Requires(t2 != null);
1878  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1879 
1880  CheckContextMatch(t1);
1881  CheckContextMatch(t2);
1882  return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1883  }
1884 
1891  public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1892  {
1893  Contract.Requires(t1 != null);
1894  Contract.Requires(t2 != null);
1895  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1896 
1897  CheckContextMatch(t1);
1898  CheckContextMatch(t2);
1899  return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1900  }
1901 
1909  {
1910  Contract.Requires(t1 != null);
1911  Contract.Requires(t2 != null);
1912  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1913 
1914  CheckContextMatch(t1);
1915  CheckContextMatch(t2);
1916  return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1917  }
1918 
1926  {
1927  Contract.Requires(t != null);
1928  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1929 
1930  CheckContextMatch(t);
1931  return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
1932  }
1933 
1940  public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1941  {
1942  Contract.Requires(t1 != null);
1943  Contract.Requires(t2 != null);
1944  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1945 
1946  CheckContextMatch(t1);
1947  CheckContextMatch(t2);
1948  return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1949  }
1950 
1958  {
1959  Contract.Requires(t1 != null);
1960  Contract.Requires(t2 != null);
1961  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1962 
1963  CheckContextMatch(t1);
1964  CheckContextMatch(t2);
1965  return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1966  }
1967  #endregion
1968 
1969  #region Arrays
1970  public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
1974  {
1975  Contract.Requires(name != null);
1976  Contract.Requires(domain != null);
1977  Contract.Requires(range != null);
1978  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
1979 
1980  return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
1981  }
1982 
1986  public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
1987  {
1988  Contract.Requires(domain != null);
1989  Contract.Requires(range != null);
1990  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
1991 
1992  return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
1993  }
1994 
2009  {
2010  Contract.Requires(a != null);
2011  Contract.Requires(i != null);
2012  Contract.Ensures(Contract.Result<Expr>() != null);
2013 
2014  CheckContextMatch(a);
2015  CheckContextMatch(i);
2016  return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2017  }
2018 
2037  {
2038  Contract.Requires(a != null);
2039  Contract.Requires(i != null);
2040  Contract.Requires(v != null);
2041  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2042 
2043  CheckContextMatch(a);
2044  CheckContextMatch(i);
2045  CheckContextMatch(v);
2046  return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2047  }
2048 
2058  public ArrayExpr MkConstArray(Sort domain, Expr v)
2059  {
2060  Contract.Requires(domain != null);
2061  Contract.Requires(v != null);
2062  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2063 
2064  CheckContextMatch(domain);
2065  CheckContextMatch(v);
2066  return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2067  }
2068 
2080  public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
2081  {
2082  Contract.Requires(f != null);
2083  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2084  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2085 
2086  CheckContextMatch(f);
2087  CheckContextMatch(args);
2088  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2089  }
2090 
2099  {
2100  Contract.Requires(array != null);
2101  Contract.Ensures(Contract.Result<Expr>() != null);
2102 
2103  CheckContextMatch(array);
2104  return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2105  }
2106  #endregion
2107 
2108  #region Sets
2109  public SetSort MkSetSort(Sort ty)
2113  {
2114  Contract.Requires(ty != null);
2115  Contract.Ensures(Contract.Result<SetSort>() != null);
2116 
2117  CheckContextMatch(ty);
2118  return new SetSort(this, ty);
2119  }
2120 
2124  public Expr MkEmptySet(Sort domain)
2125  {
2126  Contract.Requires(domain != null);
2127  Contract.Ensures(Contract.Result<Expr>() != null);
2128 
2129  CheckContextMatch(domain);
2130  return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2131  }
2132 
2136  public Expr MkFullSet(Sort domain)
2137  {
2138  Contract.Requires(domain != null);
2139  Contract.Ensures(Contract.Result<Expr>() != null);
2140 
2141  CheckContextMatch(domain);
2142  return Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2143  }
2144 
2148  public Expr MkSetAdd(Expr set, Expr element)
2149  {
2150  Contract.Requires(set != null);
2151  Contract.Requires(element != null);
2152  Contract.Ensures(Contract.Result<Expr>() != null);
2153 
2154  CheckContextMatch(set);
2155  CheckContextMatch(element);
2156  return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2157  }
2158 
2159 
2163  public Expr MkSetDel(Expr set, Expr element)
2164  {
2165  Contract.Requires(set != null);
2166  Contract.Requires(element != null);
2167  Contract.Ensures(Contract.Result<Expr>() != null);
2168 
2169  CheckContextMatch(set);
2170  CheckContextMatch(element);
2171  return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2172  }
2173 
2177  public Expr MkSetUnion(params Expr[] args)
2178  {
2179  Contract.Requires(args != null);
2180  Contract.Requires(Contract.ForAll(args, a => a != null));
2181 
2182  CheckContextMatch(args);
2183  return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2184  }
2185 
2189  public Expr MkSetIntersection(params Expr[] args)
2190  {
2191  Contract.Requires(args != null);
2192  Contract.Requires(Contract.ForAll(args, a => a != null));
2193  Contract.Ensures(Contract.Result<Expr>() != null);
2194 
2195  CheckContextMatch(args);
2196  return Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2197  }
2198 
2202  public Expr MkSetDifference(Expr arg1, Expr arg2)
2203  {
2204  Contract.Requires(arg1 != null);
2205  Contract.Requires(arg2 != null);
2206  Contract.Ensures(Contract.Result<Expr>() != null);
2207 
2208  CheckContextMatch(arg1);
2209  CheckContextMatch(arg2);
2210  return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2211  }
2212 
2217  {
2218  Contract.Requires(arg != null);
2219  Contract.Ensures(Contract.Result<Expr>() != null);
2220 
2221  CheckContextMatch(arg);
2222  return Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2223  }
2224 
2228  public Expr MkSetMembership(Expr elem, Expr set)
2229  {
2230  Contract.Requires(elem != null);
2231  Contract.Requires(set != null);
2232  Contract.Ensures(Contract.Result<Expr>() != null);
2233 
2234  CheckContextMatch(elem);
2235  CheckContextMatch(set);
2236  return Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2237  }
2238 
2242  public Expr MkSetSubset(Expr arg1, Expr arg2)
2243  {
2244  Contract.Requires(arg1 != null);
2245  Contract.Requires(arg2 != null);
2246  Contract.Ensures(Contract.Result<Expr>() != null);
2247 
2248  CheckContextMatch(arg1);
2249  CheckContextMatch(arg2);
2250  return Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2251  }
2252  #endregion
2253 
2254  #region Numerals
2255 
2256  #region General Numerals
2257  public Expr MkNumeral(string v, Sort ty)
2264  {
2265  Contract.Requires(ty != null);
2266  Contract.Ensures(Contract.Result<Expr>() != null);
2267 
2268  CheckContextMatch(ty);
2269  return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2270  }
2271 
2279  public Expr MkNumeral(int v, Sort ty)
2280  {
2281  Contract.Requires(ty != null);
2282  Contract.Ensures(Contract.Result<Expr>() != null);
2283 
2284  CheckContextMatch(ty);
2285  return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2286  }
2287 
2295  public Expr MkNumeral(uint v, Sort ty)
2296  {
2297  Contract.Requires(ty != null);
2298  Contract.Ensures(Contract.Result<Expr>() != null);
2299 
2300  CheckContextMatch(ty);
2301  return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2302  }
2303 
2311  public Expr MkNumeral(long v, Sort ty)
2312  {
2313  Contract.Requires(ty != null);
2314  Contract.Ensures(Contract.Result<Expr>() != null);
2315 
2316  CheckContextMatch(ty);
2317  return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2318  }
2319 
2327  public Expr MkNumeral(ulong v, Sort ty)
2328  {
2329  Contract.Requires(ty != null);
2330  Contract.Ensures(Contract.Result<Expr>() != null);
2331 
2332  CheckContextMatch(ty);
2333  return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2334  }
2335  #endregion
2336 
2337  #region Reals
2338  public RatNum MkReal(int num, int den)
2346  {
2347  if (den == 0)
2348  throw new Z3Exception("Denominator is zero");
2349 
2350  Contract.Ensures(Contract.Result<RatNum>() != null);
2351  Contract.EndContractBlock();
2352 
2353  return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
2354  }
2355 
2361  public RatNum MkReal(string v)
2362  {
2363  Contract.Ensures(Contract.Result<RatNum>() != null);
2364 
2365  return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
2366  }
2367 
2373  public RatNum MkReal(int v)
2374  {
2375  Contract.Ensures(Contract.Result<RatNum>() != null);
2376 
2377  return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
2378  }
2379 
2385  public RatNum MkReal(uint v)
2386  {
2387  Contract.Ensures(Contract.Result<RatNum>() != null);
2388 
2389  return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
2390  }
2391 
2397  public RatNum MkReal(long v)
2398  {
2399  Contract.Ensures(Contract.Result<RatNum>() != null);
2400 
2401  return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
2402  }
2403 
2409  public RatNum MkReal(ulong v)
2410  {
2411  Contract.Ensures(Contract.Result<RatNum>() != null);
2412 
2413  return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
2414  }
2415  #endregion
2416 
2417  #region Integers
2418  public IntNum MkInt(string v)
2423  {
2424  Contract.Ensures(Contract.Result<IntNum>() != null);
2425 
2426  return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
2427  }
2428 
2434  public IntNum MkInt(int v)
2435  {
2436  Contract.Ensures(Contract.Result<IntNum>() != null);
2437 
2438  return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
2439  }
2440 
2446  public IntNum MkInt(uint v)
2447  {
2448  Contract.Ensures(Contract.Result<IntNum>() != null);
2449 
2450  return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
2451  }
2452 
2458  public IntNum MkInt(long v)
2459  {
2460  Contract.Ensures(Contract.Result<IntNum>() != null);
2461 
2462  return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
2463  }
2464 
2470  public IntNum MkInt(ulong v)
2471  {
2472  Contract.Ensures(Contract.Result<IntNum>() != null);
2473 
2474  return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
2475  }
2476  #endregion
2477 
2478  #region Bit-vectors
2479  public BitVecNum MkBV(string v, uint size)
2485  {
2486  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2487 
2488  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2489  }
2490 
2496  public BitVecNum MkBV(int v, uint size)
2497  {
2498  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2499 
2500  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2501  }
2502 
2508  public BitVecNum MkBV(uint v, uint size)
2509  {
2510  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2511 
2512  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2513  }
2514 
2520  public BitVecNum MkBV(long v, uint size)
2521  {
2522  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2523 
2524  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2525  }
2526 
2532  public BitVecNum MkBV(ulong v, uint size)
2533  {
2534  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2535 
2536  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2537  }
2538  #endregion
2539 
2540  #endregion // Numerals
2541 
2542  #region Quantifiers
2543  public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2563  {
2564  Contract.Requires(sorts != null);
2565  Contract.Requires(names != null);
2566  Contract.Requires(body != null);
2567  Contract.Requires(sorts.Length == names.Length);
2568  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2569  Contract.Requires(Contract.ForAll(names, n => n != null));
2570  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2571  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2572 
2573  Contract.Ensures(Contract.Result<Quantifier>() != null);
2574 
2575  return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2576  }
2577 
2578 
2582  public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2583  {
2584  Contract.Requires(body != null);
2585  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
2586  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2587  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2588 
2589  Contract.Ensures(Contract.Result<Quantifier>() != null);
2590 
2591  return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2592  }
2593 
2598  public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2599  {
2600  Contract.Requires(sorts != null);
2601  Contract.Requires(names != null);
2602  Contract.Requires(body != null);
2603  Contract.Requires(sorts.Length == names.Length);
2604  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2605  Contract.Requires(Contract.ForAll(names, n => n != null));
2606  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2607  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2608  Contract.Ensures(Contract.Result<Quantifier>() != null);
2609 
2610  return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2611  }
2612 
2616  public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2617  {
2618  Contract.Requires(body != null);
2619  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2620  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2621  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2622  Contract.Ensures(Contract.Result<Quantifier>() != null);
2623 
2624  return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2625  }
2626 
2627 
2631  public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2632  {
2633  Contract.Requires(body != null);
2634  Contract.Requires(names != null);
2635  Contract.Requires(sorts != null);
2636  Contract.Requires(sorts.Length == names.Length);
2637  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2638  Contract.Requires(Contract.ForAll(names, n => n != null));
2639  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2640  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2641 
2642  Contract.Ensures(Contract.Result<Quantifier>() != null);
2643 
2644  if (universal)
2645  return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2646  else
2647  return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2648  }
2649 
2650 
2654  public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2655  {
2656  Contract.Requires(body != null);
2657  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2658  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2659  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2660 
2661  Contract.Ensures(Contract.Result<Quantifier>() != null);
2662 
2663  if (universal)
2664  return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2665  else
2666  return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2667  }
2668 
2669  #endregion
2670 
2671  #endregion // Expr
2672 
2673  #region Options
2674  public Z3_ast_print_mode PrintMode
2691  {
2692  set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
2693  }
2694  #endregion
2695 
2696  #region SMT Files & Strings
2697  public string BenchmarkToSMTString(string name, string logic, string status, string attributes,
2708  BoolExpr[] assumptions, BoolExpr formula)
2709  {
2710  Contract.Requires(assumptions != null);
2711  Contract.Requires(formula != null);
2712  Contract.Ensures(Contract.Result<string>() != null);
2713 
2714  return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
2715  (uint)assumptions.Length, AST.ArrayToNative(assumptions),
2716  formula.NativeObject);
2717  }
2718 
2729  public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2730  {
2731  uint csn = Symbol.ArrayLength(sortNames);
2732  uint cs = Sort.ArrayLength(sorts);
2733  uint cdn = Symbol.ArrayLength(declNames);
2734  uint cd = AST.ArrayLength(decls);
2735  if (csn != cs || cdn != cd)
2736  throw new Z3Exception("Argument size mismatch");
2737  Native.Z3_parse_smtlib_string(nCtx, str,
2738  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2739  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2740  }
2741 
2746  public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2747  {
2748  uint csn = Symbol.ArrayLength(sortNames);
2749  uint cs = Sort.ArrayLength(sorts);
2750  uint cdn = Symbol.ArrayLength(declNames);
2751  uint cd = AST.ArrayLength(decls);
2752  if (csn != cs || cdn != cd)
2753  throw new Z3Exception("Argument size mismatch");
2754  Native.Z3_parse_smtlib_file(nCtx, fileName,
2755  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2756  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2757  }
2758 
2762  public uint NumSMTLIBFormulas { get { return Native.Z3_get_smtlib_num_formulas(nCtx); } }
2763 
2767  public BoolExpr[] SMTLIBFormulas
2768  {
2769  get
2770  {
2771  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
2772 
2773  uint n = NumSMTLIBFormulas;
2774  BoolExpr[] res = new BoolExpr[n];
2775  for (uint i = 0; i < n; i++)
2776  res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_formula(nCtx, i));
2777  return res;
2778  }
2779  }
2780 
2784  public uint NumSMTLIBAssumptions { get { return Native.Z3_get_smtlib_num_assumptions(nCtx); } }
2785 
2789  public BoolExpr[] SMTLIBAssumptions
2790  {
2791  get
2792  {
2793  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
2794 
2795  uint n = NumSMTLIBAssumptions;
2796  BoolExpr[] res = new BoolExpr[n];
2797  for (uint i = 0; i < n; i++)
2798  res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_assumption(nCtx, i));
2799  return res;
2800  }
2801  }
2802 
2806  public uint NumSMTLIBDecls { get { return Native.Z3_get_smtlib_num_decls(nCtx); } }
2807 
2811  public FuncDecl[] SMTLIBDecls
2812  {
2813  get
2814  {
2815  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
2816 
2817  uint n = NumSMTLIBDecls;
2818  FuncDecl[] res = new FuncDecl[n];
2819  for (uint i = 0; i < n; i++)
2820  res[i] = new FuncDecl(this, Native.Z3_get_smtlib_decl(nCtx, i));
2821  return res;
2822  }
2823  }
2824 
2828  public uint NumSMTLIBSorts { get { return Native.Z3_get_smtlib_num_sorts(nCtx); } }
2829 
2833  public Sort[] SMTLIBSorts
2834  {
2835  get
2836  {
2837  Contract.Ensures(Contract.Result<Sort[]>() != null);
2838 
2839  uint n = NumSMTLIBSorts;
2840  Sort[] res = new Sort[n];
2841  for (uint i = 0; i < n; i++)
2842  res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i));
2843  return res;
2844  }
2845  }
2846 
2852  public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2853  {
2854  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2855 
2856  uint csn = Symbol.ArrayLength(sortNames);
2857  uint cs = Sort.ArrayLength(sorts);
2858  uint cdn = Symbol.ArrayLength(declNames);
2859  uint cd = AST.ArrayLength(decls);
2860  if (csn != cs || cdn != cd)
2861  throw new Z3Exception("Argument size mismatch");
2862  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
2863  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2864  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2865  }
2866 
2871  public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2872  {
2873  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2874 
2875  uint csn = Symbol.ArrayLength(sortNames);
2876  uint cs = Sort.ArrayLength(sorts);
2877  uint cdn = Symbol.ArrayLength(declNames);
2878  uint cd = AST.ArrayLength(decls);
2879  if (csn != cs || cdn != cd)
2880  throw new Z3Exception("Argument size mismatch");
2881  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
2882  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2883  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2884  }
2885  #endregion
2886 
2887  #region Goals
2888  public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
2899  {
2900  Contract.Ensures(Contract.Result<Goal>() != null);
2901 
2902  return new Goal(this, models, unsatCores, proofs);
2903  }
2904  #endregion
2905 
2906  #region ParameterSets
2907  public Params MkParams()
2911  {
2912  Contract.Ensures(Contract.Result<Params>() != null);
2913 
2914  return new Params(this);
2915  }
2916  #endregion
2917 
2918  #region Tactics
2919  public uint NumTactics
2923  {
2924  get { return Native.Z3_get_num_tactics(nCtx); }
2925  }
2926 
2930  public string[] TacticNames
2931  {
2932  get
2933  {
2934  Contract.Ensures(Contract.Result<string[]>() != null);
2935 
2936  uint n = NumTactics;
2937  string[] res = new string[n];
2938  for (uint i = 0; i < n; i++)
2939  res[i] = Native.Z3_get_tactic_name(nCtx, i);
2940  return res;
2941  }
2942  }
2943 
2947  public string TacticDescription(string name)
2948  {
2949  Contract.Ensures(Contract.Result<string>() != null);
2950 
2951  return Native.Z3_tactic_get_descr(nCtx, name);
2952  }
2953 
2957  public Tactic MkTactic(string name)
2958  {
2959  Contract.Ensures(Contract.Result<Tactic>() != null);
2960 
2961  return new Tactic(this, name);
2962  }
2963 
2968  public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
2969  {
2970  Contract.Requires(t1 != null);
2971  Contract.Requires(t2 != null);
2972  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
2973  Contract.Ensures(Contract.Result<Tactic>() != null);
2974 
2975 
2976  CheckContextMatch(t1);
2977  CheckContextMatch(t2);
2978  CheckContextMatch(ts);
2979 
2980  IntPtr last = IntPtr.Zero;
2981  if (ts != null && ts.Length > 0)
2982  {
2983  last = ts[ts.Length - 1].NativeObject;
2984  for (int i = ts.Length - 2; i >= 0; i--)
2985  last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
2986  }
2987  if (last != IntPtr.Zero)
2988  {
2989  last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
2990  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
2991  }
2992  else
2993  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
2994  }
2995 
3003  public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
3004  {
3005  Contract.Requires(t1 != null);
3006  Contract.Requires(t2 != null);
3007  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3008  Contract.Ensures(Contract.Result<Tactic>() != null);
3009 
3010  return AndThen(t1, t2, ts);
3011  }
3012 
3017  public Tactic OrElse(Tactic t1, Tactic t2)
3018  {
3019  Contract.Requires(t1 != null);
3020  Contract.Requires(t2 != null);
3021  Contract.Ensures(Contract.Result<Tactic>() != null);
3022 
3023  CheckContextMatch(t1);
3024  CheckContextMatch(t2);
3025  return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3026  }
3027 
3034  public Tactic TryFor(Tactic t, uint ms)
3035  {
3036  Contract.Requires(t != null);
3037  Contract.Ensures(Contract.Result<Tactic>() != null);
3038 
3039  CheckContextMatch(t);
3040  return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3041  }
3042 
3050  public Tactic When(Probe p, Tactic t)
3051  {
3052  Contract.Requires(p != null);
3053  Contract.Requires(t != null);
3054  Contract.Ensures(Contract.Result<Tactic>() != null);
3055 
3056  CheckContextMatch(t);
3057  CheckContextMatch(p);
3058  return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3059  }
3060 
3065  public Tactic Cond(Probe p, Tactic t1, Tactic t2)
3066  {
3067  Contract.Requires(p != null);
3068  Contract.Requires(t1 != null);
3069  Contract.Requires(t2 != null);
3070  Contract.Ensures(Contract.Result<Tactic>() != null);
3071 
3072  CheckContextMatch(p);
3073  CheckContextMatch(t1);
3074  CheckContextMatch(t2);
3075  return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3076  }
3077 
3082  public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
3083  {
3084  Contract.Requires(t != null);
3085  Contract.Ensures(Contract.Result<Tactic>() != null);
3086 
3087  CheckContextMatch(t);
3088  return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3089  }
3090 
3094  public Tactic Skip()
3095  {
3096  Contract.Ensures(Contract.Result<Tactic>() != null);
3097 
3098  return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3099  }
3100 
3104  public Tactic Fail()
3105  {
3106  Contract.Ensures(Contract.Result<Tactic>() != null);
3107 
3108  return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3109  }
3110 
3114  public Tactic FailIf(Probe p)
3115  {
3116  Contract.Requires(p != null);
3117  Contract.Ensures(Contract.Result<Tactic>() != null);
3118 
3119  CheckContextMatch(p);
3120  return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3121  }
3122 
3128  {
3129  Contract.Ensures(Contract.Result<Tactic>() != null);
3130 
3131  return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3132  }
3133 
3138  {
3139  Contract.Requires(t != null);
3140  Contract.Requires(p != null);
3141  Contract.Ensures(Contract.Result<Tactic>() != null);
3142 
3143  CheckContextMatch(t);
3144  CheckContextMatch(p);
3145  return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3146  }
3147 
3152  public Tactic With(Tactic t, Params p)
3153  {
3154  Contract.Requires(t != null);
3155  Contract.Requires(p != null);
3156  Contract.Ensures(Contract.Result<Tactic>() != null);
3157 
3158  return UsingParams(t, p);
3159  }
3160 
3164  public Tactic ParOr(params Tactic[] t)
3165  {
3166  Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3167  Contract.Ensures(Contract.Result<Tactic>() != null);
3168 
3169  CheckContextMatch(t);
3170  return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
3171  }
3172 
3178  {
3179  Contract.Requires(t1 != null);
3180  Contract.Requires(t2 != null);
3181  Contract.Ensures(Contract.Result<Tactic>() != null);
3182 
3183  CheckContextMatch(t1);
3184  CheckContextMatch(t2);
3185  return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3186  }
3187 
3192  public void Interrupt()
3193  {
3194  Native.Z3_interrupt(nCtx);
3195  }
3196  #endregion
3197 
3198  #region Probes
3199  public uint NumProbes
3203  {
3204  get { return Native.Z3_get_num_probes(nCtx); }
3205  }
3206 
3210  public string[] ProbeNames
3211  {
3212  get
3213  {
3214  Contract.Ensures(Contract.Result<string[]>() != null);
3215 
3216  uint n = NumProbes;
3217  string[] res = new string[n];
3218  for (uint i = 0; i < n; i++)
3219  res[i] = Native.Z3_get_probe_name(nCtx, i);
3220  return res;
3221  }
3222  }
3223 
3227  public string ProbeDescription(string name)
3228  {
3229  Contract.Ensures(Contract.Result<string>() != null);
3230 
3231  return Native.Z3_probe_get_descr(nCtx, name);
3232  }
3233 
3237  public Probe MkProbe(string name)
3238  {
3239  Contract.Ensures(Contract.Result<Probe>() != null);
3240 
3241  return new Probe(this, name);
3242  }
3243 
3247  public Probe ConstProbe(double val)
3248  {
3249  Contract.Ensures(Contract.Result<Probe>() != null);
3250 
3251  return new Probe(this, Native.Z3_probe_const(nCtx, val));
3252  }
3253 
3258  public Probe Lt(Probe p1, Probe p2)
3259  {
3260  Contract.Requires(p1 != null);
3261  Contract.Requires(p2 != null);
3262  Contract.Ensures(Contract.Result<Probe>() != null);
3263 
3264  CheckContextMatch(p1);
3265  CheckContextMatch(p2);
3266  return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3267  }
3268 
3273  public Probe Gt(Probe p1, Probe p2)
3274  {
3275  Contract.Requires(p1 != null);
3276  Contract.Requires(p2 != null);
3277  Contract.Ensures(Contract.Result<Probe>() != null);
3278 
3279  CheckContextMatch(p1);
3280  CheckContextMatch(p2);
3281  return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3282  }
3283 
3288  public Probe Le(Probe p1, Probe p2)
3289  {
3290  Contract.Requires(p1 != null);
3291  Contract.Requires(p2 != null);
3292  Contract.Ensures(Contract.Result<Probe>() != null);
3293 
3294  CheckContextMatch(p1);
3295  CheckContextMatch(p2);
3296  return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3297  }
3298 
3303  public Probe Ge(Probe p1, Probe p2)
3304  {
3305  Contract.Requires(p1 != null);
3306  Contract.Requires(p2 != null);
3307  Contract.Ensures(Contract.Result<Probe>() != null);
3308 
3309  CheckContextMatch(p1);
3310  CheckContextMatch(p2);
3311  return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3312  }
3313 
3318  public Probe Eq(Probe p1, Probe p2)
3319  {
3320  Contract.Requires(p1 != null);
3321  Contract.Requires(p2 != null);
3322  Contract.Ensures(Contract.Result<Probe>() != null);
3323 
3324  CheckContextMatch(p1);
3325  CheckContextMatch(p2);
3326  return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3327  }
3328 
3333  public Probe And(Probe p1, Probe p2)
3334  {
3335  Contract.Requires(p1 != null);
3336  Contract.Requires(p2 != null);
3337  Contract.Ensures(Contract.Result<Probe>() != null);
3338 
3339  CheckContextMatch(p1);
3340  CheckContextMatch(p2);
3341  return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3342  }
3343 
3348  public Probe Or(Probe p1, Probe p2)
3349  {
3350  Contract.Requires(p1 != null);
3351  Contract.Requires(p2 != null);
3352  Contract.Ensures(Contract.Result<Probe>() != null);
3353 
3354  CheckContextMatch(p1);
3355  CheckContextMatch(p2);
3356  return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3357  }
3358 
3363  public Probe Not(Probe p)
3364  {
3365  Contract.Requires(p != null);
3366  Contract.Ensures(Contract.Result<Probe>() != null);
3367 
3368  CheckContextMatch(p);
3369  return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3370  }
3371  #endregion
3372 
3373  #region Solvers
3374  public Solver MkSolver(Symbol logic = null)
3383  {
3384  Contract.Ensures(Contract.Result<Solver>() != null);
3385 
3386  if (logic == null)
3387  return new Solver(this, Native.Z3_mk_solver(nCtx));
3388  else
3389  return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3390  }
3391 
3396  public Solver MkSolver(string logic)
3397  {
3398  Contract.Ensures(Contract.Result<Solver>() != null);
3399 
3400  return MkSolver(MkSymbol(logic));
3401  }
3402 
3407  {
3408  Contract.Ensures(Contract.Result<Solver>() != null);
3409 
3410  return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3411  }
3412 
3421  {
3422  Contract.Requires(t != null);
3423  Contract.Ensures(Contract.Result<Solver>() != null);
3424 
3425  return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3426  }
3427  #endregion
3428 
3429  #region Fixedpoints
3430  public Fixedpoint MkFixedpoint()
3434  {
3435  Contract.Ensures(Contract.Result<Fixedpoint>() != null);
3436 
3437  return new Fixedpoint(this);
3438  }
3439  #endregion
3440 
3441  #region Floating-Point Arithmetic
3442 
3443  #region Rounding Modes
3444  #region RoundingMode Sort
3445  public FPRMSort MkFPRoundingModeSort()
3449  {
3450  Contract.Ensures(Contract.Result<FPRMSort>() != null);
3451  return new FPRMSort(this);
3452  }
3453  #endregion
3454 
3455  #region Numerals
3456  public FPRMExpr MkFPRoundNearestTiesToEven()
3460  {
3461  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3462  return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
3463  }
3464 
3468  public FPRMNum MkFPRNE()
3469  {
3470  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3471  return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
3472  }
3473 
3478  {
3479  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3480  return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
3481  }
3482 
3486  public FPRMNum MkFPRNA()
3487  {
3488  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3489  return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
3490  }
3491 
3496  {
3497  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3498  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
3499  }
3500 
3504  public FPRMNum MkFPRTP()
3505  {
3506  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3507  return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
3508  }
3509 
3514  {
3515  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3516  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
3517  }
3518 
3522  public FPRMNum MkFPRTN()
3523  {
3524  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3525  return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
3526  }
3527 
3532  {
3533  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3534  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
3535  }
3536 
3540  public FPRMNum MkFPRTZ()
3541  {
3542  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3543  return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
3544  }
3545  #endregion
3546  #endregion
3547 
3548  #region FloatingPoint Sorts
3549  public FPSort MkFPSort(uint ebits, uint sbits)
3555  {
3556  Contract.Ensures(Contract.Result<FPSort>() != null);
3557  return new FPSort(this, ebits, sbits);
3558  }
3559 
3564  {
3565  Contract.Ensures(Contract.Result<FPSort>() != null);
3566  return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
3567  }
3568 
3573  {
3574  Contract.Ensures(Contract.Result<FPSort>() != null);
3575  return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
3576  }
3577 
3582  {
3583  Contract.Ensures(Contract.Result<FPSort>() != null);
3584  return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
3585  }
3586 
3591  {
3592  Contract.Ensures(Contract.Result<FPSort>() != null);
3593  return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx));
3594  }
3595 
3600  {
3601  Contract.Ensures(Contract.Result<FPSort>() != null);
3602  return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
3603  }
3604 
3609  {
3610  Contract.Ensures(Contract.Result<FPSort>() != null);
3611  return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
3612  }
3613 
3618  {
3619  Contract.Ensures(Contract.Result<FPSort>() != null);
3620  return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
3621  }
3622 
3627  {
3628  Contract.Ensures(Contract.Result<FPSort>() != null);
3629  return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
3630  }
3631  #endregion
3632 
3633  #region Numerals
3634  public FPNum MkFPNaN(FPSort s)
3639  {
3640  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3641  return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
3642  }
3643 
3649  public FPNum MkFPInf(FPSort s, bool negative)
3650  {
3651  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3652  return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0));
3653  }
3654 
3660  public FPNum MkFPZero(FPSort s, bool negative)
3661  {
3662  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3663  return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
3664  }
3665 
3671  public FPNum MkFPNumeral(float v, FPSort s)
3672  {
3673  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3674  return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
3675  }
3676 
3682  public FPNum MkFPNumeral(double v, FPSort s)
3683  {
3684  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3685  return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
3686  }
3687 
3693  public FPNum MkFPNumeral(int v, FPSort s)
3694  {
3695  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3696  return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
3697  }
3698 
3706  public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
3707  {
3708  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3709  return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
3710  }
3711 
3719  public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
3720  {
3721  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3722  return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
3723  }
3724 
3730  public FPNum MkFP(float v, FPSort s)
3731  {
3732  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3733  return MkFPNumeral(v, s);
3734  }
3735 
3741  public FPNum MkFP(double v, FPSort s)
3742  {
3743  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3744  return MkFPNumeral(v, s);
3745  }
3746 
3752  public FPNum MkFP(int v, FPSort s)
3753  {
3754  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3755  return MkFPNumeral(v, s);
3756  }
3757 
3765  public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
3766  {
3767  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3768  return MkFPNumeral(sgn, exp, sig, s);
3769  }
3770 
3778  public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
3779  {
3780  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3781  return MkFPNumeral(sgn, exp, sig, s);
3782  }
3783 
3784  #endregion
3785 
3786  #region Operators
3787  public FPExpr MkFPAbs(FPExpr t)
3792  {
3793  Contract.Ensures(Contract.Result<FPNum>() != null);
3794  return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
3795  }
3796 
3801  public FPExpr MkFPNeg(FPExpr t)
3802  {
3803  Contract.Ensures(Contract.Result<FPNum>() != null);
3804  return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
3805  }
3806 
3813  public FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
3814  {
3815  Contract.Ensures(Contract.Result<FPNum>() != null);
3816  return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3817  }
3818 
3825  public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
3826  {
3827  Contract.Ensures(Contract.Result<FPNum>() != null);
3828  return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3829  }
3830 
3837  public FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
3838  {
3839  Contract.Ensures(Contract.Result<FPNum>() != null);
3840  return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3841  }
3842 
3849  public FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
3850  {
3851  Contract.Ensures(Contract.Result<FPNum>() != null);
3852  return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3853  }
3854 
3865  public FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
3866  {
3867  Contract.Ensures(Contract.Result<FPNum>() != null);
3868  return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
3869  }
3870 
3877  {
3878  Contract.Ensures(Contract.Result<FPNum>() != null);
3879  return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
3880  }
3881 
3887  public FPExpr MkFPRem(FPExpr t1, FPExpr t2)
3888  {
3889  Contract.Ensures(Contract.Result<FPNum>() != null);
3890  return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
3891  }
3892 
3900  {
3901  Contract.Ensures(Contract.Result<FPNum>() != null);
3902  return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
3903  }
3904 
3910  public FPExpr MkFPMin(FPExpr t1, FPExpr t2)
3911  {
3912  Contract.Ensures(Contract.Result<FPNum>() != null);
3913  return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
3914  }
3915 
3921  public FPExpr MkFPMax(FPExpr t1, FPExpr t2)
3922  {
3923  Contract.Ensures(Contract.Result<FPNum>() != null);
3924  return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
3925  }
3926 
3932  public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
3933  {
3934  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3935  return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
3936  }
3937 
3943  public BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
3944  {
3945  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3946  return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
3947  }
3948 
3954  public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
3955  {
3956  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3957  return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
3958  }
3959 
3965  public BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
3966  {
3967  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3968  return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
3969  }
3970 
3979  public BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
3980  {
3981  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3982  return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
3983  }
3984 
3990  {
3991  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3992  return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
3993  }
3994 
4000  {
4001  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4002  return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
4003  }
4004 
4010  {
4011  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4012  return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
4013  }
4014 
4020  {
4021  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4022  return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
4023  }
4024 
4030  {
4031  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4032  return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
4033  }
4034 
4040  {
4041  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4042  return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
4043  }
4044 
4050  {
4051  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4052  return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
4053  }
4054  #endregion
4055 
4056  #region Conversions to FloatingPoint terms
4057  public FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
4071  {
4072  Contract.Ensures(Contract.Result<FPExpr>() != null);
4073  return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
4074  }
4075 
4088  {
4089  Contract.Ensures(Contract.Result<FPExpr>() != null);
4090  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
4091  }
4092 
4105  {
4106  Contract.Ensures(Contract.Result<FPExpr>() != null);
4107  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4108  }
4109 
4122  {
4123  Contract.Ensures(Contract.Result<FPExpr>() != null);
4124  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4125  }
4126 
4140  public FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
4141  {
4142  Contract.Ensures(Contract.Result<FPExpr>() != null);
4143  if (signed)
4144  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4145  else
4146  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4147  }
4148 
4160  {
4161  Contract.Ensures(Contract.Result<FPExpr>() != null);
4162  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
4163  }
4164  #endregion
4165 
4166  #region Conversions from FloatingPoint terms
4167  public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed)
4180  {
4181  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4182  if (signed)
4183  return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4184  else
4185  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4186  }
4187 
4198  {
4199  Contract.Ensures(Contract.Result<RealExpr>() != null);
4200  return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
4201  }
4202  #endregion
4203 
4204  #region Z3-specific extensions
4205  public BitVecExpr MkFPToIEEEBV(FPExpr t)
4216  {
4217  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4218  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
4219  }
4220 
4234  {
4235  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4236  return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
4237  }
4238  #endregion
4239  #endregion // Floating-point Arithmetic
4240 
4241  #region Miscellaneous
4242  public AST WrapAST(IntPtr nativeObject)
4253  {
4254  Contract.Ensures(Contract.Result<AST>() != null);
4255  return AST.Create(this, nativeObject);
4256  }
4257 
4269  public IntPtr UnwrapAST(AST a)
4270  {
4271  return a.NativeObject;
4272  }
4273 
4277  public string SimplifyHelp()
4278  {
4279  Contract.Ensures(Contract.Result<string>() != null);
4280 
4281  return Native.Z3_simplify_get_help(nCtx);
4282  }
4283 
4287  public ParamDescrs SimplifyParameterDescriptions
4288  {
4289  get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
4290  }
4291  #endregion
4292 
4293  #region Error Handling
4294  //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
4302 
4306  //public event ErrorHandler OnError = null;
4307  #endregion
4308 
4309  #region Parameters
4310  public void UpdateParamValue(string id, string value)
4320  {
4321  Native.Z3_update_param_value(nCtx, id, value);
4322  }
4323 
4324  #endregion
4325 
4326  #region Internal
4327  internal IntPtr m_ctx = IntPtr.Zero;
4328  internal Native.Z3_error_handler m_n_err_handler = null;
4329  internal IntPtr nCtx { get { return m_ctx; } }
4330 
4331  internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
4332  {
4333  // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
4334  }
4335 
4336  internal void InitContext()
4337  {
4338  PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
4339  m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
4340  Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
4341  GC.SuppressFinalize(this);
4342  }
4343 
4344  [Pure]
4345  internal void CheckContextMatch(Z3Object other)
4346  {
4347  Contract.Requires(other != null);
4348 
4349  if (!ReferenceEquals(this, other.Context))
4350  throw new Z3Exception("Context mismatch");
4351  }
4352 
4353  [Pure]
4354  internal void CheckContextMatch(Z3Object[] arr)
4355  {
4356  Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
4357 
4358  if (arr != null)
4359  {
4360  foreach (Z3Object a in arr)
4361  {
4362  Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
4363  CheckContextMatch(a);
4364  }
4365  }
4366  }
4367 
4368  [ContractInvariantMethod]
4369  private void ObjectInvariant()
4370  {
4371  Contract.Invariant(m_AST_DRQ != null);
4372  Contract.Invariant(m_ASTMap_DRQ != null);
4373  Contract.Invariant(m_ASTVector_DRQ != null);
4374  Contract.Invariant(m_ApplyResult_DRQ != null);
4375  Contract.Invariant(m_FuncEntry_DRQ != null);
4376  Contract.Invariant(m_FuncInterp_DRQ != null);
4377  Contract.Invariant(m_Goal_DRQ != null);
4378  Contract.Invariant(m_Model_DRQ != null);
4379  Contract.Invariant(m_Params_DRQ != null);
4380  Contract.Invariant(m_ParamDescrs_DRQ != null);
4381  Contract.Invariant(m_Probe_DRQ != null);
4382  Contract.Invariant(m_Solver_DRQ != null);
4383  Contract.Invariant(m_Statistics_DRQ != null);
4384  Contract.Invariant(m_Tactic_DRQ != null);
4385  Contract.Invariant(m_Fixedpoint_DRQ != null);
4386  }
4387 
4388  readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
4389  readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue(10);
4390  readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue(10);
4391  readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue(10);
4392  readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue(10);
4393  readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue(10);
4394  readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue(10);
4395  readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue(10);
4396  readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue(10);
4397  readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue(10);
4398  readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue(10);
4399  readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue(10);
4400  readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10);
4401  readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
4402  readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
4403 
4407  public IDecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result<AST.DecRefQueue>() != null); return m_AST_DRQ; } }
4408 
4412  public IDecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null); return m_ASTMap_DRQ; } }
4413 
4417  public IDecRefQueue ASTVector_DRQ { get { Contract.Ensures(Contract.Result<ASTVector.DecRefQueue>() != null); return m_ASTVector_DRQ; } }
4418 
4422  public IDecRefQueue ApplyResult_DRQ { get { Contract.Ensures(Contract.Result<ApplyResult.DecRefQueue>() != null); return m_ApplyResult_DRQ; } }
4423 
4427  public IDecRefQueue FuncEntry_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.Entry.DecRefQueue>() != null); return m_FuncEntry_DRQ; } }
4428 
4432  public IDecRefQueue FuncInterp_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.DecRefQueue>() != null); return m_FuncInterp_DRQ; } }
4433 
4437  public IDecRefQueue Goal_DRQ { get { Contract.Ensures(Contract.Result<Goal.DecRefQueue>() != null); return m_Goal_DRQ; } }
4438 
4442  public IDecRefQueue Model_DRQ { get { Contract.Ensures(Contract.Result<Model.DecRefQueue>() != null); return m_Model_DRQ; } }
4443 
4447  public IDecRefQueue Params_DRQ { get { Contract.Ensures(Contract.Result<Params.DecRefQueue>() != null); return m_Params_DRQ; } }
4448 
4452  public IDecRefQueue ParamDescrs_DRQ { get { Contract.Ensures(Contract.Result<ParamDescrs.DecRefQueue>() != null); return m_ParamDescrs_DRQ; } }
4453 
4457  public IDecRefQueue Probe_DRQ { get { Contract.Ensures(Contract.Result<Probe.DecRefQueue>() != null); return m_Probe_DRQ; } }
4458 
4462  public IDecRefQueue Solver_DRQ { get { Contract.Ensures(Contract.Result<Solver.DecRefQueue>() != null); return m_Solver_DRQ; } }
4463 
4467  public IDecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result<Statistics.DecRefQueue>() != null); return m_Statistics_DRQ; } }
4468 
4472  public IDecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result<Tactic.DecRefQueue>() != null); return m_Tactic_DRQ; } }
4473 
4477  public IDecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
4478 
4479 
4480  internal long refCount = 0;
4481 
4485  ~Context()
4486  {
4487  // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4488  Dispose();
4489 
4490  if (refCount == 0)
4491  {
4492  m_n_err_handler = null;
4493  Native.Z3_del_context(m_ctx);
4494  m_ctx = IntPtr.Zero;
4495  }
4496  else
4497  GC.ReRegisterForFinalize(this);
4498  }
4499 
4503  public void Dispose()
4504  {
4505  // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4506  AST_DRQ.Clear(this);
4507  ASTMap_DRQ.Clear(this);
4508  ASTVector_DRQ.Clear(this);
4509  ApplyResult_DRQ.Clear(this);
4510  FuncEntry_DRQ.Clear(this);
4511  FuncInterp_DRQ.Clear(this);
4512  Goal_DRQ.Clear(this);
4513  Model_DRQ.Clear(this);
4514  Params_DRQ.Clear(this);
4515  ParamDescrs_DRQ.Clear(this);
4516  Probe_DRQ.Clear(this);
4517  Solver_DRQ.Clear(this);
4518  Statistics_DRQ.Clear(this);
4519  Tactic_DRQ.Clear(this);
4520  Fixedpoint_DRQ.Clear(this);
4521 
4522  m_boolSort = null;
4523  m_intSort = null;
4524  m_realSort = null;
4525  }
4526  #endregion
4527  }
4528 }
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:897
static Z3_ast Z3_mk_bvmul(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2557
static Z3_solver Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1)
Definition: Native.cs:5086
static Z3_sort Z3_mk_fpa_sort_64(Z3_context a0)
Definition: Native.cs:6171
BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
Two's complement signed remainder (sign follows divisor).
Definition: Context.cs:1416
string SimplifyHelp()
Return a string describing all available parameters to Expr.Simplify.
Definition: Context.cs:4277
static Z3_ast Z3_mk_bvadd_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Definition: Native.cs:2781
static string Z3_get_tactic_name(Z3_context a0, uint a1)
Definition: Native.cs:4936
static Z3_ast Z3_mk_fpa_abs(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6267
BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
Floating-point less than or equal.
Definition: Context.cs:3932
def RealSort
Definition: z3py.py:2641
static Z3_tactic Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Definition: Native.cs:4760
FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Definition: Context.cs:4104
FPExpr MkFPRem(FPExpr t1, FPExpr t2)
Floating-point remainder
Definition: Context.cs:3887
static Z3_ast Z3_mk_fpa_round_to_integral(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6339
static Z3_ast Z3_get_smtlib_formula(Z3_context a0, uint a1)
Definition: Native.cs:4125
static Z3_ast Z3_mk_bvneg_no_overflow(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2821
BoolExpr MkIsInteger(RealExpr t)
Creates an expression that checks whether a real number is an integer.
Definition: Context.cs:1127
static Z3_tactic Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Definition: Native.cs:4776
FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort...
Definition: Context.cs:4140
FPRMNum MkFPRNE()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode...
Definition: Context.cs:3468
Expr MkSetMembership(Expr elem, Expr set)
Check for set membership.
Definition: Context.cs:2228
FloatiungPoint Numerals
Definition: FPNum.cs:28
static Z3_ast Z3_mk_fpa_to_real(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6515
static Z3_ast Z3_mk_real2int(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2445
FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point division
Definition: Context.cs:3849
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
Bitwise conjunction.
Definition: Context.cs:1181
static Z3_ast Z3_mk_fpa_to_ubv(Z3_context a0, Z3_ast a1, Z3_ast a2, uint a3)
Definition: Native.cs:6499
static Z3_ast Z3_mk_set_intersect(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2933
static Z3_ast Z3_mk_bvuge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2637
Lists of constructors
DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
Create a new datatype sort.
Definition: Context.cs:374
Expr MkNumeral(uint v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
Definition: Context.cs:2295
static Z3_ast Z3_mk_mul(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2349
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:2957
static Z3_ast Z3_mk_mod(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2381
UninterpretedSort MkUninterpretedSort(string str)
Create a new uninterpreted sort.
Definition: Context.cs:184
RealExpr MkFPToReal(FPExpr t)
Conversion of a floating-point term into a real-numbered term.
Definition: Context.cs:4197
FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
Definition: Context.cs:4121
FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
Create a new finite domain sort.
Definition: Context.cs:310
def IntSort
Definition: z3py.py:2625
static Z3_ast Z3_mk_empty_set(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2893
static Z3_ast Z3_mk_fpa_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6395
def BoolSort
Definition: z3py.py:1336
FPRMNum MkFPRTN()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode...
Definition: Context.cs:3522
ArrayExpr MkConstArray(Sort domain, Expr v)
Create a constant array.
Definition: Context.cs:2058
string ProbeDescription(string name)
Returns a string containing a description of the probe with the given name.
Definition: Context.cs:3227
static Z3_ast Z3_mk_fpa_to_fp_float(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
Definition: Native.cs:6467
FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Floating-point fused multiply-add
Definition: Context.cs:3865
BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
Unsigned greater than or equal to.
Definition: Context.cs:1501
static Z3_ast Z3_mk_fpa_to_fp_signed(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
Definition: Native.cs:6483
Bit-vector sorts.
Definition: BitVecSort.cs:28
RatNum MkReal(string v)
Create a real numeral.
Definition: Context.cs:2361
Expr MkFreshConst(string prefix, Sort range)
Creates a fresh Constant of sort range and a name prefixed with prefix .
Definition: Context.cs:640
static Z3_tactic Z3_tactic_par_or(Z3_context a0, uint a1, [In] Z3_tactic[] a2)
Definition: Native.cs:4768
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:3765
static Z3_ast Z3_mk_bvashr(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2725
def AndThen(ts, ks)
Definition: z3py.py:6560
static void Z3_parse_smtlib_string(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
Definition: Native.cs:4103
def BitVecSort
Definition: z3py.py:3446
static Z3_ast Z3_mk_bv2int(Z3_context a0, Z3_ast a1, int a2)
Definition: Native.cs:2773
static string Z3_tactic_get_descr(Z3_context a0, string a1)
Definition: Native.cs:4976
BitVecNum MkBV(long v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2520
FPExpr MkFPMax(FPExpr t1, FPExpr t2)
Maximum of floating-point numbers.
Definition: Context.cs:3921
static Z3_ast Z3_mk_fpa_is_normal(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6403
Probe Not(Probe p)
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
Definition: Context.cs:3363
static Z3_ast Z3_mk_fpa_numeral_int_uint(Z3_context a0, int a1, int a2, uint a3, Z3_sort a4)
Definition: Native.cs:6251
Bit-vector numerals
Definition: BitVecNum.cs:32
Array sorts.
Definition: ArraySort.cs:29
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Unsigned division.
Definition: Context.cs:1334
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:3050
Tactic Repeat(Tactic t, uint max=uint.MaxValue)
Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number o...
Definition: Context.cs:3082
BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater than or equal to.
Definition: Context.cs:1518
static Z3_ast Z3_mk_fpa_max(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6355
static Z3_probe Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4912
BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
Bit-vector extraction.
Definition: Context.cs:1593
static Z3_ast Z3_mk_fresh_const(Z3_context a0, string a1, Z3_sort a2)
Definition: Native.cs:2245
Probe Ge(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value returned by p1 is greater than or equal the v...
Definition: Context.cs:3303
IntExpr MkIntConst(Symbol name)
Creates an integer constant.
Definition: Context.cs:685
static uint Z3_get_num_probes(Z3_context a0)
Definition: Native.cs:4944
BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
Parse the given string using the SMT-LIB2 parser.
Definition: Context.cs:2852
static Z3_ast Z3_mk_bvmul_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2837
static Z3_ast Z3_mk_fpa_geq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6379
static Z3_ast Z3_mk_bvshl(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2709
IntNum MkInt(int v)
Create an integer numeral.
Definition: Context.cs:2434
Tactic ParOr(params Tactic[] t)
Create a tactic that applies the given tactics in parallel.
Definition: Context.cs:3164
BitVecExpr MkBVNeg(BitVecExpr t)
Standard two's complement unary minus.
Definition: Context.cs:1271
static Z3_sort Z3_mk_fpa_sort_128(Z3_context a0)
Definition: Native.cs:6187
static Z3_probe Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4880
ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
Maps f on the argument arrays.
Definition: Context.cs:2080
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1283
Boolean expressions
Definition: BoolExpr.cs:31
static Z3_ast Z3_mk_real(Z3_context a0, int a1, int a2)
Definition: Native.cs:2981
static Z3_ast Z3_mk_fpa_numeral_float(Z3_context a0, float a1, Z3_sort a2)
Definition: Native.cs:6227
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3671
void Interrupt()
Interrupt the execution of a Z3 procedure.
Definition: Context.cs:3192
Probe Le(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value returned by p1 is less than or equal the valu...
Definition: Context.cs:3288
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:3540
static Z3_tactic Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3)
Definition: Native.cs:4800
FPNum MkFPInf(FPSort s, bool negative)
Create a floating-point infinity of sort s.
Definition: Context.cs:3649
Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
Create an expression representing an if-then-else: ite(t1, t2, t3).
Definition: Context.cs:839
Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create an existential Quantifier.
Definition: Context.cs:2598
Expr MkNumeral(ulong v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
Definition: Context.cs:2327
static Z3_ast Z3_mk_or(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2333
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
Definition: Probe.cs:34
FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
Create a new finite domain sort.
Definition: Context.cs:327
Expr MkConst(string name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:628
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
Definition: Context.cs:978
FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:506
static Z3_ast Z3_mk_fpa_to_fp_int_real(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3, Z3_sort a4)
Definition: Native.cs:6579
BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
Unsigned greater-than.
Definition: Context.cs:1535
FPSort MkFPSortSingle()
Create the single-precision (32-bit) FloatingPoint sort.
Definition: Context.cs:3581
Floating-point rounding mode numerals
Definition: FPRMNum.cs:31
static Z3_probe Z3_probe_eq(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4896
BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than or equal to.
Definition: Context.cs:1467
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
Definition: Context.cs:1036
static Z3_ast Z3_mk_fpa_is_negative(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6443
static Z3_ast Z3_mk_fpa_round_nearest_ties_to_away(Z3_context a0)
Definition: Native.cs:6059
static Z3_ast Z3_mk_bvredand(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2469
BoolExpr MkBoolConst(Symbol name)
Create a Boolean constant.
Definition: Context.cs:664
IntNum MkInt(uint v)
Create an integer numeral.
Definition: Context.cs:2446
static Z3_ast Z3_mk_fpa_fp(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:6219
Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 ...
Definition: Context.cs:2968
void ParseSMTLIBString(string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
Parse the given string using the SMT-LIB parser.
Definition: Context.cs:2729
Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create an existential Quantifier.
Definition: Context.cs:2616
BoolExpr MkEq(Expr x, Expr y)
Creates the equality x = y .
Definition: Context.cs:796
Probe And(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".
Definition: Context.cs:3333
static Z3_ast Z3_mk_fpa_leq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6363
static Z3_tactic Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, uint a2)
Definition: Native.cs:4784
Expr MkSetAdd(Expr set, Expr element)
Add an element to the set.
Definition: Context.cs:2148
static Z3_tactic Z3_tactic_fail(Z3_context a0)
Definition: Native.cs:4824
Expr MkEmptySet(Sort domain)
Create an empty set.
Definition: Context.cs:2124
static Z3_ast Z3_mk_fpa_round_toward_negative(Z3_context a0)
Definition: Native.cs:6091
static Z3_ast Z3_mk_implies(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2309
ListSort MkListSort(Symbol name, Sort elemSort)
Create a new list sort.
Definition: Context.cs:281
BoolExpr MkFPIsNaN(FPExpr t)
Predicate indicating whether t is a NaN.
Definition: Context.cs:4029
static Z3_solver Z3_mk_solver(Z3_context a0)
Definition: Native.cs:5062
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
Definition: Context.cs:1050
static Z3_ast Z3_mk_fpa_numeral_int64_uint64(Z3_context a0, int a1, Int64 a2, UInt64 a3, Z3_sort a4)
Definition: Native.cs:6259
DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
Create mutually recursive data-types.
Definition: Context.cs:440
static string Z3_simplify_get_help(Z3_context a0)
Definition: Native.cs:3765
static Z3_ast Z3_mk_set_add(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2909
Tactics are the basic building block for creating custom solvers for specific problem domains...
Definition: Tactic.cs:32
Expr MkSetDifference(Expr arg1, Expr arg2)
Take the difference between two sets.
Definition: Context.cs:2202
static Z3_ast Z3_mk_zero_ext(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2693
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:3706
static Z3_ast Z3_mk_le(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2413
static Z3_probe Z3_probe_const(Z3_context a0, double a1)
Definition: Native.cs:4856
static Z3_ast Z3_mk_set_subset(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2965
FPRMNum MkFPRoundTowardZero()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode...
Definition: Context.cs:3531
FPSort MkFPSort16()
Create the half-precision (16-bit) FloatingPoint sort.
Definition: Context.cs:3572
static Z3_ast Z3_mk_fpa_fma(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3, Z3_ast a4)
Definition: Native.cs:6315
FPNum MkFP(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition: Context.cs:3752
FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
Creates a fresh function declaration with a name prefixed with prefix .
Definition: Context.cs:523
BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise subtraction does not overflow.
Definition: Context.cs:1874
BoolExpr MkBoolConst(string name)
Create a Boolean constant.
Definition: Context.cs:675
BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise signed division does not overflow.
Definition: Context.cs:1908
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:565
FuncDecl MkConstDecl(Symbol name, Sort range)
Creates a new constant function declaration.
Definition: Context.cs:537
static Z3_ast Z3_mk_bvudiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2565
Solver MkSolver(string logic)
Creates a new (incremental) solver.
Definition: Context.cs:3396
BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Rotate Right.
Definition: Context.cs:1780
Probe Lt(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value returned by p1 is less than the value returne...
Definition: Context.cs:3258
A Boolean sort.
Definition: BoolSort.cs:28
static Z3_ast Z3_mk_fpa_inf(Z3_context a0, Z3_sort a1, int a2)
Definition: Native.cs:6203
static Z3_ast Z3_mk_fpa_is_infinite(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6427
static Z3_ast Z3_mk_fpa_to_sbv(Z3_context a0, Z3_ast a1, Z3_ast a2, uint a3)
Definition: Native.cs:6507
Expr MkNumeral(long v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
Definition: Context.cs:2311
static Z3_ast Z3_mk_is_int(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2453
RatNum MkReal(int v)
Create a real numeral.
Definition: Context.cs:2373
static Z3_ast Z3_mk_not(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2285
FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:475
Expr MkSetComplement(Expr arg)
Take the complement of a set.
Definition: Context.cs:2216
Vectors of ASTs.
Definition: ASTVector.cs:28
static Z3_ast Z3_mk_bvredor(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2477
FPExpr MkFPNeg(FPExpr t)
Floating-point negation
Definition: Context.cs:3801
DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
Create a new datatype sort.
Definition: Context.cs:390
static void Z3_interrupt(Z3_context a0)
Definition: Native.cs:1947
BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XNOR.
Definition: Context.cs:1256
BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Rotate Left.
Definition: Context.cs:1762
BitVecExpr MkBVRedAND(BitVecExpr t)
Take conjunction of bits in a vector, return vector of length 1.
Definition: Context.cs:1155
static Z3_ast Z3_mk_bvand(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2485
BoolExpr MkFPIsInfinite(FPExpr t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.
Definition: Context.cs:4019
BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than
Definition: Context.cs:1450
FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Definition: Context.cs:4087
static Z3_ast Z3_mk_sub(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2357
Expressions are terms.
Definition: Expr.cs:29
static Z3_func_decl Z3_get_smtlib_decl(Z3_context a0, uint a1)
Definition: Native.cs:4157
RealExpr MkRealConst(string name)
Creates a real constant.
Definition: Context.cs:718
static Z3_sort Z3_mk_bv_sort(Z3_context a0, uint a1)
Definition: Native.cs:2113
Expr MkSetIntersection(params Expr[] args)
Take the intersection of a list of sets.
Definition: Context.cs:2189
RealSort MkRealSort()
Create a real sort.
Definition: Context.cs:204
Expr MkSetUnion(params Expr[] args)
Take the union of a list of sets.
Definition: Context.cs:2177
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:3719
static string Z3_probe_get_descr(Z3_context a0, string a1)
Definition: Native.cs:4984
BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise NOR.
Definition: Context.cs:1241
static void Z3_set_ast_print_mode(Z3_context a0, uint a1)
Definition: Native.cs:4032
string TacticDescription(string name)
Returns a string containing a description of the tactic with the given name.
Definition: Context.cs:2947
Expr MkNumeral(int v, Sort ty)
Create a Term of a given sort. This function can be use to create numerals that fit in a machine inte...
Definition: Context.cs:2279
Expr MkSetDel(Expr set, Expr element)
Remove an element from a set.
Definition: Context.cs:2163
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3137
FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Conversion of a floating-point number to another FloatingPoint sort s.
Definition: Context.cs:4159
static string Z3_get_probe_name(Z3_context a0, uint a1)
Definition: Native.cs:4952
static Z3_ast Z3_mk_sign_ext(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2685
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
Definition: Context.cs:953
FuncDecl MkConstDecl(string name, Sort range)
Creates a new constant function declaration.
Definition: Context.cs:551
Tactic ParAndThen(Tactic t1, Tactic t2)
Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 ...
Definition: Context.cs:3177
BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
Two's complement addition.
Definition: Context.cs:1284
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:213
BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Signed division.
Definition: Context.cs:1358
Solver MkSolver(Tactic t)
Creates a solver that is implemented using the given tactic.
Definition: Context.cs:3420
A real sort
Definition: RealSort.cs:28
ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
Create an array constant.
Definition: Context.cs:1986
static Z3_ast Z3_mk_fpa_to_fp_unsigned(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
Definition: Native.cs:6491
static Z3_ast Z3_mk_bvsrem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2589
StringSymbol MkSymbol(string name)
Create a symbol using a string.
Definition: Context.cs:94
static Z3_ast Z3_parse_smtlib2_string(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
Definition: Native.cs:4087
static Z3_ast Z3_mk_repeat(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2701
Integer Numerals
Definition: IntNum.cs:32
FPSort MkFPSort128()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition: Context.cs:3626
static Z3_ast Z3_mk_fpa_rtn(Z3_context a0)
Definition: Native.cs:6099
BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XOR.
Definition: Context.cs:1211
BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Logical shift right
Definition: Context.cs:1687
BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise subtraction does not underflow.
Definition: Context.cs:1891
BitVecExpr MkSignExt(uint i, BitVecExpr t)
Bit-vector sign extension.
Definition: Context.cs:1610
static Z3_sort Z3_mk_fpa_sort_half(Z3_context a0)
Definition: Native.cs:6131
static Z3_ast Z3_mk_unsigned_int(Z3_context a0, uint a1, Z3_sort a2)
Definition: Native.cs:2997
static Z3_ast Z3_mk_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2269
Bit-vector expressions
Definition: BitVecExpr.cs:31
static Z3_ast Z3_mk_bvxnor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2525
static Z3_context Z3_mk_context_rc(Z3_config a0)
Definition: Native.cs:1915
static Z3_ast Z3_mk_bvadd_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2789
static Z3_ast Z3_mk_set_del(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2917
static Z3_ast Z3_mk_ext_rotate_left(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2749
static string Z3_benchmark_to_smtlib_string(Z3_context a0, string a1, string a2, string a3, string a4, uint a5, [In] Z3_ast[] a6, Z3_ast a7)
Definition: Native.cs:4079
FPNum MkFPZero(FPSort s, bool negative)
Create a floating-point zero of sort s.
Definition: Context.cs:3660
static Z3_ast Z3_mk_bvsdiv_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2813
BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise addition does not underflow.
Definition: Context.cs:1857
static Z3_ast Z3_mk_bvule(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2621
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
Definition: Context.cs:910
static Z3_ast Z3_mk_fpa_sub(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:6291
FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point addition
Definition: Context.cs:3813
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:3778
static Z3_ast Z3_mk_bvslt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2613
static Z3_ast Z3_mk_power(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2397
static Z3_ast Z3_mk_bvmul_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Definition: Native.cs:2829
BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
Two's complement signed greater-than.
Definition: Context.cs:1552
static Z3_ast Z3_mk_const_array(Z3_context a0, Z3_sort a1, Z3_ast a2)
Definition: Native.cs:2861
static Z3_ast Z3_mk_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2421
BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise multiplication does not overflow.
Definition: Context.cs:1940
static Z3_ast Z3_mk_xor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2317
BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
Floating-point equality.
Definition: Context.cs:3979
Constructors are used for datatype sorts.
Definition: Constructor.cs:29
Probe MkProbe(string name)
Creates a new Probe.
Definition: Context.cs:3237
static Z3_ast Z3_mk_ite(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:2293
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
Shift left.
Definition: Context.cs:1664
static Z3_ast Z3_mk_bvadd(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2541
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
Bitwise disjunction.
Definition: Context.cs:1196
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition: z3_api.h:1256
static Z3_ast Z3_mk_fpa_rem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6331
static void Z3_parse_smtlib_file(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
Definition: Native.cs:4110
FloatingPoint Expressions
Definition: FPExpr.cs:31
BitVecExpr MkBVConst(Symbol name, uint size)
Creates a bit-vector constant.
Definition: Context.cs:728
FPNum MkFP(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3741
static Z3_ast Z3_mk_iff(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2301
Array expressions
Definition: ArrayExpr.cs:31
static Z3_ast Z3_mk_and(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2325
static Z3_ast Z3_mk_unsigned_int64(Z3_context a0, UInt64 a1, Z3_sort a2)
Definition: Native.cs:3013
static Z3_ast Z3_mk_distinct(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2277
Tactic OrElse(Tactic t1, Tactic t2)
Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 appli...
Definition: Context.cs:3017
static Z3_ast Z3_mk_select(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2845
static Z3_ast Z3_mk_int2bv(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2765
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition: Context.cs:223
An Integer sort
Definition: IntSort.cs:28
static Z3_param_descrs Z3_simplify_get_param_descrs(Z3_context a0)
Definition: Native.cs:3773
static Z3_tactic Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Definition: Native.cs:4752
BoolSort MkBoolSort()
Create a new Boolean sort.
Definition: Context.cs:163
BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
Arithmetic shift right
Definition: Context.cs:1712
FPRMNum MkFPRoundNearestTiesToAway()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
Definition: Context.cs:3477
static Z3_ast Z3_mk_fpa_rtp(Z3_context a0)
Definition: Native.cs:6083
static Z3_sort Z3_mk_fpa_sort_16(Z3_context a0)
Definition: Native.cs:6139
BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
Two's complement signed less-than or equal to.
Definition: Context.cs:1484
static Z3_ast Z3_mk_false(Z3_context a0)
Definition: Native.cs:2261
BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
Rotate Right.
Definition: Context.cs:1746
static Z3_ast Z3_mk_bound(Z3_context a0, uint a1, Z3_sort a2)
Definition: Native.cs:3029
static Z3_ast Z3_mk_fpa_rtz(Z3_context a0)
Definition: Native.cs:6115
EnumSort MkEnumSort(string name, params string[] enumNames)
Create a new enumeration sort.
Definition: Context.cs:270
static Z3_ast Z3_mk_bvnor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2517
static Z3_probe Z3_probe_not(Z3_context a0, Z3_probe a1)
Definition: Native.cs:4920
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
Definition: ApplyResult.cs:30
static Z3_ast Z3_mk_fpa_nan(Z3_context a0, Z3_sort a1)
Definition: Native.cs:6195
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 -> t2.
Definition: Context.cs:869
static Z3_tactic Z3_tactic_fail_if(Z3_context a0, Z3_probe a1)
Definition: Native.cs:4832
BoolExpr MkFPIsNegative(FPExpr t)
Predicate indicating whether t is a negative floating-point number.
Definition: Context.cs:4039
static Z3_ast Z3_mk_bvsgt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2661
static Z3_probe Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4888
BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise multiplication does not underflow.
Definition: Context.cs:1957
static Z3_ast Z3_mk_fpa_numeral_double(Z3_context a0, double a1, Z3_sort a2)
Definition: Native.cs:6235
static Z3_ast Z3_mk_bvxor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2501
Enumeration sorts.
Definition: EnumSort.cs:29
FPRMNum MkFPRoundTowardPositive()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode...
Definition: Context.cs:3495
FPSort MkFPSortDouble()
Create the double-precision (64-bit) FloatingPoint sort.
Definition: Context.cs:3599
def EnumSort
Definition: z3py.py:4421
static uint Z3_get_smtlib_num_decls(Z3_context a0)
Definition: Native.cs:4149
BitVecExpr MkRepeat(uint i, BitVecExpr t)
Bit-vector repetition.
Definition: Context.cs:1643
Constructor MkConstructor(string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
Create a datatype constructor.
Definition: Context.cs:364
static Z3_ast Z3_mk_unary_minus(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2365
Expr MkSetSubset(Expr arg1, Expr arg2)
Check for subsetness of sets.
Definition: Context.cs:2242
static Z3_sort Z3_mk_fpa_sort_quadruple(Z3_context a0)
Definition: Native.cs:6179
static Z3_ast Z3_mk_fpa_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6371
static Z3_ast Z3_mk_set_member(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2957
Probe Or(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".
Definition: Context.cs:3348
static Z3_ast Z3_mk_fpa_is_zero(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6419
static Z3_ast Z3_mk_bvlshr(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2717
static Z3_ast Z3_mk_add(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2341
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
Definition: Context.cs:940
static void Z3_mk_datatypes(Z3_context a0, uint a1, [In] IntPtr[] a2, [Out] Z3_sort[] a3, [In, Out] Z3_constructor_list[] a4)
Definition: Native.cs:2199
static Z3_ast Z3_mk_fpa_to_fp_real(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
Definition: Native.cs:6475
static void Z3_del_context(Z3_context a0)
Definition: Native.cs:1922
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:295
static Z3_ast Z3_mk_fpa_sqrt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6323
static Z3_ast Z3_mk_full_set(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2901
BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise addition does not overflow.
Definition: Context.cs:1840
static Z3_ast Z3_mk_fpa_round_toward_zero(Z3_context a0)
Definition: Native.cs:6107
static Z3_ast Z3_mk_fpa_neg(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6275
BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
Floating-point less than.
Definition: Context.cs:3943
static Z3_tactic Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2)
Definition: Native.cs:4792
Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create a Quantifier.
Definition: Context.cs:2654
static Z3_ast Z3_mk_set_difference(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2941
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
Quantifier expressions.
Definition: Quantifier.cs:29
static Z3_ast Z3_mk_bvnot(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2461
BitVecNum MkBV(int v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2496
static void Z3_del_config(Z3_config a0)
Definition: Native.cs:1900
DecRefQueue interface
Definition: IDecRefQueue.cs:32
static Z3_config Z3_mk_config()
Definition: Native.cs:1895
static Z3_ast Z3_mk_bvsub(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2549
def ArraySort(d, r)
Definition: z3py.py:3978
static Z3_ast Z3_mk_bvsge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2645
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:1433
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition: Context.cs:883
static Z3_ast Z3_mk_store(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:2853
BoolExpr MkBVNegNoOverflow(BitVecExpr t)
Create a predicate that checks that the bit-wise negation does not overflow.
Definition: Context.cs:1925
Probe Eq(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value returned by p1 is equal to the value returned...
Definition: Context.cs:3318
BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
Bit-vector concatenation.
Definition: Context.cs:1573
static Z3_ast Z3_mk_ext_rotate_right(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2757
RealExpr MkInt2Real(IntExpr t)
Coerce an integer to a real.
Definition: Context.cs:1099
static Z3_ast Z3_mk_fpa_is_subnormal(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6411
FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point multiplication
Definition: Context.cs:3837
static Z3_ast Z3_mk_fpa_is_positive(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6451
IntExpr MkIntConst(string name)
Creates an integer constant.
Definition: Context.cs:696
BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
Floating-point greater than.
Definition: Context.cs:3965
static Z3_ast Z3_mk_rem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2389
static Z3_ast Z3_mk_ge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2429
static Z3_tactic Z3_tactic_fail_if_not_decided(Z3_context a0)
Definition: Native.cs:4840
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
Definition: Pattern.cs:32
EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
Create a new enumeration sort.
Definition: Context.cs:254
static Z3_ast Z3_mk_fpa_zero(Z3_context a0, Z3_sort a1, int a2)
Definition: Native.cs:6211
static Z3_solver Z3_mk_simple_solver(Z3_context a0)
Definition: Native.cs:5070
Tactic FailIf(Probe p)
Create a tactic that fails if the probe p evaluates to false.
Definition: Context.cs:3114
BitVecNum MkBV(uint v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2508
BitVecExpr MkBVRedOR(BitVecExpr t)
Take disjunction of bits in a vector, return vector of length 1.
Definition: Context.cs:1168
TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Create a new tuple sort.
Definition: Context.cs:237
FPExpr MkFPMin(FPExpr t1, FPExpr t2)
Minimum of floating-point numbers.
Definition: Context.cs:3910
Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create a universal Quantifier.
Definition: Context.cs:2582
static Z3_ast Z3_mk_fpa_to_ieee_bv(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6571
static Z3_sort Z3_get_smtlib_sort(Z3_context a0, uint a1)
Definition: Native.cs:4173
static Z3_ast Z3_mk_bvult(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2605
static Z3_tactic Z3_tactic_skip(Z3_context a0)
Definition: Native.cs:4816
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 iff t2.
Definition: Context.cs:855
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
static uint Z3_get_num_tactics(Z3_context a0)
Definition: Native.cs:4928
static Z3_ast Z3_mk_bvsub_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Definition: Native.cs:2805
Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 ...
Definition: Context.cs:3003
static Z3_ast Z3_mk_bvurem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2581
static Z3_ast Z3_mk_bvsdiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2573
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:3899
BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
Signed remainder.
Definition: Context.cs:1398
static Z3_probe Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4904
Tactic Fail()
Create a tactic always fails.
Definition: Context.cs:3104
BitVecExpr MkInt2BV(uint n, IntExpr t)
Create an n bit bit-vector from the integer argument t .
Definition: Context.cs:1801
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
BoolExpr MkNot(BoolExpr a)
Mk an expression representing not(a).
Definition: Context.cs:824
static uint Z3_get_smtlib_num_formulas(Z3_context a0)
Definition: Native.cs:4117
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
Definition: Context.cs:966
BoolExpr MkFPIsSubnormal(FPExpr t)
Predicate indicating whether t is a subnormal floating-point number.
Definition: Context.cs:3999
FPRMNum MkFPRTP()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode...
Definition: Context.cs:3504
static Z3_ast Z3_mk_bvsmod(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2597
static Z3_ast Z3_mk_rotate_right(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2741
FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
Floating-point square root
Definition: Context.cs:3876
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:31
ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 ^ t2.
Definition: Context.cs:1022
static Z3_ast Z3_mk_bvsle(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2629
static Z3_ast Z3_mk_int2real(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2437
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
static Z3_ast Z3_mk_rotate_left(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2733
static Z3_probe Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4872
Expr MkTermArray(ArrayExpr array)
Access the array default value.
Definition: Context.cs:2098
RatNum MkReal(ulong v)
Create a real numeral.
Definition: Context.cs:2409
ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
Array update.
Definition: Context.cs:2036
Rational Numerals
Definition: RatNum.cs:32
FPNum MkFPNumeral(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3682
Tactic With(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3152
The abstract syntax tree (AST) class.
Definition: AST.cs:31
FPSort MkFPSortQuadruple()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition: Context.cs:3617
FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point subtraction
Definition: Context.cs:3825
static uint Z3_get_smtlib_num_sorts(Z3_context a0)
Definition: Native.cs:4165
static Z3_ast Z3_mk_bvugt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2653
static Z3_ast Z3_mk_fpa_min(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6347
RealExpr MkRealConst(Symbol name)
Creates a real constant.
Definition: Context.cs:707
static Z3_ast Z3_mk_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2405
IntNum MkInt(ulong v)
Create an integer numeral.
Definition: Context.cs:2470
FloatingPoint RoundingMode Expressions
Definition: FPRMExpr.cs:31
FPRMNum MkFPRoundTowardNegative()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode...
Definition: Context.cs:3513
IntPtr UnwrapAST(AST a)
Unwraps an AST.
Definition: Context.cs:4269
static Z3_ast Z3_mk_fpa_mul(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:6299
static Z3_ast Z3_mk_fpa_is_nan(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6435
Object for managing fixedpoints
Definition: Fixedpoint.cs:29
static Z3_ast Z3_mk_fpa_add(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:6283
static Z3_ast Z3_mk_int(Z3_context a0, int a1, Z3_sort a2)
Definition: Native.cs:2989
FPNum MkFP(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3730
Probe ConstProbe(double val)
Create a probe that always evaluates to val .
Definition: Context.cs:3247
static void Z3_update_param_value(Z3_context a0, string a1, string a2)
Definition: Native.cs:1940
IntExpr MkBV2Int(BitVecExpr t, bool signed)
Create an integer from the bit-vector argument t .
Definition: Context.cs:1825
BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
Unsigned remainder.
Definition: Context.cs:1377
RatNum MkReal(long v)
Create a real numeral.
Definition: Context.cs:2397
Expr MkFullSet(Sort domain)
Create the full set.
Definition: Context.cs:2136
IntNum MkInt(long v)
Create an integer numeral.
Definition: Context.cs:2458
Expr MkSelect(ArrayExpr a, Expr i)
Array read.
Definition: Context.cs:2008
static Z3_tactic Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, uint a2)
Definition: Native.cs:4808
void ParseSMTLIBFile(string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
Parse the given file using the SMT-LIB parser.
Definition: Context.cs:2746
BoolExpr MkFPIsNormal(FPExpr t)
Predicate indicating whether t is a normal floating-point number.
Definition: Context.cs:3989
FPNum MkFPNumeral(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition: Context.cs:3693
Tactic Cond(Probe p, Tactic t1, Tactic t2)
Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise...
Definition: Context.cs:3065
static Z3_ast Z3_mk_set_union(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2925
Tactic FailIfNotDecided()
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatis...
Definition: Context.cs:3127
Z3_ast_print_mode
Z3_ast_print_mode
static Z3_ast Z3_mk_array_default(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2877
static Z3_ast Z3_mk_bvnand(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2509
BoolExpr MkFalse()
The false Term.
Definition: Context.cs:776
Set sorts.
Definition: SetSort.cs:29
BoolExpr MkFPIsZero(FPExpr t)
Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0...
Definition: Context.cs:4009
Tactic TryFor(Tactic t, uint ms)
Create a tactic that applies t to a goal for ms milliseconds.
Definition: Context.cs:3034
BitVecExpr MkBVConst(string name, uint size)
Creates a bit-vector constant.
Definition: Context.cs:739
BitVecNum MkBV(ulong v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2532
static Z3_ast Z3_mk_fpa_round_toward_positive(Z3_context a0)
Definition: Native.cs:6075
Probe Gt(Probe p1, Probe p2)
Create a probe that evaluates to "true" when the value returned by p1 is greater than the value retu...
Definition: Context.cs:3273
IntExpr MkRem(IntExpr t1, IntExpr t2)
Create an expression representing t1 rem t2.
Definition: Context.cs:1008
static Z3_ast Z3_mk_fpa_div(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:6307
FPSort MkFPSort32()
Create the single-precision (32-bit) FloatingPoint sort.
Definition: Context.cs:3590
static Z3_ast Z3_mk_int64(Z3_context a0, Int64 a1, Z3_sort a2)
Definition: Native.cs:3005
Tactic Skip()
Create a tactic that just returns the given goal.
Definition: Context.cs:3094
static Z3_ast Z3_mk_numeral(Z3_context a0, string a1, Z3_sort a2)
Definition: Native.cs:2973
FPSort MkFPSortHalf()
Create the half-precision (16-bit) FloatingPoint sort.
Definition: Context.cs:3563
FloatingPoint sort
Definition: FPSort.cs:27
IntExpr MkReal2Int(RealExpr t)
Coerce a real to an integer.
Definition: Context.cs:1115
static Z3_ast Z3_mk_bvneg(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2533
static Z3_ast Z3_mk_set_complement(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2949
static Z3_tactic Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2)
Definition: Native.cs:4848
BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
Two's complement subtraction.
Definition: Context.cs:1299
void Dispose()
Disposes of the context.
Definition: Context.cs:4503
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
Definition: Context.cs:810
static Z3_ast Z3_mk_fpa_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6387
FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:492
static uint Z3_get_smtlib_num_assumptions(Z3_context a0)
Definition: Native.cs:4133
def FPSort
Definition: z3py.py:7920
FPSort MkFPSort64()
Create the double-precision (64-bit) FloatingPoint sort.
Definition: Context.cs:3608
static Z3_ast Z3_mk_fpa_rne(Z3_context a0)
Definition: Native.cs:6051
Int expressions
Definition: IntExpr.cs:31
Context(Dictionary< string, string > settings)
Constructor.
Definition: Context.cs:62
Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create a Quantifier.
Definition: Context.cs:2631
FPRMNum MkFPRNA()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
Definition: Context.cs:3486
BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
Bitwise NAND.
Definition: Context.cs:1226
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
static Z3_ast Z3_mk_concat(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2669
static Z3_ast Z3_mk_fpa_numeral_int(Z3_context a0, int a1, Z3_sort a2)
Definition: Native.cs:6243
static Z3_solver Z3_mk_solver_for_logic(Z3_context a0, IntPtr a1)
Definition: Native.cs:5078
Numbered symbols
Definition: IntSymbol.cs:30
Function declarations.
Definition: FuncDecl.cs:29
static Z3_ast Z3_mk_fpa_to_fp_bv(Z3_context a0, Z3_ast a1, Z3_sort a2)
Definition: Native.cs:6459
Solver MkSimpleSolver()
Creates a new (incremental) solver.
Definition: Context.cs:3406
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:4233
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition: Context.cs:405
BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
Two's complement multiplication.
Definition: Context.cs:1314
BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
Floating-point greater than or equal.
Definition: Context.cs:3954
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
Definition: Context.cs:1078
static Z3_ast Z3_mk_div(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2373
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
Definition: Context.cs:172
Solvers.
Definition: Solver.cs:29
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
Definition: Context.cs:1064
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:993
Tuple sorts.
Definition: TupleSort.cs:29
static Z3_ast Z3_get_smtlib_assumption(Z3_context a0, uint a1)
Definition: Native.cs:4141
static Z3_ast Z3_parse_smtlib2_file(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
Definition: Native.cs:4095
static Z3_ast Z3_mk_fpa_rna(Z3_context a0)
Definition: Native.cs:6067
static Z3_sort Z3_mk_fpa_sort_32(Z3_context a0)
Definition: Native.cs:6155
BoolExpr MkFPIsPositive(FPExpr t)
Predicate indicating whether t is a positive floating-point number.
Definition: Context.cs:4049
BoolExpr MkBool(bool value)
Creates a Boolean value.
Definition: Context.cs:786
BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
Rotate Left.
Definition: Context.cs:1730
IntSort MkIntSort()
Create a new integer sort.
Definition: Context.cs:194
static Z3_ast Z3_mk_extract(Z3_context a0, uint a1, uint a2, Z3_ast a3)
Definition: Native.cs:2677
static Z3_ast Z3_mk_bvsub_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2797
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:31
BitVecExpr MkZeroExt(uint i, BitVecExpr t)
Bit-vector zero extension.
Definition: Context.cs:1628
Real expressions
Definition: RealExpr.cs:31
static Z3_ast Z3_mk_bvor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2493
RatNum MkReal(uint v)
Create a real numeral.
Definition: Context.cs:2385
A function interpretation is represented as a finite map and an 'else' 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:2871
Expr MkConst(FuncDecl f)
Creates a fresh constant from the FuncDecl f .
Definition: Context.cs:653
static void Z3_set_param_value(Z3_config a0, string a1, string a2)
Definition: Native.cs:1904
static Z3_sort Z3_mk_fpa_sort_single(Z3_context a0)
Definition: Native.cs:6147
static Z3_sort Z3_mk_fpa_sort_double(Z3_context a0)
Definition: Native.cs:6163
static Z3_probe Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:4864
static Z3_ast Z3_mk_map(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3)
Definition: Native.cs:2869