From 41349487350e2c7e71872e3da6a820126ebcd2b4 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 14 Mar 2012 14:12:39 +0000 Subject: [PATCH] Refactor utility code. Automatically layout, no other changes. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1594 e59a4935-1847-0410-ae03-e826735625c1 --- src/util/find_rewrites/Functionlist.h | 21 +- src/util/find_rewrites/VariableAssignment.h | 4 +- src/util/find_rewrites/misc.h | 30 +- src/util/find_rewrites/rewrite.cpp | 471 ++++++++++---------- src/util/find_rewrites/rewrite_rule.h | 108 ++--- src/util/find_rewrites/rewrite_system.h | 68 +-- 6 files changed, 346 insertions(+), 356 deletions(-) diff --git a/src/util/find_rewrites/Functionlist.h b/src/util/find_rewrites/Functionlist.h index 5ebbea8..ed1f3bd 100644 --- a/src/util/find_rewrites/Functionlist.h +++ b/src/util/find_rewrites/Functionlist.h @@ -10,11 +10,9 @@ extern Rewrite_system rewrite_system; - class Function_list { - private: - +private: // Because v and w might come from "result", if "result" is resized, they will // be moved. So we can't use references to them. @@ -22,8 +20,8 @@ class Function_list getAllFunctions(const ASTNode v, const ASTNode w, ASTVec& result) { - Kind types[] = {BVXOR, BVAND}; - + Kind types[] = + { BVXOR, BVAND }; //Kind types[] = {BVMULT, BVDIV, SBVDIV, SBVREM, SBVMOD, BVPLUS, BVMOD, BVRIGHTSHIFT, BVLEFTSHIFT, BVOR, BVAND, BVXOR, BVSRSHIFT}; const int number_types = sizeof(types) / sizeof(Kind); @@ -37,7 +35,7 @@ class Function_list applyRewritesToAll(ASTVec& functions) { rewrite_system.buildLookupTable(); - cerr << "Applying:" << rewrite_system.size() <<"rewrite rules" << endl; + cerr << "Applying:" << rewrite_system.size() << "rewrite rules" << endl; for (int i = 0; i < functions.size(); i++) { @@ -48,16 +46,15 @@ class Function_list cerr << "applyRewritesToAll:" << i << " of " << functions.size() << endl; ASTNode r = rewrite_system.rewriteNode(functions[i]); - if (r!= functions[i]) + if (r != functions[i]) { - // cerr << "changed" << functions[i] << " to "<< r; + // cerr << "changed" << functions[i] << " to "<< r; - functions[i] =r; + functions[i] = r; } } } - // If there only w variables in the problem. We can delete it because // we will have another with just v's. // NB: Can only apply at the top level. @@ -138,7 +135,6 @@ class Function_list } } - // Triples the number of functions by adding all the unary ones. void allUnary() @@ -153,7 +149,6 @@ class Function_list } } - void applyAIGs() { @@ -208,7 +203,7 @@ public: cerr << "One Level:" << functions.size() << endl; - const bool two_level = true; + const bool two_level = true; if (two_level) { diff --git a/src/util/find_rewrites/VariableAssignment.h b/src/util/find_rewrites/VariableAssignment.h index 167b655..34b6f6a 100644 --- a/src/util/find_rewrites/VariableAssignment.h +++ b/src/util/find_rewrites/VariableAssignment.h @@ -6,11 +6,10 @@ #ifndef VARIABLEASSIGNMENT_H_ #define VARIABLEASSIGNMENT_H_ -extern ASTNode v, v0, w ,w0; +extern ASTNode v, v0, w, w0; extern NodeFactory* nf; extern BEEV::STPMgr* mgr; - struct VariableAssignment { private: @@ -72,5 +71,4 @@ public: } }; - #endif /* VARIABLEASSIGNMENT_H_ */ diff --git a/src/util/find_rewrites/misc.h b/src/util/find_rewrites/misc.h index f9cbeb6..b5ee07f 100644 --- a/src/util/find_rewrites/misc.h +++ b/src/util/find_rewrites/misc.h @@ -1,27 +1,27 @@ #ifndef MISC_H #define MISC_H - extern const int bits; - extern const int widen_to; +extern const int bits; +extern const int widen_to; - extern Simplifier *simp; +extern Simplifier *simp; - ASTNode - widen(const ASTNode& w, int width); +ASTNode +widen(const ASTNode& w, int width); - ASTNode - create(Kind k, const ASTNode& n0, const ASTNode& n1); +ASTNode +create(Kind k, const ASTNode& n0, const ASTNode& n1); - int - getDifficulty(const ASTNode& n_); +int +getDifficulty(const ASTNode& n_); - bool - isConstant(const ASTNode& n, VariableAssignment& different, const int bits); +bool +isConstant(const ASTNode& n, VariableAssignment& different, const int bits); - vector - getVariables(const ASTNode& n); +vector +getVariables(const ASTNode& n); - ASTNode - rewriteThroughWithAIGS(const ASTNode &n_); +ASTNode +rewriteThroughWithAIGS(const ASTNode &n_); #endif diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp index 2da4758..97bc2cb 100644 --- a/src/util/find_rewrites/rewrite.cpp +++ b/src/util/find_rewrites/rewrite.cpp @@ -64,7 +64,6 @@ clearSAT(); bool is_subgraph(const ASTNode& g, const ASTNode& h); - void createVariables(); @@ -91,7 +90,7 @@ vector getVariables(const ASTNode& n); bool -matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width); +matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width); typedef HASHMAP ASTNodeString; @@ -107,7 +106,6 @@ ASTNode zero, one, maxNode, v, w, v0, w0; // Width of the rewrite rules that were output last time. int lastOutput = 0; - bool checkRule(const ASTNode & from, const ASTNode & to, VariableAssignment& ass, bool& bad); @@ -118,7 +116,7 @@ withNF(const ASTNode &n) return n; ASTVec c; - for (int i=0; i< n.Degree();i++) + for (int i = 0; i < n.Degree(); i++) c.push_back(withNF(n[i])); if (n.GetType() == BOOLEAN_TYPE) @@ -127,7 +125,6 @@ withNF(const ASTNode &n) return nf->CreateArrayTerm(n.GetKind(), n.GetIndexWidth(), n.GetValueWidth(), c); } - ASTNode renameVars(const ASTNode &n) { @@ -158,7 +155,6 @@ renameVarsBack(const ASTNode &n) return SubstitutionMap::replace(n, ft, cache, nf); } - // Helper functions. Don't need to specify the width. ASTNode create(Kind k, const ASTNode& n0, const ASTNode& n1) @@ -325,9 +321,9 @@ isConstant(const ASTNode& n, VariableAssignment& different, const int bits) for (int i = 0; i < symbols.size(); i++) { if (strncmp(symbols[i].GetName(), "v", 1) == 0) - different.setV(GlobalSTP->Ctr_Example->GetCounterExample(true, symbols[i])); + different.setV(GlobalSTP->Ctr_Example->GetCounterExample(true, symbols[i])); else if (strncmp(symbols[i].GetName(), "w", 1) == 0) - different.setW(GlobalSTP->Ctr_Example->GetCounterExample(true, symbols[i])); + different.setW(GlobalSTP->Ctr_Example->GetCounterExample(true, symbols[i])); } return false; } @@ -344,14 +340,14 @@ widen(const ASTNode& w, int width) if (w.isConstant() && w.GetValueWidth() == bits) { - ASTNode width_n = mgr->CreateBVConst(32,width); - return nf->CreateTerm(BVSX, width, w,width_n); + ASTNode width_n = mgr->CreateBVConst(32, width); + return nf->CreateTerm(BVSX, width, w, width_n); } if (w.isConstant() && w.GetValueWidth() == bits - 1) { - ASTNode width_n = mgr->CreateBVConst(32,width-1); - return nf->CreateTerm(BVSX, width-1, w,width_n); + ASTNode width_n = mgr->CreateBVConst(32, width - 1); + return nf->CreateTerm(BVSX, width - 1, w, width_n); } if (w.isConstant() && w.GetValueWidth() == 32) // Extract DEFINATELY. @@ -433,13 +429,13 @@ widen(const ASTNode& w, int width) bool orderEquivalence(ASTNode& from, ASTNode& to) { - if(from.IsNull()) + if (from.IsNull()) return false; - if(from.GetKind() == UNDEFINED) + if (from.GetKind() == UNDEFINED) return false; - if(to.IsNull()) + if (to.IsNull()) return false; - if(to.GetKind() == UNDEFINED) + if (to.GetKind() == UNDEFINED) return false; if (from == to) @@ -448,7 +444,7 @@ orderEquivalence(ASTNode& from, ASTNode& to) if (from.isConstant()) { assert(!to.isConstant()); - swap(from,to); + swap(from, to); return true; } @@ -458,42 +454,41 @@ orderEquivalence(ASTNode& from, ASTNode& to) return true; } - if (is_subgraph(to,from)) + if (is_subgraph(to, from)) { return true; } - if (is_subgraph(from,to)) + if (is_subgraph(from, to)) { - swap(from,to); + swap(from, to); return true; } return false; } - bool orderEquivalence_not_yet(ASTNode& from, ASTNode& to) { - if(from.IsNull()) + if (from.IsNull()) return false; - if(from.GetKind() == UNDEFINED) + if (from.GetKind() == UNDEFINED) return false; - if(to.IsNull()) + if (to.IsNull()) return false; - if(to.GetKind() == UNDEFINED) + if (to.GetKind() == UNDEFINED) return false; - { - ASTVec c; - c.push_back(from); - c.push_back(to); - ASTNode w = widen(mgr->hashingNodeFactory->CreateNode(EQ,c), widen_to); + { + ASTVec c; + c.push_back(from); + c.push_back(to); + ASTNode w = widen(mgr->hashingNodeFactory->CreateNode(EQ, c), widen_to); - if (w.IsNull() || w.GetKind() == UNDEFINED) - return false; - } + if (w.IsNull() || w.GetKind() == UNDEFINED) + return false; + } vector s_from; // The variables in the from node. ASTNodeSet visited; @@ -501,7 +496,7 @@ orderEquivalence_not_yet(ASTNode& from, ASTNode& to) std::sort(s_from.begin(), s_from.end()); const int from_c = visited.size(); - vector s_to; // The variables in the to node. + vector s_to; // The variables in the to node. visited.clear(); getVariables(to, s_to, visited); sort(s_to.begin(), s_to.end()); @@ -555,13 +550,13 @@ orderEquivalence_not_yet(ASTNode& from, ASTNode& to) if (s_from.size() > s_to.size()) return true; - if ((getDifficulty(from)+5) < getDifficulty(to)) + if ((getDifficulty(from) + 5) < getDifficulty(to)) { swap(from, to); return true; } - if (getDifficulty(from) > (getDifficulty(to)+5)) + if (getDifficulty(from) > (getDifficulty(to) + 5)) { return true; } @@ -577,8 +572,6 @@ orderEquivalence_not_yet(ASTNode& from, ASTNode& to) return true; } - - // Can't order they have the same number of nodes and the same AIG size. return false; } @@ -620,27 +613,27 @@ getDifficulty(const ASTNode& n_) // Create a new sat variable for each of the variables in the CNF. assert(ss->nVars() ==0); - for (int i = 0; i < cnfData->nVars ; i++) + for (int i = 0; i < cnfData->nVars; i++) ss->newVar(); SATSolver::vec_literals satSolverClause; for (int i = 0; i < cnfData->nClauses; i++) { satSolverClause.clear(); - for (int * pLit = cnfData->pClauses[i], *pStop = cnfData->pClauses[i - + 1]; pLit < pStop; pLit++) + for (int * pLit = cnfData->pClauses[i], *pStop = cnfData->pClauses[i + 1]; pLit < pStop; pLit++) { SATSolver::Var var = (*pLit) >> 1; - assert ((var < ss->nVars())); + assert((var < ss->nVars())); Minisat::Lit l = SATSolver::mkLit(var, (*pLit) & 1); satSolverClause.push(l); } ss->addClause(satSolverClause); - } + } ss->simplify(); - assert (ss->okay()); // should be satisfiable. + assert(ss->okay()); + // should be satisfiable. // Why we go to all this trouble. The number of clauses. const int score = ss->nClauses(); @@ -701,7 +694,8 @@ doIte(ASTNode a) } } -void do_write_out(int ignore) +void +do_write_out(int ignore) { force_writeout = true; } @@ -709,12 +703,12 @@ void do_write_out(int ignore) volatile bool debug_usr2 = false; //toggle. -void do_usr2(int ignore) +void +do_usr2(int ignore) { - debug_usr2=!debug_usr2; + debug_usr2 = !debug_usr2; } - int startup() { @@ -737,7 +731,7 @@ startup() GlobalSTP = new STP(mgr, simp, at, tosat, abs); - mgr->defaultNodeFactory = new SimplifyingNodeFactory (*mgr->hashingNodeFactory, *mgr); + mgr->defaultNodeFactory = new SimplifyingNodeFactory(*mgr->hashingNodeFactory, *mgr); nf = new TypeChecker(*mgr->defaultNodeFactory, *mgr); mgr->UserFlags.stats_flag = false; @@ -762,11 +756,10 @@ startup() w0 = mgr->LookupOrCreateSymbol("w0"); w0.SetValueWidth(bits); - // Write out the work so far.. - signal(SIGUSR1,do_write_out); + signal(SIGUSR1, do_write_out); - signal(SIGUSR2,do_usr2); + signal(SIGUSR2, do_usr2); } @@ -832,9 +825,9 @@ getHash(const ASTNode& n_, const vector& values) assert(symbols[j].GetValueWidth() == ass_bitwidth); if (strncmp(symbols[j].GetName(), "v", 1) == 0) - mapToVal.insert(make_pair(symbols[j], values[i].getV())); + mapToVal.insert(make_pair(symbols[j], values[i].getV())); else if (strncmp(symbols[j].GetName(), "w", 1) == 0) - mapToVal.insert(make_pair(symbols[j], values[i].getW())); + mapToVal.insert(make_pair(symbols[j], values[i].getW())); else { cerr << "Unknown symbol!" << symbols[j]; @@ -880,17 +873,15 @@ is_candidate(ASTNode from, ASTNode to) bool is_subgraph(const ASTNode& g, const ASTNode& h) { - if (g==h) + if (g == h) return true; for (int i = 0; i < h.Degree(); i++) - if (is_subgraph(g,h[i])) + if (is_subgraph(g, h[i])) return true; return false; - } - - +} bool lessThan(const ASTNode& n1, const ASTNode& n2) @@ -902,7 +893,7 @@ lessThan(const ASTNode& n1, const ASTNode& n2) return true; if (!n1_bad && n2_bad) - return false; + return false; if (n1_bad && n2_bad) return false; @@ -950,9 +941,9 @@ findRewrites(ASTVec& expressions, const vector& values, cons cout << "Split into " << map.size() << " pieces\n"; if (depth > 0) - { - assert(map.size() >0); - } + { + assert(map.size() >0); + } int id = 1; for (it2 = map.begin(); it2 != map.end(); it2++) @@ -972,7 +963,7 @@ findRewrites(ASTVec& expressions, const vector& values, cons for (int i = 0; i < equiv.size(); i++) { if (equiv[i].GetKind() == UNDEFINED) - continue; + continue; // nb. I haven't rebuilt the map, it's done by writeOutRules(). equiv[i] == rewrite_system.rewriteNode(equiv[i]); @@ -1231,7 +1222,7 @@ checkRule(const ASTNode & from, const ASTNode & to, VariableAssignment& assignme // Detected it's not a constant, or is constant FALSE. - cout << "*" << i - bits << "*"; + cout << "*" << i - bits << "*"; return false; } } @@ -1438,7 +1429,6 @@ template return ss.str(); } - /* Writes out: * rewrite_data_new.cpp: rules coded in C++. * array.cpp: rules in SMT2 in one big conjunct. @@ -1455,7 +1445,8 @@ writeOutRules() std::vector output; std::map dup; - for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin() ; it != rewrite_system.toWrite.end(); it++) + for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin(); + it != rewrite_system.toWrite.end(); it++) { ASTNode to = it->getTo(); ASTNode from = it->getFrom(); @@ -1491,7 +1482,6 @@ writeOutRules() rule_to_string(from, names, current, sofar); sofar += ") set(result, " + to_name + ");"; - // if (sofar.find("!!!") == std::string::npos && sofar.length() < 500) { { @@ -1511,7 +1501,7 @@ writeOutRules() ASTNodeMap fromTo; f = renameVars(f); - bool result = commutative_matchNode(f,dup.find(sofar)->second.getFrom(),fromTo,2) ; + bool result = commutative_matchNode(f, dup.find(sofar)->second.getFrom(), fromTo, 2); cout << "Has it unified:" << result << endl; ASTNodeMap seen; @@ -1520,7 +1510,7 @@ writeOutRules() continue; } else - dup.insert(make_pair(sofar,*it)); + dup.insert(make_pair(sofar, *it)); } } } @@ -1538,10 +1528,9 @@ writeOutRules() // Because we output the difficulty (i.e. the number of CNF clauses), // this is very slow. - #ifdef OUTPUT_CPP_RULES +#ifdef OUTPUT_CPP_RULES outputFile.open("rewrite_data_new.cpp", ios::trunc); - // output the C++ code. hash_map, hashF >::const_iterator it; for (it = buckets.begin(); it != buckets.end(); it++) @@ -1550,25 +1539,27 @@ writeOutRules() outputFile << "{" << endl; vector::const_iterator it2 = it->second.begin(); for (; it2 != it->second.end(); it2++) - outputFile << *it2; + outputFile << *it2; outputFile << "}" << endl; } outputFile.close(); - #endif +#endif /////////////// outputFile.open("rules_new.smt2", ios::trunc); - for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin() ; it != rewrite_system.toWrite.end(); it++) - { + for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin(); + it != rewrite_system.toWrite.end(); it++) + { it->writeOut(outputFile); - } + } outputFile.close(); ///////////////// outputFile.open("array.smt2", ios::trunc); ASTVec v; - for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin() ; it != rewrite_system.toWrite.end(); it++) + for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin(); + it != rewrite_system.toWrite.end(); it++) { v.push_back(it->getN()); } @@ -1589,7 +1580,7 @@ rename_then_rewrite(ASTNode n, const Rewrite_rule& original_rule) { n = renameVars(n); ASTNodeMap seen; - n = rewrite(n,original_rule,seen,0); + n = rewrite(n, original_rule, seen, 0); return renameVarsBack(n); } @@ -1606,15 +1597,15 @@ rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen, in ASTVec v; v.reserve(n.Degree()); for (int i = 0; i < n.Degree(); i++) - v.push_back(rewrite(n[i],original_rule,seen,depth+1)); + v.push_back(rewrite(n[i], original_rule, seen, depth + 1)); assert(v.size() > 0); ASTNode n2; - if (v!=n.GetChildren()) + if (v != n.GetChildren()) { if (n.GetType() != BOOLEAN_TYPE) - n2 = mgr->CreateArrayTerm(n.GetKind(),n.GetIndexWidth(), n.GetValueWidth(), v); + n2 = mgr->CreateArrayTerm(n.GetKind(), n.GetIndexWidth(), n.GetValueWidth(), v); else n2 = mgr->CreateNode(n.GetKind(), v); } @@ -1669,14 +1660,14 @@ rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen, in ASTNodeMap cache; ASTNode r = SubstitutionMap::replace(rr[i].getTo(), fromTo, cache, nf, false, true); - if (debug_usr2 && (getDifficulty(n2) < getDifficulty(r))) + if (debug_usr2 && (getDifficulty(n2) < getDifficulty(r))) { - cerr << rr[i].getFrom() << rr[i].getTo(); - cerr << getDifficulty(rr[i].getFrom()) << "to" << getDifficulty(rr[i].getTo()) << "\n"; - cerr << n2 << r; - cerr << getDifficulty(n2) << "to" << getDifficulty(r); - assert (getDifficulty(n2) >= getDifficulty(r)); - } + cerr << rr[i].getFrom() << rr[i].getTo(); + cerr << getDifficulty(rr[i].getFrom()) << "to" << getDifficulty(rr[i].getTo()) << "\n"; + cerr << n2 << r; + cerr << getDifficulty(n2) << "to" << getDifficulty(r); + assert(getDifficulty(n2) >= getDifficulty(r)); + } seen.insert(make_pair(n2, r)); @@ -1707,26 +1698,27 @@ rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen, in return n2; } - -int smt2_scan_string(const char *yy_str); +int +smt2_scan_string(const char *yy_str); // http://stackoverflow.com/questions/3418231/c-replace-part-of-a-string-with-another-string -bool replace(std::string& str, const std::string& from, const std::string& to) { - size_t start_pos = str.find(from); - if(start_pos == std::string::npos) - return false; - str.replace(start_pos, from.length(), to); - return true; +bool +replace(std::string& str, const std::string& from, const std::string& to) +{ + size_t start_pos = str.find(from); + if (start_pos == std::string::npos) + return false; + str.replace(start_pos, from.length(), to); + return true; } - void load_new_rules(const string fileName = "rules_new.smt2") { FILE * in; - bool opended= false; + bool opended = false; - if(!ifstream(fileName.c_str())) /// use stdin if the default file is not found. + if (!ifstream(fileName.c_str())) /// use stdin if the default file is not found. in = stdin; else { @@ -1760,36 +1752,37 @@ load_new_rules(const string fileName = "rules_new.smt2") int id, verified_to_bits, time_used, from_v, to_v; string s; - char line [63000]; + char line[63000]; bool first = true; bool done = false; while (true) { - fgets ( line, sizeof line, in ); - if (first) - { - int rv = sscanf(line, ";id:%d\tverified_to:%d\ttime:%d\tfrom_difficulty:%d\tto_difficulty:%d\n", &id, &verified_to_bits, &time_used, &from_v, &to_v); - if (rv !=5) - { - cerr << line; - done = true; - break; - } - first = false; - continue; - } - s+= line; - if (!strcmp(line,"(exit)\n")) - break; + fgets(line, sizeof line, in); + if (first) + { + int rv = sscanf(line, ";id:%d\tverified_to:%d\ttime:%d\tfrom_difficulty:%d\tto_difficulty:%d\n", &id, + &verified_to_bits, &time_used, &from_v, &to_v); + if (rv != 5) + { + cerr << line; + done = true; + break; + } + first = false; + continue; + } + s += line; + if (!strcmp(line, "(exit)\n")) + break; } if (done) break; mgr->GetRunTimes()->start(RunTimes::Parsing); - replace(s,v_string,""); - replace(s,w_string,""); + replace(s, v_string, ""); + replace(s, w_string, ""); // Load it into a string because other wise the parser reads in big blocks way past where we want it to. smt2_scan_string(s.c_str()); @@ -1818,7 +1811,7 @@ load_new_rules(const string fileName = "rules_new.smt2") } Rewrite_rule r(mgr, from, to, 0, id); - r.setVerified(verified_to_bits,time_used); + r.setVerified(verified_to_bits, time_used); rewrite_system.push_back(r); @@ -1826,7 +1819,8 @@ load_new_rules(const string fileName = "rules_new.smt2") parserInterface->popToFirstLevel(); } - extern int smt2lex_destroy(void); + extern int + smt2lex_destroy(void); smt2lex_destroy(); parserInterface->cleanUp(); @@ -1849,18 +1843,18 @@ expandRules(int timeout_ms, const char* fileName = "") load_new_rules(fileName); createVariables(); - for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.begin(); it!= rewrite_system.end();it++) + for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.begin(); it != rewrite_system.end(); it++) { if ((*it).timedCheck(timeout_ms)) { it->writeOut(cout); // omit failed. - cerr << getDifficulty(it->getFrom()) <<" " << getDifficulty(it->getTo()); + cerr << getDifficulty(it->getFrom()) << " " << getDifficulty(it->getTo()); } } } - -void t2() +void +t2() { extern FILE *smt2in; @@ -1872,24 +1866,24 @@ void t2() mgr->GetRunTimes()->start(RunTimes::Parsing); smt2parse(); - ASTVec v = FlattenKind(AND, piTypeCheckDefault.GetAsserts()); + ASTVec v = FlattenKind(AND, piTypeCheckDefault.GetAsserts()); ASTNode n = nf->CreateNode(XOR, v); //rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen) ASTNodeMap seen; createVariables(); - ASTNode r = rename_then_rewrite(n,Rewrite_rule::getNullRule()); + ASTNode r = rename_then_rewrite(n, Rewrite_rule::getNullRule()); cerr << r; parserInterface = NULL; - } // loads the already existing rules. -void load_old_rules(string fileName) +void +load_old_rules(string fileName) { - if(!ifstream(fileName.c_str())) - return; // file doesn't exist. + if (!ifstream(fileName.c_str())) + return; // file doesn't exist. extern FILE *smt2in; @@ -1943,7 +1937,7 @@ void load_old_rules(string fileName) rewrite_system.buildLookupTable(); ASTVec vvv = mgr->GetAsserts(); - for (int i=0; i < vvv.size() ;i++) + for (int i = 0; i < vvv.size(); i++) cout << vvv[i]; // So we don't output as soon as one is discovered... @@ -1969,7 +1963,8 @@ testProps() doProp(propKinds[k], a); } -int test() +int +test() { // Test code. load_old_rules("test.smt2"); @@ -2007,7 +2002,8 @@ createVariables() w0.SetValueWidth(bits); } -void unit_test() +void +unit_test() { // Create the negation and not terms in different orders. This tests the commutative matching. @@ -2016,13 +2012,13 @@ void unit_test() ASTNode not_v = create(BEEV::BVNEG, c); ASTNode neg_v = create(BEEV::BVUMINUS, c); - ASTNode plus_v = create(BVPLUS,not_v,neg_v); + ASTNode plus_v = create(BVPLUS, not_v, neg_v); c.clear(); c.push_back(w); ASTNode neg_w = create(BEEV::BVUMINUS, c); ASTNode not_w = create(BEEV::BVNEG, c); - ASTNode plus_w = create(BVPLUS,not_w,neg_w); + ASTNode plus_w = create(BVPLUS, not_w, neg_w); ASTNodeMap sub; plus_w = renameVars(plus_w); @@ -2031,57 +2027,54 @@ void unit_test() assert(commutative_matchNode(plus_v,plus_w,sub,1)); - } - int main(int argc, const char* argv[]) { startup(); - if (argc == 1) // Read the current rule set, find new rules. { - load_new_rules(); - createVariables(); - //////////// - rewrite_system.buildLookupTable(); + load_new_rules(); + createVariables(); + //////////// + rewrite_system.buildLookupTable(); - Function_list functionList; - functionList.buildAll(); + Function_list functionList; + functionList.buildAll(); - // The hash is generated on these values. - vector values; - findRewrites(functionList.functions, values); + // The hash is generated on these values. + vector values; + findRewrites(functionList.functions, values); - cout << "Initial:" << bits << " widening to :" << widen_to << endl; - cout << "Highest disproved @ level: " << highestLevel << endl; - cout << highestDisproved << endl; - //////////// + cout << "Initial:" << bits << " widening to :" << widen_to << endl; + cout << "Highest disproved @ level: " << highestLevel << endl; + cout << highestDisproved << endl; + //////////// - rewrite_system.rewriteAll(); - writeOutRules(); + rewrite_system.rewriteAll(); + writeOutRules(); } - else if (argc ==2 && !strcmp("unit-test",argv[1])) + else if (argc == 2 && !strcmp("unit-test", argv[1])) { load_new_rules(); createVariables(); unit_test(); } - else if (argc ==2 && !strcmp("verify",argv[1])) - { + else if (argc == 2 && !strcmp("verify", argv[1])) + { load_new_rules(); rewrite_system.verifyAllwithSAT(); - } - else if ((argc == 4 || argc ==3) && !strcmp("expand",argv[1])) + } + else if ((argc == 4 || argc == 3) && !strcmp("expand", argv[1])) { // expand the bit-widths rules are tested at. int timeout_ms = atoi(argv[2]); assert(timeout_ms > 0); - expandRules(timeout_ms, (argc == 4 ? argv[3]:"")); + expandRules(timeout_ms, (argc == 4 ? argv[3] : "")); } - else if (argc == 2 && !strcmp("rewrite",argv[1])) + else if (argc == 2 && !strcmp("rewrite", argv[1])) { // load the rules and apply the rewrite system to itself. load_new_rules(); @@ -2089,14 +2082,14 @@ main(int argc, const char* argv[]) rewrite_system.rewriteAll(); writeOutRules(); } - else if (argc == 2 && !strcmp("write-out",argv[1])) + else if (argc == 2 && !strcmp("write-out", argv[1])) { load_new_rules(); createVariables(); rewrite_system.rewriteAll(); writeOutRules(); // have the times now.. } - else if (argc == 2 && !strcmp("test",argv[1])) + else if (argc == 2 && !strcmp("test", argv[1])) { testProps(); } @@ -2119,55 +2112,54 @@ main(int argc, const char* argv[]) writeOutRules(); } #endif - else if (argc == 2 && !strcmp("test2",argv[1])) + else if (argc == 2 && !strcmp("test2", argv[1])) { load_new_rules(); t2(); } - for (int i=0; i< saved_array.size();i++) + for (int i = 0; i < saved_array.size(); i++) delete saved_array[i]; } #if 0 // Term variables have a specified width!!! bool -matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width) -{ - // Pointers to the same value. OK. - if (n0 == n1) +matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width) + { + // Pointers to the same value. OK. + if (n0 == n1) return true; - if (n0.GetKind() == SYMBOL && strlen(n0.GetName()) == term_variable_width) - { - if (fromTo.find(n0) != fromTo.end()) + if (n0.GetKind() == SYMBOL && strlen(n0.GetName()) == term_variable_width) + { + if (fromTo.find(n0) != fromTo.end()) return matchNode(fromTo.find(n0)->second, n1, fromTo, term_variable_width); - fromTo.insert(make_pair(n0, n1)); - return matchNode(fromTo.find(n0)->second, n1, fromTo, term_variable_width); - } + fromTo.insert(make_pair(n0, n1)); + return matchNode(fromTo.find(n0)->second, n1, fromTo, term_variable_width); + } - // Here: - // They could be different BVConsts, different symbols, or - // different functions. + // Here: + // They could be different BVConsts, different symbols, or + // different functions. - if (n0.Degree() != n1.Degree() || (n0.Degree() == 0)) - return false; + if (n0.Degree() != n1.Degree() || (n0.Degree() == 0)) + return false; - if (n0.GetKind() != n1.GetKind()) - return false; + if (n0.GetKind() != n1.GetKind()) + return false; - for (int i = 0; i < n0.Degree(); i++) - { - if (!matchNode(n0[i], n1[i], fromTo, term_variable_width)) - return false; - } + for (int i = 0; i < n0.Degree(); i++) + { + if (!matchNode(n0[i], n1[i], fromTo, term_variable_width)) + return false; + } - return true; -} + return true; + } #endif - bool debug_matching = false; ///////// @@ -2175,15 +2167,15 @@ bool debug_matching = false; // "false" if it definately can't be matched with any possible commutative ordering. // "true" can be matched, later you need to check if all the "commutative" can be matched. bool -commutative_matchNode(const ASTNode& n0, const ASTNode& n1, const int term_variable_width, - deque >& commutative, ASTNode& vNode, ASTNode& wNode) +commutative_matchNode(const ASTNode& n0, const ASTNode& n1, const int term_variable_width, + deque >& commutative, ASTNode& vNode, ASTNode& wNode) { // Pointers to the same value. OK. if (n0 == n1) return true; // If we try and match sub-terms of concatenations,e,g. 000::x = 000111, we want it to fail. - if(n0.GetValueWidth() != n1.GetValueWidth()) + if (n0.GetValueWidth() != n1.GetValueWidth()) return false; if (n0.GetKind() == SYMBOL && strlen(n0.GetName()) == term_variable_width) @@ -2217,24 +2209,24 @@ commutative_matchNode(const ASTNode& n0, const ASTNode& n1, const int term_var // different functions. if (n0.Degree() != n1.Degree() || (n0.Degree() == 0)) - return false; + return false; if (n0.GetKind() != n1.GetKind()) - return false; + return false; // If it's commutative, check it specially / seprately later. if (isCommutative(n0.GetKind()) && n0.Degree() > 1) { - commutative.push_back(make_pair(n0,n1)); + commutative.push_back(make_pair(n0, n1)); return true; } else { - for (int i = 0; i < n0.Degree(); i++) - { - if (!commutative_matchNode(n0[i], n1[i], term_variable_width,commutative,vNode,wNode)) + for (int i = 0; i < n0.Degree(); i++) + { + if (!commutative_matchNode(n0[i], n1[i], term_variable_width, commutative, vNode, wNode)) return false; - } + } } return true; } @@ -2250,15 +2242,16 @@ c_matchNode(const ASTNode& n0, const ASTNode& n1, const int term_variable_width, const int init_comm_size = commutative_to_check.size(); - bool r = commutative_matchNode(n0, n1, term_variable_width, commutative_to_check, vNode,wNode); - assert(commutative_to_check.size() >= init_comm_size); // if anything, only pushed onto the back. + bool r = commutative_matchNode(n0, n1, term_variable_width, commutative_to_check, vNode, wNode); + assert(commutative_to_check.size() >= init_comm_size); + // if anything, only pushed onto the back. if (debug_matching) { cerr << "======Commut-match=======" << r << endl; cerr << "given" << n0 << n1; cerr << "Commutative still to match:" << endl; - for (int j=0;j < commutative_to_check.size(); j++) + for (int j = 0; j < commutative_to_check.size(); j++) { cerr << "++++++++++" << endl; cerr << "first" << commutative_to_check[j].first; @@ -2313,13 +2306,12 @@ c_matchNode(const ASTNode& n0, const ASTNode& n1, const int term_variable_width, //deque > todo_copy2 = commutative_to_check; const int new_comm_size = commutative_to_check.size(); - // Check each permutation of the commutative operation's operands. do { // Check each of the operands matches. Store Extra away in "commutative_to_check". - bool good= true; - for (int i=0;i < f.size(); i++) + bool good = true; + for (int i = 0; i < f.size(); i++) { if (!commutative_matchNode(f[i], s[i], term_variable_width, commutative_to_check, vNode, wNode)) { @@ -2330,14 +2322,14 @@ c_matchNode(const ASTNode& n0, const ASTNode& n1, const int term_variable_width, // Empty out the "commutative_to_check". if (good) - if (!c_matchNode(mgr->ASTTrue, mgr->ASTTrue, term_variable_width, commutative_to_check,vNode,wNode)) - good =false; + if (!c_matchNode(mgr->ASTTrue, mgr->ASTTrue, term_variable_width, commutative_to_check, vNode, wNode)) + good = false; if (good) { - assert(commutative_to_check.size() ==0); - return true; // all match. - } + assert(commutative_to_check.size() ==0); + return true; // all match. + } else { vNode = vNode_copy2; @@ -2354,13 +2346,11 @@ c_matchNode(const ASTNode& n0, const ASTNode& n1, const int term_variable_width, vNode = vNode_copy; wNode = wNode_copy; - if (commutative_to_check.size() < init_comm_size) commutative_to_check.push_back(p); else commutative_to_check.erase(commutative_to_check.begin() + init_comm_size, commutative_to_check.end()); - return false; } @@ -2372,40 +2362,40 @@ c_matchNode(const ASTNode& n0, const ASTNode& n1, const int term_variable_width, * * NB: This uses a "static" container so this can't be called recursively. */ -bool in_commutative=false; +bool in_commutative = false; bool commutative_matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& substitution, const int term_variable_width) { assert(substitution.size() ==0); - assert(!in_commutative); // because the container is static. Check there is only one at a time. + assert(!in_commutative); + // because the container is static. Check there is only one at a time. in_commutative = true; #ifdef PEDANTIC_MATCHING_ASSERTS - { - // There shouldn't be any term variables on the RHS. - vector vars = getVariables(n1); - vector::iterator it = vars.begin(); - while (it != vars.end()) { - assert(strlen(it->GetName()) != term_variable_width); - assert(it->GetName()[0] == 'v' || it->GetName()[0] == 'w'); - it++; - } - assert(vars.size() <=2); + // There shouldn't be any term variables on the RHS. + vector vars = getVariables(n1); + vector::iterator it = vars.begin(); + while (it != vars.end()) + { + assert(strlen(it->GetName()) != term_variable_width); + assert(it->GetName()[0] == 'v' || it->GetName()[0] == 'w'); + it++; + } + assert(vars.size() <=2); - // All the LHS variables should be term variables. - vars = getVariables(n0); - it = vars.begin(); - while (it != vars.end()) - { - assert(strlen(it->GetName()) == term_variable_width); - it++; + // All the LHS variables should be term variables. + vars = getVariables(n0); + it = vars.begin(); + while (it != vars.end()) + { + assert(strlen(it->GetName()) == term_variable_width); + it++; + } + assert(vars.size() <=2); } - assert(vars.size() <=2); - } - #endif @@ -2414,12 +2404,12 @@ commutative_matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& substitu ASTNode vNode = mgr->ASTUndefined; ASTNode wNode = mgr->ASTUndefined; - bool r = c_matchNode(n0,n1,term_variable_width,commutative,vNode,wNode); + bool r = c_matchNode(n0, n1, term_variable_width, commutative, vNode, wNode); if (r) { vector s = getVariables(n0); - for (vector::iterator it = s.begin(); it != s.end();it++) + for (vector::iterator it = s.begin(); it != s.end(); it++) { assert(it->GetKind() ==SYMBOL); assert(strlen(it->GetName()) == term_variable_width); @@ -2427,13 +2417,13 @@ commutative_matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& substitu { assert(vNode != mgr->ASTUndefined); assert(vNode.GetValueWidth() == it->GetValueWidth()); - substitution.insert(make_pair(*it,vNode)); + substitution.insert(make_pair(*it, vNode)); } if (it->GetName()[0] == 'w') { assert(wNode != mgr->ASTUndefined); assert(wNode.GetValueWidth() == it->GetValueWidth()); - substitution.insert(make_pair(*it,wNode)); + substitution.insert(make_pair(*it, wNode)); } } } @@ -2446,7 +2436,8 @@ commutative_matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& substitu if (!r) { assert(substitution.size() == 0); - assert(commutative.size() ==0); // should be none left to process. + assert(commutative.size() ==0); + // should be none left to process. } assert(in_commutative); diff --git a/src/util/find_rewrites/rewrite_rule.h b/src/util/find_rewrites/rewrite_rule.h index 5c4bc8b..a27ea05 100644 --- a/src/util/find_rewrites/rewrite_rule.h +++ b/src/util/find_rewrites/rewrite_rule.h @@ -4,7 +4,8 @@ #include "../../STPManager/STPManager.h" #include "misc.h" -void soft_time_out(int ignored) +void +soft_time_out(int ignored) { mgr->soft_timeout_expired = true; } @@ -12,39 +13,36 @@ void soft_time_out(int ignored) bool orderEquivalence(ASTNode& from, ASTNode& to); - class Rewrite_rule { - ASTNode from; - ASTNode to; - ASTNode n; + ASTNode from; + ASTNode to; + ASTNode n; - int time_to_verify; - int verified_to_bits; + int time_to_verify; + int verified_to_bits; - // Only used to build the NULL rule - Rewrite_rule() - { - from = mgr->CreateZeroConst(1); - to = mgr->CreateZeroConst(1); - n = mgr->ASTTrue; - } + // Only used to build the NULL rule + Rewrite_rule() + { + from = mgr->CreateZeroConst(1); + to = mgr->CreateZeroConst(1); + n = mgr->ASTTrue; + } public: - static Rewrite_rule - getNullRule() - { - return Rewrite_rule(); - } + static Rewrite_rule + getNullRule() + { + return Rewrite_rule(); + } - void writeOut(ostream& outputFileSMT2) const + void + writeOut(ostream& outputFileSMT2) const { - outputFileSMT2 << ";id:0" - << "\tverified_to:" << verified_to_bits << "\ttime:" << getTime() - << "\tfrom_difficulty:" << getDifficulty(getFrom()) - << "\tto_difficulty:" << getDifficulty(getTo()) - << "\n"; + outputFileSMT2 << ";id:0" << "\tverified_to:" << verified_to_bits << "\ttime:" << getTime() << "\tfrom_difficulty:" + << getDifficulty(getFrom()) << "\tto_difficulty:" << getDifficulty(getTo()) << "\n"; outputFileSMT2 << "(push 1)" << endl; printer::SMTLIB2_PrintBack(outputFileSMT2, getN(), true); outputFileSMT2 << "(exit)" << endl; @@ -69,15 +67,21 @@ public: const ASTNode& getFrom() const - {return from;} + { + return from; + } const ASTNode& getTo() const - {return to;} + { + return to; + } int getTime() const - {return time_to_verify;} + { + return time_to_verify; + } ASTNode getN() const @@ -92,32 +96,32 @@ public: } // The "from" and "to" should be ordered with the orderEquivalence function. - Rewrite_rule(BEEV::STPMgr* bm, const BEEV::ASTNode& from_, const BEEV::ASTNode& to_, const int t, int _id=-1) - : from(from_), to(to_) - { + Rewrite_rule(BEEV::STPMgr* bm, const BEEV::ASTNode& from_, const BEEV::ASTNode& to_, const int t, int _id = -1) : + from(from_), to(to_) + { #if 0 if (_id ==-1) - id = static_id++; - else - { - id =_id; // relied on to be unique. So be careful. - static_id =id+1; // assuming we are loading them all up.. - } + id = static_id++; + else + { + id =_id; // relied on to be unique. So be careful. + static_id =id+1;// assuming we are loading them all up.. + } #endif - verified_to_bits = 0; - time_to_verify = t; - - ASTVec c; - c.push_back(to_); - c.push_back(from_); - n = bm->hashingNodeFactory->CreateNode(BEEV::EQ,c); - - assert(orderEquivalence(from,to)); - assert(from == from_); - assert(to == to_); - assert(BVTypeCheckRecursive(n)); - assert(!n.isConstant()); - } + verified_to_bits = 0; + time_to_verify = t; + + ASTVec c; + c.push_back(to_); + c.push_back(from_); + n = bm->hashingNodeFactory->CreateNode(BEEV::EQ, c); + + assert(orderEquivalence(from,to)); + assert(from == from_); + assert(to == to_); + assert(BVTypeCheckRecursive(n)); + assert(!n.isConstant()); + } bool operator<(const Rewrite_rule& t) const @@ -159,7 +163,7 @@ public: cerr << from << to; } - bool result = isConstant(widened, assignment,i); + bool result = isConstant(widened, assignment, i); if (!result && !mgr->soft_timeout_expired) { // not a constant, and not timed out! diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h index 1e21ba4..1d376b9 100644 --- a/src/util/find_rewrites/rewrite_system.h +++ b/src/util/find_rewrites/rewrite_system.h @@ -14,7 +14,6 @@ orderEquivalence(ASTNode& from, ASTNode& to); ASTNode create(Kind k, const ASTNode& n0, const ASTNode& n1); - template void removeDuplicates(T & big); @@ -23,12 +22,11 @@ ASTNode widen(const ASTNode& w, int width); bool -matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width); +matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width); bool commutative_matchNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width); - ASTNode renameVars(const ASTNode &n); @@ -53,7 +51,6 @@ isConstant(const ASTNode& n, VariableAssignment& different); ASTNode rewriteThroughWithAIGS(const ASTNode &n_); - class Rewrite_system { public: @@ -67,36 +64,38 @@ private: void writeOutRules(); - friend ASTNode rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen, int depth); + friend ASTNode + rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen, int depth); RewriteRuleContainer toWrite; - std::map< Kind, vector > kind_to_rr; - bool lookups_invalid; // whether the above table is bad. + std::map > kind_to_rr; + bool lookups_invalid; // whether the above table is bad. void addRuleToLookup(Rewrite_rule& r) { const ASTNode& from = r.getFrom(); kind_to_rr[from.GetKind()].push_back(r); - assert(from.Degree() > 0); // Shouldn't map from a constant, nor from a variable. + assert(from.Degree() > 0); + // Shouldn't map from a constant, nor from a variable. } - public: bool checkInvariant() { - int size=0; - std::map< Kind, vector >::iterator it; - for(it=kind_to_rr.begin();it != kind_to_rr.end();it++) + int size = 0; + std::map >::iterator it; + for (it = kind_to_rr.begin(); it != kind_to_rr.end(); it++) { - for (int i=0; i < it->second.size();i++) + for (int i = 0; i < it->second.size(); i++) { - assert(it->second[i].getFrom().GetKind() == it->first); // All have the same kind as the lookup kind. + assert(it->second[i].getFrom().GetKind() == it->first); + // All have the same kind as the lookup kind. } - size+= it->second.size(); + size += it->second.size(); } return size == toWrite.size(); @@ -119,7 +118,8 @@ public: return toWrite.end(); } - bool areLookupsGood() + bool + areLookupsGood() { return lookups_invalid; } @@ -129,11 +129,11 @@ public: { kind_to_rr.clear(); - for (RewriteRuleContainer::iterator it = toWrite.begin() ; it != toWrite.end(); it++) + for (RewriteRuleContainer::iterator it = toWrite.begin(); it != toWrite.end(); it++) { addRuleToLookup(*it); } - lookups_invalid =false; + lookups_invalid = false; } void @@ -166,9 +166,10 @@ public: return toWrite.size(); } - static ASTNode rewriteNode(ASTNode n) + static ASTNode + rewriteNode(ASTNode n) { - return rename_then_rewrite(n,Rewrite_rule::getNullRule()); + return rename_then_rewrite(n, Rewrite_rule::getNullRule()); } void @@ -179,8 +180,8 @@ public: buildLookupTable(); - int i=0; - for (RewriteRuleContainer::iterator it = toWrite.begin() ; it != toWrite.end(); it++, i++) + int i = 0; + for (RewriteRuleContainer::iterator it = toWrite.begin(); it != toWrite.end(); it++, i++) { if (i % 1000 == 0) cout << "rewrite all:" << i << " of " << toWrite.size() << endl; @@ -201,9 +202,9 @@ public: } ASTNodeMap seen; - ASTNode from_wide_rewritten = rewrite(from_wide, *it,seen,0); + ASTNode from_wide_rewritten = rewrite(from_wide, *it, seen, 0); seen = ASTNodeMap(); - ASTNode to_wide_rewritten = rewrite(to_wide, *it,seen,0); + ASTNode to_wide_rewritten = rewrite(to_wide, *it, seen, 0); seen = ASTNodeMap(); // Also apply the AIG rules. @@ -217,10 +218,10 @@ public: assert(BVTypeCheckRecursive(from_rewritten)); assert(BVTypeCheckRecursive(to_rewritten)); - assert (isConstantToSat(create(EQ, from_wide_rewritten,from_wide))); - assert (isConstantToSat(create(EQ, to_wide_rewritten,to_wide))); - assert (isConstantToSat(create(EQ, it->getFrom(),from_rewritten))); - assert (isConstantToSat(create(EQ, it->getTo(),to_rewritten))); + assert(isConstantToSat(create(EQ, from_wide_rewritten,from_wide))); + assert(isConstantToSat(create(EQ, to_wide_rewritten,to_wide))); + assert(isConstantToSat(create(EQ, it->getFrom(),from_rewritten))); + assert(isConstantToSat(create(EQ, it->getTo(),to_rewritten))); bool ok = orderEquivalence(from_rewritten, to_rewritten); if (ok) @@ -243,7 +244,7 @@ public: } if (!ok) - { + { cout << "Erasing bad rule.\n"; erase(it--); i--; @@ -257,7 +258,8 @@ public: buildLookupTable(); } - void clear() + void + clear() { toWrite.clear(); buildLookupTable(); @@ -267,7 +269,7 @@ public: verifyAllwithSAT() { cerr << "Started verifying all" << endl; - for (RewriteRuleContainer::iterator it = toWrite.begin() ; it != toWrite.end(); it++) + for (RewriteRuleContainer::iterator it = toWrite.begin(); it != toWrite.end(); it++) { VariableAssignment assignment; bool bad = false; @@ -282,14 +284,14 @@ public: assert(!bad); } if (bits >= it->getVerifiedToBits()) - it->setVerified(bits,getCurrentTime() - st); + it->setVerified(bits, getCurrentTime() - st); } } void writeOut(ostream &o) { - for (RewriteRuleContainer::iterator it = toWrite.begin() ; it != toWrite.end(); it++) + for (RewriteRuleContainer::iterator it = toWrite.begin(); it != toWrite.end(); it++) { it->writeOut(o); } -- 2.47.3