From a716da4af1df19815eef4dd9172625e7b04221c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sat, 8 Apr 2017 16:21:24 +0200 Subject: [PATCH] Finished implementing completion (unit tests to follow). --- include/anthem/ASTUtils.h | 41 ++++++++ src/anthem/ASTUtils.cpp | 190 +++++++++++++++++++++++++++++++++++++ src/anthem/Completion.cpp | 39 +++++--- src/anthem/Translation.cpp | 13 +-- 4 files changed, 261 insertions(+), 22 deletions(-) create mode 100644 include/anthem/ASTUtils.h create mode 100644 src/anthem/ASTUtils.cpp diff --git a/include/anthem/ASTUtils.h b/include/anthem/ASTUtils.h new file mode 100644 index 0000000..66bae55 --- /dev/null +++ b/include/anthem/ASTUtils.h @@ -0,0 +1,41 @@ +#ifndef __ANTHEM__AST_UTILS_H +#define __ANTHEM__AST_UTILS_H + +#include + +namespace anthem +{ +namespace ast +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// AST Utils +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +class VariableStack +{ + public: + using Layer = const std::vector *; + + public: + void push(Layer layer); + void pop(); + + bool contains(const ast::Variable &variable) const; + + private: + std::vector m_layers; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +std::vector collectFreeVariables(const ast::Formula &formula, ast::VariableStack &variableStack); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} + +#endif diff --git a/src/anthem/ASTUtils.cpp b/src/anthem/ASTUtils.cpp new file mode 100644 index 0000000..b4e8b84 --- /dev/null +++ b/src/anthem/ASTUtils.cpp @@ -0,0 +1,190 @@ +#include + +#include + +namespace anthem +{ +namespace ast +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// AST Utils +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void VariableStack::push(Layer layer) +{ + m_layers.push_back(layer); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void VariableStack::pop() +{ + m_layers.pop_back(); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +bool VariableStack::contains(const ast::Variable &variable) const +{ + const auto variableMatches = + [&variable](const auto &otherVariable) + { + return variable.name == otherVariable.name; + }; + + const auto layerContainsVariable = + [&variable, &variableMatches](const auto &layer) + { + return (std::find_if(layer->cbegin(), layer->cend(), variableMatches) != layer->cend()); + }; + + return (std::find_if(m_layers.cbegin(), m_layers.cend(), layerContainsVariable) != m_layers.cend()); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct CollectFreeVariablesVisitor +{ + //////////////////////////////////////////////////////////////////////////////////////////////// + // Formulas + //////////////////////////////////////////////////////////////////////////////////////////////// + + void visit(const ast::And &and_, VariableStack &variableStack, std::vector &freeVariables) + { + for (const auto &argument : and_.arguments) + argument.accept(*this, variableStack, freeVariables); + } + + void visit(const ast::Biconditional &biconditional, VariableStack &variableStack, std::vector &freeVariables) + { + biconditional.left.accept(*this, variableStack, freeVariables); + biconditional.right.accept(*this, variableStack, freeVariables); + } + + void visit(const ast::Boolean &, VariableStack &, std::vector &) + { + } + + void visit(const ast::Comparison &comparison, VariableStack &variableStack, std::vector &freeVariables) + { + comparison.left.accept(*this, variableStack, freeVariables); + comparison.right.accept(*this, variableStack, freeVariables); + } + + void visit(const ast::Exists &exists, VariableStack &variableStack, std::vector &freeVariables) + { + variableStack.push(&exists.variables); + exists.argument.accept(*this, variableStack, freeVariables); + variableStack.pop(); + } + + void visit(const ast::ForAll &forAll, VariableStack &variableStack, std::vector &freeVariables) + { + variableStack.push(&forAll.variables); + forAll.argument.accept(*this, variableStack, freeVariables); + variableStack.pop(); + } + + void visit(const ast::Implies &implies, VariableStack &variableStack, std::vector &freeVariables) + { + implies.antecedent.accept(*this, variableStack, freeVariables); + implies.consequent.accept(*this, variableStack, freeVariables); + } + + void visit(const ast::In &in, VariableStack &variableStack, std::vector &freeVariables) + { + in.element.accept(*this, variableStack, freeVariables); + in.set.accept(*this, variableStack, freeVariables); + } + + void visit(const ast::Not ¬_, VariableStack &variableStack, std::vector &freeVariables) + { + not_.argument.accept(*this, variableStack, freeVariables); + } + + void visit(const ast::Or &or_, VariableStack &variableStack, std::vector &freeVariables) + { + for (const auto &argument : or_.arguments) + argument.accept(*this, variableStack, freeVariables); + } + + void visit(const ast::Predicate &predicate, VariableStack &variableStack, std::vector &freeVariables) + { + for (const auto &argument : predicate.arguments) + argument.accept(*this, variableStack, freeVariables); + } + + //////////////////////////////////////////////////////////////////////////////////////////////// + // Terms + //////////////////////////////////////////////////////////////////////////////////////////////// + + void visit(const ast::BinaryOperation &binaryOperation, VariableStack &variableStack, std::vector &freeVariables) + { + binaryOperation.left.accept(*this, variableStack, freeVariables); + binaryOperation.right.accept(*this, variableStack, freeVariables); + } + + void visit(const ast::Constant &, VariableStack &, std::vector &) + { + } + + void visit(const ast::Function &function, VariableStack &variableStack, std::vector &freeVariables) + { + for (const auto &argument : function.arguments) + argument.accept(*this, variableStack, freeVariables); + } + + void visit(const ast::Integer &, VariableStack &, std::vector &) + { + } + + void visit(const ast::Interval &interval, VariableStack &variableStack, std::vector &freeVariables) + { + interval.from.accept(*this, variableStack, freeVariables); + interval.to.accept(*this, variableStack, freeVariables); + } + + void visit(const ast::SpecialInteger &, VariableStack &, std::vector &) + { + } + + void visit(const ast::String &, VariableStack &, std::vector &) + { + } + + void visit(const ast::Variable &variable, VariableStack &variableStack, std::vector &freeVariables) + { + if (variableStack.contains(variable)) + return; + + const auto &variableMatches = + [&variable](auto &otherVariable) + { + return variable.name == otherVariable.name; + }; + + if (std::find_if(freeVariables.cbegin(), freeVariables.cend(), variableMatches) != freeVariables.cend()) + return; + + freeVariables.emplace_back(ast::deepCopy(variable)); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +std::vector collectFreeVariables(const ast::Formula &formula, ast::VariableStack &variableStack) +{ + std::vector freeVariables; + + formula.accept(CollectFreeVariablesVisitor(), variableStack, freeVariables); + + return freeVariables; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp index ffb0ee1..2cb93ed 100644 --- a/src/anthem/Completion.cpp +++ b/src/anthem/Completion.cpp @@ -1,5 +1,6 @@ #include +#include #include namespace anthem @@ -41,6 +42,16 @@ void completePredicate(const ast::Predicate &predicate, std::vector variables; + variables.reserve(predicate.arguments.size()); + + for (const auto &argument : predicate.arguments) + { + assert(argument.is()); + variables.emplace_back(ast::deepCopy(argument.get())); + } + auto or_ = ast::Formula::make(); // Build the conjunction of all formulas with the predicate as consequent @@ -58,11 +69,18 @@ void completePredicate(const ast::Predicate &predicate, std::vector variables = {ast::Variable("dummy", ast::Variable::Type::UserDefined)}; - auto exists = ast::Formula::make(std::move(variables), std::move(implies.antecedent)); + ast::VariableStack variableStack; + variableStack.push(&variables); - or_.get().arguments.emplace_back(exists); + auto variables = ast::collectFreeVariables(implies.antecedent, variableStack); + + if (variables.empty()) + or_.get().arguments.emplace_back(std::move(implies.antecedent)); + else + { + auto exists = ast::Formula::make(std::move(variables), std::move(implies.antecedent)); + or_.get().arguments.emplace_back(std::move(exists)); + } if (i > formulasBegin) formulas.erase(formulas.begin() + i); @@ -70,6 +88,9 @@ void completePredicate(const ast::Predicate &predicate, std::vector().arguments.size() == 1) + or_ = or_.get().arguments.front(); + // Build the biconditional within the completed formula auto biconditional = ast::Formula::make(ast::deepCopy(predicate), std::move(or_)); @@ -79,16 +100,6 @@ void completePredicate(const ast::Predicate &predicate, std::vector variables; - variables.reserve(predicate.arguments.size()); - - for (const auto &argument : predicate.arguments) - { - assert(argument.is()); - variables.emplace_back(ast::deepCopy(argument.get())); - } - auto completedFormula = ast::Formula::make(std::move(variables), std::move(biconditional)); formulas[formulasBegin] = std::move(completedFormula); diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index 7537962..24f8371 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -56,18 +56,15 @@ void translate(const char *fileName, std::istream &stream, Context &context) Clingo::parse_program(fileContent.c_str(), translateStatement, logger); + if (context.simplify) + for (auto &formula : formulas) + simplify(formula); + if (context.complete) complete(formulas); - for (auto i = formulas.begin(); i != formulas.end(); i++) - { - auto &formula = *i; - - if (context.simplify) - simplify(formula); - + for (const auto &formula : formulas) context.logger.outputStream() << formula << std::endl; - } } ////////////////////////////////////////////////////////////////////////////////////////////////////