Commit 5d6bb4c4 authored by phlo's avatar phlo

updated BTOR2 encoding scheme

* added store buffer
parent 7de7aa6f
......@@ -4,22 +4,39 @@ using namespace std;
const string Encoder::accu_sym = "accu";
const string Encoder::mem_sym = "mem";
const string Encoder::sb_adr_sym = "sb-adr";
const string Encoder::sb_val_sym = "sb-val";
const string Encoder::sb_full_sym = "sb-full";
const string Encoder::stmt_sym = "stmt";
const string Encoder::block_sym = "block";
const string Encoder::heap_sym = "heap";
const string Encoder::exit_flag_sym = "exit";
const string Encoder::exit_code_sym = "exit-code";
const string Encoder::thread_sym = "thread";
const string Encoder::flush_sym = "flush";
const string Encoder::stmt_sym = "stmt";
const string Encoder::exec_sym = "exec";
const string Encoder::cas_sym = "cas";
const string Encoder::block_sym = "block";
const string Encoder::flush_sym = "flush";
const string Encoder::check_sym = "check";
const string Encoder::exit_flag_sym = "exit";
const string Encoder::cas_sym = "cas";
const string Encoder::accu_comment = "accu variables";
const string Encoder::mem_comment = "mem variables";
const string Encoder::sb_adr_comment = "store buffer address variables";
const string Encoder::sb_val_comment = "store buffer value variables";
const string Encoder::sb_full_comment = "store buffer full variables";
const string Encoder::stmt_comment = "statement activation variables";
const string Encoder::block_comment = "blocking variables";
const string Encoder::heap_comment = "heap variable";
const string Encoder::exit_flag_comment = "exit flag variable";
const string Encoder::exit_code_comment = "exit code variable";
const string Encoder::thread_comment = "thread activation variables";
const string Encoder::exec_comment = "statement execution variables";
const string Encoder::flush_comment = "store buffer flush variables";
const string Encoder::check_comment = "checkpoint variables";
const string Encoder::cas_comment = "CAS condition variables";
Encoder::Encoder (const Program_list_ptr p, bound_t b) :
programs(p),
......@@ -34,7 +51,7 @@ Encoder::Encoder (const Program_list_ptr p, bound_t b) :
// collect statements requiring an empty store buffer
if (op->requires_flush())
flush_pcs[thread].insert(pc);
flush_pcs[thread].push_back(pc);
// collect checkpoints
if (Check_ptr s = dynamic_pointer_cast<Check>(op))
......
This diff is collapsed.
This diff is collapsed.
......@@ -9,46 +9,63 @@ using namespace std;
const string SMTLib_Encoder::bv_sort = smtlib::bitvector(word_size);
const string SMTLib_Encoder::accu_comment =
"; accu states - " + accu_sym + "_<step>_<thread>";
smtlib::comment(
Encoder::accu_comment + " - " + accu_sym + "_<step>_<thread>" + eol);
const string SMTLib_Encoder::mem_comment =
"; mem states - " + mem_sym + "_<step>_<thread>";
smtlib::comment(
Encoder::mem_comment + " - " + mem_sym + "_<step>_<thread>" + eol);
const string SMTLib_Encoder::sb_adr_comment =
"; store buffer address states - " + sb_adr_sym + "_<step>_<thread>";
smtlib::comment(
Encoder::sb_adr_comment + " - " + sb_adr_sym + "_<step>_<thread>" + eol);
const string SMTLib_Encoder::sb_val_comment =
"; store buffer value states - " + sb_val_sym + "_<step>_<thread>";
smtlib::comment(
Encoder::sb_val_comment + " - " + sb_val_sym + "_<step>_<thread>" + eol);
const string SMTLib_Encoder::sb_full_comment =
"; store buffer full states - " + sb_full_sym + "_<step>_<thread>";
smtlib::comment(
Encoder::sb_full_comment + " - " + sb_full_sym + "_<step>_<thread>" + eol);
const string SMTLib_Encoder::stmt_comment =
"; statement activation variables - " + stmt_sym + "_<step>_<thread>_<pc>";
smtlib::comment(
Encoder::stmt_comment + " - " + stmt_sym + "_<step>_<thread>_<pc>" + eol);
const string SMTLib_Encoder::block_comment =
"; blocking variables - " + block_sym + "_<step>_<id>_<thread>";
smtlib::comment(
Encoder::block_comment + " - " + block_sym + "_<step>_<id>_<thread>" + eol);
const string SMTLib_Encoder::heap_comment =
"; heap state - " + heap_sym + "_<step>";
smtlib::comment(
Encoder::heap_comment + " - " + heap_sym + "_<step>" + eol);
const string SMTLib_Encoder::exit_flag_comment =
"; exit flag - " + exit_flag_sym + "_<step>";
smtlib::comment(
Encoder::exit_flag_comment + " - " + exit_flag_sym + "_<step>" + eol);
const string SMTLib_Encoder::exit_code_comment =
smtlib::comment(Encoder::exit_code_comment + eol);
const string SMTLib_Encoder::thread_comment =
"; thread activation variables - " + thread_sym + "_<step>_<thread>";
smtlib::comment(
Encoder::thread_comment + " - " + thread_sym + "_<step>_<thread>" + eol);
const string SMTLib_Encoder::exec_comment =
"; statement execution variables - " + exec_sym + "_<step>_<thread>_<pc>";
smtlib::comment(
Encoder::exec_comment + " - " + exec_sym + "_<step>_<thread>_<pc>" + eol);
const string SMTLib_Encoder::flush_comment =
"; store buffer flush variables - " + flush_sym + "_<step>_<thread>";
smtlib::comment(
Encoder::flush_comment + " - " + flush_sym + "_<step>_<thread>" + eol);
const string SMTLib_Encoder::check_comment =
"; checkpoint variables - " + check_sym + "_<step>_<id>";
smtlib::comment(
Encoder::check_comment + " - " + check_sym + "_<step>_<id>" + eol);
const string SMTLib_Encoder::cas_comment =
"; CAS condition - " + cas_sym + "_<step>_<thread>";
smtlib::comment(
Encoder::cas_comment + " - " + cas_sym + "_<step>_<thread>" + eol);
SMTLib_Encoder::SMTLib_Encoder (const Program_list_ptr p, bound_t b) :
Encoder(p, b),
......@@ -290,7 +307,7 @@ string SMTLib_Encoder::load (const word_t adr, const bool indirect)
void SMTLib_Encoder::declare_accu ()
{
if (verbose)
formula << accu_comment << eol;
formula << accu_comment;
iterate_threads([this] {
formula << smtlib::declare_bv_var(accu_var(), word_size) << eol;
......@@ -302,7 +319,7 @@ void SMTLib_Encoder::declare_accu ()
void SMTLib_Encoder::declare_mem ()
{
if (verbose)
formula << mem_comment << eol;
formula << mem_comment;
iterate_threads([this] {
formula << smtlib::declare_bv_var(mem_var(), word_size) << eol;
......@@ -314,7 +331,7 @@ void SMTLib_Encoder::declare_mem ()
void SMTLib_Encoder::declare_sb_adr ()
{
if (verbose)
formula << sb_adr_comment << eol;
formula << sb_adr_comment;
iterate_threads([this] {
formula << smtlib::declare_bv_var(sb_adr_var(), word_size) << eol;
......@@ -326,7 +343,7 @@ void SMTLib_Encoder::declare_sb_adr ()
void SMTLib_Encoder::declare_sb_val ()
{
if (verbose)
formula << sb_val_comment << eol;
formula << sb_val_comment;
iterate_threads([this] {
formula << smtlib::declare_bv_var(sb_val_var(), word_size) << eol;
......@@ -338,7 +355,7 @@ void SMTLib_Encoder::declare_sb_val ()
void SMTLib_Encoder::declare_sb_full ()
{
if (verbose)
formula << sb_full_comment << eol;
formula << sb_full_comment;
iterate_threads([this] {
formula << smtlib::declare_bool_var(sb_full_var()) << eol;
......@@ -350,7 +367,7 @@ void SMTLib_Encoder::declare_sb_full ()
void SMTLib_Encoder::declare_stmt ()
{
if (verbose)
formula << stmt_comment << eol;
formula << stmt_comment;
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
......@@ -366,7 +383,7 @@ void SMTLib_Encoder::declare_block ()
return;
if (verbose)
formula << block_comment << eol;
formula << block_comment;
for (const auto & [s, threads] : check_pcs)
for (const auto & t : threads)
......@@ -380,7 +397,7 @@ void SMTLib_Encoder::declare_block ()
void SMTLib_Encoder::declare_heap ()
{
if (verbose)
formula << heap_comment << eol;
formula << heap_comment;
formula
<< smtlib::declare_array_var(heap_var(), bv_sort, bv_sort)
......@@ -393,7 +410,7 @@ void SMTLib_Encoder::declare_exit_flag ()
return;
if (verbose)
formula << exit_flag_comment << eol;
formula << exit_flag_comment;
formula << smtlib::declare_bool_var(exit_flag_var()) << eol << eol;
}
......@@ -401,7 +418,7 @@ void SMTLib_Encoder::declare_exit_flag ()
void SMTLib_Encoder::declare_exit_code ()
{
if (verbose)
formula << smtlib::comment("exit code") << eol;
formula << exit_code_comment;
formula << smtlib::declare_bv_var(exit_code_sym, word_size) << eol << eol;
}
......@@ -429,7 +446,7 @@ void SMTLib_Encoder::declare_states ()
void SMTLib_Encoder::declare_thread ()
{
if (verbose)
formula << thread_comment << eol;
formula << thread_comment;
iterate_threads([this] {
formula << smtlib::declare_bool_var(thread_var()) << eol;
......@@ -441,7 +458,7 @@ void SMTLib_Encoder::declare_thread ()
void SMTLib_Encoder::declare_exec ()
{
if (verbose)
formula << exec_comment << eol;
formula << exec_comment;
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
......@@ -454,7 +471,7 @@ void SMTLib_Encoder::declare_exec ()
void SMTLib_Encoder::declare_flush ()
{
if (verbose)
formula << flush_comment << eol;
formula << flush_comment;
iterate_threads([this] {
formula << smtlib::declare_bool_var(flush_var()) << eol;
......@@ -469,7 +486,7 @@ void SMTLib_Encoder::declare_check ()
return;
if (verbose)
formula << check_comment << eol;
formula << check_comment;
for (const auto & s : check_pcs)
formula << smtlib::declare_bool_var(check_var(step, s.first)) << eol;
......@@ -484,7 +501,7 @@ void SMTLib_Encoder::declare_cas_vars ()
return;
if (verbose)
formula << cas_comment << eol;
formula << cas_comment;
iterate_threads([this] {
if (cas_threads.find(thread) != cas_threads.end())
......@@ -517,7 +534,7 @@ void SMTLib_Encoder::declare_transitions ()
void SMTLib_Encoder::init_accu ()
{
if (verbose)
formula << accu_comment << eol;
formula << accu_comment;
INIT_STATE(accu_var);
}
......@@ -525,7 +542,7 @@ void SMTLib_Encoder::init_accu ()
void SMTLib_Encoder::init_mem ()
{
if (verbose)
formula << mem_comment << eol;
formula << mem_comment;
INIT_STATE(mem_var);
}
......@@ -533,7 +550,7 @@ void SMTLib_Encoder::init_mem ()
void SMTLib_Encoder::init_sb_adr ()
{
if (verbose)
formula << sb_adr_comment << eol;
formula << sb_adr_comment;
INIT_STATE(sb_adr_var);
}
......@@ -541,7 +558,7 @@ void SMTLib_Encoder::init_sb_adr ()
void SMTLib_Encoder::init_sb_val ()
{
if (verbose)
formula << sb_val_comment << eol;
formula << sb_val_comment;
INIT_STATE(sb_val_var);
}
......@@ -549,7 +566,7 @@ void SMTLib_Encoder::init_sb_val ()
void SMTLib_Encoder::init_sb_full ()
{
if (verbose)
formula << sb_full_comment << eol;
formula << sb_full_comment;
iterate_threads([this] {
formula << smtlib::assertion(smtlib::lnot(sb_full_var())) << eol;
......@@ -561,7 +578,7 @@ void SMTLib_Encoder::init_sb_full ()
void SMTLib_Encoder::init_stmt ()
{
if (verbose)
formula << stmt_comment << eol;
formula << stmt_comment;
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
......@@ -579,7 +596,7 @@ void SMTLib_Encoder::init_block ()
return;
if (verbose)
formula << block_comment << eol;
formula << block_comment;
for (const auto & [c, threads] : check_pcs)
for (const auto & [t, pcs] : threads)
......@@ -594,7 +611,7 @@ void SMTLib_Encoder::init_exit_flag ()
return;
if (verbose)
formula << exit_flag_comment << eol;
formula << exit_flag_comment;
formula << smtlib::assertion(smtlib::lnot(exit_flag_var())) << eol << eol;
}
......@@ -619,7 +636,7 @@ void SMTLib_Encoder::init_states ()
void SMTLib_Encoder::define_exec ()
{
if (verbose)
formula << exec_comment << eol;
formula << exec_comment;
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
......@@ -637,7 +654,7 @@ void SMTLib_Encoder::define_check ()
return;
if (verbose)
formula << check_comment << eol;
formula << check_comment;
for (const auto & [c, threads] : check_pcs)
{
......@@ -790,14 +807,13 @@ void SMTLib_Encoder::encode ()
declare_states();
declare_transitions();
define_transitions();
if (step)
define_states();
else
init_states();
define_transitions();
define_constraints ();
}
}
......
......@@ -40,7 +40,7 @@ SMTLib_Encoder_Functional::SMTLib_Encoder_Functional (
void SMTLib_Encoder_Functional::define_accu ()
{
if (verbose)
formula << accu_comment << eol;
formula << accu_comment;
DEFINE_STATE(Update::accu, Types::accu, accu_var);
}
......@@ -48,7 +48,7 @@ void SMTLib_Encoder_Functional::define_accu ()
void SMTLib_Encoder_Functional::define_mem ()
{
if (verbose)
formula << mem_comment << eol;
formula << mem_comment;
DEFINE_STATE(Update::mem, Types::mem, mem_var);
}
......@@ -56,7 +56,7 @@ void SMTLib_Encoder_Functional::define_mem ()
void SMTLib_Encoder_Functional::define_sb_adr ()
{
if (verbose)
formula << sb_adr_comment << eol;
formula << sb_adr_comment;
DEFINE_STATE(Update::sb_adr, Types::write, sb_adr_var);
}
......@@ -64,7 +64,7 @@ void SMTLib_Encoder_Functional::define_sb_adr ()
void SMTLib_Encoder_Functional::define_sb_val ()
{
if (verbose)
formula << sb_val_comment << eol;
formula << sb_val_comment;
DEFINE_STATE(Update::sb_val, Types::write, sb_val_var);
}
......@@ -72,7 +72,7 @@ void SMTLib_Encoder_Functional::define_sb_val ()
void SMTLib_Encoder_Functional::define_sb_full ()
{
if (verbose)
formula << sb_full_comment << eol;
formula << sb_full_comment;
iterate_programs([this] (const Program & program) {
vector<string> args;
......@@ -99,7 +99,7 @@ void SMTLib_Encoder_Functional::define_sb_full ()
void SMTLib_Encoder_Functional::define_stmt ()
{
if (verbose)
formula << stmt_comment << eol;
formula << stmt_comment;
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
......@@ -150,7 +150,7 @@ void SMTLib_Encoder_Functional::define_block ()
return;
if (verbose)
formula << block_comment << eol;
formula << block_comment;
for (const auto & [c, threads] : check_pcs)
for (const auto & [t, pcs] : threads)
......@@ -180,7 +180,7 @@ void SMTLib_Encoder_Functional::define_block ()
void SMTLib_Encoder_Functional::define_heap ()
{
if (verbose)
formula << heap_comment << eol;
formula << heap_comment;
update = Update::heap;
......@@ -223,7 +223,7 @@ void SMTLib_Encoder_Functional::define_exit_flag ()
return;
if (verbose)
formula << exit_flag_comment << eol;
formula << exit_flag_comment;
vector<string> args {exit_flag_var(prev)};
......
......@@ -42,8 +42,8 @@ GTEST_FILTER += SMTLib_Test.*
GTEST_FILTER += SMTLib_Encoder_Test.*
GTEST_FILTER += SMTLib_Encoder_Functional_Test.*
GTEST_FILTER += SMTLib_Encoder_Relational_Test.*
# GTEST_FILTER += Btor2_Test.*
# GTEST_FILTER += Btor2_Encoder_Test.*
GTEST_FILTER += Btor2_Test.*
GTEST_FILTER += Btor2_Encoder_Test.*
# GTEST_FILTER += Thread_Test.*
# GTEST_FILTER += Simulator_Test.*
# GTEST_FILTER += Main_Test.*
......
This diff is collapsed.
This diff is collapsed.
......@@ -24,7 +24,7 @@ TEST_F(Encoder_Test, constructor)
reset_encoder();
for (const auto & pcs : encoder->flush_pcs)
ASSERT_EQ(set<word_t>({0}), pcs.second);
ASSERT_EQ(vector<word_t>({0}), pcs.second);
for (const auto & [id, threads] : encoder->check_pcs)
for (const auto & pcs : threads)
......@@ -51,7 +51,7 @@ TEST_F(Encoder_Test, constructor_flush_pcs)
reset_encoder();
for (const auto & pcs : encoder->flush_pcs)
ASSERT_EQ(set<word_t>({0, 1, 2}), pcs.second);
ASSERT_EQ(vector<word_t>({0, 1, 2}), pcs.second);
}
TEST_F(Encoder_Test, constructor_check_pcs)
......
This diff is collapsed.
......@@ -346,7 +346,7 @@ TEST_F(SMTLib_Encoder_Test, declare_accu)
encoder->declare_accu();
ASSERT_EQ(
"; accu states - accu_<step>_<thread>\n"
"; accu variables - accu_<step>_<thread>\n"
"(declare-fun accu_1_0 () (_ BitVec 16))\n"
"(declare-fun accu_1_1 () (_ BitVec 16))\n"
"(declare-fun accu_1_2 () (_ BitVec 16))\n"
......@@ -377,7 +377,7 @@ TEST_F(SMTLib_Encoder_Test, declare_mem)
encoder->declare_mem();
ASSERT_EQ(
"; mem states - mem_<step>_<thread>\n"
"; mem variables - mem_<step>_<thread>\n"
"(declare-fun mem_1_0 () (_ BitVec 16))\n"
"(declare-fun mem_1_1 () (_ BitVec 16))\n"
"(declare-fun mem_1_2 () (_ BitVec 16))\n"
......@@ -408,7 +408,7 @@ TEST_F(SMTLib_Encoder_Test, declare_sb_adr)
encoder->declare_sb_adr();
ASSERT_EQ(
"; store buffer address states - sb-adr_<step>_<thread>\n"
"; store buffer address variables - sb-adr_<step>_<thread>\n"
"(declare-fun sb-adr_1_0 () (_ BitVec 16))\n"
"(declare-fun sb-adr_1_1 () (_ BitVec 16))\n"
"(declare-fun sb-adr_1_2 () (_ BitVec 16))\n"
......@@ -439,7 +439,7 @@ TEST_F(SMTLib_Encoder_Test, declare_sb_val)
encoder->declare_sb_val();
ASSERT_EQ(
"; store buffer value states - sb-val_<step>_<thread>\n"
"; store buffer value variables - sb-val_<step>_<thread>\n"
"(declare-fun sb-val_1_0 () (_ BitVec 16))\n"
"(declare-fun sb-val_1_1 () (_ BitVec 16))\n"
"(declare-fun sb-val_1_2 () (_ BitVec 16))\n"
......@@ -470,7 +470,7 @@ TEST_F(SMTLib_Encoder_Test, declare_sb_full)
encoder->declare_sb_full();
ASSERT_EQ(
"; store buffer full states - sb-full_<step>_<thread>\n"
"; store buffer full variables - sb-full_<step>_<thread>\n"
"(declare-fun sb-full_1_0 () Bool)\n"
"(declare-fun sb-full_1_1 () Bool)\n"
"(declare-fun sb-full_1_2 () Bool)\n"
......@@ -597,7 +597,7 @@ TEST_F(SMTLib_Encoder_Test, declare_heap)
encoder->declare_heap();
ASSERT_EQ(
"; heap state - heap_<step>\n"
"; heap variable - heap_<step>\n"
"(declare-fun heap_1 () (Array (_ BitVec 16) (_ BitVec 16)))\n"
"\n",
encoder->str());
......@@ -623,7 +623,7 @@ TEST_F(SMTLib_Encoder_Test, declare_exit_flag)
encoder->declare_exit_flag();
ASSERT_EQ(
"; exit flag - exit_<step>\n"
"; exit flag variable - exit_<step>\n"
"(declare-fun exit_1 () Bool)\n"
"\n",
encoder->str());
......@@ -651,7 +651,7 @@ TEST_F(SMTLib_Encoder_Test, declare_exit_code)
encoder->declare_exit_code();
ASSERT_EQ(
"; exit code\n"
"; exit code variable\n"
"(declare-fun exit-code () (_ BitVec 16))\n"
"\n",
encoder->str());
......@@ -894,7 +894,7 @@ TEST_F(SMTLib_Encoder_Test, init_accu)
encoder->init_accu();
ASSERT_EQ(
"; accu states - accu_<step>_<thread>\n"
"; accu variables - accu_<step>_<thread>\n"
"(assert (= accu_0_0 #x0000))\n"
"(assert (= accu_0_1 #x0000))\n"
"(assert (= accu_0_2 #x0000))\n"
......@@ -925,7 +925,7 @@ TEST_F(SMTLib_Encoder_Test, init_mem)
encoder->init_mem();
ASSERT_EQ(
"; mem states - mem_<step>_<thread>\n"
"; mem variables - mem_<step>_<thread>\n"
"(assert (= mem_0_0 #x0000))\n"
"(assert (= mem_0_1 #x0000))\n"
"(assert (= mem_0_2 #x0000))\n"
......@@ -956,7 +956,7 @@ TEST_F(SMTLib_Encoder_Test, init_sb_adr)
encoder->init_sb_adr();
ASSERT_EQ(
"; store buffer address states - sb-adr_<step>_<thread>\n"
"; store buffer address variables - sb-adr_<step>_<thread>\n"
"(assert (= sb-adr_0_0 #x0000))\n"
"(assert (= sb-adr_0_1 #x0000))\n"
"(assert (= sb-adr_0_2 #x0000))\n"
......@@ -987,7 +987,7 @@ TEST_F(SMTLib_Encoder_Test, init_sb_val)
encoder->init_sb_val();
ASSERT_EQ(
"; store buffer value states - sb-val_<step>_<thread>\n"
"; store buffer value variables - sb-val_<step>_<thread>\n"
"(assert (= sb-val_0_0 #x0000))\n"
"(assert (= sb-val_0_1 #x0000))\n"
"(assert (= sb-val_0_2 #x0000))\n"
......@@ -1018,7 +1018,7 @@ TEST_F(SMTLib_Encoder_Test, init_sb_full)
encoder->init_sb_full();
ASSERT_EQ(
"; store buffer full states - sb-full_<step>_<thread>\n"
"; store buffer full variables - sb-full_<step>_<thread>\n"
"(assert (not sb-full_0_0))\n"
"(assert (not sb-full_0_1))\n"
"(assert (not sb-full_0_2))\n"
......@@ -1099,7 +1099,7 @@ TEST_F(SMTLib_Encoder_Test, init_exit_flag)
encoder->init_exit_flag();
ASSERT_EQ(
"; exit flag - exit_<step>\n"
"; exit flag variable - exit_<step>\n"
"(assert (not exit_0))\n"
"\n",
encoder->str());
......@@ -1132,19 +1132,19 @@ TEST_F(SMTLib_Encoder_Test, init_states)
ASSERT_EQ(
"; state variable initializations ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\n"
"\n"
"; accu states - accu_<step>_<thread>\n"
"; accu variables - accu_<step>_<thread>\n"
"(assert (= accu_0_0 #x0000))\n"
"\n"
"; mem states - mem_<step>_<thread>\n"
"; mem variables - mem_<step>_<thread>\n"
"(assert (= mem_0_0 #x0000))\n"
"\n"
"; store buffer address states - sb-adr_<step>_<thread>\n"
"; store buffer address variables - sb-adr_<step>_<thread>\n"
"(assert (= sb-adr_0_0 #x0000))\n"
"\n"
"; store buffer value states - sb-val_<step>_<thread>\n"
"; store buffer value variables - sb-val_<step>_<thread>\n"
"(assert (= sb-val_0_0 #x0000))\n"
"\n"
"; store buffer full states - sb-full_<step>_<thread>\n"
"; store buffer full variables - sb-full_<step>_<thread>\n"
"(assert (not sb-full_0_0))\n"
"\n"
"; statement activation variables - stmt_<step>_<thread>_<pc>\n"
......@@ -1190,19 +1190,19 @@ TEST_F(SMTLib_Encoder_Test, init_states_check_exit)
ASSERT_EQ(
"; state variable initializations ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\n"
"\n"
"; accu states - accu_<step>_<thread>\n"
"; accu variables - accu_<step>_<thread>\n"
"(assert (= accu_0_0 #x0000))\n"
"\n"
"; mem states - mem_<step>_<thread>\n"
"; mem variables - mem_<step>_<thread>\n"
"(assert (= mem_0_0 #x0000))\n"
"\n"
"; store buffer address states - sb-adr_<step>_<thread>\n"
"; store buffer address variables - sb-adr_<step>_<thread>\n"
"(assert (= sb-adr_0_0 #x0000))\n"
"\n"
"; store buffer value states - sb-val_<step>_<thread>\n"
"; store buffer value variables - sb-val_<step>_<thread>\n"
"(assert (= sb-val_0_0 #x0000))\n"
"\n"
"; store buffer full states - sb-full_<step>_<thread>\n"
"; store buffer full variables - sb-full_<step>_<thread>\n"
"(assert (not sb-full_0_0))\n"
"\n"
"; statement activation variables - stmt_<step>_<thread>_<pc>\n"
......@@ -1212,7 +1212,7 @@ TEST_F(SMTLib_Encoder_Test, init_states_check_exit)
"; blocking variables - block_<step>_<id>_<thread>\n"
"(assert (not block_0_0_0))\n"
"\n"
"; exit flag - exit_<step>\n"
"; exit flag variable - exit_<step>\n"
"(assert (not exit_0))\n"
"\n",
encoder->str());
......
......@@ -15,7 +15,7 @@ TEST_F(SMTLib_Encoder_Functional_Test, define_accu)
encoder->define_accu();
ASSERT_EQ(
"; accu states - accu_<step>_<thread>\n"
"; accu variables - accu_<step>_<thread>\n"
"(assert (= accu_1_0 "
"(ite exec_0_0_0 " // LOAD
"(ite (and sb-full_0_0 (= sb-adr_0_0 #x0001)) "
......@@ -151,7 +151,7 @@ TEST_F(SMTLib_Encoder_Functional_Test, define_mem)
encoder->define_mem();
ASSERT_EQ(
"; mem states - mem_<step>_<thread>\n"
"; mem variables - mem_<step>_<thread>\n"
"(assert (= mem_1_0 "
"(ite exec_0_0_13 "
"(ite (and sb-full_0_0 (= sb-adr_0_0 #x0001)) "
......@@ -212,7 +212,7 @@ TEST_F(SMTLib_Encoder_Functional_Test, define_sb_adr)
encoder->define_sb_adr();
ASSERT_EQ(
"; store buffer address states - sb-adr_<step>_<thread>\n"
"; store buffer address variables - sb-adr_<step>_<thread>\n"
"(assert (= sb-adr_1_0 (ite exec_0_0_1 #x0001 sb-adr_0_0)))\n"
"(assert (= sb-adr_1_1 (ite exec_0_1_1 #x0001 sb-adr_0_1)))\n"
"(assert (= sb-adr_1_2 (ite exec_0_2_1 #x0001 sb-adr_0_2)))\n"
......@@ -243,7 +243,7 @@ TEST_F(SMTLib_Encoder_Functional_Test, define_sb_val)
encoder->define_sb_val();
ASSERT_EQ(
"; store buffer value states - sb-val_<step>_<thread>\n"
"; store buffer value variables - sb-val_<step>_<thread>\n"
"(assert (= sb-val_1_0 (ite exec_0_0_1 accu_0_0 sb-val_0_0)))\n"
"(assert (= sb-val_1_1 (ite exec_0_1_1 accu_0_1 sb-val_0_1)))\n"
"(assert (= sb-val_1_2 (ite exec_0_2_1 accu_0_2 sb-val_0_2)))\n"
......@@ -274,7 +274,7 @@ TEST_F(SMTLib_Encoder_Functional_Test, define_sb_full)
encoder->define_sb_full();
ASSERT_EQ(
"; store buffer full states - sb-full_<step>_<thread>\n"
"; store buffer full variables - sb-full_<step>_<thread>\n"
"(assert (= sb-full_1_0 (ite flush_0_0 false (or exec_0_0_1 sb-full_0_0))))\n"
"(assert (= sb-full_1_1 (ite flush_0_1 false (or exec_0_1_1 sb-full_0_1))))\n"
"(assert (= sb-full_1_2 (ite flush_0_2 false (or exec_0_2_1 sb-full_0_2))))\n"
......@@ -683,7 +683,7 @@ TEST_F(SMTLib_Encoder_Functional_Test, define_heap)
encoder->define_heap();
ASSERT_EQ(
"; heap state - heap_<step>\n"
"; heap variable - heap_<step>\n"
"(assert (= heap_1 "
"(ite flush_0_0 " // FLUSH
"(store heap_0 sb-adr_0_0 sb-val_0_0) "
......@@ -750,7 +750,7 @@ TEST_F(SMTLib_Encoder_Functional_Test, define_exit_flag)
encoder->define_exit_flag();
ASSERT_EQ(
"; exit flag - exit_<step>\n"
"; exit flag variable - exit_<step>\n"
"(assert (= exit_1 (or exit_0 exec_0_0_0 exec_0_1_0 exec_0_2_0)))\n"
"\n",
encoder->str());
......@@ -846,25 +846,25 @@ TEST_F(SMTLib_Encoder_Functional_Test, define_states)
ASSERT_EQ(
"; state variable definitions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\n"
"\n"
"; accu states - accu_<step>_<thread>\n"
"; accu variables - accu_<step>_<thread>\n"
"(assert (= accu_1_0 accu_0_0))\n"
"\n"
"; mem states - mem_<step>_<thread>\n"
"; mem variables - mem_<step>_<thread>\n"
"(assert (= mem_1_0 mem_0_0))\n"
"\n"
"; store buffer address states - sb-adr_<step>_<thread>\n"
"; store buffer address variables - sb-adr_<step>_<thread>\n"
"(assert (= sb-adr_1_0 sb-adr_0_0))\n"
"\n"
"; store buffer value states - sb-val_<step>_<thread>\n"
"; store buffer value variables - sb-val_<step>_<thread>\n"
"(assert (= sb-val_1_0 sb-val_0_0))\n"
"\n"
"; store buffer full states - sb-full_<step>_<thread>\n"
"; store buffer full variables - sb-full_<step>_<thread>\n"
"(assert (= sb-full_1_0 (ite flush_0_0 false sb-full_0_0)))\n"
"\n"
"; statement activation variables - stmt_<step>_<thread>_<pc>\n"
"(assert (= stmt_1_0_0 (ite stmt_0_0_0 exec_0_0_0 (and stmt_0_0_0 (not exec_0_0_0)))))\n"
"\n"
"; heap state - heap_<step>\n"
"; heap variable - heap_<step>\n"
"(assert (= heap_1 (ite flush_0_0 (store heap_0 sb-adr_0_0 sb-val_0_0) heap_0)))\n"
"\n",
encoder->str());
......@@ -909,19 +909,19 @@ TEST_F(SMTLib_Encoder_Functional_Test, define_states_check_exit)
ASSERT_EQ(