From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 5 Feb 2011 14:04:31 +0000 (+0000)
Subject: Improvement. Simplifiy from (X bvdiv 1) to X.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b044142091ffce81c73f9f4814c449397aa331a6;p=francis%2Fstp.git

Improvement. Simplifiy from (X bvdiv 1) to X.

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

diff --git a/src/simplifier/constantBitP/Dependencies.h b/src/simplifier/constantBitP/Dependencies.h
index 62ab772..f636e9a 100644
--- a/src/simplifier/constantBitP/Dependencies.h
+++ b/src/simplifier/constantBitP/Dependencies.h
@@ -75,6 +75,31 @@ namespace simplifier
           }
       }
 
+      // The "toRemove" node is being removed. Used by unconstrained elimination.
+      void removeNode(const ASTNode& toRemove, ASTVec& variables)
+      {
+        for (unsigned i = 0; i < toRemove.GetChildren().size(); i++)
+          {
+            const ASTNode child = toRemove.GetChildren()[i];
+
+            NodeToDependentNodeMap::const_iterator it = dependents.find(child);
+            if (it == dependents.end())
+              continue;
+
+            it->second->erase(toRemove);
+            if (it->second->size() == 0)
+              {
+                removeNode(child,variables);
+                continue;
+              }
+
+            if (child.GetKind() == SYMBOL && it->second->size() ==1)
+              {
+                variables.push_back(child);
+              }
+          }
+      }
+
       void
       print() const
       {
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index e97b3de..be85f95 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2691,6 +2691,11 @@ namespace BEEV
           output = _bm->CreateOneConst(inputValueWidth);
           break;
         }
+      if (inputterm[1] == _bm->CreateOneConst(inputValueWidth))
+      {
+    	  	 output = inputterm[0];
+    	  	 break;
+      }
       output = inputterm;
       break;