Add new simplification rule
This adds the rule “(F <-> (F and G)) === (F -> G)” to the simplification rule tableau.
This commit is contained in:
parent
b88393655a
commit
6d7b91c391
GPG Key ID:
05F3611E97A70ABF
|
|
@ -0,0 +1,417 @@
|
|||
#ifndef __ANTHEM__EQUALITY_H
|
||||
#define __ANTHEM__EQUALITY_H
|
||||
|
||||
#include <anthem/AST.h>
|
||||
#include <anthem/ASTUtils.h>
|
||||
|
||||
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<And>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherAnd = otherFormula.get<And>();
|
||||
|
||||
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<Biconditional>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherBiconditional = otherFormula.get<Biconditional>();
|
||||
|
||||
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<Boolean>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherBoolean = otherFormula.get<Boolean>();
|
||||
|
||||
return (boolean.value == otherBoolean.value)
|
||||
? Tristate::True
|
||||
: Tristate::False;
|
||||
}
|
||||
|
||||
Tristate visit(const Comparison &comparison, const Formula &otherFormula)
|
||||
{
|
||||
if (!otherFormula.is<Comparison>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherComparison = otherFormula.get<Comparison>();
|
||||
|
||||
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<Exists>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
// TODO: implement stronger check
|
||||
return Tristate::Unknown;
|
||||
}
|
||||
|
||||
Tristate visit(const ForAll &, const Formula &otherFormula)
|
||||
{
|
||||
if (!otherFormula.is<ForAll>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
// TODO: implement stronger check
|
||||
return Tristate::Unknown;
|
||||
}
|
||||
|
||||
Tristate visit(const Implies &implies, const Formula &otherFormula)
|
||||
{
|
||||
if (!otherFormula.is<Implies>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherImplies = otherFormula.get<Implies>();
|
||||
|
||||
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<In>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherIn = otherFormula.get<In>();
|
||||
|
||||
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<Not>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherNot = otherFormula.get<Not>();
|
||||
|
||||
return equal(not_.argument, otherNot.argument);
|
||||
}
|
||||
|
||||
Tristate visit(const Or &or_, const Formula &otherFormula)
|
||||
{
|
||||
if (!otherFormula.is<Or>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherOr = otherFormula.get<Or>();
|
||||
|
||||
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<Predicate>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherPredicate = otherFormula.get<Predicate>();
|
||||
|
||||
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<BinaryOperation>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherBinaryOperation = otherTerm.get<BinaryOperation>();
|
||||
|
||||
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<Boolean>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherBoolean = otherTerm.get<Boolean>();
|
||||
|
||||
return (boolean.value == otherBoolean.value)
|
||||
? Tristate::True
|
||||
: Tristate::False;
|
||||
}
|
||||
|
||||
Tristate visit(const Constant &constant, const Term &otherTerm)
|
||||
{
|
||||
if (!otherTerm.is<Constant>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherConstant = otherTerm.get<Constant>();
|
||||
|
||||
return (constant.name == otherConstant.name)
|
||||
? Tristate::True
|
||||
: Tristate::False;
|
||||
}
|
||||
|
||||
Tristate visit(const Function &function, const Term &otherTerm)
|
||||
{
|
||||
if (!otherTerm.is<Function>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherFunction = otherTerm.get<Function>();
|
||||
|
||||
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<Integer>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherInteger = otherTerm.get<Integer>();
|
||||
|
||||
return (integer.value == otherInteger.value)
|
||||
? Tristate::True
|
||||
: Tristate::False;
|
||||
}
|
||||
|
||||
Tristate visit(const Interval &interval, const Term &otherTerm)
|
||||
{
|
||||
if (!otherTerm.is<Interval>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherInterval = otherTerm.get<Interval>();
|
||||
|
||||
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<SpecialInteger>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherSpecialInteger = otherTerm.get<SpecialInteger>();
|
||||
|
||||
return (specialInteger.type == otherSpecialInteger.type)
|
||||
? Tristate::True
|
||||
: Tristate::False;
|
||||
}
|
||||
|
||||
Tristate visit(const String &string, const Term &otherTerm)
|
||||
{
|
||||
if (!otherTerm.is<String>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherString = otherTerm.get<String>();
|
||||
|
||||
return (string.text == otherString.text)
|
||||
? Tristate::True
|
||||
: Tristate::False;
|
||||
}
|
||||
|
||||
Tristate visit(const Variable &variable, const Term &otherTerm)
|
||||
{
|
||||
if (!otherTerm.is<Variable>())
|
||||
return Tristate::Unknown;
|
||||
|
||||
const auto &otherVariable = otherTerm.get<Variable>();
|
||||
|
||||
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
|
||||
|
|
@ -3,6 +3,8 @@
|
|||
#include <optional>
|
||||
|
||||
#include <anthem/ASTCopy.h>
|
||||
#include <anthem/Equality.h>
|
||||
#include <anthem/output/AST.h>
|
||||
#include <anthem/SimplificationVisitors.h>
|
||||
|
||||
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<ast::Biconditional>())
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &biconditional = formula.get<ast::Biconditional>();
|
||||
|
||||
const auto leftIsPredicate = biconditional.left.is<ast::Predicate>();
|
||||
const auto rightIsPredicate = biconditional.right.is<ast::Predicate>();
|
||||
|
||||
const auto leftIsAnd = biconditional.left.is<ast::And>();
|
||||
const auto rightIsAnd = biconditional.right.is<ast::And>();
|
||||
|
||||
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<ast::And>();
|
||||
|
||||
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<ast::Implies>(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
|
||||
>;
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue