Commit ba0dd776 authored by phlo's avatar phlo

optimized BTOR2 expression generators

parent 8c6ebe14
This diff is collapsed.
This diff is collapsed.
......@@ -297,8 +297,8 @@ inline std::string card_constraint_naive (const std::vector<std::string> & vars)
std::string constraint = assertion(lor(vars)) += eol;
// <= 1 constraint
for (auto it1 = vars.cbegin(), cend = vars.cend(); it1 != cend; ++it1)
for (auto it2 = it1 + 1; it2 != cend; ++it2)
for (auto it1 = vars.begin(); it1 != vars.end(); ++it1)
for (auto it2 = it1 + 1; it2 != vars.end(); ++it2)
(constraint += assertion(lor(lnot(*it1), lnot(*it2)))) += eol;
return constraint;
......@@ -322,11 +322,14 @@ inline std::string card_constraint_sinz (const std::vector<std::string> & vars)
std::string constraint;
// n-1 auxiliary variables
std::vector<std::string> aux;
aux.reserve(n - 1);
for (size_t i = 0; i < n - 1; i++)
std::vector<std::string> auxs;
auxs.reserve(n - 1);
const auto end = --vars.end();
for (auto it = vars.begin(); it != end; ++it)
{
constraint += declare_bool_var(aux.emplace_back(vars[i] + "_aux"));
constraint += declare_bool_var(auxs.emplace_back(*it + "_aux"));
constraint += eol;
}
......@@ -336,21 +339,27 @@ inline std::string card_constraint_sinz (const std::vector<std::string> & vars)
constraint += eol;
// <= 1 constraint
constraint += assertion(lor(lnot(vars[0]), aux[0]));
constraint += eol;
constraint += assertion(lor(lnot(vars[n - 1]), lnot(aux[n - 2])));
auto var = vars.begin();
auto aux = auxs.begin();
constraint += assertion(lor(lnot(*var), *aux));
constraint += eol;
for (size_t i = 1; i < n - 1; i++)
while (++var != end)
{
constraint += assertion(lor(lnot(vars[i]), aux[i]));
const std::string & aux_prev = *aux++;
constraint += assertion(lor(lnot(*var), *aux));
constraint += eol;
constraint += assertion(lor(lnot(aux[i - 1]), aux[i]));
constraint += assertion(lor(lnot(aux_prev), *aux));
constraint += eol;
constraint += assertion(lor(lnot(vars[i]), lnot(aux[i - 1])));
constraint += assertion(lor(lnot(*var), lnot(aux_prev)));
constraint += eol;
}
constraint += assertion(lor(lnot(*var), lnot(*aux)));
constraint += eol;
return constraint;
}
......
......@@ -39,24 +39,24 @@ TEST(btor2, comment_subsection)
btor2::comment_subsection("foo"));
}
// declare_sort ================================================================
// sort_bitvec =================================================================
TEST(btor2, declare_sort)
TEST(btor2, sort_bitvec)
{
ASSERT_EQ("1 sort bitvec 1\n", btor2::declare_sort("1", "1"));
ASSERT_EQ("2 sort bitvec 16\n", btor2::declare_sort("2", "16"));
ASSERT_EQ("3 sort bitvec 32 foo\n", btor2::declare_sort("3", "32", "foo"));
ASSERT_EQ("1 sort bitvec 1\n", btor2::sort_bitvec("1", "1"));
ASSERT_EQ("2 sort bitvec 16\n", btor2::sort_bitvec("2", "16"));
ASSERT_EQ("3 sort bitvec 32 foo\n", btor2::sort_bitvec("3", "32", "foo"));
}
// declare_array ===============================================================
// sort_array ==================================================================
TEST(btor2, declare_array)
TEST(btor2, sort_array)
{
ASSERT_EQ("1 sort array 2 2\n", btor2::declare_array("1", "2", "2"));
ASSERT_EQ("2 sort array 16 16\n", btor2::declare_array("2", "16", "16"));
ASSERT_EQ("1 sort array 2 2\n", btor2::sort_array("1", "2", "2"));
ASSERT_EQ("2 sort array 16 16\n", btor2::sort_array("2", "16", "16"));
ASSERT_EQ(
"3 sort array 32 32 foo\n",
btor2::declare_array("3", "32", "32", "foo"));
btor2::sort_array("3", "32", "32", "foo"));
}
// constd ======================================================================
......@@ -400,7 +400,6 @@ TEST(btor2, land_variadic)
// 2 arguments
ASSERT_EQ("11 and 1 2 3\n", btor2::land(nid, "1", {"2", "3"}));
ASSERT_EQ(12, nid);
// 3 arguments
......@@ -410,7 +409,6 @@ TEST(btor2, land_variadic)
"11 and 1 2 3\n"
"12 and 1 4 11\n",
btor2::land(nid, "1", {"2", "3", "4"}));
ASSERT_EQ(13, nid);
// 4 arguments
......@@ -421,17 +419,6 @@ TEST(btor2, land_variadic)
"12 and 1 4 11\n"
"13 and 1 5 12 foo\n",
btor2::land(nid, "1", {"2", "3", "4", "5"}, "foo"));
ASSERT_EQ(14, nid);
// empty argument
ASSERT_THROW(btor2::land(nid, "1", {}), std::runtime_error);
ASSERT_EQ(14, nid);
// single argument
ASSERT_THROW(btor2::land(nid, "1", {"2"}), std::runtime_error);
ASSERT_EQ(14, nid);
}
......@@ -468,7 +455,6 @@ TEST(btor2, lor_variadic)
// 2 arguments
ASSERT_EQ("11 or 1 2 3\n", btor2::lor(nid, "1", {"2", "3"}));
ASSERT_EQ(12, nid);
// 3 arguments
......@@ -478,7 +464,6 @@ TEST(btor2, lor_variadic)
"11 or 1 2 3\n"
"12 or 1 4 11\n",
btor2::lor(nid, "1", {"2", "3", "4"}));
ASSERT_EQ(13, nid);
// 4 arguments
......@@ -489,17 +474,6 @@ TEST(btor2, lor_variadic)
"12 or 1 4 11\n"
"13 or 1 5 12 foo\n",
btor2::lor(nid, "1", {"2", "3", "4", "5"}, "foo"));
ASSERT_EQ(14, nid);
// empty argument
ASSERT_THROW(btor2::lor(nid, "1", {}), std::runtime_error);
ASSERT_EQ(14, nid);
// single argument
ASSERT_THROW(btor2::lor(nid, "1", {"2"}), std::runtime_error);
ASSERT_EQ(14, nid);
}
......@@ -759,14 +733,12 @@ TEST(btor2, cardinality_exactly_one_naive)
ASSERT_EQ(
"10 constraint 2\n",
btor2::card_constraint_naive(nid, "1", {"2"}));
ASSERT_EQ(nid, 11);
ASSERT_EQ(
"10 xor 1 2 3\n"
"11 constraint 10\n",
btor2::card_constraint_naive(nid = 10, "1", {"2", "3"}));
ASSERT_EQ(nid, 12);
ASSERT_EQ(
......@@ -780,7 +752,6 @@ TEST(btor2, cardinality_exactly_one_naive)
"17 and 1 15 16\n"
"18 constraint 17\n",
btor2::card_constraint_naive(nid = 10, "1", {"2", "3", "4"}));
ASSERT_EQ(nid, 19);
ASSERT_EQ(
......@@ -801,7 +772,6 @@ TEST(btor2, cardinality_exactly_one_naive)
"24 and 1 19 23\n"
"25 constraint 24\n",
btor2::card_constraint_naive(nid = 10, "1", {"2", "3", "4", "5"}));
ASSERT_EQ(nid, 26);
}
......@@ -810,7 +780,7 @@ TEST(btor2, cardinality_exactly_one_naive_verify)
BtorMC btormc;
std::string formula =
btor2::declare_sort("1", "1") +
btor2::sort_bitvec("1", "1") +
btor2::constd("2", "1", "0") +
btor2::constd("3", "1", "1");
......@@ -841,6 +811,8 @@ TEST(btor2, cardinality_exactly_one_naive_verify)
spec += btor2::land(nid, "1", eqs_zero);
spec += btor2::bad(nid);
ASSERT_FALSE(btormc.sat(spec));
// not more than one
std::vector<std::string> eqs_one;
......@@ -866,76 +838,60 @@ TEST(btor2, cardinality_exactly_one_sinz)
ASSERT_EQ(
"10 constraint 2\n",
btor2::card_constraint_naive(nid, "1", {"2"}));
btor2::card_constraint_sinz(nid, "1", {"2"}));
ASSERT_EQ(nid, 11);
ASSERT_EQ(
"10 xor 1 2 3\n"
"11 constraint 10\n",
btor2::card_constraint_naive(nid = 10, "1", {"2", "3"}));
btor2::card_constraint_sinz(nid = 10, "1", {"2", "3"}));
ASSERT_EQ(nid, 12);
ASSERT_EQ(
"10 or 1 2 3\n"
"11 or 1 4 10\n"
"12 constraint 11\n"
"13 input 1 card_aux_0\n"
"14 input 1 card_aux_1\n"
"15 not 1 2\n"
"16 or 1 13 15\n"
"17 constraint 16\n"
"18 not 1 4\n"
"19 not 1 14\n"
"20 or 1 18 19\n"
"21 constraint 20\n"
"22 not 1 3\n"
"23 or 1 14 22\n"
"24 constraint 23\n"
"25 not 1 13\n"
"26 or 1 14 25\n"
"27 constraint 26\n"
"28 or 1 22 25\n"
"29 constraint 28\n",
"13 input 1 2_aux\n"
"14 input 1 3_aux\n"
"15 or 1 -2 13\n"
"16 or 1 -3 14\n"
"17 or 1 -13 14\n"
"18 or 1 -3 -13\n"
"19 or 1 -4 -14\n"
"20 and 1 15 16\n"
"21 and 1 17 20\n"
"22 and 1 18 21\n"
"23 and 1 19 22\n"
"24 constraint 23\n",
btor2::card_constraint_sinz(nid = 10, "1", {"2", "3", "4"}));
ASSERT_EQ(nid, 30);
ASSERT_EQ(nid, 25);
ASSERT_EQ(
"10 or 1 1 2\n"
"11 or 1 3 10\n"
"12 or 1 4 11\n"
"10 or 1 2 3\n"
"11 or 1 4 10\n"
"12 or 1 5 11\n"
"13 constraint 12\n"
"14 input 1 card_aux_0\n"
"15 input 1 card_aux_1\n"
"16 input 1 card_aux_2\n"
"17 not 1 1\n"
"18 or 1 14 17\n"
"19 constraint 18\n"
"20 not 1 4\n"
"21 not 1 16\n"
"22 or 1 20 21\n"
"23 constraint 22\n"
"24 not 1 2\n"
"25 or 1 15 24\n"
"26 constraint 25\n"
"27 not 1 14\n"
"28 or 1 15 27\n"
"29 constraint 28\n"
"30 or 1 24 27\n"
"31 constraint 30\n"
"32 not 1 3\n"
"33 or 1 16 32\n"
"34 constraint 33\n"
"35 not 1 15\n"
"36 or 1 16 35\n"
"37 constraint 36\n"
"38 or 1 32 35\n"
"39 constraint 38\n",
btor2::card_constraint_sinz(nid = 10, "1", {"1", "2", "3", "4"}));
ASSERT_EQ(nid, 40);
"14 input 1 2_aux\n"
"15 input 1 3_aux\n"
"16 input 1 4_aux\n"
"17 or 1 -2 14\n"
"18 or 1 -3 15\n"
"19 or 1 -14 15\n"
"20 or 1 -3 -14\n"
"21 or 1 -4 16\n"
"22 or 1 -15 16\n"
"23 or 1 -4 -15\n"
"24 or 1 -5 -16\n"
"25 and 1 17 18\n"
"26 and 1 19 25\n"
"27 and 1 20 26\n"
"28 and 1 21 27\n"
"29 and 1 22 28\n"
"30 and 1 23 29\n"
"31 and 1 24 30\n"
"32 constraint 31\n",
btor2::card_constraint_sinz(nid = 10, "1", {"2", "3", "4", "5"}));
ASSERT_EQ(nid, 33);
}
TEST(btor2, cardinality_exactly_one_sinz_verify)
......@@ -943,7 +899,7 @@ TEST(btor2, cardinality_exactly_one_sinz_verify)
BtorMC btormc;
std::string formula =
btor2::declare_sort("1", "1") +
btor2::sort_bitvec("1", "1") +
btor2::constd("2", "1", "0") +
btor2::constd("3", "1", "1");
......@@ -974,6 +930,8 @@ TEST(btor2, cardinality_exactly_one_sinz_verify)
spec += btor2::land(nid, "1", eqs_zero);
spec += btor2::bad(nid);
ASSERT_FALSE(btormc.sat(spec));
// not more than one
std::vector<std::string> eqs_one;
......
......@@ -376,18 +376,19 @@ TEST(btor2_Encoder, define_mmap)
if (verbose)
s << btor2::comment_section("memory map");
std::string nid_init = std::to_string(nid++);
s << btor2::state(nid_init, encoder.sid_heap, "mmap");
s << btor2::state(std::to_string(nid++), encoder.sid_heap, "mmap");
for (const auto & [adr, val] : *encoder.mmap)
s <<
btor2::write(
nid_init = std::to_string(nid++),
encoder.sid_heap,
nid_init,
encoder.nids_const[adr],
encoder.nids_const[val]);
{
s <<
btor2::write(
std::to_string(nid),
encoder.sid_heap,
std::to_string(nid - 1),
encoder.nids_const[adr],
encoder.nids_const[val]);
nid++;
}
s << eol;
......@@ -2753,13 +2754,15 @@ TEST(btor2_Encoder, define_heap)
encoder.nids_sb_adr[thread],
encoder.nids_sb_val[thread]);
nid++;
std::string nid_prev = std::move(nid_next);
nid_next = std::to_string(nid);
s <<
btor2::ite(
nid_next = std::to_string(nid),
nid_next,
encoder.sid_heap,
encoder.nids_flush[thread],
std::to_string(nid - 1),
nid_next,
nid_prev,
verbose ? encoder.flush_var() : "");
nid++;
......@@ -2819,13 +2822,15 @@ TEST(btor2_Encoder, define_heap)
std::to_string(nid - 1),
encoder.nid_heap);
nid++;
nid_prev = std::move(nid_next);
nid_next = std::to_string(nid);
s <<
btor2::ite(
nid_next = std::to_string(nid),
nid_next,
encoder.sid_heap,
encoder.nids_exec[thread][pc],
std::to_string(nid - 1),
nid_next,
nid_prev,
verbose ? encoder.debug_symbol(thread, pc) : "");
nid++;
});
......@@ -2870,8 +2875,6 @@ TEST(btor2_Encoder, define_heap_mmap)
auto expected = [&encoder, &nid] {
std::ostringstream s;
std::string nid_next = encoder.nid_heap;
if (verbose)
s << encoder.heap_comment;
......@@ -2886,7 +2889,7 @@ TEST(btor2_Encoder, define_heap_mmap)
std::to_string(nid),
encoder.sid_heap,
encoder.nid_heap,
nid_next,
encoder.nid_heap,
encoder.heap_sym);
s << eol;
......
......@@ -295,11 +295,12 @@ TEST(smtlib, cardinality_exactly_one_sinz)
"(assert (or x1 x2 x3))\n"
"(assert (or (not x1) x1_aux))\n"
"(assert (or (not x3) (not x2_aux)))\n"
"(assert (or (not x2) x2_aux))\n"
"(assert (or (not x1_aux) x2_aux))\n"
"(assert (or (not x2) (not x1_aux)))\n",
"(assert (or (not x2) (not x1_aux)))\n"
"(assert (or (not x3) (not x2_aux)))\n",
smtlib::card_constraint_sinz({"x1", "x2", "x3"}));
ASSERT_EQ(
......@@ -310,7 +311,6 @@ TEST(smtlib, cardinality_exactly_one_sinz)
"(assert (or x1 x2 x3 x4))\n"
"(assert (or (not x1) x1_aux))\n"
"(assert (or (not x4) (not x3_aux)))\n"
"(assert (or (not x2) x2_aux))\n"
"(assert (or (not x1_aux) x2_aux))\n"
......@@ -318,7 +318,9 @@ TEST(smtlib, cardinality_exactly_one_sinz)
"(assert (or (not x3) x3_aux))\n"
"(assert (or (not x2_aux) x3_aux))\n"
"(assert (or (not x3) (not x2_aux)))\n",
"(assert (or (not x3) (not x2_aux)))\n"
"(assert (or (not x4) (not x3_aux)))\n",
smtlib::card_constraint_sinz({"x1", "x2", "x3", "x4"}));
}
......
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