Improvement. Better propagation for division when division be zero is possible.

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

diff --git a/src/simplifier/constantBitP/ConstantBitP_Division.cpp b/src/simplifier/constantBitP/ConstantBitP_Division.cpp
index d2e9b9154bdfbc91662924060867401b6c8f4b2e..74d549a62908b6521dbff69387540cea4597967c 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitP_Division.cpp
+++ b/src/simplifier/constantBitP/ConstantBitP_Division.cpp
@@ -659,7 +659,26 @@ Result bvUnsignedDivisionBothWays(vector<FixedBits*>& children,
                FixedBits& output, STPMgr* bm) {
 
         if (children[1]->containsZero())
-               return NO_CHANGE;
+          {
+            for (int i=children[0]->getWidth()-1; i > 0 ; i--)
+              {
+                if (children[0]->isFixedToZero(i))
+                  {
+                    if (output.isFixedToOne(i))
+                      return CONFLICT;
+                    else if (!output.isFixed(i))
+                      {
+                        output.setFixed(i,true);
+                        output.setValue(i,false);
+                      }
+                  }
+                else
+                  {
+                    break;
+                  }
+              }
+            return NOT_IMPLEMENTED;
+          }
 
        Result r = bvUnsignedQuotientAndRemainder(children, output, bm,
                        QUOTIENT_IS_OUTPUT);