Commit ac6912ac authored by phlo's avatar phlo

added default argument for External::solve

parent cb75c7d1
......@@ -113,7 +113,8 @@ struct External : Solver
virtual bool sat (const std::string & formula);
virtual Trace::ptr solve (Encoder & encoder, const std::string & constraints);
virtual Trace::ptr solve (Encoder & encoder,
const std::string & constraints = "");
// build command line for the specific solver
//
......
......@@ -13,7 +13,6 @@ namespace ConcuBinE::test {
struct Boolector : public ::testing::Test
{
std::string constraints;
ConcuBinE::Boolector boolector;
Encoder::ptr encoder;
Program::List::ptr programs = std::make_shared<Program::List>();
......@@ -51,7 +50,7 @@ TEST_F(Boolector, solve_check)
encoder = std::make_unique<smtlib::Functional>(programs, 16);
trace = boolector.solve(*encoder, constraints);
trace = boolector.solve(*encoder);
std::cout << "time to solve = " << boolector.time << "ms" << eol;
......@@ -78,7 +77,7 @@ TEST_F(Boolector, solve_cas)
encoder = std::make_unique<smtlib::Functional>(programs, 16);
trace = boolector.solve(*encoder, constraints);
trace = boolector.solve(*encoder);
std::cout << "time to solve = " << boolector.time << "ms" << eol;
......@@ -107,7 +106,7 @@ TEST_F(Boolector, print_model_check)
encoder = std::make_unique<smtlib::Functional>(programs, 16);
std::string formula = boolector.build_formula(*encoder, constraints);
std::string formula = boolector.build_formula(*encoder, "");
bool sat = boolector.sat(formula);
......@@ -129,12 +128,12 @@ TEST_F(Boolector, print_model_cas)
encoder = std::make_unique<smtlib::Functional>(programs, 16);
std::string formula = boolector.build_formula(*encoder, constraints);
std::string formula = boolector.build_formula(*encoder, "");
bool sat = boolector.sat(formula);
std::ofstream outfile("/tmp/boolector.cas.out");
outfile << boolector.std_out.str();
std::ofstream out("/tmp/boolector.cas.out");
out << boolector.std_out.str();
ASSERT_TRUE(sat);
}
......
......@@ -50,7 +50,6 @@ TEST_F(BtorMC, unsat)
TEST_F(BtorMC, solve_check)
{
// concurrent increment using CHECK
std::string constraints;
std::string increment_0 = "data/increment.check.thread.0.asm";
std::string increment_n = "data/increment.check.thread.n.asm";
......@@ -61,7 +60,7 @@ TEST_F(BtorMC, solve_check)
encoder = std::make_unique<btor2::Encoder>(programs, 16);
trace = btormc.solve(*encoder, constraints);
trace = btormc.solve(*encoder);
std::cout << "time to solve = " << btormc.time << "ms" << eol;
......@@ -79,7 +78,6 @@ TEST_F(BtorMC, solve_check)
TEST_F(BtorMC, solve_cas)
{
// concurrent increment using CAS
std::string constraints;
std::string increment = "data/increment.cas.asm";
programs = std::make_shared<Program::List>();
......@@ -89,7 +87,7 @@ TEST_F(BtorMC, solve_cas)
encoder = std::make_unique<btor2::Encoder>(programs, 16);
trace = btormc.solve(*encoder, constraints);
trace = btormc.solve(*encoder);
std::cout << "time to solve = " << btormc.time << "ms" << eol;
......@@ -122,8 +120,8 @@ TEST_F(BtorMC, print_model_check)
bool sat = btormc.sat(formula);
std::ofstream trace_file("/tmp/btormc.check.out");
trace_file << btormc.std_out.str();
std::ofstream out("/tmp/btormc.check.out");
out << btormc.std_out.str();
ASSERT_TRUE(sat);
}
......@@ -144,8 +142,8 @@ TEST_F(BtorMC, print_model_cas)
bool sat = btormc.sat(formula);
std::ofstream trace_file("/tmp/btormc.cas.out");
trace_file << btormc.std_out.str();
std::ofstream out("/tmp/btormc.cas.out");
out << btormc.std_out.str();
ASSERT_TRUE(sat);
}
......
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