From d0debc6ad1a6c4aca1a54bbf279560fcde19d803 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 13 Apr 2018 20:40:40 +0200 Subject: [PATCH] Split predicates from their declarations This refactoring separates predicates from their declarations. The purpose of this is to avoid duplicating properties specific to the predicate declaration and not its occurrences in the program. --- include/anthem/AST.h | 40 ++++----- include/anthem/ASTForward.h | 1 + include/anthem/ASTUtils.h | 6 -- include/anthem/Body.h | 34 ++++---- include/anthem/Context.h | 31 ++++++- include/anthem/Equality.h | 2 +- include/anthem/Head.h | 32 ++++---- include/anthem/HiddenPredicateElimination.h | 2 +- include/anthem/StatementVisitor.h | 21 +++-- include/anthem/output/AST.h | 10 ++- src/anthem/ASTCopy.cpp | 2 +- src/anthem/ASTUtils.cpp | 79 ------------------ src/anthem/Completion.cpp | 35 ++++---- src/anthem/HiddenPredicateElimination.cpp | 90 +++++++++------------ src/anthem/Translation.cpp | 44 +++++----- 15 files changed, 187 insertions(+), 242 deletions(-) diff --git a/include/anthem/AST.h b/include/anthem/AST.h index f7298fb..8a770ec 100644 --- a/include/anthem/AST.h +++ b/include/anthem/AST.h @@ -187,13 +187,13 @@ struct Interval struct Predicate { - explicit Predicate(std::string &&name) - : name{std::move(name)} + explicit Predicate(PredicateDeclaration *declaration) + : declaration{declaration} { } - explicit Predicate(std::string &&name, std::vector &&arguments) - : name{std::move(name)}, + explicit Predicate(PredicateDeclaration *declaration, std::vector &&arguments) + : declaration{declaration}, arguments{std::move(arguments)} { } @@ -203,35 +203,37 @@ struct Predicate Predicate(Predicate &&other) noexcept = default; Predicate &operator=(Predicate &&other) noexcept = default; - std::size_t arity() const - { - return arguments.size(); - } - - std::string name; + PredicateDeclaration *declaration{nullptr}; std::vector arguments; }; //////////////////////////////////////////////////////////////////////////////////////////////////// -// TODO: make more use of this class -struct PredicateSignature +struct PredicateDeclaration { - explicit PredicateSignature(std::string &&name, size_t arity) + enum class Visibility + { + Default, + Visible, + Hidden + }; + + explicit PredicateDeclaration(std::string &&name, size_t arity) : name{std::move(name)}, arity{arity} { } - PredicateSignature(const PredicateSignature &other) = delete; - PredicateSignature &operator=(const PredicateSignature &other) = delete; - // 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; + PredicateDeclaration(const PredicateDeclaration &other) = delete; + PredicateDeclaration &operator=(const PredicateDeclaration &other) = delete; + PredicateDeclaration(PredicateDeclaration &&other) noexcept = default; + PredicateDeclaration &operator=(PredicateDeclaration &&other) noexcept = default; std::string name; size_t arity; + bool isUsed{false}; + bool isExternal{false}; + Visibility visibility{Visibility::Default}; }; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/ASTForward.h b/include/anthem/ASTForward.h index 5a0619a..10c1a65 100644 --- a/include/anthem/ASTForward.h +++ b/include/anthem/ASTForward.h @@ -34,6 +34,7 @@ struct Interval; struct Not; struct Or; struct Predicate; +struct PredicateDeclaration; struct SpecialInteger; struct String; struct UnaryOperation; diff --git a/include/anthem/ASTUtils.h b/include/anthem/ASTUtils.h index dfb2470..75d6623 100644 --- a/include/anthem/ASTUtils.h +++ b/include/anthem/ASTUtils.h @@ -36,12 +36,6 @@ class VariableStack std::vector m_layers; }; -//////////////////////////////////////////////////////////////////////////////////////////////////// - -bool matches(const Predicate &lhs, const Predicate &rhs); -bool matches(const Predicate &predicate, const PredicateSignature &signature); -bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs); -void collectPredicateSignatures(const Formula &formula, std::vector &predicateSignatures, Context &context); //////////////////////////////////////////////////////////////////////////////////////////////////// // Replacing Variables diff --git a/include/anthem/Body.h b/include/anthem/Body.h index 3b30e3d..9995c86 100644 --- a/include/anthem/Body.h +++ b/include/anthem/Body.h @@ -43,19 +43,22 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp struct BodyTermTranslateVisitor { // TODO: refactor - std::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Function &function, + const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, + Context &context, ast::VariableStack &variableStack) { if (literal.sign == Clingo::AST::Sign::DoubleNegation) throw TranslationException(literal.location, "double-negated literals currently unsupported"); + auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size()); + predicateDeclaration->isUsed = true; + if (function.arguments.empty()) { - auto predicate = ast::Formula::make(std::string(function.name)); - if (literal.sign == Clingo::AST::Sign::None) - return std::move(predicate); + return ast::Predicate(predicateDeclaration); else if (literal.sign == Clingo::AST::Sign::Negation) - return ast::Formula::make(std::move(predicate)); + return ast::Formula::make(ast::Predicate(predicateDeclaration)); } // Create new body variable declarations @@ -78,7 +81,7 @@ struct BodyTermTranslateVisitor variableStack.pop(); - ast::Predicate predicate(std::string(function.name)); + ast::Predicate predicate(predicateDeclaration); predicate.arguments.reserve(function.arguments.size()); for (size_t i = 0; i < function.arguments.size(); i++) @@ -93,7 +96,8 @@ struct BodyTermTranslateVisitor } template - std::optional visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &) + std::optional visit(const T &, const Clingo::AST::Literal &, + const Clingo::AST::Term &term, RuleContext &, Context &, ast::VariableStack &) { assert(!term.data.is()); @@ -106,18 +110,18 @@ struct BodyTermTranslateVisitor struct BodyLiteralTranslateVisitor { - std::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &) + std::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, ast::VariableStack &) { return ast::Formula::make(boolean.value); } - std::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack) { - return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, variableStack); + return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, context, variableStack); } // TODO: refactor - std::optional visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &, ast::VariableStack &variableStack) { // Comparisons should never have a sign, because these are converted to positive comparisons by clingo if (literal.sign != Clingo::AST::Sign::None) @@ -140,7 +144,7 @@ struct BodyLiteralTranslateVisitor } template - std::optional visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &) + std::optional visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, ast::VariableStack &) { throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term"); return std::nullopt; @@ -151,16 +155,16 @@ struct BodyLiteralTranslateVisitor struct BodyBodyLiteralTranslateVisitor { - std::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack) { if (bodyLiteral.sign != Clingo::AST::Sign::None) throw TranslationException(bodyLiteral.location, "only positive body literals supported currently"); - return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, variableStack); + return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, context, variableStack); } template - std::optional visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &) + std::optional visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, Context &, ast::VariableStack &) { throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal"); return std::nullopt; diff --git a/include/anthem/Context.h b/include/anthem/Context.h index b1d0924..24acbdc 100644 --- a/include/anthem/Context.h +++ b/include/anthem/Context.h @@ -16,9 +16,9 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -struct PredicateSignatureMeta +struct PredicateDeclarationMeta { - ast::PredicateSignature predicateSignature; + ast::PredicateDeclaration *declaration; bool used{false}; }; @@ -33,13 +33,36 @@ struct Context { } + ast::PredicateDeclaration *findOrCreatePredicateDeclaration(const char *name, size_t arity) + { + const auto matchesExistingPredicateDeclaration = + [&](const auto &predicateDeclaration) + { + return (predicateDeclaration->arity == arity + && strcmp(predicateDeclaration->name.c_str(), name) == 0); + }; + + auto matchingPredicateDeclaration = std::find_if(predicateDeclarations.begin(), + predicateDeclarations.end(), matchesExistingPredicateDeclaration); + + if (matchingPredicateDeclaration != predicateDeclarations.end()) + return matchingPredicateDeclaration->get(); + + predicateDeclarations.emplace_back(std::make_unique(name, arity)); + + return predicateDeclarations.back().get(); + } + output::Logger logger; bool performSimplification{false}; bool performCompletion{false}; - std::optional> visiblePredicateSignatures; - std::optional> externalPredicateSignatures; + std::vector> predicateDeclarations; + ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible}; + + bool externalStatementsUsed{false}; + bool showStatementsUsed{false}; ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal; }; diff --git a/include/anthem/Equality.h b/include/anthem/Equality.h index bbe3a09..7c5c83b 100644 --- a/include/anthem/Equality.h +++ b/include/anthem/Equality.h @@ -237,7 +237,7 @@ struct FormulaEqualityVisitor const auto &otherPredicate = otherFormula.get(); - if (!matches(predicate, otherPredicate)) + if (predicate.declaration != otherPredicate.declaration) return Tristate::False; assert(predicate.arguments.size() == otherPredicate.arguments.size()); diff --git a/include/anthem/Head.h b/include/anthem/Head.h index f4804a0..66a9198 100644 --- a/include/anthem/Head.h +++ b/include/anthem/Head.h @@ -118,8 +118,7 @@ struct HeadLiteralCollectFunctionTermsVisitor struct FunctionTermTranslateVisitor { - // TODO: check correctness - std::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex) + std::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, size_t &headVariableIndex) { if (function.external) throw TranslationException(term.location, "external functions currently unsupported"); @@ -130,11 +129,14 @@ struct FunctionTermTranslateVisitor for (size_t i = 0; i < function.arguments.size(); i++) arguments.emplace_back(ast::Variable(ruleContext.freeVariables[headVariableIndex++].get())); - return ast::Formula::make(function.name, std::move(arguments)); + auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size()); + predicateDeclaration->isUsed = true; + + return ast::Predicate(predicateDeclaration, std::move(arguments)); } template - std::optional visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &) + std::optional visit(const T &, const Clingo::AST::Term &term, RuleContext &, Context &, size_t &) { throw TranslationException(term.location, "term currently unsupported in this context, function expected"); return std::nullopt; @@ -145,18 +147,18 @@ struct FunctionTermTranslateVisitor struct LiteralTranslateVisitor { - std::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &) + std::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, size_t &) { return ast::Formula::make(boolean.value); } - std::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, size_t &headVariableIndex) + std::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex) { - return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, headVariableIndex); + return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, context, headVariableIndex); } template - std::optional visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &) + std::optional visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, size_t &) { throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals"); return std::nullopt; @@ -167,12 +169,12 @@ struct LiteralTranslateVisitor struct HeadLiteralTranslateToConsequentVisitor { - std::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex) + std::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex) { if (literal.sign == Clingo::AST::Sign::DoubleNegation) throw TranslationException(literal.location, "double-negated head literals currently unsupported"); - auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, headVariableIndex); + auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, context, headVariableIndex); if (literal.sign == Clingo::AST::Sign::None) return translatedLiteral; @@ -183,7 +185,7 @@ struct HeadLiteralTranslateToConsequentVisitor return ast::Formula::make(std::move(translatedLiteral.value())); } - std::optional visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex) + std::optional visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex) { std::vector arguments; arguments.reserve(disjunction.elements.size()); @@ -193,7 +195,7 @@ struct HeadLiteralTranslateToConsequentVisitor if (!conditionalLiteral.condition.empty()) throw TranslationException(headLiteral.location, "conditional head literals currently unsupported"); - auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex); + auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex); if (!argument) throw TranslationException(headLiteral.location, "could not parse argument"); @@ -204,7 +206,7 @@ struct HeadLiteralTranslateToConsequentVisitor return ast::Formula::make(std::move(arguments)); } - std::optional visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex) + std::optional visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex) { if (aggregate.left_guard || aggregate.right_guard) throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported"); @@ -215,7 +217,7 @@ struct HeadLiteralTranslateToConsequentVisitor if (!conditionalLiteral.condition.empty()) throw TranslationException(headLiteral.location, "conditional head literals currently unsupported"); - return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex); + return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex); }; if (aggregate.elements.size() == 1) @@ -238,7 +240,7 @@ struct HeadLiteralTranslateToConsequentVisitor } template - std::optional visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &) + std::optional visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, Context &, size_t &) { throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate"); return std::nullopt; diff --git a/include/anthem/HiddenPredicateElimination.h b/include/anthem/HiddenPredicateElimination.h index 8016ffa..a62e912 100644 --- a/include/anthem/HiddenPredicateElimination.h +++ b/include/anthem/HiddenPredicateElimination.h @@ -13,7 +13,7 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -void eliminateHiddenPredicates(const std::vector &predicateSignatures, std::vector &completedFormulas, Context &context); +void eliminateHiddenPredicates(std::vector &completedFormulas, Context &context); //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h index 74517d4..bd0d21d 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -73,7 +73,7 @@ struct StatementVisitor // Compute consequent auto headVariableIndex = ruleContext.headVariablesStartIndex; - auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, headVariableIndex); + auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, context, headVariableIndex); assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex); @@ -98,7 +98,7 @@ struct StatementVisitor { const auto &bodyLiteral = *i; - auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, variableStack); + auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, context, variableStack); if (!argument) throw TranslationException(bodyLiteral.location, "could not translate body literal"); @@ -165,8 +165,8 @@ struct StatementVisitor if (signature.negative()) throw LogicException(statement.location, "negative #show atom signatures are currently unsupported"); - if (!context.visiblePredicateSignatures) - context.visiblePredicateSignatures.emplace(); + context.showStatementsUsed = true; + context.defaultPredicateVisibility = ast::PredicateDeclaration::Visibility::Hidden; if (std::strlen(signature.name()) == 0) { @@ -176,8 +176,8 @@ struct StatementVisitor context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”"; - auto predicateSignature = ast::PredicateSignature{std::string(signature.name()), signature.arity()}; - context.visiblePredicateSignatures.value().emplace_back(PredicateSignatureMeta{std::move(predicateSignature)}); + auto predicateDeclaration = context.findOrCreatePredicateDeclaration(signature.name(), signature.arity()); + predicateDeclaration->visibility = ast::PredicateDeclaration::Visibility::Visible; } void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector &, Context &) @@ -214,13 +214,12 @@ struct StatementVisitor if (aritySymbol.type() != Clingo::SymbolType::Number) fail(); + context.externalStatementsUsed = true; + const size_t arity = aritySymbol.number(); - if (!context.externalPredicateSignatures) - context.externalPredicateSignatures.emplace(); - - auto predicateSignature = ast::PredicateSignature{std::string(predicate.name), arity}; - context.externalPredicateSignatures->emplace_back(PredicateSignatureMeta{std::move(predicateSignature)}); + auto predicateDeclaration = context.findOrCreatePredicateDeclaration(predicate.name, arity); + predicateDeclaration->isExternal = true; } template diff --git a/include/anthem/output/AST.h b/include/anthem/output/AST.h index ff8c883..3703174 100644 --- a/include/anthem/output/AST.h +++ b/include/anthem/output/AST.h @@ -51,6 +51,7 @@ output::ColorStream &print(output::ColorStream &stream, const In &in, PrintConte output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext, bool omitParentheses = false); output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses = false); output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool omitParentheses = false); +output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &printContext, bool omitParentheses = false); output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext, bool omitParentheses = false); output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext, bool omitParentheses = false); output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false); @@ -236,7 +237,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Interval &i inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool) { - stream << predicate.name; + stream << predicate.declaration->name; if (predicate.arguments.empty()) return stream; @@ -258,6 +259,13 @@ inline output::ColorStream &print(output::ColorStream &stream, const Predicate & //////////////////////////////////////////////////////////////////////////////////////////////////// +inline output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &, bool) +{ + return (stream << predicateDeclaration.name << "/" << predicateDeclaration.arity); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &, bool) { switch (specialInteger.type) diff --git a/src/anthem/ASTCopy.cpp b/src/anthem/ASTCopy.cpp index f67912a..e19113d 100644 --- a/src/anthem/ASTCopy.cpp +++ b/src/anthem/ASTCopy.cpp @@ -133,7 +133,7 @@ Interval prepareCopy(const Interval &other) Predicate prepareCopy(const Predicate &other) { - return Predicate(std::string(other.name), prepareCopy(other.arguments)); + return Predicate(other.declaration, prepareCopy(other.arguments)); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/anthem/ASTUtils.cpp b/src/anthem/ASTUtils.cpp index 3c7aa24..4786beb 100644 --- a/src/anthem/ASTUtils.cpp +++ b/src/anthem/ASTUtils.cpp @@ -193,84 +193,5 @@ struct CollectFreeVariablesVisitor //////////////////////////////////////////////////////////////////////////////////////////////////// -struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor -{ - static void accept(const Predicate &predicate, const Formula &, std::vector &predicateSignatures, Context &context) - { - const auto predicateSignatureMatches = - [&predicate](const auto &predicateSignature) - { - return matches(predicate, predicateSignature); - }; - - if (std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), predicateSignatureMatches) != predicateSignatures.cend()) - return; - - // TODO: avoid copies - auto predicateSignature = PredicateSignature(std::string(predicate.name), predicate.arity()); - - // Ignore predicates that are declared #external - if (context.externalPredicateSignatures) - { - const auto matchesPredicateSignature = - [&](const auto &otherPredicateSignature) - { - return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature); - }; - - auto &externalPredicateSignatures = context.externalPredicateSignatures.value(); - - const auto matchingExternalPredicateSignature = - std::find_if(externalPredicateSignatures.begin(), externalPredicateSignatures.end(), matchesPredicateSignature); - - if (matchingExternalPredicateSignature != externalPredicateSignatures.end()) - { - matchingExternalPredicateSignature->used = true; - return; - } - } - - predicateSignatures.emplace_back(std::move(predicateSignature)); - } - - // Ignore all other types of expressions - template - static void accept(const T &, const Formula &, std::vector &, const Context &) - { - } -}; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -bool matches(const Predicate &lhs, const Predicate &rhs) -{ - return (lhs.name == rhs.name && lhs.arity() == rhs.arity()); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -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 collectPredicateSignatures(const Formula &formula, std::vector &predicateSignatures, Context &context) -{ - auto &formulaMutable = const_cast(formula); - formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures, context); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - } } diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp index 93280bc..a4e76fc 100644 --- a/src/anthem/Completion.cpp +++ b/src/anthem/Completion.cpp @@ -35,7 +35,7 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c auto &otherPredicate = implies.consequent.get(); - if (!ast::matches(predicate, otherPredicate)) + if (predicate.declaration != otherPredicate.declaration) continue; assert(otherPredicate.arguments.size() == parameters.size()); @@ -100,22 +100,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo //////////////////////////////////////////////////////////////////////////////////////////////////// -ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector &scopedFormulas) +ast::Formula completePredicate(ast::PredicateDeclaration &predicateDeclaration, std::vector &scopedFormulas) { // Create new set of parameters for the completed definition for the predicate ast::VariableDeclarationPointers parameters; - parameters.reserve(predicateSignature.arity); + parameters.reserve(predicateDeclaration.arity); std::vector arguments; - arguments.reserve(predicateSignature.arity); + arguments.reserve(predicateDeclaration.arity); - for (size_t i = 0; i < predicateSignature.arity; i++) + for (size_t i = 0; i < predicateDeclaration.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(predicateSignature.name), std::move(arguments)); + ast::Predicate predicateCopy(&predicateDeclaration, std::move(arguments)); auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas); auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction)); @@ -161,28 +161,27 @@ std::vector complete(std::vector &&scopedFormu throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently"); } - std::vector predicateSignatures; - - // Get a list of all predicates - for (const auto &scopedFormula : scopedFormulas) - ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures, context); - - std::sort(predicateSignatures.begin(), predicateSignatures.end(), + std::sort(context.predicateDeclarations.begin(), context.predicateDeclarations.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 lhs.arity < rhs.arity; + return lhs->arity < rhs->arity; }); std::vector completedFormulas; // Complete predicates - for (const auto &predicateSignature : predicateSignatures) - completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas)); + for (auto &predicateDeclaration : context.predicateDeclarations) + { + if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal) + continue; + + completedFormulas.emplace_back(completePredicate(*predicateDeclaration, scopedFormulas)); + } // Complete integrity constraints for (auto &scopedFormula : scopedFormulas) @@ -202,7 +201,7 @@ std::vector complete(std::vector &&scopedFormu } // Eliminate all predicates that should not be visible in the output - eliminateHiddenPredicates(predicateSignatures, completedFormulas, context); + eliminateHiddenPredicates(completedFormulas, context); return completedFormulas; } diff --git a/src/anthem/HiddenPredicateElimination.cpp b/src/anthem/HiddenPredicateElimination.cpp index 014deb1..85ec768 100644 --- a/src/anthem/HiddenPredicateElimination.cpp +++ b/src/anthem/HiddenPredicateElimination.cpp @@ -78,7 +78,7 @@ struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor { - static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateSignature &predicateSignature, bool &hasCircularDependency) + static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateDeclaration &predicateDeclaration, bool &hasCircularDependency) { - if (ast::matches(predicate, predicateSignature)) + if (predicate.declaration == &predicateDeclaration) hasCircularDependency = true; } // Ignore all other types of expressions template - static void accept(T &, ast::Formula &, const ast::PredicateSignature &, bool &) + static void accept(T &, ast::Formula &, const ast::PredicateDeclaration &, bool &) { } }; @@ -125,12 +125,12 @@ struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor q(X1, ..., Xn)” -PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Predicate &predicate) +PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Predicate &predicate) { // Declare variable used, only used in debug mode - (void)(predicateSignature); + (void)(predicateDeclaration); - assert(ast::matches(predicate, predicateSignature)); + assert(predicate.declaration == &predicateDeclaration); // Replace with “#true” return {predicate, ast::Formula::make(true)}; @@ -139,13 +139,13 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig //////////////////////////////////////////////////////////////////////////////////////////////////// // Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> not q(X1, ..., Xn)” -PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Not ¬_) +PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Not ¬_) { // Declare variable used, only used in debug mode - (void)(predicateSignature); + (void)(predicateDeclaration); assert(not_.argument.is()); - assert(ast::matches(not_.argument.get(), predicateSignature)); + assert(not_.argument.get().declaration == &predicateDeclaration); // Replace with “#false” return {not_.argument.get(), ast::Formula::make(false)}; @@ -154,13 +154,13 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig //////////////////////////////////////////////////////////////////////////////////////////////////// // Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)” -PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Biconditional &biconditional) +PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Biconditional &biconditional) { // Declare variable used, only used in debug mode - (void)(predicateSignature); + (void)(predicateDeclaration); assert(biconditional.left.is()); - assert(ast::matches(biconditional.left.get(), predicateSignature)); + assert(biconditional.left.get().declaration == &predicateDeclaration); // TODO: avoid copy return {biconditional.left.get(), ast::prepareCopy(biconditional.right)}; @@ -169,77 +169,65 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig //////////////////////////////////////////////////////////////////////////////////////////////////// // Finds a replacement for a predicate that should be hidden -PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Formula &completedPredicateDefinition) +PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Formula &completedPredicateDefinition) { // TODO: refactor if (completedPredicateDefinition.is()) - return findReplacement(predicateSignature, completedPredicateDefinition.get().argument); + return findReplacement(predicateDeclaration, completedPredicateDefinition.get().argument); else if (completedPredicateDefinition.is()) - return findReplacement(predicateSignature, completedPredicateDefinition.get()); + return findReplacement(predicateDeclaration, completedPredicateDefinition.get()); else if (completedPredicateDefinition.is()) - return findReplacement(predicateSignature, completedPredicateDefinition.get()); + return findReplacement(predicateDeclaration, completedPredicateDefinition.get()); else if (completedPredicateDefinition.is()) - return findReplacement(predicateSignature, completedPredicateDefinition.get()); + return findReplacement(predicateDeclaration, completedPredicateDefinition.get()); - throw CompletionException("unsupported completed definition for predicate “" + predicateSignature.name + "/" + std::to_string(predicateSignature.arity) + "” for hiding predicates"); + throw CompletionException("unsupported completed definition for predicate “" + predicateDeclaration.name + "/" + std::to_string(predicateDeclaration.arity) + "” for hiding predicates"); } //////////////////////////////////////////////////////////////////////////////////////////////////// -void eliminateHiddenPredicates(const std::vector &predicateSignatures, std::vector &completedFormulas, Context &context) +void eliminateHiddenPredicates(std::vector &completedFormulas, Context &context) { - if (!context.visiblePredicateSignatures) + if (context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible) { context.logger.log(output::Priority::Debug) << "no predicates to be eliminated"; return; } - auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value(); + assert(context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Hidden); + + // TODO: get rid of index-wise matching of completed formulas and predicate declarations + size_t i = -1; // Replace all occurrences of hidden predicates - for (size_t i = 0; i < predicateSignatures.size(); i++) + for (auto &predicateDeclaration : context.predicateDeclarations) { - auto &predicateSignature = predicateSignatures[i]; + // Check that the predicate is used and not declared #external + if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal) + continue; - const auto matchesPredicateSignature = - [&](const auto &otherPredicateSignature) - { - return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature); - }; + i++; - const auto matchingVisiblePredicateSignature = - std::find_if(visiblePredicateSignatures.begin(), visiblePredicateSignatures.end(), matchesPredicateSignature); + const auto isPredicateVisible = + (predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Visible) + || (predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Default + && context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible); // If the predicate ought to be visible, don’t eliminate it - if (matchingVisiblePredicateSignature != visiblePredicateSignatures.end()) - { - matchingVisiblePredicateSignature->used = true; + if (isPredicateVisible) continue; - } - // Check that the predicate is not declared #external - if (context.externalPredicateSignatures) - { - const auto &externalPredicateSignatures = context.externalPredicateSignatures.value(); - - const auto matchingExternalPredicateSignature = - std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature); - - if (matchingExternalPredicateSignature != externalPredicateSignatures.cend()) - continue; - } - - context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "”"; + context.logger.log(output::Priority::Debug) << "eliminating “" << predicateDeclaration->name << "/" << predicateDeclaration->arity << "”"; const auto &completedPredicateDefinition = completedFormulas[i]; - auto replacement = findReplacement(predicateSignature, completedPredicateDefinition); + auto replacement = findReplacement(*predicateDeclaration, completedPredicateDefinition); bool hasCircularDependency = false; - replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, predicateSignature, hasCircularDependency); + replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, *predicateDeclaration, hasCircularDependency); if (hasCircularDependency) { - context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateSignature.name << "/" << predicateSignature.arity << "” due to circular dependency"; + context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateDeclaration->name << "/" << predicateDeclaration->arity << "” due to circular dependency"; continue; } diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index cf521f1..4772d97 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -67,10 +67,10 @@ void translate(const char *fileName, std::istream &stream, Context &context) for (auto &scopedFormula : scopedFormulas) simplify(scopedFormula.formula); - if (context.visiblePredicateSignatures) + if (context.showStatementsUsed) context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled"; - if (context.externalPredicateSignatures) + if (context.externalStatementsUsed) context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled"; for (const auto &scopedFormula : scopedFormulas) @@ -85,25 +85,29 @@ void translate(const char *fileName, std::istream &stream, Context &context) // Perform completion auto completedFormulas = complete(std::move(scopedFormulas), context); - // Check for #show statements with undeclared predicates - if (context.visiblePredicateSignatures) - for (const auto &predicateSignature : context.visiblePredicateSignatures.value()) - if (!predicateSignature.used) - context.logger.log(output::Priority::Warning) - << "#show declaration of “" - << predicateSignature.predicateSignature.name - << "/" << predicateSignature.predicateSignature.arity - << "” does not match any eligible predicate"; + for (const auto &predicateDeclaration : context.predicateDeclarations) + { + if (predicateDeclaration->isUsed) + continue; - // Check for #external statements with undeclared predicates - if (context.externalPredicateSignatures) - for (const auto &predicateSignature : context.externalPredicateSignatures.value()) - if (!predicateSignature.used) - context.logger.log(output::Priority::Warning) - << "#external declaration of “" - << predicateSignature.predicateSignature.name - << "/" << predicateSignature.predicateSignature.arity - << "” does not match any eligible predicate"; + // Check for #show statements with undeclared predicates + if (predicateDeclaration->visibility != ast::PredicateDeclaration::Visibility::Default) + context.logger.log(output::Priority::Warning) + << "#show declaration of “" + << predicateDeclaration->name + << "/" + << predicateDeclaration->arity + << "” does not match any declared predicate"; + + // Check for #external statements with undeclared predicates + if (predicateDeclaration->isExternal && !predicateDeclaration->isUsed) + context.logger.log(output::Priority::Warning) + << "#external declaration of “" + << predicateDeclaration->name + << "/" + << predicateDeclaration->arity + << "” does not match any declared predicate"; + } // Simplify output if specified if (context.performSimplification)