Commit 92e6dbd1 authored by phlo's avatar phlo

updated for boolector >= 3.2.0

parent 80e8d03c
#include "boolector.hh"
#include "shell.hh"
#include "smtlib.hh"
#include "trace.hh"
namespace ConcuBinE {
......@@ -29,6 +30,13 @@ std::string Boolector::version () const
return version;
}
// Boolector::formula ----------------------------------------------------------
std::string Boolector::formula (Encoder & encoder) const
{
return Solver::formula(encoder) + smtlib::check_sat() + eol;
}
//------------------------------------------------------------------------------
// public member functions inherited from External
//------------------------------------------------------------------------------
......@@ -37,7 +45,11 @@ std::string Boolector::version () const
const std::vector<std::string> & Boolector::command () const
{
static const std::vector<std::string> cmd({name(), "--model-gen"});
static const std::vector<std::string> cmd({
name(),
"--model-gen",
"--output-format=btor"});
return cmd;
}
......
......@@ -25,6 +25,10 @@ public: //======================================================================
//
virtual std::string version () const;
// build formula from given encoding
//
virtual std::string formula (Encoder & encoder) const;
//----------------------------------------------------------------------------
// public member functions inherited from External
//----------------------------------------------------------------------------
......
......@@ -17,6 +17,13 @@ namespace ConcuBinE {
std::string BtorMC::name () const { return "btormc"; }
// BtorMC::formula -------------------------------------------------------------
std::string BtorMC::formula (Encoder & encoder) const
{
return Solver::formula(encoder);
}
// BtorMC::sat -----------------------------------------------------------------
bool BtorMC::sat (const std::string & formula, const size_t k)
......
......@@ -21,6 +21,10 @@ public: //======================================================================
//
virtual std::string name () const;
// build formula from given encoding
//
virtual std::string formula (Encoder & encoder) const;
// evaluate arbitrary formula
//
using Boolector::sat;
......
......@@ -39,10 +39,11 @@ std::string CVC4::version () const
std::string CVC4::formula (Encoder & encoder) const
{
return
External::formula(encoder) +
Solver::formula(encoder) +
smtlib::check_sat() +
eol +
smtlib::get_model();
smtlib::get_model() +
eol;
}
//------------------------------------------------------------------------------
......
......@@ -20,7 +20,7 @@ TEST_F(BtorMC, sat)
"3 bad 2\n"));
ASSERT_EQ(
"sat\n"
"b0 \n"
"b0\n"
"#0\n"
"0 1 x#0\n"
"@0\n"
......
......@@ -8,6 +8,7 @@
#include "mmap.hh"
#include "parser.hh"
#include "shell.hh"
#include "smtlib.hh"
#include "trace.hh"
namespace ConcuBinE::test {
......@@ -491,7 +492,9 @@ TEST_F(Main, solve_encoder_btor2)
TEST_F(Main, solve_encoder_smtlib_functional)
{
ASSERT_EQ(
fs::read("test/data/halt.t2.k10.functional.smt2"),
fs::read("test/data/halt.t2.k10.functional.smt2") +
smtlib::check_sat() +
eol,
shell::run({
bin,
solve,
......@@ -509,7 +512,9 @@ TEST_F(Main, solve_encoder_smtlib_functional)
TEST_F(Main, solve_encoder_smtlib_relational)
{
ASSERT_EQ(
fs::read("test/data/halt.t2.k10.relational.smt2"),
fs::read("test/data/halt.t2.k10.relational.smt2") +
smtlib::check_sat() +
eol,
shell::run({
bin,
solve,
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment