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)); + } +}