From fc538eb7fcd4e0baace57c250f9a7ef9f811c050 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 16 Mar 2017 15:45:55 +0100 Subject: [PATCH] Started implementing output simplifications. --- app/main.cpp | 1 + include/anthem/AST.h | 48 ++++++------ include/anthem/Context.h | 2 + include/anthem/Simplification.h | 21 ++++++ src/anthem/Simplification.cpp | 127 ++++++++++++++++++++++++++++++++ src/anthem/Translation.cpp | 12 ++- 6 files changed, 185 insertions(+), 26 deletions(-) create mode 100644 include/anthem/Simplification.h create mode 100644 src/anthem/Simplification.cpp diff --git a/app/main.cpp b/app/main.cpp index 7022f1a..ffb912d 100644 --- a/app/main.cpp +++ b/app/main.cpp @@ -16,6 +16,7 @@ int main(int argc, char **argv) ("help,h", "Display this help message") ("version,v", "Display version information") ("input,i", po::value>(), "Input files") + ("simplify,s", po::bool_switch(&context.simplify), "Simplify the output") ("color,c", po::value()->default_value("auto"), "Colorize output (always, never, auto)") ("log-priority,p", po::value()->default_value("warning"), "Log messages starting from this priority (debug, info, warning, error)"); diff --git a/include/anthem/AST.h b/include/anthem/AST.h index 830e71e..85976b1 100644 --- a/include/anthem/AST.h +++ b/include/anthem/AST.h @@ -397,168 +397,168 @@ const auto deepCopyVariantVector = //////////////////////////////////////////////////////////////////////////////////////////////////// -BinaryOperation deepCopy(const BinaryOperation &other) +inline BinaryOperation deepCopy(const BinaryOperation &other) { return BinaryOperation(other.operator_, deepCopy(other.left), deepCopy(other.right)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Boolean deepCopy(const Boolean &other) +inline Boolean deepCopy(const Boolean &other) { return Boolean(other.value); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Comparison deepCopy(const Comparison &other) +inline Comparison deepCopy(const Comparison &other) { return Comparison(other.operator_, deepCopy(other.left), deepCopy(other.right)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Constant deepCopy(const Constant &other) +inline Constant deepCopy(const Constant &other) { return Constant(std::string(other.name)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Function deepCopy(const Function &other) +inline Function deepCopy(const Function &other) { return Function(std::string(other.name), deepCopy(other.arguments)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Integer deepCopy(const Integer &other) +inline Integer deepCopy(const Integer &other) { return Integer(other.value); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Interval deepCopy(const Interval &other) +inline Interval deepCopy(const Interval &other) { return Interval(deepCopy(other.from), deepCopy(other.to)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Predicate deepCopy(const Predicate &other) +inline Predicate deepCopy(const Predicate &other) { return Predicate(std::string(other.name), deepCopy(other.arguments)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -SpecialInteger deepCopy(const SpecialInteger &other) +inline SpecialInteger deepCopy(const SpecialInteger &other) { return SpecialInteger(other.type); } //////////////////////////////////////////////////////////////////////////////////////////////////// -String deepCopy(const String &other) +inline String deepCopy(const String &other) { return String(std::string(other.text)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Variable deepCopy(const Variable &other) +inline Variable deepCopy(const Variable &other) { return Variable(std::string(other.name), other.type); } //////////////////////////////////////////////////////////////////////////////////////////////////// -std::vector deepCopy(const std::vector &other) +inline std::vector deepCopy(const std::vector &other) { return deepCopyUniquePtrVector(other); } //////////////////////////////////////////////////////////////////////////////////////////////////// -And deepCopy(const And &other) +inline And deepCopy(const And &other) { return And(deepCopy(other.arguments)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Biconditional deepCopy(const Biconditional &other) +inline Biconditional deepCopy(const Biconditional &other) { return Biconditional(deepCopy(other.left), deepCopy(other.right)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Exists deepCopy(const Exists &other) +inline Exists deepCopy(const Exists &other) { return Exists(deepCopy(other.variables), deepCopy(other.argument)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -ForAll deepCopy(const ForAll &other) +inline ForAll deepCopy(const ForAll &other) { return ForAll(deepCopy(other.variables), deepCopy(other.argument)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -In deepCopy(const In &other) +inline In deepCopy(const In &other) { return In(deepCopy(other.element), deepCopy(other.set)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Implies deepCopy(const Implies &other) +inline Implies deepCopy(const Implies &other) { return Implies(deepCopy(other.antecedent), deepCopy(other.consequent)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Not deepCopy(const Not &other) +inline Not deepCopy(const Not &other) { return Not(deepCopy(other.argument)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Or deepCopy(const Or &other) +inline Or deepCopy(const Or &other) { return Or(deepCopy(other.arguments)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Formula deepCopy(const Formula &formula) +inline Formula deepCopy(const Formula &formula) { return deepCopyVariant(formula); } //////////////////////////////////////////////////////////////////////////////////////////////////// -std::vector deepCopy(const std::vector &formulas) +inline std::vector deepCopy(const std::vector &formulas) { return deepCopyVariantVector(formulas); } //////////////////////////////////////////////////////////////////////////////////////////////////// -Term deepCopy(const Term &term) +inline Term deepCopy(const Term &term) { return deepCopyVariant(term); } //////////////////////////////////////////////////////////////////////////////////////////////////// -std::vector deepCopy(const std::vector &terms) +inline std::vector deepCopy(const std::vector &terms) { return deepCopyVariantVector(terms); } diff --git a/include/anthem/Context.h b/include/anthem/Context.h index 0149a20..702b1e0 100644 --- a/include/anthem/Context.h +++ b/include/anthem/Context.h @@ -30,6 +30,8 @@ struct Context bool isChoiceRule = false; size_t numberOfHeadLiterals = 0; size_t auxiliaryBodyLiteralID = 1; + + bool simplify = false; }; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/Simplification.h b/include/anthem/Simplification.h new file mode 100644 index 0000000..717802f --- /dev/null +++ b/include/anthem/Simplification.h @@ -0,0 +1,21 @@ +#ifndef __ANTHEM__SIMPLIFICATION_H +#define __ANTHEM__SIMPLIFICATION_H + +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Simplification +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ast::Formula simplify(ast::Formula &&formula); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} + +#endif diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp new file mode 100644 index 0000000..90abea3 --- /dev/null +++ b/src/anthem/Simplification.cpp @@ -0,0 +1,127 @@ +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Simplification +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +bool isPrimitiveTerm(const ast::Term &term) +{ + const auto binaryOperationIsNotPrimitiveTerm = + [](const ast::BinaryOperationPointer &) + { + return false; + }; + + const auto intervalIsNotPrimitiveTerm = + [](const ast::IntervalPointer &) + { + return false; + }; + + const auto defaultIsPrimitiveTerm = + [](const auto &) + { + return true; + }; + + return term.match(binaryOperationIsNotPrimitiveTerm, intervalIsNotPrimitiveTerm, defaultIsPrimitiveTerm); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ast::Formula simplifyFormula(ast::Formula &&formula) +{ + const auto simplifyAnd = + [&](ast::AndPointer &and_) -> ast::Formula + { + for (auto &argument : and_->arguments) + argument = simplifyFormula(std::move(argument)); + + return std::move(and_); + }; + + const auto simplifyBiconditional = + [&](ast::BiconditionalPointer &biconditional) -> ast::Formula + { + biconditional->left = simplifyFormula(std::move(biconditional->left)); + biconditional->right = simplifyFormula(std::move(biconditional->right)); + + return std::move(biconditional); + }; + + const auto simplifyExists = + [&](ast::ExistsPointer &exists) -> ast::Formula + { + exists->argument = simplifyFormula(std::move(exists->argument)); + + return std::move(exists); + }; + + const auto simplifyForAll = + [&](ast::ForAllPointer &forAll) -> ast::Formula + { + forAll->argument = simplifyFormula(std::move(forAll->argument)); + + return std::move(forAll); + }; + + const auto simplifyImplies = + [&](ast::ImpliesPointer &implies) -> ast::Formula + { + implies->antecedent = simplifyFormula(std::move(implies->antecedent)); + implies->consequent = simplifyFormula(std::move(implies->consequent)); + + return std::move(implies); + }; + + const auto simplifyIn = + [](ast::InPointer &in) -> ast::Formula + { + if (!isPrimitiveTerm(in->element) || !isPrimitiveTerm(in->set)) + return std::move(in); + + // Simplify formulas of type “A in B” to “A = B” if A and B are primitive + return std::make_unique(ast::Comparison::Operator::Equal, std::move(in->element), std::move(in->set)); + }; + + const auto simplifyNot = + [&](ast::NotPointer ¬_) -> ast::Formula + { + not_->argument = simplifyFormula(std::move(not_->argument)); + + return std::move(not_); + }; + + const auto simplifyOr = + [&](ast::OrPointer &or_) -> ast::Formula + { + for (auto &argument : or_->arguments) + argument = simplifyFormula(std::move(argument)); + + return std::move(or_); + }; + + const auto defaultDoNothing = + [&](auto &x) -> ast::Formula + { + return std::move(x); + }; + + return formula.match(simplifyAnd, simplifyBiconditional, simplifyExists, simplifyForAll, simplifyImplies, simplifyIn, simplifyNot, simplifyOr, defaultDoNothing); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ast::Formula simplify(ast::Formula &&formula) +{ + return simplifyFormula(std::move(formula)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index 300470d..edab9c4 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -7,6 +7,7 @@ #include #include +#include #include #include @@ -41,12 +42,19 @@ void translate(const char *fileName, std::istream &stream, Context &context) const auto translateStatement = [&context](const Clingo::AST::Statement &statement) { - const auto formula = statement.data.accept(StatementVisitor(), statement, context); + auto formula = statement.data.accept(StatementVisitor(), statement, context); if (!formula) return; - context.logger.outputStream() << formula.value() << std::endl; + if (!context.simplify) + { + context.logger.outputStream() << formula.value() << std::endl; + return; + } + + auto simplifiedFormula = simplify(std::move(formula.value())); + context.logger.outputStream() << simplifiedFormula << std::endl; }; const auto logger =