From: Tim King <taking@cs.nyu.edu>
Date: Sat, 15 Dec 2012 02:04:41 +0000 (-0500)
Subject: Adding unit test for different versions of division.
X-Git-Tag: cvc5-1.0.0~7391^2~36
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d0625db683e06cc55b8ffa2f56a8b26e6bb7427;p=cvc5.git

Adding unit test for different versions of division.
---

diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index d2f697637..2f9998066 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -387,4 +387,79 @@ public:
       TS_ASSERT_EQUALS(Integer(i).length(), internalLength(i));
     }
   }
+
+  void testEuclideanDivision() {
+    Integer q, r;
+
+    Integer::euclidianQR(q, r, 1, 4);
+    TS_ASSERT_EQUALS( q, Integer(0));
+    TS_ASSERT_EQUALS( r, Integer(1));
+
+
+    Integer::euclidianQR(q, r, 1, -4);
+    TS_ASSERT_EQUALS( q, Integer(0));
+    TS_ASSERT_EQUALS( r, Integer(1));
+
+    Integer::euclidianQR(q, r, -1, 4);
+    TS_ASSERT_EQUALS( q, Integer(-1));
+    TS_ASSERT_EQUALS( r, Integer(3));
+
+    Integer::euclidianQR(q,r, -1, -4);
+    TS_ASSERT_EQUALS( q, Integer(1));
+    TS_ASSERT_EQUALS( r, Integer(3));
+
+    Integer::euclidianQR(q,r, 5, 4);
+    TS_ASSERT_EQUALS( q, Integer(1));
+    TS_ASSERT_EQUALS( r, Integer(1));
+
+    Integer::euclidianQR(q,r, 5, -4);
+    TS_ASSERT_EQUALS( q, Integer(-1));
+    TS_ASSERT_EQUALS( r, Integer(1));
+
+    Integer::euclidianQR(q,r, -5, 4);
+    TS_ASSERT_EQUALS( q, Integer(-2));
+    TS_ASSERT_EQUALS( r, Integer(3));
+
+    Integer::euclidianQR(q,r, -5, -4);
+    TS_ASSERT_EQUALS( q, Integer(2));
+    TS_ASSERT_EQUALS( r, Integer(3));
+
+  }
+  void testFloorDivision() {
+    Integer q, r;
+
+    Integer::floorQR(q, r, 1, 4);
+    TS_ASSERT_EQUALS( q, Integer(0));
+    TS_ASSERT_EQUALS( r, Integer(1));
+
+
+    Integer::floorQR(q, r, 1, -4);
+    TS_ASSERT_EQUALS( q, Integer(-1));
+    TS_ASSERT_EQUALS( r, Integer(-3));
+
+    Integer::floorQR(q, r, -1, 4);
+    TS_ASSERT_EQUALS( q, Integer(-1));
+    TS_ASSERT_EQUALS( r, Integer(3));
+
+    Integer::floorQR(q,r, -1, -4);
+    TS_ASSERT_EQUALS( q, Integer(0));
+    TS_ASSERT_EQUALS( r, Integer(-1));
+
+    Integer::floorQR(q,r, 5, 4);
+    TS_ASSERT_EQUALS( q, Integer(1));
+    TS_ASSERT_EQUALS( r, Integer(1));
+
+    Integer::floorQR(q,r, 5, -4);
+    TS_ASSERT_EQUALS( q, Integer(-2));
+    TS_ASSERT_EQUALS( r, Integer(-3));
+
+    Integer::floorQR(q,r, -5, 4);
+    TS_ASSERT_EQUALS( q, Integer(-2));
+    TS_ASSERT_EQUALS( r, Integer(3));
+
+    Integer::floorQR(q,r, -5, -4);
+    TS_ASSERT_EQUALS( q, Integer(1));
+    TS_ASSERT_EQUALS( r, Integer(-1));
+
+  }
 };