From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 22 Feb 2011 00:16:17 +0000 (+0000)
Subject: Improvement. Handle extracts especially when doing unconstrained variable elimination.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=80db0ffe28882b71ac3f5b2f7fa7485903d6043e;p=francis%2Fstp.git

Improvement. Handle extracts especially when doing unconstrained variable elimination.

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

diff --git a/src/simplifier/MutableASTNode.h b/src/simplifier/MutableASTNode.h
index 092f79e..c33a109 100644
--- a/src/simplifier/MutableASTNode.h
+++ b/src/simplifier/MutableASTNode.h
@@ -16,10 +16,11 @@ namespace BEEV
   {
     static vector<MutableASTNode*> all;
 
+  public:
     typedef set<MutableASTNode *> ParentsType;
     ParentsType parents;
 
-
+private:
     MutableASTNode(const MutableASTNode&); // No definition
     MutableASTNode&
     operator=(const MutableASTNode &); // No definition
@@ -170,10 +171,65 @@ namespace BEEV
         }
     }
 
+    // Variables that have >1 disjoint extract parents.
+    static void
+    getDisjointExtractVariables(vector<MutableASTNode*> & result)
+    {
+      const int size = all.size();
+      for (int i = size-1; i >=0 ; i--)
+        {
+          if (!all[i]->isSymbol())
+            continue;
+
+          ParentsType* p = &(all[i]->parents);
+
+          if (p->size() ==1 )
+            continue; // the regular case. Don't consider here.
+
+          ASTNode& node = all[i]->n;
+          bool found[node.GetValueWidth()];
+          for (int j=0; j <node.GetValueWidth();j++)
+            found[j] = false;
+
+          ParentsType::const_iterator it;
+          for (it = p->begin(); it!= p->end();it++)
+            {
+              ASTNode& parent_node = (*it)->n;
+               if (parent_node.GetKind() != BVEXTRACT)
+                  break;
+
+               const int lb = parent_node[2].GetUnsignedConst();
+               const int ub = parent_node[1].GetUnsignedConst();
+               assert(lb<=ub);
+
+               int j;
+               for (j =lb ; j <=ub;j++)
+                 {
+                   if (found[j])
+                       break;
+                   found[j] = true;
+                 }
+
+               // if didn't make it to the finish. Then it overlaps.
+               if (j<= ub)
+                 {
+                   break;
+                 }
+            }
+
+          if (it != p->end())
+            continue;
+
+          // All are extracts that don't overlap.
+          result.push_back(all[i]);
+        }
+      return;
+    }
+
     // Visit the parent before children. So that we hopefully prune parts of the
     // tree. Ie given  ( F(x_1,... x_10000) = v), where v is unconstrained,
     // we don't spend time exploring F(..), but chop it out.
-    void
+    static void
     getAllUnconstrainedVariables(vector<MutableASTNode*> & result)
     {
       const int size = all.size();
diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp
index 36ab599..213bded 100644
--- a/src/simplifier/RemoveUnconstrained.cpp
+++ b/src/simplifier/RemoveUnconstrained.cpp
@@ -3,7 +3,7 @@
  * Robert Bruttomesso's & Robert Brummayer's dissertations describe this.
  * 
  * Nb. this isn't finished. It doesn't do READS, left shift, implies.
-* I don't think anything can be done for : bvsx, bvzx, write, bvmod.
+ * I don't think anything can be done for : bvsx, bvzx, write, bvmod.
  */
 
 #include "RemoveUnconstrained.h"
@@ -38,7 +38,11 @@ namespace BEEV
     simplifier->haveAppliedSubstitutionMap();
 
     result = topLevel_other(result, simplifier);
-    #ifndef NDEBUG
+
+    // It is idempotent if there are no big ANDS (we have a special hack), and,
+    // if we don't introduced any new "disjoint extracts."
+
+    #if 0
     ASTNode result2 = topLevel_other(result, simplifier);
     if (result2 != result)
       {
@@ -77,10 +81,90 @@ namespace BEEV
   RemoveUnconstrained::replace(const ASTNode& from, const ASTNode to)
   {
     assert(from.GetKind() == SYMBOL);
+    assert(from.GetValueWidth() == to.GetValueWidth());
     simplifier_convenient->UpdateSubstitutionMapFewChecks(from, to);
     return;
   }
 
+  /* The most complicated handling is for EXTRACTS. If a variable has parents that
+ * are all extracts and each of those extracts is disjoint (i.e. reads different bits)
+ * Then each of the extracts are replaced by a fresh variable. This is the only case
+ * where a variable with multiple distinct parents is replaced by a fresh variable.
+ * + We perform this check upfront, so will miss any extra cases the the unconstrained
+ *   variable elimination introduces.
+ * + It's all or nothing. So even if there's an extract of [0:2] [1:2] and [3:5], we wont
+ *   replace the [3:5] (even though it could be).
+ */
+  void
+  RemoveUnconstrained::
+  splitExtractOnly(vector<MutableASTNode*> extracts)
+  {
+    assert(extracts.size() >0);
+
+    // Going to be rebuilt later anyway, so discard.
+    vector<MutableASTNode*> variables;
+
+    for (int i =0; i <extracts.size(); i++)
+      {
+        ASTNode& var = extracts[i]->n;
+        assert(var.GetKind() == SYMBOL);
+        const int size = var.GetValueWidth();
+        ASTNode toVar[size];
+
+        // Create a mutable copy that we can iterate over.
+        vector <MutableASTNode*> mut;
+        mut.insert(mut.end(), extracts[i]->parents.begin(), extracts[i]->parents.end());
+
+        for (vector<MutableASTNode*>::iterator it = mut.begin(); it != mut.end(); it++)
+          {
+            ASTNode parent_node = (*it)->n;
+            assert(((**it)).children[0] == extracts[i]);
+            assert(!parent_node.IsNull());
+            assert(parent_node.GetKind() == BVEXTRACT);
+
+            int lb = parent_node[2].GetUnsignedConst();
+            // Replace each parent with a fresh.
+            toVar[lb] = replaceParentWithFresh(**it,variables);
+          }
+
+      ASTVec concatVec;
+      int empty =0;
+      for (int j=0; j < size;j++)
+      {
+          if (toVar[j].IsNull())
+            {
+              empty++;
+              continue;
+            }
+
+          if (empty > 0)
+            {
+              concatVec.push_back(bm.CreateFreshVariable(0, empty, "extract_unc"));
+              empty = 0;
+            }
+
+          concatVec.push_back(toVar[j]);
+          //cout << toVar[j];
+          assert(toVar[j].GetValueWidth() > 0);
+          j+=toVar[j].GetValueWidth()-1;
+        }
+
+      if (empty> 0)
+        {
+          concatVec.push_back(bm.CreateFreshVariable(0, empty, "extract_unc"));
+        }
+
+    ASTNode concat = concatVec[0];
+    for (int i=1; i < concatVec.size();i++)
+      {
+          assert(!concat.IsNull());
+          concat = bm.CreateTerm(BVCONCAT, concat.GetValueWidth() + concatVec[i].GetValueWidth(),concatVec[i], concat);
+      }
+
+    replace(var,concat);
+        }
+  }
+
   ASTNode
   RemoveUnconstrained::topLevel_other(const ASTNode &n, Simplifier *simplifier)
   {
@@ -94,6 +178,14 @@ namespace BEEV
     vector<MutableASTNode*> variable_array;
 
     MutableASTNode* topMutable = MutableASTNode::build(n);
+
+    vector<MutableASTNode*> extracts;
+    topMutable->getDisjointExtractVariables(extracts);
+    if (extracts.size() > 0)
+      {
+          splitExtractOnly(extracts);
+      }
+
     topMutable->getAllUnconstrainedVariables(variable_array);
 
     for (int i =0; i < variable_array.size() ; i++)
diff --git a/src/simplifier/RemoveUnconstrained.h b/src/simplifier/RemoveUnconstrained.h
index 4342986..a8856dd 100644
--- a/src/simplifier/RemoveUnconstrained.h
+++ b/src/simplifier/RemoveUnconstrained.h
@@ -25,6 +25,9 @@ namespace BEEV
     ASTNode
     topLevel_other(const ASTNode &n, Simplifier *simplifier);
 
+    void
+    splitExtractOnly(vector<MutableASTNode*> extracts);
+
     void
     replace(MutableASTNode* from, const ASTNode to);