diff --git a/include/anthem/AST.h b/include/anthem/AST.h index 9c30c0e..e5f3390 100644 --- a/include/anthem/AST.h +++ b/include/anthem/AST.h @@ -2,6 +2,7 @@ #define __ANTHEM__AST_H #include +#include namespace anthem { diff --git a/include/anthem/Equality.h b/include/anthem/Equality.h index ada8a6c..0e8ac51 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/Tristate.h b/include/anthem/Tristate.h new file mode 100644 index 0000000..dfafcba --- /dev/null +++ b/include/anthem/Tristate.h @@ -0,0 +1,24 @@ +#ifndef __ANTHEM__TRISTATE_H +#define __ANTHEM__TRISTATE_H + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Tristate +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +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())