Commit 63b01a22 authored by phlo's avatar phlo

fixed parsing models using Sinz's constraint

parent 40284b19
......@@ -142,13 +142,19 @@ External::Symbol External::symbol (std::istringstream & line)
{
step = attribute(line, "step");
thread = attribute(line, "thread");
return Symbol::thread;
// ignore auxiliary variables
if (line.peek() != '_')
return Symbol::thread;
}
else if (name == Encoder::flush_sym)
{
step = attribute(line, "step");
thread = attribute(line, "thread");
return Symbol::flush;
// ignore auxiliary variables
if (line.peek() != '_')
return Symbol::flush;
}
return Symbol::ignore;
......
......@@ -823,9 +823,16 @@ TEST(btor2, cardinality_exactly_one_naive_verify)
formula += btor2::card_constraint_naive(nid, "1", vars);
// exactly one
std::string spec = formula;
spec += btor2::eq(std::to_string(nid++), "1", "3", vars[0]);
spec += btor2::bad(nid);
ASSERT_TRUE(btormc.sat(spec));
// not none
std::vector<std::string> eqs_zero;
std::string spec = formula;
spec = formula;
for (const auto & v : vars)
spec +=
......@@ -949,9 +956,16 @@ TEST(btor2, cardinality_exactly_one_sinz_verify)
formula += btor2::card_constraint_sinz(nid, "1", vars);
// exactly one
std::string spec = formula;
spec += btor2::eq(std::to_string(nid++), "1", "3", vars[0]);
spec += btor2::bad(nid);
ASSERT_TRUE(btormc.sat(spec));
// not none
std::vector<std::string> eqs_zero;
std::string spec = formula;
spec = formula;
for (const auto & v : vars)
spec +=
......
......@@ -277,8 +277,14 @@ TEST(smtlib, cardinality_exactly_one_naive_verify)
formula += smtlib::card_constraint_naive(vars);
// exactly one
std::string spec =
formula + smtlib::assertion(vars[0]) + eol + smtlib::check_sat() + eol;
ASSERT_TRUE(btor.sat(spec));
// not none
std::string spec = formula;
spec = formula;
for (const auto & v : vars)
spec += smtlib::assertion(smtlib::lnot(v)) + eol;
......@@ -357,8 +363,14 @@ TEST(smtlib, cardinality_exactly_one_sinz_verify)
formula += smtlib::card_constraint_sinz(vars);
// exactly one
std::string spec =
formula + smtlib::assertion(vars[0]) + eol + smtlib::check_sat() + eol;
ASSERT_TRUE(btor.sat(spec));
// not none
std::string spec = formula;
spec = formula;
for (const auto & v : vars)
spec += smtlib::assertion(smtlib::lnot(v)) + eol;
......
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