1 /* Boolector: Satisfiability Modulo Theories (SMT) solver.
2 *
3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4 *
5 * This file is part of Boolector.
6 * See COPYING for more information on using this software.
7 */
8
9 #include "test.h"
10
11 extern "C" {
12 #include "boolectormc.h"
13 }
14
15 class TestMc : public TestMm
16 {
17 protected:
SetUp()18 void SetUp () override
19 {
20 TestMm::SetUp ();
21 d_check_log_file = false;
22 d_mc = boolector_mc_new ();
23 d_btor = boolector_mc_get_btor (d_mc);
24 }
25
TearDown()26 void TearDown () override
27 {
28 tear_down_iteration ();
29 TestMm::TearDown ();
30 }
31
set_up_iteration()32 void set_up_iteration ()
33 {
34 if (d_mc) boolector_mc_delete (d_mc);
35 d_mc = boolector_mc_new ();
36 d_btor = boolector_mc_get_btor (d_mc);
37 }
38
tear_down_iteration()39 void tear_down_iteration ()
40 {
41 if (d_mc) boolector_mc_delete (d_mc);
42 d_mc = nullptr;
43 d_btor = nullptr;
44 }
45
test_mc_print(BoolectorNode * node,const char * name,int32_t time,FILE * file)46 void test_mc_print (BoolectorNode *node,
47 const char *name,
48 int32_t time,
49 FILE *file)
50 {
51 char *val = boolector_mc_assignment (d_mc, node, time);
52 assert (val);
53 fprintf (file, "%s = %s\n", name, val);
54 fflush (file);
55 boolector_mc_free_assignment (d_mc, val);
56 }
57
58 BtorMC *d_mc = nullptr;
59 Btor *d_btor = nullptr;
60 };
61
62 /*------------------------------------------------------------------------*/
63
TEST_F(TestMc,new_delete)64 TEST_F (TestMc, new_delete) {}
65
66 /*------------------------------------------------------------------------*/
67
TEST_F(TestMc,toggle)68 TEST_F (TestMc, toggle)
69 {
70 open_log_file ("mctoggle");
71
72 int32_t i, k, mode;
73 BoolectorNode *bit, *one, *zero, *add, *bad;
74 BoolectorSort s;
75
76 for (mode = 0; mode < 2; mode++)
77 {
78 set_up_iteration ();
79
80 s = boolector_bitvec_sort (d_btor, 1);
81 if (mode) boolector_mc_set_opt (d_mc, BTOR_MC_OPT_TRACE_GEN, 1);
82
83 // boolector_mc_set_opt (d_mc, BTOR_MC_OPT_VERBOSITY, 3);
84
85 bit = boolector_mc_state (d_mc, s, "counter");
86 one = boolector_one (d_btor, s);
87 zero = boolector_zero (d_btor, s);
88 add = boolector_add (d_btor, bit, one);
89 bad = boolector_eq (d_btor, bit, one);
90
91 boolector_mc_next (d_mc, bit, add);
92 boolector_mc_init (d_mc, bit, zero);
93 boolector_mc_bad (d_mc, bad);
94
95 boolector_release (d_btor, one);
96 boolector_release (d_btor, zero);
97 boolector_release (d_btor, add);
98 boolector_release (d_btor, bad);
99
100 k = boolector_mc_bmc (d_mc, 0, 0);
101 ASSERT_LT (k, 0); // can not reach bad within k=0 steps
102
103 k = boolector_mc_bmc (d_mc, 0, 1);
104 ASSERT_TRUE (0 <= k && k <= 1); // bad reached within k=1 steps
105
106 if (mode)
107 {
108 fprintf (d_log_file, "Bad state property satisfied at k = %d:\n", k);
109 for (i = 0; i <= k; i++)
110 {
111 fprintf (d_log_file, "\n");
112 fprintf (d_log_file, "[ state at time %d ]\n", i);
113 test_mc_print (bit, "bit", i, d_log_file);
114 }
115 }
116
117 boolector_release (d_btor, bit);
118 boolector_release_sort (d_btor, s);
119 }
120 }
121
TEST_F(TestMc,count2enable)122 TEST_F (TestMc, count2enable)
123 {
124 open_log_file ("mccount2enable");
125
126 int32_t i, k, mode;
127 BoolectorNode *counter; // 2-bit state
128 BoolectorNode *enable; // one boolean control input
129 BoolectorNode *one, *zero, *three, *add, *ifenable, *bad;
130 BoolectorSort s1, s2;
131
132 for (mode = 0; mode < 2; mode++)
133 {
134 set_up_iteration ();
135
136 s1 = boolector_bitvec_sort (d_btor, 1);
137 s2 = boolector_bitvec_sort (d_btor, 2);
138
139 if (mode) boolector_mc_set_opt (d_mc, BTOR_MC_OPT_TRACE_GEN, 1);
140
141 // boolector_mc_set_opt (d_mc, BTOR_MC_OPT_VERBOSITY, 3);
142
143 counter = boolector_mc_state (d_mc, s2, "counter");
144 enable = boolector_mc_input (d_mc, s1, "enable");
145
146 one = boolector_one (d_btor, s2);
147 zero = boolector_zero (d_btor, s2);
148 three = boolector_const (d_btor, "11");
149 add = boolector_add (d_btor, counter, one);
150 ifenable = boolector_cond (d_btor, enable, add, counter);
151 bad = boolector_eq (d_btor, counter, three);
152
153 boolector_mc_next (d_mc, counter, ifenable);
154 boolector_mc_init (d_mc, counter, zero);
155 boolector_mc_bad (d_mc, bad);
156
157 boolector_release (d_btor, one);
158 boolector_release (d_btor, zero);
159 boolector_release (d_btor, three);
160 boolector_release (d_btor, add);
161 boolector_release (d_btor, ifenable);
162 boolector_release (d_btor, bad);
163
164 k = boolector_mc_bmc (d_mc, 0, 1);
165 ASSERT_LT (k, 0); // can not reach bad within k=1 steps
166
167 k = boolector_mc_bmc (d_mc, 0, 5);
168 ASSERT_TRUE (0 <= k && k <= 5); // bad reached within k=4 steps
169
170 if (mode)
171 {
172 boolector_mc_dump (d_mc, d_log_file);
173 fflush (d_log_file);
174 fprintf (d_log_file, "Bad state property satisfied at k = %d:\n", k);
175 for (i = 0; i <= k; i++)
176 {
177 fprintf (d_log_file, "\n");
178 fprintf (d_log_file, "[ state at time %d ]\n", i);
179 test_mc_print (counter, "counter", i, d_log_file);
180 fprintf (d_log_file, "\n");
181 fprintf (d_log_file, "[ input at time %d ]\n", i);
182 test_mc_print (enable, "enable", i, d_log_file);
183 }
184 }
185
186 boolector_release (d_btor, counter);
187 boolector_release (d_btor, enable);
188 boolector_release_sort (d_btor, s1);
189 boolector_release_sort (d_btor, s2);
190 }
191 }
192
TEST_F(TestMc,count2resetenable)193 TEST_F (TestMc, count2resetenable)
194 {
195 open_log_file ("mccount2resetenable");
196
197 int32_t k, i;
198 BoolectorNode *one, *zero, *three, *add, *ifenable, *ifreset, *bad;
199 BoolectorNode *counter; // 2-bit state
200 BoolectorNode *enable, *reset; // two boolean control inputs
201 BoolectorSort s1, s2;
202
203 boolector_mc_set_opt (d_mc, BTOR_MC_OPT_TRACE_GEN, 1);
204 // boolector_mc_set_opt (d_mc, BTOR_MC_OPT_VERBOSITY, 3);
205
206 s1 = boolector_bitvec_sort (d_btor, 1);
207 s2 = boolector_bitvec_sort (d_btor, 2);
208
209 counter = boolector_mc_state (d_mc, s2, "counter");
210 enable = boolector_mc_input (d_mc, s1, "enable");
211 reset = boolector_mc_input (d_mc, s1, "reset");
212
213 one = boolector_one (d_btor, s2);
214 zero = boolector_zero (d_btor, s2);
215 boolector_release_sort (d_btor, s1);
216 boolector_release_sort (d_btor, s2);
217 three = boolector_const (d_btor, "11");
218 add = boolector_add (d_btor, counter, one);
219 ifenable = boolector_cond (d_btor, enable, add, counter);
220 ifreset = boolector_cond (d_btor, reset, ifenable, zero);
221 bad = boolector_eq (d_btor, counter, three);
222
223 boolector_mc_next (d_mc, counter, ifreset);
224 boolector_mc_init (d_mc, counter, zero);
225 boolector_mc_bad (d_mc, bad);
226 boolector_release (d_btor, one);
227 boolector_release (d_btor, zero);
228 boolector_release (d_btor, three);
229 boolector_release (d_btor, add);
230 boolector_release (d_btor, ifenable);
231 boolector_release (d_btor, ifreset);
232 boolector_release (d_btor, bad);
233
234 k = boolector_mc_bmc (d_mc, 0, 2);
235 ASSERT_LT (k, 0); // can not reach bad within k=1 steps
236
237 k = boolector_mc_bmc (d_mc, 0, 4);
238 ASSERT_TRUE (0 <= k && k <= 4); // bad reached within k=4 steps
239
240 fprintf (d_log_file, "Bad state property satisfied at k = %d:\n", k);
241 for (i = 0; i <= k; i++)
242 {
243 fprintf (d_log_file, "\n");
244 fprintf (d_log_file, "[ state at time %d ]\n", i);
245 test_mc_print (counter, "counter", i, d_log_file);
246 fprintf (d_log_file, "[ input at time %d ]\n", i);
247 test_mc_print (reset, "reset", i, d_log_file);
248 test_mc_print (enable, "enable", i, d_log_file);
249 }
250
251 boolector_release (d_btor, counter);
252 boolector_release (d_btor, enable);
253 boolector_release (d_btor, reset);
254 }
255
256 #if 0
257 TEST_F (TestMc, twostepmodel)
258 {
259 open_log_file ("mctwostepmodel");
260
261 int32_t k, i;
262 BoolectorNode * zero, * one;
263 BoolectorNode * a, * b, * t, * n, * or, * xor;
264 BoolectorNode * nexta, * nexta1, * nexta2;
265 BoolectorNode * nextb, * nextb1, * nextb2;
266 BoolectorNode * bad, * bada, *badb;
267 BoolectorSort s;
268
269 boolector_mc_set_opt (d_mc, BTOR_MC_OPT_TRACE_GEN, 1);
270 boolector_mc_set_opt (d_mc, BTOR_MC_OPT_VERBOSITY, 3);
271
272 s = boolector_bitvec_sort (d_btor, 1);
273 a = boolector_mc_state (d_mc, s, "a");
274 b = boolector_mc_state (d_mc, s, "b");
275
276 or = boolector_or (d_btor, a, b); // dangling ...
277 xor = boolector_xor (d_btor, a, b); // dangling ...
278
279 one = boolector_ones (d_btor, s);
280 zero = boolector_zero (d_btor, s);
281
282 boolector_mc_init (d_mc, a, zero);
283 boolector_mc_init (d_mc, b, zero);
284
285 t = boolector_mc_input (d_mc, s, "t");
286 n = boolector_not (d_btor, t);
287
288 nexta1 = boolector_nor (d_btor, t, a);
289 nexta2 = boolector_implies (d_btor, n, a);
290 nexta = boolector_and (d_btor, nexta1, nexta2);
291
292 nextb1 = boolector_nor (d_btor, n, b);
293 nextb2 = boolector_implies (d_btor, t, b);
294 nextb = boolector_and (d_btor, nextb1, nextb2);
295
296 boolector_mc_next (d_mc, a, nexta);
297 boolector_mc_next (d_mc, b, nextb);
298
299 bada = boolector_eq (d_btor, a, one);
300 badb = boolector_eq (d_btor, b, one);
301 bad = boolector_and (d_btor, bada, badb);
302
303 boolector_mc_bad (d_mc, bad);
304
305 k = boolector_mc_bmc (d_mc, 0, 2);
306 ASSERT_EQ (k, 2); // can reach bad within k=2 steps
307
308 fprintf (d_log_file, "Bad state property satisfied at k = %d:\n", k);
309 for (i = 0; i <= k; i++)
310 {
311 fprintf (d_log_file, "\n");
312 fprintf (d_log_file, "[ state at time %d ]\n", i);
313 fprintf (d_log_file, "\n");
314 test_mc_print(a, "a", i, d_log_file);
315 test_mc_print(b, "b",i, d_log_file);
316 fprintf (d_log_file, "\n");
317 fprintf (d_log_file, "[ input at time %d ]\n", i);
318 fprintf (d_log_file, "\n");
319 test_mc_print(t, "t", i, d_log_file);
320 test_mc_print(n, "n", i, d_log_file);
321 fprintf (d_log_file, "\n");
322 fprintf (d_log_file, "[ logic at time %d ]\n", i);
323 fprintf (d_log_file, "\n");
324 test_mc_print(nexta1, "nexta1", i, d_log_file);
325 test_mc_print(nexta1, "nexta2", i, d_log_file);
326 test_mc_print(nexta1, "nexta", i, d_log_file);
327 test_mc_print(nexta1, "nextb1", i, d_log_file);
328 test_mc_print(nexta1, "nextb2", i, d_log_file);
329 test_mc_print(nexta1, "nextb", i, d_log_file);
330 fprintf (d_log_file, "\n");
331 fprintf (d_log_file, "[ dangling logic at time %d ]\n", i);
332 fprintf (d_log_file, "\n");
333 test_mc_print (or, "or", i, d_log_file);
334 test_mc_print (xor, "xor", i, d_log_file);
335 fprintf (d_log_file, "\n");
336 fprintf (d_log_file, "[ output at time %d ]\n", i);
337 fprintf (d_log_file, "\n");
338 test_mc_print (bada, "bada", i, d_log_file);
339 test_mc_print (badb, "badb", i, d_log_file);
340 test_mc_print (bad, "bad", i, d_log_file);
341 }
342
343 boolector_release (d_btor, or);
344 boolector_release (d_btor, xor);
345 boolector_release (d_btor, one);
346 boolector_release (d_btor, zero);
347 boolector_release (d_btor, n);
348 boolector_release (d_btor, nexta1);
349 boolector_release (d_btor, nexta2);
350 boolector_release (d_btor, nexta);
351 boolector_release (d_btor, nextb1);
352 boolector_release (d_btor, nextb2);
353 boolector_release (d_btor, nextb);
354 boolector_release (d_btor, bad);
355 boolector_release (d_btor, bada);
356 boolector_release (d_btor, badb);
357 boolector_release_sort (d_btor, s);
358
359 finish_mc_test ();
360 }
361 #endif
362
363 static int32_t test_mccount2multi_reached[4];
364
365 static void
test_mccount2multi_call_back(void * state,int32_t i,int32_t k)366 test_mccount2multi_call_back (void *state, int32_t i, int32_t k)
367 {
368 (void) state;
369 assert (test_mccount2multi_reached == (int32_t *) state);
370 assert (0 <= i), assert (i < 4);
371 assert (k >= 0);
372 assert (test_mccount2multi_reached[i] == -1);
373 test_mccount2multi_reached[i] = k;
374 #if 0
375 printf ("property %d reached at bound %d\n", i, k);
376 fflush (stdout);
377 #endif
378 }
379
TEST_F(TestMc,count2multi)380 TEST_F (TestMc, count2multi)
381 {
382 int32_t i, k;
383 BoolectorSort s;
384
385 // boolector_mc_set_opt (d_mc, BTOR_MC_OPT_VERBOSITY, 3);
386 boolector_mc_set_opt (d_mc, BTOR_MC_OPT_STOP_FIRST, 0);
387
388 BoolectorNode *count, *one, *zero, *two, *three, *next;
389 BoolectorNode *eqzero, *eqone, *eqtwo, *eqthree;
390 s = boolector_bitvec_sort (d_btor, 2);
391 count = boolector_mc_state (d_mc, s, "count");
392 one = boolector_one (d_btor, s);
393 zero = boolector_zero (d_btor, s);
394 boolector_release_sort (d_btor, s);
395 two = boolector_const (d_btor, "10");
396 three = boolector_const (d_btor, "11");
397 next = boolector_add (d_btor, count, one);
398 boolector_mc_init (d_mc, count, zero);
399 boolector_mc_next (d_mc, count, next);
400 eqzero = boolector_eq (d_btor, count, zero);
401 eqone = boolector_eq (d_btor, count, one);
402 eqtwo = boolector_eq (d_btor, count, two);
403 eqthree = boolector_eq (d_btor, count, three);
404 i = boolector_mc_bad (d_mc, eqzero);
405 ASSERT_EQ (i, 0);
406 i = boolector_mc_bad (d_mc, eqone);
407 ASSERT_EQ (i, 1);
408 i = boolector_mc_bad (d_mc, eqtwo);
409 ASSERT_EQ (i, 2);
410 i = boolector_mc_bad (d_mc, eqthree);
411 ASSERT_EQ (i, 3);
412 boolector_release (d_btor, one);
413 boolector_release (d_btor, zero);
414 boolector_release (d_btor, two);
415 boolector_release (d_btor, three);
416 boolector_release (d_btor, eqone);
417 boolector_release (d_btor, eqzero);
418 boolector_release (d_btor, eqtwo);
419 boolector_release (d_btor, eqthree);
420 boolector_release (d_btor, next);
421
422 test_mccount2multi_reached[0] = -1;
423 test_mccount2multi_reached[1] = -1;
424 test_mccount2multi_reached[2] = -1;
425 test_mccount2multi_reached[3] = -1;
426 boolector_mc_set_reached_at_bound_call_back (
427 d_mc, test_mccount2multi_reached, test_mccount2multi_call_back);
428 k = boolector_mc_bmc (d_mc, 2, 3);
429 ASSERT_EQ (k, 3);
430 ASSERT_EQ (test_mccount2multi_reached[0], -1);
431 ASSERT_EQ (test_mccount2multi_reached[1], -1);
432 ASSERT_EQ (test_mccount2multi_reached[2], 2);
433 ASSERT_EQ (test_mccount2multi_reached[3], 3);
434 ASSERT_LT (boolector_mc_reached_bad_at_bound (d_mc, 0), 0);
435 ASSERT_LT (boolector_mc_reached_bad_at_bound (d_mc, 1), 0);
436 ASSERT_EQ (boolector_mc_reached_bad_at_bound (d_mc, 2), 2);
437 ASSERT_EQ (boolector_mc_reached_bad_at_bound (d_mc, 3), 3);
438 k = boolector_mc_bmc (d_mc, 4, 10);
439 ASSERT_EQ (k, 5);
440 ASSERT_EQ (test_mccount2multi_reached[0], 4);
441 ASSERT_EQ (test_mccount2multi_reached[1], 5);
442 ASSERT_EQ (test_mccount2multi_reached[2], 2);
443 ASSERT_EQ (test_mccount2multi_reached[3], 3);
444 ASSERT_EQ (boolector_mc_reached_bad_at_bound (d_mc, 0), 4);
445 ASSERT_EQ (boolector_mc_reached_bad_at_bound (d_mc, 1), 5);
446 ASSERT_EQ (boolector_mc_reached_bad_at_bound (d_mc, 2), 2);
447 ASSERT_EQ (boolector_mc_reached_bad_at_bound (d_mc, 3), 3);
448 boolector_release (d_btor, count);
449 }
450