From e45f9ef5a16f9a10e228177fe426e19809c1cf14 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 6 Mar 2012 00:08:29 +0000 Subject: [PATCH] Improvements to rewrite utility code. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1583 e59a4935-1847-0410-ae03-e826735625c1 --- src/util/find_rewrites/rewrite.cpp | 119 ++++++++++++------------ src/util/find_rewrites/rewrite_rule.h | 2 +- src/util/find_rewrites/rewrite_system.h | 21 ++++- 3 files changed, 79 insertions(+), 63 deletions(-) diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp index 5ec798c..af38e34 100644 --- a/src/util/find_rewrites/rewrite.cpp +++ b/src/util/find_rewrites/rewrite.cpp @@ -26,7 +26,6 @@ #include "rewrite_system.h" #include "Functionlist.h" -extern FILE *smt2in; extern int smt2parse(); @@ -62,6 +61,9 @@ Rewrite_system rewrite_system; void clearSAT(); +void +createVariables(); + template void removeDuplicates(T & big); @@ -637,10 +639,6 @@ startup() w0 = mgr->LookupOrCreateSymbol("w0"); w0.SetValueWidth(bits); - //v = mgr->LookupOrCreateSymbol("v"); - // v.SetValueWidth(bits); - // w = mgr->LookupOrCreateSymbol("w"); - // w.SetValueWidth(bits); // Write out the work so far.. signal(SIGUSR1,do_write_out); @@ -1277,6 +1275,13 @@ template return ss.str(); } + +/* Writes out: + * rewrite_data_new.cpp: rules coded in C++. + * array.cpp: rules in SMT2 in one big conjunct. + * rules_new.smt2: rules in SMT2 one rule per frame. + */ + // Write out all the rules that have been discovered to various files in different formats. void writeOutRules() @@ -1508,21 +1513,50 @@ rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen) 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; +} + + void loadNewRules() { - string fileName = "rules_new.smt2"; + FILE * in; + bool opended= false; + string fileName = "rules_new.smt2" - if(!ifstream(fileName.c_str())) - return; // file doesn't exist. + if(!ifstream(fileName.c_str())) /// use stdin if the default file is not found. + in = stdin; + else + { + in = fopen(fileName.c_str(), "r"); + opended = true; // so we know to fclose it. + } + + // We store references to "v" and "w", so we need to removed the + // definitions from the input we parse. - FILE * in = fopen(fileName.c_str(), "r"); + v = mgr->LookupOrCreateSymbol("v"); + v.SetValueWidth(bits); + w = mgr->LookupOrCreateSymbol("w"); + w.SetValueWidth(bits); TypeChecker nfTypeCheckDefault(*mgr->hashingNodeFactory, *mgr); Cpp_interface piTypeCheckDefault(*mgr, &nfTypeCheckDefault); mgr->UserFlags.print_STPinput_back_SMTLIB2_flag = true; parserInterface = &piTypeCheckDefault; + stringstream v_ss, w_ss; + v_ss << "(declare-fun v () (_ BitVec " << bits << "))"; + string v_string = v_ss.str(); + + w_ss << "(declare-fun w () (_ BitVec " << bits << "))"; + string w_string = w_ss.str(); // 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)) @@ -1557,6 +1591,9 @@ loadNewRules() mgr->GetRunTimes()->start(RunTimes::Parsing); + 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()); smt2parse(); @@ -1586,65 +1623,27 @@ loadNewRules() mgr->PopQuery(); parserInterface->popToFirstLevel(); - //parserInterface->cleanUp(); } - //fclose(smt2in); + + parserInterface->cleanUp(); + if (opended) + fclose(in); cout << "New Style Rules Loaded:" << rewrite_system.size() << endl; } //read from stdin, then tests it until the timeout. void -testIndividualRule(int timeout_ms) +expandRules(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); + loadNewRules(); + createVariables(); - 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) + for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.begin(); it!= rewrite_system.end();it++) { - cout << "discarding rule that can't be ordered"; - cout << from << to; - cout << "----"; - return; + if ((*it).timedCheck(timeout_ms)) + it->writeOut(cout); // omit failed. } - - 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. @@ -1653,6 +1652,8 @@ void loadExistingRules(string fileName) if(!ifstream(fileName.c_str())) return; // file doesn't exist. + extern FILE *smt2in; + smt2in = fopen(fileName.c_str(), "r"); TypeChecker nfTypeCheckDefault(*mgr->hashingNodeFactory, *mgr); Cpp_interface piTypeCheckDefault(*mgr, &nfTypeCheckDefault); @@ -1794,11 +1795,11 @@ main(int argc, const char* argv[]) rewrite_system.rewriteAll(); writeOutRules(); } - else if (argc == 3 && !strcmp("verify-single",argv[1])) + else if (argc == 3 && !strcmp("expand",argv[1])) // expand the bit-widths rules are tested at. { int timeout_ms = atoi(argv[2]); assert(timeout_ms > 0); - testIndividualRule(timeout_ms); + expandRules(timeout_ms); } else if (argc == 2 && !strcmp("verify-all",argv[1])) { diff --git a/src/util/find_rewrites/rewrite_rule.h b/src/util/find_rewrites/rewrite_rule.h index c3e017f..b97fb0b 100644 --- a/src/util/find_rewrites/rewrite_rule.h +++ b/src/util/find_rewrites/rewrite_rule.h @@ -56,7 +56,7 @@ public: void setVerified(int bits_, int time_) { - if (bits_ > verified_to_bits) + if (bits_ >= verified_to_bits) { verified_to_bits = bits_; time_to_verify = time_; diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h index 2602fea..7c9c6c4 100644 --- a/src/util/find_rewrites/rewrite_system.h +++ b/src/util/find_rewrites/rewrite_system.h @@ -48,6 +48,11 @@ isConstant(const ASTNode& n, VariableAssignment& different); class Rewrite_system { +public: + + // Rules to write out when we get the chance. + typedef list RewriteRuleContainer; + private: friend @@ -57,9 +62,6 @@ private: friend ASTNode rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen); - // Rules to write out when we get the chance. - typedef list RewriteRuleContainer; - RewriteRuleContainer toWrite; std::map< Kind, vector > kind_to_rr; std::map< Kind, std::map< Kind, vector > > kind_kind_to_rr; @@ -70,6 +72,19 @@ public: { } + RewriteRuleContainer::iterator + begin() + { + return toWrite.begin(); + } + + RewriteRuleContainer::iterator + end() + { + return toWrite.end(); + } + + void addRuleToLookup(Rewrite_rule& r) { -- 2.47.3