Utility code. When deleting duplicate rewrite rules, keep the instance that's verifie...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1607 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/util/find_rewrites/Makefile b/src/util/find_rewrites/Makefile
index 49a3dfe631bc3d9b2c3adb8c9c55f77a8af226bb..4b0262223f47d86f0ab857186b29355e740e8eae 100644 (file)
--- 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 24d30768bc3e78c46a068f837d6dd01bcab01af2..91e6d7cd11c1073d900fe8a348f609dc5427e237 100644 (file)
--- 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()
   {