From c507793c632f70c94f597ba8e60061fa84d75da8 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 9 Mar 2011 03:45:26 +0000
Subject: [PATCH] Improvement. Now do unconstrained elimination for all
 inequalities.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1194 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/MutableASTNode.h        | 30 ++++++++++++++++
 src/simplifier/RemoveUnconstrained.cpp | 50 ++++++++++++++++++++++----
 unit_test/bvsgt2.smt2                  | 12 +++++++
 3 files changed, 86 insertions(+), 6 deletions(-)
 create mode 100644 unit_test/bvsgt2.smt2

diff --git a/src/simplifier/MutableASTNode.h b/src/simplifier/MutableASTNode.h
index c33a109..1ed2c43 100644
--- a/src/simplifier/MutableASTNode.h
+++ b/src/simplifier/MutableASTNode.h
@@ -34,6 +34,7 @@ private:
     // Make a mutable ASTNode graph like the ASTNode one, but with pointers back up too.
     // It's convoluted because we want a post order traversal. The root node of a sub-tree
     // will be created after its children.
+public:
     static MutableASTNode *
     build(ASTNode n, map<ASTNode, MutableASTNode *> & visited)
     {
@@ -57,6 +58,7 @@ private:
       visited.insert(make_pair(n, mut));
       return mut;
     }
+private:
 
     bool dirty;
 
@@ -137,6 +139,18 @@ private:
         (*it)->propagateUpDirty();
     }
 
+    void
+    replaceWithAnotherNode(MutableASTNode *newN)
+    {
+      n = newN->n;
+      vector<MutableASTNode*> vars;
+      removeChildren(vars); // ignore the result
+      children.clear();
+      children.insert(children.begin(), newN->children.begin(), newN->children.end());
+      propagateUpDirty();
+    }
+
+
     void
     replaceWithVar(ASTNode newV, vector<MutableASTNode*>& variables)
     {
@@ -241,6 +255,22 @@ private:
       return;
     }
 
+    void
+    getAllVariablesRecursively(vector<MutableASTNode*> & result, set<MutableASTNode*>& visited)
+    {
+      if (visited.find(this) != visited.end())
+        return;
+      if (isSymbol())
+        result.push_back(this);
+      const int size = children.size();
+      for (int i = 0 ; i < size; i++)
+        {
+          children[i]->getAllVariablesRecursively(result,visited);
+        }
+    }
+
+
+
     bool
     isUnconstrained()
     {
diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp
index 213bded..16290f5 100644
--- a/src/simplifier/RemoveUnconstrained.cpp
+++ b/src/simplifier/RemoveUnconstrained.cpp
@@ -96,8 +96,7 @@ namespace BEEV
  *   replace the [3:5] (even though it could be).
  */
   void
-  RemoveUnconstrained::
-  splitExtractOnly(vector<MutableASTNode*> extracts)
+  RemoveUnconstrained::splitExtractOnly(vector<MutableASTNode*> extracts)
   {
     assert(extracts.size() >0);
 
@@ -358,8 +357,7 @@ namespace BEEV
                 replace(children[0], lhs);
                 replace(children[1], rhs);
               }
-
-            if (children[0] == var && children[1].isConstant())
+            else if (children[0] == var && children[1].isConstant())
               {
                 if (children[1] == c1)
                   continue; // always false. Or always false.
@@ -369,8 +367,7 @@ namespace BEEV
                 ASTNode rhs = nf->CreateTerm(ITE, width, v,biggestNumber, smallestNumber);
                 replace(var, rhs);
               }
-
-            if (children[1] == var && children[0].isConstant())
+            else if (children[1] == var && children[0].isConstant())
               {
                 if (children[0] == c2)
                   continue;  // always false. Or always false.
@@ -380,7 +377,48 @@ namespace BEEV
                 ASTNode rhs = nf->CreateTerm(ITE, width, v, smallestNumber, biggestNumber);
                 replace(var, rhs);
               }
+            else // One side is a variable. The other is anything.
+              {
+                bool varOnLHS = (var == children[0]);
+
+                // All the ASTNode vars need to map to their existing MutableASTNodes. So we collect all the variables
+                vector<MutableASTNode*> vars;
+                set<MutableASTNode*> visited;
+                muteOther->getAllVariablesRecursively(vars, visited);
+                visited.clear();
+
+                map<ASTNode, MutableASTNode *> create;
+                for (vector<MutableASTNode*>::iterator it = vars.begin(); it != vars.end();it++)
+                  create.insert(make_pair((*it)->n, *it));
+                vars.clear();
+
+                ASTNode v= bm.CreateFreshVariable(0, 0, "STP_INTERNAL_comparison");
+
+                ASTNode rhs;
+                ASTNode n;
+                if (varOnLHS)
+                  {
+                    rhs = nf->CreateTerm(ITE, width, v, biggestNumber, smallestNumber);
 
+                    if (kind == BVSGE || kind == BVGE)
+                      n= nf->CreateNode(OR, v, nf->CreateNode(EQ, mutable_children[1]->toASTNode(nf), c1));
+                    else
+                      n= nf->CreateNode(AND, v, nf->CreateNode(NOT,nf->CreateNode(EQ, mutable_children[1]->toASTNode(nf), c1)));
+          }
+                else
+                  {
+                    rhs = nf->CreateTerm(ITE, width, v, smallestNumber, biggestNumber);
+
+                    if (kind == BVSGE || kind == BVGE)
+                      n= nf->CreateNode(OR, v, nf->CreateNode(EQ, mutable_children[0]->toASTNode(nf), c2));
+                    else
+                      n= nf->CreateNode(AND, v, nf->CreateNode(NOT,nf->CreateNode(EQ, mutable_children[0]->toASTNode(nf), c2)));
+                  }
+
+                replace(var, rhs);
+                MutableASTNode *newN = MutableASTNode::build(n,create);
+                muteParent.replaceWithAnotherNode(newN);
+              }
           }
           break;
 
diff --git a/unit_test/bvsgt2.smt2 b/unit_test/bvsgt2.smt2
new file mode 100644
index 0000000..43d58a3
--- /dev/null
+++ b/unit_test/bvsgt2.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun x () (_ BitVec 15))
+(declare-fun y () (_ BitVec 5))
+
+; Check that unconstrained elimination through >'s works.
+
+(assert (bvsgt x (concat (_ bv0 10) y)) )
+(check-sat)
+(exit)
-- 
2.47.3