import java.util.*;
import com.microsoft.z3.*;
import java.io.BufferedReader;
import java.io.FileReader;
import java.io.IOException;
import java.io.BufferedReader;
import java.io.FileInputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.nio.charset.StandardCharsets;
import java.nio.file.Files;
import java.nio.file.Paths;




class JavaExample1
{
     @SuppressWarnings("serial")
        class TestFailedException extends Exception
        {
        public TestFailedException()
        {
            super("Check FAILED");
        }
        };

    Model check(Context ctx, BoolExpr f, Status sat) throws TestFailedException
        {
        Solver s = ctx.mkSolver();
        s.add(f);
        if (s.check() != sat)
            throw new TestFailedException();
        if (sat == Status.SATISFIABLE)
            return s.getModel();
        else
            return null;
        }

 //  Shows how to read an SMT2 file.

void smt2FileTest(String filename)
    {
        Date before = new Date();

        System.out.println("SMT2 File test ");
        System.gc();

    System.out.println("Filename ="+filename);


        {
            HashMap<String, String> cfg = new HashMap<String, String>();
            cfg.put("model", "true");
            Context ctx = new Context(cfg);
            BoolExpr a = ctx.mkAnd(ctx.parseSMTLIB2File(filename, null, null, null, null));

            long t_diff = ((new Date()).getTime() - before.getTime()) / 1000;

            System.out.println("SMT2 file read time: " + t_diff + " sec");

            // Iterate over the formula.

            LinkedList<Expr> q = new LinkedList<Expr>();
            q.add(a);
            int cnt = 0;
            while (q.size() > 0)
            {
                AST cur = (AST) q.removeFirst();
                cnt++;

                if (cur.getClass() == Expr.class)
                    if (!(cur.isVar()))
                        for (Expr c : ((Expr) cur).getArgs())
                            q.add(c);
            }
            System.out.println(cnt + " ASTs");
        }

        long t_diff = ((new Date()).getTime() - before.getTime()) / 1000;
        System.out.println("SMT2 file test took " + t_diff + " sec");
    }

//  Demonstrates how to use the SMTLIB parser.

    public void parserExample1(Context ctx) throws TestFailedException
    {
        System.out.println("ParserExample1");
        Log.append("ParserExample1");

        BoolExpr f = ctx.parseSMTLIB2String(
                "(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))",
                null, null, null, null)[0];
        System.out.println("formula " + f);

        @SuppressWarnings("unused")
        Model m = check(ctx, f, Status.SATISFIABLE);
    }

    public void parserExample2(Context ctx) throws TestFailedException
    {
        System.out.println("ParserExample2");
        Log.append("ParserExample2");

        Symbol[] declNames = { ctx.mkSymbol("a"), ctx.mkSymbol("b") };
        FuncDecl a = ctx.mkConstDecl(declNames[0], ctx.mkIntSort());
        FuncDecl b = ctx.mkConstDecl(declNames[1], ctx.mkIntSort());
        FuncDecl[] decls = new FuncDecl[] { a, b };

        BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null,
                declNames, decls)[0];
        System.out.println("formula: " + f);
        check(ctx, f, Status.SATISFIABLE);
    }


    public static void main(String[] args)
    {
        JavaExample1 p = new JavaExample1();


            com.microsoft.z3.Global.ToggleWarningMessages(true);
            Log.open("test.log");

            HashMap<String, String> cfg = new HashMap<String, String>();
                cfg.put("model", "true");
                Context ctx = new Context(cfg);

            String contents="";
            try
            {
             contents = new String(Files.readAllBytes(Paths.get("file.txt")));
            }
            catch(IOException e)
            {
            e.printStackTrace();
            }

            System.out.println(contents);

            try
            {
                p.smt2FileTest(contents);
            }
            catch(Exception e)
            {
                e.printStackTrace();
            }


    }


}