diff --git a/include/anthem/ASTUtils.h b/include/anthem/ASTUtils.h index b0ed1f9..a8efe12 100644 --- a/include/anthem/ASTUtils.h +++ b/include/anthem/ASTUtils.h @@ -4,6 +4,7 @@ #include #include +#include namespace anthem { @@ -36,12 +37,59 @@ class VariableStack //////////////////////////////////////////////////////////////////////////////////////////////////// -std::vector collectFreeVariables(Formula &formula); -std::vector collectFreeVariables(Formula &formula, VariableStack &variableStack); - bool matches(const Predicate &lhs, const Predicate &rhs); void collectPredicates(const Formula &formula, std::vector &predicates); +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Replacing Variables +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Replaces all occurrences of a variable in a given term with another term +struct ReplaceVariableInTermVisitor : public RecursiveTermVisitor +{ + static void accept(Variable &variable, Term &, const VariableDeclaration *original, VariableDeclaration *replacement) + { + if (variable.declaration == original) + variable.declaration = replacement; + } + + // Ignore all other types of expressions + template + static void accept(T &, Term &, const VariableDeclaration *, VariableDeclaration *) + { + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Replaces all occurrences of a variable in a given formula with a term +struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor +{ + static void accept(Comparison &comparison, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement) + { + comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement); + comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement); + } + + static void accept(In &in, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement) + { + in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, replacement); + in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, replacement); + } + + static void accept(Predicate &predicate, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement) + { + for (auto &argument : predicate.arguments) + argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement); + } + + // Ignore all other types of expressions + template + static void accept(T &, Formula &, const VariableDeclaration *, VariableDeclaration *) + { + } +}; + //////////////////////////////////////////////////////////////////////////////////////////////////// } diff --git a/include/anthem/Completion.h b/include/anthem/Completion.h index 11bd30c..44a137c 100644 --- a/include/anthem/Completion.h +++ b/include/anthem/Completion.h @@ -12,7 +12,7 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -void complete(std::vector &scopedFormulas); +std::vector complete(std::vector &&scopedFormulas); //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/anthem/ASTCopy.cpp b/src/anthem/ASTCopy.cpp index 8be5da7..d161873 100644 --- a/src/anthem/ASTCopy.cpp +++ b/src/anthem/ASTCopy.cpp @@ -16,56 +16,6 @@ namespace ast // //////////////////////////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////////////////////////// -// Replacing Variables -//////////////////////////////////////////////////////////////////////////////////////////////////// - -// Replaces all occurrences of a variable in a given term with another term -struct ReplaceVariableInTermVisitor : public RecursiveTermVisitor -{ - static void accept(Variable &variable, Term &, const VariableDeclaration *original, VariableDeclaration *replacement) - { - if (variable.declaration == original) - variable.declaration = replacement; - } - - // Ignore all other types of expressions - template - static void accept(T &, Term &, const VariableDeclaration *, VariableDeclaration *) - { - } -}; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -// Replaces all occurrences of a variable in a given formula with a term -struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor -{ - static void accept(Comparison &comparison, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement) - { - comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement); - comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement); - } - - static void accept(In &in, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement) - { - in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, replacement); - in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, replacement); - } - - static void accept(Predicate &predicate, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement) - { - for (auto &argument : predicate.arguments) - argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement); - } - - // Ignore all other types of expressions - template - static void accept(T &, Formula &, const VariableDeclaration *, VariableDeclaration *) - { - } -}; - //////////////////////////////////////////////////////////////////////////////////////////////////// // Preparing Copying //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/anthem/ASTUtils.cpp b/src/anthem/ASTUtils.cpp index 2faed08..23f3063 100644 --- a/src/anthem/ASTUtils.cpp +++ b/src/anthem/ASTUtils.cpp @@ -192,25 +192,6 @@ struct CollectFreeVariablesVisitor //////////////////////////////////////////////////////////////////////////////////////////////////// -std::vector collectFreeVariables(Formula &formula) -{ - VariableStack variableStack; - return collectFreeVariables(formula, variableStack); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -std::vector collectFreeVariables(Formula &formula, VariableStack &variableStack) -{ - std::vector freeVariables; - - formula.accept(CollectFreeVariablesVisitor(), variableStack, freeVariables); - - return freeVariables; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - struct CollectPredicatesVisitor : public RecursiveFormulaVisitor { static void accept(const Predicate &predicate, const Formula &, std::vector &predicates) diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp index eb2ed80..1fd254b 100644 --- a/src/anthem/Completion.cpp +++ b/src/anthem/Completion.cpp @@ -1,8 +1,10 @@ #include #include +#include #include #include +#include #include namespace anthem @@ -14,33 +16,14 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -// Copies the parameters of a predicate -std::vector> copyParameters(const ast::Predicate &predicate) -{ - std::vector> parameters; - /*parameters.reserve(predicate.arity()); - - for (const auto &argument : predicate.arguments) - { - assert(argument.is()); - // TODO: reimplement - //parameters.emplace_back(ast::deepCopy(parameter.get())); - }*/ - - return parameters; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - // Builds the conjunction within the completed formula for a given predicate -ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, std::vector> ¶meters, std::vector &scopedFormulas) +ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, const ast::VariableDeclarationPointers ¶meters, std::vector &scopedFormulas) { auto disjunction = ast::Formula::make(); - /*ast::VariableStack variableStack; - variableStack.push(¶meters); + assert(predicate.arguments.size() == parameters.size()); - // Build the conjunction of all formulas with the predicate as consequent + // Build the disjunction of all formulas with the predicate as consequent for (auto &scopedFormula : scopedFormulas) { assert(scopedFormula.formula.is()); @@ -54,18 +37,36 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, s if (!ast::matches(predicate, otherPredicate)) continue; - auto variables = ast::collectFreeVariables(implies.antecedent, variableStack); + assert(otherPredicate.arguments.size() == parameters.size()); - // TODO: avoid deep copies - // TODO: reimplement - if (variables.empty()) - disjunction.get().arguments.emplace_back(ast::deepCopy(implies.antecedent)); + // 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 + for (size_t i = 0; i < parameters.size(); i++) + { + assert(otherPredicate.arguments[i].is()); + const auto &otherVariable = otherPredicate.arguments[i].get(); + + 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 { - auto exists = ast::Formula::make(std::move(variables), ast::deepCopy(implies.antecedent)); + auto exists = ast::Formula::make(std::move(freeVariables), std::move(implies.antecedent)); disjunction.get().arguments.emplace_back(std::move(exists)); } - }*/ + } return disjunction; } @@ -77,7 +78,7 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo { assert(innerFormula.is()); - /*if (innerFormula.get().arguments.empty()) + if (innerFormula.get().arguments.empty()) return ast::Formula::make(std::move(predicate)); if (innerFormula.get().arguments.size() == 1) @@ -91,72 +92,77 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo return std::move(predicate); else return ast::Formula::make(std::move(predicate)); - }*/ + } return ast::Formula::make(std::move(predicate), std::move(innerFormula)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -void completePredicate(ast::Predicate &&predicate, std::vector &scopedFormulas, std::vector &completedScopedFormulas) +ast::Formula completePredicate(const ast::Predicate &predicate, std::vector &scopedFormulas) { - /*auto parameters = copyParameters(predicate); - auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicate, parameters, scopedFormulas); - auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicate), std::move(completedFormulaDisjunction)); + // Create new set of parameters for the completed definition for the predicate + ast::VariableDeclarationPointers parameters; + parameters.reserve(predicate.arguments.size()); - if (parameters.empty()) + std::vector arguments; + arguments.reserve(predicate.arguments.size()); + + for (size_t i = 0; i < predicate.arguments.size(); i++) { - completedFormulas.emplace_back(std::move(completedFormulaQuantified)); - return; + parameters.emplace_back(std::make_unique(ast::VariableDeclaration::Type::Head)); + arguments.emplace_back(ast::Term::make(parameters.back().get())); } - auto completedFormula = ast::Formula::make(std::move(parameters), std::move(completedFormulaQuantified)); - completedFormulas.emplace_back(std::move(completedFormula));*/ + ast::Predicate predicateCopy(std::string(predicate.name), std::move(arguments)); + + auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas); + auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction)); + + if (parameters.empty()) + return completedFormulaQuantified; + + return ast::Formula::make(std::move(parameters), std::move(completedFormulaQuantified)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -void completeIntegrityConstraint(ast::Formula &formula, std::vector &) +ast::Formula completeIntegrityConstraint(ast::ScopedFormula &scopedFormula) { - /*assert(formula.is()); - auto &implies = formula.get(); + assert(scopedFormula.formula.is()); + auto &implies = scopedFormula.formula.get(); assert(implies.consequent.is()); assert(implies.consequent.get().value == false); - auto variables = ast::collectFreeVariables(implies.antecedent); + auto argument = ast::Formula::make(std::move(implies.antecedent)); - // TODO: avoid deep copies - // TODO: reimplement - auto argument = ast::Formula::make(ast::deepCopy(implies.antecedent)); + auto &freeVariables = scopedFormula.freeVariables; - if (variables.empty()) - { - completedFormulas.emplace_back(std::move(argument)); - return; - } + if (freeVariables.empty()) + return argument; - auto completedFormula = ast::Formula::make(std::move(variables), std::move(argument)); - completedFormulas.emplace_back(std::move(completedFormula));*/ + return ast::Formula::make(std::move(freeVariables), std::move(argument)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -void complete(std::vector &scopedFormulas) +std::vector complete(std::vector &&scopedFormulas) { - /*// Check whether formulas are in normal form + // Check whether formulas are in normal form for (const auto &scopedFormula : scopedFormulas) { if (!scopedFormula.formula.is()) - throw std::runtime_error("cannot perform completion, formula not in normal form"); + throw CompletionException("cannot perform completion, formula not in normal form"); auto &implies = scopedFormula.formula.get(); if (!implies.consequent.is() && !implies.consequent.is()) - throw std::runtime_error("cannot perform completion, only single predicates and Booleans supported as formula consequent currently"); + throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently"); } std::vector predicates; + // Get a list of all predicates for (const auto &scopedFormula : scopedFormulas) ast::collectPredicates(scopedFormula.formula, predicates); @@ -171,24 +177,11 @@ void complete(std::vector &scopedFormulas) return lhs->arity() < rhs->arity(); }); - std::vector completedScopedFormulas; + std::vector completedFormulas; // Complete predicates for (const auto *predicate : predicates) - { - // Create the signature of the predicate - ast::Predicate signature(std::string(predicate->name)); - signature.arguments.reserve(predicate->arguments.size()); - - // TODO: reimplement - for (std::size_t i = 0; i < predicate->arguments.size(); i++) - { - auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i + 1); - signature.arguments.emplace_back(ast::Term::make(std::move(variableName), ast::VariableDeclaration::Type::Reserved)); - } - - completePredicate(std::move(signature), scopedFormulas, completedScopedFormulas); - } + completedFormulas.emplace_back(completePredicate(*predicate, scopedFormulas)); // Complete integrity constraints for (auto &scopedFormula : scopedFormulas) @@ -204,10 +197,10 @@ void complete(std::vector &scopedFormulas) if (boolean.value == true) continue; - completeIntegrityConstraint(scopedFormula.formula, completedScopedFormulas); + completedFormulas.emplace_back(completeIntegrityConstraint(scopedFormula)); } - std::swap(scopedFormulas, completedScopedFormulas);*/ + return completedFormulas; } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index d11f077..79e2c5e 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -59,14 +59,24 @@ void translate(const char *fileName, std::istream &stream, Context &context) for (auto &scopedFormula : scopedFormulas) simplify(scopedFormula.formula); - if (context.complete) - complete(scopedFormulas); - ast::PrintContext printContext; - for (const auto &scopedFormula : scopedFormulas) + if (!context.complete) { - ast::print(context.logger.outputStream(), scopedFormula.formula, printContext); + for (const auto &scopedFormula : scopedFormulas) + { + ast::print(context.logger.outputStream(), scopedFormula.formula, printContext); + context.logger.outputStream() << std::endl; + } + + return; + } + + auto completedFormulas = complete(std::move(scopedFormulas)); + + for (const auto &completedFormula : completedFormulas) + { + ast::print(context.logger.outputStream(), completedFormula, printContext); context.logger.outputStream() << std::endl; } } diff --git a/tests/TestCompletion.cpp b/tests/TestCompletion.cpp index 3052198..9c8f9c8 100644 --- a/tests/TestCompletion.cpp +++ b/tests/TestCompletion.cpp @@ -8,7 +8,7 @@ //////////////////////////////////////////////////////////////////////////////////////////////////// -/*TEST_CASE("[completion] Rules are completed", "[completion]") +TEST_CASE("[completion] Rules are completed", "[completion]") { std::stringstream input; std::stringstream output; @@ -75,12 +75,12 @@ CHECK(output.str() == "not q\n" "forall V1 not r(V1)\n" - "forall V1 not s(V1)\n" + "forall V2 not s(V2)\n" "not t\n" - "forall V1 not u(V1)\n" + "forall V3 not u(V3)\n" "not q\n" "not r(5)\n" - "forall N not s(N)\n" + "forall U1 not s(U1)\n" "not t\n" "not u(5)\n"); } @@ -126,7 +126,7 @@ CHECK(output.str() == "not p\n" "forall V1 not q(V1)\n" - "forall V1, V2 not t(V1, V2)\n" + "forall V2, V3 not t(V2, V3)\n" "not v\n"); } @@ -140,12 +140,9 @@ anthem::translate("input", input, context); CHECK(output.str() == - "forall V1 (covered(V1) <-> exists I, S (V1 = I and in(I, S)))\n" - "forall V1, V2 (in(V1, V2) <-> (V1 in 1..n and V2 in 1..r and in(V1, V2)))\n" - "forall I not (I in 1..n and not covered(I))\n" - "forall I, S, J not (in(I, S) and in(J, S) and exists X5 (X5 in (I + J) and in(X5, S)))\n"); + "forall V1 (covered(V1) <-> exists U1, U2 (V1 = U1 and in(U1, U2)))\n" + "forall V2, V3 (in(V2, V3) <-> (V2 in 1..n and V3 in 1..r and in(V2, V3)))\n" + "forall U3 not (U3 in 1..n and not covered(U3))\n" + "forall U4, U5, U6 not (in(U4, U5) and in(U6, U5) and exists X1 (X1 in (U4 + U6) and in(X1, U5)))\n"); } - - // TODO: test collecting free variables } -*/