[SCM] polybori: Polynomials over Boolean Rings branch, upstream-hg, updated. b4a5cffaa908c53e1d958a42110f8c4dad853aa3

[Alexander Dreyer]

The following commit has been merged in the upstream-hg branch:
commit 862c99cd3ef85cd60f30bf7b5bd5ae9174aa010d
Author: Alexander Dreyer <adreyer at gmx.de>
Date:   Tue Feb 28 14:03:58 2012 +0100

    FIX: better product range check

diff --git a/groebner/include/polybori/groebner/BitMask.h b/groebner/include/polybori/groebner/BitMask.h
index be8553a..17fba84 100644
--- a/groebner/include/polybori/groebner/BitMask.h
+++ b/groebner/include/polybori/groebner/BitMask.h
@@ -38,8 +38,10 @@ public:
   unsigned long low(const unsigned long& value) const { return 0; }
   const unsigned long& high(const unsigned long& value) const { return value; }
   const unsigned long& shift(const unsigned long& value) const { return value; }
+  unsigned long back(const unsigned long& value) const { return 0; }
 };
 
+
 template <unsigned NBits>
 class BitMask {
 public:
@@ -55,9 +57,22 @@ public:
   unsigned long shift(const unsigned long& value) const {
     return value << NBits;
   }
+  unsigned long back(const unsigned long& value) const {
+    return value << (sizeof(unsigned long)*8 - NBits);
+  }
 };
 
+template <>
+class BitMask<sizeof(unsigned long)*8> {
+public:
+  static const unsigned nbits = sizeof(unsigned long)*8;
+  static const unsigned long mask = (BitMask<nbits-1>::mask << 1) + 1;
 
+  const unsigned long& low(const unsigned long& value) const { return value; }
+  unsigned long high(const unsigned long& value) const { return 0; }
+  unsigned long shift(const unsigned long& value) const { return 0; }
+  const unsigned long& back(const unsigned long& value) const { return value; }
+};
 
 END_NAMESPACE_PBORIGB
 
diff --git a/groebner/include/polybori/groebner/DelayedLongProduct.h b/groebner/include/polybori/groebner/DelayedLongProduct.h
index d3815d7..4b83c6d 100644
--- a/groebner/include/polybori/groebner/DelayedLongProduct.h
+++ b/groebner/include/polybori/groebner/DelayedLongProduct.h
@@ -21,6 +21,7 @@
 #include "DelayedLongLong.h"
 #include "LongLongConstant.h"
 #include "LongProductLess.h"
+#include "NBitsUsed.h"
 
 BEGIN_NAMESPACE_PBORIGB
 
@@ -38,19 +39,27 @@ public:
   DelayedLongProduct(const long_type& high, const long_type & low):
     base(high, low) {}
 
-  // a,b != 0,  a <= c/b:  a*b <= (c/b)*b  <= (c/b)*b + (c%b) = c
-  // a,b != 0,  a >  c/b:  Assume a*b  <= c = (c/b)*b + (c%b) ->
+  // b != 0,  a <= c/b:  a*b <= (c/b)*b  <= (c/b)*b + (c%b) = c
+  // b != 0,  a >  c/b:  Assume a*b  <= c = (c/b)*b + (c%b) ->
   //   (c/b)*b < a*b  <= (c/b)*b + (c%b)  ->  c/b < a < c/b+1 (contradicts int)
   bool greater(long_type rhs) const {
-    if (high(first) && high(second)) 
-      return (first > rhs/second);
-
-    return (first * second) > rhs;
+    return (second != 0) && (first > rhs/second);
   }
 
   template <long_type MaxHigh, long_type MaxLow>
   bool greater(const LongLongConstant<MaxHigh, MaxLow>&) const {
-    return LongProductLess<MaxHigh, MaxLow>()(first, second);
+
+   if (second == 0)
+      return false;
+
+    BitMask<sizeof(long_type)*8 - NBitsUsed<MaxHigh>::value > front;
+    long_type front_part = (front.shift(MaxHigh) + front.high(MaxLow)) ;
+
+    long_type divided  = front_part / second;
+ 
+    return (front.high(divided) == 0) &&
+      (first > (front.back(divided) + 
+		(front.back(front_part%second)+ front.low(MaxLow) ) / second));
   }
 };
 
diff --git a/groebner/include/polybori/groebner/NBitsUsed.h b/groebner/include/polybori/groebner/NBitsUsed.h
new file mode 100644
index 0000000..3ec9dc7
--- /dev/null
+++ b/groebner/include/polybori/groebner/NBitsUsed.h
@@ -0,0 +1,45 @@
+// -*- c++ -*-
+//*****************************************************************************
+/** @file NBitsUsed.h 
+ *
+ * @author Alexander Dreyer 
+ * @date 2012-02-28 
+ *
+ * This file includes the definition of the class @c NBitsUsed.
+ *
+ * @par Copyright:
+ *   (c) 2012 by The PolyBoRi Team
+ *
+**/
+//*****************************************************************************
+
+#ifndef polybori_groebner_NBitsUsed_h_
+#define polybori_groebner_NBitsUsed_h_
+
+// include basic definitions
+#include "groebner_defs.h"
+
+BEGIN_NAMESPACE_PBORIGB
+
+/** @class NBitsUsed
+ * @brief This class defines @c NBitsUsed whose value attribute computes the
+ * actual number of used bits at compile time.
+ *
+ **/
+
+template<unsigned long NValue>
+class NBitsUsed {
+public:
+  static const unsigned value = NBitsUsed<(NValue >> 1)>::value + 1;
+};
+
+template<>
+class NBitsUsed<0> {
+public:
+  static const unsigned value = 0;
+};
+
+
+END_NAMESPACE_PBORIGB
+
+#endif /* polybori_groebner_NBitsUsed_h_ */
diff --git a/testsuite/src/DelayedLongProductTest.cc b/testsuite/src/DelayedLongProductTest.cc
index 8218acf..d69bb1d 100644
--- a/testsuite/src/DelayedLongProductTest.cc
+++ b/testsuite/src/DelayedLongProductTest.cc
@@ -43,7 +43,7 @@ BOOST_AUTO_TEST_CASE(test_less) {
 
   BOOST_CHECK_EQUAL((DelayedLongProduct((unsigned long)(-1), 
 					(unsigned long)(-1)) >
-		     LongLongConstant<(unsigned long)(-1), (unsigned long)(-1)>()), false);
+		     LongLongConstant<(unsigned long)(-1), (unsigned long)(-1)>()), true);
 
   BOOST_CHECK_EQUAL((DelayedLongProduct((unsigned long)(-1), 
 					(unsigned long)(-1)) >
@@ -54,16 +54,16 @@ BOOST_AUTO_TEST_CASE(test_less) {
 		     LongLongConstant<(unsigned long)(-1)/2, 
 		     (unsigned long)(-1)>()), true);
 
-  BOOST_CHECK_EQUAL((DelayedLongProduct((unsigned long)(2)<<(sizeof(long)*4),
-					(unsigned long)(2)<<(sizeof(long)*4)) >
+  BOOST_CHECK_EQUAL((DelayedLongProduct((unsigned long)(2)<< nhalf,
+					(unsigned long)(2)<< nhalf) >
 		     LongLongConstant<3,(unsigned long)(-1)>()), true);
 
-  BOOST_CHECK_EQUAL((DelayedLongProduct((unsigned long)(2)<<(sizeof(long)*4),
-					(unsigned long)(2)<<(sizeof(long)*4)) >
+  BOOST_CHECK_EQUAL((DelayedLongProduct((unsigned long)(2)<< nhalf ,
+					(unsigned long)(2)<< nhalf ) >
 		    LongLongConstant<4,0>()), false);
 
-  BOOST_CHECK_EQUAL((DelayedLongProduct((unsigned long)(2)<<(sizeof(long)*4),
-					(unsigned long)(2)<<(sizeof(long)*4) )>
+  BOOST_CHECK_EQUAL((DelayedLongProduct((unsigned long)(2)<< nhalf,
+					(unsigned long)(2)<< nhalf )>
 		    LongLongConstant<4,1>()), false);
 
   BOOST_CHECK_EQUAL((DelayedLongProduct(5, 7) > 34), true);

-- 
polybori: Polynomials over Boolean Rings