From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 6 Aug 2011 04:02:44 +0000 (+0000)
Subject: Add unconstrained shift for left/right.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=0d378d938dfcb807159c81193970b28a7428195d;p=francis%2Fstp.git

Add unconstrained shift for left/right.

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

diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp
index 824966e..e889fd6 100644
--- a/src/simplifier/RemoveUnconstrained.cpp
+++ b/src/simplifier/RemoveUnconstrained.cpp
@@ -2,8 +2,8 @@
  * Identifies unconstrained variables and remove them from the input.
  * 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.
+ * Nb. this isn't finished. It doesn't do reads / writes.
+ * I don't think anything can be done for : bvsx, bvzx.
  */
 
 #include "RemoveUnconstrained.h"
@@ -522,11 +522,41 @@ namespace BEEV
                   }
               }
               break;
+        case BVLEFTSHIFT:
+        case BVRIGHTSHIFT:
+        case BVSRSHIFT:
+             {
+                 assert(numberOfChildren == 2);
+                 if (mutable_children[0]->isUnconstrained() && mutable_children[1]->isUnconstrained())
+                  {
+                     assert(children[0] != children[1]);
+                     ASTNode v =replaceParentWithFresh(muteParent, variable_array);
+                     replace(children[1], bm.CreateZeroConst(width));
+                     replace(children[0], v);
+                  }
+              }
+             break;
+
+        case BVMOD:
+             {
+                 assert(numberOfChildren == 2);
+                 if (mutable_children[0]->isUnconstrained() && mutable_children[1]->isUnconstrained() && bm.UserFlags.isSet("unconstrained-bvmod", "0") )
+                  {
+                     assert (children[0] != children[1]);
+                     ASTNode v =replaceParentWithFresh(muteParent, variable_array);
+                     replace(children[1], bm.CreateZeroConst(width));
+                     replace(children[0], v);
+                  }
+              }
+             break;
+
+
         case BVDIV:
              {
                  assert(numberOfChildren == 2);
                  if (mutable_children[0]->isUnconstrained() && mutable_children[1]->isUnconstrained())
                   {
+                     assert (children[0] != children[1]);
                      ASTNode v =replaceParentWithFresh(muteParent, variable_array);
                      replace(children[1], bm.CreateOneConst(width));
                      replace(children[0], v);
diff --git a/unit_test/unc_shift.smt b/unit_test/unc_shift.smt
new file mode 100644
index 0000000..b5e9405
--- /dev/null
+++ b/unit_test/unc_shift.smt
@@ -0,0 +1,21 @@
+(benchmark r
+  :status sat
+  :category { crafted }
+  :difficulty { 0 }
+  :logic QF_BV
+  :extrafuns ((x BitVec[3]))
+  :extrafuns ((y BitVec[3]))
+  
+  :extrafuns ((w BitVec[3]))
+  :extrafuns ((z BitVec[3]))
+
+  :extrafuns ((q BitVec[3]))
+  :extrafuns ((r BitVec[3]))
+
+  :assumption (= (bvshl x y )  (bv4[3]))
+  :assumption (= (bvashr w z )  (bv4[3]))
+  :assumption (= (bvshl q r )  (bv4[3]))
+
+
+    :formula true
+)