From b161df1e488136cb5110a3cdc162b1899126695a Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 18 Mar 2012 05:53:52 +0000
Subject: [PATCH] Improvement to the utility code for building rewrites.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1600 e59a4935-1847-0410-ae03-e826735625c1
---
 src/util/find_rewrites/rewrite.cpp    | 37 ++++++++++++++++++++-------
 src/util/find_rewrites/rewrite_rule.h | 14 +++++-----
 2 files changed, 34 insertions(+), 17 deletions(-)

diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp
index ba8fd19..4ef1670 100644
--- a/src/util/find_rewrites/rewrite.cpp
+++ b/src/util/find_rewrites/rewrite.cpp
@@ -702,6 +702,7 @@ doIte(ASTNode a)
 void
 do_write_out(int ignore)
 {
+  difficulty_cache.clear();
   force_writeout = true;
 }
 
@@ -927,9 +928,12 @@ findRewrites(ASTVec& expressions, const vector<VariableAssignment>& values, cons
 
   if (values.size() > 0)
     {
-      if (values.size() > 10)
+      const int old_size = values.size();
+      if (old_size > 10)
         removeDuplicates(expressions);
 
+      discarded += (old_size - values.size());
+
       // Put the functions in buckets based on their results on the values.
       HASHMAP<uint64_t, ASTVec> map;
       for (int i = 0; i < expressions.size(); i++)
@@ -1020,17 +1024,30 @@ findRewrites(ASTVec& expressions, const vector<VariableAssignment>& values, cons
               if (!r)
                 continue;
 
-              cout << "Discovered a new rule.";
-              cout << f << t;
-              cout << getDifficulty(f) << " to " << getDifficulty(t) << endl;
-
               Rewrite_rule rr(mgr, f, t, checktime);
 
-              if (!rr.timedCheck(10000))
+              VariableAssignment bad;
+              if (!rr.timedCheck(10000,bad))
                 {
+                  vector<VariableAssignment> ass;
+                  ass.push_back(bad);
+
                   cout << "Rule failed extended verification.";
-                  continue;
+
+                  // If it can fit into an unsigned. Split the list on it.
+                  if (sizeof(unsigned int) * 8 > bad.getV().GetValueWidth())
+                    {
+                      findRewrites(equiv, ass, depth + 1);
+                      return;
+                    }
+                  else
+                    continue;
                 }
+
+              cout << "Discovered a new rule.";
+              cout << f << t;
+              cout << getDifficulty(f) << " to " << getDifficulty(t) << endl;
+
               cout << "Verified Rule to: " << rr.getVerifiedToBits() << " bits" << endl;
               cout << "------";
 
@@ -1040,10 +1057,11 @@ findRewrites(ASTVec& expressions, const vector<VariableAssignment>& values, cons
               // Sometimes it doesn't. Not sure why..
               assert(t == rewrite_system.rewriteNode(f));
 
-
               equiv[i] = rewrite_system.rewriteNode(equiv[i]);
               equiv[j] = rewrite_system.rewriteNode(equiv[j]);
 
+              if (equiv[i] == equiv[j])
+                equiv[j]= mgr->ASTUndefined;
             }
           else if (!bad)
             {
@@ -1856,7 +1874,8 @@ expandRules(int timeout_ms, const char* fileName = "")
 
   for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.begin(); it != rewrite_system.end(); it++)
     {
-      if ((*it).timedCheck(timeout_ms))
+      VariableAssignment bad;
+      if ((*it).timedCheck(timeout_ms,bad))
         {
           it->writeOut(cout); // omit failed.
           cerr << getDifficulty(it->getFrom()) << " " << getDifficulty(it->getTo());
diff --git a/src/util/find_rewrites/rewrite_rule.h b/src/util/find_rewrites/rewrite_rule.h
index 44a9eb7..6508cbc 100644
--- a/src/util/find_rewrites/rewrite_rule.h
+++ b/src/util/find_rewrites/rewrite_rule.h
@@ -136,10 +136,8 @@ public:
 
   // Tests for the timeout amount of time. FALSE if a bad instance was found. Otherwise true.
   bool
-  timedCheck(int timeout_ms)
+  timedCheck(int timeout_ms, VariableAssignment& bad)
   {
-    VariableAssignment assignment;
-
     mgr->soft_timeout_expired = false;
     itimerval timeout;
     signal(SIGVTALRM, soft_time_out);
@@ -153,7 +151,7 @@ public:
     int checked_to = 0;
 
     // Start it verifying where we left off..
-    for (int i = std::max(bits, getVerifiedToBits() + 1); i < 1024; i++)
+    for (int new_bitwidth = std::max(bits, getVerifiedToBits() + 1); new_bitwidth < 1024; new_bitwidth++)
       {
         //cout << i << " ";
         ASTVec children;
@@ -161,18 +159,18 @@ public:
         children.push_back(to);
 
         const ASTNode n = mgr->hashingNodeFactory->CreateNode(EQ, children);
-        const ASTNode& widened = widen(n, i);
+        const ASTNode& widened = widen(n, new_bitwidth);
         if (widened == mgr->ASTUndefined)
           {
             cout << "cannot widen";
             cerr << from << to;
           }
 
-        bool result = isConstant(widened, assignment, i);
+        bool result = isConstant(widened, bad, new_bitwidth);
         if (!result && !mgr->soft_timeout_expired)
           {
             // not a constant, and not timed out!
-            cerr << "FAILED:" << endl << i << from << to;
+            cerr << "FAILED:" << endl << new_bitwidth << from << to;
             writeOut(cerr);
 
             // The timer might not have expired yet.
@@ -183,7 +181,7 @@ public:
         if (mgr->soft_timeout_expired)
           break;
 
-        checked_to = i;
+        checked_to = new_bitwidth;
       }
 
     if (getVerifiedToBits() <= checked_to)
-- 
2.47.3