Move some division be zero code into the bitblaster. I'm trying to make the array...

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 391bc7367ea45fe61363d9aa94bee6b93643c7e3..d8e7ba2958a8f88947fc8c9f3164acd37b205fb9 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -448,49 +448,12 @@ namespace BEEV
           else
                  result = term;
 
-          const Kind k = result.GetKind();
-
-          if (BVDIV == k 
-              || BVMOD == k 
-              || SBVDIV == k 
-              || SBVREM == k 
-              || SBVMOD == k)
-            {
-
-              // I had this as a reference, but that was wrong. Because
-              // "result" gets over-written in the next block, result[1], may
-              // get a reference count of zero, so be garbage collected.
-              const ASTNode bottom = result[1];
-
               if (SBVDIV == result.GetKind() 
                   || SBVREM == result.GetKind() 
                   || SBVMOD == result.GetKind())
                 {
                   result = TranslateSignedDivModRem(result);
                 }
-
-              if (bm->UserFlags.division_by_zero_returns_one_flag && (k==SBVDIV || k == BVDIV))
-                {
-                  // This is a difficult rule to introduce in other
-                  // places because it's recursive. i.e.  result is
-                  // embedded unchanged inside the result.
-
-                  unsigned inputValueWidth = result.GetValueWidth();
-                  ASTNode zero = bm->CreateZeroConst(inputValueWidth);
-                  ASTNode one = bm->CreateOneConst(inputValueWidth);
-                  result = 
-                    nf->CreateTerm(ITE, inputValueWidth,
-                                   nf->CreateNode(EQ, zero, bottom),
-                                   one, result);
-
-                  //return result;
-                  if (bm->UserFlags.optimize_flag)
-                      return simp->SimplifyTerm_TopLevel(result);
-                  else
-                       return result;
-
-                }
-            }
         }
         break;
       }

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 37d4ba4893b2971b557d8493b98d18a9e64f18d5..f083cda22c6d2684422bdc9826ed6b097e3fdaae 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -673,7 +673,22 @@ const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& _term,
                BBNodeVec r(num_bits);
                BBDivMod(dvdd, dvsr, q, r, num_bits, support);
                if (k == BVDIV)
-                       result = q;
+               {
+                       if (uf->division_by_zero_returns_one_flag)
+                       {
+                               BBNodeVec zero(term.GetValueWidth(), BBFalse);
+
+                               BBNode eq = BBEQ(zero, dvsr);
+                               BBNodeVec one(term.GetValueWidth(), BBFalse);
+                               one[0] = BBTrue;
+
+                          result = BBITE(eq, one, q);
+                       }
+                       else
+                       {
+                               result = q;
+                       }
+               }
                else
                        result = r;
                break;