1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * Test of integer division implemented in rationals.c
21 */
22
23 #include <stdio.h>
24 #include <inttypes.h>
25
26 #include "terms/rationals.h"
27
28
29 /*
30 * Table to initialize large numbers
31 */
32 #define NBIGS 16
33
34 static char* large_signed[NBIGS] = {
35 "1073741822",
36 "1073741823",
37 "1073741824",
38 "1073741825",
39 "-1073741822",
40 "-1073741823",
41 "-1073741824",
42 "-1073741825",
43 "3219483903484189430",
44 "-321948390344899848",
45 "219483903484189430",
46 "-21948390344899848",
47 "+100000000000",
48 "-100000000000",
49 "+80000000000000",
50 "-80000000000000"
51 };
52
53 // divisors must all be positive
54 static char* large_divisor[NBIGS] = {
55 "1073741822",
56 "1073741823",
57 "1073741824",
58 "1073741825",
59 "1073741826",
60 "1073741827",
61 "1073741828",
62 "3219483903484189430",
63 "219483903484189430",
64 "100000000000",
65 "50000000000",
66 "20000000000",
67 "80000000000000",
68 "40000000000000",
69 "20000000000000",
70 "10000000000000",
71 };
72
73
74 /*
75 * Test 1: a divided by b
76 * - both a and b are small integers
77 */
test_small_small(void)78 static void test_small_small(void) {
79 rational_t a, b, c;
80 int32_t x, y;
81
82 q_init(&a);
83 q_init(&b);
84 q_init(&c);
85
86 for (y=1; y<8; y++) {
87 q_set32(&b, y);
88 for (x=-20; x<=20; x++) {
89 q_set32(&a, x);
90 q_integer_div(&a, &b);
91 q_set32(&c, x);
92 q_integer_rem(&c, &b);
93
94 printf("div[%3"PRId32", %"PRId32"]: quotient = ", x, y);
95 q_print(stdout, &a);
96 printf(", remainder = ");
97 q_print(stdout, &c);
98 printf("\n");
99 }
100 printf("\n");
101 }
102
103 q_clear(&a);
104 q_clear(&b);
105 q_clear(&c);
106 }
107
108
109 /*
110 * Test 2: a is large, b is small
111 */
test_big_small(void)112 static void test_big_small(void) {
113 rational_t a, b, c;
114 uint32_t i;
115 int32_t y;
116
117 q_init(&a);
118 q_init(&b);
119 q_init(&c);
120
121 for (y=1; y<8; y++) {
122 q_set32(&b, y);
123 for (i=0; i<NBIGS; i++) {
124 q_set_from_string(&a, large_signed[i]);
125 q_set(&c, &a);
126 q_integer_div(&a, &b);
127 q_integer_rem(&c, &b);
128
129 printf("div[%s, %"PRId32"]: quotient = ", large_signed[i], y);
130 q_print(stdout, &a);
131 printf(", remainder = ");
132 q_print(stdout, &c);
133 printf("\n");
134 }
135 printf("\n");
136 }
137
138 q_clear(&a);
139 q_clear(&b);
140 q_clear(&c);
141 }
142
143 /*
144 * Test 3: a is small, b is large
145 */
test_small_big(void)146 static void test_small_big(void) {
147 rational_t a, b, c;
148 uint32_t i;
149 int32_t x;
150
151 q_init(&a);
152 q_init(&b);
153 q_init(&c);
154
155 for (i=0; i<NBIGS; i++) {
156 q_set_from_string(&b, large_divisor[i]);
157 for (x=-10; x<=10; x++) {
158 q_set32(&a, x);
159 q_set32(&c, x);
160 q_integer_div(&a, &b);
161 q_integer_rem(&c, &b);
162
163 printf("div[%"PRId32", %s]: quotient = ", x, large_divisor[i]);
164 q_print(stdout, &a);
165 printf(", remainder = ");
166 q_print(stdout, &c);
167 printf("\n");
168 }
169 printf("\n");
170 }
171
172 q_clear(&a);
173 q_clear(&b);
174 q_clear(&c);
175 }
176
177
178 /*
179 * Test 4: a is large, b is large
180 */
test_big_big(void)181 static void test_big_big(void) {
182 rational_t a, b, c;
183 uint32_t i, j;
184
185 q_init(&a);
186 q_init(&b);
187 q_init(&c);
188
189 for (i=0; i<NBIGS; i++) {
190 q_set_from_string(&b, large_divisor[i]);
191 for (j=0; j<NBIGS; j++) {
192 q_set_from_string(&a, large_signed[j]);
193 q_set(&c, &a);
194 q_integer_div(&a, &b);
195 q_integer_rem(&c, &b);
196
197 printf("div[%s, %s]: quotient = ", large_signed[j], large_divisor[i]);
198 q_print(stdout, &a);
199 printf(", remainder = ");
200 q_print(stdout, &c);
201 printf("\n");
202 }
203 printf("\n");
204 }
205
206 q_clear(&a);
207 q_clear(&b);
208 q_clear(&c);
209 }
210
main(void)211 int main(void) {
212 init_rationals();
213 test_small_small();
214 test_big_small();
215 test_small_big();
216 test_big_big();
217 cleanup_rationals();
218 return 0;
219 }
220