1 #include "maxand.h"
2 #include "boolector.h"
3 #include "utils/btorutil.h"
4
5 #include <assert.h>
6 #include <stdio.h>
7 #include <stdlib.h>
8
9 /* maxAND algorithm from hacker's delight, page 61 */
10
11 BoolectorNode *
btor_maxand(Btor * btor,BoolectorNode * a_in,BoolectorNode * b_in,BoolectorNode * c_in,BoolectorNode * d_in,BoolectorNode * m_in,int num_bits)12 btor_maxand (Btor *btor,
13 BoolectorNode *a_in,
14 BoolectorNode *b_in,
15 BoolectorNode *c_in,
16 BoolectorNode *d_in,
17 BoolectorNode *m_in,
18 int num_bits)
19 {
20 BoolectorNode *temp_1, *temp_2, *m, *zero;
21 BoolectorNode *tmp, *a, *b, *c, *d, *not_b, *not_d, *not_m, *m_minus_1;
22 BoolectorNode *b_and_not_d, *b_and_not_d_and_m, *b_and_not_d_and_m_ne_zero;
23 BoolectorNode *b_and_not_m, *not_b_and_d, *not_b_and_d_and_m, *d_and_not_m;
24 BoolectorNode *not_b_and_d_and_m_ne_zero, *temp_1_ugte_a, *temp_2_ugte_c;
25 BoolectorNode *result, *cond_if, *cond_else_1, *cond_else_2;
26 BoolectorNode *one_log_bits, *one_full_bits;
27 BoolectorSort sort, sort_log;
28 int i;
29
30 assert (btor != NULL);
31 assert (a_in != NULL);
32 assert (b_in != NULL);
33 assert (c_in != NULL);
34 assert (d_in != NULL);
35 assert (m_in != NULL);
36 assert (num_bits > 0);
37 assert (btor_util_is_power_of_2 (num_bits));
38
39 a = boolector_copy (btor, a_in);
40 b = boolector_copy (btor, b_in);
41 c = boolector_copy (btor, c_in);
42 d = boolector_copy (btor, d_in);
43 m = boolector_copy (btor, m_in);
44
45 sort = boolector_bitvec_sort (btor, num_bits);
46 sort_log = boolector_bitvec_sort (btor, btor_util_log_2 (num_bits));
47
48 one_log_bits = boolector_one (btor, sort_log);
49 one_full_bits = boolector_one (btor, sort);
50 zero = boolector_zero (btor, sort);
51
52 for (i = 0; i < num_bits; i++)
53 {
54 not_m = boolector_not (btor, m);
55 m_minus_1 = boolector_sub (btor, m, one_full_bits);
56
57 not_d = boolector_not (btor, d);
58 b_and_not_d = boolector_and (btor, b, not_d);
59 b_and_not_d_and_m = boolector_and (btor, b_and_not_d, m);
60 b_and_not_d_and_m_ne_zero = boolector_ne (btor, b_and_not_d_and_m, zero);
61
62 b_and_not_m = boolector_and (btor, b, not_m);
63 temp_1 = boolector_or (btor, b_and_not_m, m_minus_1);
64 temp_1_ugte_a = boolector_ugte (btor, temp_1, a);
65
66 not_b = boolector_not (btor, b);
67 not_b_and_d = boolector_and (btor, not_b, d);
68 not_b_and_d_and_m = boolector_and (btor, not_b_and_d, m);
69 not_b_and_d_and_m_ne_zero = boolector_ne (btor, not_b_and_d_and_m, zero);
70
71 d_and_not_m = boolector_and (btor, d, not_m);
72 temp_2 = boolector_or (btor, d_and_not_m, m_minus_1);
73 temp_2_ugte_c = boolector_ugte (btor, temp_2, c);
74
75 /* update b */
76 cond_if = boolector_cond (btor, temp_1_ugte_a, temp_1, b);
77 tmp = boolector_cond (btor, b_and_not_d_and_m_ne_zero, cond_if, b);
78 boolector_release (btor, b);
79 b = tmp;
80
81 /* update d */
82 cond_else_1 = boolector_cond (btor, temp_2_ugte_c, temp_2, d);
83 cond_else_2 =
84 boolector_cond (btor, not_b_and_d_and_m_ne_zero, cond_else_1, d);
85 tmp = boolector_cond (btor, b_and_not_d_and_m_ne_zero, d, cond_else_2);
86 boolector_release (btor, d);
87 d = tmp;
88
89 /* update m */
90 tmp = boolector_srl (btor, m, one_log_bits);
91 boolector_release (btor, m);
92 m = tmp;
93
94 boolector_release (btor, not_b);
95 boolector_release (btor, not_d);
96 boolector_release (btor, not_m);
97 boolector_release (btor, m_minus_1);
98 boolector_release (btor, b_and_not_d);
99 boolector_release (btor, b_and_not_d_and_m);
100 boolector_release (btor, b_and_not_d_and_m_ne_zero);
101 boolector_release (btor, not_b_and_d);
102 boolector_release (btor, not_b_and_d_and_m);
103 boolector_release (btor, not_b_and_d_and_m_ne_zero);
104 boolector_release (btor, b_and_not_m);
105 boolector_release (btor, d_and_not_m);
106 boolector_release (btor, temp_1);
107 boolector_release (btor, temp_2);
108 boolector_release (btor, temp_1_ugte_a);
109 boolector_release (btor, temp_2_ugte_c);
110 boolector_release (btor, cond_if);
111 boolector_release (btor, cond_else_1);
112 boolector_release (btor, cond_else_2);
113 }
114 result = boolector_and (btor, b, d);
115
116 boolector_release (btor, a);
117 boolector_release (btor, b);
118 boolector_release (btor, c);
119 boolector_release (btor, d);
120 boolector_release (btor, m);
121 boolector_release (btor, zero);
122 boolector_release (btor, one_log_bits);
123 boolector_release (btor, one_full_bits);
124 boolector_release_sort (btor, sort);
125 boolector_release_sort (btor, sort_log);
126
127 return result;
128 }
129