Commit c89ed040 authored by phlo's avatar phlo

moved encoding from constructor to Encoder::str()

parent 55536b48
......@@ -91,7 +91,13 @@ Encoder::Encoder (const Program::List::ptr & p, size_t b) :
// Encode::str -----------------------------------------------------------------
std::string Encoder::str () { return formula.str(); }
std::string Encoder::str ()
{
if (!formula.tellp())
encode();
return formula.str();
}
//------------------------------------------------------------------------------
// DEBUG
......
......@@ -451,9 +451,7 @@ struct Functional : public Encoder
// constructors
//----------------------------------------------------------------------------
Functional (const Program::List::ptr & programs,
size_t bound,
bool encode = true);
using Encoder::Encoder;
//----------------------------------------------------------------------------
// private member functions
......@@ -525,9 +523,7 @@ struct Relational : public Encoder
// constructors
//----------------------------------------------------------------------------
Relational (const Program::List::ptr & programs,
size_t bound,
bool encode = true);
using Encoder::Encoder;
//----------------------------------------------------------------------------
// private member functions
......@@ -807,9 +803,7 @@ struct Encoder : public ConcuBinE::Encoder
// constructors
//----------------------------------------------------------------------------
Encoder (const Program::List::ptr & programs,
size_t bound,
bool encode = true);
Encoder (const Program::List::ptr & programs, size_t bound);
//----------------------------------------------------------------------------
// private member functions
......
......@@ -163,7 +163,7 @@ const std::string Encoder::msb = std::to_string(word_size - 1);
// constructors
//------------------------------------------------------------------------------
Encoder::Encoder (const Program::List::ptr & p, const size_t b, const bool e) :
Encoder::Encoder (const Program::List::ptr & p, const size_t b) :
ConcuBinE::Encoder(p, b),
node(1)
{
......@@ -176,8 +176,6 @@ Encoder::Encoder (const Program::List::ptr & p, const size_t b, const bool e) :
if (program[pc].is_unary())
nids_const[program[pc].arg()];
});
if (e) encode();
}
//------------------------------------------------------------------------------
......
......@@ -10,18 +10,6 @@ namespace ConcuBinE::smtlib {
// smtlib::Functional
//==============================================================================
//------------------------------------------------------------------------------
// constructors
//------------------------------------------------------------------------------
Functional::Functional (const Program::List::ptr & p,
const size_t b,
const bool e) :
Encoder(p, b)
{
if (e) encode();
}
//------------------------------------------------------------------------------
// functions
//------------------------------------------------------------------------------
......
......@@ -72,18 +72,6 @@ Relational::State::operator std::string () const
// smtlib::Relational
//==============================================================================
//------------------------------------------------------------------------------
// constructors
//------------------------------------------------------------------------------
Relational::Relational (const Program::List::ptr & p,
const size_t b,
const bool e) :
Encoder(p, b)
{
if (e) Encoder::encode();
}
//------------------------------------------------------------------------------
// member functions
//------------------------------------------------------------------------------
......
......@@ -25,8 +25,7 @@ struct Encoder: public ::testing::Test
init_encoder(
std::make_unique<Impl>(
std::make_shared<Program::List>(programs),
bound,
false));
bound));
}
Program create_program (const std::string code)
......
......@@ -242,23 +242,23 @@ TEST_F(btor2_Encoder, load)
word_t address = 0;
ASSERT_EQ(encoder->nids_load[thread][address], encoder->load(address));
ASSERT_EQ(expected_load(nid, address), encoder->str());
ASSERT_EQ(expected_load(nid, address), encoder->formula.str());
encoder->formula.str("");
// another load with the same address
ASSERT_EQ(encoder->nids_load[thread][address], encoder->load(address));
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
// another load with a different address
address = 1;
ASSERT_EQ(encoder->nids_load[thread][address], encoder->load(address));
ASSERT_EQ(expected_load(nid, address), encoder->str());
ASSERT_EQ(expected_load(nid, address), encoder->formula.str());
encoder->formula.str("");
// another load from a different thread
thread = 1;
ASSERT_EQ(encoder->nids_load[thread][address], encoder->load(address));
ASSERT_EQ(expected_load(nid, address), encoder->str());
ASSERT_EQ(expected_load(nid, address), encoder->formula.str());
}
TEST_F(btor2_Encoder, load_indirect)
......@@ -274,21 +274,21 @@ TEST_F(btor2_Encoder, load_indirect)
ASSERT_EQ(
encoder->nids_load_indirect[thread][address],
encoder->load(address, true));
ASSERT_EQ(expected_load_indirect(nid, address), encoder->str());
ASSERT_EQ(expected_load_indirect(nid, address), encoder->formula.str());
encoder->formula.str("");
// another load with the same address
ASSERT_EQ(
encoder->nids_load_indirect[thread][address],
encoder->load(address, true));
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
// another load with a different address
address = 1;
ASSERT_EQ(
encoder->nids_load_indirect[thread][address],
encoder->load(address, true));
ASSERT_EQ(expected_load_indirect(nid, address), encoder->str());
ASSERT_EQ(expected_load_indirect(nid, address), encoder->formula.str());
encoder->formula.str("");
// another load from a different thread
......@@ -296,7 +296,7 @@ TEST_F(btor2_Encoder, load_indirect)
ASSERT_EQ(
encoder->nids_load_indirect[thread][address],
encoder->load(address, true));
ASSERT_EQ(expected_load_indirect(nid, address), encoder->str());
ASSERT_EQ(expected_load_indirect(nid, address), encoder->formula.str());
}
// btor2::Encoder::declare_sorts ===============================================
......@@ -680,7 +680,7 @@ TEST_F(btor2_Encoder, declare_block_empty)
{
encoder->declare_block();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// btor2::Encoder::declare_halt ================================================
......@@ -727,7 +727,7 @@ TEST_F(btor2_Encoder, declare_halt_empty)
{
encoder->declare_halt();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// btor2::Encoder::declare_heap ================================================
......@@ -798,7 +798,7 @@ TEST_F(btor2_Encoder, declare_exit_flag_empty)
{
encoder->declare_exit_flag();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// btor2::Encoder::declare_exit_code ===========================================
......@@ -1009,7 +1009,7 @@ TEST_F(btor2_Encoder, define_check)
TEST_F(btor2_Encoder, define_check_empty)
{
encoder->define_check();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// btor2::Encoder::define_accu =================================================
......@@ -2548,7 +2548,7 @@ TEST_F(btor2_Encoder, define_block)
TEST_F(btor2_Encoder, define_block_empty)
{
encoder->define_block();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// btor2::Encoder::define_halt =================================================
......@@ -2631,7 +2631,7 @@ TEST_F(btor2_Encoder, define_halt)
TEST_F(btor2_Encoder, define_halt_empty)
{
encoder->define_halt();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// btor2::Encoder::define_heap =================================================
......@@ -2877,7 +2877,7 @@ TEST_F(btor2_Encoder, define_exit_flag)
TEST_F(btor2_Encoder, define_exit_flag_empty)
{
encoder->define_exit_flag();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// btor2::Encoder::define_exit_code ============================================
......@@ -3272,7 +3272,7 @@ TEST_F(btor2_Encoder, define_checkpoint_constraints)
TEST_F(btor2_Encoder, define_checkpoint_constraints_empty)
{
encoder->define_checkpoint_constraints();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// btor2::Encoder::define_halt_constraints =====================================
......@@ -3326,7 +3326,7 @@ TEST_F(btor2_Encoder, define_halt_constraints)
TEST_F(btor2_Encoder, define_halt_constraints_empty)
{
encoder->define_checkpoint_constraints();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// btor2::Encoder::define_bound ================================================
......@@ -3866,7 +3866,7 @@ TEST_F(btor2_Encoder, JMP)
Instruction::Jmp jmp {Type::none, 0};
ASSERT_EQ("", encoder->encode(jmp));
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
TEST_F(btor2_Encoder, JZ)
......@@ -4212,7 +4212,7 @@ TEST_F(btor2_Encoder, EXIT)
Instruction::Exit exit {Type::none, 1};
ASSERT_EQ(encoder->nids_const[1], encoder->encode(exit));
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
} // namespace ConcuBinE::test
......@@ -610,7 +610,7 @@ TEST_F(smtlib_Encoder, declare_block_empty)
{
encoder->declare_block();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::declare_halt ===============================================
......@@ -649,7 +649,7 @@ TEST_F(smtlib_Encoder, declare_halt_empty)
{
encoder->declare_halt();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::declare_heap ===============================================
......@@ -707,7 +707,7 @@ TEST_F(smtlib_Encoder, declare_exit_flag_empty)
{
encoder->declare_exit_flag();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::declare_exit_code ==========================================
......@@ -896,7 +896,7 @@ TEST_F(smtlib_Encoder, declare_check_empty)
{
encoder->declare_check();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::init_accu ==================================================
......@@ -1154,7 +1154,7 @@ TEST_F(smtlib_Encoder, init_block_empty)
{
encoder->init_block();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::init_halt ==================================================
......@@ -1193,7 +1193,7 @@ TEST_F(smtlib_Encoder, init_halt_empty)
{
encoder->init_halt();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::init_exit_flag =============================================
......@@ -1225,7 +1225,7 @@ TEST_F(smtlib_Encoder, init_exit_flag_empty)
{
encoder->init_exit_flag();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::init_states ================================================
......@@ -1416,7 +1416,7 @@ TEST_F(smtlib_Encoder, define_check_empty)
{
encoder->define_check();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::define_scheduling_constraints ==============================
......@@ -1679,7 +1679,7 @@ TEST_F(smtlib_Encoder, define_checkpoint_constraints_empty)
{
encoder->define_checkpoint_constraints();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::define_halt_constraints ====================================
......@@ -1719,7 +1719,7 @@ TEST_F(smtlib_Encoder, define_halt_constraints_empty)
{
encoder->define_halt_constraints();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::encode =====================================================
......
......@@ -701,7 +701,7 @@ TEST_F(smtlib_Functional, define_block_empty)
{
encoder->define_block();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Functional::define_halt =============================================
......@@ -747,7 +747,7 @@ TEST_F(smtlib_Functional, define_halt_empty)
{
encoder->define_halt();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Functional::define_heap =============================================
......@@ -859,7 +859,7 @@ TEST_F(smtlib_Functional, define_exit_flag_empty)
{
encoder->define_exit_flag();
ASSERT_EQ("", encoder->str());
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Functional::define_exit_code ========================================
......
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