From 91814ad9a38a58da8b1d32d007ba47558d578d5a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 3 Mar 2012 01:56:43 +0000 Subject: [PATCH] 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 --- src/util/find_rewrites/rewrite.cpp | 33 +++++++++--------- src/util/find_rewrites/rewrite_system.h | 45 +++++++++++++------------ 2 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp index 1b139fa..8572082 100644 --- a/src/util/find_rewrites/rewrite.cpp +++ b/src/util/find_rewrites/rewrite.cpp @@ -1242,17 +1242,16 @@ writeOutRules(string fileName) std::vector output; std::map 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 a9785f2..220aefa 100644 --- 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 toWrite; + typedef list RewriteRuleContainer; + + RewriteRuleContainer toWrite; std::map< Kind, vector > kind_to_rr; std::map< Kind, std::map< Kind, vector > > 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; } } }; -- 2.47.3