From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 25 Mar 2012 23:20:58 +0000 (+0000)
Subject: Improvements to utility code. Less outputting to cerr, different semantics for expand.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=96647fada49ed60ec99da0d90e9925cfb89bb97c;p=francis%2Fstp.git

Improvements to utility code. Less outputting to cerr, different semantics for expand.

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

diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp
index 001d9c2..085491e 100644
--- a/src/util/find_rewrites/rewrite.cpp
+++ b/src/util/find_rewrites/rewrite.cpp
@@ -1911,10 +1911,12 @@ expandRules(int timeout_ms, const char* fileName = "")
   for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.begin(); it != rewrite_system.end(); it++)
     {
       VariableAssignment bad;
-      if ((*it).timedCheck(timeout_ms,bad))
+      int to_run = timeout_ms - it->getTime();
+      if (to_run <= 0)
+        continue;
+      if ((*it).timedCheck(to_run,bad))
         {
-          it->writeOut(cout); // omit failed.
-          cerr << getDifficulty(it->getFrom()) << " " << getDifficulty(it->getTo());
+          it->writeOut(cout); // omit succeeded.
         }
     }
 }
diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h
index 91e6d7c..5043991 100644
--- a/src/util/find_rewrites/rewrite_system.h
+++ b/src/util/find_rewrites/rewrite_system.h
@@ -154,32 +154,14 @@ public:
         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;
               }