1""" 2Boolean algebra module for Diofant. 3""" 4 5from collections import defaultdict 6from itertools import combinations, product 7 8from ..core import Atom, cacheit 9from ..core.expr import Expr 10from ..core.function import Application 11from ..core.numbers import Number 12from ..core.operations import LatticeOp 13from ..core.singleton import S 14from ..core.singleton import SingletonWithManagedProperties as Singleton 15from ..core.sympify import converter, sympify 16from ..utilities import ordered 17 18 19class Boolean(Expr): 20 """A boolean object is an object for which logic operations make sense.""" 21 22 def __and__(self, other): 23 """Overloading for & operator.""" 24 return And(self, other) 25 26 __rand__ = __and__ 27 28 def __or__(self, other): 29 """Overloading for | operator.""" 30 return Or(self, other) 31 32 __ror__ = __or__ 33 34 def __invert__(self): 35 """Overloading for ~ operator.""" 36 return Not(self) 37 38 def __rshift__(self, other): 39 """Overloading for >> operator.""" 40 return Implies(self, other) 41 42 def __lshift__(self, other): 43 """Overloading for << operator.""" 44 return Implies(other, self) 45 46 __rrshift__ = __lshift__ 47 __rlshift__ = __rshift__ 48 49 def __xor__(self, other): 50 return Xor(self, other) 51 52 __rxor__ = __xor__ 53 54 def equals(self, other, failing_expression=False): 55 """ 56 Returns True if the given formulas have the same truth table. 57 For two formulas to be equal they must have the same literals. 58 59 Examples 60 ======== 61 62 >>> (a >> b).equals(~b >> ~a) 63 True 64 >>> Not(And(a, b, c)).equals(And(Not(a), Not(b), Not(c))) 65 False 66 >>> Not(And(a, Not(a))).equals(Or(b, Not(b))) 67 False 68 69 """ 70 from ..core.relational import Relational 71 from .inference import satisfiable 72 73 other = sympify(other) 74 75 if self.has(Relational) or other.has(Relational): 76 raise NotImplementedError('handling of relationals') 77 return self.atoms() == other.atoms() and \ 78 not satisfiable(Not(Equivalent(self, other))) 79 80 81class BooleanAtom(Atom, Boolean): 82 """Base class of BooleanTrue and BooleanFalse.""" 83 84 is_Boolean = True 85 86 @property 87 def canonical(self): 88 return self 89 90 def __int__(self): 91 return int(bool(self)) 92 93 94class BooleanTrue(BooleanAtom, metaclass=Singleton): 95 """Diofant version of True, a singleton that can be accessed via ``true``. 96 97 This is the Diofant version of True, for use in the logic module. The 98 primary advantage of using true instead of True is that shorthand boolean 99 operations like ~ and >> will work as expected on this class, whereas with 100 True they act bitwise on 1. Functions in the logic module will return this 101 class when they evaluate to true. 102 103 Notes 104 ===== 105 106 There is liable to be some confusion as to when ``True`` should 107 be used and when ``true`` should be used in various contexts 108 throughout Diofant. An important thing to remember is that 109 ``sympify(True)`` returns ``true``. This means that for the most 110 part, you can just use ``True`` and it will automatically be converted 111 to ``true`` when necessary, similar to how you can generally use 1 112 instead of ``Integer(1)``. 113 114 The rule of thumb is: 115 116 "If the boolean in question can be replaced by an arbitrary symbolic 117 ``Boolean``, like ``Or(x, y)`` or ``x > 1``, use ``true``. 118 Otherwise, use ``True``". 119 120 In other words, use ``true`` only on those contexts where the 121 boolean is being used as a symbolic representation of truth. 122 For example, if the object ends up in the ``.args`` of any expression, 123 then it must necessarily be ``true`` instead of ``True``, as 124 elements of ``.args`` must be ``Basic``. On the other hand, 125 ``==`` is not a symbolic operation in Diofant, since it always returns 126 ``True`` or ``False``, and does so in terms of structural equality 127 rather than mathematical, so it should return ``True``. The assumptions 128 system should use ``True`` and ``False``. Aside from not satisfying 129 the above rule of thumb, the 130 assumptions system uses a three-valued logic (``True``, ``False``, ``None``), 131 whereas ``true`` and ``false`` represent a two-valued logic. When in 132 doubt, use ``True``. 133 134 "``true == True is True``." 135 136 While "``true is True``" is ``False``, "``true == True``" 137 is ``True``, so if there is any doubt over whether a function or 138 expression will return ``true`` or ``True``, just use ``==`` 139 instead of ``is`` to do the comparison, and it will work in either 140 case. Finally, for boolean flags, it's better to just use ``if x`` 141 instead of ``if x is True``. To quote PEP 8: 142 143 Don't compare boolean values to ``True`` or ``False`` 144 using ``==``. 145 146 * Yes: ``if greeting:`` 147 * No: ``if greeting == True:`` 148 * Worse: ``if greeting is True:`` 149 150 Examples 151 ======== 152 153 >>> sympify(True) 154 true 155 >>> ~true 156 false 157 >>> ~True 158 -2 159 >>> Or(True, False) 160 true 161 162 See Also 163 ======== 164 165 BooleanFalse 166 167 """ 168 169 def __bool__(self): 170 return True 171 172 def __hash__(self): 173 return hash(True) 174 175 def as_set(self): 176 """ 177 Rewrite logic operators and relationals in terms of real sets. 178 179 Examples 180 ======== 181 182 >>> true.as_set() 183 UniversalSet() 184 185 """ 186 return S.UniversalSet 187 188 189class BooleanFalse(BooleanAtom, metaclass=Singleton): 190 """Diofant version of False, a singleton that can be accessed via ``false``. 191 192 This is the Diofant version of False, for use in the logic module. The 193 primary advantage of using false instead of False is that shorthand boolean 194 operations like ~ and >> will work as expected on this class, whereas with 195 False they act bitwise on 0. Functions in the logic module will return this 196 class when they evaluate to false. 197 198 Notes 199 ===== 200 201 See note in :py:class:`~diofant.logic.boolalg.BooleanTrue`. 202 203 Examples 204 ======== 205 206 >>> sympify(False) 207 false 208 >>> false >> false 209 true 210 >>> False >> False 211 0 212 >>> Or(True, False) 213 true 214 215 See Also 216 ======== 217 218 BooleanTrue 219 220 """ 221 222 def __bool__(self): 223 return False 224 225 def __hash__(self): 226 return hash(False) 227 228 def as_set(self): 229 """ 230 Rewrite logic operators and relationals in terms of real sets. 231 232 Examples 233 ======== 234 235 >>> false.as_set() 236 EmptySet() 237 238 """ 239 from ..sets import EmptySet 240 return EmptySet() 241 242 243true = BooleanTrue() 244false: BooleanFalse = BooleanFalse() 245# We want S.true and S.false to work, rather than S.BooleanTrue and 246# S.BooleanFalse, but making the class and instance names the same causes some 247# major issues (like the inability to import the class directly from this 248# file). 249S.true = true 250S.false = false 251 252converter[bool] = lambda x: true if x else false 253 254 255class BooleanFunction(Application, Boolean): 256 """Boolean function is a function that lives in a boolean space. 257 258 This is used as base class for And, Or, Not, etc. 259 260 """ 261 262 is_Boolean = True 263 264 def _eval_simplify(self, ratio, measure): 265 return simplify_logic(self) 266 267 def to_nnf(self, simplify=True): 268 return self._to_nnf(*self.args, simplify=simplify) 269 270 @classmethod 271 def _to_nnf(cls, *args, **kwargs): 272 simplify = kwargs.get('simplify', True) 273 argset = set() 274 for arg in args: 275 if not is_literal(arg): 276 arg = arg.to_nnf(simplify) 277 if simplify: 278 if isinstance(arg, cls): 279 arg = arg.args 280 else: 281 arg = arg, 282 for a in arg: 283 if Not(a) in argset: 284 return cls.zero 285 argset.add(a) 286 else: 287 argset.add(arg) 288 return cls(*argset) 289 290 291class And(LatticeOp, BooleanFunction): 292 """ 293 Logical AND function. 294 295 It evaluates its arguments in order, giving False immediately 296 if any of them are False, and True if they are all True. 297 298 Examples 299 ======== 300 301 >>> x & y 302 x & y 303 304 Notes 305 ===== 306 307 The ``&`` operator is provided as a convenience, but note that its use 308 here is different from its normal use in Python, which is bitwise 309 and. Hence, ``And(a, b)`` and ``a & b`` will return different things if 310 ``a`` and ``b`` are integers. 311 312 >>> And(x, y).subs({x: 1}) 313 y 314 315 """ 316 317 zero = false 318 identity = true 319 320 nargs = None 321 322 @classmethod 323 def _new_args_filter(cls, args): 324 newargs = [] 325 rel = [] 326 for x in reversed(list(args)): 327 if isinstance(x, Number) or x in (0, 1): 328 newargs.append(True if x else False) 329 continue 330 if x.is_Relational: 331 c = x.canonical 332 if c in rel: 333 continue 334 nc = (~c).canonical 335 if any(r == nc for r in rel): 336 return [false] 337 rel.append(c) 338 newargs.append(x) 339 return LatticeOp._new_args_filter(newargs, And) 340 341 def as_set(self): 342 """ 343 Rewrite logic operators and relationals in terms of real sets. 344 345 Examples 346 ======== 347 348 >>> And(x < 2, x > -2).as_set() 349 (-2, 2) 350 351 """ 352 from ..sets import Intersection 353 if len(self.free_symbols) == 1: 354 return Intersection(*[arg.as_set() for arg in self.args]) 355 else: 356 raise NotImplementedError('Sorry, And.as_set has not yet been' 357 ' implemented for multivariate' 358 ' expressions') 359 360 361class Or(LatticeOp, BooleanFunction): 362 """ 363 Logical OR function 364 365 It evaluates its arguments in order, giving True immediately 366 if any of them are True, and False if they are all False. 367 368 Examples 369 ======== 370 371 >>> x | y 372 x | y 373 374 Notes 375 ===== 376 377 The ``|`` operator is provided as a convenience, but note that its use 378 here is different from its normal use in Python, which is bitwise 379 or. Hence, ``Or(a, b)`` and ``a | b`` will return different things if 380 ``a`` and ``b`` are integers. 381 382 >>> Or(x, y).subs({x: 0}) 383 y 384 385 """ 386 387 zero = true 388 identity = false 389 390 @classmethod 391 def _new_args_filter(cls, args): 392 newargs = [] 393 rel = [] 394 for x in args: 395 if isinstance(x, Number) or x in (0, 1): 396 newargs.append(True if x else False) 397 continue 398 if x.is_Relational: 399 c = x.canonical 400 if c in rel: 401 continue 402 nc = (~c).canonical 403 if any(r == nc for r in rel): 404 return [true] 405 rel.append(c) 406 newargs.append(x) 407 return LatticeOp._new_args_filter(newargs, Or) 408 409 def as_set(self): 410 """ 411 Rewrite logic operators and relationals in terms of real sets. 412 413 Examples 414 ======== 415 416 >>> Or(x > 2, x < -2).as_set() 417 [-oo, -2) U (2, oo] 418 419 """ 420 from ..sets import Union 421 if len(self.free_symbols) == 1: 422 return Union(*[arg.as_set() for arg in self.args]) 423 else: 424 raise NotImplementedError('Sorry, Or.as_set has not yet been' 425 ' implemented for multivariate' 426 ' expressions') 427 428 429class Not(BooleanFunction): 430 """ 431 Logical Not function (negation). 432 433 Returns True if the statement is False. 434 Returns False if the statement is True. 435 436 Examples 437 ======== 438 439 >>> Not(True) 440 false 441 >>> Not(False) 442 true 443 >>> Not(And(True, False)) 444 true 445 >>> Not(Or(True, False)) 446 false 447 >>> Not(And(And(True, x), Or(x, False))) 448 ~x 449 >>> ~x 450 ~x 451 >>> Not(And(Or(x, y), Or(~x, ~y))) 452 ~((x | y) & (~x | ~y)) 453 454 Notes 455 ===== 456 457 The ``~`` operator is provided as a convenience, but note that its use 458 here is different from its normal use in Python, which is bitwise 459 not. In particular, ``~a`` and ``Not(a)`` will be different if ``a`` is 460 an integer. Furthermore, since bools in Python subclass from ``int``, 461 ``~True`` is the same as ``~1`` which is ``-2``, which has a boolean 462 value of True. To avoid this issue, use the Diofant boolean types 463 ``true`` and ``false``. 464 465 >>> ~True 466 -2 467 >>> ~true 468 false 469 470 """ 471 472 is_Not = True 473 474 @classmethod 475 def eval(cls, arg): 476 from ..core import (Equality, GreaterThan, LessThan, StrictGreaterThan, 477 StrictLessThan, Unequality) 478 if isinstance(arg, Number) or arg in (True, False): 479 return false if arg else true 480 if arg.is_Not: 481 return arg.args[0] 482 # Simplify Relational objects. 483 if isinstance(arg, Equality): 484 return Unequality(*arg.args) 485 if isinstance(arg, Unequality): 486 return Equality(*arg.args) 487 if isinstance(arg, StrictLessThan): 488 return GreaterThan(*arg.args) 489 if isinstance(arg, StrictGreaterThan): 490 return LessThan(*arg.args) 491 if isinstance(arg, LessThan): 492 return StrictGreaterThan(*arg.args) 493 if isinstance(arg, GreaterThan): 494 return StrictLessThan(*arg.args) 495 496 def as_set(self): 497 """ 498 Rewrite logic operators and relationals in terms of real sets. 499 500 Examples 501 ======== 502 503 >>> Not(x > 0, evaluate=False).as_set() 504 (-oo, 0] 505 506 """ 507 if len(self.free_symbols) == 1: 508 return self.args[0].as_set().complement(S.Reals) 509 else: 510 raise NotImplementedError('Sorry, Not.as_set has not yet been' 511 ' implemented for mutivariate' 512 ' expressions') 513 514 def to_nnf(self, simplify=True): 515 if is_literal(self): 516 return self 517 518 expr = self.args[0] 519 520 func, args = expr.func, expr.args 521 522 if func == And: 523 return Or._to_nnf(*[~arg for arg in args], simplify=simplify) 524 525 if func == Or: 526 return And._to_nnf(*[~arg for arg in args], simplify=simplify) 527 528 if func == Implies: 529 a, b = args 530 return And._to_nnf(a, ~b, simplify=simplify) 531 532 if func == Equivalent: 533 return And._to_nnf(Or(*args), Or(*[~arg for arg in args]), simplify=simplify) 534 535 if func == Xor: 536 result = [] 537 for i in range(1, len(args)+1, 2): 538 for neg in combinations(args, i): 539 clause = [~s if s in neg else s for s in args] 540 result.append(Or(*clause)) 541 return And._to_nnf(*result, simplify=simplify) 542 543 if func == ITE: 544 a, b, c = args 545 return And._to_nnf(Or(a, ~c), Or(~a, ~b), simplify=simplify) 546 547 raise ValueError(f'Illegal operator {func} in expression') 548 549 550class Xor(BooleanFunction): 551 """ 552 Logical XOR (exclusive OR) function. 553 554 Returns True if an odd number of the arguments are True and the rest are 555 False. 556 557 Returns False if an even number of the arguments are True and the rest are 558 False. 559 560 Examples 561 ======== 562 563 >>> Xor(True, False) 564 true 565 >>> Xor(True, True) 566 false 567 >>> Xor(True, False, True, True, False) 568 true 569 >>> Xor(True, False, True, False) 570 false 571 >>> x ^ y 572 Xor(x, y) 573 574 Notes 575 ===== 576 577 The ``^`` operator is provided as a convenience, but note that its use 578 here is different from its normal use in Python, which is bitwise xor. In 579 particular, ``a ^ b`` and ``Xor(a, b)`` will be different if ``a`` and 580 ``b`` are integers. 581 582 >>> Xor(x, y).subs({y: 0}) 583 x 584 585 """ 586 587 def __new__(cls, *args, **kwargs): 588 argset = set() 589 obj = super().__new__(cls, *args, **kwargs) 590 for arg in super(Xor, obj).args: 591 if isinstance(arg, Number) or arg in (True, False): 592 if not arg: 593 continue 594 else: 595 arg = true 596 if isinstance(arg, Xor): 597 for a in arg.args: 598 argset.remove(a) if a in argset else argset.add(a) 599 elif arg in argset: 600 argset.remove(arg) 601 else: 602 argset.add(arg) 603 rel = [(r, r.canonical, (~r).canonical) for r in argset if r.is_Relational] 604 odd = False # is number of complimentary pairs odd? start 0 -> False 605 remove = [] 606 for i, (r, c, nc) in enumerate(rel): 607 for j in range(i + 1, len(rel)): 608 rj, cj = rel[j][:2] 609 if cj == nc: 610 odd = ~odd 611 break 612 elif cj == c: 613 break 614 else: 615 continue 616 remove.append((r, rj)) 617 if odd: 618 argset.remove(true) if true in argset else argset.add(true) 619 for a, b in remove: 620 argset.remove(a) 621 argset.remove(b) 622 if len(argset) == 0: 623 return false 624 elif len(argset) == 1: 625 return argset.pop() 626 elif True in argset: 627 argset.remove(True) 628 return Not(Xor(*argset)) 629 else: 630 obj._args = tuple(ordered(argset)) 631 obj._argset = frozenset(argset) 632 return obj 633 634 @property # type: ignore[misc] 635 @cacheit 636 def args(self): 637 return tuple(ordered(self._argset)) 638 639 def to_nnf(self, simplify=True): 640 args = [] 641 for i in range(0, len(self.args)+1, 2): 642 for neg in combinations(self.args, i): 643 clause = [~s if s in neg else s for s in self.args] 644 args.append(Or(*clause)) 645 return And._to_nnf(*args, simplify=simplify) 646 647 648class Nand(BooleanFunction): 649 """ 650 Logical NAND function. 651 652 It evaluates its arguments in order, giving True immediately if any 653 of them are False, and False if they are all True. 654 655 Returns True if any of the arguments are False. 656 Returns False if all arguments are True. 657 658 Examples 659 ======== 660 661 >>> Nand(False, True) 662 true 663 >>> Nand(True, True) 664 false 665 >>> Nand(x, y) 666 ~(x & y) 667 668 """ 669 670 @classmethod 671 def eval(cls, *args): 672 return Not(And(*args)) 673 674 675class Nor(BooleanFunction): 676 """ 677 Logical NOR function. 678 679 It evaluates its arguments in order, giving False immediately if any 680 of them are True, and True if they are all False. 681 682 Returns False if any argument is True. 683 Returns True if all arguments are False. 684 685 Examples 686 ======== 687 688 >>> Nor(True, False) 689 false 690 >>> Nor(True, True) 691 false 692 >>> Nor(False, True) 693 false 694 >>> Nor(False, False) 695 true 696 >>> Nor(x, y) 697 ~(x | y) 698 699 """ 700 701 @classmethod 702 def eval(cls, *args): 703 return Not(Or(*args)) 704 705 706class Implies(BooleanFunction): 707 """ 708 Logical implication. 709 710 A implies B is equivalent to !A v B 711 712 Accepts two Boolean arguments; A and B. 713 Returns False if A is True and B is False. 714 Returns True otherwise. 715 716 Examples 717 ======== 718 719 >>> Implies(True, False) 720 false 721 >>> Implies(False, False) 722 true 723 >>> Implies(True, True) 724 true 725 >>> Implies(False, True) 726 true 727 >>> x >> y 728 Implies(x, y) 729 >>> y << x 730 Implies(x, y) 731 732 Notes 733 ===== 734 735 The ``>>`` and ``<<`` operators are provided as a convenience, but note 736 that their use here is different from their normal use in Python, which is 737 bit shifts. Hence, ``Implies(a, b)`` and ``a >> b`` will return different 738 things if ``a`` and ``b`` are integers. In particular, since Python 739 considers ``True`` and ``False`` to be integers, ``True >> True`` will be 740 the same as ``1 >> 1``, i.e., 0, which has a truth value of False. To 741 avoid this issue, use the Diofant objects ``true`` and ``false``. 742 743 >>> True >> False 744 1 745 >>> true >> false 746 false 747 748 """ 749 750 @classmethod 751 def eval(cls, *args): 752 try: 753 newargs = [] 754 for x in args: 755 if isinstance(x, Number) or x in (0, 1): 756 newargs.append(True if x else False) 757 else: 758 newargs.append(x) 759 A, B = newargs 760 except ValueError: 761 raise ValueError(f'{len(args)} operand(s) used for an Implies ' 762 f'(pairs are required): {args!s}') 763 if A == true or A == false or B == true or B == false: 764 return Or(Not(A), B) 765 elif A == B: 766 return true 767 elif A.is_Relational and B.is_Relational: 768 if A.canonical == B.canonical: 769 return true 770 elif (~A).canonical == B.canonical: 771 return B 772 else: 773 return Expr.__new__(cls, *args) 774 775 def to_nnf(self, simplify=True): 776 a, b = self.args 777 return Or._to_nnf(~a, b, simplify=simplify) 778 779 780class Equivalent(BooleanFunction): 781 """ 782 Equivalence relation. 783 784 Equivalent(A, B) is True iff A and B are both True or both False. 785 786 Returns True if all of the arguments are logically equivalent. 787 Returns False otherwise. 788 789 Examples 790 ======== 791 792 >>> Equivalent(False, False, False) 793 true 794 >>> Equivalent(True, False, False) 795 false 796 >>> Equivalent(x, And(x, True)) 797 true 798 799 """ 800 801 def __new__(cls, *args, **options): 802 from ..core.relational import Relational 803 args = [sympify(arg, strict=True) for arg in args] 804 805 argset = set(args) 806 for x in args: 807 if isinstance(x, Number) or x in [True, False]: # Includes 0, 1 808 argset.discard(x) 809 argset.add(True if x else False) 810 rel = [] 811 for r in argset: 812 if isinstance(r, Relational): 813 rel.append((r, r.canonical, (~r).canonical)) 814 remove = [] 815 for i, (r, c, nc) in enumerate(rel): 816 for j in range(i + 1, len(rel)): 817 rj, cj = rel[j][:2] 818 if cj == nc: 819 return false 820 elif cj == c: 821 remove.append((r, rj)) 822 break 823 for a, b in remove: 824 argset.remove(a) 825 argset.remove(b) 826 argset.add(True) 827 if len(argset) <= 1: 828 return true 829 if True in argset: 830 argset.discard(True) 831 return And(*argset) 832 if False in argset: 833 argset.discard(False) 834 return And(*[~arg for arg in argset]) 835 _args = frozenset(argset) 836 obj = super().__new__(cls, _args) 837 obj._argset = _args 838 return obj 839 840 @property # type: ignore[misc] 841 @cacheit 842 def args(self): 843 return tuple(ordered(self._argset)) 844 845 def to_nnf(self, simplify=True): 846 args = [] 847 for a, b in zip(self.args, self.args[1:]): 848 args.append(Or(~a, b)) 849 args.append(Or(~self.args[-1], self.args[0])) 850 return And._to_nnf(*args, simplify=simplify) 851 852 853class ITE(BooleanFunction): 854 """ 855 If then else clause. 856 857 ITE(A, B, C) evaluates and returns the result of B if A is true 858 else it returns the result of C. 859 860 Examples 861 ======== 862 863 >>> ITE(True, False, True) 864 false 865 >>> ITE(Or(True, False), And(True, True), Xor(True, True)) 866 true 867 >>> ITE(x, y, z) 868 ITE(x, y, z) 869 >>> ITE(True, x, y) 870 x 871 >>> ITE(False, x, y) 872 y 873 >>> ITE(x, y, y) 874 y 875 876 """ 877 878 @classmethod 879 def eval(cls, *args): 880 try: 881 a, b, c = args 882 except ValueError: 883 raise ValueError('ITE expects exactly 3 arguments') 884 if a == true: 885 return b 886 elif a == false: 887 return c 888 elif b == c: 889 return b 890 elif b == true and c == false: 891 return a 892 elif b == false and c == true: 893 return Not(a) 894 895 def to_nnf(self, simplify=True): 896 a, b, c = self.args 897 return And._to_nnf(Or(~a, b), Or(a, c), simplify=simplify) 898 899 def _eval_derivative(self, x): 900 return self.func(self.args[0], *[a.diff(x) for a in self.args[1:]]) 901 902 903# end class definitions. Some useful methods 904 905 906def conjuncts(expr): 907 """Return a list of the conjuncts in the expr s. 908 909 Examples 910 ======== 911 912 >>> conjuncts(a & b) == frozenset([a, b]) 913 True 914 >>> conjuncts(a | b) == frozenset([Or(a, b)]) 915 True 916 917 """ 918 return And.make_args(expr) 919 920 921def disjuncts(expr): 922 """Return a list of the disjuncts in the sentence s. 923 924 Examples 925 ======== 926 927 >>> disjuncts(a | b) == frozenset([a, b]) 928 True 929 >>> disjuncts(a & b) == frozenset([And(a, b)]) 930 True 931 932 """ 933 return Or.make_args(expr) 934 935 936def distribute_and_over_or(expr): 937 """ 938 Given a sentence s consisting of conjunctions and disjunctions 939 of literals, return an equivalent sentence in CNF. 940 941 Examples 942 ======== 943 944 >>> distribute_and_over_or(Or(a, And(Not(b), Not(c)))) 945 (a | ~b) & (a | ~c) 946 947 """ 948 return _distribute((expr, And, Or)) 949 950 951def distribute_or_over_and(expr): 952 """ 953 Given a sentence s consisting of conjunctions and disjunctions 954 of literals, return an equivalent sentence in DNF. 955 956 Note that the output is NOT simplified. 957 958 Examples 959 ======== 960 961 >>> distribute_or_over_and(And(Or(Not(a), b), c)) 962 (b & c) | (c & ~a) 963 964 """ 965 return _distribute((expr, Or, And)) 966 967 968def _distribute(info): 969 """Distributes info[1] over info[2] with respect to info[0].""" 970 if isinstance(info[0], info[2]): 971 for arg in info[0].args: 972 if isinstance(arg, info[1]): 973 conj = arg 974 break 975 else: 976 return info[0] 977 rest = info[2](*[a for a in info[0].args if a is not conj]) 978 return info[1](*list(map(_distribute, 979 ((info[2](c, rest), info[1], info[2]) for c in conj.args)))) 980 elif isinstance(info[0], info[1]): 981 return info[1](*list(map(_distribute, 982 ((x, info[1], info[2]) for x in info[0].args)))) 983 else: 984 return info[0] 985 986 987def to_nnf(expr, simplify=True): 988 """ 989 Converts expr to Negation Normal Form. 990 A logical expression is in Negation Normal Form (NNF) if it 991 contains only And, Or and Not, and Not is applied only to literals. 992 If simplify is True, the result contains no redundant clauses. 993 994 Examples 995 ======== 996 997 >>> to_nnf(Not((~a & ~b) | (c & d))) 998 (a | b) & (~c | ~d) 999 >>> to_nnf(Equivalent(a >> b, b >> a)) 1000 (a | ~b | (a & ~b)) & (b | ~a | (b & ~a)) 1001 1002 """ 1003 expr = sympify(expr) 1004 if is_nnf(expr, simplify): 1005 return expr 1006 return expr.to_nnf(simplify) 1007 1008 1009def to_cnf(expr, simplify=False): 1010 """ 1011 Convert a propositional logical sentence s to conjunctive normal form. 1012 That is, of the form ((A | ~B | ...) & (B | C | ...) & ...). 1013 If simplify is True, the expr is evaluated to its simplest CNF form. 1014 1015 Examples 1016 ======== 1017 1018 >>> to_cnf(~(a | b) | c) 1019 (c | ~a) & (c | ~b) 1020 >>> to_cnf((a | b) & (a | ~a), True) 1021 a | b 1022 1023 """ 1024 expr = sympify(expr) 1025 if not isinstance(expr, BooleanFunction): 1026 return expr 1027 1028 if simplify: 1029 return simplify_logic(expr, 'cnf', True) 1030 1031 # Don't convert unless we have to 1032 if is_cnf(expr): 1033 return expr 1034 1035 expr = eliminate_implications(expr) 1036 return distribute_and_over_or(expr) 1037 1038 1039def to_dnf(expr, simplify=False): 1040 """ 1041 Convert a propositional logical sentence s to disjunctive normal form. 1042 That is, of the form ((A & ~B & ...) | (B & C & ...) | ...). 1043 If simplify is True, the expr is evaluated to its simplest DNF form. 1044 1045 Examples 1046 ======== 1047 1048 >>> to_dnf(b & (a | c)) 1049 (a & b) | (b & c) 1050 >>> to_dnf((a & b) | (a & ~b) | (b & c) | (~b & c), True) 1051 a | c 1052 1053 """ 1054 expr = sympify(expr) 1055 if not isinstance(expr, BooleanFunction): 1056 return expr 1057 1058 if simplify: 1059 return simplify_logic(expr, 'dnf', True) 1060 1061 # Don't convert unless we have to 1062 if is_dnf(expr): 1063 return expr 1064 1065 expr = eliminate_implications(expr) 1066 return distribute_or_over_and(expr) 1067 1068 1069def is_nnf(expr, simplified=True): 1070 """ 1071 Checks if expr is in Negation Normal Form. 1072 A logical expression is in Negation Normal Form (NNF) if it 1073 contains only And, Or and Not, and Not is applied only to literals. 1074 If simplified is True, checks if result contains no redundant clauses. 1075 1076 Examples 1077 ======== 1078 1079 >>> is_nnf(a & b | ~c) 1080 True 1081 >>> is_nnf((a | ~a) & (b | c)) 1082 False 1083 >>> is_nnf((a | ~a) & (b | c), False) 1084 True 1085 >>> is_nnf(Not(a & b) | c) 1086 False 1087 >>> is_nnf((a >> b) & (b >> a)) 1088 False 1089 1090 """ 1091 expr = sympify(expr) 1092 if is_literal(expr): 1093 return True 1094 1095 stack = [expr] 1096 1097 while stack: 1098 expr = stack.pop() 1099 if expr.func in (And, Or): 1100 if simplified: 1101 args = expr.args 1102 for arg in args: 1103 if Not(arg) in args: 1104 return False 1105 stack.extend(expr.args) 1106 1107 elif not is_literal(expr): 1108 return False 1109 1110 return True 1111 1112 1113def is_cnf(expr): 1114 """ 1115 Test whether or not an expression is in conjunctive normal form. 1116 1117 Examples 1118 ======== 1119 1120 >>> is_cnf(a | b | c) 1121 True 1122 >>> is_cnf(a & b & c) 1123 True 1124 >>> is_cnf((a & b) | c) 1125 False 1126 1127 """ 1128 return _is_form(expr, And, Or) 1129 1130 1131def is_dnf(expr): 1132 """ 1133 Test whether or not an expression is in disjunctive normal form. 1134 1135 Examples 1136 ======== 1137 1138 >>> is_dnf(a | b | c) 1139 True 1140 >>> is_dnf(a & b & c) 1141 True 1142 >>> is_dnf((a & b) | c) 1143 True 1144 >>> is_dnf(a & (b | c)) 1145 False 1146 1147 """ 1148 return _is_form(expr, Or, And) 1149 1150 1151def _is_form(expr, function1, function2): 1152 """Test whether or not an expression is of the required form.""" 1153 expr = sympify(expr) 1154 1155 # Special case of an Atom 1156 if expr.is_Atom: 1157 return True 1158 1159 # Special case of a single expression of function2 1160 if isinstance(expr, function2): 1161 for lit in expr.args: 1162 if isinstance(lit, Not): 1163 if not lit.args[0].is_Atom: 1164 return False 1165 else: 1166 if not lit.is_Atom: 1167 return False 1168 return True 1169 1170 # Special case of a single negation 1171 if isinstance(expr, Not): 1172 if not expr.args[0].is_Atom: 1173 return False 1174 1175 if not isinstance(expr, function1): 1176 return False 1177 1178 for cls in expr.args: 1179 if cls.is_Atom: 1180 continue 1181 if isinstance(cls, Not): 1182 if not cls.args[0].is_Atom: 1183 return False 1184 elif not isinstance(cls, function2): 1185 return False 1186 for lit in cls.args: 1187 if isinstance(lit, Not): 1188 if not lit.args[0].is_Atom: 1189 return False 1190 else: 1191 if not lit.is_Atom: 1192 return False 1193 1194 return True 1195 1196 1197def eliminate_implications(expr): 1198 """ 1199 Change >>, <<, and Equivalent into &, |, and ~. That is, return an 1200 expression that is equivalent to s, but has only &, |, and ~ as logical 1201 operators. 1202 1203 Examples 1204 ======== 1205 1206 >>> eliminate_implications(Implies(a, b)) 1207 b | ~a 1208 >>> eliminate_implications(Equivalent(a, b)) 1209 (a | ~b) & (b | ~a) 1210 >>> eliminate_implications(Equivalent(a, b, c)) 1211 (a | ~c) & (b | ~a) & (c | ~b) 1212 1213 """ 1214 return to_nnf(expr) 1215 1216 1217def is_literal(expr): 1218 """ 1219 Returns True if expr is a literal, else False. 1220 1221 Examples 1222 ======== 1223 1224 >>> is_literal(a) 1225 True 1226 >>> is_literal(~a) 1227 True 1228 >>> is_literal(a + b) 1229 True 1230 >>> is_literal(Or(a, b)) 1231 False 1232 1233 """ 1234 if isinstance(expr, Not): 1235 return not isinstance(expr.args[0], BooleanFunction) 1236 else: 1237 return not isinstance(expr, BooleanFunction) 1238 1239 1240def to_int_repr(clauses, symbols): 1241 """ 1242 Takes clauses in CNF format and puts them into an integer representation. 1243 1244 Examples 1245 ======== 1246 1247 >>> to_int_repr([x | y, y], [x, y]) 1248 [{1, 2}, {2}] 1249 1250 """ 1251 symbols = dict(zip(symbols, range(1, len(symbols) + 1))) 1252 1253 def append_symbol(arg, symbols): 1254 if isinstance(arg, Not): 1255 return -symbols[arg.args[0]] 1256 else: 1257 return symbols[arg] 1258 1259 return [{append_symbol(arg, symbols) for arg in Or.make_args(c)} 1260 for c in clauses] 1261 1262 1263def _check_pair(minterm1, minterm2): 1264 """ 1265 Checks if a pair of minterms differs by only one bit. If yes, returns 1266 index, else returns -1. 1267 1268 """ 1269 index = -1 1270 for x, (i, j) in enumerate(zip(minterm1, minterm2)): 1271 if i != j: 1272 if index == -1: 1273 index = x 1274 else: 1275 return -1 1276 return index 1277 1278 1279def _convert_to_varsSOP(minterm, variables): 1280 """ 1281 Converts a term in the expansion of a function from binary to it's 1282 variable form (for SOP). 1283 1284 """ 1285 temp = [] 1286 for i, m in enumerate(minterm): 1287 if m == 0: 1288 temp.append(Not(variables[i])) 1289 elif m == 1: 1290 temp.append(variables[i]) 1291 return And(*temp) 1292 1293 1294def _convert_to_varsPOS(maxterm, variables): 1295 """ 1296 Converts a term in the expansion of a function from binary to it's 1297 variable form (for POS). 1298 1299 """ 1300 temp = [] 1301 for i, m in enumerate(maxterm): 1302 if m == 1: 1303 temp.append(Not(variables[i])) 1304 elif m == 0: 1305 temp.append(variables[i]) 1306 return Or(*temp) 1307 1308 1309def _simplified_pairs(terms): 1310 """ 1311 Reduces a set of minterms, if possible, to a simplified set of minterms 1312 with one less variable in the terms using QM method. 1313 1314 """ 1315 simplified_terms = [] 1316 todo = list(range(len(terms))) 1317 for i, ti in enumerate(terms[:-1]): 1318 for j_i, tj in enumerate(terms[(i + 1):]): 1319 index = _check_pair(ti, tj) 1320 if index != -1: 1321 todo[i] = todo[j_i + i + 1] = None 1322 newterm = ti[:] 1323 newterm[index] = 3 1324 if newterm not in simplified_terms: 1325 simplified_terms.append(newterm) 1326 simplified_terms.extend( 1327 [terms[i] for i in [_ for _ in todo if _ is not None]]) 1328 return simplified_terms 1329 1330 1331def _compare_term(minterm, term): 1332 """ 1333 Return True if a binary term is satisfied by the given term. Used 1334 for recognizing prime implicants. 1335 1336 """ 1337 for i, x in enumerate(term): 1338 if x not in (3, minterm[i]): 1339 return False 1340 return True 1341 1342 1343def _rem_redundancy(l1, terms): 1344 """ 1345 After the truth table has been sufficiently simplified, use the prime 1346 implicant table method to recognize and eliminate redundant pairs, 1347 and return the essential arguments. 1348 1349 """ 1350 essential = [] 1351 for x in terms: 1352 temporary = [] 1353 for y in l1: 1354 if _compare_term(x, y): 1355 temporary.append(y) 1356 if len(temporary) == 1: 1357 if temporary[0] not in essential: 1358 essential.append(temporary[0]) 1359 for x in terms: 1360 for y in essential: 1361 if _compare_term(x, y): 1362 break 1363 else: 1364 for z in l1: # pragma: no branch 1365 if _compare_term(x, z): 1366 assert z not in essential 1367 essential.append(z) 1368 break 1369 1370 return essential 1371 1372 1373def SOPform(variables, minterms, dontcares=None): 1374 """ 1375 The SOPform function uses simplified_pairs and a redundant group- 1376 eliminating algorithm to convert the list of all input combos that 1377 generate '1' (the minterms) into the smallest Sum of Products form. 1378 1379 The variables must be given as the first argument. 1380 1381 Return a logical Or function (i.e., the "sum of products" or "SOP" 1382 form) that gives the desired outcome. If there are inputs that can 1383 be ignored, pass them as a list, too. 1384 1385 The result will be one of the (perhaps many) functions that satisfy 1386 the conditions. 1387 1388 Examples 1389 ======== 1390 1391 >>> minterms = [[0, 0, 0, 1], [0, 0, 1, 1], 1392 ... [0, 1, 1, 1], [1, 0, 1, 1], [1, 1, 1, 1]] 1393 >>> dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]] 1394 >>> SOPform([t, x, y, z], minterms, dontcares) 1395 (y & z) | (z & ~t) 1396 1397 References 1398 ========== 1399 1400 * https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm 1401 1402 """ 1403 variables = [sympify(v) for v in variables] 1404 if minterms == []: 1405 return false 1406 1407 minterms = [list(i) for i in minterms] 1408 dontcares = [list(i) for i in (dontcares or [])] 1409 for d in dontcares: 1410 if d in minterms: 1411 raise ValueError(f'{d} in minterms is also in dontcares') 1412 1413 old = None 1414 new = minterms + dontcares 1415 while new != old: 1416 old = new 1417 new = _simplified_pairs(old) 1418 essential = _rem_redundancy(new, minterms) 1419 return Or(*[_convert_to_varsSOP(x, variables) for x in essential]) 1420 1421 1422def POSform(variables, minterms, dontcares=None): 1423 """ 1424 The POSform function uses simplified_pairs and a redundant-group 1425 eliminating algorithm to convert the list of all input combinations 1426 that generate '1' (the minterms) into the smallest Product of Sums form. 1427 1428 The variables must be given as the first argument. 1429 1430 Return a logical And function (i.e., the "product of sums" or "POS" 1431 form) that gives the desired outcome. If there are inputs that can 1432 be ignored, pass them as a list, too. 1433 1434 The result will be one of the (perhaps many) functions that satisfy 1435 the conditions. 1436 1437 Examples 1438 ======== 1439 1440 >>> minterms = [[0, 0, 0, 1], [0, 0, 1, 1], [0, 1, 1, 1], 1441 ... [1, 0, 1, 1], [1, 1, 1, 1]] 1442 >>> dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]] 1443 >>> POSform([t, x, y, z], minterms, dontcares) 1444 z & (y | ~t) 1445 1446 References 1447 ========== 1448 1449 * https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm 1450 1451 """ 1452 variables = [sympify(v) for v in variables] 1453 if minterms == []: 1454 return false 1455 1456 minterms = [list(i) for i in minterms] 1457 dontcares = [list(i) for i in (dontcares or [])] 1458 for d in dontcares: 1459 if d in minterms: 1460 raise ValueError(f'{d} in minterms is also in dontcares') 1461 1462 maxterms = [] 1463 for t in product([0, 1], repeat=len(variables)): 1464 t = list(t) 1465 if (t not in minterms) and (t not in dontcares): 1466 maxterms.append(t) 1467 old = None 1468 new = maxterms + dontcares 1469 while new != old: 1470 old = new 1471 new = _simplified_pairs(old) 1472 essential = _rem_redundancy(new, maxterms) 1473 return And(*[_convert_to_varsPOS(x, variables) for x in essential]) 1474 1475 1476def _find_predicates(expr): 1477 """Helper to find logical predicates in BooleanFunctions. 1478 1479 A logical predicate is defined here as anything within a BooleanFunction 1480 that is not a BooleanFunction itself. 1481 1482 """ 1483 if not isinstance(expr, BooleanFunction): 1484 return {expr} 1485 return set().union(*(_find_predicates(i) for i in expr.args)) 1486 1487 1488def simplify_logic(expr, form=None, deep=True): 1489 """ 1490 This function simplifies a boolean function to its simplified version 1491 in SOP or POS form. The return type is an Or or And object in Diofant. 1492 1493 Parameters 1494 ========== 1495 1496 expr : string or boolean expression 1497 form : string ('cnf' or 'dnf') or None (default). 1498 If 'cnf' or 'dnf', the simplest expression in the corresponding 1499 normal form is returned; if None, the answer is returned 1500 according to the form with fewest args (in CNF by default). 1501 deep : boolean (default True) 1502 indicates whether to recursively simplify any 1503 non-boolean functions contained within the input. 1504 1505 Examples 1506 ======== 1507 1508 >>> b = (~x & ~y & ~z) | (~x & ~y & z) 1509 >>> simplify_logic(b) 1510 ~x & ~y 1511 1512 >>> sympify(b) 1513 (z & ~x & ~y) | (~x & ~y & ~z) 1514 >>> simplify_logic(_) 1515 ~x & ~y 1516 1517 """ 1518 if form == 'cnf' or form == 'dnf' or form is None: 1519 expr = sympify(expr) 1520 if not isinstance(expr, BooleanFunction): 1521 return expr 1522 variables = _find_predicates(expr) 1523 truthtable = [] 1524 for t in product([0, 1], repeat=len(variables)): 1525 t = list(t) 1526 if expr.xreplace(dict(zip(variables, t))): 1527 truthtable.append(t) 1528 if deep: 1529 from ..simplify import simplify 1530 variables = [simplify(v) for v in variables] 1531 if form == 'dnf' or \ 1532 (form is None and len(truthtable) >= (2 ** (len(variables) - 1))): 1533 return SOPform(variables, truthtable) 1534 elif form == 'cnf' or form is None: # pragma: no branch 1535 return POSform(variables, truthtable) 1536 else: 1537 raise ValueError('form can be cnf or dnf only') 1538 1539 1540def _finger(eq): 1541 """ 1542 Assign a 5-item fingerprint to each symbol in the equation: 1543 [ 1544 # of times it appeared as a Symbol, 1545 # of times it appeared as a Not(symbol), 1546 # of times it appeared as a Symbol in an And or Or, 1547 # of times it appeared as a Not(Symbol) in an And or Or, 1548 sum of the number of arguments with which it appeared, 1549 counting Symbol as 1 and Not(Symbol) as 2 1550 ] 1551 1552 >>> eq = Or(And(Not(y), a), And(Not(y), b), And(x, y)) 1553 >>> dict(_finger(eq)) 1554 {(0, 0, 1, 0, 2): [x], 1555 (0, 0, 1, 0, 3): [a, b], 1556 (0, 0, 1, 2, 8): [y]} 1557 1558 So y and x have unique fingerprints, but a and b do not. 1559 1560 """ 1561 f = eq.free_symbols 1562 d = {fi: [0] * 5 for fi in f} 1563 for a in eq.args: 1564 if a.is_Symbol: 1565 d[a][0] += 1 1566 elif a.is_Not: 1567 d[a.args[0]][1] += 1 1568 else: 1569 o = len(a.args) + sum(isinstance(ai, Not) for ai in a.args) 1570 for ai in a.args: 1571 if ai.is_Symbol: 1572 d[ai][2] += 1 1573 d[ai][-1] += o 1574 else: 1575 d[ai.args[0]][3] += 1 1576 d[ai.args[0]][-1] += o 1577 inv = defaultdict(list) 1578 for k, v in ordered(d.items()): 1579 inv[tuple(v)].append(k) 1580 return inv 1581 1582 1583def bool_map(bool1, bool2): 1584 """ 1585 Return the simplified version of bool1, and the mapping of variables 1586 that makes the two expressions bool1 and bool2 represent the same 1587 logical behaviour for some correspondence between the variables 1588 of each. 1589 If more than one mappings of this sort exist, one of them 1590 is returned. 1591 For example, And(x, y) is logically equivalent to And(a, b) for 1592 the mapping {x: a, y:b} or {x: b, y:a}. 1593 If no such mapping exists, return False. 1594 1595 Examples 1596 ======== 1597 1598 >>> function1 = SOPform([x, z, y], [[1, 0, 1], [0, 0, 1]]) 1599 >>> function2 = SOPform([a, b, c], [[1, 0, 1], [1, 0, 0]]) 1600 >>> bool_map(function1, function2) 1601 (y & ~z, {y: a, z: b}) 1602 1603 The results are not necessarily unique, but they are canonical. Here, 1604 ``(t, z)`` could be ``(a, d)`` or ``(d, a)``: 1605 1606 >>> eq1 = Or(And(Not(y), t), And(Not(y), z), And(x, y)) 1607 >>> eq2 = Or(And(Not(c), a), And(Not(c), d), And(b, c)) 1608 >>> bool_map(eq1, eq2) 1609 ((x & y) | (t & ~y) | (z & ~y), {t: a, x: b, y: c, z: d}) 1610 >>> eq = And(Xor(a, b), c, And(c, d)) 1611 >>> bool_map(eq, eq.subs({c: x})) 1612 (c & d & (a | b) & (~a | ~b), {a: a, b: b, c: d, d: x}) 1613 1614 """ 1615 1616 def match(function1, function2): 1617 """Return the mapping that equates variables between two 1618 simplified boolean expressions if possible. 1619 1620 By "simplified" we mean that a function has been denested 1621 and is either an And (or an Or) whose arguments are either 1622 symbols (x), negated symbols (Not(x)), or Or (or an And) whose 1623 arguments are only symbols or negated symbols. For example, 1624 And(x, Not(y), Or(w, Not(z))). 1625 1626 Basic.match is not robust enough (see issue sympy/sympy#4835) so this is 1627 a workaround that is valid for simplified boolean expressions. 1628 1629 """ 1630 # do some quick checks 1631 if function1.__class__ != function2.__class__: 1632 return 1633 if len(function1.args) != len(function2.args): 1634 return 1635 if function1.is_Symbol: 1636 return {function1: function2} 1637 1638 # get the fingerprint dictionaries 1639 f1 = _finger(function1) 1640 f2 = _finger(function2) 1641 1642 # more quick checks 1643 if len(f1) != len(f2): 1644 return 1645 1646 # assemble the match dictionary if possible 1647 matchdict = {} 1648 for k in f1: 1649 if k not in f2 or len(f1[k]) != len(f2[k]): 1650 return 1651 for i, x in enumerate(f1[k]): 1652 matchdict[x] = f2[k][i] 1653 return matchdict if matchdict else None 1654 1655 a = simplify_logic(bool1) 1656 b = simplify_logic(bool2) 1657 m = match(a, b) 1658 if m: 1659 return a, m 1660 return m is not None 1661