From 95db8a640b5ee22aa546ec0c9a0175c06644401d Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Thu, 13 Jun 2024 15:38:15 +0200 Subject: [PATCH] Show predicates instead of terms if possible. --- potassco/aspif_text.h | 1 - src/aspif_text.cpp | 64 ++++++++++++++----- tests/test_text.cpp | 143 +++++++++++++++++++++++++----------------- 3 files changed, 134 insertions(+), 74 deletions(-) diff --git a/potassco/aspif_text.h b/potassco/aspif_text.h index 25437a3..467c67c 100644 --- a/potassco/aspif_text.h +++ b/potassco/aspif_text.h @@ -101,7 +101,6 @@ class AspifTextOutput : public Potassco::AbstractProgram { private: std::ostream& printName(std::ostream& os, Lit_t lit); - std::ostream& printHide(std::ostream& os); void writeDirectives(); void visitTheories(); bool assignAtomName(Atom_t id, const std::string& name); diff --git a/src/aspif_text.cpp b/src/aspif_text.cpp index c0c0f82..0899c2b 100644 --- a/src/aspif_text.cpp +++ b/src/aspif_text.cpp @@ -338,9 +338,27 @@ struct AspifTextOutput::Data { return node && node->second == atom ? &node->first : 0; } void setGenName(Atom_t atom) { - if (!genName) genName = &*strings.insert(StringMapVal(std::string(), 0)).first; + if (!genName) genName = &*strings.insert(StringMapVal(std::string(), idMax)).first; atoms.at(atom) = genName; } + static int atomArity(const std::string& name, std::size_t* sepPos = 0) { + if (name.empty() || name[0] == '&') return -1; + std::size_t pos = std::min(name.find('('), name.size()); + POTASSCO_REQUIRE(pos == name.size() || name.back() == ')', "invalid name"); + if (sepPos) *sepPos = pos; + if (name.size() - pos <= 2) { + return 0; + } + const char* args = name.data() + pos + 1; + int arity = 0; + for (StringSpan ignore;;) { + POTASSCO_REQUIRE(matchAtomArg(args, ignore), "invalid empty argument in name"); + ++arity; + if (*args++ == ')') break; + } + POTASSCO_REQUIRE(!*args, "invalid character in name"); + return arity; + } RawVec directives; StringMap strings; @@ -412,13 +430,6 @@ std::ostream& AspifTextOutput::printName(std::ostream& os, Lit_t lit) { maxAtom_ = std::max(maxAtom_, id); return os; } -std::ostream& AspifTextOutput::printHide(std::ostream& os) { - if (data_->genName && data_->atoms[0] == data_->genName) { - data_->atoms[0] = 0; - os << "#show.\n"; - } - return os; -} void AspifTextOutput::initProgram(bool incremental) { step_ = incremental ? 0 : -1; showAtoms_ = false; @@ -478,8 +489,14 @@ static bool isAtom(const StringSpan& s) { } void AspifTextOutput::output(const StringSpan& str, const LitSpan& cond) { - if (size(cond) == 1 && isAtom(str) && assignAtomName(atom(*begin(cond)), std::string(begin(str), end(str)))) { - return; + if (size(cond) == 1 && isAtom(str)) { + std::string name(begin(str), end(str)); + std::size_t ep; + if (Data::atomArity(name, &ep) == 0 && ep < name.size()) { + name.resize(ep); + } + if (assignAtomName(atom(*begin(cond)), name)) + return; } push(Directive_t::Output).push(data_->addOutputString(str)).push(cond); } @@ -587,7 +604,6 @@ void AspifTextOutput::writeDirectives() { for (uint32_t n = get(); n--; sep = ", ") { printName(os_ << sep, get()); } break; case Directive_t::Output: - printHide(os_); sep = " : "; term = "."; os_ << "#show " << data_->out[get()]->first; for (uint32_t n = get(); n--; sep = ", ") { @@ -629,14 +645,34 @@ void AspifTextOutput::writeDirectives() { os_ << term << "\n"; } if (showAtoms_) { - printHide(os_); + std::pair last; 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"; + std::size_t ep; + int arity = Data::atomArity(*n, &ep); + if (arity < 0) continue; + POTASSCO_ASSERT(ep != std::string::npos); + data_->atoms[0] = 0; // clear hide. + if (arity == 0) { + os_ << "#show " << *n << "/0.\n"; + } + else if (last.second != arity || n->compare(0, ep, last.first) != 0) { + last.first.resize(n->size()); + auto w = snprintf(last.first.data(), n->size(), "%.*s/%d", (int) ep, n->c_str(), arity); + assert(w > ep); + last.first.resize(w); + if (data_->strings.insert(Data::StringMapVal(last.first, idMax)).second) { + os_ << "#show " << last.first << ".\n"; + } + last.first.resize(ep); + last.second = arity; } } } + if (data_->atoms[0]) { + data_->atoms[0] = 0; + os_ << "#show.\n"; + } } os_ << std::flush; } diff --git a/tests/test_text.cpp b/tests/test_text.cpp index 508c085..ea21936 100644 --- a/tests/test_text.cpp +++ b/tests/test_text.cpp @@ -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#show.\n#show foo : foo.\n"); + REQUIRE(output.str() == "{foo;x_2}.\n#show foo/0.\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#show.\n#show foo : foo.\n"); + REQUIRE(output.str() == ":- foo, x_2.\n#show foo/0.\n"); } SECTION("empty integrity constraint") { input << ":-."; @@ -243,40 +243,42 @@ 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_2}.\n#show.\n#show x_1 : x_2.\n#show -a : -a.\n"); + REQUIRE(output.str() == "{-a;x_2}.\n#show x_1 : x_2.\n#show -a/0.\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#show.\n#show foo : foo.\n#show bar : bar.\n"); + REQUIRE(output.str() == "foo :- x_2, not bar, x_4.\n#show foo/0.\n#show bar/0.\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#show.\n#show foo : foo.\n#show bar : bar.\n"); + REQUIRE(output.str() == "{foo;x_2} :- not bar, x_4.\n#show foo/0.\n#show bar/0.\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#show.\n#show foo : foo.\n#show bar : bar.\n"); + REQUIRE(output.str() == "foo|x_2 :- not bar, x_4.\n#show foo/0.\n#show bar/0.\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#show.\n#show foo : foo.\n#show bar : bar.\n"); + REQUIRE(output.str() == "foo|x_2 :- 1 #count{1 : not bar; 2 : x_4}.\n#show foo/0.\n#show bar/0.\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#show.\n#show foo " - ": foo.\n#show bar : bar.\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 foo/0.\n#show bar/0.\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#show.\n#show foo : " - "foo.\n#show bar : bar.\n"); + REQUIRE(output.str() == "foo|x_2 :- 2 #count{1 : not bar; 2 : x_4; 3 : x_5; 4 : x_6}.\n#show foo/0.\n#show bar/0.\n"); + } + SECTION("convert sum rule with duplicate to cardinality rule") { + input << "x2 :- 3{x3=1, x4=1, x5=1,x3=1}.\n"; + read(prg, input); + REQUIRE(output.str() == "x_2 :- 3 #count{1 : x_3; 2 : x_4; 3 : x_5; 4 : x_3}.\n#show.\n"); } SECTION("minimize rule") { input << "#minimize{x1,x2=2,x3}.\n#minimize{not x1=3,not x2,not x3}@1."; @@ -288,13 +290,13 @@ TEST_CASE("Text writer ", "[text]") { 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.\n#show foo.\n#show \"Hello World\" : x_2, not bar.\n" - "#show bar : bar.\n"); + REQUIRE(output.str() == "{bar;x_2}.\n#show foo.\n#show \"Hello World\" : x_2, not bar.\n" + "#show bar/0.\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.\n#show x : x_1.\n#show y : x_1.\n"); + 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"; @@ -306,27 +308,27 @@ TEST_CASE("Text writer ", "[text]") { SECTION("simple") { input << "#output a:x1.\n#output a:x2.\n"; read(prg, input); - REQUIRE(output.str() == "{x_1;x_2}.\n#show.\n#show a : x_1.\n#show a : x_2.\n"); + 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.\n#show a : a, x_2.\n#show a : a.\n"); + REQUIRE(output.str() == "{a;x_2}.\n#show a : a, x_2.\n#show a/0.\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.\n#show a : a, x_2.\n#show a : a.\n"); + REQUIRE(output.str() == "{a;x_2}.\n#show a : a, x_2.\n#show a/0.\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.\n#show a : x_1.\n#show b : x_1.\n#show a : x_2.\n"); + 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.\n#show a : x_1.\n#show b : x_1.\n#show a : x_2.\n#show f : x_2.\n"); + 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") { @@ -343,22 +345,22 @@ TEST_CASE("Text writer ", "[text]") { SECTION("one") { input << "#output a:a.\n"; read(prg, input); - REQUIRE(output.str() == "{a;x_2}.\n#show.\n#show a : a.\n"); + REQUIRE(output.str() == "{a;x_2}.\n#show a/0.\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.\n#show a : x_2.\n#show b : x_2.\n"); + 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.\n#show b : x_2.\n#show a : x_2.\n"); + 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.\n#show b : x_2.\n#show c : x_2.\n#show a : a.\n"); + REQUIRE(output.str() == "{a;x_2}.\n#show b : x_2.\n#show c : x_2.\n#show a/0.\n"); } } SECTION("output reserved name") { @@ -367,46 +369,46 @@ TEST_CASE("Text writer ", "[text]") { SECTION("match") { input << "#output x_2:b.\n#output x_1:a."; read(prg, input); - REQUIRE(output.str() == "{x_1;x_2}.\n#show.\n#show x_2 : x_2.\n#show x_1 : x_1.\n"); + REQUIRE(output.str() == "{x_1;x_2}.\n#show x_2 : x_2.\n#show x_1 : x_1.\n#show.\n"); } SECTION("mismatch") { input << "#output x_2:a.\n#output x_1:b."; read(prg, input); - REQUIRE(output.str() == "{x_1;x_2}.\n#show.\n#show x_2 : x_1.\n#show x_1 : x_2.\n"); + REQUIRE(output.str() == "{x_1;x_2}.\n#show x_2 : x_1.\n#show x_1 : x_2.\n#show.\n"); } } SECTION("some") { SECTION("match") { input << "#output x_2:b."; read(prg, input); - REQUIRE(output.str() == "{x_1;x_2}.\n#show.\n#show x_2 : x_2.\n"); + REQUIRE(output.str() == "{x_1;x_2}.\n#show x_2 : x_2.\n#show.\n"); } SECTION("mismatch") { input << "#output x_2:a."; read(prg, input); - REQUIRE(output.str() == "{x_1;x_2}.\n#show.\n#show x_2 : x_1.\n"); + REQUIRE(output.str() == "{x_1;x_2}.\n#show x_2 : x_1.\n#show.\n"); } } SECTION("incremental handled as some") { - out.initProgram(true); - out.beginStep(); - std::vector head; - std::vector cond; - out.rule(Head_t::Choice, toSpan(head = {1, 2}), {}); // {1;2}. - out.output(toSpan("x_3"), toSpan(cond = {1})); // #show x_3 : 1. - out.output(toSpan("x_2"), toSpan(cond = {2})); // #show x_2 : 2. - out.endStep(); - REQUIRE(output.str() == "% #program base.\n" - "{x_1;x_2}.\n" - "#show.\n" - "#show x_3 : x_1.\n" - "#show x_2 : x_2.\n"); - output.str(""); - out.beginStep(); - out.rule(Head_t::Choice, toSpan(head = {3}), toSpan(cond = {1, 2})); // {3} :- 1, 2. - out.endStep(); - REQUIRE(output.str() == "% #program step(1).\n" - "{x_3} :- x_1, x_2.\n"); + out.initProgram(true); + out.beginStep(); + std::vector head; + std::vector cond; + out.rule(Head_t::Choice, toSpan(head = {1, 2}), {}); // {1;2}. + out.output(toSpan("x_3"), toSpan(cond = {1})); // #show x_3 : 1. + out.output(toSpan("x_2"), toSpan(cond = {2})); // #show x_2 : 2. + out.endStep(); + REQUIRE(output.str() == "% #program base.\n" + "{x_1;x_2}.\n" + "#show x_3 : x_1.\n" + "#show x_2 : x_2.\n" + "#show.\n"); + output.str(""); + out.beginStep(); + out.rule(Head_t::Choice, toSpan(head = {3}), toSpan(cond = {1, 2})); // {3} :- 1, 2. + out.endStep(); + REQUIRE(output.str() == "% #program step(1).\n" + "{x_3} :- x_1, x_2.\n"); } } SECTION("output duplicate reserved") { @@ -419,14 +421,41 @@ TEST_CASE("Text writer ", "[text]") { out.output(toSpan("a"), toSpan(&al, 1)); // #show a : x_1. SECTION("unique alternative") { out.endStep(); - REQUIRE(output.str() == "{x_1}.\n#show.\n#show x_1 : x_1.\n#show a : x_1.\n"); + 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.\n#show x_1 : x_1.\n#show a : x_1.\n#show b : x_1.\n"); + 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("output predicate") { + std::vector head; + std::vector cond; + out.initProgram(false); + out.beginStep(); + out.rule(Head_t::Choice, toSpan(head = {1, 2, 3, 4, 5}), {}); + out.output(toSpan("a"), toSpan(cond = {1})); + out.output(toSpan("a(1,2,3,4,5,6,7,8,9,10,11,12)"), toSpan(cond = {2})); + out.output(toSpan("b(t(1,2,3))"), toSpan(cond = {3})); + out.output(toSpan("b()"), toSpan(cond = {4})); + out.endStep(); + REQUIRE(output.str() == "{a;a(1,2,3,4,5,6,7,8,9,10,11,12);b(t(1,2,3));b;x_5}.\n#show a/0.\n#show " + "a/12.\n#show b/1.\n#show b/0.\n"); + } + SECTION("output invalid predicate") { + std::vector head; + std::vector cond; + out.initProgram(false); + out.beginStep(); + out.rule(Head_t::Choice, toSpan(head = {1}), {}); + SECTION("missing close") { REQUIRE_THROWS_AS(out.output(toSpan("a("), toSpan(cond = {1})), std::logic_error); } + SECTION("missing arg") { REQUIRE_THROWS_AS(out.output(toSpan("a(1,"), toSpan(cond = {1})), std::logic_error); } + SECTION("missing arg on close") { REQUIRE_THROWS_AS(out.output(toSpan("a(1,)"), toSpan(cond = {1})), std::logic_error); } + SECTION("empty arg") { REQUIRE_THROWS_AS(out.output(toSpan("a(1,,2)"), toSpan(cond = {1})), std::logic_error); } + SECTION("unmatched close") { REQUIRE_THROWS_AS(out.output(toSpan("a(x()"), toSpan(cond = {1})), std::logic_error); } + SECTION("empty arg 2") { REQUIRE_THROWS_AS(out.output(toSpan("b(,)"), toSpan(cond = {1})), std::logic_error); } + } SECTION("write external - ") { SECTION("default") { input << "#external x1."; @@ -506,8 +535,7 @@ 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" + "#show a/1.\n" "% #program step(1).\n" "x_3 :- a(1).\n" "% #program step(2).\n" @@ -526,8 +554,7 @@ TEST_CASE("Text writer ", "[text]") { prg.parse(); REQUIRE(output.str() == "% #program base.\n" "{x_1;f}.\n" - "#show.\n" - "#show f : f.\n" + "#show f/0.\n" "% #program step(1).\n" "#show foo : x_1.\n" "x_3 :- x_1, f.\n" @@ -632,15 +659,15 @@ TEST_CASE("Text writer writes theory", "[text]") { // 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.\n#show foo : &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.\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 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"); } } } @@ -675,9 +702,7 @@ TEST_CASE("Text writer writes theory", "[text]") { out.theoryElement(0, Potassco::toSpan(ids = {14}), Potassco::toSpan()); out.theoryAtom(0, 0, Potassco::toSpan(ids = {0}), 2, 1); out.endStep(); - REQUIRE(output.str() == - "% #program step(1).\n" - "&diff{end(2) - start(2)} <= 600.\n"); + REQUIRE(output.str() == "% #program step(1).\n&diff{end(2) - start(2)} <= 600.\n"); } SECTION("invalid increment") { out.initProgram(true);