From e85807accbc676c7e1ffc3b4f8157f69dcb89133 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 4 May 2018 13:26:20 +0200 Subject: [PATCH] Fix handling of rules with multielement head MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The code responsible for completing formulas made the assumption that all head variables could be safely removed from the list of free variables of each formula. This is only correct given the current limitation that only rules with singleton heads are supported. Because of this assumption, code with multiple elements in the head were completed to an incorrect result instead of issuing an error that such rules aren’t supported yet. This commit improves the code by excluding only variables that are actually replaced from the list of free variables and not all head variables. Still, other places will need to be adjusted for full support of rules with multiple elements in the head. For this reason, this also adds an error message indicating that only rules with singleton heads are supported as of now. Finally, multiple test cases are added to check that the supported features related to the issues outlined above are translated without exceptions, while errors are returned when attempting to use unsupported features. --- src/anthem/Completion.cpp | 38 ++++++++++++++------ tests/TestUnsupported.cpp | 73 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 101 insertions(+), 10 deletions(-) create mode 100644 tests/TestUnsupported.cpp diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp index c1f1507..2c21353 100644 --- a/src/anthem/Completion.cpp +++ b/src/anthem/Completion.cpp @@ -40,8 +40,36 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c assert(otherPredicate.arguments.size() == parameters.size()); + auto &freeVariables = scopedFormula.freeVariables; + // Each formula with the predicate as its consequent currently has its own copy of the predicate’s parameters // These need to be linked to the new, unique set of parameters + + // First, remove the free variables whose occurrences will be relinked, which is why they are no longer needed + const auto isFreeVariableUnneeded = + [&](const auto &freeVariable) + { + const auto matchesVariableToBeReplaced = std::find_if(otherPredicate.arguments.cbegin(), otherPredicate.arguments.cend(), + [&](const ast::Term &argument) + { + assert(argument.is()); + const auto &otherVariable = argument.get(); + + return (freeVariable.get() == otherVariable.declaration); + }); + + return (matchesVariableToBeReplaced != otherPredicate.arguments.cend()); + }; + + freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isFreeVariableUnneeded), freeVariables.end()); + + // Currently, only rules with singleton heads are supported + // Rules with multiple elements in the head are not yet handled correctly by the head variable detection mechanism + for (const auto &freeVariable : freeVariables) + if (freeVariable->type == ast::VariableDeclaration::Type::Head) + throw CompletionException("cannot perform completion, only singleton rule heads supported currently"); + + // Second, link all occurrences of the deleted free variable to the new, unique parameter for (size_t i = 0; i < parameters.size(); i++) { assert(otherPredicate.arguments[i].is()); @@ -50,16 +78,6 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c scopedFormula.formula.accept(ast::ReplaceVariableInFormulaVisitor(), scopedFormula.formula, otherVariable.declaration, parameters[i].get()); } - // Remove all the head variables, because they are not free variables after completion - const auto isHeadVariable = - [](const auto &variableDeclaration) - { - return variableDeclaration->type == ast::VariableDeclaration::Type::Head; - }; - - auto &freeVariables = scopedFormula.freeVariables; - freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isHeadVariable), freeVariables.end()); - if (freeVariables.empty()) disjunction.get().arguments.emplace_back(std::move(implies.antecedent)); else diff --git a/tests/TestUnsupported.cpp b/tests/TestUnsupported.cpp new file mode 100644 index 0000000..5ca45ee --- /dev/null +++ b/tests/TestUnsupported.cpp @@ -0,0 +1,73 @@ +#include + +#include + +#include +#include +#include + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +TEST_CASE("[unsupported] Errors are correctly issued when using unsupported features", "[unsupported]") +{ + std::stringstream input; + std::stringstream output; + std::stringstream errors; + + anthem::output::Logger logger(output, errors); + anthem::Context context(std::move(logger)); + + SECTION("rules with disjunctive head are unsupported") + { + context.performCompletion = true; + + input << "a; b."; + + CHECK_THROWS(anthem::translate("input", input, context)); + } + + SECTION("rules with disjunctive head containing elements with arguments are unsupported") + { + context.performCompletion = true; + + input << "p(a); p(b)."; + + CHECK_THROWS(anthem::translate("input", input, context)); + } + + SECTION("singleton choice rules are supported") + { + context.performCompletion = true; + + input << "{a}."; + + CHECK_NOTHROW(anthem::translate("input", input, context)); + } + + SECTION("singleton choice rules containing an element with arguments are supported") + { + context.performCompletion = true; + + input << "{p(a)}."; + + CHECK_NOTHROW(anthem::translate("input", input, context)); + } + + SECTION("choice rules with multiple simple elements are supported") + { + context.performCompletion = true; + + input << "{a; b}."; + + CHECK_NOTHROW(anthem::translate("input", input, context)); + } + + SECTION("choice rules with multiple elements with arguments are unsupported") + { + context.performCompletion = true; + + input << "{p(a); p(b)}."; + + CHECK_THROWS(anthem::translate("input", input, context)); + } +}