diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index 29eeb5d..2f2ab52 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -317,6 +317,30 @@ struct SimplificationRuleTrivialExists //////////////////////////////////////////////////////////////////////////////////////////////////// +struct SimplificationRuleInWithPrimitiveArguments +{ + static constexpr const auto Description = "[primitive A] in [primitive B] === A = B"; + + static SimplificationResult apply(ast::Formula &formula) + { + if (!formula.is()) + return SimplificationResult::Unchanged; + + auto &in = formula.get(); + + 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; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + void simplify(ast::Exists &exists, ast::Formula &formula) { SimplificationRuleTrivialAssignmentInExists::apply(formula); @@ -341,14 +365,9 @@ struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor