Context.cs

Go to the documentation of this file.

/*++
Copyright (c) 2012 Microsoft Corporation
 
Module Name:
 
    Context.cs
 
Abstract:
 
    Z3 Managed API: Context
 
Author:
 
    Christoph Wintersteiger (cwinter) 2012-03-15
 
Notes:
 
--*/
 
using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Linq;
using System.Runtime.InteropServices;
 
namespace Microsoft.Z3
{
 
    using Z3_context = System.IntPtr;
    public class Context : IDisposable
    {
        #region Constructors
        public Context()
            : base()
        {
            lock (creation_lock)
            {
                m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
                Native.Z3_enable_concurrent_dec_ref(m_ctx);
                InitContext();
            }
        }
 
        public Context(Dictionary<string, string> settings)
            : base()
        {
            Debug.Assert(settings != null);
 
            lock (creation_lock)
            {
                IntPtr cfg = Native.Z3_mk_config();
                foreach (KeyValuePair<string, string> kv in settings)
                    Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
                m_ctx = Native.Z3_mk_context_rc(cfg);
                Native.Z3_enable_concurrent_dec_ref(m_ctx);
                Native.Z3_del_config(cfg);
                InitContext();
            }
        }
 
        internal Context(Z3_context ctx)
            : base()
        {
            lock (creation_lock)
            {
                is_external = true;
                m_ctx = ctx;
                InitContext();
            }
        }
 
        bool is_external = false;
 
        #endregion
 
        #region Symbols
        public IntSymbol MkSymbol(int i)
        {
            return new IntSymbol(this, i);
        }
 
        public StringSymbol MkSymbol(string name)
        {
            return new StringSymbol(this, name);
        }
 
        internal Symbol[] MkSymbols(string[] names)
        {
            if (names == null) return new Symbol[0];
            Symbol[] result = new Symbol[names.Length];
            for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
            return result;
        }
        #endregion
 
        #region Sorts
        private BoolSort m_boolSort = null;
        private IntSort m_intSort = null;
        private RealSort m_realSort = null;
        private ComplexSort m_complexSort = null;
        private SeqSort m_stringSort = null;
        private CharSort m_charSort = null;
 
        public BoolSort BoolSort
        {
            get
            {
                if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
            }
        }
 
        public IntSort IntSort
        {
            get
            {
                if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
            }
        }
 
 
        public RealSort RealSort
        {
            get
            {
                if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
            }
        }
 
        public ComplexSort ComplexSort
        {
            get
            {
                if (m_complexSort == null) m_complexSort = new ComplexSort(this);
                return m_complexSort;
            }
        }
 
        public CharSort CharSort
        {
            get
            {
                if (m_charSort == null) m_charSort = new CharSort(this); return m_charSort;
            }
        }
 
 
        public SeqSort StringSort
        {
            get
            {
                if (m_stringSort == null) m_stringSort = new SeqSort(this, Native.Z3_mk_string_sort(nCtx));
                return m_stringSort;
            }
        }
 
 
        public BoolSort MkBoolSort()
        {
            return new BoolSort(this);
        }
 
        public UninterpretedSort MkUninterpretedSort(Symbol s)
        {
            Debug.Assert(s != null);
 
            CheckContextMatch(s);
            return new UninterpretedSort(this, s);
        }
 
        public UninterpretedSort MkUninterpretedSort(string str)
        {
            using var sym = MkSymbol(str);
            return MkUninterpretedSort(sym);
        }
 
        public IntSort MkIntSort()
        {
 
            return new IntSort(this);
        }
 
        public RealSort MkRealSort()
        {
            return new RealSort(this);
        }
 
        public ComplexSort MkComplexSort()
        {
            return new ComplexSort(this);
        }
 
        public BitVecSort MkBitVecSort(uint size)
        {
            return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
        }
 
        public SeqSort MkSeqSort(Sort s)
        {
            Debug.Assert(s != null);
            return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
        }
 
        public ReSort MkReSort(SeqSort s)
        {
            Debug.Assert(s != null);
            return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
        }
 
        public ArraySort MkArraySort(Sort domain, Sort range)
        {
            Debug.Assert(domain != null);
            Debug.Assert(range != null);
 
            CheckContextMatch(domain);
            CheckContextMatch(range);
            return new ArraySort(this, domain, range);
        }
 
        public ArraySort MkArraySort(Sort[] domain, Sort range)
        {
            Debug.Assert(domain != null);
            Debug.Assert(range != null);
 
            CheckContextMatch<Sort>(domain);
            CheckContextMatch(range);
            return new ArraySort(this, domain, range);
        }
 
        public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
        {
            Debug.Assert(name != null);
            Debug.Assert(fieldNames != null);
            Debug.Assert(fieldNames.All(fn => fn != null));
            Debug.Assert(fieldSorts == null || fieldSorts.All(fs => fs != null));
 
            CheckContextMatch(name);
            CheckContextMatch<Symbol>(fieldNames);
            CheckContextMatch<Sort>(fieldSorts);
            return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
        }
 
        public EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
        {
            Debug.Assert(name != null);
            Debug.Assert(enumNames != null);
            Debug.Assert(enumNames.All(f => f != null));
 
 
            CheckContextMatch(name);
            CheckContextMatch<Symbol>(enumNames);
            return new EnumSort(this, name, enumNames);
        }
 
        public EnumSort MkEnumSort(string name, params string[] enumNames)
        {
            Debug.Assert(enumNames != null);
 
            var enumSymbols = MkSymbols(enumNames);
            try
            {
                using var symbol = MkSymbol(name);
                return new EnumSort(this, symbol, enumSymbols);
            }
            finally
            {
                foreach (var enumSymbol in enumSymbols)
                    enumSymbol.Dispose();
            }
        }
 
        public ListSort MkListSort(Symbol name, Sort elemSort)
        {
            Debug.Assert(name != null);
            Debug.Assert(elemSort != null);
 
            CheckContextMatch(name);
            CheckContextMatch(elemSort);
            return new ListSort(this, name, elemSort);
        }
 
        public ListSort MkListSort(string name, Sort elemSort)
        {
            Debug.Assert(elemSort != null);
 
            CheckContextMatch(elemSort);
            using var symbol = MkSymbol(name);
            return new ListSort(this, symbol, elemSort);
        }
 
        public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
        {
            Debug.Assert(name != null);
 
            CheckContextMatch(name);
            return new FiniteDomainSort(this, name, size);
        }
 
        public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
        {
            using var symbol = MkSymbol(name);
            return new FiniteDomainSort(this, symbol, size);
        }
 
 
        #region Datatypes
        public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
        {
            Debug.Assert(name != null);
            Debug.Assert(recognizer != null);
 
            return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
        }
 
        public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
        {
 
            using var nameSymbol = MkSymbol(name);
            using var recognizerSymbol = MkSymbol(recognizer);
            var fieldSymbols = MkSymbols(fieldNames);
            try
            {
                return new Constructor(this, nameSymbol, recognizerSymbol, fieldSymbols, sorts, sortRefs);
            }
            finally
            {
                foreach (var fieldSymbol in fieldSymbols)
                    fieldSymbol.Dispose();
            }
        }
 
        public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
        {
            Debug.Assert(name != null);
            Debug.Assert(constructors != null);
            Debug.Assert(constructors.All(c => c != null));
 
 
            CheckContextMatch(name);
            CheckContextMatch<Constructor>(constructors);
            return new DatatypeSort(this, name, constructors);
        }
 
        public DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
        {
            Debug.Assert(constructors != null);
            Debug.Assert(constructors.All(c => c != null));
 
            CheckContextMatch<Constructor>(constructors);
            using var symbol = MkSymbol(name);
            return new DatatypeSort(this, symbol, constructors);
        }
 
        public DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters = null)
        {
            Debug.Assert(name != null);
            CheckContextMatch(name);
            if (parameters != null)
                CheckContextMatch<Sort>(parameters);
            
            var numParams = (parameters == null) ? 0 : (uint)parameters.Length;
            var paramsNative = (parameters == null) ? null : AST.ArrayToNative(parameters);
            return new DatatypeSort(this, Native.Z3_mk_datatype_sort(nCtx, name.NativeObject, numParams, paramsNative));
        }
 
        public DatatypeSort MkDatatypeSortRef(string name, Sort[] parameters = null)
        {
            using var symbol = MkSymbol(name);
            return MkDatatypeSortRef(symbol, parameters);
        }
 
        public DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
        {
            Debug.Assert(names != null);
            Debug.Assert(c != null);
            Debug.Assert(names.Length == c.Length);
            //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
            Debug.Assert(names.All(name => name != null));
 
            CheckContextMatch<Symbol>(names);
            uint n = (uint)names.Length;
            ConstructorList[] cla = new ConstructorList[n];
            IntPtr[] n_constr = new IntPtr[n];
            for (uint i = 0; i < n; i++)
            {
                Constructor[] constructor = c[i];
                CheckContextMatch<Constructor>(constructor);
                cla[i] = new ConstructorList(this, constructor);
                n_constr[i] = cla[i].NativeObject;
            }
            IntPtr[] n_res = new IntPtr[n];
            Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
            DatatypeSort[] res = new DatatypeSort[n];
            for (uint i = 0; i < n; i++)
                res[i] = new DatatypeSort(this, n_res[i]);
            return res;
        }
 
        public DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
        {
            Debug.Assert(names != null);
            Debug.Assert(c != null);
            Debug.Assert(names.Length == c.Length);
            //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
            //Debug.Assert(names.All(name => name != null));
 
            var symbols = MkSymbols(names);
            try
            {
                return MkDatatypeSorts(symbols, c);
            }
            finally
            {
                foreach (var symbol in symbols)
                    symbol.Dispose();
            }
        }
 
        public Sort MkTypeVariable(Symbol name)
        {
            Debug.Assert(name != null);
            CheckContextMatch(name);
            return new Sort(this, Native.Z3_mk_type_variable(nCtx, name.NativeObject));
        }
 
        public Sort MkTypeVariable(string name)
        {
            using var symbol = MkSymbol(name);
            return MkTypeVariable(symbol);
        }
 
        public DatatypeSort MkPolymorphicDatatypeSort(Symbol name, Sort[] typeParams, Constructor[] constructors)
        {
            Debug.Assert(name != null);
            Debug.Assert(typeParams != null);
            Debug.Assert(constructors != null);
            Debug.Assert(constructors.All(c => c != null));
 
            CheckContextMatch(name);
            CheckContextMatch<Sort>(typeParams);
            CheckContextMatch<Constructor>(constructors);
            return new DatatypeSort(this,
                Native.Z3_mk_polymorphic_datatype(nCtx, name.NativeObject,
                    (uint)typeParams.Length, AST.ArrayToNative(typeParams),
                    (uint)constructors.Length, Z3Object.ArrayToNative(constructors)));
        }
 
        public DatatypeSort MkPolymorphicDatatypeSort(string name, Sort[] typeParams, Constructor[] constructors)
        {
            using var symbol = MkSymbol(name);
            return MkPolymorphicDatatypeSort(symbol, typeParams, constructors);
        }
 
        public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
        {
            return Expr.Create(this, Native.Z3_datatype_update_field(
                                        nCtx, field.NativeObject,
                                        t.NativeObject, v.NativeObject));
        }
 
        #endregion
        #endregion
 
        #region Function Declarations
        public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
        {
            Debug.Assert(name != null);
            Debug.Assert(range != null);
            Debug.Assert(domain.All(d => d != null));
 
            CheckContextMatch(name);
            CheckContextMatch<Sort>(domain);
            CheckContextMatch(range);
            return new FuncDecl(this, name, domain, range);
        }
 
        public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
        {
            Debug.Assert(name != null);
            Debug.Assert(domain != null);
            Debug.Assert(range != null);
 
            CheckContextMatch(name);
            CheckContextMatch(domain);
            CheckContextMatch(range);
            Sort[] q = new Sort[] { domain };
            return new FuncDecl(this, name, q, range);
        }
 
        public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
        {
            Debug.Assert(range != null);
            Debug.Assert(domain.All(d => d != null));
 
            CheckContextMatch<Sort>(domain);
            CheckContextMatch(range);
            using var symbol = MkSymbol(name);
            return new FuncDecl(this, symbol, domain, range);
        }
 
        public FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
        {
            Debug.Assert(range != null);
            Debug.Assert(domain.All(d => d != null));
 
            CheckContextMatch<Sort>(domain);
            CheckContextMatch(range);
            using var symbol = MkSymbol(name);
            return new FuncDecl(this, symbol, domain, range, true);
        }
 
        public void AddRecDef(FuncDecl f, Expr[] args, Expr body)
        {
            CheckContextMatch(f);
            CheckContextMatch<Expr>(args);
            CheckContextMatch(body);
            IntPtr[] argsNative = AST.ArrayToNative(args);
            Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
        }
 
        public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
        {
            Debug.Assert(range != null);
            Debug.Assert(domain != null);
 
            CheckContextMatch(domain);
            CheckContextMatch(range);
            using var symbol = MkSymbol(name);
            Sort[] q = new Sort[] { domain };
            return new FuncDecl(this, symbol, q, range);
        }
 
        public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
        {
            Debug.Assert(range != null);
            Debug.Assert(domain.All(d => d != null));
 
            CheckContextMatch<Sort>(domain);
            CheckContextMatch(range);
            return new FuncDecl(this, prefix, domain, range);
        }
 
        public FuncDecl MkConstDecl(Symbol name, Sort range)
        {
            Debug.Assert(name != null);
            Debug.Assert(range != null);
 
            CheckContextMatch(name);
            CheckContextMatch(range);
            return new FuncDecl(this, name, null, range);
        }
 
        public FuncDecl MkConstDecl(string name, Sort range)
        {
            Debug.Assert(range != null);
 
            CheckContextMatch(range);
            using var symbol = MkSymbol(name);
            return new FuncDecl(this, symbol, null, range);
        }
 
        public FuncDecl MkFreshConstDecl(string prefix, Sort range)
        {
            Debug.Assert(range != null);
 
            CheckContextMatch(range);
            return new FuncDecl(this, prefix, null, range);
        }
 
        public FuncDecl MkUserPropagatorFuncDecl(string name, Sort[] domain, Sort range) 
        {
             using var _name = MkSymbol(name);
             var fn = Native.Z3_solver_propagate_declare(nCtx, _name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject);
             return new FuncDecl(this, fn);
        }
        #endregion
 
        #region Bound Variables
        public Expr MkBound(uint index, Sort ty)
        {
            Debug.Assert(ty != null);
 
            return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
        }
        #endregion
 
        #region Quantifier Patterns
        public Pattern MkPattern(params Expr[] terms)
        {
            Debug.Assert(terms != null);
            if (terms.Length == 0)
                throw new Z3Exception("Cannot create a pattern from zero terms");
 
            IntPtr[] termsNative = AST.ArrayToNative(terms);
            return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
        }
        #endregion
 
        #region Constants
        public Expr MkConst(Symbol name, Sort range)
        {
            Debug.Assert(name != null);
            Debug.Assert(range != null);
 
            CheckContextMatch(name);
            CheckContextMatch(range);
 
            return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
        }
 
        public Expr MkConst(string name, Sort range)
        {
            Debug.Assert(range != null);
 
            using var symbol = MkSymbol(name);
            return MkConst(symbol, range);
        }
 
        public Expr MkFreshConst(string prefix, Sort range)
        {
            Debug.Assert(range != null);
 
            CheckContextMatch(range);
            return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
        }
 
        public Expr MkConst(FuncDecl f)
        {
            Debug.Assert(f != null);
 
            return MkApp(f);
        }
 
        public BoolExpr MkBoolConst(Symbol name)
        {
            Debug.Assert(name != null);
 
            return (BoolExpr)MkConst(name, BoolSort);
        }
 
        public BoolExpr MkBoolConst(string name)
        {
            using var symbol = MkSymbol(name);
            return (BoolExpr)MkConst(symbol, BoolSort);
        }
 
        public IntExpr MkIntConst(Symbol name)
        {
            Debug.Assert(name != null);
 
            return (IntExpr)MkConst(name, IntSort);
        }
 
        public IntExpr MkIntConst(string name)
        {
            Debug.Assert(name != null);
 
            return (IntExpr)MkConst(name, IntSort);
        }
 
        public RealExpr MkRealConst(Symbol name)
        {
            Debug.Assert(name != null);
 
            return (RealExpr)MkConst(name, RealSort);
        }
 
        public RealExpr MkRealConst(string name)
        {
 
            return (RealExpr)MkConst(name, RealSort);
        }
 
        public ComplexExpr MkComplexConst(Symbol name)
        {
            return (ComplexExpr)MkConst(name, ComplexSort);
        }
 
        public ComplexExpr MkComplexConst(string name)
        {
            return (ComplexExpr)MkConst(name, ComplexSort);
        }
 
        public ComplexExpr MkComplex(ArithExpr real, ArithExpr imag)
        {
            CheckContextMatch(real, imag);
            return new ComplexExpr(this, Native.Z3_mk_complex(nCtx, real.NativeObject, imag.NativeObject));
        }
 
        public RealExpr MkRealPart(ArithExpr value)
        {
            CheckContextMatch(value);
            return new RealExpr(this, Native.Z3_mk_real_part(nCtx, value.NativeObject));
        }
 
        public RealExpr MkImagPart(ArithExpr value)
        {
            CheckContextMatch(value);
            return new RealExpr(this, Native.Z3_mk_imag_part(nCtx, value.NativeObject));
        }
 
        public BitVecExpr MkBVConst(Symbol name, uint size)
        {
            Debug.Assert(name != null);
 
            using var sort = MkBitVecSort(size);
            return (BitVecExpr)MkConst(name, sort);
        }
 
        public BitVecExpr MkBVConst(string name, uint size)
        {
            using var sort = MkBitVecSort(size);
            return (BitVecExpr)MkConst(name, sort);
        }
        #endregion
 
        #region Terms
        public Expr MkApp(FuncDecl f, params Expr[] args)
        {
            Debug.Assert(f != null);
            Debug.Assert(args == null || args.All(a => a != null));
            CheckContextMatch(f);
            CheckContextMatch<Expr>(args);
            return Expr.Create(this, f, args);
        }
 
        public Expr MkApp(FuncDecl f, IEnumerable<Expr> args)
        {
            Debug.Assert(f != null);
            return MkApp(f, args?.ToArray());
        }
 
        #region Propositional
        public BoolExpr MkTrue()
        {
            return new BoolExpr(this, Native.Z3_mk_true(nCtx));
        }
 
        public BoolExpr MkFalse()
        {
            return new BoolExpr(this, Native.Z3_mk_false(nCtx));
        }
 
        public BoolExpr MkBool(bool value)
        {
            return value ? MkTrue() : MkFalse();
        }
 
        public BoolExpr MkEq(Expr x, Expr y)
        {
            Debug.Assert(x != null);
            Debug.Assert(y != null);
 
            CheckContextMatch(x);
            CheckContextMatch(y);
            return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
        }
 
        public BoolExpr MkDistinct(params Expr[] args)
        {
            Debug.Assert(args != null);
            Debug.Assert(args.All(a => a != null));
 
            CheckContextMatch<Expr>(args);
            return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
        }
 
        public BoolExpr MkDistinct(IEnumerable<Expr> args)
        {
            Debug.Assert(args != null);
            return MkDistinct(args.ToArray());
        }
 
        public BoolExpr MkNot(BoolExpr a)
        {
            Debug.Assert(a != null);
            CheckContextMatch(a);
            return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
        }
 
        public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
            Debug.Assert(t3 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            CheckContextMatch(t3);
            return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
        }
 
        public BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkXor(IEnumerable<BoolExpr> args)
        {
            Debug.Assert(args != null);
            var ts = args.ToArray();
            Debug.Assert(ts.All(a => a != null));
            CheckContextMatch<BoolExpr>(ts);
 
            return ts.Aggregate(MkFalse(), (r, t) =>
                    {
                        using (r)
                            return MkXor(r, t);
                    });
        }
 
        public BoolExpr MkAnd(params BoolExpr[] ts)
        {
            Debug.Assert(ts != null);
            Debug.Assert(ts.All(a => a != null));
 
            CheckContextMatch<BoolExpr>(ts);
            return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
        }
 
        public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
        {
            Debug.Assert(t != null);
            return MkAnd(t.ToArray());
        }
 
        public BoolExpr MkOr(params BoolExpr[] ts)
        {
            Debug.Assert(ts != null);
            Debug.Assert(ts.All(a => a != null));
 
            CheckContextMatch<BoolExpr>(ts);
            return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
        }
 
 
        public BoolExpr MkOr(IEnumerable<BoolExpr> ts)
        {
            Debug.Assert(ts != null);
            return MkOr(ts.ToArray());
        }
 
        #endregion
 
        #region Arithmetic
        public ArithExpr MkAdd(params ArithExpr[] ts)
        {
            Debug.Assert(ts != null);
            Debug.Assert(ts.All(a => a != null));
 
            CheckContextMatch<ArithExpr>(ts);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
        }
 
        public ArithExpr MkAdd(IEnumerable<ArithExpr> ts)
        {
            Debug.Assert(ts != null);
            return MkAdd(ts.ToArray());
        }
 
        public ArithExpr MkMul(params ArithExpr[] ts)
        {
            Debug.Assert(ts != null);
            Debug.Assert(ts.All(a => a != null));
 
            CheckContextMatch<ArithExpr>(ts);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
        }
 
        public ArithExpr MkMul(IEnumerable<ArithExpr> ts)
        {
            Debug.Assert(ts != null);
            return MkMul(ts.ToArray());
        }
 
        public ArithExpr MkSub(params ArithExpr[] ts)
        {
            Debug.Assert(ts != null);
            Debug.Assert(ts.All(a => a != null));
 
            CheckContextMatch<ArithExpr>(ts);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
        }
 
        public ArithExpr MkUnaryMinus(ArithExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
        }
 
        public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public IntExpr MkMod(IntExpr t1, IntExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public IntExpr MkRem(IntExpr t1, IntExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public RealExpr MkInt2Real(IntExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
        }
 
        public IntExpr MkReal2Int(RealExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
        }
 
        public BoolExpr MkIsInteger(RealExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
        }
        #endregion
 
        #region Bit-vectors
        public BitVecExpr MkBVNot(BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
        }
 
        public BitVecExpr MkBVRedAND(BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
        }
 
        public BitVecExpr MkBVRedOR(BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
        }
 
        public BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVNeg(BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
        }
 
        public BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
        }
 
        public BitVecExpr MkSignExt(uint i, BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
        }
 
        public BitVecExpr MkZeroExt(uint i, BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
        }
 
        public BitVecExpr MkRepeat(uint i, BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
        }
 
        public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
        }
 
        public BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
        }
 
        public BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BitVecExpr MkInt2BV(uint n, IntExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
        }
 
        public IntExpr MkBV2Int(BitVecExpr t, bool signed)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (byte)(signed ? 1 : 0)));
        }
 
        public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
        }
 
        public BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
        }
 
        public BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkBVNegNoOverflow(BitVecExpr t)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
        }
 
        public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
        }
 
        public BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
        }
        #endregion
 
        #region Arrays
        public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
        {
            Debug.Assert(name != null);
            Debug.Assert(domain != null);
            Debug.Assert(range != null);
 
            using var sort = MkArraySort(domain, range);
            return (ArrayExpr)MkConst(name, sort);
        }
 
        public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
        {
            Debug.Assert(domain != null);
            Debug.Assert(range != null);
 
            using var symbol = MkSymbol(name);
            using var sort = MkArraySort(domain, range);
            return (ArrayExpr)MkConst(symbol, sort);
        }
 
 
        public Expr MkSelect(ArrayExpr a, Expr i)
        {
            Debug.Assert(a != null);
            Debug.Assert(i != null);
 
            CheckContextMatch(a);
            CheckContextMatch(i);
            return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
        }
 
        public Expr MkSelect(ArrayExpr a, params Expr[] args)
        {
            Debug.Assert(a != null);
            Debug.Assert(args != null && args.All(n => n != null));
 
            CheckContextMatch(a);
            CheckContextMatch<Expr>(args);
            return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
        }
 
 
        public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
        {
            Debug.Assert(a != null);
            Debug.Assert(i != null);
            Debug.Assert(v != null);
 
            CheckContextMatch(a);
            CheckContextMatch(i);
            CheckContextMatch(v);
            return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
        }
 
        public ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
        {
            Debug.Assert(a != null);
            Debug.Assert(args != null);
            Debug.Assert(v != null);
 
            CheckContextMatch<Expr>(args);
            CheckContextMatch(a);
            CheckContextMatch(v);
            return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
        }
 
        public ArrayExpr MkConstArray(Sort domain, Expr v)
        {
            Debug.Assert(domain != null);
            Debug.Assert(v != null);
 
            CheckContextMatch(domain);
            CheckContextMatch(v);
            return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
        }
 
        public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
        {
            Debug.Assert(f != null);
            Debug.Assert(args == null || args.All(a => a != null));
 
            CheckContextMatch(f);
            CheckContextMatch<ArrayExpr>(args);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
        }
 
        public Expr MkTermArray(ArrayExpr array)
        {
            Debug.Assert(array != null);
 
            CheckContextMatch(array);
            return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
        }
 
        public Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
        {
            Debug.Assert(arg1 != null);
            Debug.Assert(arg2 != null);
 
            CheckContextMatch(arg1);
            CheckContextMatch(arg2);
            return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
        }
 
        #endregion
 
        #region Sets
        public SetSort MkSetSort(Sort ty)
        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return new SetSort(this, ty);
        }
 
        public ArrayExpr MkEmptySet(Sort domain)
        {
            Debug.Assert(domain != null);
 
            CheckContextMatch(domain);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
        }
 
        public ArrayExpr MkFullSet(Sort domain)
        {
            Debug.Assert(domain != null);
 
            CheckContextMatch(domain);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
        }
 
        public ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
        {
            Debug.Assert(set != null);
            Debug.Assert(element != null);
 
            CheckContextMatch(set);
            CheckContextMatch(element);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
        }
 
 
        public ArrayExpr MkSetDel(ArrayExpr set, Expr element)
        {
            Debug.Assert(set != null);
            Debug.Assert(element != null);
 
            CheckContextMatch(set);
            CheckContextMatch(element);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
        }
 
        public ArrayExpr MkSetUnion(params ArrayExpr[] args)
        {
            Debug.Assert(args != null);
            Debug.Assert(args.All(a => a != null));
 
            CheckContextMatch<ArrayExpr>(args);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
        }
 
        public ArrayExpr MkSetIntersection(params ArrayExpr[] args)
        {
            Debug.Assert(args != null);
            Debug.Assert(args.All(a => a != null));
 
            CheckContextMatch<ArrayExpr>(args);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
        }
 
        public ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
        {
            Debug.Assert(arg1 != null);
            Debug.Assert(arg2 != null);
 
            CheckContextMatch(arg1);
            CheckContextMatch(arg2);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
        }
 
        public ArrayExpr MkSetComplement(ArrayExpr arg)
        {
            Debug.Assert(arg != null);
 
            CheckContextMatch(arg);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
        }
 
        public BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
        {
            Debug.Assert(elem != null);
            Debug.Assert(set != null);
 
            CheckContextMatch(elem);
            CheckContextMatch(set);
            return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
        }
 
        public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
        {
            Debug.Assert(arg1 != null);
            Debug.Assert(arg2 != null);
 
            CheckContextMatch(arg1);
            CheckContextMatch(arg2);
            return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
        }
 
        #endregion
 
        #region Finite Sets
 
        public FiniteSetSort MkFiniteSetSort(Sort elemSort)
        {
            Debug.Assert(elemSort != null);
 
            CheckContextMatch(elemSort);
            return new FiniteSetSort(this, elemSort);
        }
 
        public bool IsFiniteSetSort(Sort s)
        {
            Debug.Assert(s != null);
 
            CheckContextMatch(s);
            return Native.Z3_is_finite_set_sort(nCtx, s.NativeObject) != 0;
        }
 
        public Sort GetFiniteSetSortBasis(Sort s)
        {
            Debug.Assert(s != null);
 
            CheckContextMatch(s);
            return Sort.Create(this, Native.Z3_get_finite_set_sort_basis(nCtx, s.NativeObject));
        }
 
        public Expr MkFiniteSetEmpty(Sort setSort)
        {
            Debug.Assert(setSort != null);
 
            CheckContextMatch(setSort);
            return Expr.Create(this, Native.Z3_mk_finite_set_empty(nCtx, setSort.NativeObject));
        }
 
        public Expr MkFiniteSetSingleton(Expr elem)
        {
            Debug.Assert(elem != null);
 
            CheckContextMatch(elem);
            return Expr.Create(this, Native.Z3_mk_finite_set_singleton(nCtx, elem.NativeObject));
        }
 
        public Expr MkFiniteSetUnion(Expr s1, Expr s2)
        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
 
            CheckContextMatch(s1);
            CheckContextMatch(s2);
            return Expr.Create(this, Native.Z3_mk_finite_set_union(nCtx, s1.NativeObject, s2.NativeObject));
        }
 
        public Expr MkFiniteSetIntersect(Expr s1, Expr s2)
        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
 
            CheckContextMatch(s1);
            CheckContextMatch(s2);
            return Expr.Create(this, Native.Z3_mk_finite_set_intersect(nCtx, s1.NativeObject, s2.NativeObject));
        }
 
        public Expr MkFiniteSetDifference(Expr s1, Expr s2)
        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
 
            CheckContextMatch(s1);
            CheckContextMatch(s2);
            return Expr.Create(this, Native.Z3_mk_finite_set_difference(nCtx, s1.NativeObject, s2.NativeObject));
        }
 
        public BoolExpr MkFiniteSetMember(Expr elem, Expr set)
        {
            Debug.Assert(elem != null);
            Debug.Assert(set != null);
 
            CheckContextMatch(elem);
            CheckContextMatch(set);
            return (BoolExpr)Expr.Create(this, Native.Z3_mk_finite_set_member(nCtx, elem.NativeObject, set.NativeObject));
        }
 
        public Expr MkFiniteSetSize(Expr set)
        {
            Debug.Assert(set != null);
 
            CheckContextMatch(set);
            return Expr.Create(this, Native.Z3_mk_finite_set_size(nCtx, set.NativeObject));
        }
 
        public BoolExpr MkFiniteSetSubset(Expr s1, Expr s2)
        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
 
            CheckContextMatch(s1);
            CheckContextMatch(s2);
            return (BoolExpr)Expr.Create(this, Native.Z3_mk_finite_set_subset(nCtx, s1.NativeObject, s2.NativeObject));
        }
 
        public Expr MkFiniteSetMap(Expr f, Expr set)
        {
            Debug.Assert(f != null);
            Debug.Assert(set != null);
 
            CheckContextMatch(f);
            CheckContextMatch(set);
            return Expr.Create(this, Native.Z3_mk_finite_set_map(nCtx, f.NativeObject, set.NativeObject));
        }
 
        public Expr MkFiniteSetFilter(Expr f, Expr set)
        {
            Debug.Assert(f != null);
            Debug.Assert(set != null);
 
            CheckContextMatch(f);
            CheckContextMatch(set);
            return Expr.Create(this, Native.Z3_mk_finite_set_filter(nCtx, f.NativeObject, set.NativeObject));
        }
 
        public Expr MkFiniteSetRange(Expr low, Expr high)
        {
            Debug.Assert(low != null);
            Debug.Assert(high != null);
 
            CheckContextMatch(low);
            CheckContextMatch(high);
            return Expr.Create(this, Native.Z3_mk_finite_set_range(nCtx, low.NativeObject, high.NativeObject));
        }
 
        #endregion
 
        #region Sequence, string and regular expressions
 
        public SeqExpr MkEmptySeq(Sort s)
        {
            Debug.Assert(s != null);
            return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
        }
 
        public SeqExpr MkUnit(Expr elem)
        {
            Debug.Assert(elem != null);
            return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
        }
 
        public SeqExpr MkString(string s)
        {
            Debug.Assert(s != null);
            return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
        }
 
        public SeqExpr IntToString(Expr e)
        {
            Debug.Assert(e != null);
            Debug.Assert(e is ArithExpr);
            return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
        }
 
        public SeqExpr UbvToString(Expr e)
        {
            Debug.Assert(e != null);
            Debug.Assert(e is ArithExpr);
            return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject));
        }
 
        public SeqExpr SbvToString(Expr e)
        {
            Debug.Assert(e != null);
            Debug.Assert(e is ArithExpr);
            return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject));
        }
 
        public IntExpr StringToInt(Expr e)
        {
            Debug.Assert(e != null);
            Debug.Assert(e is SeqExpr);
            return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject));
        }
 
 
        public SeqExpr MkConcat(params SeqExpr[] t)
        {
            Debug.Assert(t != null);
            Debug.Assert(t.All(a => a != null));
 
            CheckContextMatch<SeqExpr>(t);
            return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }
 
 
        public IntExpr MkLength(SeqExpr s)
        {
            Debug.Assert(s != null);
            return (IntExpr)Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
        }
 
        public SeqExpr MkSeqPower(SeqExpr s, Expr n)
        {
            Debug.Assert(s != null);
            Debug.Assert(n != null);
            CheckContextMatch(s, n);
            return new SeqExpr(this, Native.Z3_mk_seq_power(nCtx, s.NativeObject, n.NativeObject));
        }
 
        public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
            CheckContextMatch(s1, s2);
            return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
        }
 
        public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
            CheckContextMatch(s1, s2);
            return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
        }
 
        public BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
            CheckContextMatch(s1, s2);
            return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
        }
 
        public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
            CheckContextMatch(s1, s2);
            return new BoolExpr(this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject));
        }
 
        public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2)
        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
            CheckContextMatch(s1, s2);
            return new BoolExpr(this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject));
        }
 
        public SeqExpr MkAt(SeqExpr s, Expr index)
        {
            Debug.Assert(s != null);
            Debug.Assert(index != null);
            CheckContextMatch(s, index);
            return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
        }
 
        public Expr MkNth(SeqExpr s, Expr index)
        {
            Debug.Assert(s != null);
            Debug.Assert(index != null);
            CheckContextMatch(s, index);
            return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
        }
 
        public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
        {
            Debug.Assert(s != null);
            Debug.Assert(offset != null);
            Debug.Assert(length != null);
            CheckContextMatch(s, offset, length);
            return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
        }
 
        public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
        {
            Debug.Assert(s != null);
            Debug.Assert(offset != null);
            Debug.Assert(substr != null);
            CheckContextMatch(s, substr, offset);
            return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
        }
 
        public SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
        {
            Debug.Assert(s != null);
            Debug.Assert(src != null);
            Debug.Assert(dst != null);
            CheckContextMatch(s, src, dst);
            return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
        }
 
        public Expr MkSeqMap(Expr f, SeqExpr s)
        {
            Debug.Assert(f != null);
            Debug.Assert(s != null);
            CheckContextMatch(f, s);
            return Expr.Create(this, Native.Z3_mk_seq_map(nCtx, f.NativeObject, s.NativeObject));
        }
 
        public Expr MkSeqMapi(Expr f, Expr i, SeqExpr s)
        {
            Debug.Assert(f != null);
            Debug.Assert(i != null);
            Debug.Assert(s != null);
            CheckContextMatch(f, i, s);
            return Expr.Create(this, Native.Z3_mk_seq_mapi(nCtx, f.NativeObject, i.NativeObject, s.NativeObject));
        }
 
        public Expr MkSeqFoldLeft(Expr f, Expr a, SeqExpr s)
        {
            Debug.Assert(f != null);
            Debug.Assert(a != null);
            Debug.Assert(s != null);
            CheckContextMatch(f, a, s);
            return Expr.Create(this, Native.Z3_mk_seq_foldl(nCtx, f.NativeObject, a.NativeObject, s.NativeObject));
        }
 
        public Expr MkSeqFoldLeftI(Expr f, Expr i, Expr a, SeqExpr s)
        {
            Debug.Assert(f != null);
            Debug.Assert(i != null);
            Debug.Assert(a != null);
            Debug.Assert(s != null);
            CheckContextMatch(f, i, a);
            CheckContextMatch(s, a);
            return Expr.Create(this, Native.Z3_mk_seq_foldli(nCtx, f.NativeObject, i.NativeObject, a.NativeObject, s.NativeObject));
        }
 
        public ReExpr MkToRe(SeqExpr s)
        {
            Debug.Assert(s != null);
            return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));
        }
 
 
        public BoolExpr MkInRe(SeqExpr s, ReExpr re)
        {
            Debug.Assert(s != null);
            Debug.Assert(re != null);
            CheckContextMatch(s, re);
            return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
        }
 
        public ReExpr MkStar(ReExpr re)
        {
            Debug.Assert(re != null);
            return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
        }
 
        public ReExpr MkLoop(ReExpr re, uint lo, uint hi = 0)
        {
            Debug.Assert(re != null);
            return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi));
        }
 
        public ReExpr MkPlus(ReExpr re)
        {
            Debug.Assert(re != null);
            return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));
        }
 
        public ReExpr MkOption(ReExpr re)
        {
            Debug.Assert(re != null);
            return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
        }
 
        public ReExpr MkComplement(ReExpr re)
        {
            Debug.Assert(re != null);
            return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject));
        }
 
        public ReExpr MkConcat(params ReExpr[] t)
        {
            Debug.Assert(t != null);
            Debug.Assert(t.All(a => a != null));
 
            CheckContextMatch<ReExpr>(t);
            return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }
 
        public ReExpr MkUnion(params ReExpr[] t)
        {
            Debug.Assert(t != null);
            Debug.Assert(t.All(a => a != null));
 
            CheckContextMatch<ReExpr>(t);
            return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }
 
        public ReExpr MkIntersect(params ReExpr[] t)
        {
            Debug.Assert(t != null);
            Debug.Assert(t.All(a => a != null));
 
            CheckContextMatch<ReExpr>(t);
            return new ReExpr(this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }
 
        public ReExpr MkDiff(ReExpr a, ReExpr b)
        {
            Debug.Assert(a != null);
            Debug.Assert(b != null);
            CheckContextMatch(a, b);
            return new ReExpr(this, Native.Z3_mk_re_diff(nCtx, a.NativeObject, b.NativeObject));
        }
 
        public ReExpr MkEmptyRe(Sort s)
        {
            Debug.Assert(s != null);
            return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject));
        }
 
        public ReExpr MkFullRe(Sort s)
        {
            Debug.Assert(s != null);
            return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject));
        }
 
 
        public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
        {
            Debug.Assert(lo != null);
            Debug.Assert(hi != null);
            CheckContextMatch(lo, hi);
            return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
        }
 
        public BoolExpr MkCharLe(Expr ch1, Expr ch2)
        {
            Debug.Assert(ch1 != null);
            Debug.Assert(ch2 != null);
            return new BoolExpr(this, Native.Z3_mk_char_le(nCtx, ch1.NativeObject, ch2.NativeObject));
        }
 
        public IntExpr CharToInt(Expr ch)
        {
            Debug.Assert(ch != null);
            return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject));
        }
 
        public BitVecExpr CharToBV(Expr ch)
        {
            Debug.Assert(ch != null);
            return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject));
        }
 
        public Expr CharFromBV(BitVecExpr bv)
        {
            Debug.Assert(bv != null);
            return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject));
        }
 
        public BoolExpr MkIsDigit(Expr ch)
        {
            Debug.Assert(ch != null);
            return new BoolExpr(this, Native.Z3_mk_char_is_digit(nCtx, ch.NativeObject));
        }
 
        #endregion
 
        #region Pseudo-Boolean constraints
 
        public BoolExpr MkAtMost(IEnumerable<BoolExpr> args, uint k)
        {
            Debug.Assert(args != null);
            var ts = args.ToArray();
            CheckContextMatch<BoolExpr>(ts);
            return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint)ts.Length,
                                                          AST.ArrayToNative(ts), k));
        }
 
        public BoolExpr MkAtLeast(IEnumerable<BoolExpr> args, uint k)
        {
            Debug.Assert(args != null);
            var ts = args.ToArray();
            CheckContextMatch<BoolExpr>(ts);
            return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint)ts.Length,
                                                          AST.ArrayToNative(ts), k));
        }
 
        public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
        {
            Debug.Assert(args != null);
            Debug.Assert(coeffs != null);
            Debug.Assert(args.Length == coeffs.Length);
            CheckContextMatch<BoolExpr>(args);
            return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint)args.Length,
                                                           AST.ArrayToNative(args),
                                                           coeffs, k));
        }
 
        public BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k)
        {
            Debug.Assert(args != null);
            Debug.Assert(coeffs != null);
            Debug.Assert(args.Length == coeffs.Length);
            CheckContextMatch<BoolExpr>(args);
            return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint)args.Length,
                                                           AST.ArrayToNative(args),
                                                           coeffs, k));
        }
        public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
        {
            Debug.Assert(args != null);
            Debug.Assert(coeffs != null);
            Debug.Assert(args.Length == coeffs.Length);
            CheckContextMatch<BoolExpr>(args);
            return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint)args.Length,
                                                           AST.ArrayToNative(args),
                                                           coeffs, k));
        }
        #endregion
 
        #region Numerals
 
        #region General Numerals
        public Expr MkNumeral(string v, Sort ty)
        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
        }
 
        public Expr MkNumeral(int v, Sort ty)
        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
        }
 
        public Expr MkNumeral(uint v, Sort ty)
        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
        }
 
        public Expr MkNumeral(long v, Sort ty)
        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
        }
 
        public Expr MkNumeral(ulong v, Sort ty)
        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
        }
        #endregion
 
        #region Reals
        public RatNum MkReal(int num, int den)
        {
            if (den == 0)
                throw new Z3Exception("Denominator is zero");
 
            return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
        }
 
        public RatNum MkReal(string v)
        {
 
            return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
        }
 
        public RatNum MkReal(int v)
        {
 
            return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
        }
 
        public RatNum MkReal(uint v)
        {
 
            return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
        }
 
        public RatNum MkReal(long v)
        {
 
            return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
        }
 
        public RatNum MkReal(ulong v)
        {
 
            return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
        }
        #endregion
 
        #region Integers
        public IntNum MkInt(string v)
        {
 
            return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
        }
 
        public IntNum MkInt(int v)
        {
 
            return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
        }
 
        public IntNum MkInt(uint v)
        {
 
            return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
        }
 
        public IntNum MkInt(long v)
        {
 
            return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
        }
 
        public IntNum MkInt(ulong v)
        {
 
            return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
        }
        #endregion
 
        #region Bit-vectors
        public BitVecNum MkBV(string v, uint size)
        {
            using var sort = MkBitVecSort(size);
            return (BitVecNum)MkNumeral(v, sort);
        }
 
        public BitVecNum MkBV(int v, uint size)
        {
            using var sort = MkBitVecSort(size);
            return (BitVecNum)MkNumeral(v, sort);
        }
 
        public BitVecNum MkBV(uint v, uint size)
        {
            using var sort = MkBitVecSort(size);
            return (BitVecNum)MkNumeral(v, sort);
        }
 
        public BitVecNum MkBV(long v, uint size)
        {
            using var sort = MkBitVecSort(size);
            return (BitVecNum)MkNumeral(v, sort);
        }
 
        public BitVecNum MkBV(ulong v, uint size)
        {
            using var sort = MkBitVecSort(size);
            return (BitVecNum)MkNumeral(v, sort);
        }
 
        public BitVecNum MkBV(bool[] bits)
        {
            byte[] _bits = new byte[bits.Length];
            for (int i = 0; i < bits.Length; ++i) _bits[i] = (byte)(bits[i] ? 1 : 0);
            return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
        }
 
 
        #endregion
 
        #endregion // Numerals
 
        #region Quantifiers
        public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
        {
            Debug.Assert(sorts != null);
            Debug.Assert(names != null);
            Debug.Assert(body != null);
            Debug.Assert(sorts.Length == names.Length);
            Debug.Assert(sorts.All(s => s != null));
            Debug.Assert(names.All(n => n != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
 
            return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }
 
 
        public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
        {
            Debug.Assert(body != null);
            Debug.Assert(boundConstants == null || boundConstants.All(b => b != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
 
            return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }
 
        public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
        {
            Debug.Assert(sorts != null);
            Debug.Assert(names != null);
            Debug.Assert(body != null);
            Debug.Assert(sorts.Length == names.Length);
            Debug.Assert(sorts.All(s => s != null));
            Debug.Assert(names.All(n => n != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
            return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }
 
        public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
        {
            Debug.Assert(body != null);
            Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
            return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }
 
 
        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)
        {
            Debug.Assert(body != null);
            Debug.Assert(names != null);
            Debug.Assert(sorts != null);
            Debug.Assert(sorts.Length == names.Length);
            Debug.Assert(sorts.All(s => s != null));
            Debug.Assert(names.All(n => n != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
 
            if (universal)
                return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
            else
                return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }
 
 
        public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
        {
            Debug.Assert(body != null);
            Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
 
            if (universal)
                return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
            else
                return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }
 
        public Lambda MkLambda(Sort[] sorts, Symbol[] names, Expr body)
        {
            Debug.Assert(sorts != null);
            Debug.Assert(names != null);
            Debug.Assert(body != null);
            Debug.Assert(sorts.Length == names.Length);
            Debug.Assert(sorts.All(s => s != null));
            Debug.Assert(names.All(n => n != null));
            return new Lambda(this, sorts, names, body);
        }
 
        public Lambda MkLambda(Expr[] boundConstants, Expr body)
        {
            Debug.Assert(body != null);
            Debug.Assert(boundConstants != null && boundConstants.All(b => b != null));
            return new Lambda(this, boundConstants, body);
        }
 
 
        #endregion
 
        #endregion // Expr
 
        #region Options
        public Z3_ast_print_mode PrintMode
        {
            get { return m_print_mode; }
            set 
            { 
                Native.Z3_set_ast_print_mode(nCtx, (uint)value);
                m_print_mode = value;
            }
        }
        #endregion
 
        #region SMT Files & Strings
 
        public BoolExpr[] ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
        {
 
            uint csn = Symbol.ArrayLength(sortNames);
            uint cs = Sort.ArrayLength(sorts);
            uint cdn = Symbol.ArrayLength(declNames);
            uint cd = AST.ArrayLength(decls);
            if (csn != cs || cdn != cd)
                throw new Z3Exception("Argument size mismatch");
            using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str,
                AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
                AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
            return assertions.ToBoolExprArray();
        }
 
        public BoolExpr[] ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
        {
 
            uint csn = Symbol.ArrayLength(sortNames);
            uint cs = Sort.ArrayLength(sorts);
            uint cdn = Symbol.ArrayLength(declNames);
            uint cd = AST.ArrayLength(decls);
            if (csn != cs || cdn != cd)
                throw new Z3Exception("Argument size mismatch");
            using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
                AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
                AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
            return assertions.ToBoolExprArray();
        }
 
        public string BenchmarkToSmtlibString(string name, string logic, string status, string attributes, BoolExpr[] assumptions, BoolExpr formula)
        {
            Debug.Assert(assumptions != null);
            Debug.Assert(formula != null);
 
            return Native.Z3_benchmark_to_smtlib_string(
                nCtx,
                name,
                logic,
                status,
                attributes,
                (uint)(assumptions?.Length ?? 0),
                AST.ArrayToNative(assumptions),
                formula.NativeObject);
        }
        #endregion
 
        #region Goals
        public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
        {
 
            return new Goal(this, models, unsatCores, proofs);
        }
        #endregion
 
        #region ParameterSets
        public Params MkParams()
        {
 
            return new Params(this);
        }
        #endregion
 
        #region Tactics
        public uint NumTactics
        {
            get { return Native.Z3_get_num_tactics(nCtx); }
        }
 
        public string[] TacticNames
        {
            get
            {
 
                uint n = NumTactics;
                string[] res = new string[n];
                for (uint i = 0; i < n; i++)
                    res[i] = Native.Z3_get_tactic_name(nCtx, i);
                return res;
            }
        }
 
        public string TacticDescription(string name)
        {
 
            return Native.Z3_tactic_get_descr(nCtx, name);
        }
 
        public Tactic MkTactic(string name)
        {
 
            return new Tactic(this, name);
        }
 
        public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
            // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
 
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            CheckContextMatch<Tactic>(ts);
 
            IntPtr last = IntPtr.Zero;
            if (ts != null && ts.Length > 0)
            {
                last = ts[ts.Length - 1].NativeObject;
                for (int i = ts.Length - 2; i >= 0; i--)
                    last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
            }
            if (last != IntPtr.Zero)
            {
                last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
                return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
            }
            else
                return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
            //  Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
 
            return AndThen(t1, t2, ts);
        }
 
        public Tactic OrElse(Tactic t1, Tactic t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public Tactic TryFor(Tactic t, uint ms)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
        }
 
        public Tactic When(Probe p, Tactic t)
        {
            Debug.Assert(p != null);
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            CheckContextMatch(p);
            return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
        }
 
        public Tactic Cond(Probe p, Tactic t1, Tactic t2)
        {
            Debug.Assert(p != null);
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(p);
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
        }
 
        public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
        }
 
        public Tactic Skip()
        {
 
            return new Tactic(this, Native.Z3_tactic_skip(nCtx));
        }
 
        public Tactic Fail()
        {
 
            return new Tactic(this, Native.Z3_tactic_fail(nCtx));
        }
 
        public Tactic FailIf(Probe p)
        {
            Debug.Assert(p != null);
 
            CheckContextMatch(p);
            return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
        }
 
        public Tactic FailIfNotDecided()
        {
 
            return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
        }
 
        public Tactic UsingParams(Tactic t, Params p)
        {
            Debug.Assert(t != null);
            Debug.Assert(p != null);
 
            CheckContextMatch(t);
            CheckContextMatch(p);
            return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
        }
 
        public Tactic With(Tactic t, Params p)
        {
            Debug.Assert(t != null);
            Debug.Assert(p != null);
 
            return UsingParams(t, p);
        }
 
        public Tactic ParOr(params Tactic[] t)
        {
            Debug.Assert(t == null || t.All(tactic => tactic != null));
 
            CheckContextMatch<Tactic>(t);
            return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
        }
 
        public Tactic ParAndThen(Tactic t1, Tactic t2)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public void Interrupt()
        {
            Native.Z3_interrupt(nCtx);
        }
        #endregion
 
        #region Quantifier Elimination
        public ASTMap MkASTMap()
        {
            return new ASTMap(this);
        }
 
        public Expr QeLite(ASTVector vars, Expr body)
        {
            CheckContextMatch(vars);
            CheckContextMatch(body);
            return Expr.Create(this, Native.Z3_qe_lite(nCtx, vars.NativeObject, body.NativeObject));
        }
 
        public Expr QeModelProject(Model model, Expr[] bounds, Expr body)
        {
            CheckContextMatch(model);
            CheckContextMatch<Expr>(bounds);
            CheckContextMatch(body);
            return Expr.Create(this, Native.Z3_qe_model_project(nCtx, model.NativeObject,
                (uint)bounds.Length, AST.ArrayToNative(bounds), body.NativeObject));
        }
 
        public Expr QeModelProjectSkolem(Model model, Expr[] bounds, Expr body, ASTMap map)
        {
            CheckContextMatch(model);
            CheckContextMatch<Expr>(bounds);
            CheckContextMatch(body);
            CheckContextMatch(map);
            return Expr.Create(this, Native.Z3_qe_model_project_skolem(nCtx, model.NativeObject,
                (uint)bounds.Length, AST.ArrayToNative(bounds), body.NativeObject, map.NativeObject));
        }
 
        public Expr QeModelProjectWithWitness(Model model, Expr[] bounds, Expr body, ASTMap map)
        {
            CheckContextMatch(model);
            CheckContextMatch<Expr>(bounds);
            CheckContextMatch(body);
            CheckContextMatch(map);
            return Expr.Create(this, Native.Z3_qe_model_project_with_witness(nCtx, model.NativeObject,
                (uint)bounds.Length, AST.ArrayToNative(bounds), body.NativeObject, map.NativeObject));
        }
        #endregion
 
        #region Simplifiers
        public uint NumSimplifiers
        {
            get { return Native.Z3_get_num_simplifiers(nCtx); }
        }
 
        public string[] SimplifierNames
        {
            get
            {
 
                uint n = NumSimplifiers;
                string[] res = new string[n];
                for (uint i = 0; i < n; i++)
                    res[i] = Native.Z3_get_simplifier_name(nCtx, i);
                return res;
            }
        }
 
        public string SimplifierDescription(string name)
        {
 
            return Native.Z3_simplifier_get_descr(nCtx, name);
        }
 
        public Simplifier MkSimplifier(string name)
        {
 
            return new Simplifier(this, name);
        }
 
        public Simplifier AndThen(Simplifier t1, Simplifier t2, params Simplifier[] ts)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
            // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
 
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            CheckContextMatch<Simplifier>(ts);
 
            IntPtr last = IntPtr.Zero;
            if (ts != null && ts.Length > 0)
            {
                last = ts[ts.Length - 1].NativeObject;
                for (int i = ts.Length - 2; i >= 0; i--)
                    last = Native.Z3_simplifier_and_then(nCtx, ts[i].NativeObject, last);
            }
            if (last != IntPtr.Zero)
            {
                last = Native.Z3_simplifier_and_then(nCtx, t2.NativeObject, last);
                return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, last));
            }
            else
                return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public Simplifier Then(Simplifier t1, Simplifier t2, params Simplifier[] ts)
        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
            //  Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
 
            return AndThen(t1, t2, ts);
        }
 
        public Simplifier UsingParams(Simplifier t, Params p)
        {
            Debug.Assert(t != null);
            Debug.Assert(p != null);
 
            CheckContextMatch(t);
            CheckContextMatch(p);
            return new Simplifier(this, Native.Z3_simplifier_using_params(nCtx, t.NativeObject, p.NativeObject));
        }
        #endregion
 
        #region Probes
        public uint NumProbes
        {
            get { return Native.Z3_get_num_probes(nCtx); }
        }
 
        public string[] ProbeNames
        {
            get
            {
 
                uint n = NumProbes;
                string[] res = new string[n];
                for (uint i = 0; i < n; i++)
                    res[i] = Native.Z3_get_probe_name(nCtx, i);
                return res;
            }
        }
 
        public string ProbeDescription(string name)
        {
 
            return Native.Z3_probe_get_descr(nCtx, name);
        }
 
        public Probe MkProbe(string name)
        {
 
            return new Probe(this, name);
        }
 
        public Probe ConstProbe(double val)
        {
 
            return new Probe(this, Native.Z3_probe_const(nCtx, val));
        }
 
        public Probe Lt(Probe p1, Probe p2)
        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
        }
 
        public Probe Gt(Probe p1, Probe p2)
        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
        }
 
        public Probe Le(Probe p1, Probe p2)
        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
        }
 
        public Probe Ge(Probe p1, Probe p2)
        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
        }
 
        public Probe Eq(Probe p1, Probe p2)
        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
        }
 
        public Probe And(Probe p1, Probe p2)
        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
        }
 
        public Probe Or(Probe p1, Probe p2)
        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
        }
 
        public Probe Not(Probe p)
        {
            Debug.Assert(p != null);
 
            CheckContextMatch(p);
            return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
        }
        #endregion
 
        #region Solvers
        public Solver MkSolver(Symbol logic = null)
        {
 
            if (logic == null)
                return new Solver(this, Native.Z3_mk_solver(nCtx));
            else
                return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
        }
 
        public Solver MkSolver(string logic)
        {
            using var symbol = MkSymbol(logic);
            return MkSolver(symbol);
        }
 
        public Solver MkSimpleSolver()
        {
 
            return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
        }
 
        public Solver MkSolver(Solver s, Simplifier t)
        {
            Debug.Assert(t != null);
            Debug.Assert(s != null);
            return new Solver(this, Native.Z3_solver_add_simplifier(nCtx, s.NativeObject, t.NativeObject));
        }
 
        public Solver MkSolver(Tactic t)
        {
            Debug.Assert(t != null);
 
            return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
        }
 
 
        #endregion
 
        #region Fixedpoints
        public Fixedpoint MkFixedpoint()
        {
 
            return new Fixedpoint(this);
        }
        #endregion
 
        #region Optimization
        public Optimize MkOptimize()
        {
 
            return new Optimize(this);
        }
        #endregion
 
        #region Floating-Point Arithmetic
 
        #region Rounding Modes
        #region RoundingMode Sort
        public FPRMSort MkFPRoundingModeSort()
        {
            return new FPRMSort(this);
        }
        #endregion
 
        #region Numerals
        public FPRMExpr MkFPRoundNearestTiesToEven()
        {
            return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
        }
 
        public FPRMNum MkFPRNE()
        {
            return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
        }
 
        public FPRMNum MkFPRoundNearestTiesToAway()
        {
            return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
        }
 
        public FPRMNum MkFPRNA()
        {
            return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
        }
 
        public FPRMNum MkFPRoundTowardPositive()
        {
            return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
        }
 
        public FPRMNum MkFPRTP()
        {
            return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
        }
 
        public FPRMNum MkFPRoundTowardNegative()
        {
            return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
        }
 
        public FPRMNum MkFPRTN()
        {
            return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
        }
 
        public FPRMNum MkFPRoundTowardZero()
        {
            return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
        }
 
        public FPRMNum MkFPRTZ()
        {
            return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
        }
        #endregion
        #endregion
 
        #region FloatingPoint Sorts
        public FPSort MkFPSort(uint ebits, uint sbits)
        {
            return new FPSort(this, ebits, sbits);
        }
 
        public FPSort MkFPSortHalf()
        {
            return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
        }
 
        public FPSort MkFPSort16()
        {
            return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
        }
 
        public FPSort MkFPSortSingle()
        {
            return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
        }
 
        public FPSort MkFPSort32()
        {
            return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx));
        }
 
        public FPSort MkFPSortDouble()
        {
            return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
        }
 
        public FPSort MkFPSort64()
        {
            return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
        }
 
        public FPSort MkFPSortQuadruple()
        {
            return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
        }
 
        public FPSort MkFPSort128()
        {
            return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
        }
        #endregion
 
        #region Numerals
        public FPNum MkFPNaN(FPSort s)
        {
            return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
        }
 
        public FPNum MkFPInf(FPSort s, bool negative)
        {
            return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
        }
 
        public FPNum MkFPZero(FPSort s, bool negative)
        {
            return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
        }
 
        public FPNum MkFPNumeral(float v, FPSort s)
        {
            return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
        }
 
        public FPNum MkFPNumeral(double v, FPSort s)
        {
            return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
        }
 
        public FPNum MkFPNumeral(int v, FPSort s)
        {
            return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
        }
 
        public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
        {
            return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
        }
 
        public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
        {
            return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
        }
 
        public FPNum MkFP(float v, FPSort s)
        {
            return MkFPNumeral(v, s);
        }
 
        public FPNum MkFP(double v, FPSort s)
        {
            return MkFPNumeral(v, s);
        }
 
        public FPNum MkFP(int v, FPSort s)
        {
            return MkFPNumeral(v, s);
        }
 
        public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
        {
            return MkFPNumeral(sgn, exp, sig, s);
        }
 
        public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
        {
            return MkFPNumeral(sgn, exp, sig, s);
        }
 
        #endregion
 
        #region Operators
        public FPExpr MkFPAbs(FPExpr t)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
        }
 
        public FPExpr MkFPNeg(FPExpr t)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
        }
 
        public FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
        }
 
        public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
        }
 
        public FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
        }
 
        public FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
        }
 
        public FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
        }
 
        public FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
        }
 
        public FPExpr MkFPRem(FPExpr t1, FPExpr t2)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
        }
 
        public FPExpr MkFPMin(FPExpr t1, FPExpr t2)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public FPExpr MkFPMax(FPExpr t1, FPExpr t2)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkFPGt(FPExpr t1, FPExpr t2)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
        }
 
        public BoolExpr MkFPIsNormal(FPExpr t)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
        }
 
        public BoolExpr MkFPIsSubnormal(FPExpr t)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
        }
 
        public BoolExpr MkFPIsZero(FPExpr t)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
        }
 
        public BoolExpr MkFPIsInfinite(FPExpr t)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
        }
 
        public BoolExpr MkFPIsNaN(FPExpr t)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
        }
 
        public BoolExpr MkFPIsNegative(FPExpr t)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
        }
 
        public BoolExpr MkFPIsPositive(FPExpr t)
        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
        }
        #endregion
 
        #region Conversions to FloatingPoint terms
        public FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
        }
 
        public FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
        }
 
        public FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
        }
 
        public FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
        }
 
        public FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
        {
            if (signed)
                return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
            else
                return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
        }
 
        public FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
        {
            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
        }
        #endregion
 
        #region Conversions from FloatingPoint terms
        public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool sign)
        {
            if (sign)
                return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
            else
                return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
        }
 
        public RealExpr MkFPToReal(FPExpr t)
        {
            return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
        }
        #endregion
 
        #region Z3-specific extensions
        public BitVecExpr MkFPToIEEEBV(FPExpr t)
        {
            return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
        }
 
        public BitVecExpr MkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
        {
            return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
        }
        #endregion
        #endregion // Floating-point Arithmetic
 
        #region Miscellaneous
        public AST WrapAST(IntPtr nativeObject)
        {
            return AST.Create(this, nativeObject);
        }
 
        public IntPtr UnwrapAST(AST a)
        {
            return a.NativeObject;
        }
 
        public FuncDecl MkPartialOrder(Sort a, uint index)
        {
            return new FuncDecl(this, Native.Z3_mk_partial_order(this.nCtx, a.NativeObject, index));
        }
 
        public FuncDecl MkTransitiveClosure(FuncDecl f)
        {
            return new FuncDecl(this, Native.Z3_mk_transitive_closure(this.nCtx, f.NativeObject));
        }
 
        public ASTVector PolynomialSubresultants(Expr p, Expr q, Expr x)
        {
            CheckContextMatch(p);
            CheckContextMatch(q);
            CheckContextMatch(x);
            return new ASTVector(this, Native.Z3_polynomial_subresultants(this.nCtx, p.NativeObject, q.NativeObject, x.NativeObject));
        }
 
        public string SimplifyHelp()
        {
 
            return Native.Z3_simplify_get_help(nCtx);
        }
 
        public ParamDescrs SimplifyParameterDescriptions
        {
            get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
        }
        #endregion
 
        #region Error Handling
        //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
 
        //public event ErrorHandler OnError = null;
        #endregion
 
        #region Parameters
        public void UpdateParamValue(string id, string value)
        {
            Native.Z3_update_param_value(nCtx, id, value);
        }
 
        #endregion
 
        #region Internal
        internal IntPtr m_ctx = IntPtr.Zero;
        internal Native.Z3_error_handler m_n_err_handler = null;
        internal static Object creation_lock = new Object();
        internal IntPtr nCtx { get { return m_ctx; } }
        private Z3_ast_print_mode m_print_mode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
 
        // Estimated native memory used per context, for GC memory pressure hints.
        // The value is a conservative lower bound; actual usage may exceed this.
        private const long NativeMemoryPressureEstimate = 8 * 1024 * 1024; // 8 MB
        private bool m_memPressureAdded = false;
 
        internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
        {
            // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
        }
 
        internal void InitContext()
        {
            PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
            m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
            Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
            if (!is_external)
            {
                GC.AddMemoryPressure(NativeMemoryPressureEstimate);
                m_memPressureAdded = true;
            }
        }
 
        internal void CheckContextMatch(Z3Object other)
        {
            Debug.Assert(other != null);
 
            if (!ReferenceEquals(this, other.Context))
                throw new Z3Exception("Context mismatch");
        }
 
        internal void CheckContextMatch(Z3Object other1, Z3Object other2)
        {
            Debug.Assert(other1 != null);
            Debug.Assert(other2 != null);
            CheckContextMatch(other1);
            CheckContextMatch(other2);
        }
 
        internal void CheckContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
        {
            Debug.Assert(other1 != null);
            Debug.Assert(other2 != null);
            Debug.Assert(other3 != null);
            CheckContextMatch(other1);
            CheckContextMatch(other2);
            CheckContextMatch(other3);
        }
 
        internal void CheckContextMatch(Z3Object[] arr)
        {
            Debug.Assert(arr == null || arr.All(a => a != null));
 
            if (arr != null)
            {
                foreach (Z3Object a in arr)
                {
                    Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
                    CheckContextMatch(a);
                }
            }
        }
 
        internal void CheckContextMatch<T>(IEnumerable<T> arr) where T : Z3Object
        {
            Debug.Assert(arr == null || arr.All(a => a != null));
 
            if (arr != null)
            {
                foreach (Z3Object a in arr)
                {
                    Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
                    CheckContextMatch(a);
                }
            }
        }
 
        private void ObjectInvariant()
        {
            // none
        }
 
        ~Context()
        {
            // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
            Dispose();
        }
 
        public void Dispose()
        {
            // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
 
            if (m_boolSort != null) m_boolSort.Dispose();
            if (m_intSort != null) m_intSort.Dispose();
            if (m_realSort != null) m_realSort.Dispose();
            if (m_complexSort != null) m_complexSort.Dispose();
            if (m_stringSort != null) m_stringSort.Dispose();
            if (m_charSort != null) m_charSort.Dispose();
            m_boolSort = null;
            m_intSort = null;
            m_realSort = null;
            m_complexSort = null;
            m_stringSort = null;
            m_charSort = null;
            if (m_ctx != IntPtr.Zero)
            {
                // Suppress the finalizer before performing cleanup so that it cannot
                // run concurrently or redundantly if cleanup raises an exception.
                GC.SuppressFinalize(this);
                IntPtr ctx;
                // Keep a local reference to the error handler delegate to ensure it stays
                // alive throughout Z3_del_context. Setting m_n_err_handler = null releases
                // the field reference; without the local variable the GC could collect the
                // delegate before the native destructor finishes using the handler.
                Native.Z3_error_handler errHandler;
                lock (this)
                {
                    ctx = m_ctx;
                    errHandler = m_n_err_handler;
                    m_n_err_handler = null;
                    m_ctx = IntPtr.Zero;
                }
                // ctx is non-zero only for the thread that wins the lock and zeros m_ctx,
                // preventing double-free when Dispose() is called concurrently.
                if (ctx != IntPtr.Zero)
                {
                    if (!is_external)
                    {
                        Native.Z3_del_context(ctx);
                        GC.KeepAlive(errHandler);
                    }
                    if (m_memPressureAdded)
                    {
                        GC.RemoveMemoryPressure(NativeMemoryPressureEstimate);
                        m_memPressureAdded = false;
                    }
                }
            }
        }
 
 
        #endregion
    }
}