Commit 58377f1e authored by Martin Jonáš's avatar Martin Jonáš
Browse files

Call Boolector via Boost.

parent e8fc958e

CMakeLists.txt

+7 −2
Original line number Diff line number Diff line
@@ -37,8 +37,6 @@ antlr_target(SmtLibParser parser/smtlibv2-grammar/src/main/resources/SMTLIBv2.g4 
# include generated files in project environment

include_directories(${ANTLR_SmtLibParser_OUTPUT_DIR}/parser/smtlibv2-grammar/src/main/resources)



add_executable(formulaReducer main.cpp ${FORMULAREDUCER_SRC} ${ANTLR_SmtLibParser_CXX_OUTPUTS})



set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -Wall")

set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall")
@@ -51,8 +49,15 @@ endif(NOT LibZ3) 
include_directories(${LibZ3_INCLUDE_DIRS})

set(LIBS ${LIBS} ${LibZ3})



find_package(Boost COMPONENTS system filesystem REQUIRED)

include_directories(${Boost_INCLUDE_DIR})

link_directories(${Boost_LIBRARY_DIR})



set(LIBS ${LIBS} ${Boost_LIBRARIES})



find_package (Threads)



add_executable(formulaReducer main.cpp ${FORMULAREDUCER_SRC} ${ANTLR_SmtLibParser_CXX_OUTPUTS})

target_link_libraries(formulaReducer ${CMAKE_THREAD_LIBS_INIT})

target_link_libraries(formulaReducer ${LIBS} antlr4_static)

Solver.cpp

+38 −9
Original line number Diff line number Diff line
@@ -4,13 +4,9 @@ 
#include "FormulaReducer.h"

#include "ExprSimplifier.h"



#include<unistd.h>

#include<sys/wait.h>

#include<sys/prctl.h>

#include<signal.h>

#include<stdlib.h>

#include<string.h>

#include<stdio.h>

#include <cstdio>

#include <regex>

#include "boost/process.hpp"



Result Solver::Solve(const z3::expr &formula)

{
@@ -56,8 +52,41 @@ Result Solver::solveReduced(const z3::expr &formula, int bw) 
{

    FormulaReducer reducer;

    z3::expr reducedFormula = reducer.Reduce(formula, bw, true);

    std::cout << reducedFormula;

    std::cout << reducedFormula << std::endl;



    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);



    in << "(set-logic BV)" << std::endl;

    in << "(set-option :produce-models true)" << std::endl;

    in << "(assert " << reducedFormula << ")" << std::endl;

    in << "(check-sat)" << std::endl;

    in << "(get-model)" << std::endl;

    in << "(exit)" << std::endl;



    std::string line;

    std::getline(out, line);



    if (line == "sat")

    {

        std::cout << "The reduced formula is SAT" << std::endl;



        getline(out, line);

        //the solver has returned an assignment to some variables; use it

        if (line == "(model")

        {

            std::cout << "The model is available:" << std::endl;



            std::regex varRegex ("(\\w+)!(\\d|!)+(\\s|\\)|$)");

            while (c.running() && getline(out, line) && line != ")")

            {

                std::cout << line << std::endl;

            }

        }

    }



    c.wait();



    //TODO: Run Boolector

    return UNKNOWN;

}