00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Collections.Generic;
00022 using System.Runtime.InteropServices;
00023 using System.Diagnostics.Contracts;
00024
00025 namespace Microsoft.Z3
00026 {
00030 [ContractVerification(true)]
00031 public class Context : IDisposable
00032 {
00033 #region Constructors
00034
00035
00036
00037 public Context()
00038 : base()
00039 {
00040 m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
00041 InitContext();
00042 }
00043
00062 public Context(Dictionary<string, string> settings)
00063 : base()
00064 {
00065 Contract.Requires(settings != null);
00066
00067 IntPtr cfg = Native.Z3_mk_config();
00068 foreach (KeyValuePair<string, string> kv in settings)
00069 Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
00070 m_ctx = Native.Z3_mk_context_rc(cfg);
00071 Native.Z3_del_config(cfg);
00072 InitContext();
00073 }
00074 #endregion
00075
00076 #region Symbols
00077
00078
00079
00080
00081
00082
00083
00084 public IntSymbol MkSymbol(int i)
00085 {
00086 Contract.Ensures(Contract.Result<IntSymbol>() != null);
00087
00088 return new IntSymbol(this, i);
00089 }
00090
00094 public StringSymbol MkSymbol(string name)
00095 {
00096 Contract.Ensures(Contract.Result<StringSymbol>() != null);
00097
00098 return new StringSymbol(this, name);
00099 }
00100
00104 internal Symbol[] MkSymbols(string[] names)
00105 {
00106 Contract.Ensures(names == null || Contract.Result<Symbol[]>() != null);
00107 Contract.Ensures(names != null || Contract.Result<Symbol[]>() == null);
00108 Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.Result<Symbol[]>().Length == names.Length);
00109 Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.ForAll(Contract.Result<Symbol[]>(), s => s != null));
00110
00111 if (names == null) return null;
00112 Symbol[] result = new Symbol[names.Length];
00113 for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
00114 return result;
00115 }
00116 #endregion
00117
00118 #region Sorts
00119 private BoolSort m_boolSort = null;
00120 private IntSort m_intSort = null;
00121 private RealSort m_realSort = null;
00122
00126 public BoolSort BoolSort
00127 {
00128 get
00129 {
00130 Contract.Ensures(Contract.Result<BoolSort>() != null);
00131 if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
00132 }
00133 }
00134
00138 public IntSort IntSort
00139 {
00140 get
00141 {
00142 Contract.Ensures(Contract.Result<IntSort>() != null);
00143 if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
00144 }
00145 }
00146
00147
00151 public RealSort RealSort
00152 {
00153 get
00154 {
00155 Contract.Ensures(Contract.Result<RealSort>() != null);
00156 if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
00157 }
00158 }
00159
00163 public BoolSort MkBoolSort()
00164 {
00165 Contract.Ensures(Contract.Result<BoolSort>() != null);
00166 return new BoolSort(this);
00167 }
00168
00172 public UninterpretedSort MkUninterpretedSort(Symbol s)
00173 {
00174 Contract.Requires(s != null);
00175 Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
00176
00177 CheckContextMatch(s);
00178 return new UninterpretedSort(this, s);
00179 }
00180
00184 public UninterpretedSort MkUninterpretedSort(string str)
00185 {
00186 Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
00187
00188 return MkUninterpretedSort(MkSymbol(str));
00189 }
00190
00194 public IntSort MkIntSort()
00195 {
00196 Contract.Ensures(Contract.Result<IntSort>() != null);
00197
00198 return new IntSort(this);
00199 }
00200
00204 public RealSort MkRealSort()
00205 {
00206 Contract.Ensures(Contract.Result<RealSort>() != null);
00207 return new RealSort(this);
00208 }
00209
00213 public BitVecSort MkBitVecSort(uint size)
00214 {
00215 Contract.Ensures(Contract.Result<BitVecSort>() != null);
00216
00217 return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
00218 }
00219
00223 public ArraySort MkArraySort(Sort domain, Sort range)
00224 {
00225 Contract.Requires(domain != null);
00226 Contract.Requires(range != null);
00227 Contract.Ensures(Contract.Result<ArraySort>() != null);
00228
00229 CheckContextMatch(domain);
00230 CheckContextMatch(range);
00231 return new ArraySort(this, domain, range);
00232 }
00233
00237 public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
00238 {
00239 Contract.Requires(name != null);
00240 Contract.Requires(fieldNames != null);
00241 Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
00242 Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
00243 Contract.Ensures(Contract.Result<TupleSort>() != null);
00244
00245 CheckContextMatch(name);
00246 CheckContextMatch(fieldNames);
00247 CheckContextMatch(fieldSorts);
00248 return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
00249 }
00250
00254 public EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
00255 {
00256 Contract.Requires(name != null);
00257 Contract.Requires(enumNames != null);
00258 Contract.Requires(Contract.ForAll(enumNames, f => f != null));
00259
00260 Contract.Ensures(Contract.Result<EnumSort>() != null);
00261
00262 CheckContextMatch(name);
00263 CheckContextMatch(enumNames);
00264 return new EnumSort(this, name, enumNames);
00265 }
00266
00270 public EnumSort MkEnumSort(string name, params string[] enumNames)
00271 {
00272 Contract.Requires(enumNames != null);
00273 Contract.Ensures(Contract.Result<EnumSort>() != null);
00274
00275 return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
00276 }
00277
00281 public ListSort MkListSort(Symbol name, Sort elemSort)
00282 {
00283 Contract.Requires(name != null);
00284 Contract.Requires(elemSort != null);
00285 Contract.Ensures(Contract.Result<ListSort>() != null);
00286
00287 CheckContextMatch(name);
00288 CheckContextMatch(elemSort);
00289 return new ListSort(this, name, elemSort);
00290 }
00291
00295 public ListSort MkListSort(string name, Sort elemSort)
00296 {
00297 Contract.Requires(elemSort != null);
00298 Contract.Ensures(Contract.Result<ListSort>() != null);
00299
00300 CheckContextMatch(elemSort);
00301 return new ListSort(this, MkSymbol(name), elemSort);
00302 }
00303
00310 public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
00311 {
00312 Contract.Requires(name != null);
00313 Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
00314
00315 CheckContextMatch(name);
00316 return new FiniteDomainSort(this, name, size);
00317 }
00318
00327 public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
00328 {
00329 Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
00330
00331 return new FiniteDomainSort(this, MkSymbol(name), size);
00332 }
00333
00334
00335 #region Datatypes
00336
00337
00338
00339
00340
00341
00342
00343
00344
00345
00346 public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
00347 {
00348 Contract.Requires(name != null);
00349 Contract.Requires(recognizer != null);
00350 Contract.Ensures(Contract.Result<Constructor>() != null);
00351
00352 return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
00353 }
00354
00364 public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
00365 {
00366 Contract.Ensures(Contract.Result<Constructor>() != null);
00367
00368 return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
00369 }
00370
00374 public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
00375 {
00376 Contract.Requires(name != null);
00377 Contract.Requires(constructors != null);
00378 Contract.Requires(Contract.ForAll(constructors, c => c != null));
00379
00380 Contract.Ensures(Contract.Result<DatatypeSort>() != null);
00381
00382 CheckContextMatch(name);
00383 CheckContextMatch(constructors);
00384 return new DatatypeSort(this, name, constructors);
00385 }
00386
00390 public DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
00391 {
00392 Contract.Requires(constructors != null);
00393 Contract.Requires(Contract.ForAll(constructors, c => c != null));
00394 Contract.Ensures(Contract.Result<DatatypeSort>() != null);
00395
00396 CheckContextMatch(constructors);
00397 return new DatatypeSort(this, MkSymbol(name), constructors);
00398 }
00399
00405 public DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
00406 {
00407 Contract.Requires(names != null);
00408 Contract.Requires(c != null);
00409 Contract.Requires(names.Length == c.Length);
00410 Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
00411 Contract.Requires(Contract.ForAll(names, name => name != null));
00412 Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
00413
00414 CheckContextMatch(names);
00415 uint n = (uint)names.Length;
00416 ConstructorList[] cla = new ConstructorList[n];
00417 IntPtr[] n_constr = new IntPtr[n];
00418 for (uint i = 0; i < n; i++)
00419 {
00420 Constructor[] constructor = c[i];
00421 Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
00422 CheckContextMatch(constructor);
00423 cla[i] = new ConstructorList(this, constructor);
00424 n_constr[i] = cla[i].NativeObject;
00425 }
00426 IntPtr[] n_res = new IntPtr[n];
00427 Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
00428 DatatypeSort[] res = new DatatypeSort[n];
00429 for (uint i = 0; i < n; i++)
00430 res[i] = new DatatypeSort(this, n_res[i]);
00431 return res;
00432 }
00433
00440 public DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
00441 {
00442 Contract.Requires(names != null);
00443 Contract.Requires(c != null);
00444 Contract.Requires(names.Length == c.Length);
00445 Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
00446 Contract.Requires(Contract.ForAll(names, name => name != null));
00447 Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
00448
00449 return MkDatatypeSorts(MkSymbols(names), c);
00450 }
00451
00452 #endregion
00453 #endregion
00454
00455 #region Function Declarations
00456
00457
00458
00459 public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
00460 {
00461 Contract.Requires(name != null);
00462 Contract.Requires(range != null);
00463 Contract.Requires(Contract.ForAll(domain, d => d != null));
00464 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00465
00466 CheckContextMatch(name);
00467 CheckContextMatch(domain);
00468 CheckContextMatch(range);
00469 return new FuncDecl(this, name, domain, range);
00470 }
00471
00475 public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
00476 {
00477 Contract.Requires(name != null);
00478 Contract.Requires(domain != null);
00479 Contract.Requires(range != null);
00480 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00481
00482 CheckContextMatch(name);
00483 CheckContextMatch(domain);
00484 CheckContextMatch(range);
00485 Sort[] q = new Sort[] { domain };
00486 return new FuncDecl(this, name, q, range);
00487 }
00488
00492 public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
00493 {
00494 Contract.Requires(range != null);
00495 Contract.Requires(Contract.ForAll(domain, d => d != null));
00496 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00497
00498 CheckContextMatch(domain);
00499 CheckContextMatch(range);
00500 return new FuncDecl(this, MkSymbol(name), domain, range);
00501 }
00502
00506 public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
00507 {
00508 Contract.Requires(range != null);
00509 Contract.Requires(domain != null);
00510 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00511
00512 CheckContextMatch(domain);
00513 CheckContextMatch(range);
00514 Sort[] q = new Sort[] { domain };
00515 return new FuncDecl(this, MkSymbol(name), q, range);
00516 }
00517
00523 public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
00524 {
00525 Contract.Requires(range != null);
00526 Contract.Requires(Contract.ForAll(domain, d => d != null));
00527 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00528
00529 CheckContextMatch(domain);
00530 CheckContextMatch(range);
00531 return new FuncDecl(this, prefix, domain, range);
00532 }
00533
00537 public FuncDecl MkConstDecl(Symbol name, Sort range)
00538 {
00539 Contract.Requires(name != null);
00540 Contract.Requires(range != null);
00541 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00542
00543 CheckContextMatch(name);
00544 CheckContextMatch(range);
00545 return new FuncDecl(this, name, null, range);
00546 }
00547
00551 public FuncDecl MkConstDecl(string name, Sort range)
00552 {
00553 Contract.Requires(range != null);
00554 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00555
00556 CheckContextMatch(range);
00557 return new FuncDecl(this, MkSymbol(name), null, range);
00558 }
00559
00565 public FuncDecl MkFreshConstDecl(string prefix, Sort range)
00566 {
00567 Contract.Requires(range != null);
00568 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00569
00570 CheckContextMatch(range);
00571 return new FuncDecl(this, prefix, null, range);
00572 }
00573 #endregion
00574
00575 #region Bound Variables
00576
00577
00578
00579
00580
00581 public Expr MkBound(uint index, Sort ty)
00582 {
00583 Contract.Requires(ty != null);
00584 Contract.Ensures(Contract.Result<Expr>() != null);
00585
00586 return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
00587 }
00588 #endregion
00589
00590 #region Quantifier Patterns
00591
00592
00593
00594 public Pattern MkPattern(params Expr[] terms)
00595 {
00596 Contract.Requires(terms != null);
00597 if (terms.Length == 0)
00598 throw new Z3Exception("Cannot create a pattern from zero terms");
00599
00600 Contract.Ensures(Contract.Result<Pattern>() != null);
00601
00602 Contract.EndContractBlock();
00603
00604 IntPtr[] termsNative = AST.ArrayToNative(terms);
00605 return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
00606 }
00607 #endregion
00608
00609 #region Constants
00610
00611
00612
00613 public Expr MkConst(Symbol name, Sort range)
00614 {
00615 Contract.Requires(name != null);
00616 Contract.Requires(range != null);
00617 Contract.Ensures(Contract.Result<Expr>() != null);
00618
00619 CheckContextMatch(name);
00620 CheckContextMatch(range);
00621
00622 return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
00623 }
00624
00628 public Expr MkConst(string name, Sort range)
00629 {
00630 Contract.Requires(range != null);
00631 Contract.Ensures(Contract.Result<Expr>() != null);
00632
00633 return MkConst(MkSymbol(name), range);
00634 }
00635
00640 public Expr MkFreshConst(string prefix, Sort range)
00641 {
00642 Contract.Requires(range != null);
00643 Contract.Ensures(Contract.Result<Expr>() != null);
00644
00645 CheckContextMatch(range);
00646 return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
00647 }
00648
00653 public Expr MkConst(FuncDecl f)
00654 {
00655 Contract.Requires(f != null);
00656 Contract.Ensures(Contract.Result<Expr>() != null);
00657
00658 return MkApp(f);
00659 }
00660
00664 public BoolExpr MkBoolConst(Symbol name)
00665 {
00666 Contract.Requires(name != null);
00667 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00668
00669 return (BoolExpr)MkConst(name, BoolSort);
00670 }
00671
00675 public BoolExpr MkBoolConst(string name)
00676 {
00677 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00678
00679 return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
00680 }
00681
00685 public IntExpr MkIntConst(Symbol name)
00686 {
00687 Contract.Requires(name != null);
00688 Contract.Ensures(Contract.Result<IntExpr>() != null);
00689
00690 return (IntExpr)MkConst(name, IntSort);
00691 }
00692
00696 public IntExpr MkIntConst(string name)
00697 {
00698 Contract.Requires(name != null);
00699 Contract.Ensures(Contract.Result<IntExpr>() != null);
00700
00701 return (IntExpr)MkConst(name, IntSort);
00702 }
00703
00707 public RealExpr MkRealConst(Symbol name)
00708 {
00709 Contract.Requires(name != null);
00710 Contract.Ensures(Contract.Result<RealExpr>() != null);
00711
00712 return (RealExpr)MkConst(name, RealSort);
00713 }
00714
00718 public RealExpr MkRealConst(string name)
00719 {
00720 Contract.Ensures(Contract.Result<RealExpr>() != null);
00721
00722 return (RealExpr)MkConst(name, RealSort);
00723 }
00724
00728 public BitVecExpr MkBVConst(Symbol name, uint size)
00729 {
00730 Contract.Requires(name != null);
00731 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
00732
00733 return (BitVecExpr)MkConst(name, MkBitVecSort(size));
00734 }
00735
00739 public BitVecExpr MkBVConst(string name, uint size)
00740 {
00741 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
00742
00743 return (BitVecExpr)MkConst(name, MkBitVecSort(size));
00744 }
00745 #endregion
00746
00747 #region Terms
00748
00749
00750
00751 public Expr MkApp(FuncDecl f, params Expr[] args)
00752 {
00753 Contract.Requires(f != null);
00754 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
00755 Contract.Ensures(Contract.Result<Expr>() != null);
00756
00757 CheckContextMatch(f);
00758 CheckContextMatch(args);
00759 return Expr.Create(this, f, args);
00760 }
00761
00762 #region Propositional
00763
00764
00765
00766 public BoolExpr MkTrue()
00767 {
00768 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00769
00770 return new BoolExpr(this, Native.Z3_mk_true(nCtx));
00771 }
00772
00776 public BoolExpr MkFalse()
00777 {
00778 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00779
00780 return new BoolExpr(this, Native.Z3_mk_false(nCtx));
00781 }
00782
00786 public BoolExpr MkBool(bool value)
00787 {
00788 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00789
00790 return value ? MkTrue() : MkFalse();
00791 }
00792
00796 public BoolExpr MkEq(Expr x, Expr y)
00797 {
00798 Contract.Requires(x != null);
00799 Contract.Requires(y != null);
00800 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00801
00802 CheckContextMatch(x);
00803 CheckContextMatch(y);
00804 return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
00805 }
00806
00810 public BoolExpr MkDistinct(params Expr[] args)
00811 {
00812 Contract.Requires(args != null);
00813 Contract.Requires(Contract.ForAll(args, a => a != null));
00814
00815 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00816
00817 CheckContextMatch(args);
00818 return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
00819 }
00820
00824 public BoolExpr MkNot(BoolExpr a)
00825 {
00826 Contract.Requires(a != null);
00827 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00828
00829 CheckContextMatch(a);
00830 return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
00831 }
00832
00839 public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
00840 {
00841 Contract.Requires(t1 != null);
00842 Contract.Requires(t2 != null);
00843 Contract.Requires(t3 != null);
00844 Contract.Ensures(Contract.Result<Expr>() != null);
00845
00846 CheckContextMatch(t1);
00847 CheckContextMatch(t2);
00848 CheckContextMatch(t3);
00849 return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
00850 }
00851
00855 public BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
00856 {
00857 Contract.Requires(t1 != null);
00858 Contract.Requires(t2 != null);
00859 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00860
00861 CheckContextMatch(t1);
00862 CheckContextMatch(t2);
00863 return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
00864 }
00865
00869 public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
00870 {
00871 Contract.Requires(t1 != null);
00872 Contract.Requires(t2 != null);
00873 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00874
00875 CheckContextMatch(t1);
00876 CheckContextMatch(t2);
00877 return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
00878 }
00879
00883 public BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
00884 {
00885 Contract.Requires(t1 != null);
00886 Contract.Requires(t2 != null);
00887 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00888
00889 CheckContextMatch(t1);
00890 CheckContextMatch(t2);
00891 return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
00892 }
00893
00897 public BoolExpr MkAnd(params BoolExpr[] t)
00898 {
00899 Contract.Requires(t != null);
00900 Contract.Requires(Contract.ForAll(t, a => a != null));
00901 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00902
00903 CheckContextMatch(t);
00904 return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
00905 }
00906
00910 public BoolExpr MkOr(params BoolExpr[] t)
00911 {
00912 Contract.Requires(t != null);
00913 Contract.Requires(Contract.ForAll(t, a => a != null));
00914 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00915
00916 CheckContextMatch(t);
00917 return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
00918 }
00919
00920
00921 #endregion
00922
00923 #region Arithmetic
00924
00925
00926
00927 public ArithExpr MkAdd(params ArithExpr[] t)
00928 {
00929 Contract.Requires(t != null);
00930 Contract.Requires(Contract.ForAll(t, a => a != null));
00931 Contract.Ensures(Contract.Result<ArithExpr>() != null);
00932
00933 CheckContextMatch(t);
00934 return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
00935 }
00936
00940 public ArithExpr MkMul(params ArithExpr[] t)
00941 {
00942 Contract.Requires(t != null);
00943 Contract.Requires(Contract.ForAll(t, a => a != null));
00944 Contract.Ensures(Contract.Result<ArithExpr>() != null);
00945
00946 CheckContextMatch(t);
00947 return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
00948 }
00949
00953 public ArithExpr MkSub(params ArithExpr[] t)
00954 {
00955 Contract.Requires(t != null);
00956 Contract.Requires(Contract.ForAll(t, a => a != null));
00957 Contract.Ensures(Contract.Result<ArithExpr>() != null);
00958
00959 CheckContextMatch(t);
00960 return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
00961 }
00962
00966 public ArithExpr MkUnaryMinus(ArithExpr t)
00967 {
00968 Contract.Requires(t != null);
00969 Contract.Ensures(Contract.Result<ArithExpr>() != null);
00970
00971 CheckContextMatch(t);
00972 return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
00973 }
00974
00978 public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
00979 {
00980 Contract.Requires(t1 != null);
00981 Contract.Requires(t2 != null);
00982 Contract.Ensures(Contract.Result<ArithExpr>() != null);
00983
00984 CheckContextMatch(t1);
00985 CheckContextMatch(t2);
00986 return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
00987 }
00988
00993 public IntExpr MkMod(IntExpr t1, IntExpr t2)
00994 {
00995 Contract.Requires(t1 != null);
00996 Contract.Requires(t2 != null);
00997 Contract.Ensures(Contract.Result<IntExpr>() != null);
00998
00999 CheckContextMatch(t1);
01000 CheckContextMatch(t2);
01001 return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
01002 }
01003
01008 public IntExpr MkRem(IntExpr t1, IntExpr t2)
01009 {
01010 Contract.Requires(t1 != null);
01011 Contract.Requires(t2 != null);
01012 Contract.Ensures(Contract.Result<IntExpr>() != null);
01013
01014 CheckContextMatch(t1);
01015 CheckContextMatch(t2);
01016 return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
01017 }
01018
01022 public ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
01023 {
01024 Contract.Requires(t1 != null);
01025 Contract.Requires(t2 != null);
01026 Contract.Ensures(Contract.Result<ArithExpr>() != null);
01027
01028 CheckContextMatch(t1);
01029 CheckContextMatch(t2);
01030 return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
01031 }
01032
01036 public BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
01037 {
01038 Contract.Requires(t1 != null);
01039 Contract.Requires(t2 != null);
01040 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01041
01042 CheckContextMatch(t1);
01043 CheckContextMatch(t2);
01044 return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
01045 }
01046
01050 public BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
01051 {
01052 Contract.Requires(t1 != null);
01053 Contract.Requires(t2 != null);
01054 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01055
01056 CheckContextMatch(t1);
01057 CheckContextMatch(t2);
01058 return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
01059 }
01060
01064 public BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
01065 {
01066 Contract.Requires(t1 != null);
01067 Contract.Requires(t2 != null);
01068 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01069
01070 CheckContextMatch(t1);
01071 CheckContextMatch(t2);
01072 return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
01073 }
01074
01078 public BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
01079 {
01080 Contract.Requires(t1 != null);
01081 Contract.Requires(t2 != null);
01082 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01083
01084 CheckContextMatch(t1);
01085 CheckContextMatch(t2);
01086 return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
01087 }
01088
01099 public RealExpr MkInt2Real(IntExpr t)
01100 {
01101 Contract.Requires(t != null);
01102 Contract.Ensures(Contract.Result<RealExpr>() != null);
01103
01104 CheckContextMatch(t);
01105 return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
01106 }
01107
01115 public IntExpr MkReal2Int(RealExpr t)
01116 {
01117 Contract.Requires(t != null);
01118 Contract.Ensures(Contract.Result<IntExpr>() != null);
01119
01120 CheckContextMatch(t);
01121 return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
01122 }
01123
01127 public BoolExpr MkIsInteger(RealExpr t)
01128 {
01129 Contract.Requires(t != null);
01130 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01131
01132 CheckContextMatch(t);
01133 return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
01134 }
01135 #endregion
01136
01137 #region Bit-vectors
01138
01139
01140
01141
01142 public BitVecExpr MkBVNot(BitVecExpr t)
01143 {
01144 Contract.Requires(t != null);
01145 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01146
01147 CheckContextMatch(t);
01148 return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
01149 }
01150
01155 public BitVecExpr MkBVRedAND(BitVecExpr t)
01156 {
01157 Contract.Requires(t != null);
01158 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01159
01160 CheckContextMatch(t);
01161 return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
01162 }
01163
01168 public BitVecExpr MkBVRedOR(BitVecExpr t)
01169 {
01170 Contract.Requires(t != null);
01171 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01172
01173 CheckContextMatch(t);
01174 return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
01175 }
01176
01181 public BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
01182 {
01183 Contract.Requires(t1 != null);
01184 Contract.Requires(t2 != null);
01185 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01186
01187 CheckContextMatch(t1);
01188 CheckContextMatch(t2);
01189 return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
01190 }
01191
01196 public BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
01197 {
01198 Contract.Requires(t1 != null);
01199 Contract.Requires(t2 != null);
01200 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01201
01202 CheckContextMatch(t1);
01203 CheckContextMatch(t2);
01204 return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
01205 }
01206
01211 public BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
01212 {
01213 Contract.Requires(t1 != null);
01214 Contract.Requires(t2 != null);
01215 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01216
01217 CheckContextMatch(t1);
01218 CheckContextMatch(t2);
01219 return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
01220 }
01221
01226 public BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
01227 {
01228 Contract.Requires(t1 != null);
01229 Contract.Requires(t2 != null);
01230 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01231
01232 CheckContextMatch(t1);
01233 CheckContextMatch(t2);
01234 return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
01235 }
01236
01241 public BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
01242 {
01243 Contract.Requires(t1 != null);
01244 Contract.Requires(t2 != null);
01245 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01246
01247 CheckContextMatch(t1);
01248 CheckContextMatch(t2);
01249 return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
01250 }
01251
01256 public BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
01257 {
01258 Contract.Requires(t1 != null);
01259 Contract.Requires(t2 != null);
01260 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01261
01262 CheckContextMatch(t1);
01263 CheckContextMatch(t2);
01264 return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
01265 }
01266
01271 public BitVecExpr MkBVNeg(BitVecExpr t)
01272 {
01273 Contract.Requires(t != null);
01274 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01275
01276 CheckContextMatch(t);
01277 return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
01278 }
01279
01284 public BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
01285 {
01286 Contract.Requires(t1 != null);
01287 Contract.Requires(t2 != null);
01288 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01289
01290 CheckContextMatch(t1);
01291 CheckContextMatch(t2);
01292 return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
01293 }
01294
01299 public BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
01300 {
01301 Contract.Requires(t1 != null);
01302 Contract.Requires(t2 != null);
01303 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01304
01305 CheckContextMatch(t1);
01306 CheckContextMatch(t2);
01307 return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
01308 }
01309
01314 public BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
01315 {
01316 Contract.Requires(t1 != null);
01317 Contract.Requires(t2 != null);
01318 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01319
01320 CheckContextMatch(t1);
01321 CheckContextMatch(t2);
01322 return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
01323 }
01324
01334 public BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
01335 {
01336 Contract.Requires(t1 != null);
01337 Contract.Requires(t2 != null);
01338 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01339
01340 CheckContextMatch(t1);
01341 CheckContextMatch(t2);
01342 return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
01343 }
01344
01358 public BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
01359 {
01360 Contract.Requires(t1 != null);
01361 Contract.Requires(t2 != null);
01362 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01363
01364 CheckContextMatch(t1);
01365 CheckContextMatch(t2);
01366 return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
01367 }
01368
01377 public BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
01378 {
01379 Contract.Requires(t1 != null);
01380 Contract.Requires(t2 != null);
01381 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01382
01383 CheckContextMatch(t1);
01384 CheckContextMatch(t2);
01385 return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
01386 }
01387
01398 public BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
01399 {
01400 Contract.Requires(t1 != null);
01401 Contract.Requires(t2 != null);
01402 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01403
01404 CheckContextMatch(t1);
01405 CheckContextMatch(t2);
01406 return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
01407 }
01408
01416 public BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
01417 {
01418 Contract.Requires(t1 != null);
01419 Contract.Requires(t2 != null);
01420 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01421
01422 CheckContextMatch(t1);
01423 CheckContextMatch(t2);
01424 return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
01425 }
01426
01433 public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
01434 {
01435 Contract.Requires(t1 != null);
01436 Contract.Requires(t2 != null);
01437 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01438
01439 CheckContextMatch(t1);
01440 CheckContextMatch(t2);
01441 return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
01442 }
01443
01450 public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
01451 {
01452 Contract.Requires(t1 != null);
01453 Contract.Requires(t2 != null);
01454 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01455
01456 CheckContextMatch(t1);
01457 CheckContextMatch(t2);
01458 return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
01459 }
01460
01467 public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
01468 {
01469 Contract.Requires(t1 != null);
01470 Contract.Requires(t2 != null);
01471 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01472
01473 CheckContextMatch(t1);
01474 CheckContextMatch(t2);
01475 return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
01476 }
01477
01484 public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
01485 {
01486 Contract.Requires(t1 != null);
01487 Contract.Requires(t2 != null);
01488 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01489
01490 CheckContextMatch(t1);
01491 CheckContextMatch(t2);
01492 return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
01493 }
01494
01501 public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
01502 {
01503 Contract.Requires(t1 != null);
01504 Contract.Requires(t2 != null);
01505 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01506
01507 CheckContextMatch(t1);
01508 CheckContextMatch(t2);
01509 return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
01510 }
01511
01518 public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
01519 {
01520 Contract.Requires(t1 != null);
01521 Contract.Requires(t2 != null);
01522 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01523
01524 CheckContextMatch(t1);
01525 CheckContextMatch(t2);
01526 return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
01527 }
01528
01535 public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
01536 {
01537 Contract.Requires(t1 != null);
01538 Contract.Requires(t2 != null);
01539 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01540
01541 CheckContextMatch(t1);
01542 CheckContextMatch(t2);
01543 return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
01544 }
01545
01552 public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
01553 {
01554 Contract.Requires(t1 != null);
01555 Contract.Requires(t2 != null);
01556 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01557
01558 CheckContextMatch(t1);
01559 CheckContextMatch(t2);
01560 return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
01561 }
01562
01573 public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
01574 {
01575 Contract.Requires(t1 != null);
01576 Contract.Requires(t2 != null);
01577 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01578
01579 CheckContextMatch(t1);
01580 CheckContextMatch(t2);
01581 return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
01582 }
01583
01593 public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
01594 {
01595 Contract.Requires(t != null);
01596 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01597
01598 CheckContextMatch(t);
01599 return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
01600 }
01601
01610 public BitVecExpr MkSignExt(uint i, BitVecExpr t)
01611 {
01612 Contract.Requires(t != null);
01613 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01614
01615 CheckContextMatch(t);
01616 return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
01617 }
01618
01628 public BitVecExpr MkZeroExt(uint i, BitVecExpr t)
01629 {
01630 Contract.Requires(t != null);
01631 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01632
01633 CheckContextMatch(t);
01634 return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
01635 }
01636
01643 public BitVecExpr MkRepeat(uint i, BitVecExpr t)
01644 {
01645 Contract.Requires(t != null);
01646 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01647
01648 CheckContextMatch(t);
01649 return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
01650 }
01651
01664 public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
01665 {
01666 Contract.Requires(t1 != null);
01667 Contract.Requires(t2 != null);
01668 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01669
01670 CheckContextMatch(t1);
01671 CheckContextMatch(t2);
01672 return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
01673 }
01674
01687 public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
01688 {
01689 Contract.Requires(t1 != null);
01690 Contract.Requires(t2 != null);
01691 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01692
01693 CheckContextMatch(t1);
01694 CheckContextMatch(t2);
01695 return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
01696 }
01697
01712 public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
01713 {
01714 Contract.Requires(t1 != null);
01715 Contract.Requires(t2 != null);
01716 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01717
01718 CheckContextMatch(t1);
01719 CheckContextMatch(t2);
01720 return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
01721 }
01722
01730 public BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
01731 {
01732 Contract.Requires(t != null);
01733 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01734
01735 CheckContextMatch(t);
01736 return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
01737 }
01738
01746 public BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
01747 {
01748 Contract.Requires(t != null);
01749 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01750
01751 CheckContextMatch(t);
01752 return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
01753 }
01754
01762 public BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
01763 {
01764 Contract.Requires(t1 != null);
01765 Contract.Requires(t2 != null);
01766 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01767
01768 CheckContextMatch(t1);
01769 CheckContextMatch(t2);
01770 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
01771 }
01772
01780 public BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
01781 {
01782 Contract.Requires(t1 != null);
01783 Contract.Requires(t2 != null);
01784 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01785
01786 CheckContextMatch(t1);
01787 CheckContextMatch(t2);
01788 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
01789 }
01790
01801 public BitVecExpr MkInt2BV(uint n, IntExpr t)
01802 {
01803 Contract.Requires(t != null);
01804 Contract.Ensures(Contract.Result<BitVecExpr>() != null);
01805
01806 CheckContextMatch(t);
01807 return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
01808 }
01809
01825 public IntExpr MkBV2Int(BitVecExpr t, bool signed)
01826 {
01827 Contract.Requires(t != null);
01828 Contract.Ensures(Contract.Result<IntExpr>() != null);
01829
01830 CheckContextMatch(t);
01831 return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
01832 }
01833
01840 public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
01841 {
01842 Contract.Requires(t1 != null);
01843 Contract.Requires(t2 != null);
01844 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01845
01846 CheckContextMatch(t1);
01847 CheckContextMatch(t2);
01848 return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
01849 }
01850
01857 public BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
01858 {
01859 Contract.Requires(t1 != null);
01860 Contract.Requires(t2 != null);
01861 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01862
01863 CheckContextMatch(t1);
01864 CheckContextMatch(t2);
01865 return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
01866 }
01867
01874 public BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
01875 {
01876 Contract.Requires(t1 != null);
01877 Contract.Requires(t2 != null);
01878 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01879
01880 CheckContextMatch(t1);
01881 CheckContextMatch(t2);
01882 return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
01883 }
01884
01891 public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
01892 {
01893 Contract.Requires(t1 != null);
01894 Contract.Requires(t2 != null);
01895 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01896
01897 CheckContextMatch(t1);
01898 CheckContextMatch(t2);
01899 return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
01900 }
01901
01908 public BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
01909 {
01910 Contract.Requires(t1 != null);
01911 Contract.Requires(t2 != null);
01912 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01913
01914 CheckContextMatch(t1);
01915 CheckContextMatch(t2);
01916 return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
01917 }
01918
01925 public BoolExpr MkBVNegNoOverflow(BitVecExpr t)
01926 {
01927 Contract.Requires(t != null);
01928 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01929
01930 CheckContextMatch(t);
01931 return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
01932 }
01933
01940 public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
01941 {
01942 Contract.Requires(t1 != null);
01943 Contract.Requires(t2 != null);
01944 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01945
01946 CheckContextMatch(t1);
01947 CheckContextMatch(t2);
01948 return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
01949 }
01950
01957 public BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
01958 {
01959 Contract.Requires(t1 != null);
01960 Contract.Requires(t2 != null);
01961 Contract.Ensures(Contract.Result<BoolExpr>() != null);
01962
01963 CheckContextMatch(t1);
01964 CheckContextMatch(t2);
01965 return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
01966 }
01967 #endregion
01968
01969 #region Arrays
01970
01971
01972
01973 public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
01974 {
01975 Contract.Requires(name != null);
01976 Contract.Requires(domain != null);
01977 Contract.Requires(range != null);
01978 Contract.Ensures(Contract.Result<ArrayExpr>() != null);
01979
01980 return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
01981 }
01982
01986 public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
01987 {
01988 Contract.Requires(domain != null);
01989 Contract.Requires(range != null);
01990 Contract.Ensures(Contract.Result<ArrayExpr>() != null);
01991
01992 return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
01993 }
01994
02008 public Expr MkSelect(ArrayExpr a, Expr i)
02009 {
02010 Contract.Requires(a != null);
02011 Contract.Requires(i != null);
02012 Contract.Ensures(Contract.Result<Expr>() != null);
02013
02014 CheckContextMatch(a);
02015 CheckContextMatch(i);
02016 return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
02017 }
02018
02036 public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
02037 {
02038 Contract.Requires(a != null);
02039 Contract.Requires(i != null);
02040 Contract.Requires(v != null);
02041 Contract.Ensures(Contract.Result<ArrayExpr>() != null);
02042
02043 CheckContextMatch(a);
02044 CheckContextMatch(i);
02045 CheckContextMatch(v);
02046 return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
02047 }
02048
02058 public ArrayExpr MkConstArray(Sort domain, Expr v)
02059 {
02060 Contract.Requires(domain != null);
02061 Contract.Requires(v != null);
02062 Contract.Ensures(Contract.Result<ArrayExpr>() != null);
02063
02064 CheckContextMatch(domain);
02065 CheckContextMatch(v);
02066 return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
02067 }
02068
02080 public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
02081 {
02082 Contract.Requires(f != null);
02083 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
02084 Contract.Ensures(Contract.Result<ArrayExpr>() != null);
02085
02086 CheckContextMatch(f);
02087 CheckContextMatch(args);
02088 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
02089 }
02090
02098 public Expr MkTermArray(ArrayExpr array)
02099 {
02100 Contract.Requires(array != null);
02101 Contract.Ensures(Contract.Result<Expr>() != null);
02102
02103 CheckContextMatch(array);
02104 return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
02105 }
02106 #endregion
02107
02108 #region Sets
02109
02110
02111
02112 public SetSort MkSetSort(Sort ty)
02113 {
02114 Contract.Requires(ty != null);
02115 Contract.Ensures(Contract.Result<SetSort>() != null);
02116
02117 CheckContextMatch(ty);
02118 return new SetSort(this, ty);
02119 }
02120
02124 public Expr MkEmptySet(Sort domain)
02125 {
02126 Contract.Requires(domain != null);
02127 Contract.Ensures(Contract.Result<Expr>() != null);
02128
02129 CheckContextMatch(domain);
02130 return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
02131 }
02132
02136 public Expr MkFullSet(Sort domain)
02137 {
02138 Contract.Requires(domain != null);
02139 Contract.Ensures(Contract.Result<Expr>() != null);
02140
02141 CheckContextMatch(domain);
02142 return Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
02143 }
02144
02148 public Expr MkSetAdd(Expr set, Expr element)
02149 {
02150 Contract.Requires(set != null);
02151 Contract.Requires(element != null);
02152 Contract.Ensures(Contract.Result<Expr>() != null);
02153
02154 CheckContextMatch(set);
02155 CheckContextMatch(element);
02156 return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
02157 }
02158
02159
02163 public Expr MkSetDel(Expr set, Expr element)
02164 {
02165 Contract.Requires(set != null);
02166 Contract.Requires(element != null);
02167 Contract.Ensures(Contract.Result<Expr>() != null);
02168
02169 CheckContextMatch(set);
02170 CheckContextMatch(element);
02171 return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
02172 }
02173
02177 public Expr MkSetUnion(params Expr[] args)
02178 {
02179 Contract.Requires(args != null);
02180 Contract.Requires(Contract.ForAll(args, a => a != null));
02181
02182 CheckContextMatch(args);
02183 return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
02184 }
02185
02189 public Expr MkSetIntersection(params Expr[] args)
02190 {
02191 Contract.Requires(args != null);
02192 Contract.Requires(Contract.ForAll(args, a => a != null));
02193 Contract.Ensures(Contract.Result<Expr>() != null);
02194
02195 CheckContextMatch(args);
02196 return Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
02197 }
02198
02202 public Expr MkSetDifference(Expr arg1, Expr arg2)
02203 {
02204 Contract.Requires(arg1 != null);
02205 Contract.Requires(arg2 != null);
02206 Contract.Ensures(Contract.Result<Expr>() != null);
02207
02208 CheckContextMatch(arg1);
02209 CheckContextMatch(arg2);
02210 return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
02211 }
02212
02216 public Expr MkSetComplement(Expr arg)
02217 {
02218 Contract.Requires(arg != null);
02219 Contract.Ensures(Contract.Result<Expr>() != null);
02220
02221 CheckContextMatch(arg);
02222 return Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
02223 }
02224
02228 public Expr MkSetMembership(Expr elem, Expr set)
02229 {
02230 Contract.Requires(elem != null);
02231 Contract.Requires(set != null);
02232 Contract.Ensures(Contract.Result<Expr>() != null);
02233
02234 CheckContextMatch(elem);
02235 CheckContextMatch(set);
02236 return Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
02237 }
02238
02242 public Expr MkSetSubset(Expr arg1, Expr arg2)
02243 {
02244 Contract.Requires(arg1 != null);
02245 Contract.Requires(arg2 != null);
02246 Contract.Ensures(Contract.Result<Expr>() != null);
02247
02248 CheckContextMatch(arg1);
02249 CheckContextMatch(arg2);
02250 return Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
02251 }
02252 #endregion
02253
02254 #region Numerals
02255
02256 #region General Numerals
02257
02258
02259
02260
02261
02262
02263 public Expr MkNumeral(string v, Sort ty)
02264 {
02265 Contract.Requires(ty != null);
02266 Contract.Ensures(Contract.Result<Expr>() != null);
02267
02268 CheckContextMatch(ty);
02269 return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
02270 }
02271
02279 public Expr MkNumeral(int v, Sort ty)
02280 {
02281 Contract.Requires(ty != null);
02282 Contract.Ensures(Contract.Result<Expr>() != null);
02283
02284 CheckContextMatch(ty);
02285 return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
02286 }
02287
02295 public Expr MkNumeral(uint v, Sort ty)
02296 {
02297 Contract.Requires(ty != null);
02298 Contract.Ensures(Contract.Result<Expr>() != null);
02299
02300 CheckContextMatch(ty);
02301 return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
02302 }
02303
02311 public Expr MkNumeral(long v, Sort ty)
02312 {
02313 Contract.Requires(ty != null);
02314 Contract.Ensures(Contract.Result<Expr>() != null);
02315
02316 CheckContextMatch(ty);
02317 return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
02318 }
02319
02327 public Expr MkNumeral(ulong v, Sort ty)
02328 {
02329 Contract.Requires(ty != null);
02330 Contract.Ensures(Contract.Result<Expr>() != null);
02331
02332 CheckContextMatch(ty);
02333 return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
02334 }
02335 #endregion
02336
02337 #region Reals
02338
02339
02340
02341
02342
02343
02344
02345 public RatNum MkReal(int num, int den)
02346 {
02347 if (den == 0)
02348 throw new Z3Exception("Denominator is zero");
02349
02350 Contract.Ensures(Contract.Result<RatNum>() != null);
02351 Contract.EndContractBlock();
02352
02353 return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
02354 }
02355
02361 public RatNum MkReal(string v)
02362 {
02363 Contract.Ensures(Contract.Result<RatNum>() != null);
02364
02365 return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
02366 }
02367
02373 public RatNum MkReal(int v)
02374 {
02375 Contract.Ensures(Contract.Result<RatNum>() != null);
02376
02377 return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
02378 }
02379
02385 public RatNum MkReal(uint v)
02386 {
02387 Contract.Ensures(Contract.Result<RatNum>() != null);
02388
02389 return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
02390 }
02391
02397 public RatNum MkReal(long v)
02398 {
02399 Contract.Ensures(Contract.Result<RatNum>() != null);
02400
02401 return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
02402 }
02403
02409 public RatNum MkReal(ulong v)
02410 {
02411 Contract.Ensures(Contract.Result<RatNum>() != null);
02412
02413 return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
02414 }
02415 #endregion
02416
02417 #region Integers
02418
02419
02420
02421
02422 public IntNum MkInt(string v)
02423 {
02424 Contract.Ensures(Contract.Result<IntNum>() != null);
02425
02426 return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
02427 }
02428
02434 public IntNum MkInt(int v)
02435 {
02436 Contract.Ensures(Contract.Result<IntNum>() != null);
02437
02438 return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
02439 }
02440
02446 public IntNum MkInt(uint v)
02447 {
02448 Contract.Ensures(Contract.Result<IntNum>() != null);
02449
02450 return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
02451 }
02452
02458 public IntNum MkInt(long v)
02459 {
02460 Contract.Ensures(Contract.Result<IntNum>() != null);
02461
02462 return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
02463 }
02464
02470 public IntNum MkInt(ulong v)
02471 {
02472 Contract.Ensures(Contract.Result<IntNum>() != null);
02473
02474 return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
02475 }
02476 #endregion
02477
02478 #region Bit-vectors
02479
02480
02481
02482
02483
02484 public BitVecNum MkBV(string v, uint size)
02485 {
02486 Contract.Ensures(Contract.Result<BitVecNum>() != null);
02487
02488 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
02489 }
02490
02496 public BitVecNum MkBV(int v, uint size)
02497 {
02498 Contract.Ensures(Contract.Result<BitVecNum>() != null);
02499
02500 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
02501 }
02502
02508 public BitVecNum MkBV(uint v, uint size)
02509 {
02510 Contract.Ensures(Contract.Result<BitVecNum>() != null);
02511
02512 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
02513 }
02514
02520 public BitVecNum MkBV(long v, uint size)
02521 {
02522 Contract.Ensures(Contract.Result<BitVecNum>() != null);
02523
02524 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
02525 }
02526
02532 public BitVecNum MkBV(ulong v, uint size)
02533 {
02534 Contract.Ensures(Contract.Result<BitVecNum>() != null);
02535
02536 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
02537 }
02538 #endregion
02539
02540 #endregion // Numerals
02541
02542 #region Quantifiers
02543
02544
02545
02546
02547
02548
02549
02550
02551
02552
02553
02554
02555
02556
02557
02558
02559
02560
02561
02562 public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
02563 {
02564 Contract.Requires(sorts != null);
02565 Contract.Requires(names != null);
02566 Contract.Requires(body != null);
02567 Contract.Requires(sorts.Length == names.Length);
02568 Contract.Requires(Contract.ForAll(sorts, s => s != null));
02569 Contract.Requires(Contract.ForAll(names, n => n != null));
02570 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
02571 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
02572
02573 Contract.Ensures(Contract.Result<Quantifier>() != null);
02574
02575 return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
02576 }
02577
02578
02582 public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
02583 {
02584 Contract.Requires(body != null);
02585 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
02586 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
02587 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
02588
02589 Contract.Ensures(Contract.Result<Quantifier>() != null);
02590
02591 return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
02592 }
02593
02598 public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
02599 {
02600 Contract.Requires(sorts != null);
02601 Contract.Requires(names != null);
02602 Contract.Requires(body != null);
02603 Contract.Requires(sorts.Length == names.Length);
02604 Contract.Requires(Contract.ForAll(sorts, s => s != null));
02605 Contract.Requires(Contract.ForAll(names, n => n != null));
02606 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
02607 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
02608 Contract.Ensures(Contract.Result<Quantifier>() != null);
02609
02610 return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
02611 }
02612
02616 public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
02617 {
02618 Contract.Requires(body != null);
02619 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
02620 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
02621 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
02622 Contract.Ensures(Contract.Result<Quantifier>() != null);
02623
02624 return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
02625 }
02626
02627
02631 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)
02632 {
02633 Contract.Requires(body != null);
02634 Contract.Requires(names != null);
02635 Contract.Requires(sorts != null);
02636 Contract.Requires(sorts.Length == names.Length);
02637 Contract.Requires(Contract.ForAll(sorts, s => s != null));
02638 Contract.Requires(Contract.ForAll(names, n => n != null));
02639 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
02640 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
02641
02642 Contract.Ensures(Contract.Result<Quantifier>() != null);
02643
02644 if (universal)
02645 return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
02646 else
02647 return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
02648 }
02649
02650
02654 public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
02655 {
02656 Contract.Requires(body != null);
02657 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
02658 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
02659 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
02660
02661 Contract.Ensures(Contract.Result<Quantifier>() != null);
02662
02663 if (universal)
02664 return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
02665 else
02666 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
02667 }
02668
02669 #endregion
02670
02671 #endregion // Expr
02672
02673 #region Options
02674
02675
02676
02677
02678
02679
02680
02681
02682
02683
02684
02685
02686
02687
02688
02689
02690 public Z3_ast_print_mode PrintMode
02691 {
02692 set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
02693 }
02694 #endregion
02695
02696 #region SMT Files & Strings
02697
02698
02699
02700
02701
02702
02703
02704
02705
02706
02707 public string BenchmarkToSMTString(string name, string logic, string status, string attributes,
02708 BoolExpr[] assumptions, BoolExpr formula)
02709 {
02710 Contract.Requires(assumptions != null);
02711 Contract.Requires(formula != null);
02712 Contract.Ensures(Contract.Result<string>() != null);
02713
02714 return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
02715 (uint)assumptions.Length, AST.ArrayToNative(assumptions),
02716 formula.NativeObject);
02717 }
02718
02729 public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
02730 {
02731 uint csn = Symbol.ArrayLength(sortNames);
02732 uint cs = Sort.ArrayLength(sorts);
02733 uint cdn = Symbol.ArrayLength(declNames);
02734 uint cd = AST.ArrayLength(decls);
02735 if (csn != cs || cdn != cd)
02736 throw new Z3Exception("Argument size mismatch");
02737 Native.Z3_parse_smtlib_string(nCtx, str,
02738 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
02739 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
02740 }
02741
02746 public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
02747 {
02748 uint csn = Symbol.ArrayLength(sortNames);
02749 uint cs = Sort.ArrayLength(sorts);
02750 uint cdn = Symbol.ArrayLength(declNames);
02751 uint cd = AST.ArrayLength(decls);
02752 if (csn != cs || cdn != cd)
02753 throw new Z3Exception("Argument size mismatch");
02754 Native.Z3_parse_smtlib_file(nCtx, fileName,
02755 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
02756 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
02757 }
02758
02762 public uint NumSMTLIBFormulas { get { return Native.Z3_get_smtlib_num_formulas(nCtx); } }
02763
02767 public BoolExpr[] SMTLIBFormulas
02768 {
02769 get
02770 {
02771 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
02772
02773 uint n = NumSMTLIBFormulas;
02774 BoolExpr[] res = new BoolExpr[n];
02775 for (uint i = 0; i < n; i++)
02776 res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_formula(nCtx, i));
02777 return res;
02778 }
02779 }
02780
02784 public uint NumSMTLIBAssumptions { get { return Native.Z3_get_smtlib_num_assumptions(nCtx); } }
02785
02789 public BoolExpr[] SMTLIBAssumptions
02790 {
02791 get
02792 {
02793 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
02794
02795 uint n = NumSMTLIBAssumptions;
02796 BoolExpr[] res = new BoolExpr[n];
02797 for (uint i = 0; i < n; i++)
02798 res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_assumption(nCtx, i));
02799 return res;
02800 }
02801 }
02802
02806 public uint NumSMTLIBDecls { get { return Native.Z3_get_smtlib_num_decls(nCtx); } }
02807
02811 public FuncDecl[] SMTLIBDecls
02812 {
02813 get
02814 {
02815 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
02816
02817 uint n = NumSMTLIBDecls;
02818 FuncDecl[] res = new FuncDecl[n];
02819 for (uint i = 0; i < n; i++)
02820 res[i] = new FuncDecl(this, Native.Z3_get_smtlib_decl(nCtx, i));
02821 return res;
02822 }
02823 }
02824
02828 public uint NumSMTLIBSorts { get { return Native.Z3_get_smtlib_num_sorts(nCtx); } }
02829
02833 public Sort[] SMTLIBSorts
02834 {
02835 get
02836 {
02837 Contract.Ensures(Contract.Result<Sort[]>() != null);
02838
02839 uint n = NumSMTLIBSorts;
02840 Sort[] res = new Sort[n];
02841 for (uint i = 0; i < n; i++)
02842 res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i));
02843 return res;
02844 }
02845 }
02846
02852 public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
02853 {
02854 Contract.Ensures(Contract.Result<BoolExpr>() != null);
02855
02856 uint csn = Symbol.ArrayLength(sortNames);
02857 uint cs = Sort.ArrayLength(sorts);
02858 uint cdn = Symbol.ArrayLength(declNames);
02859 uint cd = AST.ArrayLength(decls);
02860 if (csn != cs || cdn != cd)
02861 throw new Z3Exception("Argument size mismatch");
02862 return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
02863 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
02864 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
02865 }
02866
02871 public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
02872 {
02873 Contract.Ensures(Contract.Result<BoolExpr>() != null);
02874
02875 uint csn = Symbol.ArrayLength(sortNames);
02876 uint cs = Sort.ArrayLength(sorts);
02877 uint cdn = Symbol.ArrayLength(declNames);
02878 uint cd = AST.ArrayLength(decls);
02879 if (csn != cs || cdn != cd)
02880 throw new Z3Exception("Argument size mismatch");
02881 return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
02882 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
02883 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
02884 }
02885 #endregion
02886
02887 #region Goals
02888
02889
02890
02891
02892
02893
02894
02895
02896
02897
02898 public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
02899 {
02900 Contract.Ensures(Contract.Result<Goal>() != null);
02901
02902 return new Goal(this, models, unsatCores, proofs);
02903 }
02904 #endregion
02905
02906 #region ParameterSets
02907
02908
02909
02910 public Params MkParams()
02911 {
02912 Contract.Ensures(Contract.Result<Params>() != null);
02913
02914 return new Params(this);
02915 }
02916 #endregion
02917
02918 #region Tactics
02919
02920
02921
02922 public uint NumTactics
02923 {
02924 get { return Native.Z3_get_num_tactics(nCtx); }
02925 }
02926
02930 public string[] TacticNames
02931 {
02932 get
02933 {
02934 Contract.Ensures(Contract.Result<string[]>() != null);
02935
02936 uint n = NumTactics;
02937 string[] res = new string[n];
02938 for (uint i = 0; i < n; i++)
02939 res[i] = Native.Z3_get_tactic_name(nCtx, i);
02940 return res;
02941 }
02942 }
02943
02947 public string TacticDescription(string name)
02948 {
02949 Contract.Ensures(Contract.Result<string>() != null);
02950
02951 return Native.Z3_tactic_get_descr(nCtx, name);
02952 }
02953
02957 public Tactic MkTactic(string name)
02958 {
02959 Contract.Ensures(Contract.Result<Tactic>() != null);
02960
02961 return new Tactic(this, name);
02962 }
02963
02968 public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
02969 {
02970 Contract.Requires(t1 != null);
02971 Contract.Requires(t2 != null);
02972 Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
02973 Contract.Ensures(Contract.Result<Tactic>() != null);
02974
02975
02976 CheckContextMatch(t1);
02977 CheckContextMatch(t2);
02978 CheckContextMatch(ts);
02979
02980 IntPtr last = IntPtr.Zero;
02981 if (ts != null && ts.Length > 0)
02982 {
02983 last = ts[ts.Length - 1].NativeObject;
02984 for (int i = ts.Length - 2; i >= 0; i--)
02985 last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
02986 }
02987 if (last != IntPtr.Zero)
02988 {
02989 last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
02990 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
02991 }
02992 else
02993 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
02994 }
02995
03003 public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
03004 {
03005 Contract.Requires(t1 != null);
03006 Contract.Requires(t2 != null);
03007 Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
03008 Contract.Ensures(Contract.Result<Tactic>() != null);
03009
03010 return AndThen(t1, t2, ts);
03011 }
03012
03017 public Tactic OrElse(Tactic t1, Tactic t2)
03018 {
03019 Contract.Requires(t1 != null);
03020 Contract.Requires(t2 != null);
03021 Contract.Ensures(Contract.Result<Tactic>() != null);
03022
03023 CheckContextMatch(t1);
03024 CheckContextMatch(t2);
03025 return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
03026 }
03027
03034 public Tactic TryFor(Tactic t, uint ms)
03035 {
03036 Contract.Requires(t != null);
03037 Contract.Ensures(Contract.Result<Tactic>() != null);
03038
03039 CheckContextMatch(t);
03040 return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
03041 }
03042
03050 public Tactic When(Probe p, Tactic t)
03051 {
03052 Contract.Requires(p != null);
03053 Contract.Requires(t != null);
03054 Contract.Ensures(Contract.Result<Tactic>() != null);
03055
03056 CheckContextMatch(t);
03057 CheckContextMatch(p);
03058 return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
03059 }
03060
03065 public Tactic Cond(Probe p, Tactic t1, Tactic t2)
03066 {
03067 Contract.Requires(p != null);
03068 Contract.Requires(t1 != null);
03069 Contract.Requires(t2 != null);
03070 Contract.Ensures(Contract.Result<Tactic>() != null);
03071
03072 CheckContextMatch(p);
03073 CheckContextMatch(t1);
03074 CheckContextMatch(t2);
03075 return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
03076 }
03077
03082 public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
03083 {
03084 Contract.Requires(t != null);
03085 Contract.Ensures(Contract.Result<Tactic>() != null);
03086
03087 CheckContextMatch(t);
03088 return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
03089 }
03090
03094 public Tactic Skip()
03095 {
03096 Contract.Ensures(Contract.Result<Tactic>() != null);
03097
03098 return new Tactic(this, Native.Z3_tactic_skip(nCtx));
03099 }
03100
03104 public Tactic Fail()
03105 {
03106 Contract.Ensures(Contract.Result<Tactic>() != null);
03107
03108 return new Tactic(this, Native.Z3_tactic_fail(nCtx));
03109 }
03110
03114 public Tactic FailIf(Probe p)
03115 {
03116 Contract.Requires(p != null);
03117 Contract.Ensures(Contract.Result<Tactic>() != null);
03118
03119 CheckContextMatch(p);
03120 return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
03121 }
03122
03127 public Tactic FailIfNotDecided()
03128 {
03129 Contract.Ensures(Contract.Result<Tactic>() != null);
03130
03131 return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
03132 }
03133
03137 public Tactic UsingParams(Tactic t, Params p)
03138 {
03139 Contract.Requires(t != null);
03140 Contract.Requires(p != null);
03141 Contract.Ensures(Contract.Result<Tactic>() != null);
03142
03143 CheckContextMatch(t);
03144 CheckContextMatch(p);
03145 return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
03146 }
03147
03152 public Tactic With(Tactic t, Params p)
03153 {
03154 Contract.Requires(t != null);
03155 Contract.Requires(p != null);
03156 Contract.Ensures(Contract.Result<Tactic>() != null);
03157
03158 return UsingParams(t, p);
03159 }
03160
03164 public Tactic ParOr(params Tactic[] t)
03165 {
03166 Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
03167 Contract.Ensures(Contract.Result<Tactic>() != null);
03168
03169 CheckContextMatch(t);
03170 return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
03171 }
03172
03177 public Tactic ParAndThen(Tactic t1, Tactic t2)
03178 {
03179 Contract.Requires(t1 != null);
03180 Contract.Requires(t2 != null);
03181 Contract.Ensures(Contract.Result<Tactic>() != null);
03182
03183 CheckContextMatch(t1);
03184 CheckContextMatch(t2);
03185 return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
03186 }
03187
03192 public void Interrupt()
03193 {
03194 Native.Z3_interrupt(nCtx);
03195 }
03196 #endregion
03197
03198 #region Probes
03199
03200
03201
03202 public uint NumProbes
03203 {
03204 get { return Native.Z3_get_num_probes(nCtx); }
03205 }
03206
03210 public string[] ProbeNames
03211 {
03212 get
03213 {
03214 Contract.Ensures(Contract.Result<string[]>() != null);
03215
03216 uint n = NumProbes;
03217 string[] res = new string[n];
03218 for (uint i = 0; i < n; i++)
03219 res[i] = Native.Z3_get_probe_name(nCtx, i);
03220 return res;
03221 }
03222 }
03223
03227 public string ProbeDescription(string name)
03228 {
03229 Contract.Ensures(Contract.Result<string>() != null);
03230
03231 return Native.Z3_probe_get_descr(nCtx, name);
03232 }
03233
03237 public Probe MkProbe(string name)
03238 {
03239 Contract.Ensures(Contract.Result<Probe>() != null);
03240
03241 return new Probe(this, name);
03242 }
03243
03247 public Probe ConstProbe(double val)
03248 {
03249 Contract.Ensures(Contract.Result<Probe>() != null);
03250
03251 return new Probe(this, Native.Z3_probe_const(nCtx, val));
03252 }
03253
03258 public Probe Lt(Probe p1, Probe p2)
03259 {
03260 Contract.Requires(p1 != null);
03261 Contract.Requires(p2 != null);
03262 Contract.Ensures(Contract.Result<Probe>() != null);
03263
03264 CheckContextMatch(p1);
03265 CheckContextMatch(p2);
03266 return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
03267 }
03268
03273 public Probe Gt(Probe p1, Probe p2)
03274 {
03275 Contract.Requires(p1 != null);
03276 Contract.Requires(p2 != null);
03277 Contract.Ensures(Contract.Result<Probe>() != null);
03278
03279 CheckContextMatch(p1);
03280 CheckContextMatch(p2);
03281 return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
03282 }
03283
03288 public Probe Le(Probe p1, Probe p2)
03289 {
03290 Contract.Requires(p1 != null);
03291 Contract.Requires(p2 != null);
03292 Contract.Ensures(Contract.Result<Probe>() != null);
03293
03294 CheckContextMatch(p1);
03295 CheckContextMatch(p2);
03296 return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
03297 }
03298
03303 public Probe Ge(Probe p1, Probe p2)
03304 {
03305 Contract.Requires(p1 != null);
03306 Contract.Requires(p2 != null);
03307 Contract.Ensures(Contract.Result<Probe>() != null);
03308
03309 CheckContextMatch(p1);
03310 CheckContextMatch(p2);
03311 return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
03312 }
03313
03318 public Probe Eq(Probe p1, Probe p2)
03319 {
03320 Contract.Requires(p1 != null);
03321 Contract.Requires(p2 != null);
03322 Contract.Ensures(Contract.Result<Probe>() != null);
03323
03324 CheckContextMatch(p1);
03325 CheckContextMatch(p2);
03326 return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
03327 }
03328
03333 public Probe And(Probe p1, Probe p2)
03334 {
03335 Contract.Requires(p1 != null);
03336 Contract.Requires(p2 != null);
03337 Contract.Ensures(Contract.Result<Probe>() != null);
03338
03339 CheckContextMatch(p1);
03340 CheckContextMatch(p2);
03341 return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
03342 }
03343
03348 public Probe Or(Probe p1, Probe p2)
03349 {
03350 Contract.Requires(p1 != null);
03351 Contract.Requires(p2 != null);
03352 Contract.Ensures(Contract.Result<Probe>() != null);
03353
03354 CheckContextMatch(p1);
03355 CheckContextMatch(p2);
03356 return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
03357 }
03358
03363 public Probe Not(Probe p)
03364 {
03365 Contract.Requires(p != null);
03366 Contract.Ensures(Contract.Result<Probe>() != null);
03367
03368 CheckContextMatch(p);
03369 return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
03370 }
03371 #endregion
03372
03373 #region Solvers
03374
03375
03376
03377
03378
03379
03380
03381
03382 public Solver MkSolver(Symbol logic = null)
03383 {
03384 Contract.Ensures(Contract.Result<Solver>() != null);
03385
03386 if (logic == null)
03387 return new Solver(this, Native.Z3_mk_solver(nCtx));
03388 else
03389 return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
03390 }
03391
03396 public Solver MkSolver(string logic)
03397 {
03398 Contract.Ensures(Contract.Result<Solver>() != null);
03399
03400 return MkSolver(MkSymbol(logic));
03401 }
03402
03406 public Solver MkSimpleSolver()
03407 {
03408 Contract.Ensures(Contract.Result<Solver>() != null);
03409
03410 return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
03411 }
03412
03420 public Solver MkSolver(Tactic t)
03421 {
03422 Contract.Requires(t != null);
03423 Contract.Ensures(Contract.Result<Solver>() != null);
03424
03425 return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
03426 }
03427 #endregion
03428
03429 #region Fixedpoints
03430
03431
03432
03433 public Fixedpoint MkFixedpoint()
03434 {
03435 Contract.Ensures(Contract.Result<Fixedpoint>() != null);
03436
03437 return new Fixedpoint(this);
03438 }
03439 #endregion
03440
03441
03442 #region Miscellaneous
03443
03444
03445
03446
03447
03448
03449
03450
03451
03452
03453 public AST WrapAST(IntPtr nativeObject)
03454 {
03455 Contract.Ensures(Contract.Result<AST>() != null);
03456 return AST.Create(this, nativeObject);
03457 }
03458
03470 public IntPtr UnwrapAST(AST a)
03471 {
03472 return a.NativeObject;
03473 }
03474
03478 public string SimplifyHelp()
03479 {
03480 Contract.Ensures(Contract.Result<string>() != null);
03481
03482 return Native.Z3_simplify_get_help(nCtx);
03483 }
03484
03488 public ParamDescrs SimplifyParameterDescriptions
03489 {
03490 get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
03491 }
03492
03498 public static void ToggleWarningMessages(bool enabled)
03499 {
03500 Native.Z3_toggle_warning_messages((enabled) ? 1 : 0);
03501 }
03502 #endregion
03503
03504 #region Error Handling
03505
03506
03507
03508
03509
03510
03511
03512
03513
03517
03518 #endregion
03519
03520 #region Parameters
03521
03522
03523
03524
03525
03526
03527
03528
03529
03530 public void UpdateParamValue(string id, string value)
03531 {
03532 Native.Z3_update_param_value(nCtx, id, value);
03533 }
03534
03535 #endregion
03536
03537 #region Internal
03538 internal IntPtr m_ctx = IntPtr.Zero;
03539 internal Native.Z3_error_handler m_n_err_handler = null;
03540 internal IntPtr nCtx { get { return m_ctx; } }
03541
03542 internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
03543 {
03544
03545 }
03546
03547 internal void InitContext()
03548 {
03549 PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
03550 m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler);
03551 Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
03552 GC.SuppressFinalize(this);
03553 }
03554
03555 [Pure]
03556 internal void CheckContextMatch(Z3Object other)
03557 {
03558 Contract.Requires(other != null);
03559
03560 if (!ReferenceEquals(this, other.Context))
03561 throw new Z3Exception("Context mismatch");
03562 }
03563
03564 [Pure]
03565 internal void CheckContextMatch(Z3Object[] arr)
03566 {
03567 Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
03568
03569 if (arr != null)
03570 {
03571 foreach (Z3Object a in arr)
03572 {
03573 Contract.Assert(a != null);
03574 CheckContextMatch(a);
03575 }
03576 }
03577 }
03578
03579 [ContractInvariantMethod]
03580 private void ObjectInvariant()
03581 {
03582 Contract.Invariant(m_AST_DRQ != null);
03583 Contract.Invariant(m_ASTMap_DRQ != null);
03584 Contract.Invariant(m_ASTVector_DRQ != null);
03585 Contract.Invariant(m_ApplyResult_DRQ != null);
03586 Contract.Invariant(m_FuncEntry_DRQ != null);
03587 Contract.Invariant(m_FuncInterp_DRQ != null);
03588 Contract.Invariant(m_Goal_DRQ != null);
03589 Contract.Invariant(m_Model_DRQ != null);
03590 Contract.Invariant(m_Params_DRQ != null);
03591 Contract.Invariant(m_ParamDescrs_DRQ != null);
03592 Contract.Invariant(m_Probe_DRQ != null);
03593 Contract.Invariant(m_Solver_DRQ != null);
03594 Contract.Invariant(m_Statistics_DRQ != null);
03595 Contract.Invariant(m_Tactic_DRQ != null);
03596 Contract.Invariant(m_Fixedpoint_DRQ != null);
03597 }
03598
03599 readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
03600 readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue();
03601 readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue();
03602 readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue();
03603 readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue();
03604 readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue();
03605 readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue();
03606 readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue();
03607 readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue();
03608 readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue();
03609 readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue();
03610 readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue();
03611 readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue();
03612 readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue();
03613 readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue();
03614
03615 internal AST.DecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result<AST.DecRefQueue>() != null); return m_AST_DRQ; } }
03616 internal ASTMap.DecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null); return m_ASTMap_DRQ; } }
03617 internal ASTVector.DecRefQueue ASTVector_DRQ { get { Contract.Ensures(Contract.Result<ASTVector.DecRefQueue>() != null); return m_ASTVector_DRQ; } }
03618 internal ApplyResult.DecRefQueue ApplyResult_DRQ { get { Contract.Ensures(Contract.Result<ApplyResult.DecRefQueue>() != null); return m_ApplyResult_DRQ; } }
03619 internal FuncInterp.Entry.DecRefQueue FuncEntry_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.Entry.DecRefQueue>() != null); return m_FuncEntry_DRQ; } }
03620 internal FuncInterp.DecRefQueue FuncInterp_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.DecRefQueue>() != null); return m_FuncInterp_DRQ; } }
03621 internal Goal.DecRefQueue Goal_DRQ { get { Contract.Ensures(Contract.Result<Goal.DecRefQueue>() != null); return m_Goal_DRQ; } }
03622 internal Model.DecRefQueue Model_DRQ { get { Contract.Ensures(Contract.Result<Model.DecRefQueue>() != null); return m_Model_DRQ; } }
03623 internal Params.DecRefQueue Params_DRQ { get { Contract.Ensures(Contract.Result<Params.DecRefQueue>() != null); return m_Params_DRQ; } }
03624 internal ParamDescrs.DecRefQueue ParamDescrs_DRQ { get { Contract.Ensures(Contract.Result<ParamDescrs.DecRefQueue>() != null); return m_ParamDescrs_DRQ; } }
03625 internal Probe.DecRefQueue Probe_DRQ { get { Contract.Ensures(Contract.Result<Probe.DecRefQueue>() != null); return m_Probe_DRQ; } }
03626 internal Solver.DecRefQueue Solver_DRQ { get { Contract.Ensures(Contract.Result<Solver.DecRefQueue>() != null); return m_Solver_DRQ; } }
03627 internal Statistics.DecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result<Statistics.DecRefQueue>() != null); return m_Statistics_DRQ; } }
03628 internal Tactic.DecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result<Tactic.DecRefQueue>() != null); return m_Tactic_DRQ; } }
03629 internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
03630
03631
03632 internal long refCount = 0;
03633
03637 ~Context()
03638 {
03639
03640 Dispose();
03641
03642 if (refCount == 0)
03643 {
03644 m_n_err_handler = null;
03645 Native.Z3_del_context(m_ctx);
03646 m_ctx = IntPtr.Zero;
03647 }
03648 else
03649 GC.ReRegisterForFinalize(this);
03650 }
03651
03655 public void Dispose()
03656 {
03657
03658 AST_DRQ.Clear(this);
03659 ASTMap_DRQ.Clear(this);
03660 ASTVector_DRQ.Clear(this);
03661 ApplyResult_DRQ.Clear(this);
03662 FuncEntry_DRQ.Clear(this);
03663 FuncInterp_DRQ.Clear(this);
03664 Goal_DRQ.Clear(this);
03665 Model_DRQ.Clear(this);
03666 Params_DRQ.Clear(this);
03667 ParamDescrs_DRQ.Clear(this);
03668 Probe_DRQ.Clear(this);
03669 Solver_DRQ.Clear(this);
03670 Statistics_DRQ.Clear(this);
03671 Tactic_DRQ.Clear(this);
03672 Fixedpoint_DRQ.Clear(this);
03673
03674 m_boolSort = null;
03675 m_intSort = null;
03676 m_realSort = null;
03677 }
03678 #endregion
03679 }
03680 }