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
107
108
109
110
111
|
#include "boolector.h"
int
main ()
{
// Create Boolector instance
Btor *btor = boolector_new ();
// Enable model generation
boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1);
// Create bit-vector sort of size 8
BoolectorSort bvsort8 = boolector_bitvec_sort (btor, 8);
// Create expressions
BoolectorNode *x = boolector_var (btor, bvsort8, "x");
BoolectorNode *y = boolector_var (btor, bvsort8, "y");
BoolectorNode *zero = boolector_zero (btor, bvsort8);
BoolectorNode *hundred = boolector_int (btor, 100, bvsort8);
// 0 < x
BoolectorNode *ult_x = boolector_ult (btor, zero, x);
boolector_assert (btor, ult_x);
// x <= 100
BoolectorNode *ulte_x = boolector_ulte (btor, x, hundred);
boolector_assert (btor, ulte_x);
// 0 < y
BoolectorNode *ult_y = boolector_ult (btor, zero, y);
boolector_assert (btor, ult_y);
// y <= 100
BoolectorNode *ulte_y = boolector_ulte (btor, y, hundred);
boolector_assert (btor, ulte_y);
// x * y
BoolectorNode *mul = boolector_mul (btor, x, y);
// x * y < 100
BoolectorNode *ult = boolector_ult (btor, mul, hundred);
boolector_assert (btor, ult);
BoolectorNode *umulo = boolector_umulo (btor, x, y);
BoolectorNode *numulo = boolector_not (btor, umulo); // prevent overflow
boolector_assert (btor, numulo);
int result = boolector_sat (btor);
printf ("Expect: sat\n");
printf ("Boolector: ");
if (result == BOOLECTOR_SAT)
{
printf ("sat\n");
}
else if (result == BOOLECTOR_UNSAT)
{
printf ("unsat\n");
}
else
{
printf ("unknown\n");
}
printf ("\n");
// Get assignment strings for x and y
const char *xstr = boolector_bv_assignment (btor, x); // returns "00000100"
const char *ystr = boolector_bv_assignment (btor, y); // returns "00010101"
printf ("assignment of x: %s\n", xstr);
printf ("assignment of y: %s\n", ystr);
printf ("\n");
// Alternatively, get values for x and y as nodes
BoolectorNode *x_value = boolector_get_value(btor, x);
BoolectorNode *y_value = boolector_get_value(btor, y);
const char *xvaluestr =
boolector_bv_assignment (btor, x_value); // returns "00000100"
const char *yvaluestr =
boolector_bv_assignment (btor, y_value); // returns "00010101"
printf ("assignment of x (via get-value): %s\n", xvaluestr);
printf ("assignment of y (via get-value): %s\n", yvaluestr);
printf ("\n");
printf ("Print model in BTOR format:\n");
boolector_print_model (btor, "btor", stdout);
printf ("\n");
printf ("Print model in SMT-LIBv2 format:\n");
boolector_print_model (btor, "smt2", stdout);
printf ("\n");
// Release expressions
boolector_release (btor, x);
boolector_release (btor, y);
boolector_release (btor, zero);
boolector_release (btor, hundred);
boolector_release (btor, ult_x);
boolector_release (btor, ulte_x);
boolector_release (btor, ult_y);
boolector_release (btor, ulte_y);
boolector_release (btor, mul);
boolector_release (btor, ult);
boolector_release (btor, numulo);
boolector_release (btor, umulo);
// Release assigments
boolector_free_bv_assignment (btor, xstr);
boolector_free_bv_assignment (btor, ystr);
// Release sorts
boolector_release_sort (btor, bvsort8);
// Delete Boolector instance
boolector_delete (btor);
}
|
