1 #include "maxor.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 /* maxOR algorithm from hacker's delight, page 60 */
10
11 BoolectorNode *
btor_maxor(Btor * btor,BoolectorNode * a_in,BoolectorNode * b_in,BoolectorNode * c_in,BoolectorNode * d_in,BoolectorNode * m_in,int num_bits)12 btor_maxor (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, *m_minus_1, *b_minus_m;
22 BoolectorNode *d_minus_m, *one_log_bits, *b_and_d;
23 BoolectorNode *b_and_d_and_m, *temp_1_ugte_a, *temp_2_ugte_c;
24 BoolectorNode *b_and_d_and_m_ne_zero, *cond_1, *cond_2, *result;
25 BoolectorNode *and_break, *cond_3, *cond_4, *_break;
26 BoolectorSort sort_log, sort;
27 int i;
28
29 assert (btor != NULL);
30 assert (a_in != NULL);
31 assert (b_in != NULL);
32 assert (c_in != NULL);
33 assert (d_in != NULL);
34 assert (m_in != NULL);
35 assert (num_bits > 0);
36 assert (btor_util_is_power_of_2 (num_bits));
37
38 a = boolector_copy (btor, a_in);
39 b = boolector_copy (btor, b_in);
40 c = boolector_copy (btor, c_in);
41 d = boolector_copy (btor, d_in);
42 m = boolector_copy (btor, m_in);
43
44 sort_log = boolector_bitvec_sort (btor, btor_util_log_2 (num_bits));
45 sort = boolector_bitvec_sort (btor, num_bits);
46
47 one_log_bits = boolector_one (btor, sort_log);
48 zero = boolector_zero (btor, sort);
49
50 /* as soon _break becomes 1, we do not change the values
51 * of b and d anymore */
52 _break = boolector_false (btor);
53
54 for (i = 0; i < num_bits; i++)
55 {
56 b_and_d = boolector_and (btor, b, d);
57 b_and_d_and_m = boolector_and (btor, b_and_d, m);
58 b_and_d_and_m_ne_zero = boolector_ne (btor, b_and_d_and_m, zero);
59
60 m_minus_1 = boolector_dec (btor, m);
61
62 b_minus_m = boolector_sub (btor, b, m);
63 temp_1 = boolector_or (btor, b_minus_m, m_minus_1);
64 temp_1_ugte_a = boolector_ugte (btor, temp_1, a);
65
66 d_minus_m = boolector_sub (btor, d, m);
67 temp_2 = boolector_or (btor, d_minus_m, m_minus_1);
68 temp_2_ugte_c = boolector_ugte (btor, temp_2, c);
69
70 /* update b */
71 cond_1 = boolector_cond (btor, temp_1_ugte_a, temp_1, b);
72 cond_2 = boolector_cond (btor, b_and_d_and_m_ne_zero, cond_1, b);
73 tmp = boolector_cond (btor, _break, b, cond_2);
74 boolector_release (btor, b);
75 b = tmp;
76
77 /* update _break */
78 and_break = boolector_and (btor, b_and_d_and_m_ne_zero, temp_1_ugte_a);
79 tmp = boolector_or (btor, _break, and_break);
80 boolector_release (btor, _break);
81 _break = tmp;
82 boolector_release (btor, and_break);
83
84 /* update d */
85 cond_3 = boolector_cond (btor, temp_2_ugte_c, temp_2, d);
86 cond_4 = boolector_cond (btor, b_and_d_and_m_ne_zero, cond_3, d);
87 tmp = boolector_cond (btor, _break, d, cond_4);
88 boolector_release (btor, d);
89 d = tmp;
90
91 /* update _break */
92 and_break = boolector_and (btor, b_and_d_and_m_ne_zero, temp_2_ugte_c);
93 tmp = boolector_or (btor, _break, and_break);
94 boolector_release (btor, _break);
95 _break = tmp;
96 boolector_release (btor, and_break);
97
98 /* update m */
99 tmp = boolector_srl (btor, m, one_log_bits);
100 boolector_release (btor, m);
101 m = tmp;
102
103 boolector_release (btor, b_and_d);
104 boolector_release (btor, b_and_d_and_m);
105 boolector_release (btor, b_and_d_and_m_ne_zero);
106 boolector_release (btor, cond_1);
107 boolector_release (btor, cond_2);
108 boolector_release (btor, cond_3);
109 boolector_release (btor, cond_4);
110 boolector_release (btor, m_minus_1);
111 boolector_release (btor, b_minus_m);
112 boolector_release (btor, d_minus_m);
113 boolector_release (btor, temp_1);
114 boolector_release (btor, temp_2);
115 boolector_release (btor, temp_1_ugte_a);
116 boolector_release (btor, temp_2_ugte_c);
117 }
118
119 result = boolector_or (btor, b, d);
120
121 boolector_release (btor, _break);
122 boolector_release (btor, a);
123 boolector_release (btor, b);
124 boolector_release (btor, c);
125 boolector_release (btor, d);
126 boolector_release (btor, m);
127 boolector_release (btor, zero);
128 boolector_release (btor, one_log_bits);
129 boolector_release_sort (btor, sort_log);
130 boolector_release_sort (btor, sort);
131
132 return result;
133 }
134