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 
458  public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
459  {
460  return Expr.Create(this, Native.Z3_datatype_update_field(
461  nCtx, field.NativeObject,
462  t.NativeObject, v.NativeObject));
463  }
464 
465  #endregion
466  #endregion
467 
468  #region Function Declarations
469  public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
473  {
474  Contract.Requires(name != null);
475  Contract.Requires(range != null);
476  Contract.Requires(Contract.ForAll(domain, d => d != null));
477  Contract.Ensures(Contract.Result<FuncDecl>() != null);
478 
479  CheckContextMatch(name);
480  CheckContextMatch(domain);
481  CheckContextMatch(range);
482  return new FuncDecl(this, name, domain, range);
483  }
484 
488  public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
489  {
490  Contract.Requires(name != null);
491  Contract.Requires(domain != null);
492  Contract.Requires(range != null);
493  Contract.Ensures(Contract.Result<FuncDecl>() != null);
494 
495  CheckContextMatch(name);
496  CheckContextMatch(domain);
497  CheckContextMatch(range);
498  Sort[] q = new Sort[] { domain };
499  return new FuncDecl(this, name, q, range);
500  }
501 
505  public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
506  {
507  Contract.Requires(range != null);
508  Contract.Requires(Contract.ForAll(domain, d => d != null));
509  Contract.Ensures(Contract.Result<FuncDecl>() != null);
510 
511  CheckContextMatch(domain);
512  CheckContextMatch(range);
513  return new FuncDecl(this, MkSymbol(name), domain, range);
514  }
515 
519  public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
520  {
521  Contract.Requires(range != null);
522  Contract.Requires(domain != null);
523  Contract.Ensures(Contract.Result<FuncDecl>() != null);
524 
525  CheckContextMatch(domain);
526  CheckContextMatch(range);
527  Sort[] q = new Sort[] { domain };
528  return new FuncDecl(this, MkSymbol(name), q, range);
529  }
530 
536  public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
537  {
538  Contract.Requires(range != null);
539  Contract.Requires(Contract.ForAll(domain, d => d != null));
540  Contract.Ensures(Contract.Result<FuncDecl>() != null);
541 
542  CheckContextMatch(domain);
543  CheckContextMatch(range);
544  return new FuncDecl(this, prefix, domain, range);
545  }
546 
550  public FuncDecl MkConstDecl(Symbol name, Sort range)
551  {
552  Contract.Requires(name != null);
553  Contract.Requires(range != null);
554  Contract.Ensures(Contract.Result<FuncDecl>() != null);
555 
556  CheckContextMatch(name);
557  CheckContextMatch(range);
558  return new FuncDecl(this, name, null, range);
559  }
560 
564  public FuncDecl MkConstDecl(string name, Sort range)
565  {
566  Contract.Requires(range != null);
567  Contract.Ensures(Contract.Result<FuncDecl>() != null);
568 
569  CheckContextMatch(range);
570  return new FuncDecl(this, MkSymbol(name), null, range);
571  }
572 
578  public FuncDecl MkFreshConstDecl(string prefix, Sort range)
579  {
580  Contract.Requires(range != null);
581  Contract.Ensures(Contract.Result<FuncDecl>() != null);
582 
583  CheckContextMatch(range);
584  return new FuncDecl(this, prefix, null, range);
585  }
586  #endregion
587 
588  #region Bound Variables
589  public Expr MkBound(uint index, Sort ty)
595  {
596  Contract.Requires(ty != null);
597  Contract.Ensures(Contract.Result<Expr>() != null);
598 
599  return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
600  }
601  #endregion
602 
603  #region Quantifier Patterns
604  public Pattern MkPattern(params Expr[] terms)
608  {
609  Contract.Requires(terms != null);
610  if (terms.Length == 0)
611  throw new Z3Exception("Cannot create a pattern from zero terms");
612 
613  Contract.Ensures(Contract.Result<Pattern>() != null);
614 
615  Contract.EndContractBlock();
616 
617  IntPtr[] termsNative = AST.ArrayToNative(terms);
618  return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
619  }
620  #endregion
621 
622  #region Constants
623  public Expr MkConst(Symbol name, Sort range)
627  {
628  Contract.Requires(name != null);
629  Contract.Requires(range != null);
630  Contract.Ensures(Contract.Result<Expr>() != null);
631 
632  CheckContextMatch(name);
633  CheckContextMatch(range);
634 
635  return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
636  }
637 
641  public Expr MkConst(string name, Sort range)
642  {
643  Contract.Requires(range != null);
644  Contract.Ensures(Contract.Result<Expr>() != null);
645 
646  return MkConst(MkSymbol(name), range);
647  }
648 
653  public Expr MkFreshConst(string prefix, Sort range)
654  {
655  Contract.Requires(range != null);
656  Contract.Ensures(Contract.Result<Expr>() != null);
657 
658  CheckContextMatch(range);
659  return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
660  }
661 
667  {
668  Contract.Requires(f != null);
669  Contract.Ensures(Contract.Result<Expr>() != null);
670 
671  return MkApp(f);
672  }
673 
678  {
679  Contract.Requires(name != null);
680  Contract.Ensures(Contract.Result<BoolExpr>() != null);
681 
682  return (BoolExpr)MkConst(name, BoolSort);
683  }
684 
688  public BoolExpr MkBoolConst(string name)
689  {
690  Contract.Ensures(Contract.Result<BoolExpr>() != null);
691 
692  return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
693  }
694 
698  public IntExpr MkIntConst(Symbol name)
699  {
700  Contract.Requires(name != null);
701  Contract.Ensures(Contract.Result<IntExpr>() != null);
702 
703  return (IntExpr)MkConst(name, IntSort);
704  }
705 
709  public IntExpr MkIntConst(string name)
710  {
711  Contract.Requires(name != null);
712  Contract.Ensures(Contract.Result<IntExpr>() != null);
713 
714  return (IntExpr)MkConst(name, IntSort);
715  }
716 
721  {
722  Contract.Requires(name != null);
723  Contract.Ensures(Contract.Result<RealExpr>() != null);
724 
725  return (RealExpr)MkConst(name, RealSort);
726  }
727 
731  public RealExpr MkRealConst(string name)
732  {
733  Contract.Ensures(Contract.Result<RealExpr>() != null);
734 
735  return (RealExpr)MkConst(name, RealSort);
736  }
737 
741  public BitVecExpr MkBVConst(Symbol name, uint size)
742  {
743  Contract.Requires(name != null);
744  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
745 
746  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
747  }
748 
752  public BitVecExpr MkBVConst(string name, uint size)
753  {
754  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
755 
756  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
757  }
758  #endregion
759 
760  #region Terms
761  public Expr MkApp(FuncDecl f, params Expr[] args)
765  {
766  Contract.Requires(f != null);
767  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
768  Contract.Ensures(Contract.Result<Expr>() != null);
769 
770  CheckContextMatch(f);
771  CheckContextMatch(args);
772  return Expr.Create(this, f, args);
773  }
774 
775  #region Propositional
776  public BoolExpr MkTrue()
780  {
781  Contract.Ensures(Contract.Result<BoolExpr>() != null);
782 
783  return new BoolExpr(this, Native.Z3_mk_true(nCtx));
784  }
785 
789  public BoolExpr MkFalse()
790  {
791  Contract.Ensures(Contract.Result<BoolExpr>() != null);
792 
793  return new BoolExpr(this, Native.Z3_mk_false(nCtx));
794  }
795 
799  public BoolExpr MkBool(bool value)
800  {
801  Contract.Ensures(Contract.Result<BoolExpr>() != null);
802 
803  return value ? MkTrue() : MkFalse();
804  }
805 
809  public BoolExpr MkEq(Expr x, Expr y)
810  {
811  Contract.Requires(x != null);
812  Contract.Requires(y != null);
813  Contract.Ensures(Contract.Result<BoolExpr>() != null);
814 
815  CheckContextMatch(x);
816  CheckContextMatch(y);
817  return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
818  }
819 
823  public BoolExpr MkDistinct(params Expr[] args)
824  {
825  Contract.Requires(args != null);
826  Contract.Requires(Contract.ForAll(args, a => a != null));
827 
828  Contract.Ensures(Contract.Result<BoolExpr>() != null);
829 
830  CheckContextMatch(args);
831  return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
832  }
833 
838  {
839  Contract.Requires(a != null);
840  Contract.Ensures(Contract.Result<BoolExpr>() != null);
841 
842  CheckContextMatch(a);
843  return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
844  }
845 
852  public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
853  {
854  Contract.Requires(t1 != null);
855  Contract.Requires(t2 != null);
856  Contract.Requires(t3 != null);
857  Contract.Ensures(Contract.Result<Expr>() != null);
858 
859  CheckContextMatch(t1);
860  CheckContextMatch(t2);
861  CheckContextMatch(t3);
862  return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
863  }
864 
869  {
870  Contract.Requires(t1 != null);
871  Contract.Requires(t2 != null);
872  Contract.Ensures(Contract.Result<BoolExpr>() != null);
873 
874  CheckContextMatch(t1);
875  CheckContextMatch(t2);
876  return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
877  }
878 
883  {
884  Contract.Requires(t1 != null);
885  Contract.Requires(t2 != null);
886  Contract.Ensures(Contract.Result<BoolExpr>() != null);
887 
888  CheckContextMatch(t1);
889  CheckContextMatch(t2);
890  return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
891  }
892 
897  {
898  Contract.Requires(t1 != null);
899  Contract.Requires(t2 != null);
900  Contract.Ensures(Contract.Result<BoolExpr>() != null);
901 
902  CheckContextMatch(t1);
903  CheckContextMatch(t2);
904  return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
905  }
906 
910  public BoolExpr MkAnd(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_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
918  }
919 
923  public BoolExpr MkOr(params BoolExpr[] t)
924  {
925  Contract.Requires(t != null);
926  Contract.Requires(Contract.ForAll(t, a => a != null));
927  Contract.Ensures(Contract.Result<BoolExpr>() != null);
928 
929  CheckContextMatch(t);
930  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
931  }
932 
933 
934  #endregion
935 
936  #region Arithmetic
937  public ArithExpr MkAdd(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_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
948  }
949 
953  public ArithExpr MkMul(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_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
961  }
962 
966  public ArithExpr MkSub(params ArithExpr[] t)
967  {
968  Contract.Requires(t != null);
969  Contract.Requires(Contract.ForAll(t, a => a != null));
970  Contract.Ensures(Contract.Result<ArithExpr>() != null);
971 
972  CheckContextMatch(t);
973  return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
974  }
975 
980  {
981  Contract.Requires(t != null);
982  Contract.Ensures(Contract.Result<ArithExpr>() != null);
983 
984  CheckContextMatch(t);
985  return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
986  }
987 
992  {
993  Contract.Requires(t1 != null);
994  Contract.Requires(t2 != null);
995  Contract.Ensures(Contract.Result<ArithExpr>() != null);
996 
997  CheckContextMatch(t1);
998  CheckContextMatch(t2);
999  return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1000  }
1001 
1006  public IntExpr MkMod(IntExpr t1, IntExpr t2)
1007  {
1008  Contract.Requires(t1 != null);
1009  Contract.Requires(t2 != null);
1010  Contract.Ensures(Contract.Result<IntExpr>() != null);
1011 
1012  CheckContextMatch(t1);
1013  CheckContextMatch(t2);
1014  return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1015  }
1016 
1021  public IntExpr MkRem(IntExpr t1, IntExpr t2)
1022  {
1023  Contract.Requires(t1 != null);
1024  Contract.Requires(t2 != null);
1025  Contract.Ensures(Contract.Result<IntExpr>() != null);
1026 
1027  CheckContextMatch(t1);
1028  CheckContextMatch(t2);
1029  return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1030  }
1031 
1036  {
1037  Contract.Requires(t1 != null);
1038  Contract.Requires(t2 != null);
1039  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1040 
1041  CheckContextMatch(t1);
1042  CheckContextMatch(t2);
1043  return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1044  }
1045 
1050  {
1051  Contract.Requires(t1 != null);
1052  Contract.Requires(t2 != null);
1053  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1054 
1055  CheckContextMatch(t1);
1056  CheckContextMatch(t2);
1057  return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1058  }
1059 
1064  {
1065  Contract.Requires(t1 != null);
1066  Contract.Requires(t2 != null);
1067  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1068 
1069  CheckContextMatch(t1);
1070  CheckContextMatch(t2);
1071  return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1072  }
1073 
1078  {
1079  Contract.Requires(t1 != null);
1080  Contract.Requires(t2 != null);
1081  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1082 
1083  CheckContextMatch(t1);
1084  CheckContextMatch(t2);
1085  return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1086  }
1087 
1092  {
1093  Contract.Requires(t1 != null);
1094  Contract.Requires(t2 != null);
1095  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1096 
1097  CheckContextMatch(t1);
1098  CheckContextMatch(t2);
1099  return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1100  }
1101 
1113  {
1114  Contract.Requires(t != null);
1115  Contract.Ensures(Contract.Result<RealExpr>() != null);
1116 
1117  CheckContextMatch(t);
1118  return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1119  }
1120 
1129  {
1130  Contract.Requires(t != null);
1131  Contract.Ensures(Contract.Result<IntExpr>() != null);
1132 
1133  CheckContextMatch(t);
1134  return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1135  }
1136 
1141  {
1142  Contract.Requires(t != null);
1143  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1144 
1145  CheckContextMatch(t);
1146  return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1147  }
1148  #endregion
1149 
1150  #region Bit-vectors
1151  public BitVecExpr MkBVNot(BitVecExpr t)
1156  {
1157  Contract.Requires(t != null);
1158  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1159 
1160  CheckContextMatch(t);
1161  return new BitVecExpr(this, Native.Z3_mk_bvnot(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_bvredand(nCtx, t.NativeObject));
1175  }
1176 
1182  {
1183  Contract.Requires(t != null);
1184  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1185 
1186  CheckContextMatch(t);
1187  return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1188  }
1189 
1195  {
1196  Contract.Requires(t1 != null);
1197  Contract.Requires(t2 != null);
1198  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1199 
1200  CheckContextMatch(t1);
1201  CheckContextMatch(t2);
1202  return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1203  }
1204 
1210  {
1211  Contract.Requires(t1 != null);
1212  Contract.Requires(t2 != null);
1213  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1214 
1215  CheckContextMatch(t1);
1216  CheckContextMatch(t2);
1217  return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1218  }
1219 
1225  {
1226  Contract.Requires(t1 != null);
1227  Contract.Requires(t2 != null);
1228  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1229 
1230  CheckContextMatch(t1);
1231  CheckContextMatch(t2);
1232  return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1233  }
1234 
1240  {
1241  Contract.Requires(t1 != null);
1242  Contract.Requires(t2 != null);
1243  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1244 
1245  CheckContextMatch(t1);
1246  CheckContextMatch(t2);
1247  return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1248  }
1249 
1255  {
1256  Contract.Requires(t1 != null);
1257  Contract.Requires(t2 != null);
1258  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1259 
1260  CheckContextMatch(t1);
1261  CheckContextMatch(t2);
1262  return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1263  }
1264 
1270  {
1271  Contract.Requires(t1 != null);
1272  Contract.Requires(t2 != null);
1273  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1274 
1275  CheckContextMatch(t1);
1276  CheckContextMatch(t2);
1277  return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1278  }
1279 
1285  {
1286  Contract.Requires(t != null);
1287  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1288 
1289  CheckContextMatch(t);
1290  return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1291  }
1292 
1298  {
1299  Contract.Requires(t1 != null);
1300  Contract.Requires(t2 != null);
1301  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1302 
1303  CheckContextMatch(t1);
1304  CheckContextMatch(t2);
1305  return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1306  }
1307 
1313  {
1314  Contract.Requires(t1 != null);
1315  Contract.Requires(t2 != null);
1316  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1317 
1318  CheckContextMatch(t1);
1319  CheckContextMatch(t2);
1320  return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1321  }
1322 
1328  {
1329  Contract.Requires(t1 != null);
1330  Contract.Requires(t2 != null);
1331  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1332 
1333  CheckContextMatch(t1);
1334  CheckContextMatch(t2);
1335  return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1336  }
1337 
1348  {
1349  Contract.Requires(t1 != null);
1350  Contract.Requires(t2 != null);
1351  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1352 
1353  CheckContextMatch(t1);
1354  CheckContextMatch(t2);
1355  return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1356  }
1357 
1372  {
1373  Contract.Requires(t1 != null);
1374  Contract.Requires(t2 != null);
1375  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1376 
1377  CheckContextMatch(t1);
1378  CheckContextMatch(t2);
1379  return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1380  }
1381 
1391  {
1392  Contract.Requires(t1 != null);
1393  Contract.Requires(t2 != null);
1394  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1395 
1396  CheckContextMatch(t1);
1397  CheckContextMatch(t2);
1398  return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1399  }
1400 
1412  {
1413  Contract.Requires(t1 != null);
1414  Contract.Requires(t2 != null);
1415  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1416 
1417  CheckContextMatch(t1);
1418  CheckContextMatch(t2);
1419  return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1420  }
1421 
1430  {
1431  Contract.Requires(t1 != null);
1432  Contract.Requires(t2 != null);
1433  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1434 
1435  CheckContextMatch(t1);
1436  CheckContextMatch(t2);
1437  return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1438  }
1439 
1447  {
1448  Contract.Requires(t1 != null);
1449  Contract.Requires(t2 != null);
1450  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1451 
1452  CheckContextMatch(t1);
1453  CheckContextMatch(t2);
1454  return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1455  }
1456 
1464  {
1465  Contract.Requires(t1 != null);
1466  Contract.Requires(t2 != null);
1467  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1468 
1469  CheckContextMatch(t1);
1470  CheckContextMatch(t2);
1471  return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1472  }
1473 
1481  {
1482  Contract.Requires(t1 != null);
1483  Contract.Requires(t2 != null);
1484  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1485 
1486  CheckContextMatch(t1);
1487  CheckContextMatch(t2);
1488  return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1489  }
1490 
1498  {
1499  Contract.Requires(t1 != null);
1500  Contract.Requires(t2 != null);
1501  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1502 
1503  CheckContextMatch(t1);
1504  CheckContextMatch(t2);
1505  return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1506  }
1507 
1515  {
1516  Contract.Requires(t1 != null);
1517  Contract.Requires(t2 != null);
1518  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1519 
1520  CheckContextMatch(t1);
1521  CheckContextMatch(t2);
1522  return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1523  }
1524 
1532  {
1533  Contract.Requires(t1 != null);
1534  Contract.Requires(t2 != null);
1535  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1536 
1537  CheckContextMatch(t1);
1538  CheckContextMatch(t2);
1539  return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1540  }
1541 
1549  {
1550  Contract.Requires(t1 != null);
1551  Contract.Requires(t2 != null);
1552  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1553 
1554  CheckContextMatch(t1);
1555  CheckContextMatch(t2);
1556  return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1557  }
1558 
1566  {
1567  Contract.Requires(t1 != null);
1568  Contract.Requires(t2 != null);
1569  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1570 
1571  CheckContextMatch(t1);
1572  CheckContextMatch(t2);
1573  return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1574  }
1575 
1587  {
1588  Contract.Requires(t1 != null);
1589  Contract.Requires(t2 != null);
1590  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1591 
1592  CheckContextMatch(t1);
1593  CheckContextMatch(t2);
1594  return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1595  }
1596 
1606  public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
1607  {
1608  Contract.Requires(t != null);
1609  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1610 
1611  CheckContextMatch(t);
1612  return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1613  }
1614 
1623  public BitVecExpr MkSignExt(uint i, BitVecExpr t)
1624  {
1625  Contract.Requires(t != null);
1626  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1627 
1628  CheckContextMatch(t);
1629  return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1630  }
1631 
1641  public BitVecExpr MkZeroExt(uint i, BitVecExpr t)
1642  {
1643  Contract.Requires(t != null);
1644  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1645 
1646  CheckContextMatch(t);
1647  return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1648  }
1649 
1656  public BitVecExpr MkRepeat(uint i, BitVecExpr t)
1657  {
1658  Contract.Requires(t != null);
1659  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1660 
1661  CheckContextMatch(t);
1662  return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1663  }
1664 
1678  {
1679  Contract.Requires(t1 != null);
1680  Contract.Requires(t2 != null);
1681  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1682 
1683  CheckContextMatch(t1);
1684  CheckContextMatch(t2);
1685  return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1686  }
1687 
1701  {
1702  Contract.Requires(t1 != null);
1703  Contract.Requires(t2 != null);
1704  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1705 
1706  CheckContextMatch(t1);
1707  CheckContextMatch(t2);
1708  return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1709  }
1710 
1726  {
1727  Contract.Requires(t1 != null);
1728  Contract.Requires(t2 != null);
1729  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1730 
1731  CheckContextMatch(t1);
1732  CheckContextMatch(t2);
1733  return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1734  }
1735 
1744  {
1745  Contract.Requires(t != null);
1746  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1747 
1748  CheckContextMatch(t);
1749  return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1750  }
1751 
1760  {
1761  Contract.Requires(t != null);
1762  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1763 
1764  CheckContextMatch(t);
1765  return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1766  }
1767 
1776  {
1777  Contract.Requires(t1 != null);
1778  Contract.Requires(t2 != null);
1779  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1780 
1781  CheckContextMatch(t1);
1782  CheckContextMatch(t2);
1783  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1784  }
1785 
1794  {
1795  Contract.Requires(t1 != null);
1796  Contract.Requires(t2 != null);
1797  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1798 
1799  CheckContextMatch(t1);
1800  CheckContextMatch(t2);
1801  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1802  }
1803 
1814  public BitVecExpr MkInt2BV(uint n, IntExpr t)
1815  {
1816  Contract.Requires(t != null);
1817  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1818 
1819  CheckContextMatch(t);
1820  return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1821  }
1822 
1838  public IntExpr MkBV2Int(BitVecExpr t, bool signed)
1839  {
1840  Contract.Requires(t != null);
1841  Contract.Ensures(Contract.Result<IntExpr>() != null);
1842 
1843  CheckContextMatch(t);
1844  return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
1845  }
1846 
1853  public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1854  {
1855  Contract.Requires(t1 != null);
1856  Contract.Requires(t2 != null);
1857  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1858 
1859  CheckContextMatch(t1);
1860  CheckContextMatch(t2);
1861  return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1862  }
1863 
1871  {
1872  Contract.Requires(t1 != null);
1873  Contract.Requires(t2 != null);
1874  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1875 
1876  CheckContextMatch(t1);
1877  CheckContextMatch(t2);
1878  return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1879  }
1880 
1888  {
1889  Contract.Requires(t1 != null);
1890  Contract.Requires(t2 != null);
1891  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1892 
1893  CheckContextMatch(t1);
1894  CheckContextMatch(t2);
1895  return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1896  }
1897 
1904  public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1905  {
1906  Contract.Requires(t1 != null);
1907  Contract.Requires(t2 != null);
1908  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1909 
1910  CheckContextMatch(t1);
1911  CheckContextMatch(t2);
1912  return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1913  }
1914 
1922  {
1923  Contract.Requires(t1 != null);
1924  Contract.Requires(t2 != null);
1925  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1926 
1927  CheckContextMatch(t1);
1928  CheckContextMatch(t2);
1929  return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1930  }
1931 
1939  {
1940  Contract.Requires(t != null);
1941  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1942 
1943  CheckContextMatch(t);
1944  return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
1945  }
1946 
1953  public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
1954  {
1955  Contract.Requires(t1 != null);
1956  Contract.Requires(t2 != null);
1957  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1958 
1959  CheckContextMatch(t1);
1960  CheckContextMatch(t2);
1961  return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1962  }
1963 
1971  {
1972  Contract.Requires(t1 != null);
1973  Contract.Requires(t2 != null);
1974  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1975 
1976  CheckContextMatch(t1);
1977  CheckContextMatch(t2);
1978  return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1979  }
1980  #endregion
1981 
1982  #region Arrays
1983  public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
1987  {
1988  Contract.Requires(name != null);
1989  Contract.Requires(domain != null);
1990  Contract.Requires(range != null);
1991  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
1992 
1993  return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
1994  }
1995 
1999  public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
2000  {
2001  Contract.Requires(domain != null);
2002  Contract.Requires(range != null);
2003  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2004 
2005  return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
2006  }
2007 
2022  {
2023  Contract.Requires(a != null);
2024  Contract.Requires(i != null);
2025  Contract.Ensures(Contract.Result<Expr>() != null);
2026 
2027  CheckContextMatch(a);
2028  CheckContextMatch(i);
2029  return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2030  }
2031 
2050  {
2051  Contract.Requires(a != null);
2052  Contract.Requires(i != null);
2053  Contract.Requires(v != null);
2054  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2055 
2056  CheckContextMatch(a);
2057  CheckContextMatch(i);
2058  CheckContextMatch(v);
2059  return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2060  }
2061 
2071  public ArrayExpr MkConstArray(Sort domain, Expr v)
2072  {
2073  Contract.Requires(domain != null);
2074  Contract.Requires(v != null);
2075  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2076 
2077  CheckContextMatch(domain);
2078  CheckContextMatch(v);
2079  return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2080  }
2081 
2093  public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
2094  {
2095  Contract.Requires(f != null);
2096  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2097  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2098 
2099  CheckContextMatch(f);
2100  CheckContextMatch(args);
2101  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2102  }
2103 
2112  {
2113  Contract.Requires(array != null);
2114  Contract.Ensures(Contract.Result<Expr>() != null);
2115 
2116  CheckContextMatch(array);
2117  return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2118  }
2119  #endregion
2120 
2121  #region Sets
2122  public SetSort MkSetSort(Sort ty)
2126  {
2127  Contract.Requires(ty != null);
2128  Contract.Ensures(Contract.Result<SetSort>() != null);
2129 
2130  CheckContextMatch(ty);
2131  return new SetSort(this, ty);
2132  }
2133 
2137  public ArrayExpr MkEmptySet(Sort domain)
2138  {
2139  Contract.Requires(domain != null);
2140  Contract.Ensures(Contract.Result<Expr>() != null);
2141 
2142  CheckContextMatch(domain);
2143  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2144  }
2145 
2149  public ArrayExpr MkFullSet(Sort domain)
2150  {
2151  Contract.Requires(domain != null);
2152  Contract.Ensures(Contract.Result<Expr>() != null);
2153 
2154  CheckContextMatch(domain);
2155  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2156  }
2157 
2161  public ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
2162  {
2163  Contract.Requires(set != null);
2164  Contract.Requires(element != null);
2165  Contract.Ensures(Contract.Result<Expr>() != null);
2166 
2167  CheckContextMatch(set);
2168  CheckContextMatch(element);
2169  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2170  }
2171 
2172 
2176  public ArrayExpr MkSetDel(ArrayExpr set, Expr element)
2177  {
2178  Contract.Requires(set != null);
2179  Contract.Requires(element != null);
2180  Contract.Ensures(Contract.Result<Expr>() != null);
2181 
2182  CheckContextMatch(set);
2183  CheckContextMatch(element);
2184  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2185  }
2186 
2190  public ArrayExpr MkSetUnion(params ArrayExpr[] args)
2191  {
2192  Contract.Requires(args != null);
2193  Contract.Requires(Contract.ForAll(args, a => a != null));
2194 
2195  CheckContextMatch(args);
2196  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2197  }
2198 
2202  public ArrayExpr MkSetIntersection(params ArrayExpr[] args)
2203  {
2204  Contract.Requires(args != null);
2205  Contract.Requires(Contract.ForAll(args, a => a != null));
2206  Contract.Ensures(Contract.Result<Expr>() != null);
2207 
2208  CheckContextMatch(args);
2209  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2210  }
2211 
2216  {
2217  Contract.Requires(arg1 != null);
2218  Contract.Requires(arg2 != null);
2219  Contract.Ensures(Contract.Result<Expr>() != null);
2220 
2221  CheckContextMatch(arg1);
2222  CheckContextMatch(arg2);
2223  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2224  }
2225 
2230  {
2231  Contract.Requires(arg != null);
2232  Contract.Ensures(Contract.Result<Expr>() != null);
2233 
2234  CheckContextMatch(arg);
2235  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2236  }
2237 
2242  {
2243  Contract.Requires(elem != null);
2244  Contract.Requires(set != null);
2245  Contract.Ensures(Contract.Result<Expr>() != null);
2246 
2247  CheckContextMatch(elem);
2248  CheckContextMatch(set);
2249  return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2250  }
2251 
2256  {
2257  Contract.Requires(arg1 != null);
2258  Contract.Requires(arg2 != null);
2259  Contract.Ensures(Contract.Result<Expr>() != null);
2260 
2261  CheckContextMatch(arg1);
2262  CheckContextMatch(arg2);
2263  return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2264  }
2265  #endregion
2266 
2267  #region Pseudo-Boolean constraints
2268 
2272  public BoolExpr MkAtMost(BoolExpr[] args, uint k)
2273  {
2274  Contract.Requires(args != null);
2275  Contract.Requires(Contract.Result<BoolExpr[]>() != null);
2276  CheckContextMatch(args);
2277  return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length,
2278  AST.ArrayToNative(args), k));
2279  }
2280 
2284  public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
2285  {
2286  Contract.Requires(args != null);
2287  Contract.Requires(coeffs != null);
2288  Contract.Requires(args.Length == coeffs.Length);
2289  Contract.Requires(Contract.Result<BoolExpr[]>() != null);
2290  CheckContextMatch(args);
2291  return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
2292  AST.ArrayToNative(args),
2293  coeffs, k));
2294  }
2295  #endregion
2296 
2297  #region Numerals
2298 
2299  #region General Numerals
2300  public Expr MkNumeral(string v, Sort ty)
2307  {
2308  Contract.Requires(ty != null);
2309  Contract.Ensures(Contract.Result<Expr>() != null);
2310 
2311  CheckContextMatch(ty);
2312  return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2313  }
2314 
2322  public Expr MkNumeral(int v, Sort ty)
2323  {
2324  Contract.Requires(ty != null);
2325  Contract.Ensures(Contract.Result<Expr>() != null);
2326 
2327  CheckContextMatch(ty);
2328  return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2329  }
2330 
2338  public Expr MkNumeral(uint v, Sort ty)
2339  {
2340  Contract.Requires(ty != null);
2341  Contract.Ensures(Contract.Result<Expr>() != null);
2342 
2343  CheckContextMatch(ty);
2344  return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2345  }
2346 
2354  public Expr MkNumeral(long v, Sort ty)
2355  {
2356  Contract.Requires(ty != null);
2357  Contract.Ensures(Contract.Result<Expr>() != null);
2358 
2359  CheckContextMatch(ty);
2360  return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2361  }
2362 
2370  public Expr MkNumeral(ulong v, Sort ty)
2371  {
2372  Contract.Requires(ty != null);
2373  Contract.Ensures(Contract.Result<Expr>() != null);
2374 
2375  CheckContextMatch(ty);
2376  return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2377  }
2378  #endregion
2379 
2380  #region Reals
2381  public RatNum MkReal(int num, int den)
2389  {
2390  if (den == 0)
2391  throw new Z3Exception("Denominator is zero");
2392 
2393  Contract.Ensures(Contract.Result<RatNum>() != null);
2394  Contract.EndContractBlock();
2395 
2396  return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
2397  }
2398 
2404  public RatNum MkReal(string v)
2405  {
2406  Contract.Ensures(Contract.Result<RatNum>() != null);
2407 
2408  return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
2409  }
2410 
2416  public RatNum MkReal(int v)
2417  {
2418  Contract.Ensures(Contract.Result<RatNum>() != null);
2419 
2420  return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
2421  }
2422 
2428  public RatNum MkReal(uint v)
2429  {
2430  Contract.Ensures(Contract.Result<RatNum>() != null);
2431 
2432  return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
2433  }
2434 
2440  public RatNum MkReal(long v)
2441  {
2442  Contract.Ensures(Contract.Result<RatNum>() != null);
2443 
2444  return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
2445  }
2446 
2452  public RatNum MkReal(ulong v)
2453  {
2454  Contract.Ensures(Contract.Result<RatNum>() != null);
2455 
2456  return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
2457  }
2458  #endregion
2459 
2460  #region Integers
2461  public IntNum MkInt(string v)
2466  {
2467  Contract.Ensures(Contract.Result<IntNum>() != null);
2468 
2469  return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
2470  }
2471 
2477  public IntNum MkInt(int v)
2478  {
2479  Contract.Ensures(Contract.Result<IntNum>() != null);
2480 
2481  return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
2482  }
2483 
2489  public IntNum MkInt(uint v)
2490  {
2491  Contract.Ensures(Contract.Result<IntNum>() != null);
2492 
2493  return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
2494  }
2495 
2501  public IntNum MkInt(long v)
2502  {
2503  Contract.Ensures(Contract.Result<IntNum>() != null);
2504 
2505  return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
2506  }
2507 
2513  public IntNum MkInt(ulong v)
2514  {
2515  Contract.Ensures(Contract.Result<IntNum>() != null);
2516 
2517  return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
2518  }
2519  #endregion
2520 
2521  #region Bit-vectors
2522  public BitVecNum MkBV(string v, uint size)
2528  {
2529  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2530 
2531  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2532  }
2533 
2539  public BitVecNum MkBV(int v, uint size)
2540  {
2541  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2542 
2543  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2544  }
2545 
2551  public BitVecNum MkBV(uint v, uint size)
2552  {
2553  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2554 
2555  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2556  }
2557 
2563  public BitVecNum MkBV(long v, uint size)
2564  {
2565  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2566 
2567  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2568  }
2569 
2575  public BitVecNum MkBV(ulong v, uint size)
2576  {
2577  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2578 
2579  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2580  }
2581  #endregion
2582 
2583  #endregion // Numerals
2584 
2585  #region Quantifiers
2586  public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2606  {
2607  Contract.Requires(sorts != null);
2608  Contract.Requires(names != null);
2609  Contract.Requires(body != null);
2610  Contract.Requires(sorts.Length == names.Length);
2611  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2612  Contract.Requires(Contract.ForAll(names, n => n != null));
2613  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2614  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2615 
2616  Contract.Ensures(Contract.Result<Quantifier>() != null);
2617 
2618  return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2619  }
2620 
2621 
2625  public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2626  {
2627  Contract.Requires(body != null);
2628  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
2629  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2630  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2631 
2632  Contract.Ensures(Contract.Result<Quantifier>() != null);
2633 
2634  return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2635  }
2636 
2641  public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2642  {
2643  Contract.Requires(sorts != null);
2644  Contract.Requires(names != null);
2645  Contract.Requires(body != null);
2646  Contract.Requires(sorts.Length == names.Length);
2647  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2648  Contract.Requires(Contract.ForAll(names, n => n != null));
2649  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2650  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2651  Contract.Ensures(Contract.Result<Quantifier>() != null);
2652 
2653  return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2654  }
2655 
2659  public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2660  {
2661  Contract.Requires(body != null);
2662  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2663  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2664  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2665  Contract.Ensures(Contract.Result<Quantifier>() != null);
2666 
2667  return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2668  }
2669 
2670 
2674  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)
2675  {
2676  Contract.Requires(body != null);
2677  Contract.Requires(names != null);
2678  Contract.Requires(sorts != null);
2679  Contract.Requires(sorts.Length == names.Length);
2680  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2681  Contract.Requires(Contract.ForAll(names, n => n != null));
2682  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2683  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2684 
2685  Contract.Ensures(Contract.Result<Quantifier>() != null);
2686 
2687  if (universal)
2688  return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2689  else
2690  return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2691  }
2692 
2693 
2697  public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
2698  {
2699  Contract.Requires(body != null);
2700  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2701  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2702  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2703 
2704  Contract.Ensures(Contract.Result<Quantifier>() != null);
2705 
2706  if (universal)
2707  return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2708  else
2709  return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2710  }
2711 
2712  #endregion
2713 
2714  #endregion // Expr
2715 
2716  #region Options
2717  public Z3_ast_print_mode PrintMode
2734  {
2735  set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
2736  }
2737  #endregion
2738 
2739  #region SMT Files & Strings
2740  public string BenchmarkToSMTString(string name, string logic, string status, string attributes,
2751  BoolExpr[] assumptions, BoolExpr formula)
2752  {
2753  Contract.Requires(assumptions != null);
2754  Contract.Requires(formula != null);
2755  Contract.Ensures(Contract.Result<string>() != null);
2756 
2757  return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
2758  (uint)assumptions.Length, AST.ArrayToNative(assumptions),
2759  formula.NativeObject);
2760  }
2761 
2772  public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2773  {
2774  uint csn = Symbol.ArrayLength(sortNames);
2775  uint cs = Sort.ArrayLength(sorts);
2776  uint cdn = Symbol.ArrayLength(declNames);
2777  uint cd = AST.ArrayLength(decls);
2778  if (csn != cs || cdn != cd)
2779  throw new Z3Exception("Argument size mismatch");
2780  Native.Z3_parse_smtlib_string(nCtx, str,
2781  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2782  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2783  }
2784 
2789  public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2790  {
2791  uint csn = Symbol.ArrayLength(sortNames);
2792  uint cs = Sort.ArrayLength(sorts);
2793  uint cdn = Symbol.ArrayLength(declNames);
2794  uint cd = AST.ArrayLength(decls);
2795  if (csn != cs || cdn != cd)
2796  throw new Z3Exception("Argument size mismatch");
2797  Native.Z3_parse_smtlib_file(nCtx, fileName,
2798  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2799  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2800  }
2801 
2805  public uint NumSMTLIBFormulas { get { return Native.Z3_get_smtlib_num_formulas(nCtx); } }
2806 
2810  public BoolExpr[] SMTLIBFormulas
2811  {
2812  get
2813  {
2814  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
2815 
2816  uint n = NumSMTLIBFormulas;
2817  BoolExpr[] res = new BoolExpr[n];
2818  for (uint i = 0; i < n; i++)
2819  res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_formula(nCtx, i));
2820  return res;
2821  }
2822  }
2823 
2827  public uint NumSMTLIBAssumptions { get { return Native.Z3_get_smtlib_num_assumptions(nCtx); } }
2828 
2832  public BoolExpr[] SMTLIBAssumptions
2833  {
2834  get
2835  {
2836  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
2837 
2838  uint n = NumSMTLIBAssumptions;
2839  BoolExpr[] res = new BoolExpr[n];
2840  for (uint i = 0; i < n; i++)
2841  res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_assumption(nCtx, i));
2842  return res;
2843  }
2844  }
2845 
2849  public uint NumSMTLIBDecls { get { return Native.Z3_get_smtlib_num_decls(nCtx); } }
2850 
2854  public FuncDecl[] SMTLIBDecls
2855  {
2856  get
2857  {
2858  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
2859 
2860  uint n = NumSMTLIBDecls;
2861  FuncDecl[] res = new FuncDecl[n];
2862  for (uint i = 0; i < n; i++)
2863  res[i] = new FuncDecl(this, Native.Z3_get_smtlib_decl(nCtx, i));
2864  return res;
2865  }
2866  }
2867 
2871  public uint NumSMTLIBSorts { get { return Native.Z3_get_smtlib_num_sorts(nCtx); } }
2872 
2876  public Sort[] SMTLIBSorts
2877  {
2878  get
2879  {
2880  Contract.Ensures(Contract.Result<Sort[]>() != null);
2881 
2882  uint n = NumSMTLIBSorts;
2883  Sort[] res = new Sort[n];
2884  for (uint i = 0; i < n; i++)
2885  res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i));
2886  return res;
2887  }
2888  }
2889 
2895  public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2896  {
2897  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2898 
2899  uint csn = Symbol.ArrayLength(sortNames);
2900  uint cs = Sort.ArrayLength(sorts);
2901  uint cdn = Symbol.ArrayLength(declNames);
2902  uint cd = AST.ArrayLength(decls);
2903  if (csn != cs || cdn != cd)
2904  throw new Z3Exception("Argument size mismatch");
2905  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
2906  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2907  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2908  }
2909 
2914  public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
2915  {
2916  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2917 
2918  uint csn = Symbol.ArrayLength(sortNames);
2919  uint cs = Sort.ArrayLength(sorts);
2920  uint cdn = Symbol.ArrayLength(declNames);
2921  uint cd = AST.ArrayLength(decls);
2922  if (csn != cs || cdn != cd)
2923  throw new Z3Exception("Argument size mismatch");
2924  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
2925  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2926  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2927  }
2928  #endregion
2929 
2930  #region Goals
2931  public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
2942  {
2943  Contract.Ensures(Contract.Result<Goal>() != null);
2944 
2945  return new Goal(this, models, unsatCores, proofs);
2946  }
2947  #endregion
2948 
2949  #region ParameterSets
2950  public Params MkParams()
2954  {
2955  Contract.Ensures(Contract.Result<Params>() != null);
2956 
2957  return new Params(this);
2958  }
2959  #endregion
2960 
2961  #region Tactics
2962  public uint NumTactics
2966  {
2967  get { return Native.Z3_get_num_tactics(nCtx); }
2968  }
2969 
2973  public string[] TacticNames
2974  {
2975  get
2976  {
2977  Contract.Ensures(Contract.Result<string[]>() != null);
2978 
2979  uint n = NumTactics;
2980  string[] res = new string[n];
2981  for (uint i = 0; i < n; i++)
2982  res[i] = Native.Z3_get_tactic_name(nCtx, i);
2983  return res;
2984  }
2985  }
2986 
2990  public string TacticDescription(string name)
2991  {
2992  Contract.Ensures(Contract.Result<string>() != null);
2993 
2994  return Native.Z3_tactic_get_descr(nCtx, name);
2995  }
2996 
3000  public Tactic MkTactic(string name)
3001  {
3002  Contract.Ensures(Contract.Result<Tactic>() != null);
3003 
3004  return new Tactic(this, name);
3005  }
3006 
3011  public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
3012  {
3013  Contract.Requires(t1 != null);
3014  Contract.Requires(t2 != null);
3015  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3016  Contract.Ensures(Contract.Result<Tactic>() != null);
3017 
3018 
3019  CheckContextMatch(t1);
3020  CheckContextMatch(t2);
3021  CheckContextMatch(ts);
3022 
3023  IntPtr last = IntPtr.Zero;
3024  if (ts != null && ts.Length > 0)
3025  {
3026  last = ts[ts.Length - 1].NativeObject;
3027  for (int i = ts.Length - 2; i >= 0; i--)
3028  last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3029  }
3030  if (last != IntPtr.Zero)
3031  {
3032  last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3033  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3034  }
3035  else
3036  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3037  }
3038 
3046  public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
3047  {
3048  Contract.Requires(t1 != null);
3049  Contract.Requires(t2 != null);
3050  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3051  Contract.Ensures(Contract.Result<Tactic>() != null);
3052 
3053  return AndThen(t1, t2, ts);
3054  }
3055 
3060  public Tactic OrElse(Tactic t1, Tactic t2)
3061  {
3062  Contract.Requires(t1 != null);
3063  Contract.Requires(t2 != null);
3064  Contract.Ensures(Contract.Result<Tactic>() != null);
3065 
3066  CheckContextMatch(t1);
3067  CheckContextMatch(t2);
3068  return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3069  }
3070 
3077  public Tactic TryFor(Tactic t, uint ms)
3078  {
3079  Contract.Requires(t != null);
3080  Contract.Ensures(Contract.Result<Tactic>() != null);
3081 
3082  CheckContextMatch(t);
3083  return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3084  }
3085 
3093  public Tactic When(Probe p, Tactic t)
3094  {
3095  Contract.Requires(p != null);
3096  Contract.Requires(t != null);
3097  Contract.Ensures(Contract.Result<Tactic>() != null);
3098 
3099  CheckContextMatch(t);
3100  CheckContextMatch(p);
3101  return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3102  }
3103 
3108  public Tactic Cond(Probe p, Tactic t1, Tactic t2)
3109  {
3110  Contract.Requires(p != null);
3111  Contract.Requires(t1 != null);
3112  Contract.Requires(t2 != null);
3113  Contract.Ensures(Contract.Result<Tactic>() != null);
3114 
3115  CheckContextMatch(p);
3116  CheckContextMatch(t1);
3117  CheckContextMatch(t2);
3118  return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3119  }
3120 
3125  public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
3126  {
3127  Contract.Requires(t != null);
3128  Contract.Ensures(Contract.Result<Tactic>() != null);
3129 
3130  CheckContextMatch(t);
3131  return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3132  }
3133 
3137  public Tactic Skip()
3138  {
3139  Contract.Ensures(Contract.Result<Tactic>() != null);
3140 
3141  return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3142  }
3143 
3147  public Tactic Fail()
3148  {
3149  Contract.Ensures(Contract.Result<Tactic>() != null);
3150 
3151  return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3152  }
3153 
3157  public Tactic FailIf(Probe p)
3158  {
3159  Contract.Requires(p != null);
3160  Contract.Ensures(Contract.Result<Tactic>() != null);
3161 
3162  CheckContextMatch(p);
3163  return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3164  }
3165 
3171  {
3172  Contract.Ensures(Contract.Result<Tactic>() != null);
3173 
3174  return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3175  }
3176 
3181  {
3182  Contract.Requires(t != null);
3183  Contract.Requires(p != null);
3184  Contract.Ensures(Contract.Result<Tactic>() != null);
3185 
3186  CheckContextMatch(t);
3187  CheckContextMatch(p);
3188  return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3189  }
3190 
3195  public Tactic With(Tactic t, Params p)
3196  {
3197  Contract.Requires(t != null);
3198  Contract.Requires(p != null);
3199  Contract.Ensures(Contract.Result<Tactic>() != null);
3200 
3201  return UsingParams(t, p);
3202  }
3203 
3207  public Tactic ParOr(params Tactic[] t)
3208  {
3209  Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3210  Contract.Ensures(Contract.Result<Tactic>() != null);
3211 
3212  CheckContextMatch(t);
3213  return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
3214  }
3215 
3221  {
3222  Contract.Requires(t1 != null);
3223  Contract.Requires(t2 != null);
3224  Contract.Ensures(Contract.Result<Tactic>() != null);
3225 
3226  CheckContextMatch(t1);
3227  CheckContextMatch(t2);
3228  return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3229  }
3230 
3235  public void Interrupt()
3236  {
3237  Native.Z3_interrupt(nCtx);
3238  }
3239  #endregion
3240 
3241  #region Probes
3242  public uint NumProbes
3246  {
3247  get { return Native.Z3_get_num_probes(nCtx); }
3248  }
3249 
3253  public string[] ProbeNames
3254  {
3255  get
3256  {
3257  Contract.Ensures(Contract.Result<string[]>() != null);
3258 
3259  uint n = NumProbes;
3260  string[] res = new string[n];
3261  for (uint i = 0; i < n; i++)
3262  res[i] = Native.Z3_get_probe_name(nCtx, i);
3263  return res;
3264  }
3265  }
3266 
3270  public string ProbeDescription(string name)
3271  {
3272  Contract.Ensures(Contract.Result<string>() != null);
3273 
3274  return Native.Z3_probe_get_descr(nCtx, name);
3275  }
3276 
3280  public Probe MkProbe(string name)
3281  {
3282  Contract.Ensures(Contract.Result<Probe>() != null);
3283 
3284  return new Probe(this, name);
3285  }
3286 
3290  public Probe ConstProbe(double val)
3291  {
3292  Contract.Ensures(Contract.Result<Probe>() != null);
3293 
3294  return new Probe(this, Native.Z3_probe_const(nCtx, val));
3295  }
3296 
3301  public Probe Lt(Probe p1, Probe p2)
3302  {
3303  Contract.Requires(p1 != null);
3304  Contract.Requires(p2 != null);
3305  Contract.Ensures(Contract.Result<Probe>() != null);
3306 
3307  CheckContextMatch(p1);
3308  CheckContextMatch(p2);
3309  return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3310  }
3311 
3316  public Probe Gt(Probe p1, Probe p2)
3317  {
3318  Contract.Requires(p1 != null);
3319  Contract.Requires(p2 != null);
3320  Contract.Ensures(Contract.Result<Probe>() != null);
3321 
3322  CheckContextMatch(p1);
3323  CheckContextMatch(p2);
3324  return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3325  }
3326 
3331  public Probe Le(Probe p1, Probe p2)
3332  {
3333  Contract.Requires(p1 != null);
3334  Contract.Requires(p2 != null);
3335  Contract.Ensures(Contract.Result<Probe>() != null);
3336 
3337  CheckContextMatch(p1);
3338  CheckContextMatch(p2);
3339  return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3340  }
3341 
3346  public Probe Ge(Probe p1, Probe p2)
3347  {
3348  Contract.Requires(p1 != null);
3349  Contract.Requires(p2 != null);
3350  Contract.Ensures(Contract.Result<Probe>() != null);
3351 
3352  CheckContextMatch(p1);
3353  CheckContextMatch(p2);
3354  return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3355  }
3356 
3361  public Probe Eq(Probe p1, Probe p2)
3362  {
3363  Contract.Requires(p1 != null);
3364  Contract.Requires(p2 != null);
3365  Contract.Ensures(Contract.Result<Probe>() != null);
3366 
3367  CheckContextMatch(p1);
3368  CheckContextMatch(p2);
3369  return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3370  }
3371 
3376  public Probe And(Probe p1, Probe p2)
3377  {
3378  Contract.Requires(p1 != null);
3379  Contract.Requires(p2 != null);
3380  Contract.Ensures(Contract.Result<Probe>() != null);
3381 
3382  CheckContextMatch(p1);
3383  CheckContextMatch(p2);
3384  return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3385  }
3386 
3391  public Probe Or(Probe p1, Probe p2)
3392  {
3393  Contract.Requires(p1 != null);
3394  Contract.Requires(p2 != null);
3395  Contract.Ensures(Contract.Result<Probe>() != null);
3396 
3397  CheckContextMatch(p1);
3398  CheckContextMatch(p2);
3399  return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3400  }
3401 
3406  public Probe Not(Probe p)
3407  {
3408  Contract.Requires(p != null);
3409  Contract.Ensures(Contract.Result<Probe>() != null);
3410 
3411  CheckContextMatch(p);
3412  return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3413  }
3414  #endregion
3415 
3416  #region Solvers
3417  public Solver MkSolver(Symbol logic = null)
3426  {
3427  Contract.Ensures(Contract.Result<Solver>() != null);
3428 
3429  if (logic == null)
3430  return new Solver(this, Native.Z3_mk_solver(nCtx));
3431  else
3432  return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3433  }
3434 
3439  public Solver MkSolver(string logic)
3440  {
3441  Contract.Ensures(Contract.Result<Solver>() != null);
3442 
3443  return MkSolver(MkSymbol(logic));
3444  }
3445 
3450  {
3451  Contract.Ensures(Contract.Result<Solver>() != null);
3452 
3453  return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3454  }
3455 
3464  {
3465  Contract.Requires(t != null);
3466  Contract.Ensures(Contract.Result<Solver>() != null);
3467 
3468  return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3469  }
3470  #endregion
3471 
3472  #region Fixedpoints
3473  public Fixedpoint MkFixedpoint()
3477  {
3478  Contract.Ensures(Contract.Result<Fixedpoint>() != null);
3479 
3480  return new Fixedpoint(this);
3481  }
3482  #endregion
3483 
3484  #region Optimization
3485  public Optimize MkOptimize()
3489  {
3490  Contract.Ensures(Contract.Result<Optimize>() != null);
3491 
3492  return new Optimize(this);
3493  }
3494  #endregion
3495 
3496  #region Floating-Point Arithmetic
3497 
3498  #region Rounding Modes
3499  #region RoundingMode Sort
3500  public FPRMSort MkFPRoundingModeSort()
3504  {
3505  Contract.Ensures(Contract.Result<FPRMSort>() != null);
3506  return new FPRMSort(this);
3507  }
3508  #endregion
3509 
3510  #region Numerals
3511  public FPRMExpr MkFPRoundNearestTiesToEven()
3515  {
3516  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3517  return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
3518  }
3519 
3523  public FPRMNum MkFPRNE()
3524  {
3525  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3526  return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
3527  }
3528 
3533  {
3534  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3535  return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
3536  }
3537 
3541  public FPRMNum MkFPRNA()
3542  {
3543  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3544  return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
3545  }
3546 
3551  {
3552  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3553  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
3554  }
3555 
3559  public FPRMNum MkFPRTP()
3560  {
3561  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3562  return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
3563  }
3564 
3569  {
3570  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3571  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
3572  }
3573 
3577  public FPRMNum MkFPRTN()
3578  {
3579  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3580  return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
3581  }
3582 
3587  {
3588  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3589  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
3590  }
3591 
3595  public FPRMNum MkFPRTZ()
3596  {
3597  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3598  return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
3599  }
3600  #endregion
3601  #endregion
3602 
3603  #region FloatingPoint Sorts
3604  public FPSort MkFPSort(uint ebits, uint sbits)
3610  {
3611  Contract.Ensures(Contract.Result<FPSort>() != null);
3612  return new FPSort(this, ebits, sbits);
3613  }
3614 
3619  {
3620  Contract.Ensures(Contract.Result<FPSort>() != null);
3621  return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
3622  }
3623 
3628  {
3629  Contract.Ensures(Contract.Result<FPSort>() != null);
3630  return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
3631  }
3632 
3637  {
3638  Contract.Ensures(Contract.Result<FPSort>() != null);
3639  return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
3640  }
3641 
3646  {
3647  Contract.Ensures(Contract.Result<FPSort>() != null);
3648  return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx));
3649  }
3650 
3655  {
3656  Contract.Ensures(Contract.Result<FPSort>() != null);
3657  return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
3658  }
3659 
3664  {
3665  Contract.Ensures(Contract.Result<FPSort>() != null);
3666  return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
3667  }
3668 
3673  {
3674  Contract.Ensures(Contract.Result<FPSort>() != null);
3675  return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
3676  }
3677 
3682  {
3683  Contract.Ensures(Contract.Result<FPSort>() != null);
3684  return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
3685  }
3686  #endregion
3687 
3688  #region Numerals
3689  public FPNum MkFPNaN(FPSort s)
3694  {
3695  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3696  return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
3697  }
3698 
3704  public FPNum MkFPInf(FPSort s, bool negative)
3705  {
3706  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3707  return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0));
3708  }
3709 
3715  public FPNum MkFPZero(FPSort s, bool negative)
3716  {
3717  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3718  return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
3719  }
3720 
3726  public FPNum MkFPNumeral(float v, FPSort s)
3727  {
3728  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3729  return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
3730  }
3731 
3737  public FPNum MkFPNumeral(double v, FPSort s)
3738  {
3739  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3740  return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
3741  }
3742 
3748  public FPNum MkFPNumeral(int v, FPSort s)
3749  {
3750  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3751  return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
3752  }
3753 
3761  public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
3762  {
3763  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3764  return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
3765  }
3766 
3774  public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
3775  {
3776  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3777  return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
3778  }
3779 
3785  public FPNum MkFP(float v, FPSort s)
3786  {
3787  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3788  return MkFPNumeral(v, s);
3789  }
3790 
3796  public FPNum MkFP(double v, FPSort s)
3797  {
3798  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3799  return MkFPNumeral(v, s);
3800  }
3801 
3807  public FPNum MkFP(int v, FPSort s)
3808  {
3809  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3810  return MkFPNumeral(v, s);
3811  }
3812 
3820  public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
3821  {
3822  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3823  return MkFPNumeral(sgn, exp, sig, s);
3824  }
3825 
3833  public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
3834  {
3835  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3836  return MkFPNumeral(sgn, exp, sig, s);
3837  }
3838 
3839  #endregion
3840 
3841  #region Operators
3842  public FPExpr MkFPAbs(FPExpr t)
3847  {
3848  Contract.Ensures(Contract.Result<FPNum>() != null);
3849  return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
3850  }
3851 
3856  public FPExpr MkFPNeg(FPExpr t)
3857  {
3858  Contract.Ensures(Contract.Result<FPNum>() != null);
3859  return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
3860  }
3861 
3868  public FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
3869  {
3870  Contract.Ensures(Contract.Result<FPNum>() != null);
3871  return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3872  }
3873 
3880  public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
3881  {
3882  Contract.Ensures(Contract.Result<FPNum>() != null);
3883  return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3884  }
3885 
3892  public FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
3893  {
3894  Contract.Ensures(Contract.Result<FPNum>() != null);
3895  return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3896  }
3897 
3904  public FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
3905  {
3906  Contract.Ensures(Contract.Result<FPNum>() != null);
3907  return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3908  }
3909 
3920  public FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
3921  {
3922  Contract.Ensures(Contract.Result<FPNum>() != null);
3923  return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
3924  }
3925 
3932  {
3933  Contract.Ensures(Contract.Result<FPNum>() != null);
3934  return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
3935  }
3936 
3942  public FPExpr MkFPRem(FPExpr t1, FPExpr t2)
3943  {
3944  Contract.Ensures(Contract.Result<FPNum>() != null);
3945  return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
3946  }
3947 
3955  {
3956  Contract.Ensures(Contract.Result<FPNum>() != null);
3957  return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
3958  }
3959 
3965  public FPExpr MkFPMin(FPExpr t1, FPExpr t2)
3966  {
3967  Contract.Ensures(Contract.Result<FPNum>() != null);
3968  return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
3969  }
3970 
3976  public FPExpr MkFPMax(FPExpr t1, FPExpr t2)
3977  {
3978  Contract.Ensures(Contract.Result<FPNum>() != null);
3979  return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
3980  }
3981 
3987  public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
3988  {
3989  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3990  return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
3991  }
3992 
3998  public BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
3999  {
4000  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4001  return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
4002  }
4003 
4009  public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
4010  {
4011  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4012  return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
4013  }
4014 
4020  public BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
4021  {
4022  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4023  return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
4024  }
4025 
4034  public BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
4035  {
4036  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4037  return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
4038  }
4039 
4045  {
4046  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4047  return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
4048  }
4049 
4055  {
4056  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4057  return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
4058  }
4059 
4065  {
4066  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4067  return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
4068  }
4069 
4075  {
4076  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4077  return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
4078  }
4079 
4085  {
4086  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4087  return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
4088  }
4089 
4095  {
4096  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4097  return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
4098  }
4099 
4105  {
4106  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4107  return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
4108  }
4109  #endregion
4110 
4111  #region Conversions to FloatingPoint terms
4112  public FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
4126  {
4127  Contract.Ensures(Contract.Result<FPExpr>() != null);
4128  return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
4129  }
4130 
4143  {
4144  Contract.Ensures(Contract.Result<FPExpr>() != null);
4145  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
4146  }
4147 
4160  {
4161  Contract.Ensures(Contract.Result<FPExpr>() != null);
4162  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4163  }
4164 
4177  {
4178  Contract.Ensures(Contract.Result<FPExpr>() != null);
4179  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4180  }
4181 
4195  public FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
4196  {
4197  Contract.Ensures(Contract.Result<FPExpr>() != null);
4198  if (signed)
4199  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4200  else
4201  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4202  }
4203 
4215  {
4216  Contract.Ensures(Contract.Result<FPExpr>() != null);
4217  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
4218  }
4219  #endregion
4220 
4221  #region Conversions from FloatingPoint terms
4222  public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed)
4235  {
4236  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4237  if (signed)
4238  return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4239  else
4240  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4241  }
4242 
4253  {
4254  Contract.Ensures(Contract.Result<RealExpr>() != null);
4255  return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
4256  }
4257  #endregion
4258 
4259  #region Z3-specific extensions
4260  public BitVecExpr MkFPToIEEEBV(FPExpr t)
4271  {
4272  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4273  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
4274  }
4275 
4289  {
4290  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4291  return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
4292  }
4293  #endregion
4294  #endregion // Floating-point Arithmetic
4295 
4296  #region Miscellaneous
4297  public AST WrapAST(IntPtr nativeObject)
4308  {
4309  Contract.Ensures(Contract.Result<AST>() != null);
4310  return AST.Create(this, nativeObject);
4311  }
4312 
4324  public IntPtr UnwrapAST(AST a)
4325  {
4326  return a.NativeObject;
4327  }
4328 
4332  public string SimplifyHelp()
4333  {
4334  Contract.Ensures(Contract.Result<string>() != null);
4335 
4336  return Native.Z3_simplify_get_help(nCtx);
4337  }
4338 
4342  public ParamDescrs SimplifyParameterDescriptions
4343  {
4344  get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
4345  }
4346  #endregion
4347 
4348  #region Error Handling
4349  //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
4357 
4361  //public event ErrorHandler OnError = null;
4362  #endregion
4363 
4364  #region Parameters
4365  public void UpdateParamValue(string id, string value)
4375  {
4376  Native.Z3_update_param_value(nCtx, id, value);
4377  }
4378 
4379  #endregion
4380 
4381  #region Internal
4382  internal IntPtr m_ctx = IntPtr.Zero;
4383  internal Native.Z3_error_handler m_n_err_handler = null;
4384  internal IntPtr nCtx { get { return m_ctx; } }
4385 
4386  internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
4387  {
4388  // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
4389  }
4390 
4391  internal void InitContext()
4392  {
4393  PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
4394  m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
4395  Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
4396  GC.SuppressFinalize(this);
4397  }
4398 
4399  [Pure]
4400  internal void CheckContextMatch(Z3Object other)
4401  {
4402  Contract.Requires(other != null);
4403 
4404  if (!ReferenceEquals(this, other.Context))
4405  throw new Z3Exception("Context mismatch");
4406  }
4407 
4408  [Pure]
4409  internal void CheckContextMatch(Z3Object[] arr)
4410  {
4411  Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
4412 
4413  if (arr != null)
4414  {
4415  foreach (Z3Object a in arr)
4416  {
4417  Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
4418  CheckContextMatch(a);
4419  }
4420  }
4421  }
4422 
4423  [ContractInvariantMethod]
4424  private void ObjectInvariant()
4425  {
4426  Contract.Invariant(m_AST_DRQ != null);
4427  Contract.Invariant(m_ASTMap_DRQ != null);
4428  Contract.Invariant(m_ASTVector_DRQ != null);
4429  Contract.Invariant(m_ApplyResult_DRQ != null);
4430  Contract.Invariant(m_FuncEntry_DRQ != null);
4431  Contract.Invariant(m_FuncInterp_DRQ != null);
4432  Contract.Invariant(m_Goal_DRQ != null);
4433  Contract.Invariant(m_Model_DRQ != null);
4434  Contract.Invariant(m_Params_DRQ != null);
4435  Contract.Invariant(m_ParamDescrs_DRQ != null);
4436  Contract.Invariant(m_Probe_DRQ != null);
4437  Contract.Invariant(m_Solver_DRQ != null);
4438  Contract.Invariant(m_Statistics_DRQ != null);
4439  Contract.Invariant(m_Tactic_DRQ != null);
4440  Contract.Invariant(m_Fixedpoint_DRQ != null);
4441  Contract.Invariant(m_Optimize_DRQ != null);
4442  }
4443 
4444  readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
4445  readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue(10);
4446  readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue(10);
4447  readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue(10);
4448  readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue(10);
4449  readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue(10);
4450  readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue(10);
4451  readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue(10);
4452  readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue(10);
4453  readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue(10);
4454  readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue(10);
4455  readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue(10);
4456  readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10);
4457  readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
4458  readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
4459  readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10);
4460 
4464  public IDecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result<AST.DecRefQueue>() != null); return m_AST_DRQ; } }
4465 
4469  public IDecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null); return m_ASTMap_DRQ; } }
4470 
4474  public IDecRefQueue ASTVector_DRQ { get { Contract.Ensures(Contract.Result<ASTVector.DecRefQueue>() != null); return m_ASTVector_DRQ; } }
4475 
4479  public IDecRefQueue ApplyResult_DRQ { get { Contract.Ensures(Contract.Result<ApplyResult.DecRefQueue>() != null); return m_ApplyResult_DRQ; } }
4480 
4484  public IDecRefQueue FuncEntry_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.Entry.DecRefQueue>() != null); return m_FuncEntry_DRQ; } }
4485 
4489  public IDecRefQueue FuncInterp_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.DecRefQueue>() != null); return m_FuncInterp_DRQ; } }
4490 
4494  public IDecRefQueue Goal_DRQ { get { Contract.Ensures(Contract.Result<Goal.DecRefQueue>() != null); return m_Goal_DRQ; } }
4495 
4499  public IDecRefQueue Model_DRQ { get { Contract.Ensures(Contract.Result<Model.DecRefQueue>() != null); return m_Model_DRQ; } }
4500 
4504  public IDecRefQueue Params_DRQ { get { Contract.Ensures(Contract.Result<Params.DecRefQueue>() != null); return m_Params_DRQ; } }
4505 
4509  public IDecRefQueue ParamDescrs_DRQ { get { Contract.Ensures(Contract.Result<ParamDescrs.DecRefQueue>() != null); return m_ParamDescrs_DRQ; } }
4510 
4514  public IDecRefQueue Probe_DRQ { get { Contract.Ensures(Contract.Result<Probe.DecRefQueue>() != null); return m_Probe_DRQ; } }
4515 
4519  public IDecRefQueue Solver_DRQ { get { Contract.Ensures(Contract.Result<Solver.DecRefQueue>() != null); return m_Solver_DRQ; } }
4520 
4524  public IDecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result<Statistics.DecRefQueue>() != null); return m_Statistics_DRQ; } }
4525 
4529  public IDecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result<Tactic.DecRefQueue>() != null); return m_Tactic_DRQ; } }
4530 
4534  public IDecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
4535 
4539  public IDecRefQueue Optimize_DRQ { get { Contract.Ensures(Contract.Result<Optimize.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
4540 
4541 
4542  internal long refCount = 0;
4543 
4547  ~Context()
4548  {
4549  // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4550  Dispose();
4551 
4552  if (refCount == 0)
4553  {
4554  m_n_err_handler = null;
4555  Native.Z3_del_context(m_ctx);
4556  m_ctx = IntPtr.Zero;
4557  }
4558  else
4559  GC.ReRegisterForFinalize(this);
4560  }
4561 
4565  public void Dispose()
4566  {
4567  // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4568  AST_DRQ.Clear(this);
4569  ASTMap_DRQ.Clear(this);
4570  ASTVector_DRQ.Clear(this);
4571  ApplyResult_DRQ.Clear(this);
4572  FuncEntry_DRQ.Clear(this);
4573  FuncInterp_DRQ.Clear(this);
4574  Goal_DRQ.Clear(this);
4575  Model_DRQ.Clear(this);
4576  Params_DRQ.Clear(this);
4577  ParamDescrs_DRQ.Clear(this);
4578  Probe_DRQ.Clear(this);
4579  Solver_DRQ.Clear(this);
4580  Statistics_DRQ.Clear(this);
4581  Tactic_DRQ.Clear(this);
4582  Fixedpoint_DRQ.Clear(this);
4583  Optimize_DRQ.Clear(this);
4584 
4585  m_boolSort = null;
4586  m_intSort = null;
4587  m_realSort = null;
4588  }
4589  #endregion
4590  }
4591 }
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:910
static Z3_ast Z3_mk_bvmul(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2630
static Z3_solver Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1)
Definition: Native.cs:5333
static Z3_sort Z3_mk_fpa_sort_64(Z3_context a0)
Definition: Native.cs:6418
BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement signed remainder (sign follows divisor).
Definition: Context.cs:1429
string SimplifyHelp()
Return a string describing all available parameters to Expr.Simplify.
Definition: Context.cs:4332
static Z3_ast Z3_mk_bvadd_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Definition: Native.cs:2854
static string Z3_get_tactic_name(Z3_context a0, uint a1)
Definition: Native.cs:5183
static Z3_ast Z3_mk_fpa_abs(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6514
BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
Floating-point less than or equal.
Definition: Context.cs:3987
Object for managing optimizization context
Definition: Optimize.cs:30
static Z3_tactic Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Definition: Native.cs:5007
FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Definition: Context.cs:4159
FPExpr MkFPRem(FPExpr t1, FPExpr t2)
Floating-point remainder
Definition: Context.cs:3942
static Z3_ast Z3_mk_fpa_round_to_integral(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6586
static Z3_ast Z3_get_smtlib_formula(Z3_context a0, uint a1)
Definition: Native.cs:4222
static Z3_ast Z3_mk_pble(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] int[] a3, int a4)
Definition: Native.cs:3358
static Z3_ast Z3_mk_bvneg_no_overflow(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2894
BoolExpr MkIsInteger(RealExpr t)
Creates an expression that checks whether a real number is an integer.
Definition: Context.cs:1140
static Z3_tactic Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Definition: Native.cs:5023
FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
Conversion of a 2&#39;s complement signed bit-vector term into a term of FloatingPoint sort...
Definition: Context.cs:4195
FPRMNum MkFPRNE()
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode...
Definition: Context.cs:3523
FloatiungPoint Numerals
Definition: FPNum.cs:28
static Z3_ast Z3_mk_fpa_to_real(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6762
static Z3_ast Z3_mk_real2int(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2518
FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point division
Definition: Context.cs:3904
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
Bitwise conjunction.
Definition: Context.cs:1194
static Z3_ast Z3_mk_fpa_to_ubv(Z3_context a0, Z3_ast a1, Z3_ast a2, uint a3)
Definition: Native.cs:6746
static Z3_ast Z3_mk_set_intersect(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:3006
static Z3_ast Z3_mk_bvuge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2710
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:2338
static Z3_ast Z3_mk_mul(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2422
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:3000
static Z3_ast Z3_mk_mod(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2454
BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
Create a pseudo-Boolean less-or-equal constraint.
Definition: Context.cs:2284
using System
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:4252
FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
Definition: Context.cs:4176
FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
Create a new finite domain sort.
Definition: Context.cs:310
static Z3_ast Z3_mk_empty_set(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2966
static Z3_ast Z3_mk_fpa_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6642
FPRMNum MkFPRTN()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode...
Definition: Context.cs:3577
ArrayExpr MkConstArray(Sort domain, Expr v)
Create a constant array.
Definition: Context.cs:2071
string ProbeDescription(string name)
Returns a string containing a description of the probe with the given name.
Definition: Context.cs:3270
static Z3_ast Z3_mk_fpa_to_fp_float(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
Definition: Native.cs:6714
FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Floating-point fused multiply-add
Definition: Context.cs:3920
BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
Unsigned greater than or equal to.
Definition: Context.cs:1514
static Z3_ast Z3_mk_fpa_round_nearest_ties_to_even(Z3_context a0)
Definition: Native.cs:6290
static Z3_ast Z3_mk_fpa_to_fp_signed(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
Definition: Native.cs:6730
def RealSort(ctx=None)
Definition: z3py.py:2655
Bit-vector sorts.
Definition: BitVecSort.cs:28
RatNum MkReal(string v)
Create a real numeral.
Definition: Context.cs:2404
Expr MkFreshConst(string prefix, Sort range)
Creates a fresh Constant of sort range and a name prefixed with prefix .
Definition: Context.cs:653
static Z3_tactic Z3_tactic_par_or(Z3_context a0, uint a1, [In] Z3_tactic[] a2)
Definition: Native.cs:5015
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:3820
static Z3_ast Z3_mk_bvashr(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2798
def AndThen(ts, ks)
Definition: z3py.py:6759
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:4200
static Z3_ast Z3_mk_bv2int(Z3_context a0, Z3_ast a1, int a2)
Definition: Native.cs:2846
static string Z3_tactic_get_descr(Z3_context a0, string a1)
Definition: Native.cs:5223
BitVecNum MkBV(long v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2563
FPExpr MkFPMax(FPExpr t1, FPExpr t2)
Maximum of floating-point numbers.
Definition: Context.cs:3976
BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
Check for set membership.
Definition: Context.cs:2241
static Z3_ast Z3_mk_atmost(Z3_context a0, uint a1, [In] Z3_ast[] a2, uint a3)
Definition: Native.cs:3350
static Z3_ast Z3_mk_fpa_is_normal(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6650
Probe Not(Probe p)
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
Definition: Context.cs:3406
static Z3_ast Z3_mk_fpa_numeral_int_uint(Z3_context a0, int a1, int a2, uint a3, Z3_sort a4)
Definition: Native.cs:6498
Bit-vector numerals
Definition: BitVecNum.cs:32
Array sorts.
Definition: ArraySort.cs:29
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Unsigned division.
Definition: Context.cs:1347
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:3093
Z3_error_code
Z3_error_code
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:3125
BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement signed greater than or equal to.
Definition: Context.cs:1531
static Z3_ast Z3_mk_fpa_max(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6602
static Z3_probe Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:5159
BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
Bit-vector extraction.
Definition: Context.cs:1606
static Z3_ast Z3_mk_fresh_const(Z3_context a0, string a1, Z3_sort a2)
Definition: Native.cs:2318
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:3346
IntExpr MkIntConst(Symbol name)
Creates an integer constant.
Definition: Context.cs:698
static uint Z3_get_num_probes(Z3_context a0)
Definition: Native.cs:5191
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:2895
static Z3_ast Z3_mk_bvmul_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2910
static Z3_ast Z3_mk_fpa_geq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6626
static Z3_ast Z3_mk_bvshl(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2782
IntNum MkInt(int v)
Create an integer numeral.
Definition: Context.cs:2477
Tactic ParOr(params Tactic[] t)
Create a tactic that applies the given tactics in parallel.
Definition: Context.cs:3207
BitVecExpr MkBVNeg(BitVecExpr t)
Standard two&#39;s complement unary minus.
Definition: Context.cs:1284
static Z3_sort Z3_mk_fpa_sort_128(Z3_context a0)
Definition: Native.cs:6434
static Z3_probe Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:5127
ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
Maps f on the argument arrays.
Definition: Context.cs:2093
Boolean expressions
Definition: BoolExpr.cs:31
static Z3_ast Z3_mk_real(Z3_context a0, int a1, int a2)
Definition: Native.cs:3054
static Z3_ast Z3_mk_fpa_numeral_float(Z3_context a0, float a1, Z3_sort a2)
Definition: Native.cs:6474
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3726
void Interrupt()
Interrupt the execution of a Z3 procedure.
Definition: Context.cs:3235
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:3331
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:3595
static Z3_ast Z3_mk_true(Z3_context a0)
Definition: Native.cs:2326
static Z3_tactic Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3)
Definition: Native.cs:5047
FPNum MkFPInf(FPSort s, bool negative)
Create a floating-point infinity of sort s.
Definition: Context.cs:3704
Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
Create an expression representing an if-then-else: ite(t1, t2, t3).
Definition: Context.cs:852
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:2641
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:2370
static Z3_ast Z3_mk_or(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2406
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:641
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
Definition: Context.cs:991
FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:519
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:6834
BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
Unsigned greater-than.
Definition: Context.cs:1548
FPSort MkFPSortSingle()
Create the single-precision (32-bit) FloatingPoint sort.
Definition: Context.cs:3636
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:5143
BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
Unsigned less-than or equal to.
Definition: Context.cs:1480
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
Definition: Context.cs:1049
static Z3_ast Z3_mk_fpa_is_negative(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6690
static Z3_ast Z3_mk_fpa_round_nearest_ties_to_away(Z3_context a0)
Definition: Native.cs:6306
static Z3_ast Z3_mk_bvredand(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2542
BoolExpr MkBoolConst(Symbol name)
Create a Boolean constant.
Definition: Context.cs:677
IntNum MkInt(uint v)
Create an integer numeral.
Definition: Context.cs:2489
static Z3_ast Z3_mk_fpa_fp(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:6466
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:3011
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:2772
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:2659
BoolExpr MkEq(Expr x, Expr y)
Creates the equality x = y .
Definition: Context.cs:809
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:3376
static Z3_ast Z3_mk_fpa_leq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6610
static Z3_tactic Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, uint a2)
Definition: Native.cs:5031
static Z3_tactic Z3_tactic_fail(Z3_context a0)
Definition: Native.cs:5071
static Z3_ast Z3_mk_fpa_round_toward_negative(Z3_context a0)
Definition: Native.cs:6338
static Z3_ast Z3_mk_implies(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2382
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:4084
static Z3_solver Z3_mk_solver(Z3_context a0)
Definition: Native.cs:5309
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
Definition: Context.cs:1063
ArrayExpr MkFullSet(Sort domain)
Create the full set.
Definition: Context.cs:2149
static Z3_ast Z3_mk_fpa_numeral_int64_uint64(Z3_context a0, int a1, Int64 a2, UInt64 a3, Z3_sort a4)
Definition: Native.cs:6506
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:3862
static Z3_ast Z3_mk_set_add(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2982
Tactics are the basic building block for creating custom solvers for specific problem domains...
Definition: Tactic.cs:32
static Z3_ast Z3_mk_zero_ext(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2766
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:3761
static Z3_ast Z3_mk_le(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2486
static Z3_probe Z3_probe_const(Z3_context a0, double a1)
Definition: Native.cs:5103
static Z3_ast Z3_mk_set_subset(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:3038
FPRMNum MkFPRoundTowardZero()
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode...
Definition: Context.cs:3586
FPSort MkFPSort16()
Create the half-precision (16-bit) FloatingPoint sort.
Definition: Context.cs:3627
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:6562
FPNum MkFP(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition: Context.cs:3807
FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
Creates a fresh function declaration with a name prefixed with prefix .
Definition: Context.cs:536
BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise subtraction does not overflow.
Definition: Context.cs:1887
BoolExpr MkBoolConst(string name)
Create a Boolean constant.
Definition: Context.cs:688
BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise signed division does not overflow.
Definition: Context.cs:1921
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:578
FuncDecl MkConstDecl(Symbol name, Sort range)
Creates a new constant function declaration.
Definition: Context.cs:550
static Z3_ast Z3_mk_bvudiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2638
Solver MkSolver(string logic)
Creates a new (incremental) solver.
Definition: Context.cs:3439
ArrayExpr MkSetComplement(ArrayExpr arg)
Take the complement of a set.
Definition: Context.cs:2229
BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Rotate Right.
Definition: Context.cs:1793
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:3301
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:6450
static Z3_ast Z3_mk_fpa_is_infinite(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6674
static Z3_ast Z3_mk_fpa_to_sbv(Z3_context a0, Z3_ast a1, Z3_ast a2, uint a3)
Definition: Native.cs:6754
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:2354
static Z3_ast Z3_mk_is_int(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2526
BoolExpr MkAtMost(BoolExpr[] args, uint k)
Create an at-most-k constraint.
Definition: Context.cs:2272
RatNum MkReal(int v)
Create a real numeral.
Definition: Context.cs:2416
static Z3_ast Z3_mk_not(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2358
FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:488
Vectors of ASTs.
Definition: ASTVector.cs:28
static Z3_ast Z3_mk_bvredor(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2550
FPExpr MkFPNeg(FPExpr t)
Floating-point negation
Definition: Context.cs:3856
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:2020
BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XNOR.
Definition: Context.cs:1269
BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Rotate Left.
Definition: Context.cs:1775
BitVecExpr MkBVRedAND(BitVecExpr t)
Take conjunction of bits in a vector, return vector of length 1.
Definition: Context.cs:1168
static Z3_ast Z3_mk_bvand(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2558
BoolExpr MkFPIsInfinite(FPExpr t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.
Definition: Context.cs:4074
BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement signed less-than
Definition: Context.cs:1463
FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Definition: Context.cs:4142
static Z3_ast Z3_mk_sub(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2430
Expressions are terms.
Definition: Expr.cs:29
static Z3_func_decl Z3_get_smtlib_decl(Z3_context a0, uint a1)
Definition: Native.cs:4254
RealExpr MkRealConst(string name)
Creates a real constant.
Definition: Context.cs:731
static Z3_sort Z3_mk_bv_sort(Z3_context a0, uint a1)
Definition: Native.cs:2186
RealSort MkRealSort()
Create a real sort.
Definition: Context.cs:204
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:3774
static string Z3_probe_get_descr(Z3_context a0, string a1)
Definition: Native.cs:5231
BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
Bitwise NOR.
Definition: Context.cs:1254
static void Z3_set_ast_print_mode(Z3_context a0, uint a1)
Definition: Native.cs:4129
string TacticDescription(string name)
Returns a string containing a description of the tactic with the given name.
Definition: Context.cs:2990
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6389
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:2322
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3180
FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Conversion of a floating-point number to another FloatingPoint sort s.
Definition: Context.cs:4214
static string Z3_get_probe_name(Z3_context a0, uint a1)
Definition: Native.cs:5199
static Z3_ast Z3_datatype_update_field(Z3_context a0, Z3_func_decl a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:3326
static Z3_ast Z3_mk_sign_ext(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2758
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
Definition: Context.cs:966
FuncDecl MkConstDecl(string name, Sort range)
Creates a new constant function declaration.
Definition: Context.cs:564
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:3220
BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement addition.
Definition: Context.cs:1297
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:1371
ArrayExpr MkSetUnion(params ArrayExpr[] args)
Take the union of a list of sets.
Definition: Context.cs:2190
Solver MkSolver(Tactic t)
Creates a solver that is implemented using the given tactic.
Definition: Context.cs:3463
A real sort
Definition: RealSort.cs:28
ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
Create an array constant.
Definition: Context.cs:1999
static Z3_ast Z3_mk_fpa_to_fp_unsigned(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
Definition: Native.cs:6738
static Z3_ast Z3_mk_bvsrem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2662
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:4184
static Z3_ast Z3_mk_repeat(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2774
Integer Numerals
Definition: IntNum.cs:32
FPSort MkFPSort128()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition: Context.cs:3681
static Z3_ast Z3_mk_fpa_rtn(Z3_context a0)
Definition: Native.cs:6346
BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
Bitwise XOR.
Definition: Context.cs:1224
BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Logical shift right
Definition: Context.cs:1700
BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise subtraction does not underflow.
Definition: Context.cs:1904
BitVecExpr MkSignExt(uint i, BitVecExpr t)
Bit-vector sign extension.
Definition: Context.cs:1623
static Z3_sort Z3_mk_fpa_sort_half(Z3_context a0)
Definition: Native.cs:6378
static Z3_ast Z3_mk_unsigned_int(Z3_context a0, uint a1, Z3_sort a2)
Definition: Native.cs:3070
static Z3_ast Z3_mk_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2342
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:2598
static Z3_context Z3_mk_context_rc(Z3_config a0)
Definition: Native.cs:1988
static Z3_ast Z3_mk_bvadd_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2862
static Z3_ast Z3_mk_set_del(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2990
static Z3_ast Z3_mk_ext_rotate_left(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2822
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:4176
FPNum MkFPZero(FPSort s, bool negative)
Create a floating-point zero of sort s.
Definition: Context.cs:3715
static Z3_ast Z3_mk_bvsdiv_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2886
BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise addition does not underflow.
Definition: Context.cs:1870
static Z3_ast Z3_mk_bvule(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2694
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
Definition: Context.cs:923
static Z3_ast Z3_mk_fpa_sub(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:6538
FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point addition
Definition: Context.cs:3868
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:3833
static Z3_ast Z3_mk_bvslt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2686
static Z3_ast Z3_mk_power(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2470
static Z3_ast Z3_mk_bvmul_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Definition: Native.cs:2902
BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement signed greater-than.
Definition: Context.cs:1565
static Z3_ast Z3_mk_const_array(Z3_context a0, Z3_sort a1, Z3_ast a2)
Definition: Native.cs:2934
static Z3_ast Z3_mk_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2494
ArrayExpr MkEmptySet(Sort domain)
Create an empty set.
Definition: Context.cs:2137
BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise multiplication does not overflow.
Definition: Context.cs:1953
static Z3_ast Z3_mk_xor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2390
BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
Floating-point equality.
Definition: Context.cs:4034
Constructors are used for datatype sorts.
Definition: Constructor.cs:29
Probe MkProbe(string name)
Creates a new Probe.
Definition: Context.cs:3280
static Z3_ast Z3_mk_ite(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:2366
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
Shift left.
Definition: Context.cs:1677
static Z3_ast Z3_mk_bvadd(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2614
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
Bitwise disjunction.
Definition: Context.cs:1209
static Z3_ast Z3_mk_fpa_rem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6578
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:4207
FloatingPoint Expressions
Definition: FPExpr.cs:31
BitVecExpr MkBVConst(Symbol name, uint size)
Creates a bit-vector constant.
Definition: Context.cs:741
The FloatingPoint RoundingMode sort
Definition: FPRMSort.cs:28
FPNum MkFP(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3796
static Z3_ast Z3_mk_iff(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2374
Array expressions
Definition: ArrayExpr.cs:31
static Z3_ast Z3_mk_and(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2398
static Z3_ast Z3_mk_unsigned_int64(Z3_context a0, UInt64 a1, Z3_sort a2)
Definition: Native.cs:3086
static Z3_ast Z3_mk_distinct(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2350
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:3060
static Z3_ast Z3_mk_select(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2918
static Z3_ast Z3_mk_int2bv(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2838
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:3870
static Z3_tactic Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Definition: Native.cs:4999
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
BoolSort MkBoolSort()
Create a new Boolean sort.
Definition: Context.cs:163
BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
Arithmetic shift right
Definition: Context.cs:1725
FPRMNum MkFPRoundNearestTiesToAway()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
Definition: Context.cs:3532
static Z3_ast Z3_mk_fpa_rtp(Z3_context a0)
Definition: Native.cs:6330
static Z3_sort Z3_mk_fpa_sort_16(Z3_context a0)
Definition: Native.cs:6386
BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement signed less-than or equal to.
Definition: Context.cs:1497
static Z3_ast Z3_mk_false(Z3_context a0)
Definition: Native.cs:2334
BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
Rotate Right.
Definition: Context.cs:1759
static Z3_ast Z3_mk_bound(Z3_context a0, uint a1, Z3_sort a2)
Definition: Native.cs:3102
static Z3_ast Z3_mk_fpa_rtz(Z3_context a0)
Definition: Native.cs:6362
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:2590
static Z3_probe Z3_probe_not(Z3_context a0, Z3_probe a1)
Definition: Native.cs:5167
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:6442
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 -> t2.
Definition: Context.cs:882
static Z3_tactic Z3_tactic_fail_if(Z3_context a0, Z3_probe a1)
Definition: Native.cs:5079
BoolExpr MkFPIsNegative(FPExpr t)
Predicate indicating whether t is a negative floating-point number.
Definition: Context.cs:4094
static Z3_ast Z3_mk_bvsgt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2734
static Z3_probe Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:5135
BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Create a predicate that checks that the bit-wise multiplication does not underflow.
Definition: Context.cs:1970
static Z3_ast Z3_mk_fpa_numeral_double(Z3_context a0, double a1, Z3_sort a2)
Definition: Native.cs:6482
static Z3_ast Z3_mk_bvxor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2574
Enumeration sorts.
Definition: EnumSort.cs:29
FPRMNum MkFPRoundTowardPositive()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode...
Definition: Context.cs:3550
FPSort MkFPSortDouble()
Create the double-precision (64-bit) FloatingPoint sort.
Definition: Context.cs:3654
static uint Z3_get_smtlib_num_decls(Z3_context a0)
Definition: Native.cs:4246
BitVecExpr MkRepeat(uint i, BitVecExpr t)
Bit-vector repetition.
Definition: Context.cs:1656
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:2438
static Z3_sort Z3_mk_fpa_sort_quadruple(Z3_context a0)
Definition: Native.cs:6426
static Z3_ast Z3_mk_fpa_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6618
static Z3_ast Z3_mk_set_member(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:3030
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:3391
static Z3_ast Z3_mk_fpa_is_zero(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6666
static Z3_ast Z3_mk_bvlshr(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2790
static Z3_pattern Z3_mk_pattern(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:3094
static Z3_ast Z3_mk_add(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2414
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
Definition: Context.cs:953
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:2272
static Z3_ast Z3_mk_fpa_to_fp_real(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3)
Definition: Native.cs:6722
ArrayExpr MkSetDel(ArrayExpr set, Expr element)
Remove an element from a set.
Definition: Context.cs:2176
static void Z3_del_context(Z3_context a0)
Definition: Native.cs:1995
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:6570
static Z3_ast Z3_mk_full_set(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2974
BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
Create a predicate that checks that the bit-wise addition does not overflow.
Definition: Context.cs:1853
static Z3_ast Z3_mk_fpa_round_toward_zero(Z3_context a0)
Definition: Native.cs:6354
static Z3_ast Z3_mk_fpa_neg(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6522
BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
Floating-point less than.
Definition: Context.cs:3998
static Z3_tactic Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2)
Definition: Native.cs:5039
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:2697
static Z3_ast Z3_mk_set_difference(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:3014
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:2534
BitVecNum MkBV(int v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2539
static void Z3_del_config(Z3_config a0)
Definition: Native.cs:1973
DecRefQueue interface
Definition: IDecRefQueue.cs:32
static Z3_config Z3_mk_config()
Definition: Native.cs:1968
static Z3_ast Z3_mk_bvsub(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2622
def ArraySort(d, r)
Definition: z3py.py:4004
static Z3_ast Z3_mk_bvsge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2718
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:1446
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition: Context.cs:896
def IntSort(ctx=None)
Definition: z3py.py:2639
static Z3_ast Z3_mk_store(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:2926
BoolExpr MkBVNegNoOverflow(BitVecExpr t)
Create a predicate that checks that the bit-wise negation does not overflow.
Definition: Context.cs:1938
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:3361
BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
Bit-vector concatenation.
Definition: Context.cs:1586
static Z3_ast Z3_mk_ext_rotate_right(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2830
RealExpr MkInt2Real(IntExpr t)
Coerce an integer to a real.
Definition: Context.cs:1112
static Z3_ast Z3_mk_fpa_is_subnormal(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6658
FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point multiplication
Definition: Context.cs:3892
static Z3_ast Z3_mk_fpa_is_positive(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6698
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4458
IntExpr MkIntConst(string name)
Creates an integer constant.
Definition: Context.cs:709
BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
Floating-point greater than.
Definition: Context.cs:4020
static Z3_ast Z3_mk_rem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2462
static Z3_ast Z3_mk_ge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2502
static Z3_tactic Z3_tactic_fail_if_not_decided(Z3_context a0)
Definition: Native.cs:5087
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:6458
static Z3_solver Z3_mk_simple_solver(Z3_context a0)
Definition: Native.cs:5317
Tactic FailIf(Probe p)
Create a tactic that fails if the probe p evaluates to false.
Definition: Context.cs:3157
BitVecNum MkBV(uint v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2551
BitVecExpr MkBVRedOR(BitVecExpr t)
Take disjunction of bits in a vector, return vector of length 1.
Definition: Context.cs:1181
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:3965
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:2625
static Z3_ast Z3_mk_fpa_to_ieee_bv(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6826
static Z3_sort Z3_get_smtlib_sort(Z3_context a0, uint a1)
Definition: Native.cs:4270
static Z3_ast Z3_mk_bvult(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2678
static Z3_tactic Z3_tactic_skip(Z3_context a0)
Definition: Native.cs:5063
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 iff t2.
Definition: Context.cs:868
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:5175
static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1)
Definition: Native.cs:1948
static Z3_ast Z3_mk_bvsub_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Definition: Native.cs:2878
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:3046
static Z3_ast Z3_mk_bvurem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2654
static Z3_ast Z3_mk_bvsdiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2646
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:3954
BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
Signed remainder.
Definition: Context.cs:1411
static Z3_probe Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:5151
Tactic Fail()
Create a tactic always fails.
Definition: Context.cs:3147
BitVecExpr MkInt2BV(uint n, IntExpr t)
Create an n bit bit-vector from the integer argument t .
Definition: Context.cs:1814
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:837
static uint Z3_get_smtlib_num_formulas(Z3_context a0)
Definition: Native.cs:4214
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
Definition: Context.cs:979
BoolExpr MkFPIsSubnormal(FPExpr t)
Predicate indicating whether t is a subnormal floating-point number.
Definition: Context.cs:4054
FPRMNum MkFPRTP()
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode...
Definition: Context.cs:3559
static Z3_ast Z3_mk_bvsmod(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2670
BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Check for subsetness of sets.
Definition: Context.cs:2255
static Z3_ast Z3_mk_rotate_right(Z3_context a0, uint a1, Z3_ast a2)
Definition: Native.cs:2814
FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
Floating-point square root
Definition: Context.cs:3931
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:31
ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 ^ t2.
Definition: Context.cs:1035
static Z3_ast Z3_mk_bvsle(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2702
static Z3_ast Z3_mk_int2real(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2510
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:2806
static Z3_probe Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:5119
Expr MkTermArray(ArrayExpr array)
Access the array default value.
Definition: Context.cs:2111
RatNum MkReal(ulong v)
Create a real numeral.
Definition: Context.cs:2452
ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
Array update.
Definition: Context.cs:2049
Rational Numerals
Definition: RatNum.cs:32
FPNum MkFPNumeral(double v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3737
Tactic With(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3195
The abstract syntax tree (AST) class.
Definition: AST.cs:31
FPSort MkFPSortQuadruple()
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition: Context.cs:3672
FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Floating-point subtraction
Definition: Context.cs:3880
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3460
static uint Z3_get_smtlib_num_sorts(Z3_context a0)
Definition: Native.cs:4262
static Z3_ast Z3_mk_bvugt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2726
static Z3_ast Z3_mk_fpa_min(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6594
RealExpr MkRealConst(Symbol name)
Creates a real constant.
Definition: Context.cs:720
static Z3_ast Z3_mk_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2478
IntNum MkInt(ulong v)
Create an integer numeral.
Definition: Context.cs:2513
FloatingPoint RoundingMode Expressions
Definition: FPRMExpr.cs:31
FPRMNum MkFPRoundTowardNegative()
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode...
Definition: Context.cs:3568
ArrayExpr MkSetIntersection(params ArrayExpr[] args)
Take the intersection of a list of sets.
Definition: Context.cs:2202
IntPtr UnwrapAST(AST a)
Unwraps an AST.
Definition: Context.cs:4324
static Z3_ast Z3_mk_fpa_mul(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:6546
static Z3_ast Z3_mk_fpa_is_nan(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6682
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:6530
static Z3_ast Z3_mk_int(Z3_context a0, int a1, Z3_sort a2)
Definition: Native.cs:3062
FPNum MkFP(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3785
Probe ConstProbe(double val)
Create a probe that always evaluates to val .
Definition: Context.cs:3290
static void Z3_update_param_value(Z3_context a0, string a1, string a2)
Definition: Native.cs:2013
IntExpr MkBV2Int(BitVecExpr t, bool signed)
Create an integer from the bit-vector argument t .
Definition: Context.cs:1838
BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
Unsigned remainder.
Definition: Context.cs:1390
RatNum MkReal(long v)
Create a real numeral.
Definition: Context.cs:2440
IntNum MkInt(long v)
Create an integer numeral.
Definition: Context.cs:2501
Expr MkSelect(ArrayExpr a, Expr i)
Array read.
Definition: Context.cs:2021
static Z3_tactic Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, uint a2)
Definition: Native.cs:5055
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:2789
BoolExpr MkFPIsNormal(FPExpr t)
Predicate indicating whether t is a normal floating-point number.
Definition: Context.cs:4044
FPNum MkFPNumeral(int v, FPSort s)
Create a numeral of FloatingPoint sort from an int.
Definition: Context.cs:3748
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:3108
static Z3_ast Z3_mk_set_union(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Definition: Native.cs:2998
Tactic FailIfNotDecided()
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatis...
Definition: Context.cs:3170
Z3_ast_print_mode
Z3_ast_print_mode
static Z3_ast Z3_mk_array_default(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2950
static Z3_ast Z3_mk_bvnand(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2582
BoolExpr MkFalse()
The false Term.
Definition: Context.cs:789
Set sorts.
Definition: SetSort.cs:29
ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
Add an element to the set.
Definition: Context.cs:2161
delegate void Z3_error_handler(Z3_context c, Z3_error_code e)
BoolExpr MkFPIsZero(FPExpr t)
Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0...
Definition: Context.cs:4064
Tactic TryFor(Tactic t, uint ms)
Create a tactic that applies t to a goal for ms milliseconds.
Definition: Context.cs:3077
BitVecExpr MkBVConst(string name, uint size)
Creates a bit-vector constant.
Definition: Context.cs:752
BitVecNum MkBV(ulong v, uint size)
Create a bit-vector numeral.
Definition: Context.cs:2575
static Z3_ast Z3_mk_fpa_round_toward_positive(Z3_context a0)
Definition: Native.cs:6322
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:3316
IntExpr MkRem(IntExpr t1, IntExpr t2)
Create an expression representing t1 rem t2.
Definition: Context.cs:1021
static Z3_ast Z3_mk_fpa_div(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:6554
FPSort MkFPSort32()
Create the single-precision (32-bit) FloatingPoint sort.
Definition: Context.cs:3645
static Z3_ast Z3_mk_int64(Z3_context a0, Int64 a1, Z3_sort a2)
Definition: Native.cs:3078
ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Take the difference between two sets.
Definition: Context.cs:2215
Tactic Skip()
Create a tactic that just returns the given goal.
Definition: Context.cs:3137
static Z3_ast Z3_mk_numeral(Z3_context a0, string a1, Z3_sort a2)
Definition: Native.cs:3046
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
FPSort MkFPSortHalf()
Create the half-precision (16-bit) FloatingPoint sort.
Definition: Context.cs:3618
static Z3_ast Z3_mk_const(Z3_context a0, IntPtr a1, Z3_sort a2)
Definition: Native.cs:2302
FloatingPoint sort
Definition: FPSort.cs:27
IntExpr MkReal2Int(RealExpr t)
Coerce a real to an integer.
Definition: Context.cs:1128
static Z3_ast Z3_mk_bvneg(Z3_context a0, Z3_ast a1)
Definition: Native.cs:2606
static Z3_ast Z3_mk_set_complement(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3022
static Z3_tactic Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2)
Definition: Native.cs:5095
BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement subtraction.
Definition: Context.cs:1312
void Dispose()
Disposes of the context.
Definition: Context.cs:4565
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
Definition: Context.cs:823
static Z3_ast Z3_mk_fpa_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:6634
FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
Creates a new function declaration.
Definition: Context.cs:505
static uint Z3_get_smtlib_num_assumptions(Z3_context a0)
Definition: Native.cs:4230
FPSort MkFPSort64()
Create the double-precision (64-bit) FloatingPoint sort.
Definition: Context.cs:3663
static Z3_ast Z3_mk_fpa_rne(Z3_context a0)
Definition: Native.cs:6298
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:2674
FPRMNum MkFPRNA()
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
Definition: Context.cs:3541
BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
Bitwise NAND.
Definition: Context.cs:1239
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:2742
static Z3_ast Z3_mk_fpa_numeral_int(Z3_context a0, int a1, Z3_sort a2)
Definition: Native.cs:6490
static Z3_solver Z3_mk_solver_for_logic(Z3_context a0, IntPtr a1)
Definition: Native.cs:5325
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:6706
Solver MkSimpleSolver()
Creates a new (incremental) solver.
Definition: Context.cs:3449
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:4288
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition: Context.cs:405
BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
Two&#39;s complement multiplication.
Definition: Context.cs:1327
BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
Floating-point greater than or equal.
Definition: Context.cs:4009
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
Definition: Context.cs:1091
static Z3_ast Z3_mk_div(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2446
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:1077
Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
Update a datatype field at expression t with value v. The function performs a record update at t...
Definition: Context.cs:458
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:1006
Tuple sorts.
Definition: TupleSort.cs:29
static Z3_ast Z3_get_smtlib_assumption(Z3_context a0, uint a1)
Definition: Native.cs:4238
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:4192
static Z3_ast Z3_mk_fpa_rna(Z3_context a0)
Definition: Native.cs:6314
static Z3_sort Z3_mk_fpa_sort_32(Z3_context a0)
Definition: Native.cs:6402
BoolExpr MkFPIsPositive(FPExpr t)
Predicate indicating whether t is a positive floating-point number.
Definition: Context.cs:4104
def BoolSort(ctx=None)
Definition: z3py.py:1346
BoolExpr MkBool(bool value)
Creates a Boolean value.
Definition: Context.cs:799
BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
Rotate Left.
Definition: Context.cs:1743
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:2750
static Z3_ast Z3_mk_bvsub_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2870
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:1641
Real expressions
Definition: RealExpr.cs:31
static Z3_ast Z3_mk_bvor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:2566
RatNum MkReal(uint v)
Create a real numeral.
Definition: Context.cs:2428
A function interpretation is represented as a finite map and an &#39;else&#39; value. Each entry in the finit...
Definition: FuncInterp.cs:30
BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
Parse the given file using the SMT-LIB2 parser.
Definition: Context.cs:2914
Expr MkConst(FuncDecl f)
Creates a fresh constant from the FuncDecl f .
Definition: Context.cs:666
static void Z3_set_param_value(Z3_config a0, string a1, string a2)
Definition: Native.cs:1977
static Z3_sort Z3_mk_fpa_sort_single(Z3_context a0)
Definition: Native.cs:6394
static Z3_sort Z3_mk_fpa_sort_double(Z3_context a0)
Definition: Native.cs:6410
static Z3_probe Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2)
Definition: Native.cs:5111
static Z3_ast Z3_mk_map(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3)
Definition: Native.cs:2942