From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 15 Apr 2012 06:52:35 +0000 (+0000)
Subject: Improvmeent. Speed up the division propagator a little.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=05dde65d4239f37a437d25f30103c41d66773b95;p=francis%2Fstp.git

Improvmeent. Speed up the division propagator a little.

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

diff --git a/src/simplifier/constantBitP/ConstantBitP_Division.cpp b/src/simplifier/constantBitP/ConstantBitP_Division.cpp
index bb485a8..dea6eb1 100644
--- a/src/simplifier/constantBitP/ConstantBitP_Division.cpp
+++ b/src/simplifier/constantBitP/ConstantBitP_Division.cpp
@@ -402,21 +402,24 @@ Result bvUnsignedQuotientAndRemainder(vector<FixedBits*>& children,
 		}
 
 		{
-			Result r1 = fix(a, minTop, maxTop);
-			r1 = merge(r1,fix(a, minTop, maxTop));
+                Result r1 = fix(a, minTop, maxTop);
+                if (r1 == CHANGED)
+                  r1 = merge(r1,fix(a, minTop, maxTop));
+
+                Result r2 = fix(b, minBottom, maxBottom);
+                if (r2 == CHANGED) // We call is a second time because it's not idepotent..
+                  r2 = merge(r2,fix(b, minBottom, maxBottom));
+
+                Result r3;
+                if (whatIs == QUOTIENT_IS_OUTPUT)
+                  {
+                    r3 = fix(output, minQuotient, maxQuotient);
+                    if (r3 == CHANGED)
+                      r3 = merge(r3,fix(output, minQuotient, maxQuotient));
+                  }
+                else
+                        r3 = fix(output, minRemainder, maxRemainder);
 
-			Result r2 = fix(b, minBottom, maxBottom);
-			// We call is a second time because it's not idepotent..
-			r2 = merge(r2,fix(b, minBottom, maxBottom));
-
-			Result r3;
-			if (whatIs == QUOTIENT_IS_OUTPUT)
-			  {
-			    r3 = fix(output, minQuotient, maxQuotient);
-			    r3 = merge(r3,fix(output, minQuotient, maxQuotient));
-			  }
-			else
-				r3 = fix(output, minRemainder, maxRemainder);
 
 			if (r1 == CONFLICT || r2 == CONFLICT || r3 == CONFLICT)
 			{