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 62ab77257328719aa423e4fdfaf87dcf752623d4..f636e9afd53083bbec594f58a57f928dd38d9295 100644 (file)
--- 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 e97b3de9c5745521d033188da061639c5882a223..be85f9513ceded8d7bf17f654d6d1b9f0cf3cb9c 100644 (file)
--- 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;