Z3
src/api/dotnet/Context.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Context.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Context
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-15
00015 
00016 Notes:
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         //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
03513 
03517         //public event ErrorHandler OnError = null;
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             // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.            
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); // keep reference so it doesn't get collected.
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); // It was an assume, now we added the precondition, and we made it into an assert
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             // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
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             // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines