From 72dcb55fc7c4d1f5c0fbae1b0471d97c655175ad Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Wed, 29 May 2024 12:01:56 +0200 Subject: [PATCH] Adjust show handling in text output. * Add "#show." whenever the output contains a generated atom name. * Use (:) from an output statement as name for atom only if is not reserved (i.e. 'x_') and the mapping is unique. * Require uniqueness of theory atoms. --- potassco/aspif_text.h | 7 +- src/aspif_text.cpp | 161 ++++++++++++++++++++++------- tests/test_text.cpp | 228 ++++++++++++++++++++++++++++++++++++------ 3 files changed, 329 insertions(+), 67 deletions(-) diff --git a/potassco/aspif_text.h b/potassco/aspif_text.h index 5de68e3..e19844a 100644 --- a/potassco/aspif_text.h +++ b/potassco/aspif_text.h @@ -99,11 +99,11 @@ class AspifTextOutput : public Potassco::AbstractProgram { virtual void theoryAtom(Id_t atomOrZero, Id_t termId, const IdSpan& elements, Id_t op, Id_t rhs); virtual void endStep(); - void addAtom(Atom_t id, const StringSpan& str); private: - std::ostream& printName(std::ostream& os, Lit_t lit) const; + std::ostream& printName(std::ostream& os, Lit_t lit); void writeDirectives(); void visitTheories(); + bool assignAtomName(Atom_t id, const std::string& name); AspifTextOutput& push(uint32_t x); AspifTextOutput& push(const AtomSpan& atoms); AspifTextOutput& push(const LitSpan& lits); @@ -116,6 +116,9 @@ class AspifTextOutput : public Potassco::AbstractProgram { TheoryData theory_; Data* data_; int step_; + int showAtoms_; + Atom_t startAtom_; + Atom_t maxAtom_; }; //! Converts a given theory atom to a string. diff --git a/src/aspif_text.cpp b/src/aspif_text.cpp index 4c567ef..d75b44d 100644 --- a/src/aspif_text.cpp +++ b/src/aspif_text.cpp @@ -24,12 +24,15 @@ #include #include #include +#include +#include #include #include #include #include #include -#include +#include POTASSCO_EXT_INCLUDE(unordered_map) + namespace Potassco { struct AspifTextInput::Data { void clear() { rule.clear(); symbol.clear(); } @@ -297,10 +300,14 @@ void AspifTextInput::matchStr() { // AspifTextOutput ///////////////////////////////////////////////////////////////////////////////////////// struct AspifTextOutput::Data { - typedef std::vector StringVec; - typedef std::vector AtomMap; typedef std::vector LitVec; typedef std::vector RawVec; + typedef POTASSCO_EXT_NS::unordered_map StringMap; + typedef StringMap::pointer StringMapNode; + typedef StringMap::value_type StringMapVal; + typedef std::vector AtomMap; + typedef std::vector OutOrder; + LitSpan getCondition(Id_t id) const { return toSpan(&conditions[id + 1], static_cast(conditions[id])); } @@ -312,41 +319,102 @@ struct AspifTextOutput::Data { conditions.insert(conditions.end(), begin(cond), end(cond)); return id; } - Id_t addString(const StringSpan& str) { - Id_t id = static_cast(strings.size()); - strings.push_back(std::string(Potassco::begin(str), Potassco::end(str))); - return id; + Id_t addOutputString(const StringSpan& str) { + out.push_back(&*strings.insert(StringMapVal(std::string(Potassco::begin(str), Potassco::end(str)), idMax)).first); + return static_cast(out.size() - 1); + } + void convertToOutput(StringMapNode node) { + if (node->second && node->second < atoms.size()) { + POTASSCO_REQUIRE(node->first[0] != '&', "Redefinition: theory atom '%u' already defined as '%s'", node->second, node->first.c_str()); + setGenName(node->second); + uint32_t data[4] = {static_cast(Directive_t::Output), static_cast(out.size()), 1, node->second}; + node->second = 0; + out.push_back(node); + directives.insert(directives.end(), data, data + 4); + } + } + const std::string* getAtomName(Atom_t atom) const { + StringMapNode node = atom < atoms.size() ? atoms[atom] : 0; + return node && node->second == atom ? &node->first : 0; + } + void setGenName(Atom_t atom) { + if (!genName) genName = &*strings.insert(StringMapVal(std::string(), 0)).first; + atoms.at(atom) = genName; } - RawVec directives; - StringVec strings; - AtomMap atoms; // maps into strings - LitVec conditions; - uint32_t readPos; - void reset() { directives.clear(); strings.clear(); atoms.clear(); conditions.clear(); readPos = 0; } + + RawVec directives; + StringMap strings; + AtomMap atoms; // maps into strings + OutOrder out; + LitVec conditions; + StringMapNode genName; + uint32_t readPos; + void reset() { directives.clear(); strings.clear(); atoms.clear(); conditions.clear(); out.clear(); genName = 0; readPos = 0; } }; -AspifTextOutput::AspifTextOutput(std::ostream& os) : os_(os), step_(-1) { +AspifTextOutput::AspifTextOutput(std::ostream& os) : os_(os), step_(-1), showAtoms_(0), startAtom_(0), maxAtom_(0) { data_ = new Data(); } AspifTextOutput::~AspifTextOutput() { delete data_; } -void AspifTextOutput::addAtom(Atom_t id, const StringSpan& str) { - if (id >= data_->atoms.size()) { data_->atoms.resize(id + 1, idMax); } - data_->atoms[id] = data_->addString(str); +// Try to set `str` as the unique name for `atom`. +bool AspifTextOutput::assignAtomName(Atom_t atom, const std::string& str) { + if (atom <= maxAtom_) { + return false; + } + assert(!str.empty()); + bool theory = str[0] == '&'; + if (atom >= data_->atoms.size()) { data_->atoms.resize(atom + 1, 0); } + if (Data::StringMapNode node = data_->atoms[atom]) { // atom already has a tentative name + if (node->second == atom && node->first == str) { + return true; // identical name, ignore duplicate + } + data_->convertToOutput(node); // drop assignment + if (!theory) { + return false; + } + } + if (str.size() > 2 && str[0] == 'x' && str[1] == '_') { + const char* x = str.c_str() + 2; + while (BufferedStream::isDigit(*x)) { ++x; } + if (!*x) { + data_->setGenName(atom); + return false; + } + } + Data::StringMapNode node = &*data_->strings.insert(Data::StringMapVal(str, atom)).first; + if (node->second == atom || node->second == idMax) { // assign tentative name to atom + node->second = atom; + data_->atoms[atom] = node; + return true; + } + // name already used: drop previous (tentative) assigment and prevent further assignments + if (node->second > maxAtom_) { + data_->convertToOutput(node); + } + data_->setGenName(atom); + return false; } -std::ostream& AspifTextOutput::printName(std::ostream& os, Lit_t lit) const { +std::ostream& AspifTextOutput::printName(std::ostream& os, Lit_t lit) { if (lit < 0) { os << "not "; } Atom_t id = Potassco::atom(lit); - if (id < data_->atoms.size() && data_->atoms[id] < data_->strings.size()) { - os << data_->strings[data_->atoms[id]]; + if (const std::string* name = data_->getAtomName(id)) { + os << *name; } else { os << "x_" << id; + if (showAtoms_ == 0) { + showAtoms_ = 1; + } } + maxAtom_ = std::max(maxAtom_, id); return os; } void AspifTextOutput::initProgram(bool incremental) { - step_ = incremental ? 0 : -1; + step_ = incremental ? 0 : -1; + showAtoms_ = 0; + startAtom_ = 0; + maxAtom_ = 0; data_->reset(); } void AspifTextOutput::beginStep() { @@ -384,22 +452,26 @@ void AspifTextOutput::rule(Head_t ht, const AtomSpan& head, Weight_t bound, cons void AspifTextOutput::minimize(Weight_t prio, const WeightLitSpan& lits) { push(Directive_t::Minimize).push(prio).push(lits); } + static bool isAtom(const StringSpan& s) { std::size_t sz = size(s); - char first = sz > 0 ? s[0] : char(0); - if (first == '-' && sz > 1) { - first = s[1]; + const char* p = s.first; + if (sz > 1 && *p == '-') { + ++p; // accept classical negation + --sz; } - return std::islower(static_cast(first)) || first == '_'; + while (sz && *p == '_') { + ++p; + --sz; + } + return sz && std::islower(static_cast(*p)); } void AspifTextOutput::output(const StringSpan& str, const LitSpan& cond) { - if (size(cond) == 1 && lit(*begin(cond)) > 0 && isAtom(str)) { - addAtom(Potassco::atom(*begin(cond)), str); - } - else { - push(Directive_t::Output).push(data_->addString(str)).push(cond); + if (size(cond) == 1 && isAtom(str) && assignAtomName(atom(*begin(cond)), std::string(begin(str), end(str)))) { + return; } + push(Directive_t::Output).push(data_->addOutputString(str)).push(cond); } void AspifTextOutput::external(Atom_t a, Value_t v) { push(Directive_t::External).push(a).push(static_cast(v)); @@ -506,7 +578,7 @@ void AspifTextOutput::writeDirectives() { break; case Directive_t::Output: sep = " : "; term = "."; - os_ << "#show " << data_->strings[get()]; + os_ << "#show " << data_->out[get()]->first; for (uint32_t n = get(); n--; sep = ", ") { printName(os_ << sep, get()); } @@ -545,6 +617,21 @@ void AspifTextOutput::writeDirectives() { } os_ << term << "\n"; } + if (showAtoms_) { + if (showAtoms_ == 1) { + os_ << "#show.\n"; + showAtoms_ = 2; + } + for (Atom_t a = startAtom_; a < data_->atoms.size(); ++a) { + if (const std::string* n = data_->getAtomName(a)) { + if (*n->c_str() != '&') { + os_ << "#show " << *n << " : " << *n << ".\n"; + } + } + } + startAtom_ = data_->atoms.size(); + } + os_ << std::flush; } void AspifTextOutput::visitTheories() { struct BuildStr : public TheoryAtomStringBuilder { @@ -553,8 +640,8 @@ void AspifTextOutput::visitTheories() { return self->data_->getCondition(condId); } virtual std::string getName(Atom_t id) const { - if (id < self->data_->atoms.size() && self->data_->atoms[id] < self->data_->strings.size()) { - return self->data_->strings[self->data_->atoms[id]]; + if (const std::string* name = self->data_->getAtomName(id)) { + return *name; } return std::string("x_").append(Potassco::toString(id)); } @@ -567,9 +654,8 @@ void AspifTextOutput::visitTheories() { os_ << name << ".\n"; } else { - POTASSCO_REQUIRE(atom >= data_->atoms.size() || data_->atoms[atom] == idMax, - "Redefinition: theory atom '%u' already shown as '%s'", atom, data_->strings[data_->atoms[atom]].c_str()); - addAtom(atom, toSpan(name)); + POTASSCO_REQUIRE(atom > maxAtom_, "Redefinition: theory atom '%u:%s' already defined in a previous step", atom, name.c_str()); + assignAtomName(atom, name); } } } @@ -578,7 +664,8 @@ void AspifTextOutput::endStep() { push(Directive_t::End); writeDirectives(); Data::RawVec().swap(data_->directives); - if (step_ < 0) { theory_.reset(); } + Data::OutOrder().swap(data_->out); + if (step_ < 0) { theory_.reset(); } } ///////////////////////////////////////////////////////////////////////////////////////// // TheoryAtomStringBuilder diff --git a/tests/test_text.cpp b/tests/test_text.cpp index 4201c9b..37421a2 100644 --- a/tests/test_text.cpp +++ b/tests/test_text.cpp @@ -197,7 +197,7 @@ TEST_CASE("Text writer ", "[text]") { SECTION("simple fact") { input << "x1."; read(prg, input); - REQUIRE(output.str() == "x_1.\n"); + REQUIRE(output.str() == "x_1.\n#show.\n"); } SECTION("named fact") { input << "x1.\n#output foo : x1."; @@ -207,7 +207,7 @@ TEST_CASE("Text writer ", "[text]") { SECTION("simple choice") { input << "{x1,x2}.\n#output foo : x1."; read(prg, input); - REQUIRE(output.str() == "{foo;x_2}.\n"); + REQUIRE(output.str() == "{foo;x_2}.\n#show.\n#show foo : foo.\n"); } SECTION("empty choice") { input << "{}."; @@ -217,7 +217,7 @@ TEST_CASE("Text writer ", "[text]") { SECTION("integrity constraint") { input << ":- x1,x2.\n#output foo : x1."; read(prg, input); - REQUIRE(output.str() == ":- foo, x_2.\n"); + REQUIRE(output.str() == ":- foo, x_2.\n#show.\n#show foo : foo.\n"); } SECTION("empty integrity constraint") { input << ":-."; @@ -243,67 +243,172 @@ TEST_CASE("Text writer ", "[text]") { out.output(toSpan("-a"), toSpan(&cond1, 1)); out.output(toSpan("x_1"), toSpan(&cond2, 1)); out.endStep(); - REQUIRE(output.str() == "{-a;x_1}.\n"); + REQUIRE(output.str() == "{-a;x_2}.\n#show x_1 : x_2.\n#show.\n#show -a : -a.\n"); } SECTION("basic rule") { input << "x1 :- x2, not x3, x4.\n#output foo : x1.\n#output bar : x3."; read(prg, input); - REQUIRE(output.str() == "foo :- x_2, not bar, x_4.\n"); + REQUIRE(output.str() == "foo :- x_2, not bar, x_4.\n#show.\n#show foo : foo.\n#show bar : bar.\n"); } SECTION("choice rule") { input << "{x1,x2} :- not x3, x4.\n#output foo : x1.\n#output bar : x3."; read(prg, input); - REQUIRE(output.str() == "{foo;x_2} :- not bar, x_4.\n"); + REQUIRE(output.str() == "{foo;x_2} :- not bar, x_4.\n#show.\n#show foo : foo.\n#show bar : bar.\n"); } SECTION("disjunctive rule") { input << "x1;x2 :- not x3, x4.\n#output foo : x1.\n#output bar : x3."; read(prg, input); - REQUIRE(output.str() == "foo|x_2 :- not bar, x_4.\n"); + REQUIRE(output.str() == "foo|x_2 :- not bar, x_4.\n#show.\n#show foo : foo.\n#show bar : bar.\n"); } SECTION("cardinality rule") { input << "x1;x2 :- 1{not x3, x4}.\n#output foo : x1.\n#output bar : x3."; read(prg, input); - REQUIRE(output.str() == "foo|x_2 :- 1 #count{1 : not bar; 2 : x_4}.\n"); + REQUIRE(output.str() == + "foo|x_2 :- 1 #count{1 : not bar; 2 : x_4}.\n#show.\n#show foo : foo.\n#show bar : bar.\n"); } SECTION("sum rule") { input << "x1;x2 :- 3{not x3=2, x4, x5=1,x6=2}.\n#output foo : x1.\n#output bar : x3."; read(prg, input); - REQUIRE(output.str() == "foo|x_2 :- 3 #sum{2,1 : not bar; 1,2 : x_4; 1,3 : x_5; 2,4 : x_6}.\n"); + REQUIRE(output.str() == "foo|x_2 :- 3 #sum{2,1 : not bar; 1,2 : x_4; 1,3 : x_5; 2,4 : x_6}.\n#show.\n#show foo " + ": foo.\n#show bar : bar.\n"); } SECTION("convert sum rule to cardinality rule") { input << "x1;x2 :- 3{not x3=2, x4=2, x5=2,x6=2}.\n#output foo : x1.\n#output bar : x3."; read(prg, input); - REQUIRE(output.str() == "foo|x_2 :- 2 #count{1 : not bar; 2 : x_4; 3 : x_5; 4 : x_6}.\n"); + REQUIRE(output.str() == "foo|x_2 :- 2 #count{1 : not bar; 2 : x_4; 3 : x_5; 4 : x_6}.\n#show.\n#show foo : " + "foo.\n#show bar : bar.\n"); } SECTION("minimize rule") { input << "#minimize{x1,x2=2,x3}.\n#minimize{not x1=3,not x2,not x3}@1."; read(prg, input); REQUIRE(output.str() == "#minimize{1@0,1 : x_1; 2@0,2 : x_2; 1@0,3 : x_3}.\n#minimize{3@1,1 : not x_1; 1@1,2 : not " - "x_2; 1@1,3 : not x_3}.\n"); + "x_2; 1@1,3 : not x_3}.\n#show.\n"); } SECTION("output statements") { input << "{x1;x2}.\n#output foo.\n#output bar : x1.\n#output \"Hello World\" : x2, not x1."; read(prg, input); - REQUIRE(output.str() == "{bar;x_2}.\n#show foo.\n#show \"Hello World\" : x_2, not bar.\n"); + REQUIRE(output.str() == "{bar;x_2}.\n#show foo.\n#show \"Hello World\" : x_2, not bar.\n#show.\n" + "#show bar : bar.\n"); + } + SECTION("duplicate output condition") { + input << "{a}.\n#output x:a.\n#output y:a.\n"; + read(prg, input); + REQUIRE(output.str() == "{x_1}.\n#show x : x_1.\n#show y : x_1.\n#show.\n"); + } + SECTION("bogus duplicate output condition") { + input << "{a}.\n#output x:a.\n#output x:a.\n"; + read(prg, input); + REQUIRE(output.str() == "{x}.\n"); + } + SECTION("duplicate output term") { + input << "{x1;x2}.\n"; + SECTION("simple") { + input << "#output a:x1.\n#output a:x2.\n"; + read(prg, input); + REQUIRE(output.str() == "{x_1;x_2}.\n#show a : x_1.\n#show a : x_2.\n#show.\n"); + } + SECTION("complex") { + input << "#output a:x1.\n#output a:x1,x2.\n"; + read(prg, input); + REQUIRE(output.str() == "{a;x_2}.\n#show a : a, x_2.\n#show.\n#show a : a.\n"); + } + SECTION("complex reversed") { + input << "#output a:x1,x2.\n#output a:x1.\n"; + read(prg, input); + REQUIRE(output.str() == "{a;x_2}.\n#show a : a, x_2.\n#show.\n#show a : a.\n"); + } + SECTION("duplicate condition first") { + input << "#output a:x1.\n#output b:x1.\n#output a:x2.\n"; + read(prg, input); + REQUIRE(output.str() == "{x_1;x_2}.\n#show a : x_1.\n#show b : x_1.\n#show a : x_2.\n#show.\n"); + } + SECTION("duplicate condition all") { + input << "#output a:x1.\n#output b:x1.\n#output a:x2.\n#output f:x2.\n"; + read(prg, input); + REQUIRE(output.str() == "{x_1;x_2}.\n#show a : x_1.\n#show b : x_1.\n#show a : x_2.\n#show f : x_2.\n#show.\n"); + } + } + SECTION("implicit show") { + input << "{a;b}. #output a:a.\n#output b:b.\n"; + read(prg, input); + REQUIRE(output.str() == "{a;b}.\n"); + } + SECTION("explicit show") { + input << "{a;b}.\n"; + SECTION("empty") { + read(prg, input); + REQUIRE(output.str() == "{x_1;x_2}.\n#show.\n"); + } + SECTION("one") { + input << "#output a:a.\n"; + read(prg, input); + REQUIRE(output.str() == "{a;x_2}.\n#show.\n#show a : a.\n"); + } + SECTION("duplicate one") { + input << "#output a:b.\n#output b:b.\n"; + read(prg, input); + REQUIRE(output.str() == "{x_1;x_2}.\n#show a : x_2.\n#show b : x_2.\n#show.\n"); + } + SECTION("duplicate two") { + input << "#output b:b.\n#output a:b.\n"; + read(prg, input); + REQUIRE(output.str() == "{x_1;x_2}.\n#show b : x_2.\n#show a : x_2.\n#show.\n"); + } + SECTION("duplicate three") { + input << "#output a:a.\n#output b:b.\n#output c:b.\n"; + read(prg, input); + REQUIRE(output.str() == "{a;x_2}.\n#show b : x_2.\n#show c : x_2.\n#show.\n#show a : a.\n"); + } + } + SECTION("output reserved name") { + input << "{a;b}.\n"; + SECTION("id match") { + input << "#output x_2:b.\n#output x_1:a."; + read(prg, input); + REQUIRE(output.str() == "{x_1;x_2}.\n#show x_2 : x_2.\n#show x_1 : x_1.\n#show.\n"); + } + SECTION("id mismatch") { + input << "#output x_2:a.\n#output x_1:b."; + read(prg, input); + REQUIRE(output.str() == "{x_1;x_2}.\n#show x_2 : x_1.\n#show x_1 : x_2.\n#show.\n"); + } + } + SECTION("output duplicate reserved") { + out.initProgram(false); + out.beginStep(); + Atom_t a = 1; + auto al = lit(a); + out.rule(Head_t::Choice, {&a, 1}, {}); // {x_1}. + out.output(toSpan("x_1"), toSpan(&al, 1)); // #show x_1 : x_1. NOTE: uses reserved name "x_1" + out.output(toSpan("a"), toSpan(&al, 1)); // #show a : x_1. + SECTION("unique alternative") { + out.endStep(); + REQUIRE(output.str() == "{x_1}.\n#show x_1 : x_1.\n#show a : x_1.\n#show.\n"); + } + SECTION("two alternatives") { + out.output(toSpan("b"), toSpan(&al, 1)); // #show b : x_1. + out.endStep(); + REQUIRE(output.str() == "{x_1}.\n#show x_1 : x_1.\n#show a : x_1.\n#show b : x_1.\n#show.\n"); + } } SECTION("write external - ") { SECTION("default") { input << "#external x1."; read(prg, input); - REQUIRE(output.str() == "#external x_1.\n"); + REQUIRE(output.str() == "#external x_1.\n#show.\n"); } SECTION("false is default") { input << "#external x1. [false]"; read(prg, input); - REQUIRE(output.str() == "#external x_1.\n"); + REQUIRE(output.str() == "#external x_1.\n#show.\n"); } SECTION("with value") { input << "#external x1. [true]"; input << "#external x2. [free]"; input << "#external x3. [release]"; read(prg, input); - REQUIRE(output.str() == "#external x_1. [true]\n#external x_2. [free]\n#external x_3. [release]\n"); + REQUIRE(output.str() == "#external x_1. [true]\n#external x_2. [free]\n#external x_3. [release]\n#show.\n"); } } SECTION("empty assumption directive") { @@ -314,7 +419,7 @@ TEST_CASE("Text writer ", "[text]") { SECTION("assumption directive") { input << "#assume{x1,not x2,x3}."; read(prg, input); - REQUIRE(output.str() == "#assume{x_1, not x_2, x_3}.\n"); + REQUIRE(output.str() == "#assume{x_1, not x_2, x_3}.\n#show.\n"); } SECTION("empty projection directive") { input << "#project{}."; @@ -324,30 +429,30 @@ TEST_CASE("Text writer ", "[text]") { SECTION("projection directive") { input << "#project{x1,x2,x3}."; read(prg, input); - REQUIRE(output.str() == "#project{x_1, x_2, x_3}.\n"); + REQUIRE(output.str() == "#project{x_1, x_2, x_3}.\n#show.\n"); } SECTION("edge directive") { input << "#edge (0,1) : x1, not x2."; input << "#edge (1,0)."; read(prg, input); - REQUIRE(output.str() == "#edge(0,1) : x_1, not x_2.\n#edge(1,0).\n"); + REQUIRE(output.str() == "#edge(0,1) : x_1, not x_2.\n#edge(1,0).\n#show.\n"); } SECTION("heuristic directive -") { SECTION("simple") { input << "#heuristic a. [1,true]"; read(prg, input); - REQUIRE(output.str() == "#heuristic x_1. [1, true]\n"); + REQUIRE(output.str() == "#heuristic x_1. [1, true]\n#show.\n"); } SECTION("simple with priority") { input << "#heuristic a. [1@2,true]"; read(prg, input); - REQUIRE(output.str() == "#heuristic x_1. [1@2, true]\n"); + REQUIRE(output.str() == "#heuristic x_1. [1@2, true]\n#show.\n"); } SECTION("with condition") { input << "#heuristic a : b, not c. [1@2,true]"; read(prg, input); - REQUIRE(output.str() == "#heuristic x_1 : x_2, not x_3. [1@2, true]\n"); + REQUIRE(output.str() == "#heuristic x_1 : x_2, not x_3. [1@2, true]\n#show.\n"); } } SECTION("incremental program") { @@ -366,11 +471,34 @@ TEST_CASE("Text writer ", "[text]") { "% #program base.\n" "{a(1);x_2}.\n" "#external x_3.\n" + "#show.\n" + "#show a(1) : a(1).\n" "% #program step(1).\n" "x_3 :- a(1).\n" "% #program step(2).\n" "x_4 :- x_2, not x_3.\n"); } + SECTION("incremental output") { + input << "#incremental.\n"; + input << "{x1;x2}."; + input << "#output f : x2."; + input << "#step."; + input << "#output foo : x1."; + input << "x3 :- x1, x2."; + input << "#output f : x3."; + input << "#output nX2 : x2."; + read(prg, input); + prg.parse(); + REQUIRE(output.str() == "% #program base.\n" + "{x_1;f}.\n" + "#show.\n" + "#show f : f.\n" + "% #program step(1).\n" + "#show foo : x_1.\n" + "x_3 :- x_1, f.\n" + "#show f : x_3.\n" + "#show nX2 : f.\n"); + } } TEST_CASE("Text writer writes theory", "[text]") { @@ -436,7 +564,14 @@ TEST_CASE("Text writer writes theory", "[text]") { out.theoryElement(1, Potassco::toSpan(ids = {2}), Potassco::toSpan()); out.theoryAtom(1, 0, Potassco::toSpan(ids = {0, 1})); out.endStep(); - REQUIRE(output.str() == "x_2 :- &atom{x, y; y}.\n"); + REQUIRE(output.str() == "x_2 :- &atom{x, y; y}.\n#show.\n"); + } + SECTION("Fail on duplicate theory atom") { + out.theoryTerm(0, Potassco::toSpan("t")); + out.theoryTerm(1, Potassco::toSpan("x")); + out.theoryAtom(1, 0, {}); + out.theoryAtom(1, 1, {}); + REQUIRE_THROWS_AS(out.endStep(), std::logic_error); } SECTION("Theory element with condition") { std::vector head; @@ -444,18 +579,36 @@ TEST_CASE("Text writer writes theory", "[text]") { std::vector body; out.rule(Head_t::Choice, toSpan(head = {1, 2}), toSpan()); out.rule(Head_t::Disjunctive, toSpan(head = {4}), toSpan(body = {3})); - out.output(toSpan("y"), toSpan(body = {1})); - out.output(toSpan("z"), toSpan(body = {2})); out.theoryTerm(0, Potassco::toSpan("atom")); out.theoryTerm(1, Potassco::toSpan("elem")); out.theoryTerm(2, Potassco::toSpan("p")); out.theoryElement(0, Potassco::toSpan(ids = {1}), Potassco::toSpan(body = {1, -2})); out.theoryElement(1, Potassco::toSpan(ids = {2}), Potassco::toSpan(body = {1})); out.theoryAtom(3, 0, Potassco::toSpan(ids = {0, 1})); - out.endStep(); - REQUIRE(output.str() == - "{y;z}.\n" - "x_4 :- &atom{elem : y, not z; p : y}.\n"); + SECTION("default") { + out.endStep(); + REQUIRE(output.str() == "{x_1;x_2}.\n" + "x_4 :- &atom{elem : x_1, not x_2; p : x_1}.\n#show.\n"); + } + SECTION("override output") { + out.output(Potassco::toSpan("foo"), Potassco::toSpan((body = {3}))); + SECTION("once") { + out.endStep(); + // Ensure that we don't use "foo" for x_3. + REQUIRE(output.str() == "{x_1;x_2}.\n" + "x_4 :- &atom{elem : x_1, not x_2; p : x_1}.\n" + "#show foo : &atom{elem : x_1, not x_2; p : x_1}.\n#show.\n"); + } + SECTION("twice") { + out.output(Potassco::toSpan("bar"), Potassco::toSpan((body = {3}))); + out.endStep(); + REQUIRE(output.str() == "{x_1;x_2}.\n" + "x_4 :- &atom{elem : x_1, not x_2; p : x_1}.\n" + "#show foo : &atom{elem : x_1, not x_2; p : x_1}.\n" + "#show bar : &atom{elem : x_1, not x_2; p : x_1}.\n" + "#show.\n"); + } + } } SECTION("write complex atom incrementally") { out.initProgram(true); @@ -492,5 +645,24 @@ TEST_CASE("Text writer writes theory", "[text]") { "% #program step(1).\n" "&diff{end(2) - start(2)} <= 600.\n"); } + SECTION("invalid increment") { + out.initProgram(true); + out.beginStep(); + out.theoryTerm(0, Potassco::toSpan("t")); + std::vector head; + std::vector body; + out.rule(Head_t::Choice, Potassco::toSpan((head = {1, 2})), {}); + out.output(Potassco::toSpan("a"), Potassco::toSpan((body = {1}))); + out.output(Potassco::toSpan("b"), Potassco::toSpan((body = {2}))); + out.endStep(); + REQUIRE(output.str() == "% #program base.\n" + "{a;b}.\n"); + + output.str(""); + out.beginStep(); + out.theoryAtom(2, 0, {}); + out.rule(Head_t::Choice, Potassco::toSpan((head = {4})), Potassco::toSpan((body = {2}))); + REQUIRE_THROWS_AS(out.endStep(), std::logic_error); + } } }}}