diff --git a/include/anthem/AST.h b/include/anthem/AST.h index 4e29756..94e5af3 100644 --- a/include/anthem/AST.h +++ b/include/anthem/AST.h @@ -241,8 +241,10 @@ struct PredicateSignature PredicateSignature(const PredicateSignature &other) = delete; PredicateSignature &operator=(const PredicateSignature &other) = delete; - PredicateSignature(PredicateSignature &&other) noexcept = default; - PredicateSignature &operator=(PredicateSignature &&other) noexcept = default; + // TODO: make noexcept again + // GCC versions before 7 don’t declare moving std::string noexcept and would complain here + PredicateSignature(PredicateSignature &&other) = default; + PredicateSignature &operator=(PredicateSignature &&other) = default; std::string name; size_t arity; diff --git a/include/anthem/ASTUtils.h b/include/anthem/ASTUtils.h index a8efe12..113cd3a 100644 --- a/include/anthem/ASTUtils.h +++ b/include/anthem/ASTUtils.h @@ -38,7 +38,9 @@ class VariableStack //////////////////////////////////////////////////////////////////////////////////////////////////// bool matches(const Predicate &lhs, const Predicate &rhs); -void collectPredicates(const Formula &formula, std::vector &predicates); +bool matches(const Predicate &predicate, const PredicateSignature &signature); +bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs); +void collectPredicateSignatures(const Formula &formula, std::vector &predicateSignatures); //////////////////////////////////////////////////////////////////////////////////////////////////// // Replacing Variables diff --git a/include/anthem/Completion.h b/include/anthem/Completion.h index 44a137c..29b406a 100644 --- a/include/anthem/Completion.h +++ b/include/anthem/Completion.h @@ -2,6 +2,7 @@ #define __ANTHEM__COMPLETION_H #include +#include namespace anthem { @@ -12,7 +13,7 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -std::vector complete(std::vector &&scopedFormulas); +std::vector complete(std::vector &&scopedFormulas, Context &context); //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/HiddenPredicateElimination.h b/include/anthem/HiddenPredicateElimination.h new file mode 100644 index 0000000..8016ffa --- /dev/null +++ b/include/anthem/HiddenPredicateElimination.h @@ -0,0 +1,22 @@ +#ifndef __ANTHEM__HIDDEN_PREDICATE_ELIMINATION_H +#define __ANTHEM__HIDDEN_PREDICATE_ELIMINATION_H + +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// HiddenPredicateElimination +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void eliminateHiddenPredicates(const std::vector &predicateSignatures, std::vector &completedFormulas, Context &context); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} + +#endif diff --git a/src/anthem/ASTUtils.cpp b/src/anthem/ASTUtils.cpp index 23f3063..34ab31a 100644 --- a/src/anthem/ASTUtils.cpp +++ b/src/anthem/ASTUtils.cpp @@ -192,23 +192,26 @@ struct CollectFreeVariablesVisitor //////////////////////////////////////////////////////////////////////////////////////////////////// -struct CollectPredicatesVisitor : public RecursiveFormulaVisitor +struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor { - static void accept(const Predicate &predicate, const Formula &, std::vector &predicates) + static void accept(const Predicate &predicate, const Formula &, std::vector &predicateSignatures) { - const auto predicateMatches = - [&predicate](const auto *otherPredicate) + const auto predicateSignatureMatches = + [&predicate](const auto &predicateSignature) { - return matches(predicate, *otherPredicate); + return matches(predicate, predicateSignature); }; - if (std::find_if(predicates.cbegin(), predicates.cend(), predicateMatches) == predicates.cend()) - predicates.emplace_back(&predicate); + if (std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), predicateSignatureMatches) != predicateSignatures.cend()) + return; + + // TODO: avoid copies + predicateSignatures.emplace_back(std::string(predicate.name), predicate.arity()); } // Ignore all other types of expressions template - static void accept(const T &, const Formula &, std::vector &) + static void accept(const T &, const Formula &, std::vector &) { } }; @@ -222,11 +225,25 @@ bool matches(const Predicate &lhs, const Predicate &rhs) //////////////////////////////////////////////////////////////////////////////////////////////////// +bool matches(const Predicate &predicate, const PredicateSignature &signature) +{ + return (predicate.name == signature.name && predicate.arity() == signature.arity); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs) +{ + return (lhs.name == rhs.name && lhs.arity == rhs.arity); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + // TODO: remove const_cast -void collectPredicates(const Formula &formula, std::vector &predicates) +void collectPredicateSignatures(const Formula &formula, std::vector &predicateSignatures) { auto &formulaMutable = const_cast(formula); - formulaMutable.accept(CollectPredicatesVisitor(), formulaMutable, predicates); + formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp index 420d4ba..c8c435e 100644 --- a/src/anthem/Completion.cpp +++ b/src/anthem/Completion.cpp @@ -5,6 +5,7 @@ #include #include #include +#include #include namespace anthem @@ -99,22 +100,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo //////////////////////////////////////////////////////////////////////////////////////////////////// -ast::Formula completePredicate(const ast::Predicate &predicate, std::vector &scopedFormulas) +ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector &scopedFormulas) { // Create new set of parameters for the completed definition for the predicate ast::VariableDeclarationPointers parameters; - parameters.reserve(predicate.arguments.size()); + parameters.reserve(predicateSignature.arity); std::vector arguments; - arguments.reserve(predicate.arguments.size()); + arguments.reserve(predicateSignature.arity); - for (size_t i = 0; i < predicate.arguments.size(); i++) + for (size_t i = 0; i < predicateSignature.arity; i++) { parameters.emplace_back(std::make_unique(ast::VariableDeclaration::Type::Head)); arguments.emplace_back(ast::Term::make(parameters.back().get())); } - ast::Predicate predicateCopy(std::string(predicate.name), std::move(arguments)); + ast::Predicate predicateCopy(std::string(predicateSignature.name), std::move(arguments)); auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas); auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction)); @@ -146,7 +147,7 @@ ast::Formula completeIntegrityConstraint(ast::ScopedFormula &scopedFormula) //////////////////////////////////////////////////////////////////////////////////////////////////// -std::vector complete(std::vector &&scopedFormulas) +std::vector complete(std::vector &&scopedFormulas, Context &context) { // Check whether formulas are in normal form for (const auto &scopedFormula : scopedFormulas) @@ -160,28 +161,28 @@ std::vector complete(std::vector &&scopedFormu throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently"); } - std::vector predicates; + std::vector predicateSignatures; // Get a list of all predicates for (const auto &scopedFormula : scopedFormulas) - ast::collectPredicates(scopedFormula.formula, predicates); + ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures); - std::sort(predicates.begin(), predicates.end(), - [](const auto *lhs, const auto *rhs) + std::sort(predicateSignatures.begin(), predicateSignatures.end(), + [](const auto &lhs, const auto &rhs) { - const auto order = std::strcmp(lhs->name.c_str(), rhs->name.c_str()); + const auto order = std::strcmp(lhs.name.c_str(), rhs.name.c_str()); if (order != 0) - return order < 0; + return (order < 0); - return lhs->arity() < rhs->arity(); + return lhs.arity < rhs.arity; }); std::vector completedFormulas; // Complete predicates - for (const auto *predicate : predicates) - completedFormulas.emplace_back(completePredicate(*predicate, scopedFormulas)); + for (const auto &predicateSignature : predicateSignatures) + completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas)); // Complete integrity constraints for (auto &scopedFormula : scopedFormulas) @@ -200,6 +201,9 @@ std::vector complete(std::vector &&scopedFormu completedFormulas.emplace_back(completeIntegrityConstraint(scopedFormula)); } + // Eliminate all predicates that should not be visible in the output + eliminateHiddenPredicates(predicateSignatures, completedFormulas, context); + return completedFormulas; } diff --git a/src/anthem/HiddenPredicateElimination.cpp b/src/anthem/HiddenPredicateElimination.cpp new file mode 100644 index 0000000..a3c72d8 --- /dev/null +++ b/src/anthem/HiddenPredicateElimination.cpp @@ -0,0 +1,268 @@ +#include + +#include +#include +#include +#include +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// HiddenPredicateElimination +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct PredicateReplacement +{ + const ast::Predicate &predicate; + ast::Formula replacement; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Replaces all occurrences of a variable in a given term with another variable +struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor +{ + static void accept(ast::Variable &variable, ast::Term &, const ast::VariableDeclaration &original, ast::VariableDeclaration &replacement) + { + if (variable.declaration == &original) + // No dangling variables can result from this operation, and hence, fixing them is not necessary + variable.declaration = &replacement; + } + + // Ignore all other types of expressions + template + static void accept(T &, ast::Term &, const ast::VariableDeclaration &, ast::VariableDeclaration &) + { + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Replaces all occurrences of a variable in a given formula with another variable +struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor +{ + static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration &original, ast::VariableDeclaration &replacement) + { + comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement); + comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement); + } + + static void accept(ast::In &in, ast::Formula &, const ast::VariableDeclaration &original, ast::VariableDeclaration &replacement) + { + in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, replacement); + in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, replacement); + } + + static void accept(ast::Predicate &predicate, ast::Formula &, const ast::VariableDeclaration &original, ast::VariableDeclaration &replacement) + { + for (auto &argument : predicate.arguments) + argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement); + } + + // Ignore all other types of expressions + template + static void accept(T &, ast::Formula &, const ast::VariableDeclaration &, ast::VariableDeclaration &) + { + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Replace a predicate in a term with a formula +struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor +{ + static void accept(ast::Predicate &predicate, ast::Formula &formula, const PredicateReplacement &predicateReplacement) + { + if (!ast::matches(predicate, predicateReplacement.predicate)) + return; + + auto formulaReplacement = ast::prepareCopy(predicateReplacement.replacement); + + for (size_t i = 0; i < predicate.arguments.size(); i++) + { + assert(predicateReplacement.predicate.arguments[i].is()); + const auto &original = *predicateReplacement.predicate.arguments[i].get().declaration; + + assert(predicate.arguments[i].is()); + auto &replacement = *predicate.arguments[i].get().declaration; + + formulaReplacement.accept(ReplaceVariableInFormulaVisitor(), formulaReplacement, original, replacement); + } + + formula = std::move(formulaReplacement); + } + + // Ignore all other types of expressions + template + static void accept(T &, ast::Formula &, const PredicateReplacement &) + { + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Detect whether a formula contains a circular dependency on a given predicate +struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor +{ + static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateSignature &predicateSignature, bool &hasCircularDependency) + { + if (ast::matches(predicate, predicateSignature)) + hasCircularDependency = true; + } + + // Ignore all other types of expressions + template + static void accept(T &, ast::Formula &, const ast::PredicateSignature &, bool &) + { + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)” +PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::ForAll &forAll) +{ + // Declare variable used, only used in debug mode + (void)(predicateSignature); + + // Form: “forall X1, ..., Xn p(X1, ..., Xn)” + // Replace with “#true” + if (forAll.argument.is()) + { + assert(ast::matches(forAll.argument.get(), predicateSignature)); + + return {forAll.argument.get(), ast::Formula::make(true)}; + } + + // Form: “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)” + // Replace with “#false” + if (forAll.argument.is()) + { + auto ¬Argument = forAll.argument.get().argument; + + assert(notArgument.is()); + assert(ast::matches(notArgument.get(), predicateSignature)); + + return {notArgument.get(), ast::Formula::make(false)}; + } + + assert(forAll.argument.is()); + + const auto &biconditional = forAll.argument.get(); + + assert(biconditional.left.is()); + assert(ast::matches(biconditional.left.get(), predicateSignature)); + + // TODO: avoid copy + return {biconditional.left.get(), ast::prepareCopy(biconditional.right)}; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Finds a replacement for a predicate that should be hidden +PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Formula &completedPredicateDefinition) +{ + if (completedPredicateDefinition.is()) + return findReplacement(predicateSignature, completedPredicateDefinition.get()); + else if (completedPredicateDefinition.is()) + return {completedPredicateDefinition.get(), ast::Formula::make(true)}; + else if (completedPredicateDefinition.is()) + { + const auto ¬Argument = completedPredicateDefinition.get().argument; + assert(notArgument.is()); + + return {notArgument.get(), ast::Formula::make(false)}; + } + + throw CompletionException("invalid completed predicate definition for predicate “" + predicateSignature.name + "/" + std::to_string(predicateSignature.arity) + "”"); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void eliminateHiddenPredicates(const std::vector &predicateSignatures, std::vector &completedFormulas, Context &context) +{ + if (!context.visiblePredicateSignatures) + { + context.logger.log(output::Priority::Debug) << "no predicates to be eliminated"; + return; + } + + const auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value(); + + // Check for undeclared predicates that are requested to be shown + for (const auto &visiblePredicateSignature : visiblePredicateSignatures) + { + const auto matchesPredicateSignature = + [&](const auto &predicateSignature) + { + return ast::matches(predicateSignature, visiblePredicateSignature); + }; + + const auto matchingPredicateSignature = + std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature); + + if (matchingPredicateSignature == predicateSignatures.cend()) + context.logger.log(output::Priority::Warning) << "cannot show undeclared predicate “" << visiblePredicateSignature.name << "/" << visiblePredicateSignature.arity <<"”"; + } + + // Replace all occurrences of hidden predicates + for (size_t i = 0; i < predicateSignatures.size(); i++) + { + auto &predicateSignature = predicateSignatures[i]; + + const auto matchesVisiblePredicateSignature = + [&](const auto &visiblePredicateSignature) + { + return ast::matches(predicateSignature, visiblePredicateSignature); + }; + + const auto matchingPredicateSignature = + std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesVisiblePredicateSignature); + + // If the predicate ought to be visible, don’t eliminate it + if (matchingPredicateSignature != visiblePredicateSignatures.cend()) + continue; + + context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "”"; + + const auto &completedPredicateDefinition = completedFormulas[i]; + auto replacement = findReplacement(predicateSignature, completedPredicateDefinition); + + bool hasCircularDependency = false; + replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, predicateSignature, hasCircularDependency); + + if (hasCircularDependency) + { + context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateSignature.name << "/" << predicateSignature.arity << "” due to circular dependency"; + continue; + } + + for (size_t j = 0; j < completedFormulas.size(); j++) + if (j != i) + completedFormulas[j].accept(ReplacePredicateInFormulaVisitor(), completedFormulas[j], replacement); + + // TODO: refactor + completedFormulas[i] = ast::Formula::make(true); + } + + const auto canBeRemoved = + [&](const ast::Formula &completedFormula) + { + if (!completedFormula.is()) + return false; + + return completedFormula.get().value == true; + }; + + auto removedFormulas = std::remove_if(completedFormulas.begin(), completedFormulas.end(), canBeRemoved); + completedFormulas.erase(removedFormulas, completedFormulas.end()); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index 8a41a24..a221685 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -77,7 +77,7 @@ void translate(const char *fileName, std::istream &stream, Context &context) return; } - auto completedFormulas = complete(std::move(scopedFormulas)); + auto completedFormulas = complete(std::move(scopedFormulas), context); // TODO: rethink simplification steps if (context.simplify)