From: trevor_hansen Date: Mon, 5 Mar 2012 23:26:16 +0000 (+0000) Subject: Improvements to utility code. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=dcbb6c3ada021cba450bce0c30d7ec2e6d8b1a9b;p=francis%2Fstp.git Improvements to utility code. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1582 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/util/find_rewrites/Functionlist.h b/src/util/find_rewrites/Functionlist.h index 07d1064..3e45a58 100644 --- a/src/util/find_rewrites/Functionlist.h +++ b/src/util/find_rewrites/Functionlist.h @@ -8,7 +8,7 @@ extern const int bits; extern Simplifier *simp; -extern Rewrite_system to_write; +extern Rewrite_system rewrite_system; ASTNode widen(const ASTNode& w, int width); @@ -26,7 +26,7 @@ class Function_list getAllFunctions(const ASTNode v, const ASTNode w, ASTVec& result) { - Kind types[] = {BVMULT, BVPLUS, BVXOR, BVAND}; + Kind types[] = {BVXOR, BVAND}; //Kind types[] = {BVMULT, BVDIV, SBVDIV, SBVREM, SBVMOD, BVPLUS, BVMOD, BVRIGHTSHIFT, BVLEFTSHIFT, BVOR, BVAND, BVXOR, BVSRSHIFT}; @@ -92,8 +92,8 @@ class Function_list void applyRewritesToAll(ASTVec& functions) { - to_write.buildLookupTable(); - cerr << "Applying:" << to_write.size() <<"rewrite rules" << endl; + rewrite_system.buildLookupTable(); + cerr << "Applying:" << rewrite_system.size() <<"rewrite rules" << endl; for (int i = 0; i < functions.size(); i++) { @@ -103,7 +103,7 @@ class Function_list if (i % 100000 == 0) cerr << "applyRewritesToAll:" << i << " of " << functions.size() << endl; - ASTNode r = to_write.rewriteNode(functions[i]); + ASTNode r = rewrite_system.rewriteNode(functions[i]); if (r!= functions[i]) { // cerr << "changed" << functions[i] << " to "<< r; @@ -292,7 +292,7 @@ public: removeSingleUndefined(); // All the unary combinations of the binaries. - //allUnary(functions); + allUnary(); cerr << "Two Level:" << functions.size() << endl; } diff --git a/src/util/find_rewrites/Makefile b/src/util/find_rewrites/Makefile index ad937f4..9b892b7 100644 --- a/src/util/find_rewrites/Makefile +++ b/src/util/find_rewrites/Makefile @@ -8,10 +8,14 @@ CXXFLAGS += -L../../../lib/ .PHONY: clean rewrite: $(OBJS) $(TOP)lib/libstp.a - $(CXX) $(CXXFLAGS) $@.o -o $@ -lstp + $(CXX) $(CXXFLAGS) $@.o -o $@ -lstp --static rewrite.o: rewrite.cpp Functionlist.h rewrite_rule.h rewrite_system.h VariableAssignment.h $(CXX) $(CXXFLAGS) rewrite.cpp -c clean: rm -f $(OBJS) rewrite time_cbitp test_cbitp + +upload: rewrite + strip ./rewrite + scp -C ./rewrite rimmer.csse.unimelb.edu.au:/home/pgrad/thansen diff --git a/src/util/find_rewrites/VariableAssignment.h b/src/util/find_rewrites/VariableAssignment.h index 09fff0e..167b655 100644 --- a/src/util/find_rewrites/VariableAssignment.h +++ b/src/util/find_rewrites/VariableAssignment.h @@ -7,11 +7,10 @@ #define VARIABLEASSIGNMENT_H_ extern ASTNode v, v0, w ,w0; - extern NodeFactory* nf; - extern BEEV::STPMgr* mgr; + struct VariableAssignment { private: diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp index f1344cb..5ec798c 100644 --- a/src/util/find_rewrites/rewrite.cpp +++ b/src/util/find_rewrites/rewrite.cpp @@ -33,9 +33,6 @@ smt2parse(); using namespace std; using namespace BEEV; -// Asynchronously stop solving. -bool finished = false; - // Holds the rewrite that was disproved at the largest bitwidth. ASTNode highestDisproved; int highestLevel = 0; @@ -51,13 +48,16 @@ const int values_in_hash = 64 / bits; const int mask = (1 << (bits)) - 1; ////////////////////////////////// +// Set by the signal handler to write out the rules that have been discovered. +volatile bool force_writeout = false; + // Saves a little bit of time. The vectors are saved between invocations. vector saved_array; // Stores the difficulties that have already been generated. map difficulty_cache; -Rewrite_system to_write; +Rewrite_system rewrite_system; void clearSAT(); @@ -76,10 +76,7 @@ string containsNode(const ASTNode& n, const ASTNode& hunting, string& current); void -applyRewritesToAll(ASTVec & v); - -void -writeOutRules(string fileName); +writeOutRules(); int getDifficulty(const ASTNode& n_); @@ -90,9 +87,6 @@ getVariables(const ASTNode& n); bool unifyNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width); -int -findNewRewrites(); - typedef HASHMAP ASTNodeString; BEEV::STPMgr* mgr; @@ -300,8 +294,8 @@ isConstant(const ASTNode& n, VariableAssignment& different) assert(symbols.size() > 0); // Both of them might not be contained in the assignment. - different.setV(mgr->CreateBVConst(symbols[0].GetValueWidth(), 0)); - different.setW(mgr->CreateBVConst(symbols[0].GetValueWidth(), 0)); + different.setV(mgr->CreateZeroConst(symbols[0].GetValueWidth())); + different.setW(mgr->CreateZeroConst(symbols[0].GetValueWidth())); // It might have been widened. for (int i = 0; i < symbols.size(); i++) @@ -585,6 +579,12 @@ doIte(ASTNode a) } } +void do_write_out(int ignore) +{ + force_writeout = true; +} + + int startup() { @@ -618,7 +618,7 @@ startup() mgr->UserFlags.stats_flag = false; mgr->UserFlags.optimize_flag = true; - ss = new MinisatCore(finished); + ss = new MinisatCore(mgr->soft_timeout_expired); // Prime the cache with 100.. for (int i = 0; i < 100; i++) @@ -642,6 +642,8 @@ startup() // w = mgr->LookupOrCreateSymbol("w"); // w.SetValueWidth(bits); + // Write out the work so far.. + signal(SIGUSR1,do_write_out); } @@ -649,7 +651,7 @@ void clearSAT() { delete ss; - ss = new MinisatCore(finished); + ss = new MinisatCore(mgr->soft_timeout_expired); } // Return true if the negation of the query is unsatisfiable. @@ -657,7 +659,6 @@ bool isConstantToSat(const ASTNode & query) { assert(query.GetType() == BOOLEAN_TYPE); - cout << "to"; GlobalSTP->ClearAllTables(); clearSAT(); @@ -666,7 +667,6 @@ isConstantToSat(const ASTNode & query) SOLVER_RETURN_TYPE r = GlobalSTP->Ctr_Example->CallSAT_ResultCheck(*ss, query2, query2, GlobalSTP->tosat, false); - cout << "from"; return (r == SOLVER_VALID); // unsat, always true } @@ -781,7 +781,7 @@ findRewrites(ASTVec& expressions, const vector& values, cons } cout << '\n' << "depth:" << depth << ", size:" << expressions.size() << " values:" << values.size() << " found: " - << to_write.size() << '\n'; + << rewrite_system.size() << " done:" << discarded << "\n"; assert(expressions.size() >0); @@ -832,14 +832,14 @@ findRewrites(ASTVec& expressions, const vector& values, cons continue; // nb. I haven't rebuilt the map, it's done by writeOutRules(). - equiv[i] == to_write.rewriteNode(equiv[i]); + equiv[i] == rewrite_system.rewriteNode(equiv[i]); for (int j = i + 1; j < equiv.size(); j++) /// commutative so skip some. { if (equiv[i].GetKind() == UNDEFINED || equiv[j].GetKind() == UNDEFINED) continue; - equiv[j] = to_write.rewriteNode(equiv[j]); + equiv[j] = rewrite_system.rewriteNode(equiv[j]); ASTNode from = equiv[i]; ASTNode to = equiv[j]; @@ -863,11 +863,16 @@ findRewrites(ASTVec& expressions, const vector& values, cons cout << to; cout << getDifficulty(from) << " to " << getDifficulty(to) << endl; cout << "After rewriting"; - cout << to_write.rewriteNode(from); - cout << to_write.rewriteNode(to); + cout << rewrite_system.rewriteNode(from); + cout << rewrite_system.rewriteNode(to); cout << "------"; - to_write.push_back(Rewrite_rule(mgr, from, to, getCurrentTime() - st)); + Rewrite_rule rr(mgr, from, to, getCurrentTime() - st); + + if (!rr.timedCheck(10000)) + continue; + + rewrite_system.push_back(rr); // Remove the more difficult expression. if (from == equiv[i]) @@ -895,14 +900,16 @@ findRewrites(ASTVec& expressions, const vector& values, cons } // Write out the rules intermitently. - if (lastOutput + 5000 < to_write.size()) + if (force_writeout || lastOutput + 5000 < rewrite_system.size()) { - writeOutRules("array.smt2"); - lastOutput = to_write.size(); + rewrite_system.rewriteAll(); + writeOutRules(); + lastOutput = rewrite_system.size(); } } } + discarded += expressions.size(); } // Converts the node into an IF statement that matches the node. @@ -1270,20 +1277,20 @@ template return ss.str(); } -// Write out all the rules that have been discovered to file. +// Write out all the rules that have been discovered to various files in different formats. void -writeOutRules(string fileName) +writeOutRules() { - to_write.rewriteAll(); + force_writeout = false; std::vector output; std::map dup; - for (Rewrite_system::RewriteRuleContainer::iterator it = to_write.toWrite.begin() ; it != to_write.toWrite.end(); it++) + for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin() ; it != rewrite_system.toWrite.end(); it++) { if (!it->isOK()) { - to_write.erase(it--); + rewrite_system.erase(it--); continue; } @@ -1341,6 +1348,7 @@ writeOutRules(string fileName) ASTNodeMap fromTo; + cerr << f; f = renameVars(f); //cerr << "renamed" << f; bool result = unifyNode(f,dup.find(sofar)->second.getFrom(),fromTo,2) ; @@ -1349,7 +1357,7 @@ writeOutRules(string fileName) cout << rewrite(f,*it,seen ); // The text of this rule is the same as another rule. - to_write.erase(it--); + rewrite_system.erase(it--); continue; } else @@ -1361,7 +1369,7 @@ writeOutRules(string fileName) // Remove the duplicates from output. removeDuplicates(output); - cout << "Rules Discovered in total: " << to_write.size() << endl; + cout << "Rules Discovered in total: " << rewrite_system.size() << endl; // Group functions of the same kind all together. hash_map, hashF > buckets; @@ -1384,28 +1392,18 @@ writeOutRules(string fileName) } outputFile.close(); - ofstream outputFileSMT2; - outputFileSMT2.open("rewrite_data.smt2", ios::trunc); - - for (Rewrite_system::RewriteRuleContainer::iterator it = to_write.toWrite.begin() ; it != to_write.toWrite.end(); it++) - { - 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, widened), true, false); - outputFileSMT2 << "(pop 1)\n"; - } - } - - outputFileSMT2.close(); + /////////////// + outputFile.open("rules_new.smt2", ios::trunc); + for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin() ; it != rewrite_system.toWrite.end(); it++) + { + it->writeOut(outputFile); + } + outputFile.close(); - outputFileSMT2.open(fileName.c_str(), ios::trunc); + ///////////////// + outputFile.open("array.smt2", ios::trunc); ASTVec v; - for (Rewrite_system::RewriteRuleContainer::iterator it = to_write.toWrite.begin() ; it != to_write.toWrite.end(); it++) + for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin() ; it != rewrite_system.toWrite.end(); it++) { v.push_back(it->getN()); } @@ -1413,9 +1411,9 @@ writeOutRules(string fileName) if (v.size() > 0) { ASTNode n = mgr->CreateNode(AND, v); - printer::SMTLIB2_PrintBack(outputFileSMT2, n, true); + printer::SMTLIB2_PrintBack(outputFile, n, true); } - outputFileSMT2.close(); + outputFile.close(); } @@ -1457,8 +1455,8 @@ rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen) vector& rr = n[0].Degree() > 0 ? - (to_write.kind_kind_to_rr[n.GetKind()][n[0].GetKind()]) : - (to_write.kind_to_rr[n.GetKind()]) ; + (rewrite_system.kind_kind_to_rr[n.GetKind()][n[0].GetKind()]) : + (rewrite_system.kind_to_rr[n.GetKind()]) ; for (int i = 0; i < rr.size(); i++) @@ -1508,6 +1506,147 @@ rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen) return n2; } +int smt2_scan_string(const char *yy_str); + +void +loadNewRules() +{ + string fileName = "rules_new.smt2"; + + if(!ifstream(fileName.c_str())) + return; // file doesn't exist. + + FILE * in = fopen(fileName.c_str(), "r"); + + TypeChecker nfTypeCheckDefault(*mgr->hashingNodeFactory, *mgr); + Cpp_interface piTypeCheckDefault(*mgr, &nfTypeCheckDefault); + mgr->UserFlags.print_STPinput_back_SMTLIB2_flag = true; + parserInterface = &piTypeCheckDefault; + + + // This file I/O code: 1) Is terrible 2) I'm in a big rush so just getting it working 3) am embarised by it. + while (!feof(in)) + { + int id, verified_to_bits, time_used, from_v, to_v; + + string s; + 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) + { + done = true; + break; + } + first = false; + continue; + } + s+= line; + if (!strcmp(line,"(exit)\n")) + break; + } + if (done) + break; + + mgr->GetRunTimes()->start(RunTimes::Parsing); + + // 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()); + smt2parse(); + ASTVec values = piTypeCheckDefault.GetAsserts(); + values = FlattenKind(AND, values); + + assert(values.size() ==1); + + ASTNode from = values[0][0]; + ASTNode to = values[0][1]; + + // Rule should be orderable. + bool ok = orderEquivalence(from, to); + if (!ok) + { + cout << "discarding rule that can't be ordered"; + cout << from << to; + cout << "----"; + continue; + } + + Rewrite_rule r(mgr, from, to, 0, id); + r.setVerified(verified_to_bits,time_used); + + assert(r.isOK()); + rewrite_system.push_back(r); + + mgr->PopQuery(); + parserInterface->popToFirstLevel(); + //parserInterface->cleanUp(); + } + //fclose(smt2in); + + cout << "New Style Rules Loaded:" << rewrite_system.size() << endl; +} + +//read from stdin, then tests it until the timeout. +void +testIndividualRule(int timeout_ms) +{ + int id, verified_to_bits, time_used, from_v, to_v; + scanf(";id:%d\tverified_to:%d\ttime:%d\tfrom_difficulty:%d\tto_difficulty:%d\n", &id, &verified_to_bits, &time_used, &from_v, &to_v); + + TypeChecker nfTypeCheckDefault(*mgr->hashingNodeFactory, *mgr); + Cpp_interface piTypeCheckDefault(*mgr, &nfTypeCheckDefault); + + mgr->UserFlags.print_STPinput_back_SMTLIB2_flag = true; + + parserInterface = &piTypeCheckDefault; + mgr->GetRunTimes()->start(RunTimes::Parsing); + smt2parse(); + ASTVec values = piTypeCheckDefault.GetAsserts(); + values = FlattenKind(AND, values); + + assert(values.size() ==1); + if ((values[0].GetKind() != EQ)) + { + cout << "Not equality??"; + cout << values[0]; + return; + } + + ASTNode from = values[0][0]; + ASTNode to = values[0][1]; + + // Rule should be orderable. + bool ok = orderEquivalence(from, to); + if (!ok) + { + cout << "discarding rule that can't be ordered"; + cout << from << to; + cout << "----"; + return; + } + + Rewrite_rule r(mgr, from, to, 0, id); + r.setVerified(verified_to_bits,time_used); + + assert(r.isOK()); + rewrite_system.push_back(r); + + mgr->PopQuery(); + parserInterface->popToFirstLevel(); + parserInterface->cleanUp(); + + + if (r.timedCheck(timeout_ms)) + r.writeOut(cout); // omit failed. +} + // loads the already existing rules. void loadExistingRules(string fileName) { @@ -1545,28 +1684,30 @@ void loadExistingRules(string fileName) bool ok = orderEquivalence(from, to); if (!ok) { - cout << "discarding rule that can't be ordere"; + cout << "discarding rule that can't be ordered"; + cout << from << to; + cout << "----"; continue; } Rewrite_rule r(mgr, from, to, 0); if (r.isOK()); - to_write.push_back(r); + rewrite_system.push_back(r); } mgr->PopQuery(); parserInterface->popToFirstLevel(); parserInterface->cleanUp(); - to_write.buildLookupTable(); + rewrite_system.buildLookupTable(); ASTVec vvv = mgr->GetAsserts(); for (int i=0; i < vvv.size() ;i++) cout << vvv[i]; // So we don't output as soon as one is discovered... - lastOutput = to_write.size(); + lastOutput = rewrite_system.size(); } void @@ -1605,20 +1746,14 @@ int test() w0 = mgr->LookupOrCreateSymbol("w0"); w0.SetValueWidth(bits); - writeOutRules("test-2.smt2"); - to_write.verifyAllwithSAT(); - to_write.clear(); + writeOutRules(); + rewrite_system.verifyAllwithSAT(); + rewrite_system.clear(); } -int -main() +void +createVariables() { - startup(); - //test(); - //exit(1); - - loadExistingRules("array.smt2"); - v = mgr->LookupOrCreateSymbol("v"); v.SetValueWidth(bits); @@ -1630,34 +1765,80 @@ main() w0 = mgr->LookupOrCreateSymbol("w0"); w0.SetValueWidth(bits); - - testProps(); - - findNewRewrites(); - writeOutRules("array.smt2"); - to_write.verifyAllwithSAT(); - writeOutRules("array-with-times.smt2"); // verifyingallwithsat gives us the times.. } int -findNewRewrites() +main(int argc, const char* argv[]) { - to_write.buildLookupTable(); + startup(); + + if (argc == 1) // Read the current rule set, find new rules. + { + loadExistingRules("array.smt2"); + 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; - return 0; + rewrite_system.rewriteAll(); + writeOutRules(); + } + else if (argc == 3 && !strcmp("verify-single",argv[1])) + { + int timeout_ms = atoi(argv[2]); + assert(timeout_ms > 0); + testIndividualRule(timeout_ms); + } + else if (argc == 2 && !strcmp("verify-all",argv[1])) + { + loadNewRules(); + createVariables(); + rewrite_system.verifyAllwithSAT(); + writeOutRules(); // have the times now.. + } + else if (argc == 2 && !strcmp("write-out",argv[1])) + { + loadNewRules(); + createVariables(); + rewrite_system.rewriteAll(); + writeOutRules(); // have the times now.. + } + else if (argc == 2 && !strcmp("test",argv[1])) + { + testProps(); + } + else if (argc == 2 && !strcmp("delete-failed",argv[1])) + { + loadNewRules(); + ifstream fin; + fin.open("failed.txt",ios::in); + char line[256]; + while (!fin.eof()) + { + fin.getline(line,256); + int id; + sscanf(line,"FAILED:%d",&id); + //cerr << "Failed id: " << id << endl; + rewrite_system.deleteID(id); + } + createVariables(); + writeOutRules(); + } } + // Term variables have a specified width!!! bool unifyNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width) diff --git a/src/util/find_rewrites/rewrite_rule.h b/src/util/find_rewrites/rewrite_rule.h index 36c08d8..c3e017f 100644 --- a/src/util/find_rewrites/rewrite_rule.h +++ b/src/util/find_rewrites/rewrite_rule.h @@ -9,6 +9,18 @@ extern const int bits; ASTNode widen(const ASTNode& w, int width); +int +getDifficulty(const ASTNode& n_); + +void soft_time_out(int ignored) +{ + mgr->soft_timeout_expired = true; +} + +bool +isConstant(const ASTNode& n, VariableAssignment& different); + + vector getVariables(const ASTNode& n); @@ -19,13 +31,43 @@ private: ASTNode to; ASTNode n; - int id; + int id; + static int static_id; - static int static_id; + int time_to_verify; + int verified_to_bits; public: - int time; + void writeOut(ostream& outputFileSMT2) + { + assert(isOK()); + outputFileSMT2 << ";id:" << getId() + << "\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, false); + outputFileSMT2 << "(exit)" << endl; + } + + // If we've verified it to bigger than before. Then store the bit / time. + void + setVerified(int bits_, int time_) + { + if (bits_ > verified_to_bits) + { + verified_to_bits = bits_; + time_to_verify = time_; + } + } + + int + getVerifiedToBits() + { + return verified_to_bits; + } const ASTNode& getFrom() const @@ -37,7 +79,7 @@ public: int getTime() const - {return time;} + {return time_to_verify;} ASTNode getN() const @@ -45,9 +87,17 @@ public: return n; } + int + getId() const + { + return id; + } + bool sameID(const Rewrite_rule& t) const { + return (*this == t); + if (id == t.id) { assert(n == t.n); @@ -83,11 +133,18 @@ public: } - Rewrite_rule(BEEV::STPMgr* bm, const BEEV::ASTNode& from_, const BEEV::ASTNode& to_, const int t) + Rewrite_rule(BEEV::STPMgr* bm, const BEEV::ASTNode& from_, const BEEV::ASTNode& to_, const int t, int _id=-1) : from(from_), to(to_) { - id = static_id++; - time = t; + 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.. + } + verified_to_bits = 0; + time_to_verify = t; ASTVec c; c.push_back(to_); @@ -144,5 +201,60 @@ public: { return (n < t.n); } + + // Tests for the timeout amount of time. FALSE if a bad instance was found. Otherwise true. + bool + timedCheck(int timeout_ms) + { + VariableAssignment assignment; + + mgr->soft_timeout_expired = false; + itimerval timeout; + signal(SIGVTALRM, soft_time_out); + timeout.it_interval.tv_usec = 0; + timeout.it_interval.tv_sec = 0; + timeout.it_value.tv_usec = 1000 * (timeout_ms % 1000); + timeout.it_value.tv_sec = timeout_ms / 1000; + setitimer(ITIMER_VIRTUAL, &timeout, NULL); + + const int st = getCurrentTime(); + int checked_to = 0; + + // Start it verifying where we left off.. + for (int i = std::max(bits, getVerifiedToBits() + 1); i < 1024; i++) + { + //cout << i << " "; + ASTVec children; + children.push_back(from); + children.push_back(to); + + const ASTNode n = mgr->hashingNodeFactory->CreateNode(EQ, children); + const ASTNode& widened = widen(n, i); + if (widened == mgr->ASTUndefined) + { + cout << "cannot widen"; + cerr << from << to; + } + + bool result = isConstant(widened, assignment); + if (!result && !mgr->soft_timeout_expired) + { + // not a constant, and not timed out! + cerr << "FAILED:" << getId() << endl << i << from << to; + writeOut(cerr); + return false; + } + if (mgr->soft_timeout_expired) + break; + + checked_to = i; + } + + if (getVerifiedToBits() <= checked_to) + setVerified(checked_to, getTime() + (getCurrentTime() - st)); + + return true; + } + }; #endif diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h index 683208a..2602fea 100644 --- a/src/util/find_rewrites/rewrite_system.h +++ b/src/util/find_rewrites/rewrite_system.h @@ -43,12 +43,17 @@ rename_then_rewrite(ASTNode n, const Rewrite_rule& original_rule); bool isConstantToSat(const ASTNode & query); +bool +isConstant(const ASTNode& n, VariableAssignment& different); class Rewrite_system { private: - friend void writeOutRules(string fileName); + friend + void + writeOutRules(); + friend ASTNode rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen); @@ -77,6 +82,19 @@ public: kind_kind_to_rr[from.GetKind()][from[0].GetKind()].push_back(r); } + void + deleteID(int id) + { + for (RewriteRuleContainer::iterator it = toWrite.begin() ; it != toWrite.end(); it++) + { + if (it->getId() == id) + { + toWrite.erase(it--); + cerr << "matched" << id; + } + } + } + void buildLookupTable() { @@ -199,10 +217,14 @@ public: } else { - cout << "Mapped but couldn't order"; - cout << rewritten_from << to; + if (rewritten_from != to) + { + cout << "Mapped but couldn't order"; + cout << rewritten_from << to; + } erase(it--); i--; + buildLookupTable(); // Otherwise two rules will remove each other? } } } @@ -233,7 +255,18 @@ public: assert(r); assert(!bad); } - it->time = getCurrentTime() - st; + if (bits > it->getVerifiedToBits()) + it->setVerified(bits,getCurrentTime() - st); + } + } + + + void + writeOut(ostream &o) + { + for (RewriteRuleContainer::iterator it = toWrite.begin() ; it != toWrite.end(); it++) + { + it->writeOut(o); } } };