From 6d7b91c391fc19b36fb8e8d699ec8bc0e26082be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Mon, 9 Apr 2018 23:13:21 +0200 Subject: [PATCH] Add new simplification rule MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This adds the rule “(F <-> (F and G)) === (F -> G)” to the simplification rule tableau. --- include/anthem/Equality.h | 417 +++++++++++++++++++++++ src/anthem/Simplification.cpp | 49 ++- tests/TestCompletion.cpp | 2 +- tests/TestHiddenPredicateElimination.cpp | 5 +- tests/TestPlaceholders.cpp | 2 +- 5 files changed, 469 insertions(+), 6 deletions(-) create mode 100644 include/anthem/Equality.h diff --git a/include/anthem/Equality.h b/include/anthem/Equality.h new file mode 100644 index 0000000..158cf34 --- /dev/null +++ b/include/anthem/Equality.h @@ -0,0 +1,417 @@ +#ifndef __ANTHEM__EQUALITY_H +#define __ANTHEM__EQUALITY_H + +#include +#include + +namespace anthem +{ +namespace ast +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Equality +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// TODO: move to separate class +enum class Tristate +{ + True, + False, + Unknown, +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Tristate equal(const Formula &lhs, const Formula &rhs); +Tristate equal(const Term &lhs, const Term &rhs); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct FormulaEqualityVisitor +{ + Tristate visit(const And &and_, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + const auto &otherAnd = otherFormula.get(); + + for (const auto &argument : and_.arguments) + { + const auto match = std::find_if( + otherAnd.arguments.cbegin(), otherAnd.arguments.cend(), + [&](const auto &otherArgument) + { + return equal(argument, otherArgument) == Tristate::True; + }); + + if (match == otherAnd.arguments.cend()) + return Tristate::Unknown; + } + + for (const auto &otherArgument : otherAnd.arguments) + { + const auto match = std::find_if( + and_.arguments.cbegin(), and_.arguments.cend(), + [&](const auto &argument) + { + return equal(otherArgument, argument) == Tristate::True; + }); + + if (match == and_.arguments.cend()) + return Tristate::Unknown; + } + + return Tristate::True; + } + + Tristate visit(const Biconditional &biconditional, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + const auto &otherBiconditional = otherFormula.get(); + + if (equal(biconditional.left, otherBiconditional.left) == Tristate::True + && equal(biconditional.right, otherBiconditional.right) == Tristate::True) + { + return Tristate::True; + } + + if (equal(biconditional.left, otherBiconditional.right) == Tristate::True + && equal(biconditional.right, otherBiconditional.left) == Tristate::True) + { + return Tristate::True; + } + + return Tristate::Unknown; + } + + Tristate visit(const Boolean &boolean, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + const auto &otherBoolean = otherFormula.get(); + + return (boolean.value == otherBoolean.value) + ? Tristate::True + : Tristate::False; + } + + Tristate visit(const Comparison &comparison, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + const auto &otherComparison = otherFormula.get(); + + if (comparison.operator_ != otherComparison.operator_) + return Tristate::Unknown; + + if (equal(comparison.left, otherComparison.left) == Tristate::True + && equal(comparison.right, otherComparison.right) == Tristate::True) + { + return Tristate::True; + } + + // Only = and != are commutative operators, all others don’t need to be checked with exchanged arguments + if (comparison.operator_ != Comparison::Operator::Equal + && comparison.operator_ != Comparison::Operator::NotEqual) + { + return Tristate::Unknown; + } + + if (equal(comparison.left, otherComparison.right) == Tristate::True + && equal(comparison.right, otherComparison.left) == Tristate::True) + { + return Tristate::True; + } + + return Tristate::Unknown; + } + + Tristate visit(const Exists &, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + // TODO: implement stronger check + return Tristate::Unknown; + } + + Tristate visit(const ForAll &, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + // TODO: implement stronger check + return Tristate::Unknown; + } + + Tristate visit(const Implies &implies, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + const auto &otherImplies = otherFormula.get(); + + if (equal(implies.antecedent, otherImplies.antecedent) == Tristate::True + && equal(implies.consequent, otherImplies.consequent) == Tristate::True) + { + return Tristate::True; + } + + return Tristate::Unknown; + } + + Tristate visit(const In &in, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + const auto &otherIn = otherFormula.get(); + + if (equal(in.element, otherIn.element) == Tristate::True + && equal(in.set, otherIn.set) == Tristate::True) + { + return Tristate::True; + } + + return Tristate::Unknown; + } + + Tristate visit(const Not ¬_, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + const auto &otherNot = otherFormula.get(); + + return equal(not_.argument, otherNot.argument); + } + + Tristate visit(const Or &or_, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + const auto &otherOr = otherFormula.get(); + + for (const auto &argument : or_.arguments) + { + const auto match = std::find_if( + otherOr.arguments.cbegin(), otherOr.arguments.cend(), + [&](const auto &otherArgument) + { + return equal(argument, otherArgument) == Tristate::True; + }); + + if (match == otherOr.arguments.cend()) + return Tristate::Unknown; + } + + for (const auto &otherArgument : otherOr.arguments) + { + const auto match = std::find_if( + or_.arguments.cbegin(), or_.arguments.cend(), + [&](const auto &argument) + { + return equal(otherArgument, argument) == Tristate::True; + }); + + if (match == or_.arguments.cend()) + return Tristate::Unknown; + } + + return Tristate::True; + } + + Tristate visit(const Predicate &predicate, const Formula &otherFormula) + { + if (!otherFormula.is()) + return Tristate::Unknown; + + const auto &otherPredicate = otherFormula.get(); + + if (!matches(predicate, otherPredicate)) + return Tristate::False; + + assert(predicate.arguments.size() == otherPredicate.arguments.size()); + + for (size_t i = 0; i < predicate.arguments.size(); i++) + if (equal(predicate.arguments[i], otherPredicate.arguments[i]) != Tristate::True) + return Tristate::Unknown; + + return Tristate::True; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct TermEqualityVisitor +{ + Tristate visit(const BinaryOperation &binaryOperation, const Term &otherTerm) + { + if (!otherTerm.is()) + return Tristate::Unknown; + + const auto &otherBinaryOperation = otherTerm.get(); + + if (binaryOperation.operator_ != otherBinaryOperation.operator_) + return Tristate::Unknown; + + if (equal(binaryOperation.left, otherBinaryOperation.left) == Tristate::True + && equal(binaryOperation.right, otherBinaryOperation.right) == Tristate::True) + { + return Tristate::True; + } + + // Only + and * are commutative operators, all others don’t need to be checked with exchanged arguments + if (binaryOperation.operator_ != BinaryOperation::Operator::Plus + && binaryOperation.operator_ != BinaryOperation::Operator::Multiplication) + { + return Tristate::Unknown; + } + + if (equal(binaryOperation.left, binaryOperation.right) == Tristate::True + && equal(binaryOperation.right, binaryOperation.left) == Tristate::True) + { + return Tristate::True; + } + + return Tristate::Unknown; + } + + Tristate visit(const Boolean &boolean, const Term &otherTerm) + { + if (!otherTerm.is()) + return Tristate::Unknown; + + const auto &otherBoolean = otherTerm.get(); + + return (boolean.value == otherBoolean.value) + ? Tristate::True + : Tristate::False; + } + + Tristate visit(const Constant &constant, const Term &otherTerm) + { + if (!otherTerm.is()) + return Tristate::Unknown; + + const auto &otherConstant = otherTerm.get(); + + return (constant.name == otherConstant.name) + ? Tristate::True + : Tristate::False; + } + + Tristate visit(const Function &function, const Term &otherTerm) + { + if (!otherTerm.is()) + return Tristate::Unknown; + + const auto &otherFunction = otherTerm.get(); + + if (function.name != otherFunction.name) + return Tristate::False; + + if (function.arguments.size() != otherFunction.arguments.size()) + return Tristate::False; + + for (size_t i = 0; i < function.arguments.size(); i++) + if (equal(function.arguments[i], otherFunction.arguments[i]) != Tristate::True) + return Tristate::Unknown; + + return Tristate::True; + } + + Tristate visit(const Integer &integer, const Term &otherTerm) + { + if (!otherTerm.is()) + return Tristate::Unknown; + + const auto &otherInteger = otherTerm.get(); + + return (integer.value == otherInteger.value) + ? Tristate::True + : Tristate::False; + } + + Tristate visit(const Interval &interval, const Term &otherTerm) + { + if (!otherTerm.is()) + return Tristate::Unknown; + + const auto &otherInterval = otherTerm.get(); + + if (equal(interval.from, otherInterval.from) != Tristate::True) + return Tristate::Unknown; + + if (equal(interval.to, otherInterval.to) != Tristate::True) + return Tristate::Unknown; + + return Tristate::True; + } + + Tristate visit(const SpecialInteger &specialInteger, const Term &otherTerm) + { + if (!otherTerm.is()) + return Tristate::Unknown; + + const auto &otherSpecialInteger = otherTerm.get(); + + return (specialInteger.type == otherSpecialInteger.type) + ? Tristate::True + : Tristate::False; + } + + Tristate visit(const String &string, const Term &otherTerm) + { + if (!otherTerm.is()) + return Tristate::Unknown; + + const auto &otherString = otherTerm.get(); + + return (string.text == otherString.text) + ? Tristate::True + : Tristate::False; + } + + Tristate visit(const Variable &variable, const Term &otherTerm) + { + if (!otherTerm.is()) + return Tristate::Unknown; + + const auto &otherVariable = otherTerm.get(); + + return (variable.declaration == otherVariable.declaration) + ? Tristate::True + : Tristate::False; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Tristate equal(const Formula &lhs, const Formula &rhs) +{ + return lhs.accept(FormulaEqualityVisitor(), rhs); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Tristate equal(const Term &lhs, const Term &rhs) +{ + return lhs.accept(TermEqualityVisitor(), rhs); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} + +#endif diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index a7654ad..e4f69b4 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -3,6 +3,8 @@ #include #include +#include +#include #include namespace anthem @@ -333,6 +335,50 @@ struct SimplificationRuleInWithPrimitiveArguments //////////////////////////////////////////////////////////////////////////////////////////////////// +struct SimplificationRuleSubsumptionInBiconditionals +{ + static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)"; + + static SimplificationResult apply(ast::Formula &formula) + { + if (!formula.is()) + return SimplificationResult::Unchanged; + + auto &biconditional = formula.get(); + + const auto leftIsPredicate = biconditional.left.is(); + const auto rightIsPredicate = biconditional.right.is(); + + const auto leftIsAnd = biconditional.left.is(); + const auto rightIsAnd = biconditional.right.is(); + + if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd)) + return SimplificationResult::Unchanged; + + auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right); + auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left); + auto &and_ = andSide.get(); + + const auto matchingPredicate = + std::find_if(and_.arguments.cbegin(), and_.arguments.cend(), + [&](const auto &argument) + { + return (ast::equal(predicateSide, argument) == ast::Tristate::True); + }); + + if (matchingPredicate == and_.arguments.cend()) + return SimplificationResult::Unchanged; + + and_.arguments.erase(matchingPredicate); + + formula = ast::Formula::make(std::move(predicateSide), std::move(andSide)); + + return SimplificationResult::Simplified; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + const auto simplifyWithDefaultRules = simplify < @@ -342,7 +388,8 @@ const auto simplifyWithDefaultRules = SimplificationRuleTrivialExists, SimplificationRuleOneElementConjunction, SimplificationRuleExistsWithoutQuantifiedVariables, - SimplificationRuleInWithPrimitiveArguments + SimplificationRuleInWithPrimitiveArguments, + SimplificationRuleSubsumptionInBiconditionals >; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/tests/TestCompletion.cpp b/tests/TestCompletion.cpp index 19419b4..27ac73a 100644 --- a/tests/TestCompletion.cpp +++ b/tests/TestCompletion.cpp @@ -152,7 +152,7 @@ TEST_CASE("[completion] Rules are completed", "[completion]") CHECK(output.str() == "forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n" - "forall V2, V3 (in(V2, V3) <-> (V2 in 1..n and V3 in 1..r and in(V2, V3)))\n" + "forall V2, V3 (in(V2, V3) -> (V2 in 1..n and V3 in 1..r))\n" "forall U2 not (U2 in 1..n and not covered(U2))\n" "forall U3, U4, U5 not (in(U3, U4) and in(U5, U4) and exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n"); } diff --git a/tests/TestHiddenPredicateElimination.cpp b/tests/TestHiddenPredicateElimination.cpp index 792e24b..04d0089 100644 --- a/tests/TestHiddenPredicateElimination.cpp +++ b/tests/TestHiddenPredicateElimination.cpp @@ -164,10 +164,9 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin "#show t/0."; anthem::translate("input", input, context); - // TODO: simplify further CHECK(output.str() == - "(s <-> (not #false and s))\n" - "(t <-> (not #false and t))\n" + "(s -> not #false)\n" + "(t -> not #false)\n" "not (s and not t)\n" "not (not #false and not #false and #false)\n"); } diff --git a/tests/TestPlaceholders.cpp b/tests/TestPlaceholders.cpp index 3cc4652..810d3b9 100644 --- a/tests/TestPlaceholders.cpp +++ b/tests/TestPlaceholders.cpp @@ -55,7 +55,7 @@ TEST_CASE("[placeholders] Programs with placeholders are correctly completed", " anthem::translate("input", input, context); CHECK(output.str() == - "forall V1, V2 (color(V1, V2) <-> (vertex(V1) and color(V2) and color(V1, V2)))\n" + "forall V1, V2 (color(V1, V2) -> (vertex(V1) and color(V2)))\n" "forall U1 not (vertex(U1) and not exists U2 color(U1, U2))\n" "forall U3, U4, U5 not (color(U3, U4) and color(U5, U4) and edge(U3, U5))\n"); }