Fixes to code for manipulating rewrite rules.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1595 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/util/find_rewrites/Functionlist.h b/src/util/find_rewrites/Functionlist.h
index ed1f3bd7b017b8381d6e5043ca793eb64aab5fca..8716e9ac2a07bd717056ee098e0dde76034e1839 100644 (file)
--- a/src/util/find_rewrites/Functionlist.h
+++ b/src/util/find_rewrites/Functionlist.h
@@ -21,7 +21,7 @@ private:
   {
 
     Kind types[] =
-      { BVXOR, BVAND };
+      {BVMULT, BVDIV, SBVDIV, SBVREM, SBVMOD, BVMOD, BVLEFTSHIFT};
 
     //Kind types[] = {BVMULT, BVDIV, SBVDIV, SBVREM, SBVMOD, BVPLUS, BVMOD, BVRIGHTSHIFT, BVLEFTSHIFT, BVOR, BVAND, BVXOR, BVSRSHIFT};
     const int number_types = sizeof(types) / sizeof(Kind);
@@ -220,7 +220,9 @@ public:
         removeDuplicates(functions);
         //applySpeculative();
 
+        // Put back in later! Too slow for now...
         applyAIGs();
+        removeDuplicates(functions);
 
         // All the unary combinations of the binaries.
         allUnary();

diff --git a/src/util/find_rewrites/VariableAssignment.h b/src/util/find_rewrites/VariableAssignment.h
index 34b6f6a45cfceb86d08438cbe531f5f4d923f02a..dd7868c83aa3aff69df92d3963490aef17f9c447 100644 (file)
--- a/src/util/find_rewrites/VariableAssignment.h
+++ b/src/util/find_rewrites/VariableAssignment.h
@@ -1,74 +1,46 @@
-/*
- * VariableAssignment.h
- *
- */
-
 #ifndef VARIABLEASSIGNMENT_H_
 #define VARIABLEASSIGNMENT_H_
 
-extern ASTNode v, v0, w, w0;
-extern NodeFactory* nf;
-extern BEEV::STPMgr* mgr;
+// A pair of constants of the same bit-width assigned to v and w..
 
 struct VariableAssignment
 {
 private:
   ASTNode v;
   ASTNode w;
+  bool empty;
 
 public:
   ASTNode
   getV() const
   {
-    assert(v.isConstant());
+    assert(!empty);
     return v;
   }
 
   ASTNode
   getW() const
   {
-    assert(w.isConstant());
+    assert(!empty);
     return w;
   }
 
   void
-  setV(const ASTNode& nv)
+  setValues(const ASTNode& nv, const ASTNode& nw)
   {
     assert(nv.isConstant());
+    assert(nw.isConstant());
+    assert(nw.GetValueWidth() == nv.GetValueWidth());
+    w = nw;
     v = nv;
-  }
-
-  void
-  setW(const ASTNode& nW)
-  {
-    assert(nW.isConstant());
-    w = nW;
-  }
-
-  bool
-  isEmpty()
-  {
-    return (v == mgr->ASTUndefined || w == mgr->ASTUndefined);
+    empty = false;
   }
 
   VariableAssignment()
   {
+    empty = true;
   }
 
-  // Generate w from v a bit randomly.
-  explicit
-  VariableAssignment(const ASTNode & n)
-  {
-    setV(n);
-    srand(v.GetUnsignedConst());
-    w = mgr->CreateBVConst(n.GetValueWidth(), rand());
-  }
-
-  VariableAssignment(ASTNode & n0, ASTNode & n1)
-  {
-    setV(n0);
-    setV(n1);
-  }
 };
 
-#endif /* VARIABLEASSIGNMENT_H_ */
+#endif

diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp
index 97bc2cb6bda889c315331493e4e408a127c53c69..ba8fd19fbf6713ae37002a2aae4f7cef63949779 100644 (file)
--- a/src/util/find_rewrites/rewrite.cpp
+++ b/src/util/find_rewrites/rewrite.cpp
@@ -301,9 +301,9 @@ checkProp(const ASTNode& n)
   return true;
 }
 
-// True if it's always true. Otherwise fills the assignment.
+// True if it's always true, otherwise fills the assignment.
 bool
-isConstant(const ASTNode& n, VariableAssignment& different, const int bits)
+isConstant(const ASTNode& n, VariableAssignment& different, const int bit_width)
 {
   if (isConstantToSat(n))
     return true;
@@ -313,18 +313,23 @@ isConstant(const ASTNode& n, VariableAssignment& different, const int bits)
 
       vector<ASTNode> symbols = getVariables(n);
 
-      // Both of them might not be contained in the assignment.
-      different.setV(mgr->CreateZeroConst(bits));
-      different.setW(mgr->CreateZeroConst(bits));
+      // Both of them might not be contained in the assignment,
+      // (which might have been widened).
+      ASTNode vN = mgr->CreateZeroConst(bit_width);
+      ASTNode wN = mgr->CreateZeroConst(bit_width);
 
-      // It might have been widened.
       for (int i = 0; i < symbols.size(); i++)
         {
+          assert(symbols[i].GetValueWidth() == bit_width);
+
           if (strncmp(symbols[i].GetName(), "v", 1) == 0)
-            different.setV(GlobalSTP->Ctr_Example->GetCounterExample(true, symbols[i]));
+            vN = 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]));
+            wN = GlobalSTP->Ctr_Example->GetCounterExample(true, symbols[i]);
         }
+
+      different.setValues(vN, wN);
+
       return false;
     }
 }
@@ -727,7 +732,8 @@ startup()
   simp = new Simplifier(mgr);
   ArrayTransformer * at = new ArrayTransformer(mgr, simp);
   AbsRefine_CounterExample* abs = new AbsRefine_CounterExample(mgr, simp, at);
-  ToSAT* tosat = new ToSAT(mgr);
+  ToSATAIG* tosat = new ToSATAIG(mgr);
+  tosat->setArrayTransformer(at);
 
   GlobalSTP = new STP(mgr, simp, at, tosat, abs);
 
@@ -758,9 +764,7 @@ startup()
 
   // Write out the work so far..
   signal(SIGUSR1, do_write_out);
-
   signal(SIGUSR2, do_usr2);
-
 }
 
 void
@@ -768,6 +772,11 @@ clearSAT()
 {
   delete ss;
   ss = new MinisatCore<Minisat::Solver>(mgr->soft_timeout_expired);
+
+  delete GlobalSTP->tosat;
+  ToSATAIG* aig = new ToSATAIG(mgr);
+  aig->setArrayTransformer(GlobalSTP->arrayTransformer);
+  GlobalSTP->tosat = aig;
 }
 
 // Return true if the negation of the query is unsatisfiable.
@@ -979,6 +988,12 @@ findRewrites(ASTVec& expressions, const vector<VariableAssignment>& values, cons
           if (from.isConstant() && to.isConstant())
             continue;
 
+          // If they can't be ordered continue. Maybe they could be ordered if we applied
+          // the rewrites through..
+          ASTNode f = from, t = to;
+          if (!orderEquivalence(f,t))
+            continue;
+
           VariableAssignment different;
           bool bad = false;
           const int st = getCurrentTime();
@@ -1025,17 +1040,10 @@ findRewrites(ASTVec& expressions, const vector<VariableAssignment>& values, cons
               // Sometimes it doesn't. Not sure why..
               assert(t == rewrite_system.rewriteNode(f));
 
-              // Remove the more difficult expression.
-              if (f == equiv[i])
-                {
-                  cout << ".";
-                  equiv[i] = mgr->ASTUndefined;
-                }
-              if (t == equiv[j])
-                {
-                  cout << ".";
-                  equiv[j] = mgr->ASTUndefined;
-                }
+
+              equiv[i] = rewrite_system.rewriteNode(equiv[i]);
+              equiv[j] = rewrite_system.rewriteNode(equiv[j]);
+
             }
           else if (!bad)
             {
@@ -1210,7 +1218,7 @@ checkRule(const ASTNode & from, const ASTNode & to, VariableAssignment& assignme
         }
 
       // Send it to the SAT solver to verify that the widening has the same answer.
-      bool result = isConstant(widened, assignment, bits);
+      bool result = isConstant(widened, assignment, i);
 
       if (!result)
         {
@@ -1442,6 +1450,7 @@ writeOutRules()
   cout << "Writing out: " << rewrite_system.size() << " rules" << endl;
   force_writeout = false;
 
+#if 0
   std::vector<string> output;
   std::map<string, Rewrite_rule> dup;
 
@@ -1520,9 +1529,11 @@ writeOutRules()
 
   cout << "Rules Discovered in total: " << rewrite_system.size() << endl;
 
+
   // Group functions of the same kind all together.
   hash_map<string, vector<string>, hashF<std::string> > buckets;
   bucket("n.GetKind() ==", output, buckets);
+#endif
 
   ofstream outputFile;
 

diff --git a/src/util/find_rewrites/rewrite_rule.h b/src/util/find_rewrites/rewrite_rule.h
index a27ea057fcef60c663191cd379a0f995716291b0..44a9eb741f511a351d179f980751b8451bbabb94 100644 (file)
--- a/src/util/find_rewrites/rewrite_rule.h
+++ b/src/util/find_rewrites/rewrite_rule.h
@@ -4,6 +4,11 @@
 #include "../../STPManager/STPManager.h"
 #include "misc.h"
 
+extern ASTNode v, v0, w, w0;
+extern NodeFactory* nf;
+extern BEEV::STPMgr* mgr;
+
+
 void
 soft_time_out(int ignored)
 {

diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h
index 1d376b96cd7a82d71c356d3fbaad03892dc36e41..24d30768bc3e78c46a068f837d6dd01bcab01af2 100644 (file)
--- a/src/util/find_rewrites/rewrite_system.h
+++ b/src/util/find_rewrites/rewrite_system.h
@@ -246,6 +246,8 @@ public:
             if (!ok)
               {
                 cout << "Erasing bad rule.\n";
+                cout << "Initially" << it->getFrom() << it->getTo();
+                cout << "Now" << from_rewritten << to_rewritten;
                 erase(it--);
                 i--;
                 lookups_invalid = true;