From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 11 Apr 2011 13:26:53 +0000 (+0000)
Subject: Move some division be zero code into the bitblaster. I'm trying to make the array... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=3c2764a7a6d01feadda19286cdcd7983c7c870f0;p=francis%2Fstp.git

Move some division be zero code into the bitblaster. I'm trying to make the array transformer (which also transforms signed div/mod) idempotent.

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 391bc73..d8e7ba2 100644
--- 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 37d4ba4..f083cda 100644
--- 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;