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 construction of distinct maps
21 */
22
23#include <stdio.h>
24#include <stdint.h>
25#include <inttypes.h>
26
27#include "types.h"
28#include "abstract_values.h"
29#include "fun_maps.h"
30
31static type_table_t types;
32static pstore_t store;
33/*
34 * Print particle x as a index (or tuple)
35 */
36static void print_index(particle_t x) {
37  particle_tuple_t *tup;
38  uint32_t i, n;
39
40  switch (particle_kind(&store, x)) {
41  case LABEL_PARTICLE:
42    printf("L%"PRId32, particle_label(&store, x));
43    break;
44  case FRESH_PARTICLE:
45    printf("p!%"PRId32, x);
46    break;
47  case TUPLE_PARTICLE:
48    tup = tuple_particle_desc(&store, x);
49    n = tup->nelems;
50    for (i=0; i<n; i++) {
51      if (i>0) printf(" ");
52      print_index(tup->elem[i]);
53    }
54    break;
55  }
56}
57
58
59/*
60 * Print particle x as a value
61 */
62static void print_value(particle_t x) {
63  particle_tuple_t *tup;
64  uint32_t i, n;
65
66  switch (particle_kind(&store, x)) {
67  case LABEL_PARTICLE:
68    printf("L%"PRId32, particle_label(&store, x));
69    break;
70  case FRESH_PARTICLE:
71    printf("p!%"PRId32, x);
72    break;
73  case TUPLE_PARTICLE:
74    tup = tuple_particle_desc(&store, x);
75    printf("(tuple ");
76    n = tup->nelems;
77    for (i=0; i<n; i++) {
78      printf(" ");
79      print_value(tup->elem[i]);
80    }
81    printf(")");
82    break;
83  }
84}
85
86
87/*
88 * Print a map
89 */
90static void print_map(map_t *map) {
91  uint32_t i, n;
92  particle_t idx, v;
93  bool vmode;
94
95  printf("map[%p]", map);
96  n = map->nelems;
97  vmode = n>=5; // vmode means one map per line
98
99  for (i=0; i<n; i++) {
100    idx = map->data[i].index;
101    v = map->data[i].value;
102    if (vmode) {
103      printf("\n   ");
104    } else if (i == 0) {
105      printf(": ");
106    } else {
107      printf(", ");
108    }
109    print_index(idx);
110    printf(" -> ");
111    print_value(v);
112  }
113
114  v = map_default_value(map);
115  if (v != null_particle) {
116    if (vmode) {
117      printf("\n   ");
118    } else if (i == 0) {
119      printf(": ");
120    } else {
121      printf(", ");
122    }
123    printf("def -> ");
124    print_value(v);
125  }
126
127  printf("\n");
128}
129
130
131
132/*
133 * Create type tau1 -> tau2
134 */
135static type_t fun_type1(type_t tau1, type_t tau2) {
136  return function_type(&types, tau2, 1, &tau1);
137}
138
139/*
140 * Create type tau1 x tau2 -> tau3
141 */
142static type_t fun_type2(type_t tau1, type_t tau2, type_t tau3) {
143  type_t aux[2];
144
145  aux[0] = tau1;
146  aux[1] = tau2;
147  return function_type(&types, tau3, 2, aux);
148}
149
150
151/*
152 * Test1: 4 maps [bool -> bool]
153 */
154static void test1(void) {
155  map_t *map[4];
156  type_t tau;
157  function_type_t *f;
158  uint32_t i;
159  bool ok;
160
161  printf("\n"
162	 "***********************\n"
163	 "*       TEST 1        *\n"
164         "***********************\n");
165
166  init_pstore(&store, &types);
167
168  for (i=0; i<4; i++) {
169    map[i] = new_map(3);
170  }
171
172  // print all the maps;
173  printf("\nIinitial maps\n");
174  for (i=0; i<4; i++) {
175    print_map(map[i]);
176  }
177  printf("\n");
178
179  tau = bool_type(&types);
180  tau = fun_type1(tau, tau); // [bool -> bool]
181  f = function_type_desc(&types, tau);
182  ok = force_maps_to_differ(&store, f, 4, map);
183  if (ok) {
184    printf("All distinct: OK\n");
185  } else {
186    printf("All distinct: failed\n");
187  }
188
189  // print all the maps;
190  printf("\nFinal maps\n");
191  for (i=0; i<4; i++) {
192    print_map(map[i]);
193  }
194  printf("\n");
195
196  // cleanup
197  for (i=0; i<4; i++) {
198    free_map(map[i]);
199  }
200
201  delete_pstore(&store);
202}
203
204
205/*
206 * Test2: 5 maps [bool -> bool]
207 */
208static void test2(void) {
209  map_t *map[5];
210  type_t tau;
211  function_type_t *f;
212  uint32_t i;
213  bool ok;
214
215  printf("\n"
216	 "***********************\n"
217	 "*       TEST 2        *\n"
218         "***********************\n");
219
220  init_pstore(&store, &types);
221
222  for (i=0; i<5; i++) {
223    map[i] = new_map(3);
224  }
225
226  // print all the maps;
227  printf("\nIinitial maps\n");
228  for (i=0; i<5; i++) {
229    print_map(map[i]);
230  }
231  printf("\n");
232
233  tau = bool_type(&types);
234  tau = fun_type1(tau, tau); // [bool -> bool]
235  f = function_type_desc(&types, tau);
236  ok = force_maps_to_differ(&store, f, 5, map);
237  if (ok) {
238    printf("All distinct: OK\n");
239  } else {
240    printf("All distinct: failed\n");
241  }
242
243  // print all the maps;
244  printf("\nFinal maps\n");
245  for (i=0; i<5; i++) {
246    print_map(map[i]);
247  }
248  printf("\n");
249
250  // cleanup
251  for (i=0; i<5; i++) {
252    free_map(map[i]);
253  }
254
255  delete_pstore(&store);
256}
257
258
259/*
260 * Test 3: 16 functions of type [bool bool -> bool]
261 */
262static void test3(void) {
263  map_t *map[16];
264  type_t tau;
265  function_type_t *f;
266  uint32_t i;
267  bool ok;
268
269  printf("\n"
270	 "***********************\n"
271	 "*       TEST 3        *\n"
272         "***********************\n");
273
274  init_pstore(&store, &types);
275
276  for (i=0; i<16; i++) {
277    map[i] = new_map(3);
278  }
279
280  // print all the maps;
281  printf("\nIinitial maps\n");
282  for (i=0; i<16; i++) {
283    print_map(map[i]);
284  }
285  printf("\n");
286
287  tau = bool_type(&types);
288  tau = fun_type2(tau, tau, tau); // [bool bool -> bool]
289  f = function_type_desc(&types, tau);
290  ok = force_maps_to_differ(&store, f, 16, map);
291  if (ok) {
292    printf("All distinct: OK\n");
293  } else {
294    printf("All distinct: failed\n");
295  }
296
297  // print all the maps;
298  printf("\nFinal maps\n");
299  for (i=0; i<16; i++) {
300    print_map(map[i]);
301  }
302  printf("\n");
303
304  // cleanup
305  for (i=0; i<16; i++) {
306    free_map(map[i]);
307  }
308
309  delete_pstore(&store);
310}
311
312
313/*
314 * Test 4: 17 functions of type [bool bool -> bool]
315 */
316static void test4(void) {
317  map_t *map[17];
318  type_t tau;
319  function_type_t *f;
320  uint32_t i;
321  bool ok;
322
323  printf("\n"
324	 "***********************\n"
325 	 "*       TEST 4        *\n"
326         "***********************\n");
327
328  init_pstore(&store, &types);
329
330  for (i=0; i<17; i++) {
331    map[i] = new_map(3);
332  }
333
334  // print all the maps;
335  printf("\nIinitial maps\n");
336  for (i=0; i<17; i++) {
337    print_map(map[i]);
338  }
339  printf("\n");
340
341  tau = bool_type(&types);
342  tau = fun_type2(tau, tau, tau); // [bool bool -> bool]
343  f = function_type_desc(&types, tau);
344  ok = force_maps_to_differ(&store, f, 17, map);
345  if (ok) {
346    printf("All distinct: OK\n");
347  } else {
348    printf("All distinct: failed\n");
349  }
350
351  // print all the maps;
352  printf("\nFinal maps\n");
353  for (i=0; i<17; i++) {
354    print_map(map[i]);
355  }
356  printf("\n");
357
358  // cleanup
359  for (i=0; i<17; i++) {
360    free_map(map[i]);
361  }
362
363  delete_pstore(&store);
364}
365
366
367
368/*
369 * Test 5: [bool -> U]
370 */
371static void test5(void) {
372  map_t *map[5];
373  type_t unint, tau;
374  function_type_t *f;
375  uint32_t i;
376  bool ok;
377
378  printf("\n"
379	 "***********************\n"
380	 "*       TEST 5        *\n"
381         "***********************\n");
382
383  init_pstore(&store, &types);
384
385  for (i=0; i<5; i++) {
386    map[i] = new_map(3);
387  }
388
389  // print all the maps;
390  printf("\nIinitial maps\n");
391  for (i=0; i<5; i++) {
392    print_map(map[i]);
393  }
394  printf("\n");
395
396  tau = bool_type(&types);
397  unint = new_uninterpreted_type(&types);
398  tau = fun_type1(tau, unint); // [bool -> unint]
399  f = function_type_desc(&types, tau);
400  ok = force_maps_to_differ(&store, f, 5, map);
401  if (ok) {
402    printf("All distinct: OK\n");
403  } else {
404    printf("All distinct: failed\n");
405  }
406
407  // print all the maps;
408  printf("\nFinal maps\n");
409  for (i=0; i<5; i++) {
410    print_map(map[i]);
411  }
412  printf("\n");
413
414  // cleanup
415  for (i=0; i<5; i++) {
416    free_map(map[i]);
417  }
418
419  delete_pstore(&store);
420}
421
422
423
424/*
425 * Test 6: [U -> bool]
426 */
427static void test6(void) {
428  map_t *map[5];
429  type_t unint, tau;
430  function_type_t *f;
431  uint32_t i;
432  bool ok;
433
434  printf("\n"
435	 "***********************\n"
436	 "*       TEST 6        *\n"
437         "***********************\n");
438
439  init_pstore(&store, &types);
440
441  for (i=0; i<5; i++) {
442    map[i] = new_map(3);
443  }
444
445  // print all the maps;
446  printf("\nIinitial maps\n");
447  for (i=0; i<5; i++) {
448    print_map(map[i]);
449  }
450  printf("\n");
451
452  tau = bool_type(&types);
453  unint = new_uninterpreted_type(&types);
454  tau = fun_type1(unint, tau); // [unint -> bool]
455  f = function_type_desc(&types, tau);
456  ok = force_maps_to_differ(&store, f, 5, map);
457  if (ok) {
458    printf("All distinct: OK\n");
459  } else {
460    printf("All distinct: failed\n");
461  }
462
463  // print all the maps;
464  printf("\nFinal maps\n");
465  for (i=0; i<5; i++) {
466    print_map(map[i]);
467  }
468  printf("\n");
469
470  // cleanup
471  for (i=0; i<5; i++) {
472    free_map(map[i]);
473  }
474
475  delete_pstore(&store);
476}
477
478
479
480
481
482
483int main(void) {
484  init_type_table(&types, 10);
485
486  test1();
487  test2();
488  test3();
489  test4();
490  test5();
491  test6();
492
493  delete_type_table(&types);
494
495  return 0;
496}
497
498