internal Quantifier(Context ctx, bool isForall, Expr[] bound, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
            : base(ctx)
        {
            Contract.Requires(ctx != null);
            Contract.Requires(body != null);

            Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
            Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
            Contract.Requires(bound == null || Contract.ForAll(bound, n => n != null));

            Context.CheckContextMatch(noPatterns);
            Context.CheckContextMatch(patterns);
            //Context.CheckContextMatch(bound);
            Context.CheckContextMatch(body);

            if (noPatterns == null && quantifierID == null && skolemID == null)
            {
                NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) ? 1 : 0, weight,
                                                 AST.ArrayLength(bound), AST.ArrayToNative(bound),
                                                 AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
                                                 body.NativeObject);
            }
            else
            {
                NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
                                        AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
                                        AST.ArrayLength(bound), AST.ArrayToNative(bound),
                                        AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
                                        AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
                                        body.NativeObject);
            }
        }

 internal DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
     : base(ctx, Native.Z3_mk_datatype(ctx.nCtx, name.NativeObject, (uint)constructors.Length, ArrayToNative(constructors)))
 {
     Contract.Requires(ctx != null);
     Contract.Requires(name != null);
     Contract.Requires(constructors != null);
 }

        internal FiniteDomainSort(Context ctx, Symbol name, ulong size)
            : base(ctx, Native.Z3_mk_finite_domain_sort(ctx.nCtx, name.NativeObject, size))
        {
            Contract.Requires(ctx != null);
            Contract.Requires(name != null);

        }

        /// <summary>
        /// Adds a parameter setting.
        /// </summary>
        public void Add(Symbol name, Symbol value)
        {
            Contract.Requires(name != null);
            Contract.Requires(value != null);

            Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
        }

        internal TupleSort(Context ctx, Symbol name, uint numFields, Symbol[] fieldNames, Sort[] fieldSorts)
            : base(ctx)
        {
            Contract.Requires(ctx != null);
            Contract.Requires(name != null);

            IntPtr t = IntPtr.Zero;
            NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
                                                   Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
                                                   ref t, new IntPtr[numFields]);
        }

        /// <summary>
        /// Create axiom: function f is injective in the i-th argument.
        /// </summary>
        /// <remarks>
        /// The following axiom is produced:
        /// <c>
        /// forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i
        /// </c>
        /// Where, <code>finv</code>is a fresh function declaration.
        /// </summary>
        public static BoolExpr InjAxiom(Context ctx, FuncDecl f, int i)
        {
            Sort[] domain = f.Domain;
            uint sz = f.DomainSize;

            if (i >= sz)
            {
                Console.WriteLine("failed to create inj axiom");
                return null;
            }

            /* declare the i-th inverse of f: finv */
            Sort finv_domain = f.Range;
            Sort finv_range = domain[i];
            FuncDecl finv = ctx.MkFuncDecl("f_fresh", finv_domain, finv_range);

            /* allocate temporary arrays */
            Expr[] xs = new Expr[sz];
            Symbol[] names = new Symbol[sz];
            Sort[] types = new Sort[sz];

            /* fill types, names and xs */

            for (uint j = 0; j < sz; j++)
            {
                types[j] = domain[j];
                names[j] = ctx.MkSymbol(String.Format("x_{0}", j));
                xs[j] = ctx.MkBound(j, types[j]);
            }
            Expr x_i = xs[i];

            /* create f(x_0, ..., x_i, ..., x_{n-1}) */
            Expr fxs = f[xs];

            /* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */
            Expr finv_fxs = finv[fxs];

            /* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */
            Expr eq = ctx.MkEq(finv_fxs, x_i);

            /* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier */
            Pattern p = ctx.MkPattern(new Expr[] { fxs });

            /* create & assert quantifier */
            BoolExpr q = ctx.MkForall(
                types, /* types of quantified variables */
                names, /* names of quantified variables */
                eq,
                1,
                new Pattern[] { p } /* patterns */);

            return q;
        }

        internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
            : base(ctx)
        {
            Contract.Requires(ctx != null);
            Contract.Requires(name != null);
            Contract.Requires(enumNames != null);

            int n = enumNames.Length;
            IntPtr[] n_constdecls = new IntPtr[n];
            IntPtr[] n_testers = new IntPtr[n];
            NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
                                                         Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
        }

        internal ListSort(Context ctx, Symbol name, Sort elemSort)
            : base(ctx)
        {
            Contract.Requires(ctx != null);
            Contract.Requires(name != null);
            Contract.Requires(elemSort != null);

            IntPtr inil = IntPtr.Zero, iisnil = IntPtr.Zero,
                   icons = IntPtr.Zero, iiscons = IntPtr.Zero,
                   ihead = IntPtr.Zero, itail = IntPtr.Zero;

            NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
                                                  ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
        }

        internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body,
            uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
            Symbol quantifierID = null, Symbol skolemID = null
            )
            : base(ctx)
        {
            Contract.Requires(ctx != null);
            Contract.Requires(sorts != null);
            Contract.Requires(names != null);
            Contract.Requires(body != null);
            Contract.Requires(sorts.Length == names.Length);
            Contract.Requires(Contract.ForAll(sorts, s => s != null));
            Contract.Requires(Contract.ForAll(names, n => n != null));
            Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
            Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));

            Context.CheckContextMatch(patterns);
            Context.CheckContextMatch(noPatterns);
            Context.CheckContextMatch(sorts);
            Context.CheckContextMatch(names);
            Context.CheckContextMatch(body);

            if (sorts.Length != names.Length)
                throw new Z3Exception("Number of sorts does not match number of names");

            IntPtr[] _patterns = AST.ArrayToNative(patterns);

            if (noPatterns == null && quantifierID == null && skolemID == null)
            {
                NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
                                           AST.ArrayLength(patterns),  AST.ArrayToNative(patterns),
                                           AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
                                           Symbol.ArrayToNative(names),
                                           body.NativeObject);
            }
            else
            {
                NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
                                  AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
                                  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
                                  AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
                                  AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
                                  Symbol.ArrayToNative(names),
                                  body.NativeObject);
            }
        }

        internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
            Sort[] sorts, uint[] sortRefs)
            : base(ctx)
        {
            Contract.Requires(ctx != null);
            Contract.Requires(name != null);
            Contract.Requires(recognizer != null);

            n = AST.ArrayLength(fieldNames);

            if (n != AST.ArrayLength(sorts))
                throw new Z3Exception("Number of field names does not match number of sorts");
            if (sortRefs != null && sortRefs.Length != n)
                throw new Z3Exception("Number of field names does not match number of sort refs");

            if (sortRefs == null) sortRefs = new uint[n];

            NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
                                                    n,
                                                    Symbol.ArrayToNative(fieldNames),
                                                    Sort.ArrayToNative(sorts),
                                                    sortRefs);
        }

 /// <summary>
 /// Parse the given string using the SMT-LIB parser. 
 /// </summary>
 /// <remarks>
 /// The symbol table of the parser can be initialized using the given sorts and declarations. 
 /// The symbols in the arrays <paramref name="sortNames"/> and <paramref name="declNames"/> 
 /// don't need to match the names of the sorts and declarations in the arrays <paramref name="sorts"/> 
 /// and <paramref name="decls"/>. This is a useful feature since we can use arbitrary names to 
 /// reference sorts and declarations.
 /// </remarks>
 public void ParseSMTLIBString(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");
     Native.Z3_parse_smtlib_string(nCtx, str,
         AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
         AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
 }

        /// <summary>
        /// Create a new uninterpreted sort.
        /// </summary>
        public UninterpretedSort MkUninterpretedSort(Symbol s)
        {
            Contract.Requires(s != null);
            Contract.Ensures(Contract.Result<UninterpretedSort>() != null);

            CheckContextMatch(s);
            return new UninterpretedSort(this, s);
        }

        /// <summary>
        /// Parse the given string using the SMT-LIB2 parser. 
        /// </summary>
        /// <seealso cref="ParseSMTLIBString"/>
        /// <returns>A conjunction of assertions in the scope (up to push/pop) at the end of the string.</returns>
        public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
        {
            Contract.Ensures(Contract.Result<BoolExpr>() != 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");
            return (BoolExpr)Expr.Create(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)));
        }

        /// <summary>
        /// Creates a new (incremental) solver. 
        /// </summary>
        /// <remarks>
        /// This solver also uses a set of builtin tactics for handling the first 
        /// check-sat command, and check-sat commands that take more than a given 
        /// number of milliseconds to be solved. 
        /// </remarks>    
        public Solver MkSolver(Symbol logic = null)
        {
            Contract.Ensures(Contract.Result<Solver>() != 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));
        }

        /// <summary>
        /// Create a new tuple sort.
        /// </summary>    
        public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
        {
            Contract.Requires(name != null);
            Contract.Requires(fieldNames != null);
            Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
            Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
            Contract.Ensures(Contract.Result<TupleSort>() != null);

            CheckContextMatch(name);
            CheckContextMatch(fieldNames);
            CheckContextMatch(fieldSorts);
            return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
        }

        /// <summary>
        /// Create a new enumeration sort.
        /// </summary>
        public EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
        {
            Contract.Requires(name != null);
            Contract.Requires(enumNames != null);
            Contract.Requires(Contract.ForAll(enumNames, f => f != null));

            Contract.Ensures(Contract.Result<EnumSort>() != null);

            CheckContextMatch(name);
            CheckContextMatch(enumNames);
            return new EnumSort(this, name, enumNames);
        }

        /// <summary>
        /// Creates a real constant.
        /// </summary>
        public RealExpr MkRealConst(Symbol name)
        {
            Contract.Requires(name != null);
            Contract.Ensures(Contract.Result<RealExpr>() != null);

            return (RealExpr)MkConst(name, RealSort);
        }

        /// <summary>
        /// Creates an integer constant.
        /// </summary>        
        public IntExpr MkIntConst(Symbol name)
        {
            Contract.Requires(name != null);
            Contract.Ensures(Contract.Result<IntExpr>() != null);

            return (IntExpr)MkConst(name, IntSort);
        }

        /// <summary>
        /// Create a new list sort.
        /// </summary>
        public ListSort MkListSort(Symbol name, Sort elemSort)
        {
            Contract.Requires(name != null);
            Contract.Requires(elemSort != null);
            Contract.Ensures(Contract.Result<ListSort>() != null);

            CheckContextMatch(name);
            CheckContextMatch(elemSort);
            return new ListSort(this, name, elemSort);
        }

        /// <summary>
        /// Create a Boolean constant.
        /// </summary>        
        public BoolExpr MkBoolConst(Symbol name)
        {
            Contract.Requires(name != null);
            Contract.Ensures(Contract.Result<BoolExpr>() != null);

            return (BoolExpr)MkConst(name, BoolSort);
        }