1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2018 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * EXPERIMENTAL: BOOLEAN GATES
21 */
22 #include <assert.h>
23
24 #include "solvers/cdcl/new_gates.h"
25 #include "utils/memalloc.h"
26
27
28 /*
29 * ARRAY OF GATE DESCRIPTORS
30 */
init_bgate_array(bgate_array_t * a)31 void init_bgate_array(bgate_array_t *a) {
32 a->data = NULL;
33 a->ngates = 0;
34 a->size = 0;
35 }
36
extend_bgate_array(bgate_array_t * a)37 static void extend_bgate_array(bgate_array_t *a) {
38 uint32_t n;
39
40 n = a->size;
41 if (n == 0) {
42 n = DEF_BGATE_ARRAY_SIZE; // first allocation
43 assert(n <= MAX_BGATE_ARRAY_SIZE);
44 a->data = (bgate_t *) safe_malloc(n * sizeof(bgate_t));
45 a->size = n;
46 } else {
47 // try to make the table 50% larger
48 n += (n >> 1);
49 assert(n > a->size);
50 if (n > MAX_BGATE_ARRAY_SIZE) {
51 out_of_memory();
52 }
53
54 a->data = (bgate_t *) safe_realloc(a->data, n * sizeof(bgate_t));
55 a->size = n;
56 }
57 }
58
delete_bgate_array(bgate_array_t * a)59 void delete_bgate_array(bgate_array_t *a) {
60 safe_free(a->data);
61 a->data = NULL;
62 }
63
64
65 /*
66 * Store a new descriptor in a
67 * - tt = (normalized) truth table
68 * - return the index of the newly allocated element
69 */
store_bgate(bgate_array_t * a,ttbl_t * tt)70 uint32_t store_bgate(bgate_array_t *a, ttbl_t *tt) {
71 uint32_t i;
72
73 i = a->ngates;
74 if (i == a->size) {
75 extend_bgate_array(a);
76 }
77 assert(i < a->size);
78 a->data[i].ttbl = tt->mask;
79 a->data[i].var[0] = tt->label[0];
80 a->data[i].var[1] = tt->label[1];
81 a->data[i].var[2] = tt->label[2];
82 a->ngates = i+1;
83
84 return i;
85 }
86
87
88 /*
89 * Arity = number of non-null variables in g
90 */
bgate_arity(bgate_t * g)91 static uint32_t bgate_arity(bgate_t *g) {
92 uint32_t n;
93
94 n = (g->var[0] >= 0) + (g->var[1] >= 0) + (g->var[2] >= 2);
95 assert(n <= 3);
96 return n;
97 }
98
99
100 /*
101 * Get the truth table for gate i: store it in tt
102 */
get_bgate(const bgate_array_t * a,uint32_t i,ttbl_t * tt)103 void get_bgate(const bgate_array_t *a, uint32_t i, ttbl_t *tt) {
104 assert(i < a->size);
105 assert(a->data[i].ttbl < 256);
106
107 tt->nvars = bgate_arity(a->data + i);
108 tt->label[0] = a->data[i].var[0];
109 tt->label[1] = a->data[i].var[1];
110 tt->label[2] = a->data[i].var[2];
111 tt->mask = a->data[i].ttbl;
112 }
113
114
115
116 /*
117 * Normalize and store a gate with two input literals.
118 * - b = truth table for the gate
119 * (only the eight low-order bits are used)
120 * - l1, l2 = input literals
121 *
122 * - b must be of the form [b3 b3 b2 b2 b1 b1 b0 b0]
123 * - this defines a function f(l1, l2) with the following table
124 *
125 * l1 l2 f
126 *
127 * 0 0 b0
128 * 0 1 b1
129 * 1 0 b2
130 * 1 1 b3
131 */
store_binary_gate(bgate_array_t * a,uint32_t b,literal_t l1,literal_t l2)132 uint32_t store_binary_gate(bgate_array_t *a, uint32_t b, literal_t l1, literal_t l2) {
133 ttbl_t tt;
134
135 tt.nvars = 2;
136 tt.label[0] = l1;
137 tt.label[1] = l2;
138 tt.label[2] = null_bvar;
139 tt.mask = (uint8_t) b;
140 normalize_truth_table2(&tt);
141
142 return store_bgate(a, &tt);
143 }
144
145
146 /*
147 * Normalize and store a gate with three input literals:
148 * - b = truth table for the gate
149 * (only the eight low-order bits are used)
150 * - l1, l2, l3 = input literals
151 *
152 * - b is [b7 b6 b5 b4 b3 b2 b1 b0]
153 * - the corresponding function is defined by this table:
154 *
155 * l1 l2 l3 f
156 *
157 * 0 0 0 b0
158 * 0 0 1 b1
159 * 0 1 0 b2
160 * 0 1 1 b3
161 * 1 0 0 b4
162 * 1 0 1 b5
163 * 1 1 0 b6
164 * 1 1 1 b7
165 */
store_ternary_gate(bgate_array_t * a,uint32_t b,literal_t l1,literal_t l2,literal_t l3)166 uint32_t store_ternary_gate(bgate_array_t *a, uint32_t b, literal_t l1, literal_t l2, literal_t l3) {
167 ttbl_t tt;
168
169 tt.nvars = 3;
170 tt.label[0] = l1;
171 tt.label[1] = l2;
172 tt.label[2] = l3;
173 tt.mask = (uint8_t) b;
174 normalize_truth_table3(&tt);
175
176 return store_bgate(a, &tt);
177 }
178