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)