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 001d9c2a3623e19fb5edeed0e1065275dc15416d..085491edb2238fdd41e28f17eb2afc7e8b482095 100644 (file)
--- 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 91e6d7cd11c1073d900fe8a348f609dc5427e237..50439912abaca47d2002782202c5502a286f9e93 100644 (file)
--- 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;
               }