From d2b48f967914994cfce720b13df32f1d5a513fed Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Thu, 19 Apr 2018 14:41:49 +0200
Subject: [PATCH] Move Tristate class to separate header

The Tristate class (representing truth values that are either true,
false, or unknown) is used at multiple ends. This moves it to a separate
header for reusing it properly.
---
 include/anthem/AST.h          |  1 +
 include/anthem/Equality.h     | 11 +----------
 include/anthem/Tristate.h     | 24 ++++++++++++++++++++++++
 src/anthem/Simplification.cpp |  2 +-
 4 files changed, 27 insertions(+), 11 deletions(-)
 create mode 100644 include/anthem/Tristate.h

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 <anthem/ASTForward.h>
+#include <anthem/Tristate.h>
 
 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 <anthem/AST.h>
 #include <anthem/ASTUtils.h>
+#include <anthem/Tristate.h>
 
 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())