1""" 2Boolean algebra module for SymPy 3""" 4 5from collections import defaultdict 6from itertools import chain, combinations, product 7from sympy.core.add import Add 8from sympy.core.basic import Basic 9from sympy.core.cache import cacheit 10from sympy.core.compatibility import ordered, as_int 11from sympy.core.decorators import sympify_method_args, sympify_return 12from sympy.core.function import Application, Derivative 13from sympy.core.numbers import Number 14from sympy.core.operations import LatticeOp 15from sympy.core.singleton import Singleton, S 16from sympy.core.sympify import converter, _sympify, sympify 17from sympy.core.kind import BooleanKind 18from sympy.utilities.iterables import sift, ibin 19from sympy.utilities.misc import filldedent 20 21 22def as_Boolean(e): 23 """Like bool, return the Boolean value of an expression, e, 24 which can be any instance of Boolean or bool. 25 26 Examples 27 ======== 28 29 >>> from sympy import true, false, nan 30 >>> from sympy.logic.boolalg import as_Boolean 31 >>> from sympy.abc import x 32 >>> as_Boolean(0) is false 33 True 34 >>> as_Boolean(1) is true 35 True 36 >>> as_Boolean(x) 37 x 38 >>> as_Boolean(2) 39 Traceback (most recent call last): 40 ... 41 TypeError: expecting bool or Boolean, not `2`. 42 >>> as_Boolean(nan) 43 Traceback (most recent call last): 44 ... 45 TypeError: expecting bool or Boolean, not `nan`. 46 47 """ 48 from sympy.core.symbol import Symbol 49 if e == True: 50 return S.true 51 if e == False: 52 return S.false 53 if isinstance(e, Symbol): 54 z = e.is_zero 55 if z is None: 56 return e 57 return S.false if z else S.true 58 if isinstance(e, Boolean): 59 return e 60 raise TypeError('expecting bool or Boolean, not `%s`.' % e) 61 62 63@sympify_method_args 64class Boolean(Basic): 65 """A boolean object is an object for which logic operations make sense.""" 66 67 __slots__ = () 68 69 kind = BooleanKind 70 71 @sympify_return([('other', 'Boolean')], NotImplemented) 72 def __and__(self, other): 73 return And(self, other) 74 75 __rand__ = __and__ 76 77 @sympify_return([('other', 'Boolean')], NotImplemented) 78 def __or__(self, other): 79 return Or(self, other) 80 81 __ror__ = __or__ 82 83 def __invert__(self): 84 """Overloading for ~""" 85 return Not(self) 86 87 @sympify_return([('other', 'Boolean')], NotImplemented) 88 def __rshift__(self, other): 89 return Implies(self, other) 90 91 @sympify_return([('other', 'Boolean')], NotImplemented) 92 def __lshift__(self, other): 93 return Implies(other, self) 94 95 __rrshift__ = __lshift__ 96 __rlshift__ = __rshift__ 97 98 @sympify_return([('other', 'Boolean')], NotImplemented) 99 def __xor__(self, other): 100 return Xor(self, other) 101 102 __rxor__ = __xor__ 103 104 def equals(self, other): 105 """ 106 Returns True if the given formulas have the same truth table. 107 For two formulas to be equal they must have the same literals. 108 109 Examples 110 ======== 111 112 >>> from sympy.abc import A, B, C 113 >>> from sympy.logic.boolalg import And, Or, Not 114 >>> (A >> B).equals(~B >> ~A) 115 True 116 >>> Not(And(A, B, C)).equals(And(Not(A), Not(B), Not(C))) 117 False 118 >>> Not(And(A, Not(A))).equals(Or(B, Not(B))) 119 False 120 121 """ 122 from sympy.logic.inference import satisfiable 123 from sympy.core.relational import Relational 124 125 if self.has(Relational) or other.has(Relational): 126 raise NotImplementedError('handling of relationals') 127 return self.atoms() == other.atoms() and \ 128 not satisfiable(Not(Equivalent(self, other))) 129 130 def to_nnf(self, simplify=True): 131 # override where necessary 132 return self 133 134 def as_set(self): 135 """ 136 Rewrites Boolean expression in terms of real sets. 137 138 Examples 139 ======== 140 141 >>> from sympy import Symbol, Eq, Or, And 142 >>> x = Symbol('x', real=True) 143 >>> Eq(x, 0).as_set() 144 {0} 145 >>> (x > 0).as_set() 146 Interval.open(0, oo) 147 >>> And(-2 < x, x < 2).as_set() 148 Interval.open(-2, 2) 149 >>> Or(x < -2, 2 < x).as_set() 150 Union(Interval.open(-oo, -2), Interval.open(2, oo)) 151 152 """ 153 from sympy.calculus.util import periodicity 154 from sympy.core.relational import Relational 155 free = self.free_symbols 156 if len(free) == 1: 157 x = free.pop() 158 reps = {} 159 for r in self.atoms(Relational): 160 if periodicity(r, x) not in (0, None): 161 s = r._eval_as_set() 162 if s in (S.EmptySet, S.UniversalSet, S.Reals): 163 reps[r] = s.as_relational(x) 164 continue 165 raise NotImplementedError(filldedent(''' 166 as_set is not implemented for relationals 167 with periodic solutions 168 ''')) 169 return self.subs(reps)._eval_as_set() 170 else: 171 raise NotImplementedError("Sorry, as_set has not yet been" 172 " implemented for multivariate" 173 " expressions") 174 175 @property 176 def binary_symbols(self): 177 from sympy.core.relational import Eq, Ne 178 return set().union(*[i.binary_symbols for i in self.args 179 if i.is_Boolean or i.is_Symbol 180 or isinstance(i, (Eq, Ne))]) 181 182 def _eval_refine(self, assumptions): 183 from sympy.assumptions import ask 184 ret = ask(self, assumptions) 185 if ret is True: 186 return true 187 elif ret is False: 188 return false 189 return None 190 191 192class BooleanAtom(Boolean): 193 """ 194 Base class of BooleanTrue and BooleanFalse. 195 """ 196 is_Boolean = True 197 is_Atom = True 198 _op_priority = 11 # higher than Expr 199 200 def simplify(self, *a, **kw): 201 return self 202 203 def expand(self, *a, **kw): 204 return self 205 206 @property 207 def canonical(self): 208 return self 209 210 def _noop(self, other=None): 211 raise TypeError('BooleanAtom not allowed in this context.') 212 213 __add__ = _noop 214 __radd__ = _noop 215 __sub__ = _noop 216 __rsub__ = _noop 217 __mul__ = _noop 218 __rmul__ = _noop 219 __pow__ = _noop 220 __rpow__ = _noop 221 __truediv__ = _noop 222 __rtruediv__ = _noop 223 __mod__ = _noop 224 __rmod__ = _noop 225 _eval_power = _noop 226 227 # /// drop when Py2 is no longer supported 228 def __lt__(self, other): 229 raise TypeError(filldedent(''' 230 A Boolean argument can only be used in 231 Eq and Ne; all other relationals expect 232 real expressions. 233 ''')) 234 235 __le__ = __lt__ 236 __gt__ = __lt__ 237 __ge__ = __lt__ 238 # \\\ 239 240 241class BooleanTrue(BooleanAtom, metaclass=Singleton): 242 """ 243 SymPy version of True, a singleton that can be accessed via S.true. 244 245 This is the SymPy version of True, for use in the logic module. The 246 primary advantage of using true instead of True is that shorthand boolean 247 operations like ~ and >> will work as expected on this class, whereas with 248 True they act bitwise on 1. Functions in the logic module will return this 249 class when they evaluate to true. 250 251 Notes 252 ===== 253 254 There is liable to be some confusion as to when ``True`` should 255 be used and when ``S.true`` should be used in various contexts 256 throughout SymPy. An important thing to remember is that 257 ``sympify(True)`` returns ``S.true``. This means that for the most 258 part, you can just use ``True`` and it will automatically be converted 259 to ``S.true`` when necessary, similar to how you can generally use 1 260 instead of ``S.One``. 261 262 The rule of thumb is: 263 264 "If the boolean in question can be replaced by an arbitrary symbolic 265 ``Boolean``, like ``Or(x, y)`` or ``x > 1``, use ``S.true``. 266 Otherwise, use ``True``" 267 268 In other words, use ``S.true`` only on those contexts where the 269 boolean is being used as a symbolic representation of truth. 270 For example, if the object ends up in the ``.args`` of any expression, 271 then it must necessarily be ``S.true`` instead of ``True``, as 272 elements of ``.args`` must be ``Basic``. On the other hand, 273 ``==`` is not a symbolic operation in SymPy, since it always returns 274 ``True`` or ``False``, and does so in terms of structural equality 275 rather than mathematical, so it should return ``True``. The assumptions 276 system should use ``True`` and ``False``. Aside from not satisfying 277 the above rule of thumb, the assumptions system uses a three-valued logic 278 (``True``, ``False``, ``None``), whereas ``S.true`` and ``S.false`` 279 represent a two-valued logic. When in doubt, use ``True``. 280 281 "``S.true == True is True``." 282 283 While "``S.true is True``" is ``False``, "``S.true == True``" 284 is ``True``, so if there is any doubt over whether a function or 285 expression will return ``S.true`` or ``True``, just use ``==`` 286 instead of ``is`` to do the comparison, and it will work in either 287 case. Finally, for boolean flags, it's better to just use ``if x`` 288 instead of ``if x is True``. To quote PEP 8: 289 290 Don't compare boolean values to ``True`` or ``False`` 291 using ``==``. 292 293 * Yes: ``if greeting:`` 294 * No: ``if greeting == True:`` 295 * Worse: ``if greeting is True:`` 296 297 Examples 298 ======== 299 300 >>> from sympy import sympify, true, false, Or 301 >>> sympify(True) 302 True 303 >>> _ is True, _ is true 304 (False, True) 305 306 >>> Or(true, false) 307 True 308 >>> _ is true 309 True 310 311 Python operators give a boolean result for true but a 312 bitwise result for True 313 314 >>> ~true, ~True 315 (False, -2) 316 >>> true >> true, True >> True 317 (True, 0) 318 319 Python operators give a boolean result for true but a 320 bitwise result for True 321 322 >>> ~true, ~True 323 (False, -2) 324 >>> true >> true, True >> True 325 (True, 0) 326 327 See Also 328 ======== 329 330 sympy.logic.boolalg.BooleanFalse 331 332 """ 333 def __bool__(self): 334 return True 335 336 def __hash__(self): 337 return hash(True) 338 339 @property 340 def negated(self): 341 return S.false 342 343 def as_set(self): 344 """ 345 Rewrite logic operators and relationals in terms of real sets. 346 347 Examples 348 ======== 349 350 >>> from sympy import true 351 >>> true.as_set() 352 UniversalSet 353 354 """ 355 return S.UniversalSet 356 357 358class BooleanFalse(BooleanAtom, metaclass=Singleton): 359 """ 360 SymPy version of False, a singleton that can be accessed via S.false. 361 362 This is the SymPy version of False, for use in the logic module. The 363 primary advantage of using false instead of False is that shorthand boolean 364 operations like ~ and >> will work as expected on this class, whereas with 365 False they act bitwise on 0. Functions in the logic module will return this 366 class when they evaluate to false. 367 368 Notes 369 ====== 370 371 See the notes section in :py:class:`sympy.logic.boolalg.BooleanTrue` 372 373 Examples 374 ======== 375 376 >>> from sympy import sympify, true, false, Or 377 >>> sympify(False) 378 False 379 >>> _ is False, _ is false 380 (False, True) 381 382 >>> Or(true, false) 383 True 384 >>> _ is true 385 True 386 387 Python operators give a boolean result for false but a 388 bitwise result for False 389 390 >>> ~false, ~False 391 (True, -1) 392 >>> false >> false, False >> False 393 (True, 0) 394 395 See Also 396 ======== 397 398 sympy.logic.boolalg.BooleanTrue 399 400 """ 401 def __bool__(self): 402 return False 403 404 def __hash__(self): 405 return hash(False) 406 407 @property 408 def negated(self): 409 return S.true 410 411 def as_set(self): 412 """ 413 Rewrite logic operators and relationals in terms of real sets. 414 415 Examples 416 ======== 417 418 >>> from sympy import false 419 >>> false.as_set() 420 EmptySet 421 """ 422 return S.EmptySet 423 424 425true = BooleanTrue() 426false = BooleanFalse() 427# We want S.true and S.false to work, rather than S.BooleanTrue and 428# S.BooleanFalse, but making the class and instance names the same causes some 429# major issues (like the inability to import the class directly from this 430# file). 431S.true = true 432S.false = false 433 434converter[bool] = lambda x: S.true if x else S.false 435 436 437class BooleanFunction(Application, Boolean): 438 """Boolean function is a function that lives in a boolean space 439 It is used as base class for And, Or, Not, etc. 440 """ 441 is_Boolean = True 442 443 def _eval_simplify(self, **kwargs): 444 rv = self.func(*[a.simplify(**kwargs) for a in self.args]) 445 return simplify_logic(rv) 446 447 def simplify(self, **kwargs): 448 from sympy.simplify.simplify import simplify 449 return simplify(self, **kwargs) 450 451 def __lt__(self, other): 452 raise TypeError(filldedent(''' 453 A Boolean argument can only be used in 454 Eq and Ne; all other relationals expect 455 real expressions. 456 ''')) 457 __le__ = __lt__ 458 __ge__ = __lt__ 459 __gt__ = __lt__ 460 461 @classmethod 462 def binary_check_and_simplify(self, *args): 463 from sympy.core.relational import Relational, Eq, Ne 464 args = [as_Boolean(i) for i in args] 465 bin_syms = set().union(*[i.binary_symbols for i in args]) 466 rel = set().union(*[i.atoms(Relational) for i in args]) 467 reps = {} 468 for x in bin_syms: 469 for r in rel: 470 if x in bin_syms and x in r.free_symbols: 471 if isinstance(r, (Eq, Ne)): 472 if not ( 473 S.true in r.args or 474 S.false in r.args): 475 reps[r] = S.false 476 else: 477 raise TypeError(filldedent(''' 478 Incompatible use of binary symbol `%s` as a 479 real variable in `%s` 480 ''' % (x, r))) 481 return [i.subs(reps) for i in args] 482 483 def to_nnf(self, simplify=True): 484 return self._to_nnf(*self.args, simplify=simplify) 485 486 def to_anf(self, deep=True): 487 return self._to_anf(*self.args, deep=deep) 488 489 @classmethod 490 def _to_nnf(cls, *args, **kwargs): 491 simplify = kwargs.get('simplify', True) 492 argset = set() 493 for arg in args: 494 if not is_literal(arg): 495 arg = arg.to_nnf(simplify) 496 if simplify: 497 if isinstance(arg, cls): 498 arg = arg.args 499 else: 500 arg = (arg,) 501 for a in arg: 502 if Not(a) in argset: 503 return cls.zero 504 argset.add(a) 505 else: 506 argset.add(arg) 507 return cls(*argset) 508 509 @classmethod 510 def _to_anf(cls, *args, **kwargs): 511 deep = kwargs.get('deep', True) 512 argset = set() 513 for arg in args: 514 if deep: 515 if not is_literal(arg) or isinstance(arg, Not): 516 arg = arg.to_anf(deep=deep) 517 argset.add(arg) 518 else: 519 argset.add(arg) 520 return cls(*argset, remove_true=False) 521 522 # the diff method below is copied from Expr class 523 def diff(self, *symbols, **assumptions): 524 assumptions.setdefault("evaluate", True) 525 return Derivative(self, *symbols, **assumptions) 526 527 def _eval_derivative(self, x): 528 if x in self.binary_symbols: 529 from sympy.core.relational import Eq 530 from sympy.functions.elementary.piecewise import Piecewise 531 return Piecewise( 532 (0, Eq(self.subs(x, 0), self.subs(x, 1))), 533 (1, True)) 534 elif x in self.free_symbols: 535 # not implemented, see https://www.encyclopediaofmath.org/ 536 # index.php/Boolean_differential_calculus 537 pass 538 else: 539 return S.Zero 540 541 def _apply_patternbased_simplification(self, rv, patterns, measure, 542 dominatingvalue, 543 replacementvalue=None): 544 """ 545 Replace patterns of Relational 546 547 Parameters 548 ========== 549 550 rv : Expr 551 Boolean expression 552 553 patterns : tuple 554 Tuple of tuples, with (pattern to simplify, simplified pattern) 555 556 measure : function 557 Simplification measure 558 559 dominatingvalue : boolean or None 560 The dominating value for the function of consideration. 561 For example, for And S.false is dominating. As soon as one 562 expression is S.false in And, the whole expression is S.false. 563 564 replacementvalue : boolean or None, optional 565 The resulting value for the whole expression if one argument 566 evaluates to dominatingvalue. 567 For example, for Nand S.false is dominating, but in this case 568 the resulting value is S.true. Default is None. If replacementvalue 569 is None and dominatingvalue is not None, 570 replacementvalue = dominatingvalue 571 572 """ 573 from sympy.core.relational import Relational, _canonical 574 from sympy.functions.elementary.miscellaneous import Min, Max 575 576 if replacementvalue is None and dominatingvalue is not None: 577 replacementvalue = dominatingvalue 578 # Use replacement patterns for Relationals 579 changed = True 580 Rel, nonRel = sift(rv.args, lambda i: isinstance(i, Relational), 581 binary=True) 582 if len(Rel) <= 1: 583 return rv 584 Rel, nonRealRel = sift(Rel, lambda i: all(s.is_real is not False 585 for s in i.free_symbols), 586 binary=True) 587 Rel = [i.canonical for i in Rel] 588 while changed and len(Rel) >= 2: 589 changed = False 590 # Sort based on ordered 591 Rel = list(ordered(Rel)) 592 # Create a list of possible replacements 593 results = [] 594 # Try all combinations 595 for ((i, pi), (j, pj)) in combinations(enumerate(Rel), 2): 596 for pattern, simp in patterns: 597 res = [] 598 # use SymPy matching 599 oldexpr = rv.func(pi, pj) 600 tmpres = oldexpr.match(pattern) 601 if tmpres: 602 res.append((tmpres, oldexpr)) 603 # Try reversing first relational 604 # This and the rest should not be required with a better 605 # canonical 606 oldexpr = rv.func(pi.reversed, pj) 607 tmpres = oldexpr.match(pattern) 608 if tmpres: 609 res.append((tmpres, oldexpr)) 610 # Try reversing second relational 611 oldexpr = rv.func(pi, pj.reversed) 612 tmpres = oldexpr.match(pattern) 613 if tmpres: 614 res.append((tmpres, oldexpr)) 615 # Try reversing both relationals 616 oldexpr = rv.func(pi.reversed, pj.reversed) 617 tmpres = oldexpr.match(pattern) 618 if tmpres: 619 res.append((tmpres, oldexpr)) 620 621 if res: 622 for tmpres, oldexpr in res: 623 # we have a matching, compute replacement 624 np = simp.subs(tmpres) 625 if np == dominatingvalue: 626 # if dominatingvalue, the whole expression 627 # will be replacementvalue 628 return replacementvalue 629 # add replacement 630 if not isinstance(np, ITE) and not np.has(Min, Max): 631 # We only want to use ITE and Min/Max 632 # replacements if they simplify away 633 costsaving = measure(oldexpr) - measure(np) 634 if costsaving > 0: 635 results.append((costsaving, (i, j, np))) 636 if results: 637 # Sort results based on complexity 638 results = list(reversed(sorted(results, 639 key=lambda pair: pair[0]))) 640 # Replace the one providing most simplification 641 replacement = results[0][1] 642 i, j, newrel = replacement 643 # Remove the old relationals 644 del Rel[j] 645 del Rel[i] 646 if dominatingvalue is None or newrel != ~dominatingvalue: 647 # Insert the new one (no need to insert a value that will 648 # not affect the result) 649 Rel.append(newrel) 650 # We did change something so try again 651 changed = True 652 653 rv = rv.func(*([_canonical(i) for i in ordered(Rel)] 654 + nonRel + nonRealRel)) 655 return rv 656 657 658class And(LatticeOp, BooleanFunction): 659 """ 660 Logical AND function. 661 662 It evaluates its arguments in order, giving False immediately 663 if any of them are False, and True if they are all True. 664 665 Examples 666 ======== 667 668 >>> from sympy.abc import x, y 669 >>> from sympy.logic.boolalg import And 670 >>> x & y 671 x & y 672 673 Notes 674 ===== 675 676 The ``&`` operator is provided as a convenience, but note that its use 677 here is different from its normal use in Python, which is bitwise 678 and. Hence, ``And(a, b)`` and ``a & b`` will return different things if 679 ``a`` and ``b`` are integers. 680 681 >>> And(x, y).subs(x, 1) 682 y 683 684 """ 685 zero = false 686 identity = true 687 688 nargs = None 689 690 @classmethod 691 def _new_args_filter(cls, args): 692 args = BooleanFunction.binary_check_and_simplify(*args) 693 args = LatticeOp._new_args_filter(args, And) 694 newargs = [] 695 rel = set() 696 for x in ordered(args): 697 if x.is_Relational: 698 c = x.canonical 699 if c in rel: 700 continue 701 elif c.negated.canonical in rel: 702 return [S.false] 703 else: 704 rel.add(c) 705 newargs.append(x) 706 return newargs 707 708 def _eval_subs(self, old, new): 709 args = [] 710 bad = None 711 for i in self.args: 712 try: 713 i = i.subs(old, new) 714 except TypeError: 715 # store TypeError 716 if bad is None: 717 bad = i 718 continue 719 if i == False: 720 return S.false 721 elif i != True: 722 args.append(i) 723 if bad is not None: 724 # let it raise 725 bad.subs(old, new) 726 # If old is And, replace the parts of the arguments with new if all 727 # are there 728 if isinstance(old, And): 729 old_set = set(old.args) 730 if old_set.issubset(args): 731 args = set(args) - old_set 732 args.add(new) 733 734 return self.func(*args) 735 736 def _eval_simplify(self, **kwargs): 737 from sympy.core.relational import Equality, Relational 738 from sympy.solvers.solveset import linear_coeffs 739 # standard simplify 740 rv = super()._eval_simplify(**kwargs) 741 if not isinstance(rv, And): 742 return rv 743 744 # simplify args that are equalities involving 745 # symbols so x == 0 & x == y -> x==0 & y == 0 746 Rel, nonRel = sift(rv.args, lambda i: isinstance(i, Relational), 747 binary=True) 748 if not Rel: 749 return rv 750 eqs, other = sift(Rel, lambda i: isinstance(i, Equality), binary=True) 751 752 measure = kwargs['measure'] 753 if eqs: 754 ratio = kwargs['ratio'] 755 reps = {} 756 sifted = {} 757 # group by length of free symbols 758 sifted = sift(ordered([ 759 (i.free_symbols, i) for i in eqs]), 760 lambda x: len(x[0])) 761 eqs = [] 762 nonlineqs = [] 763 while 1 in sifted: 764 for free, e in sifted.pop(1): 765 x = free.pop() 766 if (e.lhs != x or x in e.rhs.free_symbols) and x not in reps: 767 try: 768 m, b = linear_coeffs( 769 e.rewrite(Add, evaluate=False), x) 770 enew = e.func(x, -b/m) 771 if measure(enew) <= ratio*measure(e): 772 e = enew 773 else: 774 eqs.append(e) 775 continue 776 except ValueError: 777 pass 778 if x in reps: 779 eqs.append(e.subs(x, reps[x])) 780 elif e.lhs == x and x not in e.rhs.free_symbols: 781 reps[x] = e.rhs 782 eqs.append(e) 783 else: 784 # x is not yet identified, but may be later 785 nonlineqs.append(e) 786 resifted = defaultdict(list) 787 for k in sifted: 788 for f, e in sifted[k]: 789 e = e.xreplace(reps) 790 f = e.free_symbols 791 resifted[len(f)].append((f, e)) 792 sifted = resifted 793 for k in sifted: 794 eqs.extend([e for f, e in sifted[k]]) 795 nonlineqs = [ei.subs(reps) for ei in nonlineqs] 796 other = [ei.subs(reps) for ei in other] 797 rv = rv.func(*([i.canonical for i in (eqs + nonlineqs + other)] + nonRel)) 798 patterns = simplify_patterns_and() 799 return self._apply_patternbased_simplification(rv, patterns, 800 measure, False) 801 802 def _eval_as_set(self): 803 from sympy.sets.sets import Intersection 804 return Intersection(*[arg.as_set() for arg in self.args]) 805 806 def _eval_rewrite_as_Nor(self, *args, **kwargs): 807 return Nor(*[Not(arg) for arg in self.args]) 808 809 def to_anf(self, deep=True): 810 if deep: 811 result = And._to_anf(*self.args, deep=deep) 812 return distribute_xor_over_and(result) 813 return self 814 815 816class Or(LatticeOp, BooleanFunction): 817 """ 818 Logical OR function 819 820 It evaluates its arguments in order, giving True immediately 821 if any of them are True, and False if they are all False. 822 823 Examples 824 ======== 825 826 >>> from sympy.abc import x, y 827 >>> from sympy.logic.boolalg import Or 828 >>> x | y 829 x | y 830 831 Notes 832 ===== 833 834 The ``|`` operator is provided as a convenience, but note that its use 835 here is different from its normal use in Python, which is bitwise 836 or. Hence, ``Or(a, b)`` and ``a | b`` will return different things if 837 ``a`` and ``b`` are integers. 838 839 >>> Or(x, y).subs(x, 0) 840 y 841 842 """ 843 zero = true 844 identity = false 845 846 @classmethod 847 def _new_args_filter(cls, args): 848 newargs = [] 849 rel = [] 850 args = BooleanFunction.binary_check_and_simplify(*args) 851 for x in args: 852 if x.is_Relational: 853 c = x.canonical 854 if c in rel: 855 continue 856 nc = c.negated.canonical 857 if any(r == nc for r in rel): 858 return [S.true] 859 rel.append(c) 860 newargs.append(x) 861 return LatticeOp._new_args_filter(newargs, Or) 862 863 def _eval_subs(self, old, new): 864 args = [] 865 bad = None 866 for i in self.args: 867 try: 868 i = i.subs(old, new) 869 except TypeError: 870 # store TypeError 871 if bad is None: 872 bad = i 873 continue 874 if i == True: 875 return S.true 876 elif i != False: 877 args.append(i) 878 if bad is not None: 879 # let it raise 880 bad.subs(old, new) 881 # If old is Or, replace the parts of the arguments with new if all 882 # are there 883 if isinstance(old, Or): 884 old_set = set(old.args) 885 if old_set.issubset(args): 886 args = set(args) - old_set 887 args.add(new) 888 889 return self.func(*args) 890 891 def _eval_as_set(self): 892 from sympy.sets.sets import Union 893 return Union(*[arg.as_set() for arg in self.args]) 894 895 def _eval_rewrite_as_Nand(self, *args, **kwargs): 896 return Nand(*[Not(arg) for arg in self.args]) 897 898 def _eval_simplify(self, **kwargs): 899 # standard simplify 900 rv = super()._eval_simplify(**kwargs) 901 if not isinstance(rv, Or): 902 return rv 903 patterns = simplify_patterns_or() 904 return self._apply_patternbased_simplification(rv, patterns, 905 kwargs['measure'], S.true) 906 907 def to_anf(self, deep=True): 908 args = range(1, len(self.args) + 1) 909 args = (combinations(self.args, j) for j in args) 910 args = chain.from_iterable(args) # powerset 911 args = (And(*arg) for arg in args) 912 args = map(lambda x: to_anf(x, deep=deep) if deep else x, args) 913 return Xor(*list(args), remove_true=False) 914 915 916class Not(BooleanFunction): 917 """ 918 Logical Not function (negation) 919 920 921 Returns True if the statement is False 922 Returns False if the statement is True 923 924 Examples 925 ======== 926 927 >>> from sympy.logic.boolalg import Not, And, Or 928 >>> from sympy.abc import x, A, B 929 >>> Not(True) 930 False 931 >>> Not(False) 932 True 933 >>> Not(And(True, False)) 934 True 935 >>> Not(Or(True, False)) 936 False 937 >>> Not(And(And(True, x), Or(x, False))) 938 ~x 939 >>> ~x 940 ~x 941 >>> Not(And(Or(A, B), Or(~A, ~B))) 942 ~((A | B) & (~A | ~B)) 943 944 Notes 945 ===== 946 947 - The ``~`` operator is provided as a convenience, but note that its use 948 here is different from its normal use in Python, which is bitwise 949 not. In particular, ``~a`` and ``Not(a)`` will be different if ``a`` is 950 an integer. Furthermore, since bools in Python subclass from ``int``, 951 ``~True`` is the same as ``~1`` which is ``-2``, which has a boolean 952 value of True. To avoid this issue, use the SymPy boolean types 953 ``true`` and ``false``. 954 955 >>> from sympy import true 956 >>> ~True 957 -2 958 >>> ~true 959 False 960 961 """ 962 963 is_Not = True 964 965 @classmethod 966 def eval(cls, arg): 967 if isinstance(arg, Number) or arg in (True, False): 968 return false if arg else true 969 if arg.is_Not: 970 return arg.args[0] 971 # Simplify Relational objects. 972 if arg.is_Relational: 973 return arg.negated 974 975 def _eval_as_set(self): 976 """ 977 Rewrite logic operators and relationals in terms of real sets. 978 979 Examples 980 ======== 981 982 >>> from sympy import Not, Symbol 983 >>> x = Symbol('x') 984 >>> Not(x > 0).as_set() 985 Interval(-oo, 0) 986 """ 987 return self.args[0].as_set().complement(S.Reals) 988 989 def to_nnf(self, simplify=True): 990 if is_literal(self): 991 return self 992 993 expr = self.args[0] 994 995 func, args = expr.func, expr.args 996 997 if func == And: 998 return Or._to_nnf(*[~arg for arg in args], simplify=simplify) 999 1000 if func == Or: 1001 return And._to_nnf(*[~arg for arg in args], simplify=simplify) 1002 1003 if func == Implies: 1004 a, b = args 1005 return And._to_nnf(a, ~b, simplify=simplify) 1006 1007 if func == Equivalent: 1008 return And._to_nnf(Or(*args), Or(*[~arg for arg in args]), 1009 simplify=simplify) 1010 1011 if func == Xor: 1012 result = [] 1013 for i in range(1, len(args)+1, 2): 1014 for neg in combinations(args, i): 1015 clause = [~s if s in neg else s for s in args] 1016 result.append(Or(*clause)) 1017 return And._to_nnf(*result, simplify=simplify) 1018 1019 if func == ITE: 1020 a, b, c = args 1021 return And._to_nnf(Or(a, ~c), Or(~a, ~b), simplify=simplify) 1022 1023 raise ValueError("Illegal operator %s in expression" % func) 1024 1025 def to_anf(self, deep=True): 1026 return Xor._to_anf(true, self.args[0], deep=deep) 1027 1028 1029class Xor(BooleanFunction): 1030 """ 1031 Logical XOR (exclusive OR) function. 1032 1033 1034 Returns True if an odd number of the arguments are True and the rest are 1035 False. 1036 1037 Returns False if an even number of the arguments are True and the rest are 1038 False. 1039 1040 Examples 1041 ======== 1042 1043 >>> from sympy.logic.boolalg import Xor 1044 >>> from sympy import symbols 1045 >>> x, y = symbols('x y') 1046 >>> Xor(True, False) 1047 True 1048 >>> Xor(True, True) 1049 False 1050 >>> Xor(True, False, True, True, False) 1051 True 1052 >>> Xor(True, False, True, False) 1053 False 1054 >>> x ^ y 1055 x ^ y 1056 1057 Notes 1058 ===== 1059 1060 The ``^`` operator is provided as a convenience, but note that its use 1061 here is different from its normal use in Python, which is bitwise xor. In 1062 particular, ``a ^ b`` and ``Xor(a, b)`` will be different if ``a`` and 1063 ``b`` are integers. 1064 1065 >>> Xor(x, y).subs(y, 0) 1066 x 1067 1068 """ 1069 def __new__(cls, *args, remove_true=True, **kwargs): 1070 argset = set() 1071 obj = super().__new__(cls, *args, **kwargs) 1072 for arg in obj._args: 1073 if isinstance(arg, Number) or arg in (True, False): 1074 if arg: 1075 arg = true 1076 else: 1077 continue 1078 if isinstance(arg, Xor): 1079 for a in arg.args: 1080 argset.remove(a) if a in argset else argset.add(a) 1081 elif arg in argset: 1082 argset.remove(arg) 1083 else: 1084 argset.add(arg) 1085 rel = [(r, r.canonical, r.negated.canonical) 1086 for r in argset if r.is_Relational] 1087 odd = False # is number of complimentary pairs odd? start 0 -> False 1088 remove = [] 1089 for i, (r, c, nc) in enumerate(rel): 1090 for j in range(i + 1, len(rel)): 1091 rj, cj = rel[j][:2] 1092 if cj == nc: 1093 odd = ~odd 1094 break 1095 elif cj == c: 1096 break 1097 else: 1098 continue 1099 remove.append((r, rj)) 1100 if odd: 1101 argset.remove(true) if true in argset else argset.add(true) 1102 for a, b in remove: 1103 argset.remove(a) 1104 argset.remove(b) 1105 if len(argset) == 0: 1106 return false 1107 elif len(argset) == 1: 1108 return argset.pop() 1109 elif True in argset and remove_true: 1110 argset.remove(True) 1111 return Not(Xor(*argset)) 1112 else: 1113 obj._args = tuple(ordered(argset)) 1114 obj._argset = frozenset(argset) 1115 return obj 1116 1117 # XXX: This should be cached on the object rather than using cacheit 1118 # Maybe it can be computed in __new__? 1119 @property # type: ignore 1120 @cacheit 1121 def args(self): 1122 return tuple(ordered(self._argset)) 1123 1124 def to_nnf(self, simplify=True): 1125 args = [] 1126 for i in range(0, len(self.args)+1, 2): 1127 for neg in combinations(self.args, i): 1128 clause = [~s if s in neg else s for s in self.args] 1129 args.append(Or(*clause)) 1130 return And._to_nnf(*args, simplify=simplify) 1131 1132 def _eval_rewrite_as_Or(self, *args, **kwargs): 1133 a = self.args 1134 return Or(*[_convert_to_varsSOP(x, self.args) 1135 for x in _get_odd_parity_terms(len(a))]) 1136 1137 def _eval_rewrite_as_And(self, *args, **kwargs): 1138 a = self.args 1139 return And(*[_convert_to_varsPOS(x, self.args) 1140 for x in _get_even_parity_terms(len(a))]) 1141 1142 def _eval_simplify(self, **kwargs): 1143 # as standard simplify uses simplify_logic which writes things as 1144 # And and Or, we only simplify the partial expressions before using 1145 # patterns 1146 rv = self.func(*[a.simplify(**kwargs) for a in self.args]) 1147 if not isinstance(rv, Xor): # This shouldn't really happen here 1148 return rv 1149 patterns = simplify_patterns_xor() 1150 return self._apply_patternbased_simplification(rv, patterns, 1151 kwargs['measure'], None) 1152 1153 def _eval_subs(self, old, new): 1154 # If old is Xor, replace the parts of the arguments with new if all 1155 # are there 1156 if isinstance(old, Xor): 1157 old_set = set(old.args) 1158 if old_set.issubset(self.args): 1159 args = set(self.args) - old_set 1160 args.add(new) 1161 return self.func(*args) 1162 1163 1164class Nand(BooleanFunction): 1165 """ 1166 Logical NAND function. 1167 1168 It evaluates its arguments in order, giving True immediately if any 1169 of them are False, and False if they are all True. 1170 1171 Returns True if any of the arguments are False 1172 Returns False if all arguments are True 1173 1174 Examples 1175 ======== 1176 1177 >>> from sympy.logic.boolalg import Nand 1178 >>> from sympy import symbols 1179 >>> x, y = symbols('x y') 1180 >>> Nand(False, True) 1181 True 1182 >>> Nand(True, True) 1183 False 1184 >>> Nand(x, y) 1185 ~(x & y) 1186 1187 """ 1188 @classmethod 1189 def eval(cls, *args): 1190 return Not(And(*args)) 1191 1192 1193class Nor(BooleanFunction): 1194 """ 1195 Logical NOR function. 1196 1197 It evaluates its arguments in order, giving False immediately if any 1198 of them are True, and True if they are all False. 1199 1200 Returns False if any argument is True 1201 Returns True if all arguments are False 1202 1203 Examples 1204 ======== 1205 1206 >>> from sympy.logic.boolalg import Nor 1207 >>> from sympy import symbols 1208 >>> x, y = symbols('x y') 1209 1210 >>> Nor(True, False) 1211 False 1212 >>> Nor(True, True) 1213 False 1214 >>> Nor(False, True) 1215 False 1216 >>> Nor(False, False) 1217 True 1218 >>> Nor(x, y) 1219 ~(x | y) 1220 1221 """ 1222 @classmethod 1223 def eval(cls, *args): 1224 return Not(Or(*args)) 1225 1226 1227class Xnor(BooleanFunction): 1228 """ 1229 Logical XNOR function. 1230 1231 Returns False if an odd number of the arguments are True and the rest are 1232 False. 1233 1234 Returns True if an even number of the arguments are True and the rest are 1235 False. 1236 1237 Examples 1238 ======== 1239 1240 >>> from sympy.logic.boolalg import Xnor 1241 >>> from sympy import symbols 1242 >>> x, y = symbols('x y') 1243 >>> Xnor(True, False) 1244 False 1245 >>> Xnor(True, True) 1246 True 1247 >>> Xnor(True, False, True, True, False) 1248 False 1249 >>> Xnor(True, False, True, False) 1250 True 1251 1252 """ 1253 @classmethod 1254 def eval(cls, *args): 1255 return Not(Xor(*args)) 1256 1257 1258class Implies(BooleanFunction): 1259 """ 1260 Logical implication. 1261 1262 A implies B is equivalent to !A v B 1263 1264 Accepts two Boolean arguments; A and B. 1265 Returns False if A is True and B is False 1266 Returns True otherwise. 1267 1268 Examples 1269 ======== 1270 1271 >>> from sympy.logic.boolalg import Implies 1272 >>> from sympy import symbols 1273 >>> x, y = symbols('x y') 1274 1275 >>> Implies(True, False) 1276 False 1277 >>> Implies(False, False) 1278 True 1279 >>> Implies(True, True) 1280 True 1281 >>> Implies(False, True) 1282 True 1283 >>> x >> y 1284 Implies(x, y) 1285 >>> y << x 1286 Implies(x, y) 1287 1288 Notes 1289 ===== 1290 1291 The ``>>`` and ``<<`` operators are provided as a convenience, but note 1292 that their use here is different from their normal use in Python, which is 1293 bit shifts. Hence, ``Implies(a, b)`` and ``a >> b`` will return different 1294 things if ``a`` and ``b`` are integers. In particular, since Python 1295 considers ``True`` and ``False`` to be integers, ``True >> True`` will be 1296 the same as ``1 >> 1``, i.e., 0, which has a truth value of False. To 1297 avoid this issue, use the SymPy objects ``true`` and ``false``. 1298 1299 >>> from sympy import true, false 1300 >>> True >> False 1301 1 1302 >>> true >> false 1303 False 1304 1305 """ 1306 @classmethod 1307 def eval(cls, *args): 1308 try: 1309 newargs = [] 1310 for x in args: 1311 if isinstance(x, Number) or x in (0, 1): 1312 newargs.append(bool(x)) 1313 else: 1314 newargs.append(x) 1315 A, B = newargs 1316 except ValueError: 1317 raise ValueError( 1318 "%d operand(s) used for an Implies " 1319 "(pairs are required): %s" % (len(args), str(args))) 1320 if A == True or A == False or B == True or B == False: 1321 return Or(Not(A), B) 1322 elif A == B: 1323 return S.true 1324 elif A.is_Relational and B.is_Relational: 1325 if A.canonical == B.canonical: 1326 return S.true 1327 if A.negated.canonical == B.canonical: 1328 return B 1329 else: 1330 return Basic.__new__(cls, *args) 1331 1332 def to_nnf(self, simplify=True): 1333 a, b = self.args 1334 return Or._to_nnf(~a, b, simplify=simplify) 1335 1336 def to_anf(self, deep=True): 1337 a, b = self.args 1338 return Xor._to_anf(true, a, And(a, b), deep=deep) 1339 1340 1341class Equivalent(BooleanFunction): 1342 """ 1343 Equivalence relation. 1344 1345 Equivalent(A, B) is True iff A and B are both True or both False 1346 1347 Returns True if all of the arguments are logically equivalent. 1348 Returns False otherwise. 1349 1350 Examples 1351 ======== 1352 1353 >>> from sympy.logic.boolalg import Equivalent, And 1354 >>> from sympy.abc import x 1355 >>> Equivalent(False, False, False) 1356 True 1357 >>> Equivalent(True, False, False) 1358 False 1359 >>> Equivalent(x, And(x, True)) 1360 True 1361 1362 """ 1363 def __new__(cls, *args, **options): 1364 from sympy.core.relational import Relational 1365 args = [_sympify(arg) for arg in args] 1366 1367 argset = set(args) 1368 for x in args: 1369 if isinstance(x, Number) or x in [True, False]: # Includes 0, 1 1370 argset.discard(x) 1371 argset.add(bool(x)) 1372 rel = [] 1373 for r in argset: 1374 if isinstance(r, Relational): 1375 rel.append((r, r.canonical, r.negated.canonical)) 1376 remove = [] 1377 for i, (r, c, nc) in enumerate(rel): 1378 for j in range(i + 1, len(rel)): 1379 rj, cj = rel[j][:2] 1380 if cj == nc: 1381 return false 1382 elif cj == c: 1383 remove.append((r, rj)) 1384 break 1385 for a, b in remove: 1386 argset.remove(a) 1387 argset.remove(b) 1388 argset.add(True) 1389 if len(argset) <= 1: 1390 return true 1391 if True in argset: 1392 argset.discard(True) 1393 return And(*argset) 1394 if False in argset: 1395 argset.discard(False) 1396 return And(*[~arg for arg in argset]) 1397 _args = frozenset(argset) 1398 obj = super().__new__(cls, _args) 1399 obj._argset = _args 1400 return obj 1401 1402 # XXX: This should be cached on the object rather than using cacheit 1403 # Maybe it can be computed in __new__? 1404 @property # type: ignore 1405 @cacheit 1406 def args(self): 1407 return tuple(ordered(self._argset)) 1408 1409 def to_nnf(self, simplify=True): 1410 args = [] 1411 for a, b in zip(self.args, self.args[1:]): 1412 args.append(Or(~a, b)) 1413 args.append(Or(~self.args[-1], self.args[0])) 1414 return And._to_nnf(*args, simplify=simplify) 1415 1416 def to_anf(self, deep=True): 1417 a = And(*self.args) 1418 b = And(*[to_anf(Not(arg), deep=False) for arg in self.args]) 1419 b = distribute_xor_over_and(b) 1420 return Xor._to_anf(a, b, deep=deep) 1421 1422 1423class ITE(BooleanFunction): 1424 """ 1425 If then else clause. 1426 1427 ITE(A, B, C) evaluates and returns the result of B if A is true 1428 else it returns the result of C. All args must be Booleans. 1429 1430 Examples 1431 ======== 1432 1433 >>> from sympy.logic.boolalg import ITE, And, Xor, Or 1434 >>> from sympy.abc import x, y, z 1435 >>> ITE(True, False, True) 1436 False 1437 >>> ITE(Or(True, False), And(True, True), Xor(True, True)) 1438 True 1439 >>> ITE(x, y, z) 1440 ITE(x, y, z) 1441 >>> ITE(True, x, y) 1442 x 1443 >>> ITE(False, x, y) 1444 y 1445 >>> ITE(x, y, y) 1446 y 1447 1448 Trying to use non-Boolean args will generate a TypeError: 1449 1450 >>> ITE(True, [], ()) 1451 Traceback (most recent call last): 1452 ... 1453 TypeError: expecting bool, Boolean or ITE, not `[]` 1454 1455 """ 1456 def __new__(cls, *args, **kwargs): 1457 from sympy.core.relational import Eq, Ne 1458 if len(args) != 3: 1459 raise ValueError('expecting exactly 3 args') 1460 a, b, c = args 1461 # check use of binary symbols 1462 if isinstance(a, (Eq, Ne)): 1463 # in this context, we can evaluate the Eq/Ne 1464 # if one arg is a binary symbol and the other 1465 # is true/false 1466 b, c = map(as_Boolean, (b, c)) 1467 bin_syms = set().union(*[i.binary_symbols for i in (b, c)]) 1468 if len(set(a.args) - bin_syms) == 1: 1469 # one arg is a binary_symbols 1470 _a = a 1471 if a.lhs is S.true: 1472 a = a.rhs 1473 elif a.rhs is S.true: 1474 a = a.lhs 1475 elif a.lhs is S.false: 1476 a = ~a.rhs 1477 elif a.rhs is S.false: 1478 a = ~a.lhs 1479 else: 1480 # binary can only equal True or False 1481 a = S.false 1482 if isinstance(_a, Ne): 1483 a = ~a 1484 else: 1485 a, b, c = BooleanFunction.binary_check_and_simplify( 1486 a, b, c) 1487 rv = None 1488 if kwargs.get('evaluate', True): 1489 rv = cls.eval(a, b, c) 1490 if rv is None: 1491 rv = BooleanFunction.__new__(cls, a, b, c, evaluate=False) 1492 return rv 1493 1494 @classmethod 1495 def eval(cls, *args): 1496 from sympy.core.relational import Eq, Ne 1497 # do the args give a singular result? 1498 a, b, c = args 1499 if isinstance(a, (Ne, Eq)): 1500 _a = a 1501 if S.true in a.args: 1502 a = a.lhs if a.rhs is S.true else a.rhs 1503 elif S.false in a.args: 1504 a = ~a.lhs if a.rhs is S.false else ~a.rhs 1505 else: 1506 _a = None 1507 if _a is not None and isinstance(_a, Ne): 1508 a = ~a 1509 if a is S.true: 1510 return b 1511 if a is S.false: 1512 return c 1513 if b == c: 1514 return b 1515 else: 1516 # or maybe the results allow the answer to be expressed 1517 # in terms of the condition 1518 if b is S.true and c is S.false: 1519 return a 1520 if b is S.false and c is S.true: 1521 return Not(a) 1522 if [a, b, c] != args: 1523 return cls(a, b, c, evaluate=False) 1524 1525 def to_nnf(self, simplify=True): 1526 a, b, c = self.args 1527 return And._to_nnf(Or(~a, b), Or(a, c), simplify=simplify) 1528 1529 def _eval_as_set(self): 1530 return self.to_nnf().as_set() 1531 1532 def _eval_rewrite_as_Piecewise(self, *args, **kwargs): 1533 from sympy.functions import Piecewise 1534 return Piecewise((args[1], args[0]), (args[2], True)) 1535 1536 1537class Exclusive(BooleanFunction): 1538 """ 1539 True if only one or no argument is true. 1540 1541 ``Exclusive(A, B, C)`` is equivalent to ``~(A & B) & ~(A & C) & ~(B & C)``. 1542 1543 Examples 1544 ======== 1545 1546 >>> from sympy.logic.boolalg import Exclusive 1547 >>> Exclusive(False, False, False) 1548 True 1549 >>> Exclusive(False, True, False) 1550 True 1551 >>> Exclusive(False, True, True) 1552 False 1553 1554 """ 1555 @classmethod 1556 def eval(cls, *args): 1557 and_args = [] 1558 for a, b in combinations(args, 2): 1559 and_args.append(Not(And(a, b))) 1560 return And(*and_args) 1561 1562 1563# end class definitions. Some useful methods 1564 1565 1566def conjuncts(expr): 1567 """Return a list of the conjuncts in the expr s. 1568 1569 Examples 1570 ======== 1571 1572 >>> from sympy.logic.boolalg import conjuncts 1573 >>> from sympy.abc import A, B 1574 >>> conjuncts(A & B) 1575 frozenset({A, B}) 1576 >>> conjuncts(A | B) 1577 frozenset({A | B}) 1578 1579 """ 1580 return And.make_args(expr) 1581 1582 1583def disjuncts(expr): 1584 """Return a list of the disjuncts in the sentence s. 1585 1586 Examples 1587 ======== 1588 1589 >>> from sympy.logic.boolalg import disjuncts 1590 >>> from sympy.abc import A, B 1591 >>> disjuncts(A | B) 1592 frozenset({A, B}) 1593 >>> disjuncts(A & B) 1594 frozenset({A & B}) 1595 1596 """ 1597 return Or.make_args(expr) 1598 1599 1600def distribute_and_over_or(expr): 1601 """ 1602 Given a sentence s consisting of conjunctions and disjunctions 1603 of literals, return an equivalent sentence in CNF. 1604 1605 Examples 1606 ======== 1607 1608 >>> from sympy.logic.boolalg import distribute_and_over_or, And, Or, Not 1609 >>> from sympy.abc import A, B, C 1610 >>> distribute_and_over_or(Or(A, And(Not(B), Not(C)))) 1611 (A | ~B) & (A | ~C) 1612 1613 """ 1614 return _distribute((expr, And, Or)) 1615 1616 1617def distribute_or_over_and(expr): 1618 """ 1619 Given a sentence s consisting of conjunctions and disjunctions 1620 of literals, return an equivalent sentence in DNF. 1621 1622 Note that the output is NOT simplified. 1623 1624 Examples 1625 ======== 1626 1627 >>> from sympy.logic.boolalg import distribute_or_over_and, And, Or, Not 1628 >>> from sympy.abc import A, B, C 1629 >>> distribute_or_over_and(And(Or(Not(A), B), C)) 1630 (B & C) | (C & ~A) 1631 1632 """ 1633 return _distribute((expr, Or, And)) 1634 1635 1636def distribute_xor_over_and(expr): 1637 """ 1638 Given a sentence s consisting of conjunction and 1639 exclusive disjunctions of literals, return an 1640 equivalent exclusive disjunction. 1641 1642 Note that the output is NOT simplified. 1643 1644 Examples 1645 ======== 1646 1647 >>> from sympy.logic.boolalg import distribute_xor_over_and, And, Xor, Not 1648 >>> from sympy.abc import A, B, C 1649 >>> distribute_xor_over_and(And(Xor(Not(A), B), C)) 1650 (B & C) ^ (C & ~A) 1651 """ 1652 return _distribute((expr, Xor, And)) 1653 1654 1655def _distribute(info): 1656 """ 1657 Distributes info[1] over info[2] with respect to info[0]. 1658 """ 1659 if isinstance(info[0], info[2]): 1660 for arg in info[0].args: 1661 if isinstance(arg, info[1]): 1662 conj = arg 1663 break 1664 else: 1665 return info[0] 1666 rest = info[2](*[a for a in info[0].args if a is not conj]) 1667 return info[1](*list(map(_distribute, 1668 [(info[2](c, rest), info[1], info[2]) 1669 for c in conj.args])), remove_true=False) 1670 elif isinstance(info[0], info[1]): 1671 return info[1](*list(map(_distribute, 1672 [(x, info[1], info[2]) 1673 for x in info[0].args])), 1674 remove_true=False) 1675 else: 1676 return info[0] 1677 1678 1679def to_anf(expr, deep=True): 1680 r""" 1681 Converts expr to Algebraic Normal Form (ANF). 1682 1683 ANF is a canonical normal form, which means that two 1684 equivalent formulas will convert to the same ANF. 1685 1686 A logical expression is in ANF if it has the form 1687 1688 .. math:: 1 \oplus a \oplus b \oplus ab \oplus abc 1689 1690 i.e. it can be: 1691 - purely true, 1692 - purely false, 1693 - conjunction of variables, 1694 - exclusive disjunction. 1695 1696 The exclusive disjunction can only contain true, variables 1697 or conjunction of variables. No negations are permitted. 1698 1699 If ``deep`` is ``False``, arguments of the boolean 1700 expression are considered variables, i.e. only the 1701 top-level expression is converted to ANF. 1702 1703 Examples 1704 ======== 1705 >>> from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent 1706 >>> from sympy.logic.boolalg import to_anf 1707 >>> from sympy.abc import A, B, C 1708 >>> to_anf(Not(A)) 1709 A ^ True 1710 >>> to_anf(And(Or(A, B), Not(C))) 1711 A ^ B ^ (A & B) ^ (A & C) ^ (B & C) ^ (A & B & C) 1712 >>> to_anf(Implies(Not(A), Equivalent(B, C)), deep=False) 1713 True ^ ~A ^ (~A & (Equivalent(B, C))) 1714 1715 """ 1716 expr = sympify(expr) 1717 1718 if is_anf(expr): 1719 return expr 1720 return expr.to_anf(deep=deep) 1721 1722 1723def to_nnf(expr, simplify=True): 1724 """ 1725 Converts expr to Negation Normal Form. 1726 A logical expression is in Negation Normal Form (NNF) if it 1727 contains only And, Or and Not, and Not is applied only to literals. 1728 If simplify is True, the result contains no redundant clauses. 1729 1730 Examples 1731 ======== 1732 1733 >>> from sympy.abc import A, B, C, D 1734 >>> from sympy.logic.boolalg import Not, Equivalent, to_nnf 1735 >>> to_nnf(Not((~A & ~B) | (C & D))) 1736 (A | B) & (~C | ~D) 1737 >>> to_nnf(Equivalent(A >> B, B >> A)) 1738 (A | ~B | (A & ~B)) & (B | ~A | (B & ~A)) 1739 1740 """ 1741 if is_nnf(expr, simplify): 1742 return expr 1743 return expr.to_nnf(simplify) 1744 1745 1746def to_cnf(expr, simplify=False, force=False): 1747 """ 1748 Convert a propositional logical sentence s to conjunctive normal 1749 form: ((A | ~B | ...) & (B | C | ...) & ...). 1750 If simplify is True, the expr is evaluated to its simplest CNF 1751 form using the Quine-McCluskey algorithm; this may take a long 1752 time if there are more than 8 variables and requires that the 1753 ``force`` flag be set to True (default is False). 1754 1755 Examples 1756 ======== 1757 1758 >>> from sympy.logic.boolalg import to_cnf 1759 >>> from sympy.abc import A, B, D 1760 >>> to_cnf(~(A | B) | D) 1761 (D | ~A) & (D | ~B) 1762 >>> to_cnf((A | B) & (A | ~A), True) 1763 A | B 1764 1765 """ 1766 expr = sympify(expr) 1767 if not isinstance(expr, BooleanFunction): 1768 return expr 1769 1770 if simplify: 1771 if not force and len(_find_predicates(expr)) > 8: 1772 raise ValueError(filldedent(''' 1773 To simplify a logical expression with more 1774 than 8 variables may take a long time and requires 1775 the use of `force=True`.''')) 1776 return simplify_logic(expr, 'cnf', True, force=force) 1777 1778 # Don't convert unless we have to 1779 if is_cnf(expr): 1780 return expr 1781 1782 expr = eliminate_implications(expr) 1783 res = distribute_and_over_or(expr) 1784 1785 return res 1786 1787 1788def to_dnf(expr, simplify=False, force=False): 1789 """ 1790 Convert a propositional logical sentence s to disjunctive normal 1791 form: ((A & ~B & ...) | (B & C & ...) | ...). 1792 If simplify is True, the expr is evaluated to its simplest DNF form using 1793 the Quine-McCluskey algorithm; this may take a long 1794 time if there are more than 8 variables and requires that the 1795 ``force`` flag be set to True (default is False). 1796 1797 Examples 1798 ======== 1799 1800 >>> from sympy.logic.boolalg import to_dnf 1801 >>> from sympy.abc import A, B, C 1802 >>> to_dnf(B & (A | C)) 1803 (A & B) | (B & C) 1804 >>> to_dnf((A & B) | (A & ~B) | (B & C) | (~B & C), True) 1805 A | C 1806 1807 """ 1808 expr = sympify(expr) 1809 if not isinstance(expr, BooleanFunction): 1810 return expr 1811 1812 if simplify: 1813 if not force and len(_find_predicates(expr)) > 8: 1814 raise ValueError(filldedent(''' 1815 To simplify a logical expression with more 1816 than 8 variables may take a long time and requires 1817 the use of `force=True`.''')) 1818 return simplify_logic(expr, 'dnf', True, force=force) 1819 1820 # Don't convert unless we have to 1821 if is_dnf(expr): 1822 return expr 1823 1824 expr = eliminate_implications(expr) 1825 return distribute_or_over_and(expr) 1826 1827 1828def is_anf(expr): 1829 r""" 1830 Checks if expr is in Algebraic Normal Form (ANF). 1831 1832 A logical expression is in ANF if it has the form 1833 1834 .. math:: 1 \oplus a \oplus b \oplus ab \oplus abc 1835 1836 i.e. it is purely true, purely false, conjunction of 1837 variables or exclusive disjunction. The exclusive 1838 disjunction can only contain true, variables or 1839 conjunction of variables. No negations are permitted. 1840 1841 Examples 1842 ======== 1843 >>> from sympy.logic.boolalg import And, Not, Xor, true, is_anf 1844 >>> from sympy.abc import A, B, C 1845 >>> is_anf(true) 1846 True 1847 >>> is_anf(A) 1848 True 1849 >>> is_anf(And(A, B, C)) 1850 True 1851 >>> is_anf(Xor(A, Not(B))) 1852 False 1853 1854 """ 1855 expr = sympify(expr) 1856 1857 if is_literal(expr) and not isinstance(expr, Not): 1858 return True 1859 1860 if isinstance(expr, And): 1861 for arg in expr.args: 1862 if not arg.is_Symbol: 1863 return False 1864 return True 1865 1866 elif isinstance(expr, Xor): 1867 for arg in expr.args: 1868 if isinstance(arg, And): 1869 for a in arg.args: 1870 if not a.is_Symbol: 1871 return False 1872 elif is_literal(arg): 1873 if isinstance(arg, Not): 1874 return False 1875 else: 1876 return False 1877 return True 1878 1879 else: 1880 return False 1881 1882 1883def is_nnf(expr, simplified=True): 1884 """ 1885 Checks if expr is in Negation Normal Form. 1886 A logical expression is in Negation Normal Form (NNF) if it 1887 contains only And, Or and Not, and Not is applied only to literals. 1888 If simplified is True, checks if result contains no redundant clauses. 1889 1890 Examples 1891 ======== 1892 1893 >>> from sympy.abc import A, B, C 1894 >>> from sympy.logic.boolalg import Not, is_nnf 1895 >>> is_nnf(A & B | ~C) 1896 True 1897 >>> is_nnf((A | ~A) & (B | C)) 1898 False 1899 >>> is_nnf((A | ~A) & (B | C), False) 1900 True 1901 >>> is_nnf(Not(A & B) | C) 1902 False 1903 >>> is_nnf((A >> B) & (B >> A)) 1904 False 1905 1906 """ 1907 1908 expr = sympify(expr) 1909 if is_literal(expr): 1910 return True 1911 1912 stack = [expr] 1913 1914 while stack: 1915 expr = stack.pop() 1916 if expr.func in (And, Or): 1917 if simplified: 1918 args = expr.args 1919 for arg in args: 1920 if Not(arg) in args: 1921 return False 1922 stack.extend(expr.args) 1923 1924 elif not is_literal(expr): 1925 return False 1926 1927 return True 1928 1929 1930def is_cnf(expr): 1931 """ 1932 Test whether or not an expression is in conjunctive normal form. 1933 1934 Examples 1935 ======== 1936 1937 >>> from sympy.logic.boolalg import is_cnf 1938 >>> from sympy.abc import A, B, C 1939 >>> is_cnf(A | B | C) 1940 True 1941 >>> is_cnf(A & B & C) 1942 True 1943 >>> is_cnf((A & B) | C) 1944 False 1945 1946 """ 1947 return _is_form(expr, And, Or) 1948 1949 1950def is_dnf(expr): 1951 """ 1952 Test whether or not an expression is in disjunctive normal form. 1953 1954 Examples 1955 ======== 1956 1957 >>> from sympy.logic.boolalg import is_dnf 1958 >>> from sympy.abc import A, B, C 1959 >>> is_dnf(A | B | C) 1960 True 1961 >>> is_dnf(A & B & C) 1962 True 1963 >>> is_dnf((A & B) | C) 1964 True 1965 >>> is_dnf(A & (B | C)) 1966 False 1967 1968 """ 1969 return _is_form(expr, Or, And) 1970 1971 1972def _is_form(expr, function1, function2): 1973 """ 1974 Test whether or not an expression is of the required form. 1975 1976 """ 1977 expr = sympify(expr) 1978 1979 vals = function1.make_args(expr) if isinstance(expr, function1) else [expr] 1980 for lit in vals: 1981 if isinstance(lit, function2): 1982 vals2 = function2.make_args(lit) if isinstance(lit, function2) else [lit] 1983 for l in vals2: 1984 if is_literal(l) is False: 1985 return False 1986 elif is_literal(lit) is False: 1987 return False 1988 1989 return True 1990 1991 1992def eliminate_implications(expr): 1993 """ 1994 Change >>, <<, and Equivalent into &, |, and ~. That is, return an 1995 expression that is equivalent to s, but has only &, |, and ~ as logical 1996 operators. 1997 1998 Examples 1999 ======== 2000 2001 >>> from sympy.logic.boolalg import Implies, Equivalent, \ 2002 eliminate_implications 2003 >>> from sympy.abc import A, B, C 2004 >>> eliminate_implications(Implies(A, B)) 2005 B | ~A 2006 >>> eliminate_implications(Equivalent(A, B)) 2007 (A | ~B) & (B | ~A) 2008 >>> eliminate_implications(Equivalent(A, B, C)) 2009 (A | ~C) & (B | ~A) & (C | ~B) 2010 2011 """ 2012 return to_nnf(expr, simplify=False) 2013 2014 2015def is_literal(expr): 2016 """ 2017 Returns True if expr is a literal, else False. 2018 2019 Examples 2020 ======== 2021 2022 >>> from sympy import Or, Q 2023 >>> from sympy.abc import A, B 2024 >>> from sympy.logic.boolalg import is_literal 2025 >>> is_literal(A) 2026 True 2027 >>> is_literal(~A) 2028 True 2029 >>> is_literal(Q.zero(A)) 2030 True 2031 >>> is_literal(A + B) 2032 True 2033 >>> is_literal(Or(A, B)) 2034 False 2035 2036 """ 2037 from sympy.assumptions import AppliedPredicate 2038 2039 if isinstance(expr, Not): 2040 return is_literal(expr.args[0]) 2041 elif expr in (True, False) or isinstance(expr, AppliedPredicate) or expr.is_Atom: 2042 return True 2043 elif not isinstance(expr, BooleanFunction) and all( 2044 (isinstance(expr, AppliedPredicate) or a.is_Atom) for a in expr.args): 2045 return True 2046 return False 2047 2048 2049def to_int_repr(clauses, symbols): 2050 """ 2051 Takes clauses in CNF format and puts them into an integer representation. 2052 2053 Examples 2054 ======== 2055 2056 >>> from sympy.logic.boolalg import to_int_repr 2057 >>> from sympy.abc import x, y 2058 >>> to_int_repr([x | y, y], [x, y]) == [{1, 2}, {2}] 2059 True 2060 2061 """ 2062 2063 # Convert the symbol list into a dict 2064 symbols = dict(list(zip(symbols, list(range(1, len(symbols) + 1))))) 2065 2066 def append_symbol(arg, symbols): 2067 if isinstance(arg, Not): 2068 return -symbols[arg.args[0]] 2069 else: 2070 return symbols[arg] 2071 2072 return [{append_symbol(arg, symbols) for arg in Or.make_args(c)} 2073 for c in clauses] 2074 2075 2076def term_to_integer(term): 2077 """ 2078 Return an integer corresponding to the base-2 digits given by ``term``. 2079 2080 Parameters 2081 ========== 2082 2083 term : a string or list of ones and zeros 2084 2085 Examples 2086 ======== 2087 2088 >>> from sympy.logic.boolalg import term_to_integer 2089 >>> term_to_integer([1, 0, 0]) 2090 4 2091 >>> term_to_integer('100') 2092 4 2093 2094 """ 2095 2096 return int(''.join(list(map(str, list(term)))), 2) 2097 2098 2099def integer_to_term(k, n_bits=None): 2100 """ 2101 Return a list of the base-2 digits in the integer, ``k``. 2102 2103 Parameters 2104 ========== 2105 2106 k : int 2107 n_bits : int 2108 If ``n_bits`` is given and the number of digits in the binary 2109 representation of ``k`` is smaller than ``n_bits`` then left-pad the 2110 list with 0s. 2111 2112 Examples 2113 ======== 2114 2115 >>> from sympy.logic.boolalg import integer_to_term 2116 >>> integer_to_term(4) 2117 [1, 0, 0] 2118 >>> integer_to_term(4, 6) 2119 [0, 0, 0, 1, 0, 0] 2120 """ 2121 2122 s = '{0:0{1}b}'.format(abs(as_int(k)), as_int(abs(n_bits or 0))) 2123 return list(map(int, s)) 2124 2125 2126def truth_table(expr, variables, input=True): 2127 """ 2128 Return a generator of all possible configurations of the input variables, 2129 and the result of the boolean expression for those values. 2130 2131 Parameters 2132 ========== 2133 2134 expr : string or boolean expression 2135 variables : list of variables 2136 input : boolean (default True) 2137 indicates whether to return the input combinations. 2138 2139 Examples 2140 ======== 2141 2142 >>> from sympy.logic.boolalg import truth_table 2143 >>> from sympy.abc import x,y 2144 >>> table = truth_table(x >> y, [x, y]) 2145 >>> for t in table: 2146 ... print('{0} -> {1}'.format(*t)) 2147 [0, 0] -> True 2148 [0, 1] -> True 2149 [1, 0] -> False 2150 [1, 1] -> True 2151 2152 >>> table = truth_table(x | y, [x, y]) 2153 >>> list(table) 2154 [([0, 0], False), ([0, 1], True), ([1, 0], True), ([1, 1], True)] 2155 2156 If input is false, truth_table returns only a list of truth values. 2157 In this case, the corresponding input values of variables can be 2158 deduced from the index of a given output. 2159 2160 >>> from sympy.logic.boolalg import integer_to_term 2161 >>> vars = [y, x] 2162 >>> values = truth_table(x >> y, vars, input=False) 2163 >>> values = list(values) 2164 >>> values 2165 [True, False, True, True] 2166 2167 >>> for i, value in enumerate(values): 2168 ... print('{0} -> {1}'.format(list(zip( 2169 ... vars, integer_to_term(i, len(vars)))), value)) 2170 [(y, 0), (x, 0)] -> True 2171 [(y, 0), (x, 1)] -> False 2172 [(y, 1), (x, 0)] -> True 2173 [(y, 1), (x, 1)] -> True 2174 2175 """ 2176 variables = [sympify(v) for v in variables] 2177 2178 expr = sympify(expr) 2179 if not isinstance(expr, BooleanFunction) and not is_literal(expr): 2180 return 2181 2182 table = product((0, 1), repeat=len(variables)) 2183 for term in table: 2184 term = list(term) 2185 value = expr.xreplace(dict(zip(variables, term))) 2186 2187 if input: 2188 yield term, value 2189 else: 2190 yield value 2191 2192 2193def _check_pair(minterm1, minterm2): 2194 """ 2195 Checks if a pair of minterms differs by only one bit. If yes, returns 2196 index, else returns -1. 2197 """ 2198 # Early termination seems to be faster than list comprehension, 2199 # at least for large examples. 2200 index = -1 2201 for x, i in enumerate(minterm1): # zip(minterm1, minterm2) is slower 2202 if i != minterm2[x]: 2203 if index == -1: 2204 index = x 2205 else: 2206 return -1 2207 return index 2208 2209 2210def _convert_to_varsSOP(minterm, variables): 2211 """ 2212 Converts a term in the expansion of a function from binary to its 2213 variable form (for SOP). 2214 """ 2215 temp = [variables[n] if val == 1 else Not(variables[n]) 2216 for n, val in enumerate(minterm) if val != 3] 2217 return And(*temp) 2218 2219 2220def _convert_to_varsPOS(maxterm, variables): 2221 """ 2222 Converts a term in the expansion of a function from binary to its 2223 variable form (for POS). 2224 """ 2225 temp = [variables[n] if val == 0 else Not(variables[n]) 2226 for n, val in enumerate(maxterm) if val != 3] 2227 return Or(*temp) 2228 2229 2230def _convert_to_varsANF(term, variables): 2231 """ 2232 Converts a term in the expansion of a function from binary to it's 2233 variable form (for ANF). 2234 2235 Parameters 2236 ========== 2237 2238 term : list of 1's and 0's (complementation patter) 2239 variables : list of variables 2240 2241 """ 2242 temp = [variables[n] for n, t in enumerate(term) if t == 1] 2243 2244 if not temp: 2245 return true 2246 2247 return And(*temp) 2248 2249 2250def _get_odd_parity_terms(n): 2251 """ 2252 Returns a list of lists, with all possible combinations of n zeros and ones 2253 with an odd number of ones. 2254 """ 2255 return [e for e in [ibin(i, n) for i in range(2**n)] if sum(e) % 2 == 1] 2256 2257 2258def _get_even_parity_terms(n): 2259 """ 2260 Returns a list of lists, with all possible combinations of n zeros and ones 2261 with an even number of ones. 2262 """ 2263 return [e for e in [ibin(i, n) for i in range(2**n)] if sum(e) % 2 == 0] 2264 2265 2266def _simplified_pairs(terms): 2267 """ 2268 Reduces a set of minterms, if possible, to a simplified set of minterms 2269 with one less variable in the terms using QM method. 2270 """ 2271 if not terms: 2272 return [] 2273 2274 simplified_terms = [] 2275 todo = list(range(len(terms))) 2276 2277 # Count number of ones as _check_pair can only potentially match if there 2278 # is at most a difference of a single one 2279 termdict = defaultdict(list) 2280 for n, term in enumerate(terms): 2281 ones = sum([1 for t in term if t == 1]) 2282 termdict[ones].append(n) 2283 2284 variables = len(terms[0]) 2285 for k in range(variables): 2286 for i in termdict[k]: 2287 for j in termdict[k+1]: 2288 index = _check_pair(terms[i], terms[j]) 2289 if index != -1: 2290 # Mark terms handled 2291 todo[i] = todo[j] = None 2292 # Copy old term 2293 newterm = terms[i][:] 2294 # Set differing position to don't care 2295 newterm[index] = 3 2296 # Add if not already there 2297 if newterm not in simplified_terms: 2298 simplified_terms.append(newterm) 2299 2300 if simplified_terms: 2301 # Further simplifications only among the new terms 2302 simplified_terms = _simplified_pairs(simplified_terms) 2303 2304 # Add remaining, non-simplified, terms 2305 simplified_terms.extend([terms[i] for i in todo if i is not None]) 2306 return simplified_terms 2307 2308 2309def _rem_redundancy(l1, terms): 2310 """ 2311 After the truth table has been sufficiently simplified, use the prime 2312 implicant table method to recognize and eliminate redundant pairs, 2313 and return the essential arguments. 2314 """ 2315 2316 if not terms: 2317 return [] 2318 2319 nterms = len(terms) 2320 nl1 = len(l1) 2321 2322 # Create dominating matrix 2323 dommatrix = [[0]*nl1 for n in range(nterms)] 2324 colcount = [0]*nl1 2325 rowcount = [0]*nterms 2326 for primei, prime in enumerate(l1): 2327 for termi, term in enumerate(terms): 2328 # Check prime implicant covering term 2329 if all(t == 3 or t == mt for t, mt in zip(prime, term)): 2330 dommatrix[termi][primei] = 1 2331 colcount[primei] += 1 2332 rowcount[termi] += 1 2333 2334 # Keep track if anything changed 2335 anythingchanged = True 2336 # Then, go again 2337 while anythingchanged: 2338 anythingchanged = False 2339 2340 for rowi in range(nterms): 2341 # Still non-dominated? 2342 if rowcount[rowi]: 2343 row = dommatrix[rowi] 2344 for row2i in range(nterms): 2345 # Still non-dominated? 2346 if rowi != row2i and rowcount[rowi] and (rowcount[rowi] <= rowcount[row2i]): 2347 row2 = dommatrix[row2i] 2348 if all(row2[n] >= row[n] for n in range(nl1)): 2349 # row2 dominating row, remove row2 2350 rowcount[row2i] = 0 2351 anythingchanged = True 2352 for primei, prime in enumerate(row2): 2353 if prime: 2354 # Make corresponding entry 0 2355 dommatrix[row2i][primei] = 0 2356 colcount[primei] -= 1 2357 2358 colcache = dict() 2359 2360 for coli in range(nl1): 2361 # Still non-dominated? 2362 if colcount[coli]: 2363 if coli in colcache: 2364 col = colcache[coli] 2365 else: 2366 col = [dommatrix[i][coli] for i in range(nterms)] 2367 colcache[coli] = col 2368 for col2i in range(nl1): 2369 # Still non-dominated? 2370 if coli != col2i and colcount[col2i] and (colcount[coli] >= colcount[col2i]): 2371 if col2i in colcache: 2372 col2 = colcache[col2i] 2373 else: 2374 col2 = [dommatrix[i][col2i] for i in range(nterms)] 2375 colcache[col2i] = col2 2376 if all(col[n] >= col2[n] for n in range(nterms)): 2377 # col dominating col2, remove col2 2378 colcount[col2i] = 0 2379 anythingchanged = True 2380 for termi, term in enumerate(col2): 2381 if term and dommatrix[termi][col2i]: 2382 # Make corresponding entry 0 2383 dommatrix[termi][col2i] = 0 2384 rowcount[termi] -= 1 2385 2386 if not anythingchanged: 2387 # Heuristically select the prime implicant covering most terms 2388 maxterms = 0 2389 bestcolidx = -1 2390 for coli in range(nl1): 2391 s = colcount[coli] 2392 if s > maxterms: 2393 bestcolidx = coli 2394 maxterms = s 2395 2396 # In case we found a prime implicant covering at least two terms 2397 if bestcolidx != -1 and maxterms > 1: 2398 for primei, prime in enumerate(l1): 2399 if primei != bestcolidx: 2400 for termi, term in enumerate(colcache[bestcolidx]): 2401 if term and dommatrix[termi][primei]: 2402 # Make corresponding entry 0 2403 dommatrix[termi][primei] = 0 2404 anythingchanged = True 2405 rowcount[termi] -= 1 2406 colcount[primei] -= 1 2407 2408 return [l1[i] for i in range(nl1) if colcount[i]] 2409 2410 2411def _input_to_binlist(inputlist, variables): 2412 binlist = [] 2413 bits = len(variables) 2414 for val in inputlist: 2415 if isinstance(val, int): 2416 binlist.append(ibin(val, bits)) 2417 elif isinstance(val, dict): 2418 nonspecvars = list(variables) 2419 for key in val.keys(): 2420 nonspecvars.remove(key) 2421 for t in product((0, 1), repeat=len(nonspecvars)): 2422 d = dict(zip(nonspecvars, t)) 2423 d.update(val) 2424 binlist.append([d[v] for v in variables]) 2425 elif isinstance(val, (list, tuple)): 2426 if len(val) != bits: 2427 raise ValueError("Each term must contain {bits} bits as there are" 2428 "\n{bits} variables (or be an integer)." 2429 "".format(bits=bits)) 2430 binlist.append(list(val)) 2431 else: 2432 raise TypeError("A term list can only contain lists," 2433 " ints or dicts.") 2434 return binlist 2435 2436 2437def SOPform(variables, minterms, dontcares=None): 2438 """ 2439 The SOPform function uses simplified_pairs and a redundant group- 2440 eliminating algorithm to convert the list of all input combos that 2441 generate '1' (the minterms) into the smallest Sum of Products form. 2442 2443 The variables must be given as the first argument. 2444 2445 Return a logical Or function (i.e., the "sum of products" or "SOP" 2446 form) that gives the desired outcome. If there are inputs that can 2447 be ignored, pass them as a list, too. 2448 2449 The result will be one of the (perhaps many) functions that satisfy 2450 the conditions. 2451 2452 Examples 2453 ======== 2454 2455 >>> from sympy.logic import SOPform 2456 >>> from sympy import symbols 2457 >>> w, x, y, z = symbols('w x y z') 2458 >>> minterms = [[0, 0, 0, 1], [0, 0, 1, 1], 2459 ... [0, 1, 1, 1], [1, 0, 1, 1], [1, 1, 1, 1]] 2460 >>> dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]] 2461 >>> SOPform([w, x, y, z], minterms, dontcares) 2462 (y & z) | (~w & ~x) 2463 2464 The terms can also be represented as integers: 2465 2466 >>> minterms = [1, 3, 7, 11, 15] 2467 >>> dontcares = [0, 2, 5] 2468 >>> SOPform([w, x, y, z], minterms, dontcares) 2469 (y & z) | (~w & ~x) 2470 2471 They can also be specified using dicts, which does not have to be fully 2472 specified: 2473 2474 >>> minterms = [{w: 0, x: 1}, {y: 1, z: 1, x: 0}] 2475 >>> SOPform([w, x, y, z], minterms) 2476 (x & ~w) | (y & z & ~x) 2477 2478 Or a combination: 2479 2480 >>> minterms = [4, 7, 11, [1, 1, 1, 1]] 2481 >>> dontcares = [{w : 0, x : 0, y: 0}, 5] 2482 >>> SOPform([w, x, y, z], minterms, dontcares) 2483 (w & y & z) | (~w & ~y) | (x & z & ~w) 2484 2485 References 2486 ========== 2487 2488 .. [1] https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm 2489 2490 """ 2491 if minterms == []: 2492 return false 2493 2494 variables = tuple(map(sympify, variables)) 2495 2496 2497 minterms = _input_to_binlist(minterms, variables) 2498 dontcares = _input_to_binlist((dontcares or []), variables) 2499 for d in dontcares: 2500 if d in minterms: 2501 raise ValueError('%s in minterms is also in dontcares' % d) 2502 2503 new = _simplified_pairs(minterms + dontcares) 2504 essential = _rem_redundancy(new, minterms) 2505 return Or(*[_convert_to_varsSOP(x, variables) for x in essential]) 2506 2507 2508def POSform(variables, minterms, dontcares=None): 2509 """ 2510 The POSform function uses simplified_pairs and a redundant-group 2511 eliminating algorithm to convert the list of all input combinations 2512 that generate '1' (the minterms) into the smallest Product of Sums form. 2513 2514 The variables must be given as the first argument. 2515 2516 Return a logical And function (i.e., the "product of sums" or "POS" 2517 form) that gives the desired outcome. If there are inputs that can 2518 be ignored, pass them as a list, too. 2519 2520 The result will be one of the (perhaps many) functions that satisfy 2521 the conditions. 2522 2523 Examples 2524 ======== 2525 2526 >>> from sympy.logic import POSform 2527 >>> from sympy import symbols 2528 >>> w, x, y, z = symbols('w x y z') 2529 >>> minterms = [[0, 0, 0, 1], [0, 0, 1, 1], [0, 1, 1, 1], 2530 ... [1, 0, 1, 1], [1, 1, 1, 1]] 2531 >>> dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]] 2532 >>> POSform([w, x, y, z], minterms, dontcares) 2533 z & (y | ~w) 2534 2535 The terms can also be represented as integers: 2536 2537 >>> minterms = [1, 3, 7, 11, 15] 2538 >>> dontcares = [0, 2, 5] 2539 >>> POSform([w, x, y, z], minterms, dontcares) 2540 z & (y | ~w) 2541 2542 They can also be specified using dicts, which does not have to be fully 2543 specified: 2544 2545 >>> minterms = [{w: 0, x: 1}, {y: 1, z: 1, x: 0}] 2546 >>> POSform([w, x, y, z], minterms) 2547 (x | y) & (x | z) & (~w | ~x) 2548 2549 Or a combination: 2550 2551 >>> minterms = [4, 7, 11, [1, 1, 1, 1]] 2552 >>> dontcares = [{w : 0, x : 0, y: 0}, 5] 2553 >>> POSform([w, x, y, z], minterms, dontcares) 2554 (w | x) & (y | ~w) & (z | ~y) 2555 2556 2557 References 2558 ========== 2559 2560 .. [1] https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm 2561 2562 """ 2563 if minterms == []: 2564 return false 2565 2566 variables = tuple(map(sympify, variables)) 2567 minterms = _input_to_binlist(minterms, variables) 2568 dontcares = _input_to_binlist((dontcares or []), variables) 2569 for d in dontcares: 2570 if d in minterms: 2571 raise ValueError('%s in minterms is also in dontcares' % d) 2572 2573 maxterms = [] 2574 for t in product((0, 1), repeat=len(variables)): 2575 t = list(t) 2576 if (t not in minterms) and (t not in dontcares): 2577 maxterms.append(t) 2578 2579 new = _simplified_pairs(maxterms + dontcares) 2580 essential = _rem_redundancy(new, maxterms) 2581 return And(*[_convert_to_varsPOS(x, variables) for x in essential]) 2582 2583 2584def ANFform(variables, truthvalues): 2585 """ 2586 The ANFform function converts the list of truth values to 2587 Algebraic Normal Form (ANF). 2588 2589 The variables must be given as the first argument. 2590 2591 Return True, False, logical And funciton (i.e., the 2592 "Zhegalkin monomial") or logical Xor function (i.e., 2593 the "Zhegalkin polynomial"). When True and False 2594 are represented by 1 and 0, respectively, then 2595 And is multiplication and Xor is addition. 2596 2597 Formally a "Zhegalkin monomial" is the product (logical 2598 And) of a finite set of distinct variables, including 2599 the empty set whose product is denoted 1 (True). 2600 A "Zhegalkin polynomial" is the sum (logical Xor) of a 2601 set of Zhegalkin monomials, with the empty set denoted 2602 by 0 (False). 2603 2604 Parameters 2605 ========== 2606 2607 variables : list of variables 2608 truthvalues : list of 1's and 0's (result column of truth table) 2609 2610 Examples 2611 ======== 2612 >>> from sympy.logic.boolalg import ANFform 2613 >>> from sympy.abc import x, y 2614 >>> ANFform([x], [1, 0]) 2615 x ^ True 2616 >>> ANFform([x, y], [0, 1, 1, 1]) 2617 x ^ y ^ (x & y) 2618 2619 References 2620 ========== 2621 2622 .. [2] https://en.wikipedia.org/wiki/Zhegalkin_polynomial 2623 2624 """ 2625 2626 n_vars = len(variables) 2627 n_values = len(truthvalues) 2628 2629 if n_values != 2 ** n_vars: 2630 raise ValueError("The number of truth values must be equal to 2^%d, " 2631 "got %d" % (n_vars, n_values)) 2632 2633 variables = tuple(map(sympify, variables)) 2634 2635 coeffs = anf_coeffs(truthvalues) 2636 terms = [] 2637 2638 for i, t in enumerate(product((0, 1), repeat=n_vars)): 2639 if coeffs[i] == 1: 2640 terms.append(t) 2641 2642 return Xor(*[_convert_to_varsANF(x, variables) for x in terms], 2643 remove_true=False) 2644 2645 2646def anf_coeffs(truthvalues): 2647 """ 2648 Convert a list of truth values of some boolean expression 2649 to the list of coefficients of the polynomial mod 2 (exclusive 2650 disjunction) representing the boolean expression in ANF 2651 (i.e., the "Zhegalkin polynomial"). 2652 2653 There are 2^n possible Zhegalkin monomials in n variables, since 2654 each monomial is fully specified by the presence or absence of 2655 each variable. 2656 2657 We can enumerate all the monomials. For example, boolean 2658 function with four variables (a, b, c, d) can contain 2659 up to 2^4 = 16 monomials. The 13-th monomial is the 2660 product a & b & d, because 13 in binary is 1, 1, 0, 1. 2661 2662 A given monomial's presence or absence in a polynomial corresponds 2663 to that monomial's coefficient being 1 or 0 respectively. 2664 2665 Examples 2666 ======== 2667 >>> from sympy.logic.boolalg import anf_coeffs, bool_monomial, Xor 2668 >>> from sympy.abc import a, b, c 2669 >>> truthvalues = [0, 1, 1, 0, 0, 1, 0, 1] 2670 >>> coeffs = anf_coeffs(truthvalues) 2671 >>> coeffs 2672 [0, 1, 1, 0, 0, 0, 1, 0] 2673 >>> polynomial = Xor(*[ 2674 ... bool_monomial(k, [a, b, c]) 2675 ... for k, coeff in enumerate(coeffs) if coeff == 1 2676 ... ]) 2677 >>> polynomial 2678 b ^ c ^ (a & b) 2679 2680 """ 2681 2682 s = '{:b}'.format(len(truthvalues)) 2683 n = len(s) - 1 2684 2685 if len(truthvalues) != 2**n: 2686 raise ValueError("The number of truth values must be a power of two, " 2687 "got %d" % len(truthvalues)) 2688 2689 coeffs = [[v] for v in truthvalues] 2690 2691 for i in range(n): 2692 tmp = [] 2693 for j in range(2 ** (n-i-1)): 2694 tmp.append(coeffs[2*j] + 2695 list(map(lambda x, y: x^y, coeffs[2*j], coeffs[2*j+1]))) 2696 coeffs = tmp 2697 2698 return coeffs[0] 2699 2700 2701def bool_minterm(k, variables): 2702 """ 2703 Return the k-th minterm. 2704 2705 Minterms are numbered by a binary encoding of the complementation 2706 pattern of the variables. This convention assigns the value 1 to 2707 the direct form and 0 to the complemented form. 2708 2709 Parameters 2710 ========== 2711 2712 k : int or list of 1's and 0's (complementation patter) 2713 variables : list of variables 2714 2715 Examples 2716 ======== 2717 >>> from sympy.logic.boolalg import bool_minterm 2718 >>> from sympy.abc import x, y, z 2719 >>> bool_minterm([1, 0, 1], [x, y, z]) 2720 x & z & ~y 2721 >>> bool_minterm(6, [x, y, z]) 2722 x & y & ~z 2723 2724 References 2725 ========== 2726 2727 .. [3] https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_minterms 2728 2729 """ 2730 if isinstance(k, int): 2731 k = integer_to_term(k, len(variables)) 2732 variables = tuple(map(sympify, variables)) 2733 return _convert_to_varsSOP(k, variables) 2734 2735 2736def bool_maxterm(k, variables): 2737 """ 2738 Return the k-th maxterm. 2739 2740 Each maxterm is assigned an index based on the opposite 2741 conventional binary encoding used for minterms. The maxterm 2742 convention assigns the value 0 to the direct form and 1 to 2743 the complemented form. 2744 2745 Parameters 2746 ========== 2747 2748 k : int or list of 1's and 0's (complementation pattern) 2749 variables : list of variables 2750 2751 Examples 2752 ======== 2753 >>> from sympy.logic.boolalg import bool_maxterm 2754 >>> from sympy.abc import x, y, z 2755 >>> bool_maxterm([1, 0, 1], [x, y, z]) 2756 y | ~x | ~z 2757 >>> bool_maxterm(6, [x, y, z]) 2758 z | ~x | ~y 2759 2760 References 2761 ========== 2762 2763 .. [4] https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_maxterms 2764 2765 """ 2766 if isinstance(k, int): 2767 k = integer_to_term(k, len(variables)) 2768 variables = tuple(map(sympify, variables)) 2769 return _convert_to_varsPOS(k, variables) 2770 2771 2772def bool_monomial(k, variables): 2773 """ 2774 Return the k-th monomial. 2775 2776 Monomials are numbered by a binary encoding of the presence and 2777 absences of the variables. This convention assigns the value 2778 1 to the presence of variable and 0 to the absence of variable. 2779 2780 Each boolean function can be uniquely represented by a 2781 Zhegalkin Polynomial (Algebraic Normal Form). The Zhegalkin 2782 Polynomial of the boolean function with n variables can contain 2783 up to 2^n monomials. We can enumarate all the monomials. 2784 Each monomial is fully specified by the presence or absence 2785 of each variable. 2786 2787 For example, boolean function with four variables (a, b, c, d) 2788 can contain up to 2^4 = 16 monomials. The 13-th monomial is the 2789 product a & b & d, because 13 in binary is 1, 1, 0, 1. 2790 2791 Parameters 2792 ========== 2793 2794 k : int or list of 1's and 0's 2795 variables : list of variables 2796 2797 Examples 2798 ======== 2799 >>> from sympy.logic.boolalg import bool_monomial 2800 >>> from sympy.abc import x, y, z 2801 >>> bool_monomial([1, 0, 1], [x, y, z]) 2802 x & z 2803 >>> bool_monomial(6, [x, y, z]) 2804 x & y 2805 2806 """ 2807 if isinstance(k, int): 2808 k = integer_to_term(k, len(variables)) 2809 variables = tuple(map(sympify, variables)) 2810 return _convert_to_varsANF(k, variables) 2811 2812 2813def _find_predicates(expr): 2814 """Helper to find logical predicates in BooleanFunctions. 2815 2816 A logical predicate is defined here as anything within a BooleanFunction 2817 that is not a BooleanFunction itself. 2818 2819 """ 2820 if not isinstance(expr, BooleanFunction): 2821 return {expr} 2822 return set().union(*(map(_find_predicates, expr.args))) 2823 2824 2825def simplify_logic(expr, form=None, deep=True, force=False): 2826 """ 2827 This function simplifies a boolean function to its simplified version 2828 in SOP or POS form. The return type is an Or or And object in SymPy. 2829 2830 Parameters 2831 ========== 2832 2833 expr : string or boolean expression 2834 2835 form : string ('cnf' or 'dnf') or None (default). 2836 If 'cnf' or 'dnf', the simplest expression in the corresponding 2837 normal form is returned; if None, the answer is returned 2838 according to the form with fewest args (in CNF by default). 2839 2840 deep : boolean (default True) 2841 Indicates whether to recursively simplify any 2842 non-boolean functions contained within the input. 2843 2844 force : boolean (default False) 2845 As the simplifications require exponential time in the number 2846 of variables, there is by default a limit on expressions with 2847 8 variables. When the expression has more than 8 variables 2848 only symbolical simplification (controlled by ``deep``) is 2849 made. By setting force to ``True``, this limit is removed. Be 2850 aware that this can lead to very long simplification times. 2851 2852 Examples 2853 ======== 2854 2855 >>> from sympy.logic import simplify_logic 2856 >>> from sympy.abc import x, y, z 2857 >>> from sympy import S 2858 >>> b = (~x & ~y & ~z) | ( ~x & ~y & z) 2859 >>> simplify_logic(b) 2860 ~x & ~y 2861 2862 >>> S(b) 2863 (z & ~x & ~y) | (~x & ~y & ~z) 2864 >>> simplify_logic(_) 2865 ~x & ~y 2866 2867 """ 2868 2869 if form not in (None, 'cnf', 'dnf'): 2870 raise ValueError("form can be cnf or dnf only") 2871 expr = sympify(expr) 2872 # check for quick exit if form is given: right form and all args are 2873 # literal and do not involve Not 2874 if form: 2875 form_ok = False 2876 if form == 'cnf': 2877 form_ok = is_cnf(expr) 2878 elif form == 'dnf': 2879 form_ok = is_dnf(expr) 2880 2881 if form_ok and all(is_literal(a) 2882 for a in expr.args): 2883 return expr 2884 if deep: 2885 variables = _find_predicates(expr) 2886 from sympy.simplify.simplify import simplify 2887 s = tuple(map(simplify, variables)) 2888 expr = expr.xreplace(dict(zip(variables, s))) 2889 if not isinstance(expr, BooleanFunction): 2890 return expr 2891 # get variables in case not deep or after doing 2892 # deep simplification since they may have changed 2893 variables = _find_predicates(expr) 2894 if not force and len(variables) > 8: 2895 return expr 2896 # group into constants and variable values 2897 c, v = sift(ordered(variables), lambda x: x in (True, False), binary=True) 2898 variables = c + v 2899 truthtable = [] 2900 # standardize constants to be 1 or 0 in keeping with truthtable 2901 c = [1 if i == True else 0 for i in c] 2902 for t in product((0, 1), repeat=len(v)): 2903 if expr.xreplace(dict(zip(v, t))) == True: 2904 truthtable.append(c + list(t)) 2905 big = len(truthtable) >= (2 ** (len(variables) - 1)) 2906 if form == 'dnf' or form is None and big: 2907 return SOPform(variables, truthtable) 2908 return POSform(variables, truthtable) 2909 2910 2911def _finger(eq): 2912 """ 2913 Assign a 5-item fingerprint to each symbol in the equation: 2914 [ 2915 # of times it appeared as a Symbol; 2916 # of times it appeared as a Not(symbol); 2917 # of times it appeared as a Symbol in an And or Or; 2918 # of times it appeared as a Not(Symbol) in an And or Or; 2919 a sorted tuple of tuples, (i, j, k), where i is the number of arguments 2920 in an And or Or with which it appeared as a Symbol, and j is 2921 the number of arguments that were Not(Symbol); k is the number 2922 of times that (i, j) was seen. 2923 ] 2924 2925 Examples 2926 ======== 2927 2928 >>> from sympy.logic.boolalg import _finger as finger 2929 >>> from sympy import And, Or, Not, Xor, to_cnf, symbols 2930 >>> from sympy.abc import a, b, x, y 2931 >>> eq = Or(And(Not(y), a), And(Not(y), b), And(x, y)) 2932 >>> dict(finger(eq)) 2933 {(0, 0, 1, 0, ((2, 0, 1),)): [x], 2934 (0, 0, 1, 0, ((2, 1, 1),)): [a, b], 2935 (0, 0, 1, 2, ((2, 0, 1),)): [y]} 2936 >>> dict(finger(x & ~y)) 2937 {(0, 1, 0, 0, ()): [y], (1, 0, 0, 0, ()): [x]} 2938 2939 In the following, the (5, 2, 6) means that there were 6 Or 2940 functions in which a symbol appeared as itself amongst 5 arguments in 2941 which there were also 2 negated symbols, e.g. ``(a0 | a1 | a2 | ~a3 | ~a4)`` 2942 is counted once for a0, a1 and a2. 2943 2944 >>> dict(finger(to_cnf(Xor(*symbols('a:5'))))) 2945 {(0, 0, 8, 8, ((5, 0, 1), (5, 2, 6), (5, 4, 1))): [a0, a1, a2, a3, a4]} 2946 2947 The equation must not have more than one level of nesting: 2948 2949 >>> dict(finger(And(Or(x, y), y))) 2950 {(0, 0, 1, 0, ((2, 0, 1),)): [x], (1, 0, 1, 0, ((2, 0, 1),)): [y]} 2951 >>> dict(finger(And(Or(x, And(a, x)), y))) 2952 Traceback (most recent call last): 2953 ... 2954 NotImplementedError: unexpected level of nesting 2955 2956 So y and x have unique fingerprints, but a and b do not. 2957 """ 2958 f = eq.free_symbols 2959 d = dict(list(zip(f, [[0]*4 + [defaultdict(int)] for fi in f]))) 2960 for a in eq.args: 2961 if a.is_Symbol: 2962 d[a][0] += 1 2963 elif a.is_Not: 2964 d[a.args[0]][1] += 1 2965 else: 2966 o = len(a.args), sum(isinstance(ai, Not) for ai in a.args) 2967 for ai in a.args: 2968 if ai.is_Symbol: 2969 d[ai][2] += 1 2970 d[ai][-1][o] += 1 2971 elif ai.is_Not: 2972 d[ai.args[0]][3] += 1 2973 else: 2974 raise NotImplementedError('unexpected level of nesting') 2975 inv = defaultdict(list) 2976 for k, v in ordered(iter(d.items())): 2977 v[-1] = tuple(sorted([i + (j,) for i, j in v[-1].items()])) 2978 inv[tuple(v)].append(k) 2979 return inv 2980 2981 2982def bool_map(bool1, bool2): 2983 """ 2984 Return the simplified version of bool1, and the mapping of variables 2985 that makes the two expressions bool1 and bool2 represent the same 2986 logical behaviour for some correspondence between the variables 2987 of each. 2988 If more than one mappings of this sort exist, one of them 2989 is returned. 2990 For example, And(x, y) is logically equivalent to And(a, b) for 2991 the mapping {x: a, y:b} or {x: b, y:a}. 2992 If no such mapping exists, return False. 2993 2994 Examples 2995 ======== 2996 2997 >>> from sympy import SOPform, bool_map, Or, And, Not, Xor 2998 >>> from sympy.abc import w, x, y, z, a, b, c, d 2999 >>> function1 = SOPform([x, z, y],[[1, 0, 1], [0, 0, 1]]) 3000 >>> function2 = SOPform([a, b, c],[[1, 0, 1], [1, 0, 0]]) 3001 >>> bool_map(function1, function2) 3002 (y & ~z, {y: a, z: b}) 3003 3004 The results are not necessarily unique, but they are canonical. Here, 3005 ``(w, z)`` could be ``(a, d)`` or ``(d, a)``: 3006 3007 >>> eq = Or(And(Not(y), w), And(Not(y), z), And(x, y)) 3008 >>> eq2 = Or(And(Not(c), a), And(Not(c), d), And(b, c)) 3009 >>> bool_map(eq, eq2) 3010 ((x & y) | (w & ~y) | (z & ~y), {w: a, x: b, y: c, z: d}) 3011 >>> eq = And(Xor(a, b), c, And(c,d)) 3012 >>> bool_map(eq, eq.subs(c, x)) 3013 (c & d & (a | b) & (~a | ~b), {a: a, b: b, c: d, d: x}) 3014 3015 """ 3016 3017 def match(function1, function2): 3018 """Return the mapping that equates variables between two 3019 simplified boolean expressions if possible. 3020 3021 By "simplified" we mean that a function has been denested 3022 and is either an And (or an Or) whose arguments are either 3023 symbols (x), negated symbols (Not(x)), or Or (or an And) whose 3024 arguments are only symbols or negated symbols. For example, 3025 And(x, Not(y), Or(w, Not(z))). 3026 3027 Basic.match is not robust enough (see issue 4835) so this is 3028 a workaround that is valid for simplified boolean expressions 3029 """ 3030 3031 # do some quick checks 3032 if function1.__class__ != function2.__class__: 3033 return None # maybe simplification makes them the same? 3034 if len(function1.args) != len(function2.args): 3035 return None # maybe simplification makes them the same? 3036 if function1.is_Symbol: 3037 return {function1: function2} 3038 3039 # get the fingerprint dictionaries 3040 f1 = _finger(function1) 3041 f2 = _finger(function2) 3042 3043 # more quick checks 3044 if len(f1) != len(f2): 3045 return False 3046 3047 # assemble the match dictionary if possible 3048 matchdict = {} 3049 for k in f1.keys(): 3050 if k not in f2: 3051 return False 3052 if len(f1[k]) != len(f2[k]): 3053 return False 3054 for i, x in enumerate(f1[k]): 3055 matchdict[x] = f2[k][i] 3056 return matchdict 3057 3058 a = simplify_logic(bool1) 3059 b = simplify_logic(bool2) 3060 m = match(a, b) 3061 if m: 3062 return a, m 3063 return m 3064 3065 3066def simplify_patterns_and(): 3067 from sympy.functions.elementary.miscellaneous import Min, Max 3068 from sympy.core import Wild 3069 from sympy.core.relational import Eq, Ne, Ge, Gt, Le, Lt 3070 a = Wild('a') 3071 b = Wild('b') 3072 c = Wild('c') 3073 # With a better canonical fewer results are required 3074 _matchers_and = ((And(Eq(a, b), Ge(a, b)), Eq(a, b)), 3075 (And(Eq(a, b), Gt(a, b)), S.false), 3076 (And(Eq(a, b), Le(a, b)), Eq(a, b)), 3077 (And(Eq(a, b), Lt(a, b)), S.false), 3078 (And(Ge(a, b), Gt(a, b)), Gt(a, b)), 3079 (And(Ge(a, b), Le(a, b)), Eq(a, b)), 3080 (And(Ge(a, b), Lt(a, b)), S.false), 3081 (And(Ge(a, b), Ne(a, b)), Gt(a, b)), 3082 (And(Gt(a, b), Le(a, b)), S.false), 3083 (And(Gt(a, b), Lt(a, b)), S.false), 3084 (And(Gt(a, b), Ne(a, b)), Gt(a, b)), 3085 (And(Le(a, b), Lt(a, b)), Lt(a, b)), 3086 (And(Le(a, b), Ne(a, b)), Lt(a, b)), 3087 (And(Lt(a, b), Ne(a, b)), Lt(a, b)), 3088 # Min/max 3089 (And(Ge(a, b), Ge(a, c)), Ge(a, Max(b, c))), 3090 (And(Ge(a, b), Gt(a, c)), ITE(b > c, Ge(a, b), Gt(a, c))), 3091 (And(Gt(a, b), Gt(a, c)), Gt(a, Max(b, c))), 3092 (And(Le(a, b), Le(a, c)), Le(a, Min(b, c))), 3093 (And(Le(a, b), Lt(a, c)), ITE(b < c, Le(a, b), Lt(a, c))), 3094 (And(Lt(a, b), Lt(a, c)), Lt(a, Min(b, c))), 3095 # Sign 3096 (And(Eq(a, b), Eq(a, -b)), And(Eq(a, S.Zero), Eq(b, S.Zero))), 3097 ) 3098 return _matchers_and 3099 3100 3101def simplify_patterns_or(): 3102 from sympy.functions.elementary.miscellaneous import Min, Max 3103 from sympy.core import Wild 3104 from sympy.core.relational import Eq, Ne, Ge, Gt, Le, Lt 3105 a = Wild('a') 3106 b = Wild('b') 3107 c = Wild('c') 3108 _matchers_or = ((Or(Eq(a, b), Ge(a, b)), Ge(a, b)), 3109 (Or(Eq(a, b), Gt(a, b)), Ge(a, b)), 3110 (Or(Eq(a, b), Le(a, b)), Le(a, b)), 3111 (Or(Eq(a, b), Lt(a, b)), Le(a, b)), 3112 (Or(Ge(a, b), Gt(a, b)), Ge(a, b)), 3113 (Or(Ge(a, b), Le(a, b)), S.true), 3114 (Or(Ge(a, b), Lt(a, b)), S.true), 3115 (Or(Ge(a, b), Ne(a, b)), S.true), 3116 (Or(Gt(a, b), Le(a, b)), S.true), 3117 (Or(Gt(a, b), Lt(a, b)), Ne(a, b)), 3118 (Or(Gt(a, b), Ne(a, b)), Ne(a, b)), 3119 (Or(Le(a, b), Lt(a, b)), Le(a, b)), 3120 (Or(Le(a, b), Ne(a, b)), S.true), 3121 (Or(Lt(a, b), Ne(a, b)), Ne(a, b)), 3122 # Min/max 3123 (Or(Ge(a, b), Ge(a, c)), Ge(a, Min(b, c))), 3124 (Or(Ge(a, b), Gt(a, c)), ITE(b > c, Gt(a, c), Ge(a, b))), 3125 (Or(Gt(a, b), Gt(a, c)), Gt(a, Min(b, c))), 3126 (Or(Le(a, b), Le(a, c)), Le(a, Max(b, c))), 3127 (Or(Le(a, b), Lt(a, c)), ITE(b >= c, Le(a, b), Lt(a, c))), 3128 (Or(Lt(a, b), Lt(a, c)), Lt(a, Max(b, c))), 3129 ) 3130 return _matchers_or 3131 3132def simplify_patterns_xor(): 3133 from sympy.functions.elementary.miscellaneous import Min, Max 3134 from sympy.core import Wild 3135 from sympy.core.relational import Eq, Ne, Ge, Gt, Le, Lt 3136 a = Wild('a') 3137 b = Wild('b') 3138 c = Wild('c') 3139 _matchers_xor = ((Xor(Eq(a, b), Ge(a, b)), Gt(a, b)), 3140 (Xor(Eq(a, b), Gt(a, b)), Ge(a, b)), 3141 (Xor(Eq(a, b), Le(a, b)), Lt(a, b)), 3142 (Xor(Eq(a, b), Lt(a, b)), Le(a, b)), 3143 (Xor(Ge(a, b), Gt(a, b)), Eq(a, b)), 3144 (Xor(Ge(a, b), Le(a, b)), Ne(a, b)), 3145 (Xor(Ge(a, b), Lt(a, b)), S.true), 3146 (Xor(Ge(a, b), Ne(a, b)), Le(a, b)), 3147 (Xor(Gt(a, b), Le(a, b)), S.true), 3148 (Xor(Gt(a, b), Lt(a, b)), Ne(a, b)), 3149 (Xor(Gt(a, b), Ne(a, b)), Lt(a, b)), 3150 (Xor(Le(a, b), Lt(a, b)), Eq(a, b)), 3151 (Xor(Le(a, b), Ne(a, b)), Ge(a, b)), 3152 (Xor(Lt(a, b), Ne(a, b)), Gt(a, b)), 3153 # Min/max 3154 (Xor(Ge(a, b), Ge(a, c)), 3155 And(Ge(a, Min(b, c)), Lt(a, Max(b, c)))), 3156 (Xor(Ge(a, b), Gt(a, c)), 3157 ITE(b > c, And(Gt(a, c), Lt(a, b)), 3158 And(Ge(a, b), Le(a, c)))), 3159 (Xor(Gt(a, b), Gt(a, c)), 3160 And(Gt(a, Min(b, c)), Le(a, Max(b, c)))), 3161 (Xor(Le(a, b), Le(a, c)), 3162 And(Le(a, Max(b, c)), Gt(a, Min(b, c)))), 3163 (Xor(Le(a, b), Lt(a, c)), 3164 ITE(b < c, And(Lt(a, c), Gt(a, b)), 3165 And(Le(a, b), Ge(a, c)))), 3166 (Xor(Lt(a, b), Lt(a, c)), 3167 And(Lt(a, Max(b, c)), Ge(a, Min(b, c)))), 3168 ) 3169 return _matchers_xor 3170