From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 19 Mar 2012 00:31:21 +0000 (+0000)
Subject: Improvements to utility code for generating rewrite rules.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e5edba912d8ee1845c05557ccb33029c91bd24c1;p=francis%2Fstp.git

Improvements to utility code for generating rewrite rules.

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

diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp
index 4ef1670..e5f96e2 100644
--- a/src/util/find_rewrites/rewrite.cpp
+++ b/src/util/find_rewrites/rewrite.cpp
@@ -989,13 +989,22 @@ findRewrites(ASTVec& expressions, const vector<VariableAssignment>& values, cons
           ASTNode& from = equiv[i];
           ASTNode& to = equiv[j];
 
-          if (from.isConstant() && to.isConstant())
-            continue;
+          if (from == to)
+            {
+              to = mgr->ASTUndefined;
+              continue;
+            }
+
+          /* If they can't be ordered continue. Maybe they could be ordered if we applied
+           * the rewrites through. This also means that we won't split on terms that can't
+           * be ordered.
+           *
+           * Sometimes we run it anyway. Otherwise we do O(n^2) on big groups of
+           * expression that can't be ordered.
+           */
 
-          // 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))
+          if ((rand() % 100 == 0) &&  !orderEquivalence(f,t))
             continue;
 
           VariableAssignment different;
@@ -1019,6 +1028,12 @@ findRewrites(ASTVec& expressions, const vector<VariableAssignment>& values, cons
               ASTNode f = equiv[i];
               ASTNode t = equiv[j];
 
+              if (t == f)
+                {
+                  equiv[j] = mgr->ASTUndefined;
+                  continue;
+                }
+
               bool r = orderEquivalence(f, t);
 
               if (!r)
@@ -1026,6 +1041,8 @@ findRewrites(ASTVec& expressions, const vector<VariableAssignment>& values, cons
 
               Rewrite_rule rr(mgr, f, t, checktime);
 
+              cout << "i:" << i << " j:" << j << " size:" << equiv.size() << "\n";
+
               VariableAssignment bad;
               if (!rr.timedCheck(10000,bad))
                 {
@@ -1060,6 +1077,7 @@ findRewrites(ASTVec& expressions, const vector<VariableAssignment>& values, cons
               equiv[i] = rewrite_system.rewriteNode(equiv[i]);
               equiv[j] = rewrite_system.rewriteNode(equiv[j]);
 
+              // They're the same, so in future we only care about one of them.
               if (equiv[i] == equiv[j])
                 equiv[j]= mgr->ASTUndefined;
             }