1 /* 2 * This file is part of the Yices SMT Solver. 3 * Copyright (C) 2019 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 * TRUTH TABLES 21 */ 22 23 #ifndef __TRUTH_TABLES_H 24 #define __TRUTH_TABLES_H 25 26 #include <stdint.h> 27 28 #include "solvers/cdcl/smt_core_base_types.h" 29 30 /* 31 * Truth tables for functions of arity <= 3. 32 * 33 * - for functions of arity 3, 34 * label[0], label[1], label[2] are the indices of three Boolean variables 35 * in increasing order 36 * - for functions of arity 2, label[2] is not used (it's null_bvar = -1) 37 * label[0] and label[1] are two Boolean variables 38 * 39 * - the truth table is an array of 8bits b7 ... b0 40 * 41 * For functions of arity 3, the encoding is as follows 42 * 43 * label[0] label[1] label[2] f 44 * 0 0 0 b0 45 * 0 0 1 b1 46 * 0 1 0 b2 47 * 0 1 1 b3 48 * 1 0 0 b4 49 * 1 0 1 b5 50 * 1 1 0 b6 51 * 1 1 1 b7 52 * 53 * For functions of arity 2, this looks like: 54 * 55 * label[0] label[1] label[2] f 56 * 0 0 0 b0 57 * 0 0 1 b0 58 * 0 1 0 b2 59 * 0 1 1 b2 60 * 1 0 0 b4 61 * 1 0 1 b4 62 * 1 1 0 b6 63 * 1 1 1 b6 64 * 65 */ 66 67 /* 68 * Structure to store a truth table: 69 * - this is used to simplify and normalize truth tables 70 * - a table consists of nvars columns where nvars is between 0 and 3 71 * - each column is labeled by a signed integer, which can be either a literal 72 * or a Boolean variable, or -1 73 * - the truth values are stored in a bit mask (8 bit, unsigned word). 74 * all 8bits are used even if the table has fewer than 3 columms. 75 */ 76 typedef struct ttbl_s { 77 uint32_t nvars; // number of columns (between 0 and 3) 78 int32_t label[3] ; // column labels 79 uint8_t mask; // 8-bit truth table 80 } ttbl_t; 81 82 83 /* 84 * Normalize a truth table with two columns: 85 * - tt.nvars must be 2 86 * - tt.label[0] and tt.label[1] must be literals 87 * - tt.label[2] must be -1 88 * 89 * After normalization, we can have: 90 * - tt.nvars = 0 and tt.mask = 0x00 or 0xff (constant function) 91 * - tt.nvars = 1 and tt.label[0] is a Boolean variable 92 * and tt.mask is either 0x0f or 0xf0: 93 * label[0] is the input variable X 94 * the output is either X or (not X) 95 * - tt.nvars = 2 and tt.label[0] and tt.label[1] are Boolean variables 96 * and label[0] < label[1]. 97 * label[0] and label[1] are two input variables 98 * tt.mask gives the truth table for the output function 99 * 100 * In addition, all unused labels are set to null_bvar (i.e., -1). 101 * For example, if tt.nvars = 1 then both tt.label[1] and tt.label[2] 102 * are equal to null_bvar. 103 */ 104 extern void normalize_truth_table2(ttbl_t *tt); 105 106 /* 107 * Normalize a truth table with three columns: 108 * - tt.nvars must be 3 109 * - tt.label[0 .. 2] must be literals 110 * 111 * After normalization: 112 * - tt.nvars is a number between 0 and 3. 113 * - label[0 .. tt.nvars-1] are distinct Boolean variables, 114 * sorted in increasing order. 115 * - tt.mask is the truth table for the defined gate. 116 * - unused labels are set to null_bvars (i.e., -1). 117 */ 118 extern void normalize_truth_table3(ttbl_t *tt); 119 120 121 /* 122 * General form 123 */ 124 extern void normalize_truth_table(ttbl_t *tt); 125 126 127 /* 128 * Literal encoded in tt 129 * - tt must have a single variable 130 */ 131 extern literal_t literal_of_ttbl1(ttbl_t *tt); 132 133 /* 134 * Literal encoded in tt 135 * - tt must be a constant function (tt->nvars == 0) 136 */ 137 extern literal_t literal_of_ttbl0(ttbl_t *tt); 138 139 /* 140 * Combine two binary truth tables: 141 * - tt1 defines a function f(x, y) 142 * - tt2 defines x as a function g(z, t) 143 * - the result is the truth table for f(g(z, t), y) 144 */ 145 extern void compose_ttbl_left(const ttbl_t *tt1, const ttbl_t *tt2, ttbl_t *result); 146 147 /* 148 * Combine two binary truth tables: 149 * - tt1 defines f(x, y) 150 * - tt2 defines y as a g(z, t) 151 * - the result is the truth table for f(x, g(z, t)) 152 */ 153 extern void compose_ttbl_right(const ttbl_t *tt1, const ttbl_t *tt2, ttbl_t *result); 154 155 /* 156 * Try to compose three binary tables and reduce the result to 157 * a three-column table. 158 * - tt1 defines f(x, y) 159 * - tt2 defines g(a, b) for x 160 * - tt3 defined h(c, d) for y 161 * 162 * The function returns true if at least two of the 163 * variables a, b, c, d are equal and store the truth table 164 * for f(g(a, b), h(c, d)) into result. 165 * 166 * The function returns false otherwise. 167 */ 168 extern bool compose_ttbl_left_right1(const ttbl_t *tt1, const ttbl_t *tt2, const ttbl_t *tt3, ttbl_t *result); 169 170 /* 171 * Try to compose three tables and reduce the result to a three-column table. 172 * - tt1 defines f(x, y) 173 * - tt2 defines g(a, b) for x 174 * - tt3 defines h(c, d, e) for y 175 * 176 * Succeed if { a, b } is a subset of { c, d, e }. 177 * In this case, store the truth table for f(g(a, b), h(c, d, e)) in result. 178 * Otherwise return false. 179 */ 180 extern bool compose_ttbl_left_right2(const ttbl_t *tt1, const ttbl_t *tt2, const ttbl_t *tt3, ttbl_t *result); 181 182 /* 183 * Same thing but with the tt2 defining a ternary function and tt3 a binary function. 184 * - tt1 defines f(x, y) 185 * - tt2 defines g(a, b, c) for x 186 * - tt3 defines h(e, f) for y 187 * 188 * Succeed if { e, f } is a subset of { a, b, c}. 189 * Return true and store the table for f(g(a, b, c), h(e, f)) in result. 190 * Otherwise, return false. 191 */ 192 extern bool compose_ttbl_left_right3(const ttbl_t *tt1, const ttbl_t *tt2, const ttbl_t *tt3, ttbl_t *result); 193 194 195 /* 196 * Same thing but with two ternary functions: 197 * - tt1 defines f(x, y) 198 * - tt2 defines g(a, b, c) for x 199 * - tt3 defines h(d, e, f) for y 200 * 201 * Succeed if a = d and b = e and c = f. 202 * Then store the table for f(g(a, b, c), h(d, e, f)) in result. 203 * Otherwise return false. 204 */ 205 extern bool compose_ttbl_left_right4(const ttbl_t *tt1, const ttbl_t *tt2, const ttbl_t *tt3, ttbl_t *result); 206 207 208 /* 209 * General form: 210 * - tt1 defines f(x, y) 211 * - tt2 defines a function g(...) for x (either binary or ternary) 212 * - tt3 defines a function h(...) for y (either binary or ternary) 213 * 214 * Succeed if f(g(...), h(...)) can be reduced to a three-column table. 215 * Store the result in *result if so, and return true. 216 * Return false otherwise. 217 */ 218 extern bool compose_ttbl_left_right(const ttbl_t *tt1, const ttbl_t *tt2, const ttbl_t *tt3, ttbl_t *result); 219 220 221 222 #endif /* __TRUTH_TABLES_H */ 223