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

diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp
index 5ec798c5f9fd84d03338da913b9c7851e5176735..af38e34883d8d6214eea1ed7969293e044b5426b 100644 (file)
--- 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<class T>
   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<class T>
     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 c3e017f611b21d67b7a5fc69226fec76cae37a13..b97fb0b3220a269b6d91104312796b44eeac47b5 100644 (file)
--- 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 2602fea253689fb40b1d6b31dbde2a6c44190411..7c9c6c4709537245dab2c75552dbed19121e0188 100644 (file)
--- 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<Rewrite_rule> 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<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;
@@ -70,6 +72,19 @@ public:
   {
   }
 
+  RewriteRuleContainer::iterator
+  begin()
+  {
+    return toWrite.begin();
+  }
+
+  RewriteRuleContainer::iterator
+  end()
+  {
+    return toWrite.end();
+  }
+
+
   void
   addRuleToLookup(Rewrite_rule& r)
   {