Austin Eng | cc2516a | 2023-10-17 20:57:54 +0000 | [diff] [blame] | 1 | // Copyright 2023 The Dawn & Tint Authors |
Ben Clayton | ec6262f | 2023-08-18 18:30:15 +0000 | [diff] [blame] | 2 | // |
Austin Eng | cc2516a | 2023-10-17 20:57:54 +0000 | [diff] [blame] | 3 | // Redistribution and use in source and binary forms, with or without |
| 4 | // modification, are permitted provided that the following conditions are met: |
Ben Clayton | ec6262f | 2023-08-18 18:30:15 +0000 | [diff] [blame] | 5 | // |
Austin Eng | cc2516a | 2023-10-17 20:57:54 +0000 | [diff] [blame] | 6 | // 1. Redistributions of source code must retain the above copyright notice, this |
| 7 | // list of conditions and the following disclaimer. |
Ben Clayton | ec6262f | 2023-08-18 18:30:15 +0000 | [diff] [blame] | 8 | // |
Austin Eng | cc2516a | 2023-10-17 20:57:54 +0000 | [diff] [blame] | 9 | // 2. Redistributions in binary form must reproduce the above copyright notice, |
| 10 | // this list of conditions and the following disclaimer in the documentation |
| 11 | // and/or other materials provided with the distribution. |
| 12 | // |
| 13 | // 3. Neither the name of the copyright holder nor the names of its |
| 14 | // contributors may be used to endorse or promote products derived from |
| 15 | // this software without specific prior written permission. |
| 16 | // |
| 17 | // THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" |
| 18 | // AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE |
| 19 | // IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE |
| 20 | // DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE |
| 21 | // FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL |
| 22 | // DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR |
| 23 | // SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
| 24 | // CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, |
| 25 | // OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE |
| 26 | // OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
Ben Clayton | ec6262f | 2023-08-18 18:30:15 +0000 | [diff] [blame] | 27 | |
| 28 | package cnf_test |
| 29 | |
| 30 | import ( |
| 31 | "testing" |
| 32 | |
| 33 | "dawn.googlesource.com/dawn/tools/src/cnf" |
| 34 | "github.com/google/go-cmp/cmp" |
| 35 | ) |
| 36 | |
| 37 | func TestAnd(t *testing.T) { |
| 38 | type E = cnf.Expr |
| 39 | for _, test := range []struct { |
| 40 | lhs, rhs cnf.Expr |
| 41 | expect cnf.Expr |
| 42 | }{ |
| 43 | { // And('', '') => '' |
| 44 | lhs: E{}, rhs: E{}, |
| 45 | expect: E{}, |
| 46 | }, |
| 47 | { // And('X', '') => 'X' |
| 48 | lhs: E{{T("X")}}, rhs: E{}, |
| 49 | expect: E{{T("X")}}, |
| 50 | }, |
| 51 | { // And('!X', '') => '!X' |
| 52 | lhs: E{{F("X")}}, rhs: E{}, |
| 53 | expect: E{{F("X")}}, |
| 54 | }, |
| 55 | { // And('', 'X') => 'X' |
| 56 | lhs: E{}, rhs: E{{T("X")}}, |
| 57 | expect: E{{T("X")}}, |
| 58 | }, |
| 59 | { // And('', '!X') => '!X' |
| 60 | lhs: E{}, rhs: E{{F("X")}}, |
| 61 | expect: E{{F("X")}}, |
| 62 | }, |
| 63 | { // And('X', 'Y') => 'X && Y' |
| 64 | lhs: E{{T("X")}}, rhs: E{{T("Y")}}, |
| 65 | expect: E{{T("X")}, {T("Y")}}, |
| 66 | }, |
| 67 | { // And('X', '!Y') => 'X && !Y' |
| 68 | lhs: E{{T("X")}}, rhs: E{{F("Y")}}, |
| 69 | expect: E{{T("X")}, {F("Y")}}, |
| 70 | }, |
| 71 | { // And('Y', 'X') => 'Y && X' |
| 72 | lhs: E{{T("Y")}}, rhs: E{{T("X")}}, |
| 73 | expect: E{{T("Y")}, {T("X")}}, |
| 74 | }, |
| 75 | { // And('!Y', 'X') => '!Y && X' |
| 76 | lhs: E{{F("Y")}}, rhs: E{{T("X")}}, |
| 77 | expect: E{{F("Y")}, {T("X")}}, |
| 78 | }, |
| 79 | { // And('X && Y', 'Z') => 'X && Y && Z' |
| 80 | lhs: E{{T("X")}, {T("Y")}}, rhs: E{{T("Z")}}, |
| 81 | expect: E{{T("X")}, {T("Y")}, {T("Z")}}, |
| 82 | }, |
| 83 | { // And('!X && Y', 'Z') => '!X && Y && Z' |
| 84 | lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Z")}}, |
| 85 | expect: E{{F("X")}, {T("Y")}, {T("Z")}}, |
| 86 | }, |
| 87 | { // And('X && !Y', 'Z') => 'X && !Y && Z' |
| 88 | lhs: E{{T("X")}, {F("Y")}}, rhs: E{{T("Z")}}, |
| 89 | expect: E{{T("X")}, {F("Y")}, {T("Z")}}, |
| 90 | }, |
| 91 | { // And('X && Y', '!Z') => 'X && Y && !Z' |
| 92 | lhs: E{{T("X")}, {T("Y")}}, rhs: E{{F("Z")}}, |
| 93 | expect: E{{T("X")}, {T("Y")}, {F("Z")}}, |
| 94 | }, |
| 95 | { // And('X', 'Y && Z') => 'X && Y && Z' |
| 96 | lhs: E{{T("X")}}, rhs: E{{T("Y")}, {T("Z")}}, |
| 97 | expect: E{{T("X")}, {T("Y")}, {T("Z")}}, |
| 98 | }, |
| 99 | { // And('!X', 'Y && Z') => '!X && Y && Z' |
| 100 | lhs: E{{F("X")}}, rhs: E{{T("Y")}, {T("Z")}}, |
| 101 | expect: E{{F("X")}, {T("Y")}, {T("Z")}}, |
| 102 | }, |
| 103 | { // And('X', '!Y && Z') => 'X && !Y && Z' |
| 104 | lhs: E{{T("X")}}, rhs: E{{F("Y")}, {T("Z")}}, |
| 105 | expect: E{{T("X")}, {F("Y")}, {T("Z")}}, |
| 106 | }, |
| 107 | { // And('X', 'Y && !Z') => 'X && Y && !Z' |
| 108 | lhs: E{{T("X")}}, rhs: E{{T("Y")}, {F("Z")}}, |
| 109 | expect: E{{T("X")}, {T("Y")}, {F("Z")}}, |
| 110 | }, |
| 111 | { // And('X && Y', 'Y && Z') => 'X && Y && Y && Z' |
| 112 | lhs: E{{T("X")}, {T("Y")}}, rhs: E{{T("Y")}, {T("Z")}}, |
| 113 | expect: E{{T("X")}, {T("Y")}, {T("Y")}, {T("Z")}}, |
| 114 | }, |
| 115 | { // And('!X && Y', 'Y && !Z') => '!X && Y && Y && !Z' |
| 116 | lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Y")}, {F("Z")}}, |
| 117 | expect: E{{F("X")}, {T("Y")}, {T("Y")}, {F("Z")}}, |
| 118 | }, |
| 119 | { // And('X || Y', 'Z') => '(X || Y) && Z' |
| 120 | lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Z")}}, |
| 121 | expect: E{{T("X"), T("Y")}, {T("Z")}}, |
| 122 | }, |
| 123 | { // And('!X || Y', 'Z') => '(!X || Y) && Z' |
| 124 | lhs: E{{F("X"), T("Y")}}, rhs: E{{T("Z")}}, |
| 125 | expect: E{{F("X"), T("Y")}, {T("Z")}}, |
| 126 | }, |
| 127 | { // And('X || !Y', 'Z') => '(X || !Y) && Z' |
| 128 | lhs: E{{T("X"), F("Y")}}, rhs: E{{T("Z")}}, |
| 129 | expect: E{{T("X"), F("Y")}, {T("Z")}}, |
| 130 | }, |
| 131 | { // And('X || Y', '!Z') => '(X || Y) && !Z' |
| 132 | lhs: E{{T("X"), T("Y")}}, rhs: E{{F("Z")}}, |
| 133 | expect: E{{T("X"), T("Y")}, {F("Z")}}, |
| 134 | }, |
| 135 | { // And('X', 'Y || Z') => 'X && (Y || Z)' |
| 136 | lhs: E{{T("X")}}, rhs: E{{T("Y"), T("Z")}}, |
| 137 | expect: E{{T("X")}, {T("Y"), T("Z")}}, |
| 138 | }, |
| 139 | { // And('!X', 'Y || Z') => '!X && (Y || Z)' |
| 140 | lhs: E{{F("X")}}, rhs: E{{T("Y"), T("Z")}}, |
| 141 | expect: E{{F("X")}, {T("Y"), T("Z")}}, |
| 142 | }, |
| 143 | { // And('X', '!Y || Z') => 'X && (!Y || Z)' |
| 144 | lhs: E{{T("X")}}, rhs: E{{F("Y"), T("Z")}}, |
| 145 | expect: E{{T("X")}, {F("Y"), T("Z")}}, |
| 146 | }, |
| 147 | { // And('X', 'Y || !Z') => 'X && (Y || !Z)' |
| 148 | lhs: E{{T("X")}}, rhs: E{{T("Y"), F("Z")}}, |
| 149 | expect: E{{T("X")}, {T("Y"), F("Z")}}, |
| 150 | }, |
| 151 | { // And('X || Y', 'Y || Z') => '(X || Y) && (Y || Z)' |
| 152 | lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Y"), T("Z")}}, |
| 153 | expect: E{{T("X"), T("Y")}, {T("Y"), T("Z")}}, |
| 154 | }, |
| 155 | { // And('!X || Y', 'Y || !Z') => '(!X || Y) && (Y || !Z)' |
| 156 | lhs: E{{F("X"), T("Y")}}, rhs: E{{T("Y"), F("Z")}}, |
| 157 | expect: E{{F("X"), T("Y")}, {T("Y"), F("Z")}}, |
| 158 | }, |
| 159 | { // And('X || Y', 'Y && Z') => '(X || Y) && Y && Z' |
| 160 | lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Y")}, {T("Z")}}, |
| 161 | expect: E{{T("X"), T("Y")}, {T("Y")}, {T("Z")}}, |
| 162 | }, |
| 163 | { // And('!X && Y', 'Y || !Z') => '!X && Y && (Y || !Z)' |
| 164 | lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Y"), F("Z")}}, |
| 165 | expect: E{{F("X")}, {T("Y")}, {T("Y"), F("Z")}}, |
| 166 | }, |
| 167 | } { |
| 168 | got := cnf.And(test.lhs, test.rhs) |
| 169 | if diff := cmp.Diff(test.expect, got); diff != "" { |
| 170 | t.Errorf("And('%v', '%v') returned '%v'. Diff:\n%v", test.lhs, test.rhs, got, diff) |
| 171 | } |
| 172 | } |
| 173 | } |
| 174 | |
| 175 | func TestOr(t *testing.T) { |
| 176 | type E = cnf.Expr |
| 177 | for _, test := range []struct { |
| 178 | lhs, rhs cnf.Expr |
| 179 | expect cnf.Expr |
| 180 | }{ |
| 181 | { // Or('', '') => '' |
| 182 | lhs: E{}, rhs: E{}, |
| 183 | expect: E{}, |
| 184 | }, |
| 185 | { // Or('X', '') => 'X' |
| 186 | lhs: E{{T("X")}}, rhs: E{}, |
| 187 | expect: E{{T("X")}}, |
| 188 | }, |
| 189 | { // Or('!X', '') => '!X' |
| 190 | lhs: E{{F("X")}}, rhs: E{}, |
| 191 | expect: E{{F("X")}}, |
| 192 | }, |
| 193 | { // Or('', 'X') => 'X' |
| 194 | lhs: E{}, rhs: E{{T("X")}}, |
| 195 | expect: E{{T("X")}}, |
| 196 | }, |
| 197 | { // Or('', '!X') => '!X' |
| 198 | lhs: E{}, rhs: E{{F("X")}}, |
| 199 | expect: E{{F("X")}}, |
| 200 | }, |
| 201 | { // Or('X', 'Y') => 'X || Y' |
| 202 | lhs: E{{T("X")}}, rhs: E{{T("Y")}}, |
| 203 | expect: E{{T("X"), T("Y")}}, |
| 204 | }, |
| 205 | { // Or('X', '!Y') => 'X || !Y' |
| 206 | lhs: E{{T("X")}}, rhs: E{{F("Y")}}, |
| 207 | expect: E{{T("X"), F("Y")}}, |
| 208 | }, |
| 209 | { // Or('Y', 'X') => 'Y || X' |
| 210 | lhs: E{{T("Y")}}, rhs: E{{T("X")}}, |
| 211 | expect: E{{T("Y"), T("X")}}, |
| 212 | }, |
| 213 | { // Or('!Y', 'X') => '!Y || X' |
| 214 | lhs: E{{F("Y")}}, rhs: E{{T("X")}}, |
| 215 | expect: E{{F("Y"), T("X")}}, |
| 216 | }, |
| 217 | { // Or('X && Y', 'Z') => '(X || Z) && (Y || Z)' |
| 218 | lhs: E{{T("X")}, {T("Y")}}, rhs: E{{T("Z")}}, |
| 219 | expect: E{{T("X"), T("Z")}, {T("Y"), T("Z")}}, |
| 220 | }, |
| 221 | { // Or('!X && Y', 'Z') => '(!X || Z) && (Y || Z)' |
| 222 | lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Z")}}, |
| 223 | expect: E{{F("X"), T("Z")}, {T("Y"), T("Z")}}, |
| 224 | }, |
| 225 | { // Or('X && !Y', 'Z') => '(X || Z) && (!Y || Z)' |
| 226 | lhs: E{{T("X")}, {F("Y")}}, rhs: E{{T("Z")}}, |
| 227 | expect: E{{T("X"), T("Z")}, {F("Y"), T("Z")}}, |
| 228 | }, |
| 229 | { // Or('X && Y', '!Z') => '(X || !Z) && (Y || !Z)' |
| 230 | lhs: E{{T("X")}, {T("Y")}}, rhs: E{{F("Z")}}, |
| 231 | expect: E{{T("X"), F("Z")}, {T("Y"), F("Z")}}, |
| 232 | }, |
| 233 | { // Or('X', 'Y && Z') => '(X || Y) && (X || Z)' |
| 234 | lhs: E{{T("X")}}, rhs: E{{T("Y")}, {T("Z")}}, |
| 235 | expect: E{{T("X"), T("Y")}, {T("X"), T("Z")}}, |
| 236 | }, |
| 237 | { // Or('!X', 'Y && Z') => '(!X || Y) && (!X || Z)' |
| 238 | lhs: E{{F("X")}}, rhs: E{{T("Y")}, {T("Z")}}, |
| 239 | expect: E{{F("X"), T("Y")}, {F("X"), T("Z")}}, |
| 240 | }, |
| 241 | { // Or('X', '!Y && Z') => '(X || !Y) && (X || Z)' |
| 242 | lhs: E{{T("X")}}, rhs: E{{F("Y")}, {T("Z")}}, |
| 243 | expect: E{{T("X"), F("Y")}, {T("X"), T("Z")}}, |
| 244 | }, |
| 245 | { // Or('X', 'Y && !Z') => '(X || Y) && (X || !Z)' |
| 246 | lhs: E{{T("X")}}, rhs: E{{T("Y")}, {F("Z")}}, |
| 247 | expect: E{{T("X"), T("Y")}, {T("X"), F("Z")}}, |
| 248 | }, |
| 249 | { // Or('X && Y', 'Z && W') => '(X || Z) && (X || W) && (Y || Z) && (Y || W)' |
| 250 | lhs: E{{T("X")}, {T("Y")}}, rhs: E{{T("Z")}, {T("W")}}, |
| 251 | expect: E{{T("X"), T("Z")}, {T("X"), T("W")}, {T("Y"), T("Z")}, {T("Y"), T("W")}}, |
| 252 | }, |
| 253 | { // Or('!X && Y', 'Z && !W') => '(!X || Z) && (!X || !W) && (Y || Z) && (Y || !W)' |
| 254 | lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Z")}, {F("W")}}, |
| 255 | expect: E{{F("X"), T("Z")}, {F("X"), F("W")}, {T("Y"), T("Z")}, {T("Y"), F("W")}}, |
| 256 | }, |
| 257 | { // Or('X || Y', 'Z') => 'X || Y || Z' |
| 258 | lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Z")}}, |
| 259 | expect: E{{T("X"), T("Y"), T("Z")}}, |
| 260 | }, |
| 261 | { // Or('!X || Y', 'Z') => '!X || Y || Z' |
| 262 | lhs: E{{F("X"), T("Y")}}, rhs: E{{T("Z")}}, |
| 263 | expect: E{{F("X"), T("Y"), T("Z")}}, |
| 264 | }, |
| 265 | { // Or('X || !Y', 'Z') => 'X || !Y || Z' |
| 266 | lhs: E{{T("X"), F("Y")}}, rhs: E{{T("Z")}}, |
| 267 | expect: E{{T("X"), F("Y"), T("Z")}}, |
| 268 | }, |
| 269 | { // Or('X || Y', '!Z') => 'X || Y || !Z' |
| 270 | lhs: E{{T("X"), T("Y")}}, rhs: E{{F("Z")}}, |
| 271 | expect: E{{T("X"), T("Y"), F("Z")}}, |
| 272 | }, |
| 273 | { // Or('X', 'Y || Z') => 'X || Y || Z' |
| 274 | lhs: E{{T("X")}}, rhs: E{{T("Y"), T("Z")}}, |
| 275 | expect: E{{T("X"), T("Y"), T("Z")}}, |
| 276 | }, |
| 277 | { // Or('!X', 'Y || Z') => '!X || Y || Z' |
| 278 | lhs: E{{F("X")}}, rhs: E{{T("Y"), T("Z")}}, |
| 279 | expect: E{{F("X"), T("Y"), T("Z")}}, |
| 280 | }, |
| 281 | { // Or('X', '!Y || Z') => 'X || !Y || Z' |
| 282 | lhs: E{{T("X")}}, rhs: E{{F("Y"), T("Z")}}, |
| 283 | expect: E{{T("X"), F("Y"), T("Z")}}, |
| 284 | }, |
| 285 | { // Or('X', 'Y || !Z') => 'X || Y || !Z' |
| 286 | lhs: E{{T("X")}}, rhs: E{{T("Y"), F("Z")}}, |
| 287 | expect: E{{T("X"), T("Y"), F("Z")}}, |
| 288 | }, |
| 289 | { // Or('X || Y', 'Y || Z') => 'X || Y || Y || Z' |
| 290 | lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Y"), T("Z")}}, |
| 291 | expect: E{{T("X"), T("Y"), T("Y"), T("Z")}}, |
| 292 | }, |
| 293 | { // Or('!X || Y', 'Y || !Z') => '!X || Y || Y || !Z' |
| 294 | lhs: E{{F("X"), T("Y")}}, rhs: E{{T("Y"), F("Z")}}, |
| 295 | expect: E{{F("X"), T("Y"), T("Y"), F("Z")}}, |
| 296 | }, |
| 297 | { // Or('X || Y', 'Y && Z') => '(X || Y || Y) && (X || Y || Z)' |
| 298 | lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Y")}, {T("Z")}}, |
| 299 | expect: E{{T("X"), T("Y"), T("Y")}, {T("X"), T("Y"), T("Z")}}, |
| 300 | }, |
| 301 | { // Or('!X && Y', 'Z || !W') => '(!X || Z || !W) && (Y || Z || !W)' |
| 302 | lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Z"), F("W")}}, |
| 303 | expect: E{{F("X"), T("Z"), F("W")}, {T("Y"), T("Z"), F("W")}}, |
| 304 | }, |
| 305 | } { |
| 306 | got := cnf.Or(test.lhs, test.rhs) |
| 307 | if diff := cmp.Diff(test.expect, got); diff != "" { |
| 308 | t.Errorf("Or('%v', '%v') returned '%v'. Diff:\n%v", test.lhs, test.rhs, got, diff) |
| 309 | } |
| 310 | } |
| 311 | } |
| 312 | |
| 313 | func TestNot(t *testing.T) { |
| 314 | type E = cnf.Expr |
| 315 | for _, test := range []struct { |
| 316 | expr cnf.Expr |
| 317 | expect cnf.Expr |
| 318 | }{ |
| 319 | { // Not('') => '' |
| 320 | expr: E{}, |
| 321 | expect: E{}, |
| 322 | }, |
| 323 | { // Not('X') => '!X' |
| 324 | expr: E{{T("X")}}, |
| 325 | expect: E{{F("X")}}, |
| 326 | }, |
| 327 | { // Not('!X') => 'X' |
| 328 | expr: E{{F("X")}}, |
| 329 | expect: E{{T("X")}}, |
| 330 | }, |
| 331 | { // Not('X || Y') => '!X && !Y' |
| 332 | expr: E{{T("X"), T("Y")}}, |
| 333 | expect: E{{F("X")}, {F("Y")}}, |
| 334 | }, |
| 335 | { // Not('X || !Y') => '!X && Y' |
| 336 | expr: E{{T("X"), F("Y")}}, |
| 337 | expect: E{{F("X")}, {T("Y")}}, |
| 338 | }, |
| 339 | { // Not('X && Y') => '!X || !Y' |
| 340 | expr: E{{T("X")}, {T("Y")}}, |
| 341 | expect: E{{F("X"), F("Y")}}, |
| 342 | }, |
| 343 | { // Not('!X && Y') => 'X || !Y' |
| 344 | expr: E{{F("X")}, {T("Y")}}, |
| 345 | expect: E{{T("X"), F("Y")}}, |
| 346 | }, |
| 347 | { // Not('(X || Y) && Z') => '(!X || !Z) && (!Y || !Z)' |
| 348 | expr: E{{T("X"), T("Y")}, {T("Z")}}, |
| 349 | expect: E{{F("X"), F("Z")}, {F("Y"), F("Z")}}, |
| 350 | }, |
| 351 | { // Not('X && (Y || Z)') => '(!X || !Y) && (!X || !Z)' |
| 352 | expr: E{{T("X")}, {T("Y"), T("Z")}}, |
| 353 | expect: E{{F("X"), F("Y")}, {F("X"), F("Z")}}, |
| 354 | }, |
| 355 | { // Not('X && (!Y || Z)') => '(!X || Y) && (!X || !Z)' |
| 356 | expr: E{{T("X")}, {F("Y"), T("Z")}}, |
| 357 | expect: E{{F("X"), T("Y")}, {F("X"), F("Z")}}, |
| 358 | }, |
| 359 | { // Not('(X || Y) && (Z || W)') => '(!X || !Z) && (!X || !W) && (!Y || !Z) && (!Y || !W)' |
| 360 | expr: E{{T("X"), T("Y")}, {T("Z"), T("W")}}, |
| 361 | expect: E{{F("X"), F("Z")}, {F("X"), F("W")}, {F("Y"), F("Z")}, {F("Y"), F("W")}}, |
| 362 | }, |
| 363 | { // Not('(X || !Y) && (!Z || W)') => '(!X || Z) && (!X || !W) && (Y || Z) && (Y || !W)' |
| 364 | expr: E{{T("X"), F("Y")}, {F("Z"), T("W")}}, |
| 365 | expect: E{{F("X"), T("Z")}, {F("X"), F("W")}, {T("Y"), T("Z")}, {T("Y"), F("W")}}, |
| 366 | }, |
| 367 | } { |
| 368 | got := cnf.Not(test.expr) |
| 369 | if diff := cmp.Diff(test.expect, got); diff != "" { |
| 370 | t.Errorf("Not('%v') returned '%v'. Diff:\n%v", test.expr, got, diff) |
| 371 | } |
| 372 | } |
| 373 | } |