Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/util/integer_black.cpp	Lines:	371	371	100.0 %
Date:	2021-09-14	Branches:	1164	3806	30.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Tim King
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Black box testing of cvc5::Integer.
 */

#include <limits>
#include <sstream>

#include "base/exception.h"
#include "test.h"
#include "util/integer.h"

namespace cvc5 {
namespace test {

class TestUtilBlackInteger : public TestInternal
{
 protected:
  uint32_t internalLength(int32_t i)
  {
    if (i == 0)
    {
      return 1;
    }
    else
    {
      int32_t absi = i < 0 ? -i : i;
      uint32_t n = 0;
      int32_t powN = 1;
      do
      {
        powN <<= 1;
        ++n;
      } while (absi >= powN);
      return n;
    }
  }
  static const char* s_large_val;
  static const char* s_lots_of_leading_zeros;
};

const char* TestUtilBlackInteger::s_large_val =
    "4547897890548754897897897897890789078907890";
const char* TestUtilBlackInteger::s_lots_of_leading_zeros =
    "00000000000000000000000000000000000000000000000000000000000000000000000000"
    "000000000000000000000000000000000000000000000000000000000000000000000001";

TEST_F(TestUtilBlackInteger, constructors)
{
  Integer z0(1);
  ASSERT_EQ(z0.getLong(), 1);

  Integer z1(0);
  ASSERT_EQ(z1.getLong(), 0);

  Integer z2(-1);
  ASSERT_EQ(z2.getLong(), -1);

  Integer z3(0x890UL);
  ASSERT_EQ(z3.getUnsignedLong(), 0x890UL);

  Integer z4;
  ASSERT_EQ(z4.getLong(), 0);

  Integer z5("7896890");
  ASSERT_EQ(z5.getUnsignedLong(), 7896890ul);

  Integer z6(z5);
  ASSERT_EQ(z5.getUnsignedLong(), 7896890ul);
  ASSERT_EQ(z6.getUnsignedLong(), 7896890ul);

  std::string bigValue("1536729");
  Integer z7(bigValue);
  ASSERT_EQ(z7.getUnsignedLong(), 1536729ul);
}

TEST_F(TestUtilBlackInteger, compare_against_zero)
{
  Integer z(0);
  ASSERT_NO_THROW((void)(z == 0););
  ASSERT_EQ(z, 0);
}

TEST_F(TestUtilBlackInteger, operator_assign)
{
  Integer x(0);
  Integer y(79);
  Integer z(45789);

  ASSERT_EQ(x.getUnsignedLong(), 0ul);
  ASSERT_EQ(y.getUnsignedLong(), 79ul);
  ASSERT_EQ(z.getUnsignedLong(), 45789ul);

  x = y = z;

  ASSERT_EQ(x.getUnsignedLong(), 45789ul);
  ASSERT_EQ(y.getUnsignedLong(), 45789ul);
  ASSERT_EQ(z.getUnsignedLong(), 45789ul);

  Integer a(2);

  y = a;

  ASSERT_EQ(a.getUnsignedLong(), 2ul);
  ASSERT_EQ(y.getUnsignedLong(), 2ul);
  ASSERT_EQ(x.getUnsignedLong(), 45789ul);
  ASSERT_EQ(z.getUnsignedLong(), 45789ul);
}

TEST_F(TestUtilBlackInteger, operator_equals)
{
  Integer a(0);
  Integer b(79);
  Integer c("79");
  Integer d;

  ASSERT_TRUE(a == a);
  ASSERT_FALSE(a == b);
  ASSERT_FALSE(a == c);
  ASSERT_TRUE(a == d);

  ASSERT_FALSE(b == a);
  ASSERT_TRUE(b == b);
  ASSERT_TRUE(b == c);
  ASSERT_FALSE(b == d);

  ASSERT_FALSE(c == a);
  ASSERT_TRUE(c == b);
  ASSERT_TRUE(c == c);
  ASSERT_FALSE(c == d);

  ASSERT_TRUE(d == a);
  ASSERT_FALSE(d == b);
  ASSERT_FALSE(d == c);
  ASSERT_TRUE(d == d);
}

TEST_F(TestUtilBlackInteger, operator_not_equals)
{
  Integer a(0);
  Integer b(79);
  Integer c("79");
  Integer d;

  ASSERT_FALSE(a != a);
  ASSERT_TRUE(a != b);
  ASSERT_TRUE(a != c);
  ASSERT_FALSE(a != d);

  ASSERT_TRUE(b != a);
  ASSERT_FALSE(b != b);
  ASSERT_FALSE(b != c);
  ASSERT_TRUE(b != d);

  ASSERT_TRUE(c != a);
  ASSERT_FALSE(c != b);
  ASSERT_FALSE(c != c);
  ASSERT_TRUE(c != d);

  ASSERT_FALSE(d != a);
  ASSERT_TRUE(d != b);
  ASSERT_TRUE(d != c);
  ASSERT_FALSE(d != d);
}

TEST_F(TestUtilBlackInteger, operator_subtract)
{
  Integer x(0);
  Integer y(79);
  Integer z(-34);

  Integer act0 = x - x;
  Integer act1 = x - y;
  Integer act2 = x - z;
  Integer exp0(0);
  Integer exp1(-79);
  Integer exp2(34);

  Integer act3 = y - x;
  Integer act4 = y - y;
  Integer act5 = y - z;
  Integer exp3(79);
  Integer exp4(0);
  Integer exp5(113);

  Integer act6 = z - x;
  Integer act7 = z - y;
  Integer act8 = z - z;
  Integer exp6(-34);
  Integer exp7(-113);
  Integer exp8(0);

  ASSERT_EQ(act0, exp0);
  ASSERT_EQ(act1, exp1);
  ASSERT_EQ(act2, exp2);
  ASSERT_EQ(act3, exp3);
  ASSERT_EQ(act4, exp4);
  ASSERT_EQ(act5, exp5);
  ASSERT_EQ(act6, exp6);
  ASSERT_EQ(act7, exp7);
  ASSERT_EQ(act8, exp8);
}

TEST_F(TestUtilBlackInteger, operator_add)
{
  Integer x(0);
  Integer y(79);
  Integer z(-34);

  Integer act0 = x + x;
  Integer act1 = x + y;
  Integer act2 = x + z;
  Integer exp0(0);
  Integer exp1(79);
  Integer exp2(-34);

  Integer act3 = y + x;
  Integer act4 = y + y;
  Integer act5 = y + z;
  Integer exp3(79);
  Integer exp4(158);
  Integer exp5(45);

  Integer act6 = z + x;
  Integer act7 = z + y;
  Integer act8 = z + z;
  Integer exp6(-34);
  Integer exp7(45);
  Integer exp8(-68);

  ASSERT_EQ(act0, exp0);
  ASSERT_EQ(act1, exp1);
  ASSERT_EQ(act2, exp2);
  ASSERT_EQ(act3, exp3);
  ASSERT_EQ(act4, exp4);
  ASSERT_EQ(act5, exp5);
  ASSERT_EQ(act6, exp6);
  ASSERT_EQ(act7, exp7);
  ASSERT_EQ(act8, exp8);
}

TEST_F(TestUtilBlackInteger, operator_mult)
{
  Integer x(0);
  Integer y(79);
  Integer z(-34);

  Integer act0 = x * x;
  Integer act1 = x * y;
  Integer act2 = x * z;
  Integer exp0(0);
  Integer exp1(0);
  Integer exp2(0);

  Integer act3 = y * x;
  Integer act4 = y * y;
  Integer act5 = y * z;
  Integer exp3(0);
  Integer exp4(6241);
  Integer exp5(-2686);

  Integer act6 = z * x;
  Integer act7 = z * y;
  Integer act8 = z * z;
  Integer exp6(0);
  Integer exp7(-2686);
  Integer exp8(1156);

  ASSERT_EQ(act0, exp0);
  ASSERT_EQ(act1, exp1);
  ASSERT_EQ(act2, exp2);
  ASSERT_EQ(act3, exp3);
  ASSERT_EQ(act4, exp4);
  ASSERT_EQ(act5, exp5);
  ASSERT_EQ(act6, exp6);
  ASSERT_EQ(act7, exp7);
  ASSERT_EQ(act8, exp8);
}

TEST_F(TestUtilBlackInteger, to_string)
{
  std::stringstream ss;
  Integer large(s_large_val);
  ss << large;
  std::string res = ss.str();

  ASSERT_EQ(res, large.toString());
}

TEST_F(TestUtilBlackInteger, base_inference)
{
  ASSERT_EQ(Integer("0xa", 0), 10);
  ASSERT_EQ(Integer("0xff", 0), 255);
  ASSERT_EQ(Integer("011", 0), 9);
  ASSERT_EQ(Integer("0b1010", 0), 10);
  ASSERT_EQ(Integer("-1", 0), -1);
  ASSERT_EQ(Integer("42", 0), 42);
}

TEST_F(TestUtilBlackInteger, parse_errors)
{
  ASSERT_THROW(Integer("abracadabra"), std::invalid_argument);
  ASSERT_THROW(Integer("+-1"), std::invalid_argument);
  ASSERT_THROW(Integer("-+1"), std::invalid_argument);
  ASSERT_THROW(Integer("5i"), std::invalid_argument);
  ASSERT_THROW(Integer("10xyz"), std::invalid_argument);
  ASSERT_THROW(Integer("0xff", 10), std::invalid_argument);
  ASSERT_THROW(Integer("#x5", 0), std::invalid_argument);
  ASSERT_THROW(Integer("0b123", 0), std::invalid_argument);
}

TEST_F(TestUtilBlackInteger, pow)
{
  ASSERT_EQ(Integer(1), Integer(1).pow(0));
  ASSERT_EQ(Integer(1), Integer(5).pow(0));
  ASSERT_EQ(Integer(1), Integer(-1).pow(0));
  ASSERT_EQ(Integer(0), Integer(0).pow(1));
  ASSERT_EQ(Integer(5), Integer(5).pow(1));
  ASSERT_EQ(Integer(-5), Integer(-5).pow(1));
  ASSERT_EQ(Integer(16), Integer(2).pow(4));
  ASSERT_EQ(Integer(16), Integer(-2).pow(4));
  ASSERT_EQ(Integer(1000), Integer(10).pow(3));
  ASSERT_EQ(Integer(-1000), Integer(-10).pow(3));
}

TEST_F(TestUtilBlackInteger, overly_long)
{
  uint64_t ul = std::numeric_limits<uint64_t>::max();
  Integer i(ul);
  ASSERT_EQ(i.getUnsignedLong(), ul);
  ASSERT_THROW(i.getLong(), IllegalArgumentException);
  uint64_t ulplus1 = ul + 1;
  ASSERT_EQ(ulplus1, 0);
  i = i + 1;
  ASSERT_THROW(i.getUnsignedLong(), IllegalArgumentException);
}

TEST_F(TestUtilBlackInteger, testBit)
{
  ASSERT_FALSE(Integer(0).testBit(6));
  ASSERT_FALSE(Integer(0).testBit(5));
  ASSERT_FALSE(Integer(0).testBit(4));
  ASSERT_FALSE(Integer(0).testBit(3));
  ASSERT_FALSE(Integer(0).testBit(2));
  ASSERT_FALSE(Integer(0).testBit(1));
  ASSERT_FALSE(Integer(0).testBit(0));

  ASSERT_TRUE(Integer(-1).testBit(6));
  ASSERT_TRUE(Integer(-1).testBit(5));
  ASSERT_TRUE(Integer(-1).testBit(4));
  ASSERT_TRUE(Integer(-1).testBit(3));
  ASSERT_TRUE(Integer(-1).testBit(2));
  ASSERT_TRUE(Integer(-1).testBit(1));
  ASSERT_TRUE(Integer(-1).testBit(0));

  ASSERT_FALSE(Integer(10).testBit(6));
  ASSERT_FALSE(Integer(10).testBit(5));
  ASSERT_FALSE(Integer(10).testBit(4));
  ASSERT_TRUE(Integer(10).testBit(3));
  ASSERT_FALSE(Integer(10).testBit(2));
  ASSERT_TRUE(Integer(10).testBit(1));
  ASSERT_FALSE(Integer(10).testBit(0));

  ASSERT_FALSE(Integer(14).testBit(6));
  ASSERT_FALSE(Integer(14).testBit(5));
  ASSERT_FALSE(Integer(14).testBit(4));
  ASSERT_TRUE(Integer(14).testBit(3));
  ASSERT_TRUE(Integer(14).testBit(2));
  ASSERT_TRUE(Integer(14).testBit(1));
  ASSERT_FALSE(Integer(14).testBit(0));

  ASSERT_TRUE(Integer(64).testBit(6));
  ASSERT_FALSE(Integer(64).testBit(5));
  ASSERT_FALSE(Integer(64).testBit(4));
  ASSERT_FALSE(Integer(64).testBit(3));
  ASSERT_FALSE(Integer(64).testBit(2));
  ASSERT_FALSE(Integer(64).testBit(1));
  ASSERT_FALSE(Integer(64).testBit(0));
}

TEST_F(TestUtilBlackInteger, length)
{
  for (int32_t i = -17; i <= 17; ++i)
  {
    ASSERT_EQ(Integer(i).length(), internalLength(i));
  }
}

TEST_F(TestUtilBlackInteger, euclidianQR)
{
  Integer q, r;

  Integer::euclidianQR(q, r, 1, 4);
  ASSERT_EQ(q, Integer(0));
  ASSERT_EQ(r, Integer(1));

  Integer::euclidianQR(q, r, 1, -4);
  ASSERT_EQ(q, Integer(0));
  ASSERT_EQ(r, Integer(1));

  Integer::euclidianQR(q, r, -1, 4);
  ASSERT_EQ(q, Integer(-1));
  ASSERT_EQ(r, Integer(3));

  Integer::euclidianQR(q, r, -1, -4);
  ASSERT_EQ(q, Integer(1));
  ASSERT_EQ(r, Integer(3));

  Integer::euclidianQR(q, r, 5, 4);
  ASSERT_EQ(q, Integer(1));
  ASSERT_EQ(r, Integer(1));

  Integer::euclidianQR(q, r, 5, -4);
  ASSERT_EQ(q, Integer(-1));
  ASSERT_EQ(r, Integer(1));

  Integer::euclidianQR(q, r, -5, 4);
  ASSERT_EQ(q, Integer(-2));
  ASSERT_EQ(r, Integer(3));

  Integer::euclidianQR(q, r, -5, -4);
  ASSERT_EQ(q, Integer(2));
  ASSERT_EQ(r, Integer(3));
}

TEST_F(TestUtilBlackInteger, floorQR)
{
  Integer q, r;

  Integer::floorQR(q, r, 1, 4);
  ASSERT_EQ(q, Integer(0));
  ASSERT_EQ(r, Integer(1));

  Integer::floorQR(q, r, 1, -4);
  ASSERT_EQ(q, Integer(-1));
  ASSERT_EQ(r, Integer(-3));

  Integer::floorQR(q, r, -1, 4);
  ASSERT_EQ(q, Integer(-1));
  ASSERT_EQ(r, Integer(3));

  Integer::floorQR(q, r, -1, -4);
  ASSERT_EQ(q, Integer(0));
  ASSERT_EQ(r, Integer(-1));

  Integer::floorQR(q, r, 5, 4);
  ASSERT_EQ(q, Integer(1));
  ASSERT_EQ(r, Integer(1));

  Integer::floorQR(q, r, 5, -4);
  ASSERT_EQ(q, Integer(-2));
  ASSERT_EQ(r, Integer(-3));

  Integer::floorQR(q, r, -5, 4);
  ASSERT_EQ(q, Integer(-2));
  ASSERT_EQ(r, Integer(3));

  Integer::floorQR(q, r, -5, -4);
  ASSERT_EQ(q, Integer(1));
  ASSERT_EQ(r, Integer(-1));
}

TEST_F(TestUtilBlackInteger, leadingZeros)
{
  std::string leadingZeros(s_lots_of_leading_zeros);
  Integer one(1u);
  Integer one_from_string(leadingZeros, 2);
  ASSERT_EQ(one, one_from_string);
}

TEST_F(TestUtilBlackInteger, modAdd)
{
  for (uint32_t i = 0; i <= 10; ++i)
  {
    for (uint32_t j = 0; j <= 10; ++j)
    {
      Integer yy;
      Integer x(i);
      Integer y = x + j;
      Integer yp = x.modAdd(j, 3);
      for (yy = y; yy >= 3; yy -= 3)
        ;
      ASSERT_EQ(yp, yy);
      yp = x.modAdd(j, 7);
      for (yy = y; yy >= 7; yy -= 7)
        ;
      ASSERT_EQ(yp, yy);
      yp = x.modAdd(j, 11);
      for (yy = y; yy >= 11; yy -= 11)
        ;
      ASSERT_EQ(yp, yy);
    }
  }
}

TEST_F(TestUtilBlackInteger, modMultiply)
{
  for (uint32_t i = 0; i <= 10; ++i)
  {
    for (uint32_t j = 0; j <= 10; ++j)
    {
      Integer yy;
      Integer x(i);
      Integer y = x * j;
      Integer yp = x.modMultiply(j, 3);
      for (yy = y; yy >= 3; yy -= 3)
        ;
      ASSERT_EQ(yp, yy);
      yp = x.modMultiply(j, 7);
      for (yy = y; yy >= 7; yy -= 7)
        ;
      ASSERT_EQ(yp, yy);
      yp = x.modMultiply(j, 11);
      for (yy = y; yy >= 11; yy -= 11)
        ;
      ASSERT_EQ(yp, yy);
    }
  }
}

TEST_F(TestUtilBlackInteger, modInverse)
{
  for (uint32_t i = 0; i <= 10; ++i)
  {
    Integer x(i);
    Integer inv = x.modInverse(3);
    if (i == 0 || i == 3 || i == 6 || i == 9)
    {
      ASSERT_EQ(inv, -1); /* no inverse */
    }
    else
    {
      ASSERT_EQ(x.modMultiply(inv, 3), 1);
    }
    inv = x.modInverse(7);
    if (i == 0 || i == 7)
    {
      ASSERT_EQ(inv, -1); /* no inverse */
    }
    else
    {
      ASSERT_EQ(x.modMultiply(inv, 7), 1);
    }
    inv = x.modInverse(11);
    if (i == 0)
    {
      ASSERT_EQ(inv, -1); /* no inverse */
    }
    else
    {
      ASSERT_EQ(x.modMultiply(inv, 11), 1);
    }
  }
}
}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Tim King
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Black box testing of cvc5::Integer.
14		*/
15
16		#include <limits>
17		#include <sstream>
18
19		#include "base/exception.h"
20		#include "test.h"
21		#include "util/integer.h"
22
23		namespace cvc5 {
24		namespace test {
25
26	84	class TestUtilBlackInteger : public TestInternal
27		{
28		protected:
29	70	uint32_t internalLength(int32_t i)
30		{
31	70	if (i == 0)
32		{
33	2	return 1;
34		}
35		else
36		{
37	68	int32_t absi = i < 0 ? -i : i;
38	68	uint32_t n = 0;
39	68	int32_t powN = 1;
40	168	do
41		{
42	236	powN <<= 1;
43	236	++n;
44	236	} while (absi >= powN);
45	68	return n;
46		}
47		}
48		static const char* s_large_val;
49		static const char* s_lots_of_leading_zeros;
50		};
51
52		const char* TestUtilBlackInteger::s_large_val =
53		"4547897890548754897897897897890789078907890";
54		const char* TestUtilBlackInteger::s_lots_of_leading_zeros =
55		"00000000000000000000000000000000000000000000000000000000000000000000000000"
56		"000000000000000000000000000000000000000000000000000000000000000000000001";
57
58	30	TEST_F(TestUtilBlackInteger, constructors)
59		{
60	4	Integer z0(1);
61	2	ASSERT_EQ(z0.getLong(), 1);
62
63	4	Integer z1(0);
64	2	ASSERT_EQ(z1.getLong(), 0);
65
66	4	Integer z2(-1);
67	2	ASSERT_EQ(z2.getLong(), -1);
68
69	4	Integer z3(0x890UL);
70	2	ASSERT_EQ(z3.getUnsignedLong(), 0x890UL);
71
72	4	Integer z4;
73	2	ASSERT_EQ(z4.getLong(), 0);
74
75	4	Integer z5("7896890");
76	2	ASSERT_EQ(z5.getUnsignedLong(), 7896890ul);
77
78	4	Integer z6(z5);
79	2	ASSERT_EQ(z5.getUnsignedLong(), 7896890ul);
80	2	ASSERT_EQ(z6.getUnsignedLong(), 7896890ul);
81
82	4	std::string bigValue("1536729");
83	4	Integer z7(bigValue);
84	2	ASSERT_EQ(z7.getUnsignedLong(), 1536729ul);
85		}
86
87	30	TEST_F(TestUtilBlackInteger, compare_against_zero)
88		{
89	4	Integer z(0);
90	2	ASSERT_NO_THROW((void)(z == 0););
91	2	ASSERT_EQ(z, 0);
92		}
93
94	30	TEST_F(TestUtilBlackInteger, operator_assign)
95		{
96	4	Integer x(0);
97	4	Integer y(79);
98	4	Integer z(45789);
99
100	2	ASSERT_EQ(x.getUnsignedLong(), 0ul);
101	2	ASSERT_EQ(y.getUnsignedLong(), 79ul);
102	2	ASSERT_EQ(z.getUnsignedLong(), 45789ul);
103
104	2	x = y = z;
105
106	2	ASSERT_EQ(x.getUnsignedLong(), 45789ul);
107	2	ASSERT_EQ(y.getUnsignedLong(), 45789ul);
108	2	ASSERT_EQ(z.getUnsignedLong(), 45789ul);
109
110	4	Integer a(2);
111
112	2	y = a;
113
114	2	ASSERT_EQ(a.getUnsignedLong(), 2ul);
115	2	ASSERT_EQ(y.getUnsignedLong(), 2ul);
116	2	ASSERT_EQ(x.getUnsignedLong(), 45789ul);
117	2	ASSERT_EQ(z.getUnsignedLong(), 45789ul);
118		}
119
120	30	TEST_F(TestUtilBlackInteger, operator_equals)
121		{
122	4	Integer a(0);
123	4	Integer b(79);
124	4	Integer c("79");
125	4	Integer d;
126
127	2	ASSERT_TRUE(a == a);
128	2	ASSERT_FALSE(a == b);
129	2	ASSERT_FALSE(a == c);
130	2	ASSERT_TRUE(a == d);
131
132	2	ASSERT_FALSE(b == a);
133	2	ASSERT_TRUE(b == b);
134	2	ASSERT_TRUE(b == c);
135	2	ASSERT_FALSE(b == d);
136
137	2	ASSERT_FALSE(c == a);
138	2	ASSERT_TRUE(c == b);
139	2	ASSERT_TRUE(c == c);
140	2	ASSERT_FALSE(c == d);
141
142	2	ASSERT_TRUE(d == a);
143	2	ASSERT_FALSE(d == b);
144	2	ASSERT_FALSE(d == c);
145	2	ASSERT_TRUE(d == d);
146		}
147
148	30	TEST_F(TestUtilBlackInteger, operator_not_equals)
149		{
150	4	Integer a(0);
151	4	Integer b(79);
152	4	Integer c("79");
153	4	Integer d;
154
155	2	ASSERT_FALSE(a != a);
156	2	ASSERT_TRUE(a != b);
157	2	ASSERT_TRUE(a != c);
158	2	ASSERT_FALSE(a != d);
159
160	2	ASSERT_TRUE(b != a);
161	2	ASSERT_FALSE(b != b);
162	2	ASSERT_FALSE(b != c);
163	2	ASSERT_TRUE(b != d);
164
165	2	ASSERT_TRUE(c != a);
166	2	ASSERT_FALSE(c != b);
167	2	ASSERT_FALSE(c != c);
168	2	ASSERT_TRUE(c != d);
169
170	2	ASSERT_FALSE(d != a);
171	2	ASSERT_TRUE(d != b);
172	2	ASSERT_TRUE(d != c);
173	2	ASSERT_FALSE(d != d);
174		}
175
176	30	TEST_F(TestUtilBlackInteger, operator_subtract)
177		{
178	4	Integer x(0);
179	4	Integer y(79);
180	4	Integer z(-34);
181
182	4	Integer act0 = x - x;
183	4	Integer act1 = x - y;
184	4	Integer act2 = x - z;
185	4	Integer exp0(0);
186	4	Integer exp1(-79);
187	4	Integer exp2(34);
188
189	4	Integer act3 = y - x;
190	4	Integer act4 = y - y;
191	4	Integer act5 = y - z;
192	4	Integer exp3(79);
193	4	Integer exp4(0);
194	4	Integer exp5(113);
195
196	4	Integer act6 = z - x;
197	4	Integer act7 = z - y;
198	4	Integer act8 = z - z;
199	4	Integer exp6(-34);
200	4	Integer exp7(-113);
201	4	Integer exp8(0);
202
203	2	ASSERT_EQ(act0, exp0);
204	2	ASSERT_EQ(act1, exp1);
205	2	ASSERT_EQ(act2, exp2);
206	2	ASSERT_EQ(act3, exp3);
207	2	ASSERT_EQ(act4, exp4);
208	2	ASSERT_EQ(act5, exp5);
209	2	ASSERT_EQ(act6, exp6);
210	2	ASSERT_EQ(act7, exp7);
211	2	ASSERT_EQ(act8, exp8);
212		}
213
214	30	TEST_F(TestUtilBlackInteger, operator_add)
215		{
216	4	Integer x(0);
217	4	Integer y(79);
218	4	Integer z(-34);
219
220	4	Integer act0 = x + x;
221	4	Integer act1 = x + y;
222	4	Integer act2 = x + z;
223	4	Integer exp0(0);
224	4	Integer exp1(79);
225	4	Integer exp2(-34);
226
227	4	Integer act3 = y + x;
228	4	Integer act4 = y + y;
229	4	Integer act5 = y + z;
230	4	Integer exp3(79);
231	4	Integer exp4(158);
232	4	Integer exp5(45);
233
234	4	Integer act6 = z + x;
235	4	Integer act7 = z + y;
236	4	Integer act8 = z + z;
237	4	Integer exp6(-34);
238	4	Integer exp7(45);
239	4	Integer exp8(-68);
240
241	2	ASSERT_EQ(act0, exp0);
242	2	ASSERT_EQ(act1, exp1);
243	2	ASSERT_EQ(act2, exp2);
244	2	ASSERT_EQ(act3, exp3);
245	2	ASSERT_EQ(act4, exp4);
246	2	ASSERT_EQ(act5, exp5);
247	2	ASSERT_EQ(act6, exp6);
248	2	ASSERT_EQ(act7, exp7);
249	2	ASSERT_EQ(act8, exp8);
250		}
251
252	30	TEST_F(TestUtilBlackInteger, operator_mult)
253		{
254	4	Integer x(0);
255	4	Integer y(79);
256	4	Integer z(-34);
257
258	4	Integer act0 = x * x;
259	4	Integer act1 = x * y;
260	4	Integer act2 = x * z;
261	4	Integer exp0(0);
262	4	Integer exp1(0);
263	4	Integer exp2(0);
264
265	4	Integer act3 = y * x;
266	4	Integer act4 = y * y;
267	4	Integer act5 = y * z;
268	4	Integer exp3(0);
269	4	Integer exp4(6241);
270	4	Integer exp5(-2686);
271
272	4	Integer act6 = z * x;
273	4	Integer act7 = z * y;
274	4	Integer act8 = z * z;
275	4	Integer exp6(0);
276	4	Integer exp7(-2686);
277	4	Integer exp8(1156);
278
279	2	ASSERT_EQ(act0, exp0);
280	2	ASSERT_EQ(act1, exp1);
281	2	ASSERT_EQ(act2, exp2);
282	2	ASSERT_EQ(act3, exp3);
283	2	ASSERT_EQ(act4, exp4);
284	2	ASSERT_EQ(act5, exp5);
285	2	ASSERT_EQ(act6, exp6);
286	2	ASSERT_EQ(act7, exp7);
287	2	ASSERT_EQ(act8, exp8);
288		}
289
290	30	TEST_F(TestUtilBlackInteger, to_string)
291		{
292	4	std::stringstream ss;
293	4	Integer large(s_large_val);
294	2	ss << large;
295	4	std::string res = ss.str();
296
297	2	ASSERT_EQ(res, large.toString());
298		}
299
300	30	TEST_F(TestUtilBlackInteger, base_inference)
301		{
302	2	ASSERT_EQ(Integer("0xa", 0), 10);
303	2	ASSERT_EQ(Integer("0xff", 0), 255);
304	2	ASSERT_EQ(Integer("011", 0), 9);
305	2	ASSERT_EQ(Integer("0b1010", 0), 10);
306	2	ASSERT_EQ(Integer("-1", 0), -1);
307	2	ASSERT_EQ(Integer("42", 0), 42);
308		}
309
310	30	TEST_F(TestUtilBlackInteger, parse_errors)
311		{
312	4	ASSERT_THROW(Integer("abracadabra"), std::invalid_argument);
313	4	ASSERT_THROW(Integer("+-1"), std::invalid_argument);
314	4	ASSERT_THROW(Integer("-+1"), std::invalid_argument);
315	4	ASSERT_THROW(Integer("5i"), std::invalid_argument);
316	4	ASSERT_THROW(Integer("10xyz"), std::invalid_argument);
317	4	ASSERT_THROW(Integer("0xff", 10), std::invalid_argument);
318	4	ASSERT_THROW(Integer("#x5", 0), std::invalid_argument);
319	4	ASSERT_THROW(Integer("0b123", 0), std::invalid_argument);
320		}
321
322	30	TEST_F(TestUtilBlackInteger, pow)
323		{
324	2	ASSERT_EQ(Integer(1), Integer(1).pow(0));
325	2	ASSERT_EQ(Integer(1), Integer(5).pow(0));
326	2	ASSERT_EQ(Integer(1), Integer(-1).pow(0));
327	2	ASSERT_EQ(Integer(0), Integer(0).pow(1));
328	2	ASSERT_EQ(Integer(5), Integer(5).pow(1));
329	2	ASSERT_EQ(Integer(-5), Integer(-5).pow(1));
330	2	ASSERT_EQ(Integer(16), Integer(2).pow(4));
331	2	ASSERT_EQ(Integer(16), Integer(-2).pow(4));
332	2	ASSERT_EQ(Integer(1000), Integer(10).pow(3));
333	2	ASSERT_EQ(Integer(-1000), Integer(-10).pow(3));
334		}
335
336	30	TEST_F(TestUtilBlackInteger, overly_long)
337		{
338	2	uint64_t ul = std::numeric_limits<uint64_t>::max();
339	4	Integer i(ul);
340	2	ASSERT_EQ(i.getUnsignedLong(), ul);
341	4	ASSERT_THROW(i.getLong(), IllegalArgumentException);
342	2	uint64_t ulplus1 = ul + 1;
343	2	ASSERT_EQ(ulplus1, 0);
344	2	i = i + 1;
345	4	ASSERT_THROW(i.getUnsignedLong(), IllegalArgumentException);
346		}
347
348	30	TEST_F(TestUtilBlackInteger, testBit)
349		{
350	2	ASSERT_FALSE(Integer(0).testBit(6));
351	2	ASSERT_FALSE(Integer(0).testBit(5));
352	2	ASSERT_FALSE(Integer(0).testBit(4));
353	2	ASSERT_FALSE(Integer(0).testBit(3));
354	2	ASSERT_FALSE(Integer(0).testBit(2));
355	2	ASSERT_FALSE(Integer(0).testBit(1));
356	2	ASSERT_FALSE(Integer(0).testBit(0));
357
358	2	ASSERT_TRUE(Integer(-1).testBit(6));
359	2	ASSERT_TRUE(Integer(-1).testBit(5));
360	2	ASSERT_TRUE(Integer(-1).testBit(4));
361	2	ASSERT_TRUE(Integer(-1).testBit(3));
362	2	ASSERT_TRUE(Integer(-1).testBit(2));
363	2	ASSERT_TRUE(Integer(-1).testBit(1));
364	2	ASSERT_TRUE(Integer(-1).testBit(0));
365
366	2	ASSERT_FALSE(Integer(10).testBit(6));
367	2	ASSERT_FALSE(Integer(10).testBit(5));
368	2	ASSERT_FALSE(Integer(10).testBit(4));
369	2	ASSERT_TRUE(Integer(10).testBit(3));
370	2	ASSERT_FALSE(Integer(10).testBit(2));
371	2	ASSERT_TRUE(Integer(10).testBit(1));
372	2	ASSERT_FALSE(Integer(10).testBit(0));
373
374	2	ASSERT_FALSE(Integer(14).testBit(6));
375	2	ASSERT_FALSE(Integer(14).testBit(5));
376	2	ASSERT_FALSE(Integer(14).testBit(4));
377	2	ASSERT_TRUE(Integer(14).testBit(3));
378	2	ASSERT_TRUE(Integer(14).testBit(2));
379	2	ASSERT_TRUE(Integer(14).testBit(1));
380	2	ASSERT_FALSE(Integer(14).testBit(0));
381
382	2	ASSERT_TRUE(Integer(64).testBit(6));
383	2	ASSERT_FALSE(Integer(64).testBit(5));
384	2	ASSERT_FALSE(Integer(64).testBit(4));
385	2	ASSERT_FALSE(Integer(64).testBit(3));
386	2	ASSERT_FALSE(Integer(64).testBit(2));
387	2	ASSERT_FALSE(Integer(64).testBit(1));
388	2	ASSERT_FALSE(Integer(64).testBit(0));
389		}
390
391	30	TEST_F(TestUtilBlackInteger, length)
392		{
393	72	for (int32_t i = -17; i <= 17; ++i)
394		{
395	70	ASSERT_EQ(Integer(i).length(), internalLength(i));
396		}
397		}
398
399	30	TEST_F(TestUtilBlackInteger, euclidianQR)
400		{
401	4	Integer q, r;
402
403	2	Integer::euclidianQR(q, r, 1, 4);
404	2	ASSERT_EQ(q, Integer(0));
405	2	ASSERT_EQ(r, Integer(1));
406
407	2	Integer::euclidianQR(q, r, 1, -4);
408	2	ASSERT_EQ(q, Integer(0));
409	2	ASSERT_EQ(r, Integer(1));
410
411	2	Integer::euclidianQR(q, r, -1, 4);
412	2	ASSERT_EQ(q, Integer(-1));
413	2	ASSERT_EQ(r, Integer(3));
414
415	2	Integer::euclidianQR(q, r, -1, -4);
416	2	ASSERT_EQ(q, Integer(1));
417	2	ASSERT_EQ(r, Integer(3));
418
419	2	Integer::euclidianQR(q, r, 5, 4);
420	2	ASSERT_EQ(q, Integer(1));
421	2	ASSERT_EQ(r, Integer(1));
422
423	2	Integer::euclidianQR(q, r, 5, -4);
424	2	ASSERT_EQ(q, Integer(-1));
425	2	ASSERT_EQ(r, Integer(1));
426
427	2	Integer::euclidianQR(q, r, -5, 4);
428	2	ASSERT_EQ(q, Integer(-2));
429	2	ASSERT_EQ(r, Integer(3));
430
431	2	Integer::euclidianQR(q, r, -5, -4);
432	2	ASSERT_EQ(q, Integer(2));
433	2	ASSERT_EQ(r, Integer(3));
434		}
435
436	30	TEST_F(TestUtilBlackInteger, floorQR)
437		{
438	4	Integer q, r;
439
440	2	Integer::floorQR(q, r, 1, 4);
441	2	ASSERT_EQ(q, Integer(0));
442	2	ASSERT_EQ(r, Integer(1));
443
444	2	Integer::floorQR(q, r, 1, -4);
445	2	ASSERT_EQ(q, Integer(-1));
446	2	ASSERT_EQ(r, Integer(-3));
447
448	2	Integer::floorQR(q, r, -1, 4);
449	2	ASSERT_EQ(q, Integer(-1));
450	2	ASSERT_EQ(r, Integer(3));
451
452	2	Integer::floorQR(q, r, -1, -4);
453	2	ASSERT_EQ(q, Integer(0));
454	2	ASSERT_EQ(r, Integer(-1));
455
456	2	Integer::floorQR(q, r, 5, 4);
457	2	ASSERT_EQ(q, Integer(1));
458	2	ASSERT_EQ(r, Integer(1));
459
460	2	Integer::floorQR(q, r, 5, -4);
461	2	ASSERT_EQ(q, Integer(-2));
462	2	ASSERT_EQ(r, Integer(-3));
463
464	2	Integer::floorQR(q, r, -5, 4);
465	2	ASSERT_EQ(q, Integer(-2));
466	2	ASSERT_EQ(r, Integer(3));
467
468	2	Integer::floorQR(q, r, -5, -4);
469	2	ASSERT_EQ(q, Integer(1));
470	2	ASSERT_EQ(r, Integer(-1));
471		}
472
473	30	TEST_F(TestUtilBlackInteger, leadingZeros)
474		{
475	4	std::string leadingZeros(s_lots_of_leading_zeros);
476	4	Integer one(1u);
477	4	Integer one_from_string(leadingZeros, 2);
478	2	ASSERT_EQ(one, one_from_string);
479		}
480
481	30	TEST_F(TestUtilBlackInteger, modAdd)
482		{
483	24	for (uint32_t i = 0; i <= 10; ++i)
484		{
485	264	for (uint32_t j = 0; j <= 10; ++j)
486		{
487	484	Integer yy;
488	484	Integer x(i);
489	484	Integer y = x + j;
490	484	Integer yp = x.modAdd(j, 3);
491	242	for (yy = y; yy >= 3; yy -= 3)
492		;
493	242	ASSERT_EQ(yp, yy);
494	242	yp = x.modAdd(j, 7);
495	242	for (yy = y; yy >= 7; yy -= 7)
496		;
497	242	ASSERT_EQ(yp, yy);
498	242	yp = x.modAdd(j, 11);
499	242	for (yy = y; yy >= 11; yy -= 11)
500		;
501	242	ASSERT_EQ(yp, yy);
502		}
503		}
504		}
505
506	30	TEST_F(TestUtilBlackInteger, modMultiply)
507		{
508	24	for (uint32_t i = 0; i <= 10; ++i)
509		{
510	264	for (uint32_t j = 0; j <= 10; ++j)
511		{
512	484	Integer yy;
513	484	Integer x(i);
514	484	Integer y = x * j;
515	484	Integer yp = x.modMultiply(j, 3);
516	242	for (yy = y; yy >= 3; yy -= 3)
517		;
518	242	ASSERT_EQ(yp, yy);
519	242	yp = x.modMultiply(j, 7);
520	242	for (yy = y; yy >= 7; yy -= 7)
521		;
522	242	ASSERT_EQ(yp, yy);
523	242	yp = x.modMultiply(j, 11);
524	242	for (yy = y; yy >= 11; yy -= 11)
525		;
526	242	ASSERT_EQ(yp, yy);
527		}
528		}
529		}
530
531	30	TEST_F(TestUtilBlackInteger, modInverse)
532		{
533	24	for (uint32_t i = 0; i <= 10; ++i)
534		{
535	44	Integer x(i);
536	44	Integer inv = x.modInverse(3);
537	22	if (i == 0 \|\| i == 3 \|\| i == 6 \|\| i == 9)
538		{
539	8	ASSERT_EQ(inv, -1); /* no inverse */
540		}
541		else
542		{
543	14	ASSERT_EQ(x.modMultiply(inv, 3), 1);
544		}
545	22	inv = x.modInverse(7);
546	22	if (i == 0 \|\| i == 7)
547		{
548	4	ASSERT_EQ(inv, -1); /* no inverse */
549		}
550		else
551		{
552	18	ASSERT_EQ(x.modMultiply(inv, 7), 1);
553		}
554	22	inv = x.modInverse(11);
555	22	if (i == 0)
556		{
557	2	ASSERT_EQ(inv, -1); /* no inverse */
558		}
559		else
560		{
561	20	ASSERT_EQ(x.modMultiply(inv, 11), 1);
562		}
563		}
564		}
565		} // namespace test
566	66	} // namespace cvc5