From 825cd4de39d52edbf3b69c96e9e52979933b5beb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 23 Mar 2017 00:44:10 +0100 Subject: [PATCH] =?UTF-8?q?Refactored=20formula=20simplification=20with=20?= =?UTF-8?q?Clingo=E2=80=99s=20variants.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .gitmodules | 3 - include/anthem/AST.h | 48 ++++- include/anthem/ASTForward.h | 47 ++--- include/anthem/Body.h | 38 ++-- include/anthem/Head.h | 12 +- include/anthem/Simplification.h | 2 +- include/anthem/StatementVisitor.h | 22 +-- include/anthem/Term.h | 24 +-- include/anthem/output/AST.h | 68 +++---- lib/variant | 1 - src/anthem/Simplification.cpp | 288 +++++++++++++++--------------- src/anthem/Translation.cpp | 4 +- 12 files changed, 296 insertions(+), 261 deletions(-) delete mode 160000 lib/variant diff --git a/.gitmodules b/.gitmodules index e74e0ac..c09da0b 100644 --- a/.gitmodules +++ b/.gitmodules @@ -4,6 +4,3 @@ [submodule "lib/catch"] path = lib/catch url = https://github.com/philsquared/Catch -[submodule "lib/variant"] - path = lib/variant - url = https://github.com/mapbox/variant diff --git a/include/anthem/AST.h b/include/anthem/AST.h index 85976b1..79c3505 100644 --- a/include/anthem/AST.h +++ b/include/anthem/AST.h @@ -253,13 +253,13 @@ struct Biconditional struct Exists { - Exists(std::vector &&variables, Formula &&argument) + Exists(std::vector &&variables, Formula &&argument) : variables{std::move(variables)}, argument{std::move(argument)} { } - std::vector variables; + std::vector variables; Formula argument; }; @@ -267,13 +267,13 @@ struct Exists struct ForAll { - ForAll(std::vector &&variables, Formula &&argument) + ForAll(std::vector &&variables, Formula &&argument) : variables{std::move(variables)}, argument{std::move(argument)} { } - std::vector variables; + std::vector variables; Formula argument; }; @@ -332,7 +332,7 @@ Predicate deepCopy(const Predicate &other); SpecialInteger deepCopy(const SpecialInteger &other); String deepCopy(const String &other); Variable deepCopy(const Variable &other); -std::vector deepCopy(const std::vector &other); +std::vector deepCopy(const std::vector &other); And deepCopy(const And &other); Biconditional deepCopy(const Biconditional &other); Exists deepCopy(const Exists &other); @@ -347,7 +347,7 @@ Term deepCopy(const Term &term); std::vector deepCopy(const std::vector &terms); //////////////////////////////////////////////////////////////////////////////////////////////////// - +/* const auto deepCopyUniquePtr = [](const auto &uniquePtr) -> typename std::decay::type { @@ -370,13 +370,27 @@ const auto deepCopyUniquePtrVector = return result; }; +*/ +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +struct VariantDeepCopyVisitor +{ + template + Variant visit(const T &x) + { + return deepCopy(x); + } +}; //////////////////////////////////////////////////////////////////////////////////////////////////// const auto deepCopyVariant = [](const auto &variant) -> typename std::decay::type { - return variant.match([](const auto &x) -> typename std::decay::type {return deepCopyUniquePtr(x);}); + using VariantType = typename std::decay::type; + + return variant.accept(VariantDeepCopyVisitor()); }; //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -397,6 +411,22 @@ const auto deepCopyVariantVector = //////////////////////////////////////////////////////////////////////////////////////////////////// +const auto deepCopyVector = + [](const auto &vector) -> typename std::decay::type + { + using Type = typename std::decay::type::value_type; + + std::vector result; + result.reserve(vector.size()); + + for (const auto &element : vector) + result.emplace_back(deepCopy(element)); + + return result; + }; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + inline BinaryOperation deepCopy(const BinaryOperation &other) { return BinaryOperation(other.operator_, deepCopy(other.left), deepCopy(other.right)); @@ -474,9 +504,9 @@ inline Variable deepCopy(const Variable &other) //////////////////////////////////////////////////////////////////////////////////////////////////// -inline std::vector deepCopy(const std::vector &other) +inline std::vector deepCopy(const std::vector &other) { - return deepCopyUniquePtrVector(other); + return deepCopyVector(other); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/ASTForward.h b/include/anthem/ASTForward.h index 37eee39..4440448 100644 --- a/include/anthem/ASTForward.h +++ b/include/anthem/ASTForward.h @@ -3,9 +3,10 @@ #include #include -#include #include +#include + namespace anthem { @@ -64,34 +65,34 @@ using VariablePointer = std::unique_ptr; // Variants //////////////////////////////////////////////////////////////////////////////////////////////////// -using FormulaT = mapbox::util::variant< - AndPointer, - BiconditionalPointer, - BooleanPointer, - ComparisonPointer, - ExistsPointer, - ForAllPointer, - ImpliesPointer, - InPointer, - NotPointer, - OrPointer, - PredicatePointer>; +using FormulaT = Clingo::Variant< + And, + Biconditional, + Boolean, + Comparison, + Exists, + ForAll, + Implies, + In, + Not, + Or, + Predicate>; class Formula : public FormulaT { using FormulaT::FormulaT; }; -using TermT = mapbox::util::variant< - BinaryOperationPointer, - BooleanPointer, - ConstantPointer, - FunctionPointer, - IntegerPointer, - IntervalPointer, - SpecialIntegerPointer, - StringPointer, - VariablePointer>; +using TermT = Clingo::Variant< + BinaryOperation, + Boolean, + Constant, + Function, + Integer, + Interval, + SpecialInteger, + String, + Variable>; class Term : public TermT { diff --git a/include/anthem/Body.h b/include/anthem/Body.h index 550b700..5ac0f8b 100644 --- a/include/anthem/Body.h +++ b/include/anthem/Body.h @@ -40,11 +40,11 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp //////////////////////////////////////////////////////////////////////////////////////////////////// -ast::VariablePointer makeAuxiliaryBodyVariable(const int i) +ast::Variable makeAuxiliaryBodyVariable(const int i) { auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(i); - return std::make_unique(std::move(variableName), ast::Variable::Type::Reserved); + return ast::Variable(std::move(variableName), ast::Variable::Type::Reserved); } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -88,36 +88,36 @@ struct BodyTermTranslateVisitor throwErrorAtLocation(literal.location, "double-negated literals currently unsupported", context); if (function.arguments.empty()) - return std::make_unique(std::string(function.name)); + return ast::Formula::make(std::string(function.name)); - std::vector variables; + std::vector variables; variables.reserve(function.arguments.size()); for (size_t i = 0; i < function.arguments.size(); i++) variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i)); - auto conjunction = std::make_unique(); + ast::And conjunction; for (size_t i = 0; i < function.arguments.size(); i++) { const auto &argument = function.arguments[i]; - conjunction->arguments.emplace_back(std::make_unique(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i), translate(argument, context))); + conjunction.arguments.emplace_back(ast::Formula::make(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i), translate(argument, context))); } - auto predicate = std::make_unique(std::string(function.name)); - predicate->arguments.reserve(function.arguments.size()); + ast::Predicate predicate(std::string(function.name)); + predicate.arguments.reserve(function.arguments.size()); for (size_t i = 0; i < function.arguments.size(); i++) - predicate->arguments.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i)); + predicate.arguments.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i)); if (literal.sign == Clingo::AST::Sign::None) - conjunction->arguments.emplace_back(std::move(predicate)); + conjunction.arguments.emplace_back(std::move(predicate)); else - conjunction->arguments.emplace_back(std::make_unique(std::move(predicate))); + conjunction.arguments.emplace_back(ast::Formula::make(std::move(predicate))); context.auxiliaryBodyLiteralID += function.arguments.size(); - return std::make_unique(std::move(variables), std::move(conjunction)); + return ast::Formula::make(std::move(variables), std::move(conjunction)); } std::experimental::optional visit(const Clingo::AST::Pool &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) @@ -150,20 +150,20 @@ struct BodyLiteralTranslateVisitor const auto operator_ = translate(comparison.comparison); - std::vector variables; + std::vector variables; variables.reserve(2); variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID)); variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1)); - auto conjunction = std::make_unique(); - conjunction->arguments.reserve(3); - conjunction->arguments.emplace_back(std::make_unique(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID), translate(comparison.left, context))); - conjunction->arguments.emplace_back(std::make_unique(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1), translate(comparison.right, context))); - conjunction->arguments.emplace_back(std::make_unique(operator_, makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID), makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1))); + ast::And conjunction; + conjunction.arguments.reserve(3); + conjunction.arguments.emplace_back(ast::Formula::make(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID), translate(comparison.left, context))); + conjunction.arguments.emplace_back(ast::Formula::make(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1), translate(comparison.right, context))); + conjunction.arguments.emplace_back(ast::Formula::make(operator_, makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID), makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1))); context.auxiliaryBodyLiteralID += 2; - return std::make_unique(std::move(variables), std::move(conjunction)); + return ast::Formula::make(std::move(variables), std::move(conjunction)); } std::experimental::optional visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context) diff --git a/include/anthem/Head.h b/include/anthem/Head.h index 95a2150..4fa76f2 100644 --- a/include/anthem/Head.h +++ b/include/anthem/Head.h @@ -188,10 +188,10 @@ struct FunctionTermTranslateVisitor assert(matchingTerm != context.headTerms.cend()); auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(matchingTerm - context.headTerms.cbegin() + 1); - arguments.emplace_back(std::make_unique(std::move(variableName), ast::Variable::Type::Reserved)); + arguments.emplace_back(ast::Variable(std::move(variableName), ast::Variable::Type::Reserved)); } - return std::make_unique(function.name, std::move(arguments)); + return ast::Formula::make(function.name, std::move(arguments)); } std::experimental::optional visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &context) @@ -207,7 +207,7 @@ struct LiteralTranslateVisitor { std::experimental::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, Context &) { - return std::make_unique(boolean.value); + return ast::Formula::make(boolean.value); } std::experimental::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, Context &context) @@ -245,7 +245,7 @@ struct HeadLiteralTranslateToConsequentVisitor if (!translatedLiteral) return std::experimental::nullopt; - return std::make_unique(std::move(translatedLiteral.value())); + return ast::Formula::make(std::move(translatedLiteral.value())); } std::experimental::optional visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, Context &context) @@ -266,7 +266,7 @@ struct HeadLiteralTranslateToConsequentVisitor arguments.emplace_back(std::move(argument.value())); } - return std::make_unique(std::move(arguments)); + return ast::Formula::make(std::move(arguments)); } std::experimental::optional visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, Context &context) @@ -299,7 +299,7 @@ struct HeadLiteralTranslateToConsequentVisitor arguments.emplace_back(std::move(argument.value())); } - return std::make_unique(std::move(arguments)); + return ast::Formula::make(std::move(arguments)); } std::experimental::optional visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, Context &context) diff --git a/include/anthem/Simplification.h b/include/anthem/Simplification.h index 717802f..162559f 100644 --- a/include/anthem/Simplification.h +++ b/include/anthem/Simplification.h @@ -12,7 +12,7 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -ast::Formula simplify(ast::Formula &&formula); +void simplify(ast::Formula &formula); //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h index 6b3df03..7563be4 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -36,7 +36,7 @@ struct StatementVisitor // Concatenate all head terms rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, context); - auto antecedent = std::make_unique(); + ast::And antecedent; // Compute consequent auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, context); @@ -53,11 +53,11 @@ struct StatementVisitor const auto &headTerm = **i; auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i - context.headTerms.cbegin() + 1); - auto element = std::make_unique(std::move(variableName), ast::Variable::Type::Reserved); + auto element = ast::Variable(std::move(variableName), ast::Variable::Type::Reserved); auto set = translate(headTerm, context); - auto in = std::make_unique(std::move(element), std::move(set)); + auto in = ast::In(std::move(element), std::move(set)); - antecedent->arguments.emplace_back(std::move(in)); + antecedent.arguments.emplace_back(std::move(in)); } // Print translated body literals @@ -73,20 +73,20 @@ struct StatementVisitor if (!argument) throwErrorAtLocation(bodyLiteral.location, "could not translate body literal", context); - antecedent->arguments.emplace_back(std::move(argument.value())); + antecedent.arguments.emplace_back(std::move(argument.value())); } // Handle choice rules if (context.isChoiceRule) - antecedent->arguments.emplace_back(ast::deepCopy(consequent.value())); + antecedent.arguments.emplace_back(ast::deepCopy(consequent.value())); // Use “true” as the consequent in case it is empty - if (antecedent->arguments.empty()) - return std::make_unique(std::make_unique(true), std::move(consequent.value())); - else if (antecedent->arguments.size() == 1) - return std::make_unique(std::move(antecedent->arguments[0]), std::move(consequent.value())); + if (antecedent.arguments.empty()) + return ast::Formula::make(ast::Boolean(true), std::move(consequent.value())); + else if (antecedent.arguments.size() == 1) + return ast::Formula::make(std::move(antecedent.arguments[0]), std::move(consequent.value())); - return std::make_unique(std::move(antecedent), std::move(consequent.value())); + return ast::Formula::make(std::move(antecedent), std::move(consequent.value())); } std::experimental::optional visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context) diff --git a/include/anthem/Term.h b/include/anthem/Term.h index 1782c67..1904240 100644 --- a/include/anthem/Term.h +++ b/include/anthem/Term.h @@ -50,17 +50,19 @@ struct TermTranslateVisitor switch (symbol.type()) { case Clingo::SymbolType::Number: - return std::make_unique(symbol.number()); + return ast::Term::make(symbol.number()); case Clingo::SymbolType::Infimum: - return std::make_unique(ast::SpecialInteger::Type::Infimum); + return ast::Term::make(ast::SpecialInteger::Type::Infimum); case Clingo::SymbolType::Supremum: - return std::make_unique(ast::SpecialInteger::Type::Supremum); + return ast::Term::make(ast::SpecialInteger::Type::Supremum); case Clingo::SymbolType::String: - return std::make_unique(std::string(symbol.string())); + return ast::Term::make(std::string(symbol.string())); case Clingo::SymbolType::Function: { - auto function = std::make_unique(symbol.name()); - function->arguments.reserve(symbol.arguments().size()); + auto function = ast::Term::make(symbol.name()); + // TODO: remove workaround + auto &functionRaw = function.get(); + functionRaw.arguments.reserve(symbol.arguments().size()); for (const auto &argument : symbol.arguments()) { @@ -69,7 +71,7 @@ struct TermTranslateVisitor if (!translatedArgument) throwErrorAtLocation(term.location, "could not translate argument", context); - function->arguments.emplace_back(std::move(translatedArgument.value())); + functionRaw.arguments.emplace_back(std::move(translatedArgument.value())); } return std::move(function); @@ -83,7 +85,7 @@ struct TermTranslateVisitor std::experimental::optional visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, Context &) { - return std::make_unique(std::string(variable.name), ast::Variable::Type::UserDefined); + return ast::Term::make(std::string(variable.name), ast::Variable::Type::UserDefined); } std::experimental::optional visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, Context &context) @@ -98,7 +100,7 @@ struct TermTranslateVisitor auto left = translate(binaryOperation.left, context); auto right = translate(binaryOperation.right, context); - return std::make_unique(operator_, std::move(left), std::move(right)); + return ast::Term::make(operator_, std::move(left), std::move(right)); } std::experimental::optional visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, Context &context) @@ -106,7 +108,7 @@ struct TermTranslateVisitor auto left = translate(interval.left, context); auto right = translate(interval.right, context); - return std::make_unique(std::move(left), std::move(right)); + return ast::Term::make(std::move(left), std::move(right)); } std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context) @@ -120,7 +122,7 @@ struct TermTranslateVisitor for (const auto &argument : function.arguments) arguments.emplace_back(translate(argument, context)); - return std::make_unique(function.name, std::move(arguments)); + return ast::Term::make(function.name, std::move(arguments)); } std::experimental::optional visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &context) diff --git a/include/anthem/output/AST.h b/include/anthem/output/AST.h index 68b48bd..d7007f8 100644 --- a/include/anthem/output/AST.h +++ b/include/anthem/output/AST.h @@ -48,7 +48,7 @@ output::ColorStream &operator<<(output::ColorStream &stream, const Term &term); // Primitives //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, BinaryOperation::Operator operator_) +inline output::ColorStream &operator<<(output::ColorStream &stream, BinaryOperation::Operator operator_) { switch (operator_) { @@ -69,14 +69,14 @@ output::ColorStream &operator<<(output::ColorStream &stream, BinaryOperation::Op //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const BinaryOperation &binaryOperation) +inline output::ColorStream &operator<<(output::ColorStream &stream, const BinaryOperation &binaryOperation) { return (stream << "(" << binaryOperation.left << " " << binaryOperation.operator_ << " " << binaryOperation.right << ")"); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Boolean &boolean) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Boolean &boolean) { if (boolean.value) return (stream << output::Boolean("#true")); @@ -86,7 +86,7 @@ output::ColorStream &operator<<(output::ColorStream &stream, const Boolean &bool //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, Comparison::Operator operator_) +inline output::ColorStream &operator<<(output::ColorStream &stream, Comparison::Operator operator_) { switch (operator_) { @@ -109,21 +109,21 @@ output::ColorStream &operator<<(output::ColorStream &stream, Comparison::Operato //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Comparison &comparison) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Comparison &comparison) { return (stream << comparison.left << " " << comparison.operator_ << " " << comparison.right); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Constant &constant) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Constant &constant) { return (stream << constant.name); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Function &function) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Function &function) { stream << function.name; @@ -148,28 +148,28 @@ output::ColorStream &operator<<(output::ColorStream &stream, const Function &fun //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const In &in) +inline output::ColorStream &operator<<(output::ColorStream &stream, const In &in) { return (stream << in.element << " " << output::Keyword("in") << " " << in.set); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Integer &integer) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Integer &integer) { return (stream << output::Number(integer.value)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Interval &interval) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Interval &interval) { return (stream << interval.from << ".." << interval.to); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Predicate &predicate) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Predicate &predicate) { stream << predicate.name; @@ -191,7 +191,7 @@ output::ColorStream &operator<<(output::ColorStream &stream, const Predicate &pr //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const SpecialInteger &specialInteger) +inline output::ColorStream &operator<<(output::ColorStream &stream, const SpecialInteger &specialInteger) { switch (specialInteger.type) { @@ -206,14 +206,14 @@ output::ColorStream &operator<<(output::ColorStream &stream, const SpecialIntege //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const String &string) +inline output::ColorStream &operator<<(output::ColorStream &stream, const String &string) { return (stream << output::String(string.text.c_str())); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Variable &variable) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Variable &variable) { assert(!variable.name.empty()); assert(variable.name[0] >= 65 && variable.name[0] <= 90); @@ -230,7 +230,7 @@ output::ColorStream &operator<<(output::ColorStream &stream, const Variable &var // Expressions //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const And &and_) +inline output::ColorStream &operator<<(output::ColorStream &stream, const And &and_) { stream << "("; @@ -247,14 +247,14 @@ output::ColorStream &operator<<(output::ColorStream &stream, const And &and_) //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Biconditional &biconditional) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Biconditional &biconditional) { return (stream << "(" << biconditional.left << " <-> " << biconditional.right << ")"); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Exists &exists) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Exists &exists) { stream << output::Keyword("exists") << " "; @@ -263,7 +263,7 @@ output::ColorStream &operator<<(output::ColorStream &stream, const Exists &exist if (i != exists.variables.cbegin()) stream << ", "; - stream << (**i); + stream << (*i); } return (stream << " " << exists.argument); @@ -271,7 +271,7 @@ output::ColorStream &operator<<(output::ColorStream &stream, const Exists &exist //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const ForAll &forAll) +inline output::ColorStream &operator<<(output::ColorStream &stream, const ForAll &forAll) { stream << output::Keyword("forall") << " "; @@ -280,7 +280,7 @@ output::ColorStream &operator<<(output::ColorStream &stream, const ForAll &forAl if (i != forAll.variables.cbegin()) stream << ", "; - stream << (**i); + stream << (*i); } return (stream << " " << forAll.argument); @@ -288,21 +288,21 @@ output::ColorStream &operator<<(output::ColorStream &stream, const ForAll &forAl //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Implies &implies) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Implies &implies) { return (stream << "(" << implies.antecedent << " -> " << implies.consequent << ")"); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Not ¬_) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Not ¬_) { return (stream << output::Keyword("not ") << not_.argument); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Or &or_) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Or &or_) { stream << "("; @@ -321,20 +321,28 @@ output::ColorStream &operator<<(output::ColorStream &stream, const Or &or_) // Variants //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Formula &formula) +template +struct VariantPrintVisitor { - formula.match([&](const auto &x){stream << *x;}); + template + output::ColorStream &visit(const T &x, output::ColorStream &stream) + { + return (stream << x); + } +}; - return stream; +//////////////////////////////////////////////////////////////////////////////////////////////////// + +inline output::ColorStream &operator<<(output::ColorStream &stream, const Formula &formula) +{ + return formula.accept(VariantPrintVisitor(), stream); } //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Term &term) +inline output::ColorStream &operator<<(output::ColorStream &stream, const Term &term) { - term.match([&](const auto &x){stream << *x;}); - - return stream; + return term.accept(VariantPrintVisitor(), stream); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/lib/variant b/lib/variant deleted file mode 160000 index d2588a8..0000000 --- a/lib/variant +++ /dev/null @@ -1 +0,0 @@ -Subproject commit d2588a8f1d6b5d480d228e6d8a906ce634bdea9a diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index e162fdb..bab3285 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -1,7 +1,5 @@ #include -#include - namespace anthem { @@ -13,92 +11,139 @@ namespace anthem bool isPrimitiveTerm(const ast::Term &term) { - const auto handleBinaryOperation = - [](const ast::BinaryOperationPointer &) - { - return false; - }; - - const auto handleInterval = - [](const ast::IntervalPointer &) - { - return false; - }; - - const auto handleDefault = - [](const auto &) - { - return true; - }; - - return term.match(handleBinaryOperation, handleInterval, handleDefault); + return (!term.is() && !term.is()); } //////////////////////////////////////////////////////////////////////////////////////////////////// -bool matchesVariable(const ast::Term &term, const ast::VariablePointer &variable) +template +struct RecursiveFormulaVisitor { - const auto handleVariable = - [&](const ast::VariablePointer &other) - { - return variable->name == other->name; - }; + void visit(ast::And &and_, ast::Formula &formula) + { + for (auto &argument : and_.arguments) + argument.accept(*this, argument); - const auto handleDefault = - [](const auto &) - { - return false; - }; + return T::accept(and_, formula); + } - return term.match(handleVariable, handleDefault); + void visit(ast::Biconditional &biconditional, ast::Formula &formula) + { + biconditional.left.accept(*this, biconditional.left); + biconditional.right.accept(*this, biconditional.right); + + return T::accept(biconditional, formula); + } + + void visit(ast::Boolean &boolean, ast::Formula &formula) + { + return T::accept(boolean, formula); + } + + void visit(ast::Comparison &comparison, ast::Formula &formula) + { + return T::accept(comparison, formula); + } + + void visit(ast::Exists &exists, ast::Formula &formula) + { + exists.argument.accept(*this, exists.argument); + + return T::accept(exists, formula); + } + + void visit(ast::ForAll &forAll, ast::Formula &formula) + { + forAll.argument.accept(*this, forAll.argument); + + return T::accept(forAll, formula); + } + + void visit(ast::Implies &implies, ast::Formula &formula) + { + implies.antecedent.accept(*this, implies.antecedent); + implies.consequent.accept(*this, implies.consequent); + + return T::accept(implies, formula); + } + + void visit(ast::In &in, ast::Formula &formula) + { + return T::accept(in, formula); + } + + void visit(ast::Not ¬_, ast::Formula &formula) + { + not_.argument.accept(*this, not_.argument); + + return T::accept(not_, formula); + } + + void visit(ast::Or &or_, ast::Formula &formula) + { + for (auto &argument : or_.arguments) + argument.accept(*this, argument); + + return T::accept(or_, formula); + } + + void visit(ast::Predicate &predicate, ast::Formula &formula) + { + return T::accept(predicate, formula); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +bool matchesVariable(const ast::Term &term, const ast::Variable &variable) +{ + if (!term.is()) + return false; + + const auto otherVariable = term.get(); + + return variable.name == otherVariable.name; } //////////////////////////////////////////////////////////////////////////////////////////////////// -std::experimental::optional extractAssignedTerm(ast::Formula &formula, const ast::VariablePointer &variable) +std::experimental::optional extractAssignedTerm(ast::Formula &formula, const ast::Variable &variable) { - const auto handleComparison = - [&](ast::ComparisonPointer &comparison) -> std::experimental::optional - { - if (comparison->operator_ != ast::Comparison::Operator::Equal) - return std::experimental::nullopt; + if (!formula.is()) + return std::experimental::nullopt; - if (matchesVariable(comparison->left, variable)) - return std::move(comparison->right); + auto &comparison = formula.get(); - if (matchesVariable(comparison->right, variable)) - return std::move(comparison->left); + if (comparison.operator_ != ast::Comparison::Operator::Equal) + return std::experimental::nullopt; - return std::experimental::nullopt; - }; + if (matchesVariable(comparison.left, variable)) + return std::move(comparison.right); - const auto handleDefault = - [](auto &) -> std::experimental::optional - { - return std::experimental::nullopt; - }; + if (matchesVariable(comparison.right, variable)) + return std::move(comparison.left); - return formula.match(handleComparison, handleDefault); + return std::experimental::nullopt; } //////////////////////////////////////////////////////////////////////////////////////////////////// -ast::Formula simplify(ast::ExistsPointer &exists) +void simplify(ast::Exists &exists, ast::Formula &formula) { - if (!exists->argument.is()) - return std::move(exists); + if (!exists.argument.is()) + return; - auto &conjunction = exists->argument.get_unchecked(); - auto &arguments = conjunction->arguments; + auto &conjunction = exists.argument.get(); + auto &arguments = conjunction.arguments; // Check that formula is in normal form - if (!arguments.back().is()) - return std::move(exists); + if (!arguments.back().is()) + return; const auto replaceVariableInPredicateWithTerm = - [](ast::PredicatePointer &predicate, const ast::VariablePointer &variable, ast::Term &&term) + [](ast::Predicate &predicate, const ast::Variable &variable, ast::Term &term) { - for (auto &argument : predicate->arguments) + for (auto &argument : predicate.arguments) { if (!matchesVariable(argument, variable)) continue; @@ -109,7 +154,7 @@ ast::Formula simplify(ast::ExistsPointer &exists) }; // Simplify formulas of type “exists X (X = t and F(Y))” to “F(t)” - for (auto i = exists->variables.begin(); i != exists->variables.end();) + for (auto i = exists.variables.begin(); i != exists.variables.end();) { auto &variable = *i; @@ -123,10 +168,10 @@ ast::Formula simplify(ast::ExistsPointer &exists) if (!assignedTerm) continue; - auto &lastArgument = arguments.back().get_unchecked(); + auto &lastArgument = arguments.back().get(); // If this argument is an assignment of the variable to some other term, remove the assignment and replace the variable with the other term - replaceVariableInPredicateWithTerm(lastArgument, variable, std::move(assignedTerm.value())); + replaceVariableInPredicateWithTerm(lastArgument, variable, assignedTerm.value()); arguments.erase(j); wasVariableReplaced = true; @@ -135,107 +180,60 @@ ast::Formula simplify(ast::ExistsPointer &exists) if (wasVariableReplaced) { - i = exists->variables.erase(i); + i = exists.variables.erase(i); continue; } i++; } - if (exists->variables.empty()) + // If there are still variables, do nothing more + if (!exists.variables.empty()) + return; + + assert(!conjunction.arguments.empty()); + + // If the argument is a conjunction with just one element, directly replace the input formula with the argument + if (conjunction.arguments.size() == 1) { - assert(!conjunction->arguments.empty()); - - if (conjunction->arguments.size() == 1) - return std::move(conjunction->arguments.front()); - - return std::move(exists->argument); + auto test = std::move(conjunction.arguments.front()); + formula = std::move(test); + return; } - return std::move(exists); + // If there is more than one element in the conjunction, replace the input formula with the conjunction + formula = std::move(exists.argument); } //////////////////////////////////////////////////////////////////////////////////////////////////// -ast::Formula simplify(ast::Formula &&formula) +struct SimplifyFormulaVisitor : public RecursiveFormulaVisitor { - const auto handleAnd = - [&](ast::AndPointer &and_) -> ast::Formula - { - for (auto &argument : and_->arguments) - argument = simplify(std::move(argument)); + static void accept(ast::Exists &exists, ast::Formula &formula) + { + simplify(exists, formula); + } - return std::move(and_); - }; + static void accept(ast::In &in, ast::Formula &formula) + { + if (!isPrimitiveTerm(in.element) || !isPrimitiveTerm(in.set)) + return; - const auto handleBiconditional = - [&](ast::BiconditionalPointer &biconditional) -> ast::Formula - { - biconditional->left = simplify(std::move(biconditional->left)); - biconditional->right = simplify(std::move(biconditional->right)); + // Simplify formulas of type “A in B” to “A = B” if A and B are primitive + formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set)); + } - return std::move(biconditional); - }; + template + static void accept(T &, ast::Formula &) + { + } +}; - const auto handleExists = - [&](ast::ExistsPointer &exists) -> ast::Formula - { - exists->argument = simplify(std::move(exists->argument)); +//////////////////////////////////////////////////////////////////////////////////////////////////// - return simplify(exists); - }; - - const auto handleForAll = - [&](ast::ForAllPointer &forAll) -> ast::Formula - { - forAll->argument = simplify(std::move(forAll->argument)); - - return std::move(forAll); - }; - - const auto handleImplies = - [&](ast::ImpliesPointer &implies) -> ast::Formula - { - implies->antecedent = simplify(std::move(implies->antecedent)); - implies->consequent = simplify(std::move(implies->consequent)); - - return std::move(implies); - }; - - const auto handleIn = - [](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 handleNot = - [&](ast::NotPointer ¬_) -> ast::Formula - { - not_->argument = simplify(std::move(not_->argument)); - - return std::move(not_); - }; - - const auto handleOr = - [&](ast::OrPointer &or_) -> ast::Formula - { - for (auto &argument : or_->arguments) - argument = simplify(std::move(argument)); - - return std::move(or_); - }; - - const auto handleDefault = - [&](auto &x) -> ast::Formula - { - return std::move(x); - }; - - return formula.match(handleAnd, handleBiconditional, handleExists, handleForAll, handleImplies, handleIn, handleNot, handleOr, handleDefault); +void simplify(ast::Formula &formula) +{ + formula.accept(SimplifyFormulaVisitor(), formula); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index edab9c4..d71c919 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -53,8 +53,8 @@ void translate(const char *fileName, std::istream &stream, Context &context) return; } - auto simplifiedFormula = simplify(std::move(formula.value())); - context.logger.outputStream() << simplifiedFormula << std::endl; + simplify(formula.value()); + context.logger.outputStream() << formula.value() << std::endl; }; const auto logger =