From 6610a35bdc9877063528547a5ff2cc78dbd56ef5 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 25 Mar 2012 04:40:50 +0000
Subject: [PATCH] Utility code. When deleting duplicate rewrite rules, keep the
 instance that's verified to the highest bit-width.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1607 e59a4935-1847-0410-ae03-e826735625c1
---
 src/util/find_rewrites/Makefile         |  7 +++-
 src/util/find_rewrites/rewrite_system.h | 49 ++++++++++++++++++++++++-
 2 files changed, 54 insertions(+), 2 deletions(-)

diff --git a/src/util/find_rewrites/Makefile b/src/util/find_rewrites/Makefile
index 49a3dfe..4b02622 100644
--- a/src/util/find_rewrites/Makefile
+++ b/src/util/find_rewrites/Makefile
@@ -7,8 +7,12 @@ CXXFLAGS += -L../../../lib/
 
 .PHONY: clean
 
+rr.a: $(OBJS)
+	$(RM) $@
+	$(AR) qcs $@ $^
+
 rewrite: $(OBJS)  $(TOP)lib/libstp.a  
-	$(CXX)   $(CXXFLAGS) $@.o -o $@ -lstp #--static
+	$(CXX)   $(CXXFLAGS) $@.o -o $@ -lstp --static
 
 rewrite.o: rewrite.cpp Functionlist.h  rewrite_rule.h  rewrite_system.h  VariableAssignment.h
 	$(CXX)   $(CXXFLAGS) rewrite.cpp -c 
@@ -19,3 +23,4 @@ clean:
 upload: rewrite
 	strip ./rewrite
 	scp -C ./rewrite rimmer.csse.unimelb.edu.au:/home/pgrad/thansen
+	scp -C rules_new.smt2 rimmer.csse.unimelb.edu.au:/home/pgrad/thansen
diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h
index 24d3076..91e6d7c 100644
--- a/src/util/find_rewrites/rewrite_system.h
+++ b/src/util/find_rewrites/rewrite_system.h
@@ -136,11 +136,57 @@ public:
     lookups_invalid = false;
   }
 
+  // Remove syntactically the same rewrite rules. Remove the rule verified to a lower level.
   void
   eraseDuplicates()
   {
     toWrite.sort();
-    toWrite.unique();
+    for (RewriteRuleContainer::iterator it = toWrite.begin(); it != toWrite.end(); )
+      {
+        RewriteRuleContainer::iterator next = it;
+        next++;
+        if (next == toWrite.end())
+          {
+            it++;
+            continue;
+          }
+
+        if (*next == *it)
+          {
+             // The same, erase the one with the lowest verified to bits.
+            bool output =false;
+            if (next->getVerifiedToBits() != it->getVerifiedToBits())
+              output=true;
+
+            if (next->getVerifiedToBits() > it->getVerifiedToBits())
+              {
+                if (output)
+                  {
+                    cerr << "deleting";
+                    it->writeOut(cerr);
+                    next->writeOut(cerr);
+                    cerr << "====";
+                  }
+                erase(it);
+                it = next;
+                continue;
+              }
+            else
+              {
+                if (output)
+                  {
+                    cerr << "deleting";
+                    next->writeOut(cerr);
+                    it->writeOut(cerr);
+                    cerr << "====";
+                  }
+                erase(next);
+                continue;
+              }
+          }
+        it++;
+      }
+
     lookups_invalid = true;
   }
 
@@ -172,6 +218,7 @@ public:
     return rename_then_rewrite(n, Rewrite_rule::getNullRule());
   }
 
+
   void
   rewriteAll()
   {
-- 
2.47.3