Compare commits
12 Commits
develop
...
v0.1.8-rc.
Author | SHA1 | Date |
---|---|---|
Patrick Lühne | 285fa08e5a | |
Patrick Lühne | dfffdcfce6 | |
Patrick Lühne | 4967576b6c | |
Patrick Lühne | 1c5851441d | |
Patrick Lühne | b18ddcc575 | |
Patrick Lühne | 00ab975c2d | |
Patrick Lühne | e01b5dc561 | |
Patrick Lühne | 91529b84aa | |
Patrick Lühne | 1cbfd335a1 | |
Patrick Lühne | a86e978a5a | |
Patrick Lühne | 5eb3ed5681 | |
Patrick Lühne | 3d0266136c |
|
@ -1,6 +1,10 @@
|
||||||
# Change Log
|
# Change Log
|
||||||
|
|
||||||
## (unreleased)
|
## 0.1.8 RC 1 (2018-04-10)
|
||||||
|
|
||||||
|
### Features
|
||||||
|
|
||||||
|
* more, advanced simplification rules
|
||||||
|
|
||||||
## 0.1.7 (2018-04-08)
|
## 0.1.7 (2018-04-08)
|
||||||
|
|
||||||
|
|
|
@ -70,7 +70,7 @@ int main(int argc, char **argv)
|
||||||
|
|
||||||
if (version)
|
if (version)
|
||||||
{
|
{
|
||||||
std::cout << "anthem version 0.1.7+git" << std::endl;
|
std::cout << "anthem version 0.1.8-rc.1" << std::endl;
|
||||||
return EXIT_SUCCESS;
|
return EXIT_SUCCESS;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -3,3 +3,5 @@ covered(I) :- in(I, S).
|
||||||
|
|
||||||
:- I = 1..n, not covered(I).
|
:- I = 1..n, not covered(I).
|
||||||
:- in(I, S), in(J, S), in(I + J, S).
|
:- in(I, S), in(J, S), in(I + J, S).
|
||||||
|
|
||||||
|
#show in/2.
|
||||||
|
|
|
@ -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
|
|
@ -12,6 +12,14 @@ namespace anthem
|
||||||
//
|
//
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
enum class SimplificationResult
|
||||||
|
{
|
||||||
|
Simplified,
|
||||||
|
Unchanged,
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
void simplify(ast::Formula &formula);
|
void simplify(ast::Formula &formula);
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
@ -0,0 +1,198 @@
|
||||||
|
#ifndef __ANTHEM__SIMPLIFICATION_VISITORS_H
|
||||||
|
#define __ANTHEM__SIMPLIFICATION_VISITORS_H
|
||||||
|
|
||||||
|
#include <anthem/AST.h>
|
||||||
|
#include <anthem/Simplification.h>
|
||||||
|
|
||||||
|
namespace anthem
|
||||||
|
{
|
||||||
|
namespace ast
|
||||||
|
{
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
//
|
||||||
|
// Simplification Visitor
|
||||||
|
//
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
template<class T>
|
||||||
|
struct FormulaSimplificationVisitor
|
||||||
|
{
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
for (auto &argument : and_.arguments)
|
||||||
|
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Not ¬_, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
for (auto &argument : or_.arguments)
|
||||||
|
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
template<class T, class SimplificationResult = void>
|
||||||
|
struct TermSimplificationVisitor
|
||||||
|
{
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Constant &, Term &term, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
for (auto &argument : function.arguments)
|
||||||
|
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(String &, Term &term, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments)
|
||||||
|
{
|
||||||
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
#endif
|
|
@ -3,7 +3,9 @@
|
||||||
#include <optional>
|
#include <optional>
|
||||||
|
|
||||||
#include <anthem/ASTCopy.h>
|
#include <anthem/ASTCopy.h>
|
||||||
#include <anthem/ASTVisitors.h>
|
#include <anthem/Equality.h>
|
||||||
|
#include <anthem/output/AST.h>
|
||||||
|
#include <anthem/SimplificationVisitors.h>
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
|
@ -97,18 +99,65 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// Simplifies exists statements by using the equivalence “exists X (X = t and F(X))” == “F(t)”
|
template<class SimplificationRule>
|
||||||
// The exists statement has to be of the form “exists <variables> <conjunction>”
|
SimplificationResult simplify(ast::Formula &formula)
|
||||||
void simplify(ast::Exists &exists, ast::Formula &formula)
|
|
||||||
{
|
{
|
||||||
// Simplify formulas like “exists X (X = Y)” to “#true”
|
return SimplificationRule::apply(formula);
|
||||||
// TODO: check that this covers all cases
|
}
|
||||||
if (exists.argument.is<ast::Comparison>())
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
|
||||||
|
SimplificationResult simplify(ast::Formula &formula)
|
||||||
|
{
|
||||||
|
if (simplify<FirstSimplificationRule>(formula) == SimplificationResult::Simplified)
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct SimplificationRuleExistsWithoutQuantifiedVariables
|
||||||
|
{
|
||||||
|
static constexpr const auto Description = "exists () (F) === F";
|
||||||
|
|
||||||
|
static SimplificationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
|
if (!formula.is<ast::Exists>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto &exists = formula.get<ast::Exists>();
|
||||||
|
|
||||||
|
if (!exists.variables.empty())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
formula = std::move(exists.argument);
|
||||||
|
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct SimplificationRuleTrivialAssignmentInExists
|
||||||
|
{
|
||||||
|
static constexpr const auto Description = "exists X (X = Y) === #true";
|
||||||
|
|
||||||
|
static SimplificationResult apply(ast::Formula &formula)
|
||||||
|
{
|
||||||
|
if (!formula.is<ast::Exists>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
const auto &exists = formula.get<ast::Exists>();
|
||||||
|
|
||||||
|
if (!exists.argument.is<ast::Comparison>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
const auto &comparison = exists.argument.get<ast::Comparison>();
|
const auto &comparison = exists.argument.get<ast::Comparison>();
|
||||||
|
|
||||||
if (comparison.operator_ != ast::Comparison::Operator::Equal)
|
if (comparison.operator_ != ast::Comparison::Operator::Equal)
|
||||||
return;
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
|
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
|
||||||
[&](const auto &variableDeclaration)
|
[&](const auto &variableDeclaration)
|
||||||
|
@ -117,107 +166,331 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
|
||||||
|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
|
|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
|
||||||
});
|
});
|
||||||
|
|
||||||
if (matchingAssignment != exists.variables.cend())
|
if (matchingAssignment == exists.variables.cend())
|
||||||
formula = ast::Formula::make<ast::Boolean>(true);
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
return;
|
formula = ast::Formula::make<ast::Boolean>(true);
|
||||||
|
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
}
|
}
|
||||||
|
};
|
||||||
|
|
||||||
if (!exists.argument.is<ast::And>())
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
return;
|
|
||||||
|
|
||||||
auto &conjunction = exists.argument.get<ast::And>();
|
struct SimplificationRuleAssignmentInExists
|
||||||
auto &arguments = conjunction.arguments;
|
{
|
||||||
|
static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
|
||||||
|
|
||||||
// Simplify formulas of type “exists X (X = t and F(X))” to “F(t)”
|
static SimplificationResult apply(ast::Formula &formula)
|
||||||
for (auto i = exists.variables.begin(); i != exists.variables.end();)
|
|
||||||
{
|
{
|
||||||
const auto &variableDeclaration = **i;
|
if (!formula.is<ast::Exists>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
bool wasVariableReplaced = false;
|
auto &exists = formula.get<ast::Exists>();
|
||||||
|
|
||||||
// TODO: refactor
|
if (!exists.argument.is<ast::And>())
|
||||||
for (auto j = arguments.begin(); j != arguments.end(); j++)
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto &and_ = exists.argument.get<ast::And>();
|
||||||
|
auto &arguments = and_.arguments;
|
||||||
|
|
||||||
|
auto simplificationResult = SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
for (auto i = exists.variables.begin(); i != exists.variables.end();)
|
||||||
{
|
{
|
||||||
auto &argument = *j;
|
const auto &variableDeclaration = **i;
|
||||||
// Find term that is equivalent to the given variable
|
|
||||||
auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
|
|
||||||
|
|
||||||
if (!assignedTerm)
|
bool wasVariableReplaced = false;
|
||||||
continue;
|
|
||||||
|
|
||||||
// Replace all occurrences of the variable with the equivalent term
|
// TODO: refactor
|
||||||
for (auto k = arguments.begin(); k != arguments.end(); k++)
|
for (auto j = arguments.begin(); j != arguments.end(); j++)
|
||||||
{
|
{
|
||||||
if (k == j)
|
auto &argument = *j;
|
||||||
|
// Find term that is equivalent to the given variable
|
||||||
|
auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
|
||||||
|
|
||||||
|
if (!assignedTerm)
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
auto &otherArgument = *k;
|
// Replace all occurrences of the variable with the equivalent term
|
||||||
otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
|
for (auto k = arguments.begin(); k != arguments.end(); k++)
|
||||||
|
{
|
||||||
|
if (k == j)
|
||||||
|
continue;
|
||||||
|
|
||||||
|
auto &otherArgument = *k;
|
||||||
|
otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
|
||||||
|
}
|
||||||
|
|
||||||
|
arguments.erase(j);
|
||||||
|
|
||||||
|
wasVariableReplaced = true;
|
||||||
|
simplificationResult = SimplificationResult::Simplified;
|
||||||
|
|
||||||
|
break;
|
||||||
}
|
}
|
||||||
|
|
||||||
arguments.erase(j);
|
if (wasVariableReplaced)
|
||||||
wasVariableReplaced = true;
|
{
|
||||||
break;
|
i = exists.variables.erase(i);
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
|
||||||
|
i++;
|
||||||
}
|
}
|
||||||
|
|
||||||
if (wasVariableReplaced)
|
return simplificationResult;
|
||||||
{
|
|
||||||
i = exists.variables.erase(i);
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
i++;
|
|
||||||
}
|
}
|
||||||
|
};
|
||||||
|
|
||||||
// If there are no arguments left, we had a formula of the form “exists X1, ..., Xn (X1 = Y1 and ... and Xn = Yn)”
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
// Such exists statements are useless and can be safely replaced with “#true”
|
|
||||||
if (arguments.empty())
|
struct SimplificationRuleEmptyConjunction
|
||||||
|
{
|
||||||
|
static constexpr const auto Description = "[empty conjunction] === #true";
|
||||||
|
|
||||||
|
static SimplificationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
|
if (!formula.is<ast::And>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto &and_ = formula.get<ast::And>();
|
||||||
|
|
||||||
|
if (!and_.arguments.empty())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
formula = ast::Formula::make<ast::Boolean>(true);
|
formula = ast::Formula::make<ast::Boolean>(true);
|
||||||
return;
|
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
}
|
}
|
||||||
|
};
|
||||||
|
|
||||||
// If the argument now is a conjunction with just one element, directly replace the input formula with the argument
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
if (arguments.size() == 1)
|
|
||||||
exists.argument = std::move(arguments.front());
|
|
||||||
|
|
||||||
// If there are still remaining variables, simplification is over
|
struct SimplificationRuleOneElementConjunction
|
||||||
if (!exists.variables.empty())
|
{
|
||||||
return;
|
static constexpr const auto Description = "[conjunction of only F] === F";
|
||||||
|
|
||||||
assert(!arguments.empty());
|
static SimplificationResult apply(ast::Formula &formula)
|
||||||
|
{
|
||||||
|
if (!formula.is<ast::And>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
// If there is more than one element in the conjunction, replace the input formula with the conjunction
|
auto &and_ = formula.get<ast::And>();
|
||||||
formula = std::move(exists.argument);
|
|
||||||
}
|
if (and_.arguments.size() != 1)
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
formula = std::move(and_.arguments.front());
|
||||||
|
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct SimplificationRuleTrivialExists
|
||||||
|
{
|
||||||
|
static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
|
||||||
|
|
||||||
|
static SimplificationResult apply(ast::Formula &formula)
|
||||||
|
{
|
||||||
|
if (!formula.is<ast::Exists>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto &exists = formula.get<ast::Exists>();
|
||||||
|
|
||||||
|
if (!exists.argument.is<ast::Boolean>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
formula = std::move(exists.argument);
|
||||||
|
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct SimplificationRuleInWithPrimitiveArguments
|
||||||
|
{
|
||||||
|
static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
|
||||||
|
|
||||||
|
static SimplificationResult apply(ast::Formula &formula)
|
||||||
|
{
|
||||||
|
if (!formula.is<ast::In>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto &in = formula.get<ast::In>();
|
||||||
|
|
||||||
|
assert(ast::isPrimitive(in.element));
|
||||||
|
|
||||||
|
if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
|
||||||
|
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
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;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct SimplificationRuleDoubleNegation
|
||||||
|
{
|
||||||
|
static constexpr const auto Description = "not not F === F";
|
||||||
|
|
||||||
|
static SimplificationResult apply(ast::Formula &formula)
|
||||||
|
{
|
||||||
|
if (!formula.is<ast::Not>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto ¬_ = formula.get<ast::Not>();
|
||||||
|
|
||||||
|
if (!not_.argument.is<ast::Not>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto ¬Not = not_.argument.get<ast::Not>();
|
||||||
|
|
||||||
|
formula = std::move(notNot.argument);
|
||||||
|
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct SimplificationRuleDeMorganForConjunctions
|
||||||
|
{
|
||||||
|
static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
|
||||||
|
|
||||||
|
static SimplificationResult apply(ast::Formula &formula)
|
||||||
|
{
|
||||||
|
if (!formula.is<ast::Not>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto ¬_ = formula.get<ast::Not>();
|
||||||
|
|
||||||
|
if (!not_.argument.is<ast::And>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto &and_ = not_.argument.get<ast::And>();
|
||||||
|
|
||||||
|
for (auto &argument : and_.arguments)
|
||||||
|
argument = ast::Formula::make<ast::Not>(std::move(argument));
|
||||||
|
|
||||||
|
formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
|
||||||
|
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct SimplificationRuleImplicationFromDisjunction
|
||||||
|
{
|
||||||
|
static constexpr const auto Description = "(not F or G) === (F -> G)";
|
||||||
|
|
||||||
|
static SimplificationResult apply(ast::Formula &formula)
|
||||||
|
{
|
||||||
|
if (!formula.is<ast::Or>())
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto &or_ = formula.get<ast::Or>();
|
||||||
|
|
||||||
|
if (or_.arguments.size() != 2)
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
const auto leftIsNot = or_.arguments[0].is<ast::Not>();
|
||||||
|
const auto rightIsNot = or_.arguments[1].is<ast::Not>();
|
||||||
|
|
||||||
|
if (leftIsNot == rightIsNot)
|
||||||
|
return SimplificationResult::Unchanged;
|
||||||
|
|
||||||
|
auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
|
||||||
|
auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
|
||||||
|
|
||||||
|
assert(negativeSide.is<ast::Not>());
|
||||||
|
assert(!positiveSide.is<ast::Not>());
|
||||||
|
|
||||||
|
auto &negativeSideArgument = negativeSide.get<ast::Not>().argument;
|
||||||
|
|
||||||
|
formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
|
||||||
|
|
||||||
|
return SimplificationResult::Simplified;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
const auto simplifyWithDefaultRules =
|
||||||
|
simplify
|
||||||
|
<
|
||||||
|
SimplificationRuleDoubleNegation,
|
||||||
|
SimplificationRuleTrivialAssignmentInExists,
|
||||||
|
SimplificationRuleAssignmentInExists,
|
||||||
|
SimplificationRuleEmptyConjunction,
|
||||||
|
SimplificationRuleTrivialExists,
|
||||||
|
SimplificationRuleOneElementConjunction,
|
||||||
|
SimplificationRuleExistsWithoutQuantifiedVariables,
|
||||||
|
SimplificationRuleInWithPrimitiveArguments,
|
||||||
|
SimplificationRuleSubsumptionInBiconditionals,
|
||||||
|
SimplificationRuleDeMorganForConjunctions,
|
||||||
|
SimplificationRuleImplicationFromDisjunction
|
||||||
|
>;
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// Performs the different simplification techniques
|
// Performs the different simplification techniques
|
||||||
struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyFormulaVisitor>
|
struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
|
||||||
{
|
{
|
||||||
// Forward exists statements to the dedicated simplification function
|
|
||||||
static void accept(ast::Exists &exists, ast::Formula &formula)
|
|
||||||
{
|
|
||||||
simplify(exists, formula);
|
|
||||||
}
|
|
||||||
|
|
||||||
// Simplify formulas of type “A in B” to “A = B” if A and B are primitive
|
|
||||||
static void accept(ast::In &in, ast::Formula &formula)
|
|
||||||
{
|
|
||||||
assert(ast::isPrimitive(in.element));
|
|
||||||
|
|
||||||
if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
|
|
||||||
return;
|
|
||||||
|
|
||||||
formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
|
|
||||||
}
|
|
||||||
|
|
||||||
// Do nothing for all other types of expressions
|
// Do nothing for all other types of expressions
|
||||||
template<class T>
|
static SimplificationResult accept(ast::Formula &formula)
|
||||||
static void accept(T &, ast::Formula &)
|
|
||||||
{
|
{
|
||||||
|
return simplifyWithDefaultRules(formula);
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -225,7 +498,7 @@ struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyForm
|
||||||
|
|
||||||
void simplify(ast::Formula &formula)
|
void simplify(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
formula.accept(SimplifyFormulaVisitor(), formula);
|
while (formula.accept(SimplifyFormulaVisitor(), formula) == SimplificationResult::Simplified);
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
@ -152,9 +152,9 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
|
||||||
|
|
||||||
CHECK(output.str() ==
|
CHECK(output.str() ==
|
||||||
"forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n"
|
"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 U2 (U2 in 1..n -> 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");
|
"forall U3, U4, U5 (not in(U3, U4) or not in(U5, U4) or not exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
SECTION("binary operations with multiple variables")
|
SECTION("binary operations with multiple variables")
|
||||||
|
|
|
@ -103,9 +103,10 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
|
||||||
"#show a/1.";
|
"#show a/1.";
|
||||||
anthem::translate("input", input, context);
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
|
// TODO: simplify further
|
||||||
CHECK(output.str() ==
|
CHECK(output.str() ==
|
||||||
"forall V1 (a(V1) <-> not d(V1))\n"
|
"forall V1 (a(V1) <-> not d(V1))\n"
|
||||||
"forall V2 (d(V2) <-> not not d(V2))\n"
|
"forall V2 (d(V2) <-> d(V2))\n"
|
||||||
"forall V3 (e(V3) <-> e(V3))\n");
|
"forall V3 (e(V3) <-> e(V3))\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -164,12 +165,11 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
|
||||||
"#show t/0.";
|
"#show t/0.";
|
||||||
anthem::translate("input", input, context);
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
// TODO: simplify further
|
|
||||||
CHECK(output.str() ==
|
CHECK(output.str() ==
|
||||||
"(s <-> (not #false and s))\n"
|
"(s -> not #false)\n"
|
||||||
"(t <-> (not #false and t))\n"
|
"(t -> not #false)\n"
|
||||||
"not (s and not t)\n"
|
"(s -> t)\n"
|
||||||
"not (not #false and not #false and #false)\n");
|
"(#false or #false or not #false)\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
SECTION("predicate with more than one argument is hidden correctly")
|
SECTION("predicate with more than one argument is hidden correctly")
|
||||||
|
|
|
@ -55,8 +55,8 @@ TEST_CASE("[placeholders] Programs with placeholders are correctly completed", "
|
||||||
anthem::translate("input", input, context);
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
CHECK(output.str() ==
|
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 U1 (vertex(U1) -> exists U2 color(U1, U2))\n"
|
||||||
"forall U3, U4, U5 not (color(U3, U4) and color(U5, U4) and edge(U3, U5))\n");
|
"forall U3, U4, U5 (not color(U3, U4) or not color(U5, U4) or not edge(U3, U5))\n");
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue