From 3013f745d3fde8363ff9781817767db6926686ee Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 20 Dec 2011 00:30:14 +0000
Subject: [PATCH] Improvement. A better type for the polarities of the pure
 literal elimination.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1436 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/FindPureLiterals.h | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/simplifier/FindPureLiterals.h b/src/simplifier/FindPureLiterals.h
index d5c19cb..1036dfc 100644
--- a/src/simplifier/FindPureLiterals.h
+++ b/src/simplifier/FindPureLiterals.h
@@ -27,13 +27,14 @@ namespace BEEV
 
 class FindPureLiterals
 {
-  const static int truePolarity = 1;
-  const static int falsePolarity = 2;
-  const static int bothPolarity = 3;
+  typedef char polarity_type;
+  const static polarity_type truePolarity = 1;
+  const static polarity_type falsePolarity = 2;
+  const static polarity_type bothPolarity = 3;
 
-  map<ASTNode, int> nodeToPolarity;
+  map<ASTNode, polarity_type> nodeToPolarity;
 
-  int swap(int polarity)
+  int swap(polarity_type polarity)
   {
     if (polarity == truePolarity)
       return falsePolarity;
@@ -62,11 +63,11 @@ public:
     build(n , truePolarity);
     bool changed = false;
 
-    map<ASTNode, int>::const_iterator it = nodeToPolarity.begin();
+    map<ASTNode, polarity_type>::const_iterator it = nodeToPolarity.begin();
     while (it != nodeToPolarity.end())
       {
         const ASTNode& n = it->first;
-        const int polarity = it->second;
+        const polarity_type polarity = it->second;
         if (n.GetType() == BOOLEAN_TYPE && n.GetKind() == SYMBOL && polarity != bothPolarity)
           {
               if (polarity == truePolarity)
@@ -85,12 +86,12 @@ public:
   }
 
 
-  void build(const ASTNode& n , int polarity)
+  void build(const ASTNode& n , polarity_type polarity)
   {
     if (n.isConstant())
       return;
 
-    map<ASTNode, int>::iterator it = nodeToPolarity.find(n);
+    map<ASTNode, polarity_type>::iterator it = nodeToPolarity.find(n);
     if (it != nodeToPolarity.end())
       {
         int lookupPolarity = it->second;
-- 
2.47.3