2017-03-16 15:45:55 +01:00
|
|
|
#include <anthem/Simplification.h>
|
|
|
|
|
|
|
|
namespace anthem
|
|
|
|
{
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
//
|
|
|
|
// Simplification
|
|
|
|
//
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
bool isPrimitiveTerm(const ast::Term &term)
|
|
|
|
{
|
2017-03-23 00:44:10 +01:00
|
|
|
return (!term.is<ast::BinaryOperation>() && !term.is<ast::Interval>());
|
|
|
|
}
|
2017-03-16 15:45:55 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
2017-03-16 15:45:55 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
template<class T>
|
|
|
|
struct RecursiveFormulaVisitor
|
|
|
|
{
|
|
|
|
void visit(ast::And &and_, ast::Formula &formula)
|
|
|
|
{
|
|
|
|
for (auto &argument : and_.arguments)
|
|
|
|
argument.accept(*this, argument);
|
2017-03-16 15:45:55 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
return T::accept(and_, formula);
|
|
|
|
}
|
|
|
|
|
|
|
|
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);
|
|
|
|
}
|
|
|
|
};
|
2017-03-17 02:42:48 +01:00
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
bool matchesVariable(const ast::Term &term, const ast::Variable &variable)
|
2017-03-17 02:42:48 +01:00
|
|
|
{
|
2017-03-23 00:44:10 +01:00
|
|
|
if (!term.is<ast::Variable>())
|
|
|
|
return false;
|
2017-03-17 02:42:48 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
const auto otherVariable = term.get<ast::Variable>();
|
2017-03-17 02:42:48 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
return variable.name == otherVariable.name;
|
2017-03-17 02:42:48 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
std::experimental::optional<ast::Term> extractAssignedTerm(ast::Formula &formula, const ast::Variable &variable)
|
2017-03-17 02:42:48 +01:00
|
|
|
{
|
2017-03-23 00:44:10 +01:00
|
|
|
if (!formula.is<ast::Comparison>())
|
|
|
|
return std::experimental::nullopt;
|
2017-03-17 02:42:48 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
auto &comparison = formula.get<ast::Comparison>();
|
2017-03-17 02:42:48 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
if (comparison.operator_ != ast::Comparison::Operator::Equal)
|
|
|
|
return std::experimental::nullopt;
|
2017-03-17 02:42:48 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
if (matchesVariable(comparison.left, variable))
|
|
|
|
return std::move(comparison.right);
|
2017-03-17 02:42:48 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
if (matchesVariable(comparison.right, variable))
|
|
|
|
return std::move(comparison.left);
|
2017-03-17 02:42:48 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
return std::experimental::nullopt;
|
2017-03-17 02:42:48 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
void simplify(ast::Exists &exists, ast::Formula &formula)
|
2017-03-17 02:42:48 +01:00
|
|
|
{
|
2017-03-23 00:44:10 +01:00
|
|
|
if (!exists.argument.is<ast::And>())
|
|
|
|
return;
|
2017-03-17 02:42:48 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
auto &conjunction = exists.argument.get<ast::And>();
|
|
|
|
auto &arguments = conjunction.arguments;
|
2017-03-17 02:42:48 +01:00
|
|
|
|
|
|
|
// Check that formula is in normal form
|
2017-03-23 00:44:10 +01:00
|
|
|
if (!arguments.back().is<ast::Predicate>())
|
|
|
|
return;
|
2017-03-17 02:42:48 +01:00
|
|
|
|
|
|
|
const auto replaceVariableInPredicateWithTerm =
|
2017-03-23 00:44:10 +01:00
|
|
|
[](ast::Predicate &predicate, const ast::Variable &variable, ast::Term &term)
|
2017-03-17 02:42:48 +01:00
|
|
|
{
|
2017-03-23 00:44:10 +01:00
|
|
|
for (auto &argument : predicate.arguments)
|
2017-03-17 02:42:48 +01:00
|
|
|
{
|
|
|
|
if (!matchesVariable(argument, variable))
|
|
|
|
continue;
|
|
|
|
|
|
|
|
argument = std::move(term);
|
|
|
|
break;
|
|
|
|
}
|
|
|
|
};
|
|
|
|
|
|
|
|
// Simplify formulas of type “exists X (X = t and F(Y))” to “F(t)”
|
2017-03-23 00:44:10 +01:00
|
|
|
for (auto i = exists.variables.begin(); i != exists.variables.end();)
|
2017-03-17 02:42:48 +01:00
|
|
|
{
|
|
|
|
auto &variable = *i;
|
|
|
|
|
|
|
|
bool wasVariableReplaced = false;
|
|
|
|
|
|
|
|
for (auto j = arguments.begin(); j != arguments.end(); j++)
|
|
|
|
{
|
|
|
|
auto &argument = *j;
|
|
|
|
auto assignedTerm = extractAssignedTerm(argument, variable);
|
|
|
|
|
|
|
|
if (!assignedTerm)
|
|
|
|
continue;
|
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
auto &lastArgument = arguments.back().get<ast::Predicate>();
|
2017-03-17 02:42:48 +01:00
|
|
|
|
|
|
|
// If this argument is an assignment of the variable to some other term, remove the assignment and replace the variable with the other term
|
2017-03-23 00:44:10 +01:00
|
|
|
replaceVariableInPredicateWithTerm(lastArgument, variable, assignedTerm.value());
|
2017-03-17 02:42:48 +01:00
|
|
|
|
|
|
|
arguments.erase(j);
|
|
|
|
wasVariableReplaced = true;
|
|
|
|
break;
|
|
|
|
}
|
|
|
|
|
|
|
|
if (wasVariableReplaced)
|
|
|
|
{
|
2017-03-23 00:44:10 +01:00
|
|
|
i = exists.variables.erase(i);
|
2017-03-17 02:42:48 +01:00
|
|
|
continue;
|
|
|
|
}
|
|
|
|
|
|
|
|
i++;
|
|
|
|
}
|
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
// If there are still variables, do nothing more
|
|
|
|
if (!exists.variables.empty())
|
|
|
|
return;
|
2017-03-17 02:42:48 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
assert(!conjunction.arguments.empty());
|
2017-03-17 02:42:48 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
// If the argument is a conjunction with just one element, directly replace the input formula with the argument
|
|
|
|
if (conjunction.arguments.size() == 1)
|
|
|
|
{
|
|
|
|
auto test = std::move(conjunction.arguments.front());
|
|
|
|
formula = std::move(test);
|
|
|
|
return;
|
2017-03-17 02:42:48 +01:00
|
|
|
}
|
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
// If there is more than one element in the conjunction, replace the input formula with the conjunction
|
|
|
|
formula = std::move(exists.argument);
|
2017-03-16 15:45:55 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
struct SimplifyFormulaVisitor : public RecursiveFormulaVisitor<SimplifyFormulaVisitor>
|
2017-03-16 15:45:55 +01:00
|
|
|
{
|
2017-03-23 00:44:10 +01:00
|
|
|
static void accept(ast::Exists &exists, ast::Formula &formula)
|
|
|
|
{
|
|
|
|
simplify(exists, formula);
|
|
|
|
}
|
2017-03-16 15:45:55 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
static void accept(ast::In &in, ast::Formula &formula)
|
|
|
|
{
|
|
|
|
if (!isPrimitiveTerm(in.element) || !isPrimitiveTerm(in.set))
|
|
|
|
return;
|
2017-03-16 15:45:55 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
// 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));
|
|
|
|
}
|
2017-03-16 15:45:55 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
template<class T>
|
|
|
|
static void accept(T &, ast::Formula &)
|
|
|
|
{
|
|
|
|
}
|
|
|
|
};
|
2017-03-16 15:45:55 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
2017-03-16 15:45:55 +01:00
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
void simplify(ast::Formula &formula)
|
|
|
|
{
|
|
|
|
formula.accept(SimplifyFormulaVisitor(), formula);
|
2017-03-16 15:45:55 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
}
|