LogiXpr
Loading...
Searching...
No Matches
equivLaws.cpp
Go to the documentation of this file.
1
6#include "../include/equivLaws.h"
7
8std::unordered_map<EquivLaws::EquivLaw, std::string> EquivLaws::laws = {
9 {identity, "Identity Law"},
10 {domination, "Domination Law"},
11 {idempotent, "Idempotent Law"},
12 {doubleNegation, "Double Negation Law"},
13 {commutative, "Commutative Law"},
14 {associative, "Associative Law"},
15 {associativeReversed, "Associative Law"},
16 {distributive, "Distributive Law"},
17 {distributiveReversed, "Distributive Law"},
18 {deMorgan, "De Morgan's Law"},
19 {deMorganReversed, "De Morgan's Law"},
20 {absorption, "Absorption Law"},
21 {negation, "Negation Law"},
22};
23
24std::unordered_map<EquivLaws::EquivLaw, std::string> EquivLaws::implications = {
25 {implication0, "Implication Equivalence"},
26 {implication0Reversed, "Implication Equivalence"},
27 {implication1, "Implication Equivalence"},
28 {implication1Reversed, "Implication Equivalence"},
29 {implication2, "Implication Equivalence"},
30 {implication2Reversed, "Implication Equivalence"},
31 {implication3, "Implication Equivalence"},
32 {implication3Reversed, "Implication Equivalence"},
33 {implication4, "Implication Equivalence"},
34 {implication4Reversed, "Implication Equivalence"},
35 {implication5, "Implication Equivalence"},
36 {implication5Reversed, "Implication Equivalence"},
37 {implication6, "Implication Equivalence"},
38 {implication6Reversed, "Implication Equivalence"},
39 {implication7, "Implication Equivalence"},
40 {implication7Reversed, "Implication Equivalence"},
41 {implication8, "Implication Equivalence"},
42 {implication8Reversed, "Implication Equivalence"},
43};
44
45std::unordered_map<EquivLaws::EquivLaw, std::string>
46 EquivLaws::bidirectionalImplications = {
47 {bidirectionalImplication0, "Bidirectional Implication Equivalence"},
48 {bidirectionalImplication0Reversed, "Bidirectional Implication Equivalence"},
49 {bidirectionalImplication1, "Bidirectional Implication Equivalence"},
50 {bidirectionalImplication2, "Bidirectional Implication Equivalence"},
51 {bidirectionalImplication2Reversed, "Bidirectional Implication Equivalence"},
52 {bidirectionalImplication3, "Bidirectional Implication Equivalence"},
53 {bidirectionalImplication3Reversed, "Bidirectional Implication Equivalence"},
54 {bidirectionalImplication4, "Bidirectional Implication Equivalence"},
55 {bidirectionalImplication4Reversed, "Bidirectional Implication Equivalence"},
56};
57
58void EquivLaws::replace(std::shared_ptr<Expression> &expression,
59 std::shared_ptr<Expression> newExpression)
60{
61 std::shared_ptr<Expression> parent = expression->getParent();
62 if (parent == nullptr)
63 {
64 // if the parent is null, then the current expression is the root
65 // set the new expression as the root
66 expression = newExpression;
67 expression->setParent(nullptr);
68 return;
69 }
70
71 // determine if the current expression is the left or right subexpression of
72 // the parent
73 if (parent->getLeft() == expression)
74 parent->setLeft(newExpression, parent);
75 else
76 parent->setRight(newExpression, parent);
77 expression = newExpression;
78}
79
80bool EquivLaws::identity(std::shared_ptr<Expression> &expression)
81{
82 if (expression->getValue() == AND && expression->getRight()->getValue() == TRUE)
83 {
84 // replace the current expression with the left
85 std::shared_ptr<Expression> parent = expression->getParent();
86 std::shared_ptr<Expression> newExpression = expression->getLeft();
87
88 replace(expression, newExpression);
89 return true;
90 }
91 else if (expression->getValue() == OR && expression->getRight()->getValue() == FALSE)
92 {
93 // replace the current expression with the left
94 std::shared_ptr<Expression> parent = expression->getParent();
95 std::shared_ptr<Expression> newExpression = expression->getLeft();
96
97 replace(expression, newExpression);
98 return true;
99 }
100 return false;
101}
102
103bool EquivLaws::domination(std::shared_ptr<Expression> &expression)
104{
105 // p & F = F, p | T = T
106 if (expression->getValue() == AND && expression->getRight()->getValue() == FALSE)
107 {
108 // replace the current expression with the right
109 std::shared_ptr<Expression> parent = expression->getParent();
110 std::shared_ptr<Expression> newExpression = expression->getRight();
111
112 replace(expression, newExpression);
113
114 return true;
115 }
116 else if (expression->getValue() == OR && expression->getRight()->getValue() == TRUE)
117 {
118 // replace the current expression with the right
119 std::shared_ptr<Expression> parent = expression->getParent();
120 std::shared_ptr<Expression> newExpression = expression->getRight();
121
122 replace(expression, newExpression);
123
124 return true;
125 }
126 return false;
127}
128
129bool EquivLaws::idempotent(std::shared_ptr<Expression> &expression)
130{
131 if (expression->getValue() == AND || expression->getValue() == OR)
132 {
133 // p & p = p, p | p = p
134 std::shared_ptr<Expression> left = expression->getLeft();
135 std::shared_ptr<Expression> right = expression->getRight();
136
137 if (!left->compare(right))
138 return false;
139
140 // replace the current expression with the left
141 std::shared_ptr<Expression> parent = expression->getParent();
142 std::shared_ptr<Expression> newExpression = expression->getLeft();
143
144 replace(expression, newExpression);
145
146 return true;
147 }
148 return false;
149}
150
151bool EquivLaws::doubleNegation(std::shared_ptr<Expression> &expression)
152{
153 // !!p = p
154 if (expression->getValue() == NOT &&
155 expression->getLeft()->getValue() == NOT)
156 {
157 // replace the current expression with the left
158 std::shared_ptr<Expression> parent = expression->getParent();
159 std::shared_ptr<Expression> newExpression =
160 expression->getLeft()->getLeft();
161
162 replace(expression, newExpression);
163
164 return true;
165 }
166 return false;
167}
168
169bool EquivLaws::commutative(std::shared_ptr<Expression> &expression)
170{
171 if (expression->getValue() == AND || expression->getValue() == OR)
172 {
173 // p & q = q & p, p | q = q | p
174 std::shared_ptr<Expression> left = expression->getLeft();
175 std::shared_ptr<Expression> right = expression->getRight();
176
177 // create a new expression
178 std::shared_ptr<Expression> newExpression =
179 std::make_shared<Expression>(expression->getValue());
180 newExpression->setLeft(right, newExpression);
181 newExpression->setRight(left, newExpression);
182
183 replace(expression, newExpression);
184
185 return true;
186 }
187 return false;
188}
189
190bool EquivLaws::associative(std::shared_ptr<Expression> &expression)
191{
192 // (p | q) | r = p | (q | r), (p & q) & r = p & (q & r)
193 if ((expression->getValue() == AND || expression->getValue() == OR) &&
194 expression->getLeft()->getValue() == expression->getValue())
195 {
196 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
197 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
198 std::shared_ptr<Expression> right = expression->getRight();
199
200 // create a new expression
201 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(expression->getValue());
202 newExpression->setLeft(left1, newExpression);
203 newExpression->setRight(std::make_shared<Expression>(expression->getValue()), newExpression);
204 newExpression->getRight()->setLeft(left2, newExpression->getRight());
205 newExpression->getRight()->setRight(right, newExpression->getRight());
206
207 replace(expression, newExpression);
208
209 return true;
210 }
211 return false;
212}
213
214bool EquivLaws::associativeReversed(std::shared_ptr<Expression> &expression)
215{
216 // p | (q | r) = (p | q) | r, p & (q & r) = (p & q) & r
217 if ((expression->getValue() == AND || expression->getValue() == OR) && expression->getRight()->getValue() == expression->getValue())
218 {
219 std::shared_ptr<Expression> left = expression->getLeft();
220 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
221 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
222
223 // create a new expression
224 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(expression->getValue());
225 newExpression->setLeft(std::make_shared<Expression>(expression->getValue()), newExpression);
226 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
227 newExpression->getLeft()->setRight(right1, newExpression->getLeft());
228 newExpression->setRight(right2, newExpression);
229
230 replace(expression, newExpression);
231
232 return true;
233 }
234 return false;
235}
236
237bool EquivLaws::distributive(std::shared_ptr<Expression> &expression)
238{
239 // p | (q & r) = (p | q) & (p | r), p & (q | r) = (p & q) | (p & r)
240 if (expression->getValue() == AND && expression->getRight()->getValue() == OR)
241 {
242 std::shared_ptr<Expression> left = expression->getLeft();
243 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
244 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
245
246 // create a new expression
247 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(OR);
248 newExpression->setLeft(std::make_shared<Expression>(AND), newExpression);
249 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
250 newExpression->getLeft()->setRight(right1, newExpression->getLeft());
251 newExpression->setRight(std::make_shared<Expression>(AND), newExpression);
252 newExpression->getRight()->setLeft(left, newExpression->getRight());
253 newExpression->getRight()->setRight(right2, newExpression->getRight());
254
255 replace(expression, newExpression);
256
257 return true;
258 }
259 else if (expression->getValue() == OR && expression->getRight()->getValue() == AND)
260 {
261 std::shared_ptr<Expression> left = expression->getLeft();
262 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
263 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
264
265 // create a new expression
266 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(AND);
267 newExpression->setLeft(std::make_shared<Expression>(OR), newExpression);
268 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
269 newExpression->getLeft()->setRight(right1, newExpression->getLeft());
270 newExpression->setRight(std::make_shared<Expression>(OR), newExpression);
271 newExpression->getRight()->setLeft(left, newExpression->getRight());
272 newExpression->getRight()->setRight(right2, newExpression->getRight());
273
274 replace(expression, newExpression);
275
276 return true;
277 }
278 return false;
279}
280
281bool EquivLaws::distributiveReversed(std::shared_ptr<Expression> &expression)
282{
283 // (p | q) & (p | r) = p | (q & r), (p & q) | (p & r) = p & (q | r)
284 if (expression->getValue() == AND && expression->getLeft()->getValue() == OR && expression->getRight()->getValue() == OR)
285 {
286 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
287 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
288 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
289 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
290
291 // check if left1 == right1
292 if (!left1->compare(right1))
293 return false;
294
295 // create a new expression
296 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(OR);
297 newExpression->setLeft(left1, newExpression);
298 newExpression->setRight(std::make_shared<Expression>(AND), newExpression);
299 newExpression->getRight()->setLeft(left2, newExpression->getRight());
300 newExpression->getRight()->setRight(right2, newExpression->getRight());
301
302 replace(expression, newExpression);
303
304 return true;
305 }
306 else if (expression->getValue() == OR && expression->getLeft()->getValue() == AND && expression->getRight()->getValue() == AND)
307 {
308 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
309 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
310 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
311 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
312
313 // check if left1 == right1
314 if (!left1->compare(right1))
315 return false;
316
317 // create a new expression
318 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(AND);
319 newExpression->setLeft(left1, newExpression);
320 newExpression->setRight(std::make_shared<Expression>(OR), newExpression);
321 newExpression->getRight()->setLeft(left2, newExpression->getRight());
322 newExpression->getRight()->setRight(right2, newExpression->getRight());
323
324 replace(expression, newExpression);
325
326 return true;
327 }
328 return false;
329}
330
331bool EquivLaws::deMorgan(std::shared_ptr<Expression> &expression)
332{
333 // !(p | q) = !p & !q, !(p & q) = !p | !q
334 if (expression->getValue() == NOT)
335 {
336 if (expression->getLeft()->getValue() == OR)
337 {
338 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
339 std::shared_ptr<Expression> right = expression->getLeft()->getRight();
340
341 // create a new expression
342 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(AND);
343 newExpression->setLeft(std::make_shared<Expression>(NOT), newExpression);
344 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
345 newExpression->setRight(std::make_shared<Expression>(NOT), newExpression);
346 newExpression->getRight()->setLeft(right, newExpression->getRight());
347
348 replace(expression, newExpression);
349
350 return true;
351 }
352 else if (expression->getLeft()->getValue() == AND)
353 {
354 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
355 std::shared_ptr<Expression> right = expression->getLeft()->getRight();
356
357 // create a new expression with the left and right subexpressions swapped
358 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(OR);
359 newExpression->setLeft(std::make_shared<Expression>(NOT), newExpression);
360 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
361 newExpression->setRight(std::make_shared<Expression>(NOT), newExpression);
362 newExpression->getRight()->setLeft(right, newExpression->getRight());
363
364 replace(expression, newExpression);
365
366 return true;
367 }
368 }
369 return false;
370}
371
372bool EquivLaws::deMorganReversed(std::shared_ptr<Expression> &expression)
373{
374 // !p & !q = !(p | q), !p | !q = !(p & q)
375 if (expression->getValue() == AND && expression->getLeft()->getValue() == NOT && expression->getRight()->getValue() == NOT)
376 {
377 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
378 std::shared_ptr<Expression> right = expression->getRight()->getLeft();
379
380 // create a new expression
381 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(NOT);
382 newExpression->setLeft(std::make_shared<Expression>(OR), newExpression);
383 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
384 newExpression->getLeft()->setRight(right, newExpression->getLeft());
385
386 replace(expression, newExpression);
387
388 return true;
389 }
390 else if (expression->getValue() == OR && expression->getLeft()->getValue() == NOT && expression->getRight()->getValue() == NOT)
391 {
392 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
393 std::shared_ptr<Expression> right = expression->getRight()->getLeft();
394
395 // create a new expression
396 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(NOT);
397 newExpression->setLeft(std::make_shared<Expression>(AND), newExpression);
398 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
399 newExpression->getLeft()->setRight(right, newExpression->getLeft());
400
401 replace(expression, newExpression);
402
403 return true;
404 }
405 return false;
406}
407
408bool EquivLaws::absorption(std::shared_ptr<Expression> &expression)
409{
410 // p | (p & q) = p, p & (p | q) = p
411 if ((expression->getValue() == OR && expression->getRight()->getValue() == AND) || (expression->getValue() == AND && expression->getRight()->getValue() == OR))
412 {
413
414 std::shared_ptr<Expression> left1 = expression->getLeft();
415 std::shared_ptr<Expression> left2 = expression->getRight()->getLeft();
416 std::shared_ptr<Expression> right1 = expression->getRight()->getRight();
417
418 // check if left1 == left2
419 if (!left1->compare(left2))
420 return false;
421
422 replace(expression, left1);
423
424 return true;
425 }
426 return false;
427}
428
429bool EquivLaws::negation(std::shared_ptr<Expression> &expression)
430{
431 // p | !p = T, p & !p = F
432 if (expression->getValue() == OR && expression->getRight()->getValue() == NOT)
433 {
434 std::shared_ptr<Expression> left = expression->getLeft();
435 std::shared_ptr<Expression> right = expression->getRight()->getLeft();
436 if (!left->compare(right))
437 return false;
438
439 // replace the current expression with T
440 replace(expression, std::make_shared<Expression>(TRUE));
441
442 return true;
443 }
444 else if (expression->getValue() == AND && expression->getRight()->getValue() == NOT)
445 {
446 std::shared_ptr<Expression> left = expression->getLeft();
447 std::shared_ptr<Expression> right = expression->getRight()->getLeft();
448 if (!left->compare(right))
449 return false;
450
451 // replace the current expression with F
452 replace(expression, std::make_shared<Expression>(FALSE));
453
454 return true;
455 }
456 return false;
457}
458
459bool EquivLaws::implication0(std::shared_ptr<Expression> &expression)
460{
461 // p -> q = !p | q
462 if (expression->getValue() == IMPLIES)
463 {
464 std::shared_ptr<Expression> left = expression->getLeft();
465 std::shared_ptr<Expression> right = expression->getRight();
466
467 // create a new expression
468 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(OR);
469 newExpression->setLeft(std::make_shared<Expression>(NOT), newExpression);
470 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
471 newExpression->setRight(right, newExpression);
472
473 replace(expression, newExpression);
474
475 return true;
476 }
477 return false;
478}
479
480bool EquivLaws::implication0Reversed(std::shared_ptr<Expression> &expression)
481{
482 // !p | q = p -> q
483 if (expression->getValue() == OR && expression->getLeft()->getValue() == NOT)
484 {
485 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
486 std::shared_ptr<Expression> right = expression->getRight();
487
488 // create a new expression
489 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IMPLIES);
490 newExpression->setLeft(left, newExpression);
491 newExpression->setRight(right, newExpression);
492
493 replace(expression, newExpression);
494
495 return true;
496 }
497 return false;
498}
499
500bool EquivLaws::implication1(std::shared_ptr<Expression> &expression)
501{
502 // p -> q = !q -> !p
503 if (expression->getValue() == IMPLIES)
504 {
505 std::shared_ptr<Expression> left = expression->getLeft();
506 std::shared_ptr<Expression> right = expression->getRight();
507
508 // create a new expression
509 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IMPLIES);
510 newExpression->setLeft(std::make_shared<Expression>(NOT), newExpression);
511 newExpression->getLeft()->setLeft(right, newExpression->getLeft());
512 newExpression->setRight(std::make_shared<Expression>(NOT), newExpression);
513 newExpression->getRight()->setLeft(left, newExpression->getRight());
514
515 replace(expression, newExpression);
516
517 return true;
518 }
519 return false;
520}
521
522bool EquivLaws::implication1Reversed(std::shared_ptr<Expression> &expression)
523{
524 // !q -> !p = p -> q
525 if (expression->getValue() == IMPLIES && expression->getLeft()->getValue() == NOT && expression->getRight()->getValue() == NOT)
526 {
527 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
528 std::shared_ptr<Expression> right = expression->getRight()->getLeft();
529
530 // create a new expression
531 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IMPLIES);
532 newExpression->setLeft(right, newExpression);
533 newExpression->setRight(left, newExpression);
534
535 replace(expression, newExpression);
536
537 return true;
538 }
539 return false;
540}
541
542bool EquivLaws::implication2(std::shared_ptr<Expression> &expression)
543{
544 // p | q = !p -> q
545 if (expression->getValue() == OR)
546 {
547 std::shared_ptr<Expression> left = expression->getLeft();
548 std::shared_ptr<Expression> right = expression->getRight();
549
550 // create a new expression
551 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IMPLIES);
552 newExpression->setLeft(std::make_shared<Expression>(NOT), newExpression);
553 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
554 newExpression->setRight(right, newExpression);
555
556 replace(expression, newExpression);
557
558 return true;
559 }
560 return false;
561}
562
563bool EquivLaws::implication2Reversed(std::shared_ptr<Expression> &expression)
564{
565 // !p -> q = p | q
566 if (expression->getValue() == IMPLIES && expression->getLeft()->getValue() == NOT)
567 {
568 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
569 std::shared_ptr<Expression> right = expression->getRight();
570
571 // create a new expression
572 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(OR);
573 newExpression->setLeft(left, newExpression);
574 newExpression->setRight(right, newExpression);
575
576 replace(expression, newExpression);
577
578 return true;
579 }
580 return false;
581}
582
583bool EquivLaws::implication3(std::shared_ptr<Expression> &expression)
584{
585 // p & q = !(p -> !q)
586 if (expression->getValue() == AND)
587 {
588 std::shared_ptr<Expression> left = expression->getLeft();
589 std::shared_ptr<Expression> right = expression->getRight();
590
591 // create a new expression
592 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(NOT);
593 newExpression->setLeft(std::make_shared<Expression>(IMPLIES), newExpression);
594 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
595 newExpression->getLeft()->setRight(std::make_shared<Expression>(NOT), newExpression->getLeft());
596 newExpression->getLeft()->getRight()->setLeft(right, newExpression->getLeft()->getRight());
597
598 replace(expression, newExpression);
599
600 return true;
601 }
602 return false;
603}
604
605bool EquivLaws::implication3Reversed(std::shared_ptr<Expression> &expression)
606{
607 // !(p -> !q) = p & q
608 if (expression->getValue() == NOT && expression->getLeft()->getValue() == IMPLIES && expression->getLeft()->getRight()->getValue() == NOT)
609 {
610 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
611 std::shared_ptr<Expression> right = expression->getLeft()->getRight()->getLeft();
612
613 // create a new expression
614 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(AND);
615 newExpression->setLeft(left, newExpression);
616 newExpression->setRight(right, newExpression);
617
618 replace(expression, newExpression);
619
620 return true;
621 }
622 return false;
623}
624
625bool EquivLaws::implication4(std::shared_ptr<Expression> &expression)
626{
627 // !(p -> q) = p & !q
628 if (expression->getValue() == NOT && expression->getLeft()->getValue() == IMPLIES)
629 {
630 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
631 std::shared_ptr<Expression> right = expression->getLeft()->getRight();
632
633 // create a new expression
634 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(AND);
635 newExpression->setLeft(left, newExpression);
636 newExpression->setRight(std::make_shared<Expression>(NOT), newExpression);
637 newExpression->getRight()->setLeft(right, newExpression->getRight());
638
639 replace(expression, newExpression);
640
641 return true;
642 }
643 return false;
644}
645
646bool EquivLaws::implication4Reversed(std::shared_ptr<Expression> &expression)
647{
648 // p & !q = !(p -> q)
649 if (expression->getValue() == AND && expression->getRight()->getValue() == NOT)
650 {
651 std::shared_ptr<Expression> left = expression->getLeft();
652 std::shared_ptr<Expression> right = expression->getRight()->getLeft();
653
654 // create a new expression
655 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(NOT);
656 newExpression->setLeft(std::make_shared<Expression>(IMPLIES), newExpression);
657 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
658 newExpression->getLeft()->setRight(right, newExpression->getLeft());
659
660 replace(expression, newExpression);
661
662 return true;
663 }
664 return false;
665}
666
667bool EquivLaws::implication5(std::shared_ptr<Expression> &expression)
668{
669 // (p -> q) & (p -> r) = p -> (q & r)
670 if (expression->getValue() == AND && expression->getLeft()->getValue() == IMPLIES && expression->getRight()->getValue() == IMPLIES)
671 {
672 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
673 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
674 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
675 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
676
677 // check if the p's are the same
678 if (!left1->compare(right1))
679 return false;
680
681 // create a new expression
682 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IMPLIES);
683 newExpression->setLeft(left1, newExpression);
684 newExpression->setRight(std::make_shared<Expression>(AND), newExpression);
685 newExpression->getRight()->setLeft(left2, newExpression->getRight());
686 newExpression->getRight()->setRight(right2, newExpression->getRight());
687
688 replace(expression, newExpression);
689
690 return true;
691 }
692 return false;
693}
694
695bool EquivLaws::implication5Reversed(std::shared_ptr<Expression> &expression)
696{
697 // p -> (q & r) = (p -> q) & (p -> r)
698 if (expression->getValue() == IMPLIES && expression->getRight()->getValue() == AND)
699 {
700 std::shared_ptr<Expression> left = expression->getLeft();
701 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
702 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
703
704 // create a new expression
705 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(AND);
706 newExpression->setLeft(std::make_shared<Expression>(IMPLIES), newExpression);
707 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
708 newExpression->getLeft()->setRight(right1, newExpression->getLeft());
709 newExpression->setRight(std::make_shared<Expression>(IMPLIES), newExpression);
710 newExpression->getRight()->setLeft(left, newExpression->getRight());
711 newExpression->getRight()->setRight(right2, newExpression->getRight());
712
713 replace(expression, newExpression);
714
715 return true;
716 }
717 return false;
718}
719
720bool EquivLaws::implication6(std::shared_ptr<Expression> &expression)
721{
722 // (p -> q) & (q -> r) = (p | q) -> r
723 if (expression->getValue() == AND && expression->getLeft()->getValue() == IMPLIES && expression->getRight()->getValue() == IMPLIES)
724 {
725 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
726 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
727 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
728 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
729
730 // check if the q's are the same
731 if (!left2->compare(right1))
732 return false;
733
734 // create a new expression
735 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IMPLIES);
736 newExpression->setLeft(std::make_shared<Expression>(OR), newExpression);
737 newExpression->getLeft()->setLeft(left1, newExpression->getLeft());
738 newExpression->getLeft()->setRight(left2, newExpression->getLeft());
739 newExpression->setRight(right2, newExpression);
740
741 replace(expression, newExpression);
742
743 return true;
744 }
745 return false;
746}
747
748bool EquivLaws::implication6Reversed(std::shared_ptr<Expression> &expression)
749{
750 // (p | q) -> r = (p -> q) & (q -> r)
751 if (expression->getValue() == IMPLIES && expression->getLeft()->getValue() == OR)
752 {
753 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
754 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
755 std::shared_ptr<Expression> right = expression->getRight();
756
757 // create a new expression
758 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(AND);
759 newExpression->setLeft(std::make_shared<Expression>(IMPLIES), newExpression);
760 newExpression->getLeft()->setLeft(left1, newExpression->getLeft());
761 newExpression->getLeft()->setRight(left2, newExpression->getLeft());
762 newExpression->setRight(std::make_shared<Expression>(IMPLIES), newExpression);
763 newExpression->getRight()->setLeft(left2, newExpression->getRight());
764 newExpression->getRight()->setRight(right, newExpression->getRight());
765
766 replace(expression, newExpression);
767
768 return true;
769 }
770 return false;
771}
772
773bool EquivLaws::implication7(std::shared_ptr<Expression> &expression)
774{
775 // (p -> q) | (p -> r) = p -> (q | r)
776 if (expression->getValue() == OR && expression->getLeft()->getValue() == IMPLIES && expression->getRight()->getValue() == IMPLIES)
777 {
778 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
779 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
780 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
781 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
782
783 // check if the p's are the same
784 if (!left1->compare(right1))
785 return false;
786
787 // create a new expression
788 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IMPLIES);
789 newExpression->setLeft(left1, newExpression);
790 newExpression->setRight(std::make_shared<Expression>(OR), newExpression);
791 newExpression->getRight()->setLeft(left2, newExpression->getRight());
792 newExpression->getRight()->setRight(right2, newExpression->getRight());
793
794 replace(expression, newExpression);
795
796 return true;
797 }
798 return false;
799}
800
801bool EquivLaws::implication7Reversed(std::shared_ptr<Expression> &expression)
802{
803 // p -> (q | r) = (p -> q) | (p -> r)
804 if (expression->getValue() == IMPLIES && expression->getRight()->getValue() == OR)
805 {
806 std::shared_ptr<Expression> left = expression->getLeft();
807 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
808 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
809
810 // create a new expression
811 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(OR);
812 newExpression->setLeft(std::make_shared<Expression>(IMPLIES), newExpression);
813 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
814 newExpression->getLeft()->setRight(right1, newExpression->getLeft());
815 newExpression->setRight(std::make_shared<Expression>(IMPLIES), newExpression);
816 newExpression->getRight()->setLeft(left, newExpression->getRight());
817 newExpression->getRight()->setRight(right2, newExpression->getRight());
818
819 replace(expression, newExpression);
820
821 return true;
822 }
823 return false;
824}
825
826bool EquivLaws::implication8(std::shared_ptr<Expression> &expression)
827{
828 // (p -> q) | (q -> r) = (p & q) -> r
829 if (expression->getValue() == OR && expression->getLeft()->getValue() == IMPLIES && expression->getRight()->getValue() == IMPLIES)
830 {
831 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
832 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
833 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
834 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
835
836 // check if the q's are the same
837 if (!left2->compare(right1))
838 return false;
839
840 // create a new expression
841 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IMPLIES);
842 newExpression->setLeft(std::make_shared<Expression>(AND), newExpression);
843 newExpression->getLeft()->setLeft(left1, newExpression->getLeft());
844 newExpression->getLeft()->setRight(left2, newExpression->getLeft());
845 newExpression->setRight(right2, newExpression);
846
847 replace(expression, newExpression);
848
849 return true;
850 }
851 return false;
852}
853
854bool EquivLaws::implication8Reversed(std::shared_ptr<Expression> &expression)
855{
856 // (p & q) -> r = (p -> q) | (q -> r)
857 if (expression->getValue() == IMPLIES && expression->getLeft()->getValue() == AND)
858 {
859 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
860 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
861 std::shared_ptr<Expression> right = expression->getRight();
862
863 // create a new expression
864 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(OR);
865 newExpression->setLeft(std::make_shared<Expression>(IMPLIES), newExpression);
866 newExpression->getLeft()->setLeft(left1, newExpression->getLeft());
867 newExpression->getLeft()->setRight(left2, newExpression->getLeft());
868 newExpression->setRight(std::make_shared<Expression>(IMPLIES), newExpression);
869 newExpression->getRight()->setLeft(left2, newExpression->getRight());
870 newExpression->getRight()->setRight(right, newExpression->getRight());
871
872 replace(expression, newExpression);
873
874 return true;
875 }
876 return false;
877}
878
879bool EquivLaws::bidirectionalImplication0(std::shared_ptr<Expression> &expression)
880{
881 // p <-> q = (p -> q) & (q -> p)
882 if (expression->getValue() == IFF)
883 {
884 std::shared_ptr<Expression> left = expression->getLeft();
885 std::shared_ptr<Expression> right = expression->getRight();
886
887 // create a new expression
888 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(AND);
889 newExpression->setLeft(std::make_shared<Expression>(IMPLIES), newExpression);
890 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
891 newExpression->getLeft()->setRight(right, newExpression->getLeft());
892 newExpression->setRight(std::make_shared<Expression>(IMPLIES), newExpression);
893 newExpression->getRight()->setLeft(right, newExpression->getRight());
894 newExpression->getRight()->setRight(left, newExpression->getRight());
895
896 replace(expression, newExpression);
897
898 return true;
899 }
900 return false;
901}
902
903bool EquivLaws::bidirectionalImplication0Reversed(std::shared_ptr<Expression> &expression)
904{
905 // (p -> q) & (q -> p) = p <-> q
906 if (expression->getValue() == AND && expression->getLeft()->getValue() == IMPLIES && expression->getRight()->getValue() == IMPLIES)
907 {
908 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
909 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
910 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft();
911 std::shared_ptr<Expression> right2 = expression->getRight()->getRight();
912
913 // check if the q's are the same
914 if (!left2->compare(right1))
915 return false;
916
917 // create a new expression
918 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IFF);
919 newExpression->setLeft(left1, newExpression);
920 newExpression->setRight(left2, newExpression);
921
922 replace(expression, newExpression);
923
924 return true;
925 }
926 return false;
927}
928
929bool EquivLaws::bidirectionalImplication1(std::shared_ptr<Expression> &expression)
930{
931 // p <-> q = q <-> p
932 if (expression->getValue() == IFF)
933 {
934 std::shared_ptr<Expression> left = expression->getLeft();
935 std::shared_ptr<Expression> right = expression->getRight();
936
937 // create a new expression
938 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IFF);
939 newExpression->setLeft(right, newExpression);
940 newExpression->setRight(left, newExpression);
941
942 replace(expression, newExpression);
943
944 return true;
945 }
946 return false;
947}
948
949bool EquivLaws::bidirectionalImplication2(std::shared_ptr<Expression> &expression)
950{
951 // p <-> q = !p <-> !q
952 if (expression->getValue() == IFF)
953 {
954 std::shared_ptr<Expression> left = expression->getLeft();
955 std::shared_ptr<Expression> right = expression->getRight();
956
957 // create a new expression
958 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IFF);
959 newExpression->setLeft(std::make_shared<Expression>(NOT), newExpression);
960 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
961 newExpression->setRight(std::make_shared<Expression>(NOT), newExpression);
962 newExpression->getRight()->setLeft(right, newExpression->getRight());
963
964 replace(expression, newExpression);
965
966 return true;
967 }
968 return false;
969}
970
971bool EquivLaws::bidirectionalImplication2Reversed(std::shared_ptr<Expression> &expression)
972{
973 // !p <-> !q = p <-> q
974 if (expression->getValue() == IFF && expression->getLeft()->getValue() == NOT && expression->getRight()->getValue() == NOT)
975 {
976 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
977 std::shared_ptr<Expression> right = expression->getRight()->getLeft();
978
979 // create a new expression
980 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IFF);
981 newExpression->setLeft(left, newExpression);
982 newExpression->setRight(right, newExpression);
983
984 replace(expression, newExpression);
985
986 return true;
987 }
988 return false;
989}
990
991bool EquivLaws::bidirectionalImplication3(std::shared_ptr<Expression> &expression)
992{
993 // p <-> q = (p & q) | (!p & !q)
994 if (expression->getValue() == IFF)
995 {
996 std::shared_ptr<Expression> left = expression->getLeft();
997 std::shared_ptr<Expression> right = expression->getRight();
998
999 // create a new expression
1000 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(OR);
1001 newExpression->setLeft(std::make_shared<Expression>(AND), newExpression);
1002 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
1003 newExpression->getLeft()->setRight(right, newExpression->getLeft());
1004 newExpression->setRight(std::make_shared<Expression>(AND), newExpression);
1005 newExpression->getRight()->setLeft(std::make_shared<Expression>(NOT), newExpression->getRight());
1006 newExpression->getRight()->getLeft()->setLeft(left, newExpression->getRight()->getLeft());
1007 newExpression->getRight()->setRight(std::make_shared<Expression>(NOT), newExpression->getRight());
1008 newExpression->getRight()->getRight()->setLeft(right, newExpression->getRight()->getRight());
1009
1010 replace(expression, newExpression);
1011
1012 return true;
1013 }
1014 return false;
1015}
1016
1017bool EquivLaws::bidirectionalImplication3Reversed(std::shared_ptr<Expression> &expression)
1018{
1019 // (p & q) | (!p & !q) = p <-> q
1020 if (expression->getValue() == OR && expression->getLeft()->getValue() == AND && expression->getRight()->getValue() == AND)
1021 {
1022 std::shared_ptr<Expression> left1 = expression->getLeft()->getLeft();
1023 std::shared_ptr<Expression> left2 = expression->getLeft()->getRight();
1024 std::shared_ptr<Expression> right1 = expression->getRight()->getLeft()->getLeft();
1025 std::shared_ptr<Expression> right2 = expression->getRight()->getRight()->getLeft();
1026
1027 // create a new expression
1028 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IFF);
1029 newExpression->setLeft(left1, newExpression);
1030 newExpression->setRight(left2, newExpression);
1031
1032 replace(expression, newExpression);
1033
1034 return true;
1035 }
1036 return false;
1037}
1038
1039bool EquivLaws::bidirectionalImplication4(std::shared_ptr<Expression> &expression)
1040{
1041 // !(p <-> q) = p <-> !q
1042 if (expression->getValue() == NOT && expression->getLeft()->getValue() == IFF)
1043 {
1044 std::shared_ptr<Expression> left = expression->getLeft()->getLeft();
1045 std::shared_ptr<Expression> right = expression->getLeft()->getRight();
1046
1047 // create a new expression
1048 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(IFF);
1049 newExpression->setLeft(left, newExpression);
1050 newExpression->setRight(std::make_shared<Expression>(NOT), newExpression);
1051 newExpression->getRight()->setLeft(right, newExpression->getRight());
1052
1053 replace(expression, newExpression);
1054
1055 return true;
1056 }
1057 return false;
1058}
1059
1060bool EquivLaws::bidirectionalImplication4Reversed(std::shared_ptr<Expression> &expression)
1061{
1062 // p <-> !q = !(p <-> q)
1063 if (expression->getValue() == IFF && expression->getRight()->getValue() == NOT)
1064 {
1065 std::shared_ptr<Expression> left = expression->getLeft();
1066 std::shared_ptr<Expression> right = expression->getRight()->getLeft();
1067
1068 // create a new expression
1069 std::shared_ptr<Expression> newExpression = std::make_shared<Expression>(NOT);
1070 newExpression->setLeft(std::make_shared<Expression>(IFF), newExpression);
1071 newExpression->getLeft()->setLeft(left, newExpression->getLeft());
1072 newExpression->getLeft()->setRight(right, newExpression->getLeft());
1073
1074 replace(expression, newExpression);
1075
1076 return true;
1077 }
1078 return false;
1079}
EquivLaws::implications
static std::unordered_map< EquivLaw, std::string > implications
Map of implication equivalences to their string representations.
Definition equivLaws.h:24
EquivLaws::implication6
static bool implication6(std::shared_ptr< Expression > &expression)
Applies implication: (p -> q) & (q -> r) = (p | q) -> r.
Definition equivLaws.cpp:720
EquivLaws::bidirectionalImplication0
static bool bidirectionalImplication0(std::shared_ptr< Expression > &expression)
Applies bidirectional implication: p <-> q = (p -> q) & (q -> p)
Definition equivLaws.cpp:879
EquivLaws::implication2Reversed
static bool implication2Reversed(std::shared_ptr< Expression > &expression)
Applies implication2() but reversed !p -> q = p | q.
Definition equivLaws.cpp:563
EquivLaws::implication3Reversed
static bool implication3Reversed(std::shared_ptr< Expression > &expression)
Applies implication3() but reversed !(p -> !q) = p & q.
Definition equivLaws.cpp:605
EquivLaws::bidirectionalImplication3
static bool bidirectionalImplication3(std::shared_ptr< Expression > &expression)
Applies bidirectional implication: p <-> q = (p & q) | (!p & !q)
Definition equivLaws.cpp:991
EquivLaws::laws
static std::unordered_map< EquivLaw, std::string > laws
Map of equivalence laws to their string representations.
Definition equivLaws.h:8
EquivLaws::bidirectionalImplication2Reversed
static bool bidirectionalImplication2Reversed(std::shared_ptr< Expression > &expression)
Applies bidirectionalImplication2() but reversed !p <-> !q = p <-> q.
Definition equivLaws.cpp:971
EquivLaws::implication8Reversed
static bool implication8Reversed(std::shared_ptr< Expression > &expression)
Applies implication8() but reversed (p & q) -> r = (p -> q) | (q -> r)
Definition equivLaws.cpp:854
EquivLaws::distributive
static bool distributive(std::shared_ptr< Expression > &expression)
Applies distributive law p | (q & r) = (p | q) & (p | r), p & (q | r) = (p & q) | (p & r)
Definition equivLaws.cpp:237
EquivLaws::implication7
static bool implication7(std::shared_ptr< Expression > &expression)
Applies implication: (p -> q) | (p -> r) = p -> (q | r)
Definition equivLaws.cpp:773
EquivLaws::commutative
static bool commutative(std::shared_ptr< Expression > &expression)
Applies the commutative law (p | q) = (q | p), (p & q) = (q & p)
Definition equivLaws.cpp:169
EquivLaws::domination
static bool domination(std::shared_ptr< Expression > &expression)
Applies the domination law (p | T) = T, (p & F) = F.
Definition equivLaws.cpp:103
EquivLaws::replace
static void replace(std::shared_ptr< Expression > &expression, std::shared_ptr< Expression > newExpression)
Replace the current expression with the new expression.
Definition equivLaws.cpp:58
EquivLaws::associative
static bool associative(std::shared_ptr< Expression > &expression)
Applies the associative law (p | q) | r = p | (q | r), (p & q) & r = p & (q & r)
Definition equivLaws.cpp:190
EquivLaws::implication0Reversed
static bool implication0Reversed(std::shared_ptr< Expression > &expression)
Applies implication0() but reversed !p | q = p -> q.
Definition equivLaws.cpp:480
EquivLaws::implication0
static bool implication0(std::shared_ptr< Expression > &expression)
Applies implication: p -> q = !p | q.
Definition equivLaws.cpp:459
EquivLaws::implication5
static bool implication5(std::shared_ptr< Expression > &expression)
Applies implication: (p -> q) & (p -> r) = p -> (q & r)
Definition equivLaws.cpp:667
EquivLaws::implication6Reversed
static bool implication6Reversed(std::shared_ptr< Expression > &expression)
Applies implication6() but reversed (p | q) -> r = (p -> q) & (q -> r)
Definition equivLaws.cpp:748
EquivLaws::absorption
static bool absorption(std::shared_ptr< Expression > &expression)
Applies the absorption law p | (p & q) = p, p & (p | q) = p.
Definition equivLaws.cpp:408
EquivLaws::idempotent
static bool idempotent(std::shared_ptr< Expression > &expression)
Applies the idempotent law (p | p) = p, (p & p) = p.
Definition equivLaws.cpp:129
EquivLaws::distributiveReversed
static bool distributiveReversed(std::shared_ptr< Expression > &expression)
Applies distributive() but reversed (p | q) & (p | r) = p | (q & r), (p & q) | (p & r) = p & (q | r)
Definition equivLaws.cpp:281
EquivLaws::implication1
static bool implication1(std::shared_ptr< Expression > &expression)
Applies implication: p -> q = !q -> !p.
Definition equivLaws.cpp:500
EquivLaws::implication3
static bool implication3(std::shared_ptr< Expression > &expression)
Applies implication: p & q = !(p -> !q)
Definition equivLaws.cpp:583
EquivLaws::bidirectionalImplication2
static bool bidirectionalImplication2(std::shared_ptr< Expression > &expression)
Applies bidirectional implication: p <-> q = !p <-> !q.
Definition equivLaws.cpp:949
EquivLaws::implication7Reversed
static bool implication7Reversed(std::shared_ptr< Expression > &expression)
Applies implication7() but reversed p -> (q | r) = (p -> q) | (p -> r)
Definition equivLaws.cpp:801
EquivLaws::implication2
static bool implication2(std::shared_ptr< Expression > &expression)
Applies implication: p | q = !p -> q.
Definition equivLaws.cpp:542
EquivLaws::bidirectionalImplications
static std::unordered_map< EquivLaw, std::string > bidirectionalImplications
Map of biimplication equivalences to their string representations.
Definition equivLaws.h:46
EquivLaws::identity
static bool identity(std::shared_ptr< Expression > &expression)
Applies the identity law (p & T) = p, (p | F) = p.
Definition equivLaws.cpp:80
EquivLaws::implication1Reversed
static bool implication1Reversed(std::shared_ptr< Expression > &expression)
Applies implication1() but reversed !q -> !p = p -> q.
Definition equivLaws.cpp:522
EquivLaws::deMorganReversed
static bool deMorganReversed(std::shared_ptr< Expression > &expression)
Applies deMorgan() but reversed !p & !q = !(p | q), !p | !q = !(p & q)
Definition equivLaws.cpp:372
EquivLaws::implication5Reversed
static bool implication5Reversed(std::shared_ptr< Expression > &expression)
Applies implication5() but reversed p -> (q & r) = (p -> q) & (p -> r)
Definition equivLaws.cpp:695
EquivLaws::associativeReversed
static bool associativeReversed(std::shared_ptr< Expression > &expression)
Applies associative() but reversed p | (q | r) = (p | q) | r, p & (q & r) = (p & q) & r.
Definition equivLaws.cpp:214
EquivLaws::implication4Reversed
static bool implication4Reversed(std::shared_ptr< Expression > &expression)
Applies implication4() but reversed p & !q = !(p -> q)
Definition equivLaws.cpp:646
EquivLaws::implication4
static bool implication4(std::shared_ptr< Expression > &expression)
Applies implication: !(p -> q) = p & !q.
Definition equivLaws.cpp:625
EquivLaws::bidirectionalImplication1
static bool bidirectionalImplication1(std::shared_ptr< Expression > &expression)
Applies bidirectional implication: p <-> q = q <-> p.
Definition equivLaws.cpp:929
EquivLaws::bidirectionalImplication4Reversed
static bool bidirectionalImplication4Reversed(std::shared_ptr< Expression > &expression)
Applies bidirectionalImplication4() but reversed p <-> !q = !(p <-> q)
Definition equivLaws.cpp:1060
EquivLaws::deMorgan
static bool deMorgan(std::shared_ptr< Expression > &expression)
Applies De Morgan's law !(p | q) = !p & !q, !(p & q) = !p | !q.
Definition equivLaws.cpp:331
EquivLaws::implication8
static bool implication8(std::shared_ptr< Expression > &expression)
Applies implication: (p -> q) | (q -> r) = (p & q) -> r.
Definition equivLaws.cpp:826
EquivLaws::negation
static bool negation(std::shared_ptr< Expression > &expression)
Applies the negation law p | !p = T, p & !p = F.
Definition equivLaws.cpp:429
EquivLaws::bidirectionalImplication3Reversed
static bool bidirectionalImplication3Reversed(std::shared_ptr< Expression > &expression)
Applies bidirectionalImplication3() but reversed (p & q) | (!p & !q) = p <-> q.
Definition equivLaws.cpp:1017
EquivLaws::bidirectionalImplication0Reversed
static bool bidirectionalImplication0Reversed(std::shared_ptr< Expression > &expression)
Applies bidirectionalImplication0() but reversed (p -> q) & (q -> p) = p <-> q.
Definition equivLaws.cpp:903
EquivLaws::bidirectionalImplication4
static bool bidirectionalImplication4(std::shared_ptr< Expression > &expression)
Applies bidirectional implication: !(p <-> q) = p <-> !q.
Definition equivLaws.cpp:1039
EquivLaws::doubleNegation
static bool doubleNegation(std::shared_ptr< Expression > &expression)
Applies the double negation law !!p = p.
Definition equivLaws.cpp:151
IMPLIES
#define IMPLIES
Definition expression.h:25
IFF
#define IFF
Definition expression.h:26
OR
#define OR
Definition expression.h:22
TRUE
#define TRUE
Definition expression.h:29
FALSE
#define FALSE
Definition expression.h:30
AND
#define AND
Definition expression.h:21
NOT
#define NOT
Definition expression.h:23
Generated by doxygen 1.9.8