Commit 59a422a9 authored by name's avatar name
Browse files

Make compatible with newer Z3 and Boolector

parent 638c9854

ExprSimplifier.cpp

+3 −3
Original line number Diff line number Diff line
@@ -178,7 +178,7 @@ expr ExprSimplifier::CanonizeBoundVariables(const expr &e) 
	Z3_ast quantAst = Z3_mk_quantifier(

	    *context,

	    Z3_is_quantifier_forall(*context, ast),

	    Z3_get_quantifier_weight(*context, ast),

	    1,

	    0,

	    {},

	    numBound,
@@ -282,7 +282,7 @@ expr ExprSimplifier::modifyQuantifierBody(const expr& quantifierExpr, const expr 
    Z3_ast newAst = Z3_mk_quantifier(

	*context,

	Z3_is_quantifier_forall(*context, ast),

	Z3_get_quantifier_weight(*context, ast),

	1,

	0,

	{},

	numBound,
@@ -310,7 +310,7 @@ expr ExprSimplifier::flipQuantifierAndModifyBody(const expr& quantifierExpr, con 
    Z3_ast newAst = Z3_mk_quantifier(

	*context,

	!Z3_is_quantifier_forall(*context, ast),

	Z3_get_quantifier_weight(*context, ast),

	1,

	0,

	{},

	numBound,

Solver.cpp

+10 −10
Original line number Diff line number Diff line
@@ -33,14 +33,14 @@ Result Solver::Solve(const z3::expr &formula) 
        std::cout << "Solving the formula reduced to " << i << " bits" << std::endl;

        Result result = solveReduced(canonized, i, originalFormulaStats.maxBitWidth);



        if (result == SAT)

	if (i == originalFormulaStats.maxBitWidth)

        {

            return SAT;

            return UNKNOWN;

        }



        if (i == originalFormulaStats.maxBitWidth)

        if (result == SAT)

        {

            return result;

            return SAT;

        }

    }
@@ -86,7 +86,7 @@ Result Solver::solveReduced(const z3::expr &formula, int bw, int originalBw) 


    boost::process::opstream in;

    boost::process::ipstream out;

    boost::process::child c(boost::process::search_path("boolector"), "--quant:dual=0", boost::process::std_out > out, boost::process::std_in < in);

    boost::process::child c(boost::process::search_path("boolector"), "--quant-dual=0", boost::process::std_out > out, boost::process::std_in < in);



    Z3_set_ast_print_mode(formula.ctx(), Z3_PRINT_SMTLIB_FULL);
@@ -112,10 +112,10 @@ Result Solver::solveReduced(const z3::expr &formula, int bw, int originalBw) 
    std::string line;

    std::getline(out, line);



    if (bw == originalBw && (line == "sat" || line == "unsat"))

    {

      return line == "sat" ? SAT : UNSAT;

    }

    //if (bw == originalBw && (line == "sat" || line == "unsat"))

    //{

    //  return line == "sat" ? SAT : UNSAT;

    //}



    if (line == "sat")

    {
@@ -184,7 +184,7 @@ Result Solver::solveReduced(const z3::expr &formula, int bw, int originalBw) 
            std::vector<std::string> boundVars;



            z3::expr substituted = simplifier.SubstituteExistentials(origFormula, model, boundVars);



	    std::cout << substituted << std::endl;

            if (verify(substituted, "boolector"))

            {

                return SAT;