patrick/anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity

Add integer simplification rule

Browse Source 
This adds the rule “(F in G) === (F = G) if F and G are integer
variables” to the simplification rule tableau
This commit is contained in:
Patrick Lühne 2018-04-21 18:12:43 +02:00
parent a70b1fb726
commit 69688d1d39
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 31 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
src/anthem/Simplification.cpp
View File

@ -5,6 +5,7 @@
#include <anthem/ASTCopy.h>
#include <anthem/Equality.h>
#include <anthem/SimplificationVisitors.h>
#include <anthem/Type.h>
#include <anthem/output/AST.h>
namespace anthem
@ -512,6 +513,34 @@ struct SimplificationRuleNegatedComparison
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleIntegerSetInclusion
{
static constexpr const auto Description = "(F in G) === (F = G) if F and G are integer variables";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::In>())
return OperationResult::Unchanged;
auto &in = formula.get<ast::In>();
const auto elementType = type(in.element);
const auto setType = type(in.set);
if (elementType.domain != Domain::Integer || setType.domain != Domain::Integer
|| elementType.setSize != SetSize::Unit || setType.setSize != SetSize::Unit)
{
return OperationResult::Unchanged;
}
formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
const auto simplifyWithDefaultRules =
simplify
<
@ -526,7 +555,8 @@ const auto simplifyWithDefaultRules =
SimplificationRuleSubsumptionInBiconditionals,
SimplificationRuleDeMorganForConjunctions,
SimplificationRuleImplicationFromDisjunction,
SimplificationRuleNegatedComparison
SimplificationRuleNegatedComparison,
SimplificationRuleIntegerSetInclusion
>;
////////////////////////////////////////////////////////////////////////////////////////////////////