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#include <stdio.h>
20#include <inttypes.h>
21
22#include "bv_constants.h"
23#include "bitvectors.h"
24#include "bvpoly_buffer.h"
25
26
27
28/*
29 * Print monomial a * x
30 * n = number of bits used
31 */
32static void print_mono64(uint64_t a, thvar_t x, uint32_t n) {
33  assert(0 < n && n <= 64);
34
35  printf("0b");
36  do {
37    n --;
38    if ((a & (((uint64_t) 1) << n)) == 0) {
39      printf("0");
40    } else {
41      printf("1");
42    }
43  } while (n > 0);
44
45  if (x != const_idx) {
46    printf(" * u!%"PRId32, x);
47  }
48}
49
50
51/*
52 * Same thing for a large constant a
53 */
54static void print_monomial(uint32_t *a, thvar_t x, uint32_t n) {
55  assert(n > 64);
56
57  bvconst_print(stdout, a, n);
58  if (x != const_idx) {
59    printf(" * u!%"PRId32, x);
60  }
61}
62
63
64/*
65 * Print 0 in binary format. n = number of bits
66 */
67static void print_zero(uint32_t n) {
68  printf("0b");
69  while (n > 0) {
70    printf("0");
71    n --;
72  }
73}
74
75
76/*
77 * Print the content of buffer
78 * - if use_signs is true, take the bit-signs into account
79 */
80static void print_bvpoly_buffer(bvpoly_buffer_t *buffer, bool use_signs) {
81  uint32_t i, n, b;
82
83  b = buffer->bitsize;
84  n = buffer->nterms;
85  if (n == 0) {
86    print_zero(b);
87  } else if (b <= 64) {
88    if (use_signs && tst_bit(buffer->sign, 0)) {
89      printf("- ");
90    }
91    print_mono64(buffer->c[0], buffer->var[0], b);
92    for (i=1; i<n; i++) {
93      if (use_signs && tst_bit(buffer->sign, i)) {
94	printf(" - ");
95      } else {
96	printf(" + ");
97      }
98      print_mono64(buffer->c[i], buffer->var[i], b);
99    }
100  } else {
101    if (use_signs && tst_bit(buffer->sign, 0)) {
102      printf("- ");
103    }
104    print_monomial(buffer->p[0], buffer->var[0], b);
105    for (i=1; i<n; i++) {
106      if (use_signs && tst_bit(buffer->sign, i)) {
107	printf(" - ");
108      } else {
109	printf(" + ");
110      }
111      print_monomial(buffer->p[i], buffer->var[i], b);
112    }
113  }
114  fflush(stdout);
115}
116
117
118
119
120
121/*
122 * Test1: buffer with small constants
123 */
124static void test1(bvpoly_buffer_t *buffer) {
125  printf("\n"
126         "******************\n"
127         "*     TEST 1     *\n"
128         "******************\n\n");
129
130  reset_bvpoly_buffer(buffer, 8);
131  printf("---> reset: size 8\n");
132  print_bvpoly_buffer(buffer, false);
133  printf("\n");
134
135  bvpoly_buffer_add_mono64(buffer, 3, 255);
136  bvpoly_buffer_add_mono64(buffer, 1, 63);
137  bvpoly_buffer_add_const64(buffer, 1);
138  bvpoly_buffer_sub_mono64(buffer, 2, 3);
139
140  printf("---> 255 * u!3 + 63 * u!1 + 1 - 3 * u!2\n");
141  print_bvpoly_buffer(buffer, false);
142  printf("\n");
143
144  normalize_bvpoly_buffer(buffer);
145  printf("---> normalized\n");
146  print_bvpoly_buffer(buffer, true);
147  printf("\n\n");
148
149  reset_bvpoly_buffer(buffer, 10);
150  printf("---> reset: size 10\n");
151  print_bvpoly_buffer(buffer, false);
152  printf("\n");
153
154  bvpoly_buffer_sub_mono64(buffer, 7, 1);
155  bvpoly_buffer_add_mono64(buffer, 5, 1);
156  bvpoly_buffer_add_mono64(buffer, 3, 2);
157  bvpoly_buffer_sub_mono64(buffer, 1, 4);
158  bvpoly_buffer_add_mono64(buffer, 3, 2);
159  bvpoly_buffer_add_mono64(buffer, 7, 1);
160
161  printf("---> - u!7 + u!5 + 2 * u!3 - 4 * u!1 + 2 * u!3 + u!7\n");
162  print_bvpoly_buffer(buffer, false);
163  printf("\n");
164
165  normalize_bvpoly_buffer(buffer);
166  printf("---> normalized\n");
167  print_bvpoly_buffer(buffer, true);
168  printf("\n\n");
169
170  reset_bvpoly_buffer(buffer, 10);
171  printf("---> reset: size 10\n");
172  print_bvpoly_buffer(buffer, false);
173  printf("\n");
174
175  bvpoly_buffer_add_mono64(buffer, 1, 1);
176  bvpoly_buffer_add_mono64(buffer, 2, 2);
177  bvpoly_buffer_add_mono64(buffer, 3, 4);
178  bvpoly_buffer_add_mono64(buffer, 4, 8);
179  bvpoly_buffer_add_mono64(buffer, 5, 16);
180  bvpoly_buffer_add_mono64(buffer, 6, 32);
181  bvpoly_buffer_add_mono64(buffer, 10, 512);
182  bvpoly_buffer_add_mono64(buffer, 9, 256);
183  bvpoly_buffer_add_mono64(buffer, 8, 128);
184  bvpoly_buffer_add_mono64(buffer, 7, 64);
185
186  printf("---> u!1 + 2 u!2 + 4 u!3 + 8 u!4 + 16 u!5 + 32 u!6 + 512 u!10 + 256 u!9 + 128 u!8 + 64 u!7\n");
187  print_bvpoly_buffer(buffer, false);
188  printf("\n");
189
190  normalize_bvpoly_buffer(buffer);
191  printf("---> normalized\n");
192  print_bvpoly_buffer(buffer, true);
193  printf("\n\n");
194
195  reset_bvpoly_buffer(buffer, 10);
196  printf("---> reset: size 10\n");
197  print_bvpoly_buffer(buffer, false);
198  printf("\n");
199
200  bvpoly_buffer_sub_var(buffer, 12);
201  bvpoly_buffer_add_var(buffer, 10);
202  bvpoly_buffer_add_var(buffer, 10);
203  printf("---> - u!12 + u!10 + u!10\n");
204  print_bvpoly_buffer(buffer, false);
205  printf("\n");
206
207  normalize_bvpoly_buffer(buffer);
208  printf("---> normalized\n");
209  print_bvpoly_buffer(buffer, true);
210  printf("\n\n");
211
212
213  reset_bvpoly_buffer(buffer, 32);
214  printf("---> reset: size 32\n");
215  print_bvpoly_buffer(buffer, false);
216  printf("\n");
217
218  normalize_bvpoly_buffer(buffer);
219  printf("---> normalized\n");
220  print_bvpoly_buffer(buffer, true);
221  printf("\n\n");
222
223  bvpoly_buffer_add_var(buffer, 1);
224  printf("---> add var u!1\n");
225  print_bvpoly_buffer(buffer, false);
226  printf("\n");
227
228  normalize_bvpoly_buffer(buffer);
229  printf("---> normalized\n");
230  print_bvpoly_buffer(buffer, true);
231  printf("\n\n");
232
233  bvpoly_buffer_sub_const64(buffer, 1);
234  printf("---> sub const 1\n");
235  print_bvpoly_buffer(buffer, false);
236  printf("\n");
237
238  normalize_bvpoly_buffer(buffer);
239  printf("---> normalized\n");
240  print_bvpoly_buffer(buffer, true);
241  printf("\n\n");
242
243}
244
245
246/*
247 * Test2: buffer with large constants
248 */
249static void test2(bvpoly_buffer_t *buffer) {
250  uint32_t aux[10]; // enough for 320 bits
251
252  printf("\n"
253         "******************\n"
254         "*     TEST 2     *\n"
255         "******************\n\n");
256
257  reset_bvpoly_buffer(buffer, 80);
258  printf("---> reset: size 80\n");
259  print_bvpoly_buffer(buffer, false);
260  printf("\n");
261
262  // width = 3
263  bvconst_set32(aux, 3, 255);
264  bvpoly_buffer_add_monomial(buffer, 3, aux);
265  bvconst_set32(aux, 3, 63);
266  bvpoly_buffer_add_monomial(buffer, 1, aux);
267  bvconst_set32(aux, 3, 1);
268  bvpoly_buffer_add_constant(buffer, aux);
269  bvconst_set32(aux, 3, 3);
270  bvpoly_buffer_sub_monomial(buffer, 2, aux);
271
272  printf("---> 255 * u!3 + 63 * u!1 + 1 - 3 * u!2\n");
273  print_bvpoly_buffer(buffer, false);
274  printf("\n");
275
276  normalize_bvpoly_buffer(buffer);
277  printf("---> normalized\n");
278  print_bvpoly_buffer(buffer, true);
279  printf("\n\n");
280
281  reset_bvpoly_buffer(buffer, 100);
282  printf("---> reset: size 100\n");
283  print_bvpoly_buffer(buffer, false);
284  printf("\n");
285
286  // width = 4
287  bvconst_set32(aux, 4, 1);
288  bvpoly_buffer_sub_monomial(buffer, 7, aux);
289  bvconst_set32(aux, 4, 1);
290  bvpoly_buffer_add_monomial(buffer, 5, aux);
291  bvconst_set32(aux, 4, 2);
292  bvpoly_buffer_add_monomial(buffer, 3, aux);
293  bvconst_set32(aux, 4, 4);
294  bvpoly_buffer_sub_monomial(buffer, 1, aux);
295  bvconst_set32(aux, 4, 2);
296  bvpoly_buffer_add_monomial(buffer, 3, aux);
297  bvconst_set_one(aux, 4);
298  bvpoly_buffer_add_monomial(buffer, 7, aux);
299
300  printf("---> - u!7 + u!5 + 2 * u!3 - 4 * u!1 + 2 * u!3 + u!7\n");
301  print_bvpoly_buffer(buffer, false);
302  printf("\n");
303
304  normalize_bvpoly_buffer(buffer);
305  printf("---> normalized\n");
306  print_bvpoly_buffer(buffer, true);
307  printf("\n\n");
308
309  reset_bvpoly_buffer(buffer, 65);
310  printf("---> reset: size 65\n");
311  print_bvpoly_buffer(buffer, false);
312  printf("\n");
313
314  // width = 3
315  bvconst_set32(aux, 3, 1);
316  bvpoly_buffer_add_monomial(buffer, 1, aux);
317  bvconst_set32(aux, 3, 2);
318  bvpoly_buffer_add_monomial(buffer, 2, aux);
319  bvconst_set32(aux, 3, 4);
320  bvpoly_buffer_add_monomial(buffer, 3, aux);
321  bvconst_set32(aux, 3, 8);
322  bvpoly_buffer_add_monomial(buffer, 4, aux);
323  bvconst_set32(aux, 3, 16);
324  bvpoly_buffer_add_monomial(buffer, 5, aux);
325  bvconst_set32(aux, 3, 32);
326  bvpoly_buffer_add_monomial(buffer, 6, aux);
327  bvconst_set32(aux, 3, 512);
328  bvpoly_buffer_add_monomial(buffer, 10, aux);
329  bvconst_set32(aux, 3, 256);
330  bvpoly_buffer_add_monomial(buffer, 9, aux);
331  bvconst_set32(aux, 3, 128);
332  bvpoly_buffer_add_monomial(buffer, 8, aux);
333  bvconst_set32(aux, 3, 64);
334  bvpoly_buffer_add_monomial(buffer, 7, aux);
335
336  printf("---> u!1 + 2 u!2 + 4 u!3 + 8 u!4 + 16 u!5 + 32 u!6 + 512 u!10 + 256 u!9 + 128 u!8 + 64 u!7\n");
337  print_bvpoly_buffer(buffer, false);
338  printf("\n");
339
340  normalize_bvpoly_buffer(buffer);
341  printf("---> normalized\n");
342  print_bvpoly_buffer(buffer, true);
343  printf("\n\n");
344
345  reset_bvpoly_buffer(buffer, 100);
346  printf("---> reset: size 100\n");
347  print_bvpoly_buffer(buffer, false);
348  printf("\n");
349
350  bvpoly_buffer_sub_var(buffer, 12);
351  bvpoly_buffer_add_var(buffer, 10);
352  bvpoly_buffer_add_var(buffer, 10);
353  printf("---> - u!12 + u!10 + u!10\n");
354  print_bvpoly_buffer(buffer, false);
355  printf("\n");
356
357  normalize_bvpoly_buffer(buffer);
358  printf("---> normalized\n");
359  print_bvpoly_buffer(buffer, true);
360  printf("\n\n");
361
362
363  reset_bvpoly_buffer(buffer, 128);
364  printf("---> reset: size 128\n");
365  print_bvpoly_buffer(buffer, false);
366  printf("\n");
367
368  normalize_bvpoly_buffer(buffer);
369  printf("---> normalized\n");
370  print_bvpoly_buffer(buffer, true);
371  printf("\n\n");
372
373  bvpoly_buffer_add_var(buffer, 1);
374  printf("---> add var u!1\n");
375  print_bvpoly_buffer(buffer, false);
376  printf("\n");
377
378  normalize_bvpoly_buffer(buffer);
379  printf("---> normalized\n");
380  print_bvpoly_buffer(buffer, true);
381  printf("\n\n");
382
383  bvconst_set_one(aux, 4);
384  bvpoly_buffer_sub_constant(buffer, aux);
385  printf("---> sub const 1\n");
386  print_bvpoly_buffer(buffer, false);
387  printf("\n");
388
389  normalize_bvpoly_buffer(buffer);
390  printf("---> normalized\n");
391  print_bvpoly_buffer(buffer, true);
392  printf("\n\n");
393}
394
395
396/*
397 * Global buffer
398 */
399static bvpoly_buffer_t buffer;
400
401int main(void) {
402  init_bvpoly_buffer(&buffer);
403  test1(&buffer);
404  test2(&buffer);
405  delete_bvpoly_buffer(&buffer);
406  return 0;
407}
408