diff --git a/include/anthem/Equality.h b/include/anthem/Equality.h index 683bef6..64d16e5 100644 --- a/include/anthem/Equality.h +++ b/include/anthem/Equality.h @@ -3,6 +3,7 @@ #include #include +#include namespace anthem { @@ -15,16 +16,6 @@ namespace ast // //////////////////////////////////////////////////////////////////////////////////////////////////// -// 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); diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h index 660597b..161ed92 100644 --- a/include/anthem/Utils.h +++ b/include/anthem/Utils.h @@ -23,6 +23,15 @@ constexpr const auto UserVariablePrefix = "U"; //////////////////////////////////////////////////////////////////////////////////////////////////// +enum class Tristate +{ + True, + False, + Unknown, +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + } #endif diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index 1774504..4b6d149 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -363,7 +363,7 @@ struct SimplificationRuleSubsumptionInBiconditionals std::find_if(and_.arguments.cbegin(), and_.arguments.cend(), [&](const auto &argument) { - return (ast::equal(predicateSide, argument) == ast::Tristate::True); + return (ast::equal(predicateSide, argument) == Tristate::True); }); if (matchingPredicate == and_.arguments.cend())