public void Run()
    {
        Dictionary<string, string> cfg = new Dictionary<string, string>() {
            { "AUTO_CONFIG", "true" } };

        using (Context ctx = new Context(cfg))
        {
            IntExpr[] X = new IntExpr[5];
            for (uint i = 0; i < 5; i++)
                X[i] = ctx.MkIntConst(string.Format("x_{0}", i));

            RealExpr[] Y = new RealExpr[5];
            for (uint i = 0; i < 5; i++)
                Y[i] = ctx.MkRealConst(string.Format("y_{0}", i));

            BoolExpr[] P = new BoolExpr[5];
            for (uint i = 0; i < 5; i++)
                P[i] = ctx.MkBoolConst(string.Format("p_{0}", i));

            foreach (Expr x in X)
                Console.WriteLine(x);
            foreach (Expr x in Y)
                Console.WriteLine(x);
            foreach (Expr x in P)
                Console.WriteLine(x);

            foreach (ArithExpr y in Y)
                Console.WriteLine(ctx.MkPower(y, ctx.MkReal(2)));

            ArithExpr[] Yp = new ArithExpr[Y.Length];
            for (uint i = 0; i < Y.Length; i++)
                Yp[i] = ctx.MkPower(Y[i], ctx.MkReal(2));
            Console.WriteLine(ctx.MkAdd(Yp));
        }
    }

 public BoolExpr DependsOn(Context ctx, BoolExpr pack, BoolExpr[] deps)
 {
     BoolExpr[] q = new BoolExpr[deps.Length];
     for (uint i = 0; i < deps.Length; i++)
         q[i] = ctx.MkImplies(pack, deps[i]);
     return ctx.MkAnd(q);
 }

        /// <summary>
        /// Create an expression that marks a formula position for interpolation.
        /// </summary>
        public BoolExpr MkInterpolant(BoolExpr a)
        {
            Contract.Requires(a != null);
            Contract.Ensures(Contract.Result<BoolExpr>() != null);

            CheckContextMatch(a);
            return new BoolExpr(this, Native.Z3_mk_interpolant(nCtx, a.NativeObject));
        }

    public void Run()
    {
        Dictionary<string, string> cfg = new Dictionary<string, string>() {
            { "AUTO_CONFIG", "true" } };

        using (Context ctx = new Context(cfg))
        {
            ArithExpr[] a = new ArithExpr[5];
            for (uint x = 0; x < 5; x++)
                a[x] = ctx.MkInt(x+1);

            foreach (Expr e in a)
                Console.WriteLine(e);

            ArithExpr[] X = new ArithExpr[5];
            for (uint i = 0; i < 5; i++)
                X[i] = ctx.MkIntConst(string.Format("x{0}", i));

            ArithExpr[] Y = new ArithExpr[5];
            for (uint i = 0; i < 5; i++)
                Y[i] = ctx.MkIntConst(string.Format("y{0}", i));

            foreach (Expr e in X)
                Console.WriteLine(e);

            ArithExpr[] X_plus_Y = new ArithExpr[5];
            for (uint i = 0; i < 5; i++)
                X_plus_Y[i] = ctx.MkAdd(X[i], Y[i]);

            foreach (Expr e in X_plus_Y)
                Console.WriteLine(e);

            BoolExpr[] X_gt_Y = new BoolExpr[5];
            for (uint i = 0; i < 5; i++)
                X_gt_Y[i] = ctx.MkGt(X[i], Y[i]);

            foreach (Expr e in X_gt_Y)
                Console.WriteLine(e);

            Console.WriteLine(ctx.MkAnd(X_gt_Y));

            Expr[][] matrix = new Expr[3][];
            for (uint i = 0; i < 3; i++) {
                matrix[i] = new Expr[3];
                for (uint j = 0; j < 3; j++)
                    matrix[i][j] = ctx.MkIntConst(string.Format("x_{0}_{1}", i + 1, j + 1));
            }

            foreach(Expr[] row in matrix) {
                foreach(Expr e in row)
                    Console.Write(" " + e);
                Console.WriteLine();
            }
        }
    }

    public void Run()
    {
        Dictionary<string, string> cfg = new Dictionary<string, string>() {
            { "AUTO_CONFIG", "true" } };

        using (Context ctx = new Context(cfg))
        {
            RealExpr d = ctx.MkRealConst("d");
            RealExpr a = ctx.MkRealConst("a");
            RealExpr t = ctx.MkRealConst("t");
            RealExpr v_i = ctx.MkRealConst("v_i");
            RealExpr v_f = ctx.MkRealConst("v_f");

            BoolExpr[] equations = new BoolExpr[] {
                ctx.MkEq(d, ctx.MkAdd(ctx.MkMul(v_i, t),
                                      ctx.MkDiv(ctx.MkMul(a, ctx.MkPower(t, ctx.MkReal(2))),
                                                ctx.MkReal(2)))),
                ctx.MkEq(v_f, ctx.MkAdd(v_i, ctx.MkMul(a, t)))
            };

            Console.WriteLine("Kinematic equations: ");
            foreach (BoolExpr e in equations)
                Console.WriteLine(e);

            BoolExpr[] problem = new BoolExpr[] {
                ctx.MkEq(v_i, ctx.MkReal(0)),
                ctx.MkEq(t, ctx.MkReal("4.10")),
                ctx.MkEq(a, ctx.MkReal(6))
            };

            Console.WriteLine("Problem: ");
            foreach (BoolExpr p in problem)
                Console.WriteLine(p);

            Solver s = ctx.MkSolver();
            s.Assert(equations);
            s.Assert(problem);

            if (s.Check() != Status.SATISFIABLE)
                throw new Exception("BUG");

            Console.WriteLine("Solution: ");
            Console.WriteLine(s.Model);

            Console.WriteLine("Decimal Solution: ");
            foreach (FuncDecl f in s.Model.ConstDecls)
                Console.WriteLine(f.Name + " = " + ((RatNum)s.Model.ConstInterp(f)).ToDecimalString(10));
        }
    }

        /// <summary> 
        /// Computes an interpolant.
        /// </summary>    
        /// <remarks>For more information on interpolation please refer
        /// too the function Z3_compute_interpolant in the C/C++ API, which is 
        /// well documented.</remarks>
        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
        {
            Contract.Requires(pat != null);
            Contract.Requires(p != null);
            Contract.Ensures(Contract.ValueAtReturn(out interp) != null);
            Contract.Ensures(Contract.ValueAtReturn(out model) != null);

            CheckContextMatch(pat);
            CheckContextMatch(p);

            IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
            int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
            interp = new ASTVector(this, i).ToBoolExprArray();
            model = new Model(this, m);
            return (Z3_lbool)r;
        }

 /// <summary> 
 /// Checks the correctness of an interpolant.
 /// </summary>    
 /// <remarks>For more information on interpolation please refer
 /// too the function Z3_check_interpolant in the C/C++ API, which is 
 /// well documented.</remarks>
 public int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
 {
     Contract.Requires(cnsts.Length == parents.Length);
     Contract.Requires(cnsts.Length == interps.Length + 1);
     IntPtr n_err_str;
     int r = Native.Z3_check_interpolant(nCtx,
                                         (uint)cnsts.Length,
                                         Expr.ArrayToNative(cnsts),
                                         parents,
                                         Expr.ArrayToNative(interps),
                                         out n_err_str,
                                         (uint)theory.Length,
                                         Expr.ArrayToNative(theory));
     error = Marshal.PtrToStringAnsi(n_err_str);
     return r;
 }

 static Model Check(Context ctx, BoolExpr f, Status sat)
 {
     Solver s = ctx.MkSolver();
     s.Assert(f);
     if (s.Check() != sat)
     {
         return null;
     };
     if (sat == Status.SATISFIABLE)
     {
         Console.WriteLine("Data:" + s.Model);
         return s.Model;
     }
     else
         return null;
 }

    public void InstallCheck(Context ctx, BoolExpr[] p)
    {
        Solver s = ctx.MkSolver();

        s.Assert(p);

        if (s.Check() == Status.SATISFIABLE)
        {
            Model m = s.Model;
            foreach (FuncDecl f in m.ConstDecls)
            {
                if (m.ConstInterp(f).IsTrue)
                    Console.WriteLine(f.Name);
            }
        }
        else
            Console.WriteLine("invalid installation profile");
    }

    public void Run()
    {
        Dictionary<string, string> cfg = new Dictionary<string, string>() {
            { "AUTO_CONFIG", "true" } };

        using (Context ctx = new Context(cfg))
        {
            ArithExpr[] Q = new ArithExpr[8];
            for (uint i = 0; i < 8; i++)
                Q[i] = ctx.MkIntConst(string.Format("Q_{0}", i + 1));

            BoolExpr[] val_c = new BoolExpr[8];
            for (uint i = 0; i < 8; i++)
                val_c[i] = ctx.MkAnd(ctx.MkLe(ctx.MkInt(1), Q[i]),
                                     ctx.MkLe(Q[i], ctx.MkInt(8)));

            BoolExpr col_c = ctx.MkDistinct(Q);

            BoolExpr[][] diag_c = new BoolExpr[8][];
            for (uint i = 0; i < 8; i++)
            {
                diag_c[i] = new BoolExpr[i];
                for (uint j = 0; j < i; j++)
                    diag_c[i][j] = (BoolExpr)ctx.MkITE(ctx.MkEq(ctx.MkInt(i), ctx.MkInt(j)),
                                             ctx.MkTrue(),
                                             ctx.MkAnd(ctx.MkNot(ctx.MkEq(ctx.MkSub(Q[i], Q[j]),
                                                                          ctx.MkSub(ctx.MkInt(i), ctx.MkInt(j)))),
                                                       ctx.MkNot(ctx.MkEq(ctx.MkSub(Q[i], Q[j]),
                                                                          ctx.MkSub(ctx.MkInt(j), ctx.MkInt(i))))));
            }

            Solver s = ctx.MkSolver();
            s.Assert(val_c);
            s.Assert(col_c);
            foreach (var c in diag_c)
                s.Assert(c);

            Console.WriteLine(s.Check());
            Console.WriteLine(s.Model);
        }
    }

    public void Run()
    {
        Dictionary<string, string> cfg = new Dictionary<string, string>() {
            { "AUTO_CONFIG", "true" } };

        using (Context ctx = new Context(cfg))
        {
            Sort T = ctx.MkUninterpretedSort("Type");
            FuncDecl subtype = ctx.MkFuncDecl("subtype", new Sort[] { T, T }, ctx.BoolSort);
            FuncDecl array_of = ctx.MkFuncDecl("array_of", T, T);
            Expr root = ctx.MkConst("root", T);

            Expr x = ctx.MkConst("x", T);
            Expr y = ctx.MkConst("y", T);
            Expr z = ctx.MkConst("z", T);

            BoolExpr[] axioms = new BoolExpr[] {
                ctx.MkForall(new Expr[] { x }, subtype[x, x]),
                ctx.MkForall(new Expr[] { x, y , z }, ctx.MkImplies(ctx.MkAnd((BoolExpr)subtype[x,y], (BoolExpr)subtype[y,z]), (BoolExpr)subtype[x,z])),
                ctx.MkForall(new Expr[] { x, y }, ctx.MkImplies(ctx.MkAnd((BoolExpr)subtype[x, y], (BoolExpr)subtype[y,x]), ctx.MkEq(x, y))),
                ctx.MkForall(new Expr[] { x, y, z }, ctx.MkImplies(ctx.MkAnd((BoolExpr)subtype[x,y],(BoolExpr)subtype[x,z]),
                                                                   ctx.MkOr((BoolExpr)subtype[y,z], (BoolExpr)subtype[z,y]))),
                ctx.MkForall(new Expr[] { x, y }, ctx.MkImplies((BoolExpr)subtype[x,y], (BoolExpr)subtype[array_of[x], array_of[y]])),
                ctx.MkForall(new Expr[] { x }, (BoolExpr) subtype[root, x])
            };

            Solver s = ctx.MkSolver();
            s.Assert(axioms);
            Console.WriteLine(s);
            Console.WriteLine(s.Check());
            Expr[] universe = s.Model.SortUniverse(T);
            foreach (var e in universe)
                Console.WriteLine(e);
            Console.WriteLine(s.Model);
        }
    }

        public static void WriteExprToDisk(BoolExpr expr, string exprName, string path)
        {
            // Convert the expr to a SMT-LIB formatted string
            var exprArray = new BoolExpr[0];
            var output = Z3.Context.BenchmarkToSMTString(exprName, "QF_AUFLIRA", "unknown", "", exprArray, expr);

            if (File.Exists(path))
            {
            //    // Note that no lock is put on the
            //    // file and the possibility exists
            //    // that another process could do
            //    // something with it between
            //    // the calls to Exists and Delete.
                File.Delete(path);
            }

            //// Create the file.
            using (FileStream fs = File.Create(path))
            {
                Byte[] info = new UTF8Encoding(true).GetBytes(output);
                // Write the SMT string to the file
                fs.Write(info, 0, info.Length);
            }
        }

        /// <summary>
        /// Query the fixedpoint solver.
        /// A query is a conjunction of constraints. The constraints may include the recursively defined relations.
        /// The query is satisfiable if there is an instance of the query variables and a derivation for it.
        /// The query is unsatisfiable if there are no derivations satisfying the query variables. 
        /// </summary>        
        public Status Query(BoolExpr query)
        {
            Contract.Requires(query != null);

            Context.CheckContextMatch(query);
            Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query(Context.nCtx, NativeObject, query.NativeObject);
            switch (r)
            {
                case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
                case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
                default: return Status.UNKNOWN;
            }
        }

 internal void AssertBool(BoolExpr row)
 {
     _optSolver.Assert(row);
 }

 BoolExpr[] ToBoolExprs(ASTVector v)
 {
     uint n = v.Size;
     BoolExpr[] res = new BoolExpr[n];
     for (uint i = 0; i < n; i++)
         res[i] = new BoolExpr(Context, v[i].NativeObject);
     return res;
 }

 /// <summary>
 /// Convert benchmark given as set of axioms, rules and queries to a string.
 /// </summary>                
 public string ToString(BoolExpr[] queries)
 {
     return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
                      AST.ArrayLength(queries), AST.ArrayToNative(queries));
 }

        /// <summary>
        /// Assert a constraint into the solver, and track it (in the unsat) core 
        /// using the Boolean constant p. 
        /// </summary>
        /// <remarks>
        /// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
        /// Both APIs can be used in the same solver. The unsat core will contain a combination
        /// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/> 
        /// and the Boolean literals
        /// provided using <see cref="Check"/> with assumptions.
        /// </remarks>        
        public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
        {
            Contract.Requires(constraint != null);
            Contract.Requires(p != null);
            Context.CheckContextMatch(constraint);
            Context.CheckContextMatch(p);

            Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
        }

        /// <summary>
        /// Convert a benchmark into an SMT-LIB formatted string.
        /// </summary>
        /// <param name="name">Name of the benchmark. The argument is optional.</param>
        /// <param name="logic">The benchmark logic. </param>
        /// <param name="status">The status string (sat, unsat, or unknown)</param>
        /// <param name="attributes">Other attributes, such as source, difficulty or category.</param>
        /// <param name="assumptions">Auxiliary assumptions.</param>
        /// <param name="formula">Formula to be checked for consistency in conjunction with assumptions.</param>
        /// <returns>A string representation of the benchmark.</returns>
        public string BenchmarkToSMTString(string name, string logic, string status, string attributes,
                                           BoolExpr[] assumptions, BoolExpr formula)
        {
            Contract.Requires(assumptions != null);
            Contract.Requires(formula != null);
            Contract.Ensures(Contract.Result<string>() != null);

            return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
                                            (uint)assumptions.Length, AST.ArrayToNative(assumptions),
                                            formula.NativeObject);
        }

        /// <summary>    
        ///  Create an expression representing an if-then-else: <c>ite(t1, t2, t3)</c>.
        /// </summary>
        /// <param name="t1">An expression with Boolean sort</param>
        /// <param name="t2">An expression </param>
        /// <param name="t3">An expression with the same sort as <paramref name="t2"/></param>
        public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
        {
            Contract.Requires(t1 != null);
            Contract.Requires(t2 != null);
            Contract.Requires(t3 != null);
            Contract.Ensures(Contract.Result<Expr>() != null);

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            CheckContextMatch(t3);
            return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
        }

 /// <summary>
 /// Create a pseudo-Boolean less-or-equal constraint.
 /// </summary>
 public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
 {
     Contract.Requires(args != null);
        Contract.Requires(coeffs != null);
        Contract.Requires(args.Length == coeffs.Length);
        Contract.Requires(Contract.Result<BoolExpr[]>() != null);
        CheckContextMatch(args);
        return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
                                                   AST.ArrayToNative(args),
                                                   coeffs, k));
 }