1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include "boolector.h"
#define ARRAY2_EXAMPLE_ELEM_BW 8
#define ARRAY2_EXAMPLE_INDEX_BW 1
/* We demonstrate Boolector's ability to obtain Array models.
* We check the following formula for satisfiability:
* write (array1, 0, 3) = write (array2, 1, 5)
*/
int
main (void)
{
Btor *btor;
BoolectorNode *array1, *array2, *zero, *one, *val1, *val2;
BoolectorNode *write1, *write2, *formula;
BoolectorSort sort_index, sort_elem, sort_array;
char **indices, **values;
int32_t result;
uint32_t i, size;
btor = boolector_new ();
boolector_set_opt (btor, BTOR_OPT_OUTPUT_NUMBER_FORMAT, BTOR_OUTPUT_BASE_HEX);
sort_index = boolector_bitvec_sort (btor, ARRAY2_EXAMPLE_INDEX_BW);
sort_elem = boolector_bitvec_sort (btor, ARRAY2_EXAMPLE_ELEM_BW);
sort_array = boolector_array_sort (btor, sort_index, sort_elem);
boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1);
zero = boolector_zero (btor, sort_index);
one = boolector_one (btor, sort_index);
val1 = boolector_int (btor, 3, sort_elem);
val2 = boolector_int (btor, 5, sort_elem);
array1 = boolector_array (btor, sort_array, 0);
array2 = boolector_array (btor, sort_array, 0);
write1 = boolector_write (btor, array1, zero, val1);
write2 = boolector_write (btor, array2, one, val2);
/* Note: we compare two arrays for equality ---> needs extensional theory */
formula = boolector_eq (btor, write1, write2);
boolector_assert (btor, formula);
result = boolector_sat (btor);
printf ("Expect: sat\n");
printf ("Boolector: %s\n",
result == BOOLECTOR_SAT
? "sat"
: (result == BOOLECTOR_UNSAT ? "unsat" : "unknown"));
if (result != BOOLECTOR_SAT) abort ();
printf ("\nModel:\n");
/* Formula is satisfiable, we can obtain array models: */
boolector_array_assignment (btor, array1, &indices, &values, &size);
if (size > 0)
{
printf ("Array1:\n");
for (i = 0; i < size; i++)
printf ("Array1[#x%s] = #x%s\n", indices[i], values[i]);
boolector_free_array_assignment (btor, indices, values, size);
}
boolector_array_assignment (btor, array2, &indices, &values, &size);
if (size > 0)
{
printf ("\nArray2:\n");
for (i = 0; i < size; i++)
printf ("Array2[#x%s] = #x%s\n", indices[i], values[i]);
boolector_free_array_assignment (btor, indices, values, size);
}
boolector_array_assignment (btor, write1, &indices, &values, &size);
if (size > 0)
{
printf ("\nWrite1:\n");
for (i = 0; i < size; i++)
printf ("Write1[#x%s] = #x%s\n", indices[i], values[i]);
boolector_free_array_assignment (btor, indices, values, size);
}
boolector_array_assignment (btor, write2, &indices, &values, &size);
if (size > 0)
{
printf ("\nWrite2:\n");
for (i = 0; i < size; i++)
printf ("Write2[#x%s] = #x%s\n", indices[i], values[i]);
boolector_free_array_assignment (btor, indices, values, size);
}
/* clean up */
boolector_release (btor, formula);
boolector_release (btor, write1);
boolector_release (btor, write2);
boolector_release (btor, array1);
boolector_release (btor, array2);
boolector_release (btor, val1);
boolector_release (btor, val2);
boolector_release (btor, zero);
boolector_release (btor, one);
boolector_release_sort (btor, sort_array);
boolector_release_sort (btor, sort_index);
boolector_release_sort (btor, sort_elem);
assert (boolector_get_refs (btor) == 0);
boolector_delete (btor);
return 0;
}
|
