Improvement to utility code. Replace directly accessing arrays with iterators.

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

diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp
index 1b139fa0cf38765073e340af60f5062c0d6f2432..8572082480c242424ec08198a87f3977be85bcd3 100644 (file)
--- a/src/util/find_rewrites/rewrite.cpp
+++ b/src/util/find_rewrites/rewrite.cpp
@@ -1242,17 +1242,16 @@ writeOutRules(string fileName)
   std::vector<string> output;
   std::map<string, Rewrite_rule> dup;
 
-  for (int i = 0; i < to_write.size(); i++)
+  for (Rewrite_system::RewriteRuleContainer::iterator it = to_write.toWrite.begin() ; it != to_write.toWrite.end(); it++)
     {
-      if (!to_write.toWrite[i].isOK())
+      if (!it->isOK())
         {
-          to_write.toWrite.erase(to_write.toWrite.begin() + i);
-          i--;
+          to_write.toWrite.erase(it--);
           continue;
         }
 
-      ASTNode to = to_write.toWrite[i].getTo();
-      ASTNode from = to_write.toWrite[i].getFrom();
+      ASTNode to = it->getTo();
+      ASTNode from = it->getFrom();
 
       // If the RHS is just part of the LHS, then we output something like children[0][1][0][1] as the RHS.
       string to_name = getToName(to, from);
@@ -1299,7 +1298,7 @@ writeOutRules(string fileName)
                   cerr << "-----";
                   cerr << sofar;
 
-                  ASTNode f = to_write.toWrite[i].getFrom();
+                  ASTNode f = it->getFrom();
                   cerr << f << std::endl;
                   cerr << dup.find(sofar)->second.getFrom();
 
@@ -1310,15 +1309,14 @@ writeOutRules(string fileName)
                   bool result = unifyNode(f,dup.find(sofar)->second.getFrom(),fromTo,2) ;
                   cerr << "unified" << result << endl;
                   ASTNodeMap seen;
-                  cerr << rewrite(f,to_write.toWrite[i],seen );
+                  cerr << rewrite(f,*it,seen );
 
                   // The text of this rule is the same as another rule.
-                  to_write.toWrite.erase(to_write.toWrite.begin() + i);
-                  i--;
+                  to_write.toWrite.erase(it--);
                   continue;
                 }
               else
-                dup.insert(make_pair(sofar,to_write.toWrite[i]));
+                dup.insert(make_pair(sofar,*it));
             }
         }
     }
@@ -1352,15 +1350,16 @@ writeOutRules(string fileName)
   ofstream outputFileSMT2;
   outputFileSMT2.open("rewrite_data.smt2", ios::trunc);
 
-  for (int i = 0; i < to_write.size(); i++)
+  for (Rewrite_system::RewriteRuleContainer::iterator it = to_write.toWrite.begin() ; it != to_write.toWrite.end(); it++)
     {
-      assert(to_write.toWrite[i].isOK());
-      outputFileSMT2 << ";  " << "bits:" << bits << "->" << widen_to << " time to verify:" << to_write.toWrite[i].getTime()
+      assert(it->isOK());
+      outputFileSMT2 << ";  " << "bits:" << bits << "->" << widen_to << " time to verify:" << it->getTime()
           << '\n';
       for (int j = widen_to; j < widen_to + 5; j++)
         {
+          ASTNode widened = widen(it->getN(),j);
           outputFileSMT2 << "(push 1)\n";
-          printer::SMTLIB2_PrintBack(outputFileSMT2, mgr->CreateNode(NOT, w), true, false);
+          printer::SMTLIB2_PrintBack(outputFileSMT2, mgr->CreateNode(NOT, widened), true, false);
           outputFileSMT2 << "(pop 1)\n";
         }
     }
@@ -1369,9 +1368,9 @@ writeOutRules(string fileName)
 
   outputFileSMT2.open(fileName.c_str(), ios::trunc);
   ASTVec v;
-  for (int i = 0; i < to_write.size(); i++)
+  for (Rewrite_system::RewriteRuleContainer::iterator it = to_write.toWrite.begin() ; it != to_write.toWrite.end(); it++)
     {
-      v.push_back(to_write.toWrite[i].getN());
+      v.push_back(it->getN());
     }
 
   if (v.size() > 0)

diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h
index a9785f25246295666f7d5a8a55c3f1684cfb3b5f..220aefa813ca99e1dd55a973218f93163e690abc 100644 (file)
--- a/src/util/find_rewrites/rewrite_system.h
+++ b/src/util/find_rewrites/rewrite_system.h
@@ -53,7 +53,9 @@ private:
   friend ASTNode  rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen);
 
   // Rules to write out when we get the chance.
-  vector<Rewrite_rule> toWrite;
+  typedef list<Rewrite_rule> RewriteRuleContainer;
+
+  RewriteRuleContainer toWrite;
   std::map< Kind, vector<Rewrite_rule> > kind_to_rr;
   std::map< Kind, std::map< Kind, vector<Rewrite_rule> > > kind_kind_to_rr;
 
@@ -69,20 +71,21 @@ public:
     kind_to_rr.clear();
     kind_kind_to_rr.clear();
 
-    for (int i = 0; i < toWrite.size(); i++)
+    for (RewriteRuleContainer::iterator it = toWrite.begin() ; it != toWrite.end(); it++)
       {
-        ASTNode from = toWrite[i].getFrom();
-        kind_to_rr[from.GetKind()].push_back(toWrite[i]);
+        ASTNode from = it->getFrom();
+        kind_to_rr[from.GetKind()].push_back(*it);
 
         if (from[0].Degree() > 0)
-          kind_kind_to_rr[from.GetKind()][from[0].GetKind()].push_back(toWrite[i]);
+          kind_kind_to_rr[from.GetKind()][from[0].GetKind()].push_back(*it);
       }
   }
 
   void
   eraseDuplicates()
   {
-    removeDuplicates(toWrite);
+    toWrite.sort();
+    toWrite.unique();
   }
 
   void
@@ -111,43 +114,41 @@ public:
 
     buildRules();
 
-    for (int i = 0; i < toWrite.size(); i++)
+    int i=0;
+    for (RewriteRuleContainer::iterator it = toWrite.begin() ; it != toWrite.end(); it++, i++)
       {
         if (i % 1000 == 0)
           cerr << "rewrite all:" << i << " of " << toWrite.size() << endl;
 
-        if (!toWrite[i].isOK())
+        if (!it->isOK())
           {
-            toWrite.erase(toWrite.begin() + i);
-            i--;
+            toWrite.erase(it--);
             continue;
           }
 
-        ASTNode n = renameVars(toWrite[i].getFrom());
+        ASTNode n = renameVars(it->getFrom());
         ASTNodeMap seen;
-        ASTNode rewritten_from = rewrite(n, toWrite[i],seen);
+        ASTNode rewritten_from = rewrite(n, *it,seen);
 
         if (n != rewritten_from)
           {
             assert (isConstantToSat(create(EQ, rewritten_from,n)));
 
             rewritten_from = renameVarsBack(rewritten_from);
-            ASTNode to = toWrite[i].getTo();
+            ASTNode to = it->getTo();
             bool r = orderEquivalence(rewritten_from, to);
             if (r)
               {
                 Rewrite_rule rr(mgr, rewritten_from, to, 0);
                 if (rr.isOK())
                   {
-                    toWrite[i] = rr;
+                    *it= rr;
                     buildRules(); // Otherwise two rules will remove each other?
                   }
                 else
                   {
                     cout << "Erasing rule";
-                    toWrite.erase(toWrite.begin() + i);
-                    i--;
-                  }
+                    toWrite.erase(it--);                  }
               }
             else
               {
@@ -169,21 +170,21 @@ public:
   void
   verifyAllwithSAT()
   {
-    for (int i = 0; i < toWrite.size(); i++)
+    for (RewriteRuleContainer::iterator it = toWrite.begin() ; it != toWrite.end(); it++)
       {
         VariableAssignment assignment;
         bool bad = false;
         const int st = getCurrentTime();
-        bool r = checkRule(toWrite[i].getFrom(), toWrite[i].getTo(), assignment, bad);
+        bool r = checkRule(it->getFrom(), it->getTo(), assignment, bad);
         if (!r || bad)
           {
             cerr << "Bad to, then from" << endl;
-            cerr << toWrite[i].getFrom();
-            cerr << toWrite[i].getTo();
+            cerr << it->getFrom();
+            cerr << it->getTo();
             assert(r);
             assert(!bad);
           }
-        toWrite[i].time = getCurrentTime() - st;
+        it->time = getCurrentTime() - st;
       }
   }
 };