Coverage for /usr/lib/python3/dist-packages/sympy/logic/boolalg.py: 18%
1340 statements
« prev ^ index » next coverage.py v7.9.1, created at 2025-06-14 15:55 +0200
1"""
2Boolean algebra module for SymPy
3"""
5from collections import defaultdict
6from itertools import chain, combinations, product, permutations
7from sympy.core.add import Add
8from sympy.core.basic import Basic
9from sympy.core.cache import cacheit
10from sympy.core.containers import Tuple
11from sympy.core.decorators import sympify_method_args, sympify_return
12from sympy.core.function import Application, Derivative
13from sympy.core.kind import BooleanKind, NumberKind
14from sympy.core.numbers import Number
15from sympy.core.operations import LatticeOp
16from sympy.core.singleton import Singleton, S
17from sympy.core.sorting import ordered
18from sympy.core.sympify import _sympy_converter, _sympify, sympify
19from sympy.utilities.iterables import sift, ibin
20from sympy.utilities.misc import filldedent
23def as_Boolean(e):
24 """Like ``bool``, return the Boolean value of an expression, e,
25 which can be any instance of :py:class:`~.Boolean` or ``bool``.
27 Examples
28 ========
30 >>> from sympy import true, false, nan
31 >>> from sympy.logic.boolalg import as_Boolean
32 >>> from sympy.abc import x
33 >>> as_Boolean(0) is false
34 True
35 >>> as_Boolean(1) is true
36 True
37 >>> as_Boolean(x)
38 x
39 >>> as_Boolean(2)
40 Traceback (most recent call last):
41 ...
42 TypeError: expecting bool or Boolean, not `2`.
43 >>> as_Boolean(nan)
44 Traceback (most recent call last):
45 ...
46 TypeError: expecting bool or Boolean, not `nan`.
48 """
49 from sympy.core.symbol import Symbol
50 if e == True:
51 return true
52 if e == False:
53 return false
54 if isinstance(e, Symbol):
55 z = e.is_zero
56 if z is None:
57 return e
58 return false if z else true
59 if isinstance(e, Boolean):
60 return e
61 raise TypeError('expecting bool or Boolean, not `%s`.' % e)
64@sympify_method_args
65class Boolean(Basic):
66 """A Boolean object is an object for which logic operations make sense."""
68 __slots__ = ()
70 kind = BooleanKind
72 @sympify_return([('other', 'Boolean')], NotImplemented)
73 def __and__(self, other):
74 return And(self, other)
76 __rand__ = __and__
78 @sympify_return([('other', 'Boolean')], NotImplemented)
79 def __or__(self, other):
80 return Or(self, other)
82 __ror__ = __or__
84 def __invert__(self):
85 """Overloading for ~"""
86 return Not(self)
88 @sympify_return([('other', 'Boolean')], NotImplemented)
89 def __rshift__(self, other):
90 return Implies(self, other)
92 @sympify_return([('other', 'Boolean')], NotImplemented)
93 def __lshift__(self, other):
94 return Implies(other, self)
96 __rrshift__ = __lshift__
97 __rlshift__ = __rshift__
99 @sympify_return([('other', 'Boolean')], NotImplemented)
100 def __xor__(self, other):
101 return Xor(self, other)
103 __rxor__ = __xor__
105 def equals(self, other):
106 """
107 Returns ``True`` if the given formulas have the same truth table.
108 For two formulas to be equal they must have the same literals.
110 Examples
111 ========
113 >>> from sympy.abc import A, B, C
114 >>> from sympy import And, Or, Not
115 >>> (A >> B).equals(~B >> ~A)
116 True
117 >>> Not(And(A, B, C)).equals(And(Not(A), Not(B), Not(C)))
118 False
119 >>> Not(And(A, Not(A))).equals(Or(B, Not(B)))
120 False
122 """
123 from sympy.logic.inference import satisfiable
124 from sympy.core.relational import Relational
126 if self.has(Relational) or other.has(Relational):
127 raise NotImplementedError('handling of relationals')
128 return self.atoms() == other.atoms() and \
129 not satisfiable(Not(Equivalent(self, other)))
131 def to_nnf(self, simplify=True):
132 # override where necessary
133 return self
135 def as_set(self):
136 """
137 Rewrites Boolean expression in terms of real sets.
139 Examples
140 ========
142 >>> from sympy import Symbol, Eq, Or, And
143 >>> x = Symbol('x', real=True)
144 >>> Eq(x, 0).as_set()
145 {0}
146 >>> (x > 0).as_set()
147 Interval.open(0, oo)
148 >>> And(-2 < x, x < 2).as_set()
149 Interval.open(-2, 2)
150 >>> Or(x < -2, 2 < x).as_set()
151 Union(Interval.open(-oo, -2), Interval.open(2, oo))
153 """
154 from sympy.calculus.util import periodicity
155 from sympy.core.relational import Relational
157 free = self.free_symbols
158 if len(free) == 1:
159 x = free.pop()
160 if x.kind is NumberKind:
161 reps = {}
162 for r in self.atoms(Relational):
163 if periodicity(r, x) not in (0, None):
164 s = r._eval_as_set()
165 if s in (S.EmptySet, S.UniversalSet, S.Reals):
166 reps[r] = s.as_relational(x)
167 continue
168 raise NotImplementedError(filldedent('''
169 as_set is not implemented for relationals
170 with periodic solutions
171 '''))
172 new = self.subs(reps)
173 if new.func != self.func:
174 return new.as_set() # restart with new obj
175 else:
176 return new._eval_as_set()
178 return self._eval_as_set()
179 else:
180 raise NotImplementedError("Sorry, as_set has not yet been"
181 " implemented for multivariate"
182 " expressions")
184 @property
185 def binary_symbols(self):
186 from sympy.core.relational import Eq, Ne
187 return set().union(*[i.binary_symbols for i in self.args
188 if i.is_Boolean or i.is_Symbol
189 or isinstance(i, (Eq, Ne))])
191 def _eval_refine(self, assumptions):
192 from sympy.assumptions import ask
193 ret = ask(self, assumptions)
194 if ret is True:
195 return true
196 elif ret is False:
197 return false
198 return None
201class BooleanAtom(Boolean):
202 """
203 Base class of :py:class:`~.BooleanTrue` and :py:class:`~.BooleanFalse`.
204 """
205 is_Boolean = True
206 is_Atom = True
207 _op_priority = 11 # higher than Expr
209 def simplify(self, *a, **kw):
210 return self
212 def expand(self, *a, **kw):
213 return self
215 @property
216 def canonical(self):
217 return self
219 def _noop(self, other=None):
220 raise TypeError('BooleanAtom not allowed in this context.')
222 __add__ = _noop
223 __radd__ = _noop
224 __sub__ = _noop
225 __rsub__ = _noop
226 __mul__ = _noop
227 __rmul__ = _noop
228 __pow__ = _noop
229 __rpow__ = _noop
230 __truediv__ = _noop
231 __rtruediv__ = _noop
232 __mod__ = _noop
233 __rmod__ = _noop
234 _eval_power = _noop
236 # /// drop when Py2 is no longer supported
237 def __lt__(self, other):
238 raise TypeError(filldedent('''
239 A Boolean argument can only be used in
240 Eq and Ne; all other relationals expect
241 real expressions.
242 '''))
244 __le__ = __lt__
245 __gt__ = __lt__
246 __ge__ = __lt__
247 # \\\
249 def _eval_simplify(self, **kwargs):
250 return self
253class BooleanTrue(BooleanAtom, metaclass=Singleton):
254 """
255 SymPy version of ``True``, a singleton that can be accessed via ``S.true``.
257 This is the SymPy version of ``True``, for use in the logic module. The
258 primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean
259 operations like ``~`` and ``>>`` will work as expected on this class, whereas with
260 True they act bitwise on 1. Functions in the logic module will return this
261 class when they evaluate to true.
263 Notes
264 =====
266 There is liable to be some confusion as to when ``True`` should
267 be used and when ``S.true`` should be used in various contexts
268 throughout SymPy. An important thing to remember is that
269 ``sympify(True)`` returns ``S.true``. This means that for the most
270 part, you can just use ``True`` and it will automatically be converted
271 to ``S.true`` when necessary, similar to how you can generally use 1
272 instead of ``S.One``.
274 The rule of thumb is:
276 "If the boolean in question can be replaced by an arbitrary symbolic
277 ``Boolean``, like ``Or(x, y)`` or ``x > 1``, use ``S.true``.
278 Otherwise, use ``True``"
280 In other words, use ``S.true`` only on those contexts where the
281 boolean is being used as a symbolic representation of truth.
282 For example, if the object ends up in the ``.args`` of any expression,
283 then it must necessarily be ``S.true`` instead of ``True``, as
284 elements of ``.args`` must be ``Basic``. On the other hand,
285 ``==`` is not a symbolic operation in SymPy, since it always returns
286 ``True`` or ``False``, and does so in terms of structural equality
287 rather than mathematical, so it should return ``True``. The assumptions
288 system should use ``True`` and ``False``. Aside from not satisfying
289 the above rule of thumb, the assumptions system uses a three-valued logic
290 (``True``, ``False``, ``None``), whereas ``S.true`` and ``S.false``
291 represent a two-valued logic. When in doubt, use ``True``.
293 "``S.true == True is True``."
295 While "``S.true is True``" is ``False``, "``S.true == True``"
296 is ``True``, so if there is any doubt over whether a function or
297 expression will return ``S.true`` or ``True``, just use ``==``
298 instead of ``is`` to do the comparison, and it will work in either
299 case. Finally, for boolean flags, it's better to just use ``if x``
300 instead of ``if x is True``. To quote PEP 8:
302 Do not compare boolean values to ``True`` or ``False``
303 using ``==``.
305 * Yes: ``if greeting:``
306 * No: ``if greeting == True:``
307 * Worse: ``if greeting is True:``
309 Examples
310 ========
312 >>> from sympy import sympify, true, false, Or
313 >>> sympify(True)
314 True
315 >>> _ is True, _ is true
316 (False, True)
318 >>> Or(true, false)
319 True
320 >>> _ is true
321 True
323 Python operators give a boolean result for true but a
324 bitwise result for True
326 >>> ~true, ~True
327 (False, -2)
328 >>> true >> true, True >> True
329 (True, 0)
331 Python operators give a boolean result for true but a
332 bitwise result for True
334 >>> ~true, ~True
335 (False, -2)
336 >>> true >> true, True >> True
337 (True, 0)
339 See Also
340 ========
342 sympy.logic.boolalg.BooleanFalse
344 """
345 def __bool__(self):
346 return True
348 def __hash__(self):
349 return hash(True)
351 def __eq__(self, other):
352 if other is True:
353 return True
354 if other is False:
355 return False
356 return super().__eq__(other)
358 @property
359 def negated(self):
360 return false
362 def as_set(self):
363 """
364 Rewrite logic operators and relationals in terms of real sets.
366 Examples
367 ========
369 >>> from sympy import true
370 >>> true.as_set()
371 UniversalSet
373 """
374 return S.UniversalSet
377class BooleanFalse(BooleanAtom, metaclass=Singleton):
378 """
379 SymPy version of ``False``, a singleton that can be accessed via ``S.false``.
381 This is the SymPy version of ``False``, for use in the logic module. The
382 primary advantage of using ``false`` instead of ``False`` is that shorthand
383 Boolean operations like ``~`` and ``>>`` will work as expected on this class,
384 whereas with ``False`` they act bitwise on 0. Functions in the logic module
385 will return this class when they evaluate to false.
387 Notes
388 ======
390 See the notes section in :py:class:`sympy.logic.boolalg.BooleanTrue`
392 Examples
393 ========
395 >>> from sympy import sympify, true, false, Or
396 >>> sympify(False)
397 False
398 >>> _ is False, _ is false
399 (False, True)
401 >>> Or(true, false)
402 True
403 >>> _ is true
404 True
406 Python operators give a boolean result for false but a
407 bitwise result for False
409 >>> ~false, ~False
410 (True, -1)
411 >>> false >> false, False >> False
412 (True, 0)
414 See Also
415 ========
417 sympy.logic.boolalg.BooleanTrue
419 """
420 def __bool__(self):
421 return False
423 def __hash__(self):
424 return hash(False)
426 def __eq__(self, other):
427 if other is True:
428 return False
429 if other is False:
430 return True
431 return super().__eq__(other)
433 @property
434 def negated(self):
435 return true
437 def as_set(self):
438 """
439 Rewrite logic operators and relationals in terms of real sets.
441 Examples
442 ========
444 >>> from sympy import false
445 >>> false.as_set()
446 EmptySet
447 """
448 return S.EmptySet
451true = BooleanTrue()
452false = BooleanFalse()
453# We want S.true and S.false to work, rather than S.BooleanTrue and
454# S.BooleanFalse, but making the class and instance names the same causes some
455# major issues (like the inability to import the class directly from this
456# file).
457S.true = true
458S.false = false
460_sympy_converter[bool] = lambda x: true if x else false
463class BooleanFunction(Application, Boolean):
464 """Boolean function is a function that lives in a boolean space
465 It is used as base class for :py:class:`~.And`, :py:class:`~.Or`,
466 :py:class:`~.Not`, etc.
467 """
468 is_Boolean = True
470 def _eval_simplify(self, **kwargs):
471 rv = simplify_univariate(self)
472 if not isinstance(rv, BooleanFunction):
473 return rv.simplify(**kwargs)
474 rv = rv.func(*[a.simplify(**kwargs) for a in rv.args])
475 return simplify_logic(rv)
477 def simplify(self, **kwargs):
478 from sympy.simplify.simplify import simplify
479 return simplify(self, **kwargs)
481 def __lt__(self, other):
482 raise TypeError(filldedent('''
483 A Boolean argument can only be used in
484 Eq and Ne; all other relationals expect
485 real expressions.
486 '''))
487 __le__ = __lt__
488 __ge__ = __lt__
489 __gt__ = __lt__
491 @classmethod
492 def binary_check_and_simplify(self, *args):
493 from sympy.core.relational import Relational, Eq, Ne
494 args = [as_Boolean(i) for i in args]
495 bin_syms = set().union(*[i.binary_symbols for i in args])
496 rel = set().union(*[i.atoms(Relational) for i in args])
497 reps = {}
498 for x in bin_syms:
499 for r in rel:
500 if x in bin_syms and x in r.free_symbols:
501 if isinstance(r, (Eq, Ne)):
502 if not (
503 true in r.args or
504 false in r.args):
505 reps[r] = false
506 else:
507 raise TypeError(filldedent('''
508 Incompatible use of binary symbol `%s` as a
509 real variable in `%s`
510 ''' % (x, r)))
511 return [i.subs(reps) for i in args]
513 def to_nnf(self, simplify=True):
514 return self._to_nnf(*self.args, simplify=simplify)
516 def to_anf(self, deep=True):
517 return self._to_anf(*self.args, deep=deep)
519 @classmethod
520 def _to_nnf(cls, *args, **kwargs):
521 simplify = kwargs.get('simplify', True)
522 argset = set()
523 for arg in args:
524 if not is_literal(arg):
525 arg = arg.to_nnf(simplify)
526 if simplify:
527 if isinstance(arg, cls):
528 arg = arg.args
529 else:
530 arg = (arg,)
531 for a in arg:
532 if Not(a) in argset:
533 return cls.zero
534 argset.add(a)
535 else:
536 argset.add(arg)
537 return cls(*argset)
539 @classmethod
540 def _to_anf(cls, *args, **kwargs):
541 deep = kwargs.get('deep', True)
542 argset = set()
543 for arg in args:
544 if deep:
545 if not is_literal(arg) or isinstance(arg, Not):
546 arg = arg.to_anf(deep=deep)
547 argset.add(arg)
548 else:
549 argset.add(arg)
550 return cls(*argset, remove_true=False)
552 # the diff method below is copied from Expr class
553 def diff(self, *symbols, **assumptions):
554 assumptions.setdefault("evaluate", True)
555 return Derivative(self, *symbols, **assumptions)
557 def _eval_derivative(self, x):
558 if x in self.binary_symbols:
559 from sympy.core.relational import Eq
560 from sympy.functions.elementary.piecewise import Piecewise
561 return Piecewise(
562 (0, Eq(self.subs(x, 0), self.subs(x, 1))),
563 (1, True))
564 elif x in self.free_symbols:
565 # not implemented, see https://www.encyclopediaofmath.org/
566 # index.php/Boolean_differential_calculus
567 pass
568 else:
569 return S.Zero
572class And(LatticeOp, BooleanFunction):
573 """
574 Logical AND function.
576 It evaluates its arguments in order, returning false immediately
577 when an argument is false and true if they are all true.
579 Examples
580 ========
582 >>> from sympy.abc import x, y
583 >>> from sympy import And
584 >>> x & y
585 x & y
587 Notes
588 =====
590 The ``&`` operator is provided as a convenience, but note that its use
591 here is different from its normal use in Python, which is bitwise
592 and. Hence, ``And(a, b)`` and ``a & b`` will produce different results if
593 ``a`` and ``b`` are integers.
595 >>> And(x, y).subs(x, 1)
596 y
598 """
599 zero = false
600 identity = true
602 nargs = None
604 @classmethod
605 def _new_args_filter(cls, args):
606 args = BooleanFunction.binary_check_and_simplify(*args)
607 args = LatticeOp._new_args_filter(args, And)
608 newargs = []
609 rel = set()
610 for x in ordered(args):
611 if x.is_Relational:
612 c = x.canonical
613 if c in rel:
614 continue
615 elif c.negated.canonical in rel:
616 return [false]
617 else:
618 rel.add(c)
619 newargs.append(x)
620 return newargs
622 def _eval_subs(self, old, new):
623 args = []
624 bad = None
625 for i in self.args:
626 try:
627 i = i.subs(old, new)
628 except TypeError:
629 # store TypeError
630 if bad is None:
631 bad = i
632 continue
633 if i == False:
634 return false
635 elif i != True:
636 args.append(i)
637 if bad is not None:
638 # let it raise
639 bad.subs(old, new)
640 # If old is And, replace the parts of the arguments with new if all
641 # are there
642 if isinstance(old, And):
643 old_set = set(old.args)
644 if old_set.issubset(args):
645 args = set(args) - old_set
646 args.add(new)
648 return self.func(*args)
650 def _eval_simplify(self, **kwargs):
651 from sympy.core.relational import Equality, Relational
652 from sympy.solvers.solveset import linear_coeffs
653 # standard simplify
654 rv = super()._eval_simplify(**kwargs)
655 if not isinstance(rv, And):
656 return rv
658 # simplify args that are equalities involving
659 # symbols so x == 0 & x == y -> x==0 & y == 0
660 Rel, nonRel = sift(rv.args, lambda i: isinstance(i, Relational),
661 binary=True)
662 if not Rel:
663 return rv
664 eqs, other = sift(Rel, lambda i: isinstance(i, Equality), binary=True)
666 measure = kwargs['measure']
667 if eqs:
668 ratio = kwargs['ratio']
669 reps = {}
670 sifted = {}
671 # group by length of free symbols
672 sifted = sift(ordered([
673 (i.free_symbols, i) for i in eqs]),
674 lambda x: len(x[0]))
675 eqs = []
676 nonlineqs = []
677 while 1 in sifted:
678 for free, e in sifted.pop(1):
679 x = free.pop()
680 if (e.lhs != x or x in e.rhs.free_symbols) and x not in reps:
681 try:
682 m, b = linear_coeffs(
683 e.rewrite(Add, evaluate=False), x)
684 enew = e.func(x, -b/m)
685 if measure(enew) <= ratio*measure(e):
686 e = enew
687 else:
688 eqs.append(e)
689 continue
690 except ValueError:
691 pass
692 if x in reps:
693 eqs.append(e.subs(x, reps[x]))
694 elif e.lhs == x and x not in e.rhs.free_symbols:
695 reps[x] = e.rhs
696 eqs.append(e)
697 else:
698 # x is not yet identified, but may be later
699 nonlineqs.append(e)
700 resifted = defaultdict(list)
701 for k in sifted:
702 for f, e in sifted[k]:
703 e = e.xreplace(reps)
704 f = e.free_symbols
705 resifted[len(f)].append((f, e))
706 sifted = resifted
707 for k in sifted:
708 eqs.extend([e for f, e in sifted[k]])
709 nonlineqs = [ei.subs(reps) for ei in nonlineqs]
710 other = [ei.subs(reps) for ei in other]
711 rv = rv.func(*([i.canonical for i in (eqs + nonlineqs + other)] + nonRel))
712 patterns = _simplify_patterns_and()
713 threeterm_patterns = _simplify_patterns_and3()
714 return _apply_patternbased_simplification(rv, patterns,
715 measure, false,
716 threeterm_patterns=threeterm_patterns)
718 def _eval_as_set(self):
719 from sympy.sets.sets import Intersection
720 return Intersection(*[arg.as_set() for arg in self.args])
722 def _eval_rewrite_as_Nor(self, *args, **kwargs):
723 return Nor(*[Not(arg) for arg in self.args])
725 def to_anf(self, deep=True):
726 if deep:
727 result = And._to_anf(*self.args, deep=deep)
728 return distribute_xor_over_and(result)
729 return self
732class Or(LatticeOp, BooleanFunction):
733 """
734 Logical OR function
736 It evaluates its arguments in order, returning true immediately
737 when an argument is true, and false if they are all false.
739 Examples
740 ========
742 >>> from sympy.abc import x, y
743 >>> from sympy import Or
744 >>> x | y
745 x | y
747 Notes
748 =====
750 The ``|`` operator is provided as a convenience, but note that its use
751 here is different from its normal use in Python, which is bitwise
752 or. Hence, ``Or(a, b)`` and ``a | b`` will return different things if
753 ``a`` and ``b`` are integers.
755 >>> Or(x, y).subs(x, 0)
756 y
758 """
759 zero = true
760 identity = false
762 @classmethod
763 def _new_args_filter(cls, args):
764 newargs = []
765 rel = []
766 args = BooleanFunction.binary_check_and_simplify(*args)
767 for x in args:
768 if x.is_Relational:
769 c = x.canonical
770 if c in rel:
771 continue
772 nc = c.negated.canonical
773 if any(r == nc for r in rel):
774 return [true]
775 rel.append(c)
776 newargs.append(x)
777 return LatticeOp._new_args_filter(newargs, Or)
779 def _eval_subs(self, old, new):
780 args = []
781 bad = None
782 for i in self.args:
783 try:
784 i = i.subs(old, new)
785 except TypeError:
786 # store TypeError
787 if bad is None:
788 bad = i
789 continue
790 if i == True:
791 return true
792 elif i != False:
793 args.append(i)
794 if bad is not None:
795 # let it raise
796 bad.subs(old, new)
797 # If old is Or, replace the parts of the arguments with new if all
798 # are there
799 if isinstance(old, Or):
800 old_set = set(old.args)
801 if old_set.issubset(args):
802 args = set(args) - old_set
803 args.add(new)
805 return self.func(*args)
807 def _eval_as_set(self):
808 from sympy.sets.sets import Union
809 return Union(*[arg.as_set() for arg in self.args])
811 def _eval_rewrite_as_Nand(self, *args, **kwargs):
812 return Nand(*[Not(arg) for arg in self.args])
814 def _eval_simplify(self, **kwargs):
815 from sympy.core.relational import Le, Ge, Eq
816 lege = self.atoms(Le, Ge)
817 if lege:
818 reps = {i: self.func(
819 Eq(i.lhs, i.rhs), i.strict) for i in lege}
820 return self.xreplace(reps)._eval_simplify(**kwargs)
821 # standard simplify
822 rv = super()._eval_simplify(**kwargs)
823 if not isinstance(rv, Or):
824 return rv
825 patterns = _simplify_patterns_or()
826 return _apply_patternbased_simplification(rv, patterns,
827 kwargs['measure'], true)
829 def to_anf(self, deep=True):
830 args = range(1, len(self.args) + 1)
831 args = (combinations(self.args, j) for j in args)
832 args = chain.from_iterable(args) # powerset
833 args = (And(*arg) for arg in args)
834 args = (to_anf(x, deep=deep) if deep else x for x in args)
835 return Xor(*list(args), remove_true=False)
838class Not(BooleanFunction):
839 """
840 Logical Not function (negation)
843 Returns ``true`` if the statement is ``false`` or ``False``.
844 Returns ``false`` if the statement is ``true`` or ``True``.
846 Examples
847 ========
849 >>> from sympy import Not, And, Or
850 >>> from sympy.abc import x, A, B
851 >>> Not(True)
852 False
853 >>> Not(False)
854 True
855 >>> Not(And(True, False))
856 True
857 >>> Not(Or(True, False))
858 False
859 >>> Not(And(And(True, x), Or(x, False)))
860 ~x
861 >>> ~x
862 ~x
863 >>> Not(And(Or(A, B), Or(~A, ~B)))
864 ~((A | B) & (~A | ~B))
866 Notes
867 =====
869 - The ``~`` operator is provided as a convenience, but note that its use
870 here is different from its normal use in Python, which is bitwise
871 not. In particular, ``~a`` and ``Not(a)`` will be different if ``a`` is
872 an integer. Furthermore, since bools in Python subclass from ``int``,
873 ``~True`` is the same as ``~1`` which is ``-2``, which has a boolean
874 value of True. To avoid this issue, use the SymPy boolean types
875 ``true`` and ``false``.
877 >>> from sympy import true
878 >>> ~True
879 -2
880 >>> ~true
881 False
883 """
885 is_Not = True
887 @classmethod
888 def eval(cls, arg):
889 if isinstance(arg, Number) or arg in (True, False):
890 return false if arg else true
891 if arg.is_Not:
892 return arg.args[0]
893 # Simplify Relational objects.
894 if arg.is_Relational:
895 return arg.negated
897 def _eval_as_set(self):
898 """
899 Rewrite logic operators and relationals in terms of real sets.
901 Examples
902 ========
904 >>> from sympy import Not, Symbol
905 >>> x = Symbol('x')
906 >>> Not(x > 0).as_set()
907 Interval(-oo, 0)
908 """
909 return self.args[0].as_set().complement(S.Reals)
911 def to_nnf(self, simplify=True):
912 if is_literal(self):
913 return self
915 expr = self.args[0]
917 func, args = expr.func, expr.args
919 if func == And:
920 return Or._to_nnf(*[Not(arg) for arg in args], simplify=simplify)
922 if func == Or:
923 return And._to_nnf(*[Not(arg) for arg in args], simplify=simplify)
925 if func == Implies:
926 a, b = args
927 return And._to_nnf(a, Not(b), simplify=simplify)
929 if func == Equivalent:
930 return And._to_nnf(Or(*args), Or(*[Not(arg) for arg in args]),
931 simplify=simplify)
933 if func == Xor:
934 result = []
935 for i in range(1, len(args)+1, 2):
936 for neg in combinations(args, i):
937 clause = [Not(s) if s in neg else s for s in args]
938 result.append(Or(*clause))
939 return And._to_nnf(*result, simplify=simplify)
941 if func == ITE:
942 a, b, c = args
943 return And._to_nnf(Or(a, Not(c)), Or(Not(a), Not(b)), simplify=simplify)
945 raise ValueError("Illegal operator %s in expression" % func)
947 def to_anf(self, deep=True):
948 return Xor._to_anf(true, self.args[0], deep=deep)
951class Xor(BooleanFunction):
952 """
953 Logical XOR (exclusive OR) function.
956 Returns True if an odd number of the arguments are True and the rest are
957 False.
959 Returns False if an even number of the arguments are True and the rest are
960 False.
962 Examples
963 ========
965 >>> from sympy.logic.boolalg import Xor
966 >>> from sympy import symbols
967 >>> x, y = symbols('x y')
968 >>> Xor(True, False)
969 True
970 >>> Xor(True, True)
971 False
972 >>> Xor(True, False, True, True, False)
973 True
974 >>> Xor(True, False, True, False)
975 False
976 >>> x ^ y
977 x ^ y
979 Notes
980 =====
982 The ``^`` operator is provided as a convenience, but note that its use
983 here is different from its normal use in Python, which is bitwise xor. In
984 particular, ``a ^ b`` and ``Xor(a, b)`` will be different if ``a`` and
985 ``b`` are integers.
987 >>> Xor(x, y).subs(y, 0)
988 x
990 """
991 def __new__(cls, *args, remove_true=True, **kwargs):
992 argset = set()
993 obj = super().__new__(cls, *args, **kwargs)
994 for arg in obj._args:
995 if isinstance(arg, Number) or arg in (True, False):
996 if arg:
997 arg = true
998 else:
999 continue
1000 if isinstance(arg, Xor):
1001 for a in arg.args:
1002 argset.remove(a) if a in argset else argset.add(a)
1003 elif arg in argset:
1004 argset.remove(arg)
1005 else:
1006 argset.add(arg)
1007 rel = [(r, r.canonical, r.negated.canonical)
1008 for r in argset if r.is_Relational]
1009 odd = False # is number of complimentary pairs odd? start 0 -> False
1010 remove = []
1011 for i, (r, c, nc) in enumerate(rel):
1012 for j in range(i + 1, len(rel)):
1013 rj, cj = rel[j][:2]
1014 if cj == nc:
1015 odd = ~odd
1016 break
1017 elif cj == c:
1018 break
1019 else:
1020 continue
1021 remove.append((r, rj))
1022 if odd:
1023 argset.remove(true) if true in argset else argset.add(true)
1024 for a, b in remove:
1025 argset.remove(a)
1026 argset.remove(b)
1027 if len(argset) == 0:
1028 return false
1029 elif len(argset) == 1:
1030 return argset.pop()
1031 elif True in argset and remove_true:
1032 argset.remove(True)
1033 return Not(Xor(*argset))
1034 else:
1035 obj._args = tuple(ordered(argset))
1036 obj._argset = frozenset(argset)
1037 return obj
1039 # XXX: This should be cached on the object rather than using cacheit
1040 # Maybe it can be computed in __new__?
1041 @property # type: ignore
1042 @cacheit
1043 def args(self):
1044 return tuple(ordered(self._argset))
1046 def to_nnf(self, simplify=True):
1047 args = []
1048 for i in range(0, len(self.args)+1, 2):
1049 for neg in combinations(self.args, i):
1050 clause = [Not(s) if s in neg else s for s in self.args]
1051 args.append(Or(*clause))
1052 return And._to_nnf(*args, simplify=simplify)
1054 def _eval_rewrite_as_Or(self, *args, **kwargs):
1055 a = self.args
1056 return Or(*[_convert_to_varsSOP(x, self.args)
1057 for x in _get_odd_parity_terms(len(a))])
1059 def _eval_rewrite_as_And(self, *args, **kwargs):
1060 a = self.args
1061 return And(*[_convert_to_varsPOS(x, self.args)
1062 for x in _get_even_parity_terms(len(a))])
1064 def _eval_simplify(self, **kwargs):
1065 # as standard simplify uses simplify_logic which writes things as
1066 # And and Or, we only simplify the partial expressions before using
1067 # patterns
1068 rv = self.func(*[a.simplify(**kwargs) for a in self.args])
1069 if not isinstance(rv, Xor): # This shouldn't really happen here
1070 return rv
1071 patterns = _simplify_patterns_xor()
1072 return _apply_patternbased_simplification(rv, patterns,
1073 kwargs['measure'], None)
1075 def _eval_subs(self, old, new):
1076 # If old is Xor, replace the parts of the arguments with new if all
1077 # are there
1078 if isinstance(old, Xor):
1079 old_set = set(old.args)
1080 if old_set.issubset(self.args):
1081 args = set(self.args) - old_set
1082 args.add(new)
1083 return self.func(*args)
1086class Nand(BooleanFunction):
1087 """
1088 Logical NAND function.
1090 It evaluates its arguments in order, giving True immediately if any
1091 of them are False, and False if they are all True.
1093 Returns True if any of the arguments are False
1094 Returns False if all arguments are True
1096 Examples
1097 ========
1099 >>> from sympy.logic.boolalg import Nand
1100 >>> from sympy import symbols
1101 >>> x, y = symbols('x y')
1102 >>> Nand(False, True)
1103 True
1104 >>> Nand(True, True)
1105 False
1106 >>> Nand(x, y)
1107 ~(x & y)
1109 """
1110 @classmethod
1111 def eval(cls, *args):
1112 return Not(And(*args))
1115class Nor(BooleanFunction):
1116 """
1117 Logical NOR function.
1119 It evaluates its arguments in order, giving False immediately if any
1120 of them are True, and True if they are all False.
1122 Returns False if any argument is True
1123 Returns True if all arguments are False
1125 Examples
1126 ========
1128 >>> from sympy.logic.boolalg import Nor
1129 >>> from sympy import symbols
1130 >>> x, y = symbols('x y')
1132 >>> Nor(True, False)
1133 False
1134 >>> Nor(True, True)
1135 False
1136 >>> Nor(False, True)
1137 False
1138 >>> Nor(False, False)
1139 True
1140 >>> Nor(x, y)
1141 ~(x | y)
1143 """
1144 @classmethod
1145 def eval(cls, *args):
1146 return Not(Or(*args))
1149class Xnor(BooleanFunction):
1150 """
1151 Logical XNOR function.
1153 Returns False if an odd number of the arguments are True and the rest are
1154 False.
1156 Returns True if an even number of the arguments are True and the rest are
1157 False.
1159 Examples
1160 ========
1162 >>> from sympy.logic.boolalg import Xnor
1163 >>> from sympy import symbols
1164 >>> x, y = symbols('x y')
1165 >>> Xnor(True, False)
1166 False
1167 >>> Xnor(True, True)
1168 True
1169 >>> Xnor(True, False, True, True, False)
1170 False
1171 >>> Xnor(True, False, True, False)
1172 True
1174 """
1175 @classmethod
1176 def eval(cls, *args):
1177 return Not(Xor(*args))
1180class Implies(BooleanFunction):
1181 r"""
1182 Logical implication.
1184 A implies B is equivalent to if A then B. Mathematically, it is written
1185 as `A \Rightarrow B` and is equivalent to `\neg A \vee B` or ``~A | B``.
1187 Accepts two Boolean arguments; A and B.
1188 Returns False if A is True and B is False
1189 Returns True otherwise.
1191 Examples
1192 ========
1194 >>> from sympy.logic.boolalg import Implies
1195 >>> from sympy import symbols
1196 >>> x, y = symbols('x y')
1198 >>> Implies(True, False)
1199 False
1200 >>> Implies(False, False)
1201 True
1202 >>> Implies(True, True)
1203 True
1204 >>> Implies(False, True)
1205 True
1206 >>> x >> y
1207 Implies(x, y)
1208 >>> y << x
1209 Implies(x, y)
1211 Notes
1212 =====
1214 The ``>>`` and ``<<`` operators are provided as a convenience, but note
1215 that their use here is different from their normal use in Python, which is
1216 bit shifts. Hence, ``Implies(a, b)`` and ``a >> b`` will return different
1217 things if ``a`` and ``b`` are integers. In particular, since Python
1218 considers ``True`` and ``False`` to be integers, ``True >> True`` will be
1219 the same as ``1 >> 1``, i.e., 0, which has a truth value of False. To
1220 avoid this issue, use the SymPy objects ``true`` and ``false``.
1222 >>> from sympy import true, false
1223 >>> True >> False
1224 1
1225 >>> true >> false
1226 False
1228 """
1229 @classmethod
1230 def eval(cls, *args):
1231 try:
1232 newargs = []
1233 for x in args:
1234 if isinstance(x, Number) or x in (0, 1):
1235 newargs.append(bool(x))
1236 else:
1237 newargs.append(x)
1238 A, B = newargs
1239 except ValueError:
1240 raise ValueError(
1241 "%d operand(s) used for an Implies "
1242 "(pairs are required): %s" % (len(args), str(args)))
1243 if A in (True, False) or B in (True, False):
1244 return Or(Not(A), B)
1245 elif A == B:
1246 return true
1247 elif A.is_Relational and B.is_Relational:
1248 if A.canonical == B.canonical:
1249 return true
1250 if A.negated.canonical == B.canonical:
1251 return B
1252 else:
1253 return Basic.__new__(cls, *args)
1255 def to_nnf(self, simplify=True):
1256 a, b = self.args
1257 return Or._to_nnf(Not(a), b, simplify=simplify)
1259 def to_anf(self, deep=True):
1260 a, b = self.args
1261 return Xor._to_anf(true, a, And(a, b), deep=deep)
1264class Equivalent(BooleanFunction):
1265 """
1266 Equivalence relation.
1268 ``Equivalent(A, B)`` is True iff A and B are both True or both False.
1270 Returns True if all of the arguments are logically equivalent.
1271 Returns False otherwise.
1273 For two arguments, this is equivalent to :py:class:`~.Xnor`.
1275 Examples
1276 ========
1278 >>> from sympy.logic.boolalg import Equivalent, And
1279 >>> from sympy.abc import x
1280 >>> Equivalent(False, False, False)
1281 True
1282 >>> Equivalent(True, False, False)
1283 False
1284 >>> Equivalent(x, And(x, True))
1285 True
1287 """
1288 def __new__(cls, *args, **options):
1289 from sympy.core.relational import Relational
1290 args = [_sympify(arg) for arg in args]
1292 argset = set(args)
1293 for x in args:
1294 if isinstance(x, Number) or x in [True, False]: # Includes 0, 1
1295 argset.discard(x)
1296 argset.add(bool(x))
1297 rel = []
1298 for r in argset:
1299 if isinstance(r, Relational):
1300 rel.append((r, r.canonical, r.negated.canonical))
1301 remove = []
1302 for i, (r, c, nc) in enumerate(rel):
1303 for j in range(i + 1, len(rel)):
1304 rj, cj = rel[j][:2]
1305 if cj == nc:
1306 return false
1307 elif cj == c:
1308 remove.append((r, rj))
1309 break
1310 for a, b in remove:
1311 argset.remove(a)
1312 argset.remove(b)
1313 argset.add(True)
1314 if len(argset) <= 1:
1315 return true
1316 if True in argset:
1317 argset.discard(True)
1318 return And(*argset)
1319 if False in argset:
1320 argset.discard(False)
1321 return And(*[Not(arg) for arg in argset])
1322 _args = frozenset(argset)
1323 obj = super().__new__(cls, _args)
1324 obj._argset = _args
1325 return obj
1327 # XXX: This should be cached on the object rather than using cacheit
1328 # Maybe it can be computed in __new__?
1329 @property # type: ignore
1330 @cacheit
1331 def args(self):
1332 return tuple(ordered(self._argset))
1334 def to_nnf(self, simplify=True):
1335 args = []
1336 for a, b in zip(self.args, self.args[1:]):
1337 args.append(Or(Not(a), b))
1338 args.append(Or(Not(self.args[-1]), self.args[0]))
1339 return And._to_nnf(*args, simplify=simplify)
1341 def to_anf(self, deep=True):
1342 a = And(*self.args)
1343 b = And(*[to_anf(Not(arg), deep=False) for arg in self.args])
1344 b = distribute_xor_over_and(b)
1345 return Xor._to_anf(a, b, deep=deep)
1348class ITE(BooleanFunction):
1349 """
1350 If-then-else clause.
1352 ``ITE(A, B, C)`` evaluates and returns the result of B if A is true
1353 else it returns the result of C. All args must be Booleans.
1355 From a logic gate perspective, ITE corresponds to a 2-to-1 multiplexer,
1356 where A is the select signal.
1358 Examples
1359 ========
1361 >>> from sympy.logic.boolalg import ITE, And, Xor, Or
1362 >>> from sympy.abc import x, y, z
1363 >>> ITE(True, False, True)
1364 False
1365 >>> ITE(Or(True, False), And(True, True), Xor(True, True))
1366 True
1367 >>> ITE(x, y, z)
1368 ITE(x, y, z)
1369 >>> ITE(True, x, y)
1370 x
1371 >>> ITE(False, x, y)
1372 y
1373 >>> ITE(x, y, y)
1374 y
1376 Trying to use non-Boolean args will generate a TypeError:
1378 >>> ITE(True, [], ())
1379 Traceback (most recent call last):
1380 ...
1381 TypeError: expecting bool, Boolean or ITE, not `[]`
1383 """
1384 def __new__(cls, *args, **kwargs):
1385 from sympy.core.relational import Eq, Ne
1386 if len(args) != 3:
1387 raise ValueError('expecting exactly 3 args')
1388 a, b, c = args
1389 # check use of binary symbols
1390 if isinstance(a, (Eq, Ne)):
1391 # in this context, we can evaluate the Eq/Ne
1392 # if one arg is a binary symbol and the other
1393 # is true/false
1394 b, c = map(as_Boolean, (b, c))
1395 bin_syms = set().union(*[i.binary_symbols for i in (b, c)])
1396 if len(set(a.args) - bin_syms) == 1:
1397 # one arg is a binary_symbols
1398 _a = a
1399 if a.lhs is true:
1400 a = a.rhs
1401 elif a.rhs is true:
1402 a = a.lhs
1403 elif a.lhs is false:
1404 a = Not(a.rhs)
1405 elif a.rhs is false:
1406 a = Not(a.lhs)
1407 else:
1408 # binary can only equal True or False
1409 a = false
1410 if isinstance(_a, Ne):
1411 a = Not(a)
1412 else:
1413 a, b, c = BooleanFunction.binary_check_and_simplify(
1414 a, b, c)
1415 rv = None
1416 if kwargs.get('evaluate', True):
1417 rv = cls.eval(a, b, c)
1418 if rv is None:
1419 rv = BooleanFunction.__new__(cls, a, b, c, evaluate=False)
1420 return rv
1422 @classmethod
1423 def eval(cls, *args):
1424 from sympy.core.relational import Eq, Ne
1425 # do the args give a singular result?
1426 a, b, c = args
1427 if isinstance(a, (Ne, Eq)):
1428 _a = a
1429 if true in a.args:
1430 a = a.lhs if a.rhs is true else a.rhs
1431 elif false in a.args:
1432 a = Not(a.lhs) if a.rhs is false else Not(a.rhs)
1433 else:
1434 _a = None
1435 if _a is not None and isinstance(_a, Ne):
1436 a = Not(a)
1437 if a is true:
1438 return b
1439 if a is false:
1440 return c
1441 if b == c:
1442 return b
1443 else:
1444 # or maybe the results allow the answer to be expressed
1445 # in terms of the condition
1446 if b is true and c is false:
1447 return a
1448 if b is false and c is true:
1449 return Not(a)
1450 if [a, b, c] != args:
1451 return cls(a, b, c, evaluate=False)
1453 def to_nnf(self, simplify=True):
1454 a, b, c = self.args
1455 return And._to_nnf(Or(Not(a), b), Or(a, c), simplify=simplify)
1457 def _eval_as_set(self):
1458 return self.to_nnf().as_set()
1460 def _eval_rewrite_as_Piecewise(self, *args, **kwargs):
1461 from sympy.functions.elementary.piecewise import Piecewise
1462 return Piecewise((args[1], args[0]), (args[2], True))
1465class Exclusive(BooleanFunction):
1466 """
1467 True if only one or no argument is true.
1469 ``Exclusive(A, B, C)`` is equivalent to ``~(A & B) & ~(A & C) & ~(B & C)``.
1471 For two arguments, this is equivalent to :py:class:`~.Xor`.
1473 Examples
1474 ========
1476 >>> from sympy.logic.boolalg import Exclusive
1477 >>> Exclusive(False, False, False)
1478 True
1479 >>> Exclusive(False, True, False)
1480 True
1481 >>> Exclusive(False, True, True)
1482 False
1484 """
1485 @classmethod
1486 def eval(cls, *args):
1487 and_args = []
1488 for a, b in combinations(args, 2):
1489 and_args.append(Not(And(a, b)))
1490 return And(*and_args)
1493# end class definitions. Some useful methods
1496def conjuncts(expr):
1497 """Return a list of the conjuncts in ``expr``.
1499 Examples
1500 ========
1502 >>> from sympy.logic.boolalg import conjuncts
1503 >>> from sympy.abc import A, B
1504 >>> conjuncts(A & B)
1505 frozenset({A, B})
1506 >>> conjuncts(A | B)
1507 frozenset({A | B})
1509 """
1510 return And.make_args(expr)
1513def disjuncts(expr):
1514 """Return a list of the disjuncts in ``expr``.
1516 Examples
1517 ========
1519 >>> from sympy.logic.boolalg import disjuncts
1520 >>> from sympy.abc import A, B
1521 >>> disjuncts(A | B)
1522 frozenset({A, B})
1523 >>> disjuncts(A & B)
1524 frozenset({A & B})
1526 """
1527 return Or.make_args(expr)
1530def distribute_and_over_or(expr):
1531 """
1532 Given a sentence ``expr`` consisting of conjunctions and disjunctions
1533 of literals, return an equivalent sentence in CNF.
1535 Examples
1536 ========
1538 >>> from sympy.logic.boolalg import distribute_and_over_or, And, Or, Not
1539 >>> from sympy.abc import A, B, C
1540 >>> distribute_and_over_or(Or(A, And(Not(B), Not(C))))
1541 (A | ~B) & (A | ~C)
1543 """
1544 return _distribute((expr, And, Or))
1547def distribute_or_over_and(expr):
1548 """
1549 Given a sentence ``expr`` consisting of conjunctions and disjunctions
1550 of literals, return an equivalent sentence in DNF.
1552 Note that the output is NOT simplified.
1554 Examples
1555 ========
1557 >>> from sympy.logic.boolalg import distribute_or_over_and, And, Or, Not
1558 >>> from sympy.abc import A, B, C
1559 >>> distribute_or_over_and(And(Or(Not(A), B), C))
1560 (B & C) | (C & ~A)
1562 """
1563 return _distribute((expr, Or, And))
1566def distribute_xor_over_and(expr):
1567 """
1568 Given a sentence ``expr`` consisting of conjunction and
1569 exclusive disjunctions of literals, return an
1570 equivalent exclusive disjunction.
1572 Note that the output is NOT simplified.
1574 Examples
1575 ========
1577 >>> from sympy.logic.boolalg import distribute_xor_over_and, And, Xor, Not
1578 >>> from sympy.abc import A, B, C
1579 >>> distribute_xor_over_and(And(Xor(Not(A), B), C))
1580 (B & C) ^ (C & ~A)
1581 """
1582 return _distribute((expr, Xor, And))
1585def _distribute(info):
1586 """
1587 Distributes ``info[1]`` over ``info[2]`` with respect to ``info[0]``.
1588 """
1589 if isinstance(info[0], info[2]):
1590 for arg in info[0].args:
1591 if isinstance(arg, info[1]):
1592 conj = arg
1593 break
1594 else:
1595 return info[0]
1596 rest = info[2](*[a for a in info[0].args if a is not conj])
1597 return info[1](*list(map(_distribute,
1598 [(info[2](c, rest), info[1], info[2])
1599 for c in conj.args])), remove_true=False)
1600 elif isinstance(info[0], info[1]):
1601 return info[1](*list(map(_distribute,
1602 [(x, info[1], info[2])
1603 for x in info[0].args])),
1604 remove_true=False)
1605 else:
1606 return info[0]
1609def to_anf(expr, deep=True):
1610 r"""
1611 Converts expr to Algebraic Normal Form (ANF).
1613 ANF is a canonical normal form, which means that two
1614 equivalent formulas will convert to the same ANF.
1616 A logical expression is in ANF if it has the form
1618 .. math:: 1 \oplus a \oplus b \oplus ab \oplus abc
1620 i.e. it can be:
1621 - purely true,
1622 - purely false,
1623 - conjunction of variables,
1624 - exclusive disjunction.
1626 The exclusive disjunction can only contain true, variables
1627 or conjunction of variables. No negations are permitted.
1629 If ``deep`` is ``False``, arguments of the boolean
1630 expression are considered variables, i.e. only the
1631 top-level expression is converted to ANF.
1633 Examples
1634 ========
1635 >>> from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent
1636 >>> from sympy.logic.boolalg import to_anf
1637 >>> from sympy.abc import A, B, C
1638 >>> to_anf(Not(A))
1639 A ^ True
1640 >>> to_anf(And(Or(A, B), Not(C)))
1641 A ^ B ^ (A & B) ^ (A & C) ^ (B & C) ^ (A & B & C)
1642 >>> to_anf(Implies(Not(A), Equivalent(B, C)), deep=False)
1643 True ^ ~A ^ (~A & (Equivalent(B, C)))
1645 """
1646 expr = sympify(expr)
1648 if is_anf(expr):
1649 return expr
1650 return expr.to_anf(deep=deep)
1653def to_nnf(expr, simplify=True):
1654 """
1655 Converts ``expr`` to Negation Normal Form (NNF).
1657 A logical expression is in NNF if it
1658 contains only :py:class:`~.And`, :py:class:`~.Or` and :py:class:`~.Not`,
1659 and :py:class:`~.Not` is applied only to literals.
1660 If ``simplify`` is ``True``, the result contains no redundant clauses.
1662 Examples
1663 ========
1665 >>> from sympy.abc import A, B, C, D
1666 >>> from sympy.logic.boolalg import Not, Equivalent, to_nnf
1667 >>> to_nnf(Not((~A & ~B) | (C & D)))
1668 (A | B) & (~C | ~D)
1669 >>> to_nnf(Equivalent(A >> B, B >> A))
1670 (A | ~B | (A & ~B)) & (B | ~A | (B & ~A))
1672 """
1673 if is_nnf(expr, simplify):
1674 return expr
1675 return expr.to_nnf(simplify)
1678def to_cnf(expr, simplify=False, force=False):
1679 """
1680 Convert a propositional logical sentence ``expr`` to conjunctive normal
1681 form: ``((A | ~B | ...) & (B | C | ...) & ...)``.
1682 If ``simplify`` is ``True``, ``expr`` is evaluated to its simplest CNF
1683 form using the Quine-McCluskey algorithm; this may take a long
1684 time. If there are more than 8 variables the ``force`` flag must be set
1685 to ``True`` to simplify (default is ``False``).
1687 Examples
1688 ========
1690 >>> from sympy.logic.boolalg import to_cnf
1691 >>> from sympy.abc import A, B, D
1692 >>> to_cnf(~(A | B) | D)
1693 (D | ~A) & (D | ~B)
1694 >>> to_cnf((A | B) & (A | ~A), True)
1695 A | B
1697 """
1698 expr = sympify(expr)
1699 if not isinstance(expr, BooleanFunction):
1700 return expr
1702 if simplify:
1703 if not force and len(_find_predicates(expr)) > 8:
1704 raise ValueError(filldedent('''
1705 To simplify a logical expression with more
1706 than 8 variables may take a long time and requires
1707 the use of `force=True`.'''))
1708 return simplify_logic(expr, 'cnf', True, force=force)
1710 # Don't convert unless we have to
1711 if is_cnf(expr):
1712 return expr
1714 expr = eliminate_implications(expr)
1715 res = distribute_and_over_or(expr)
1717 return res
1720def to_dnf(expr, simplify=False, force=False):
1721 """
1722 Convert a propositional logical sentence ``expr`` to disjunctive normal
1723 form: ``((A & ~B & ...) | (B & C & ...) | ...)``.
1724 If ``simplify`` is ``True``, ``expr`` is evaluated to its simplest DNF form using
1725 the Quine-McCluskey algorithm; this may take a long
1726 time. If there are more than 8 variables, the ``force`` flag must be set to
1727 ``True`` to simplify (default is ``False``).
1729 Examples
1730 ========
1732 >>> from sympy.logic.boolalg import to_dnf
1733 >>> from sympy.abc import A, B, C
1734 >>> to_dnf(B & (A | C))
1735 (A & B) | (B & C)
1736 >>> to_dnf((A & B) | (A & ~B) | (B & C) | (~B & C), True)
1737 A | C
1739 """
1740 expr = sympify(expr)
1741 if not isinstance(expr, BooleanFunction):
1742 return expr
1744 if simplify:
1745 if not force and len(_find_predicates(expr)) > 8:
1746 raise ValueError(filldedent('''
1747 To simplify a logical expression with more
1748 than 8 variables may take a long time and requires
1749 the use of `force=True`.'''))
1750 return simplify_logic(expr, 'dnf', True, force=force)
1752 # Don't convert unless we have to
1753 if is_dnf(expr):
1754 return expr
1756 expr = eliminate_implications(expr)
1757 return distribute_or_over_and(expr)
1760def is_anf(expr):
1761 r"""
1762 Checks if ``expr`` is in Algebraic Normal Form (ANF).
1764 A logical expression is in ANF if it has the form
1766 .. math:: 1 \oplus a \oplus b \oplus ab \oplus abc
1768 i.e. it is purely true, purely false, conjunction of
1769 variables or exclusive disjunction. The exclusive
1770 disjunction can only contain true, variables or
1771 conjunction of variables. No negations are permitted.
1773 Examples
1774 ========
1776 >>> from sympy.logic.boolalg import And, Not, Xor, true, is_anf
1777 >>> from sympy.abc import A, B, C
1778 >>> is_anf(true)
1779 True
1780 >>> is_anf(A)
1781 True
1782 >>> is_anf(And(A, B, C))
1783 True
1784 >>> is_anf(Xor(A, Not(B)))
1785 False
1787 """
1788 expr = sympify(expr)
1790 if is_literal(expr) and not isinstance(expr, Not):
1791 return True
1793 if isinstance(expr, And):
1794 for arg in expr.args:
1795 if not arg.is_Symbol:
1796 return False
1797 return True
1799 elif isinstance(expr, Xor):
1800 for arg in expr.args:
1801 if isinstance(arg, And):
1802 for a in arg.args:
1803 if not a.is_Symbol:
1804 return False
1805 elif is_literal(arg):
1806 if isinstance(arg, Not):
1807 return False
1808 else:
1809 return False
1810 return True
1812 else:
1813 return False
1816def is_nnf(expr, simplified=True):
1817 """
1818 Checks if ``expr`` is in Negation Normal Form (NNF).
1820 A logical expression is in NNF if it
1821 contains only :py:class:`~.And`, :py:class:`~.Or` and :py:class:`~.Not`,
1822 and :py:class:`~.Not` is applied only to literals.
1823 If ``simplified`` is ``True``, checks if result contains no redundant clauses.
1825 Examples
1826 ========
1828 >>> from sympy.abc import A, B, C
1829 >>> from sympy.logic.boolalg import Not, is_nnf
1830 >>> is_nnf(A & B | ~C)
1831 True
1832 >>> is_nnf((A | ~A) & (B | C))
1833 False
1834 >>> is_nnf((A | ~A) & (B | C), False)
1835 True
1836 >>> is_nnf(Not(A & B) | C)
1837 False
1838 >>> is_nnf((A >> B) & (B >> A))
1839 False
1841 """
1843 expr = sympify(expr)
1844 if is_literal(expr):
1845 return True
1847 stack = [expr]
1849 while stack:
1850 expr = stack.pop()
1851 if expr.func in (And, Or):
1852 if simplified:
1853 args = expr.args
1854 for arg in args:
1855 if Not(arg) in args:
1856 return False
1857 stack.extend(expr.args)
1859 elif not is_literal(expr):
1860 return False
1862 return True
1865def is_cnf(expr):
1866 """
1867 Test whether or not an expression is in conjunctive normal form.
1869 Examples
1870 ========
1872 >>> from sympy.logic.boolalg import is_cnf
1873 >>> from sympy.abc import A, B, C
1874 >>> is_cnf(A | B | C)
1875 True
1876 >>> is_cnf(A & B & C)
1877 True
1878 >>> is_cnf((A & B) | C)
1879 False
1881 """
1882 return _is_form(expr, And, Or)
1885def is_dnf(expr):
1886 """
1887 Test whether or not an expression is in disjunctive normal form.
1889 Examples
1890 ========
1892 >>> from sympy.logic.boolalg import is_dnf
1893 >>> from sympy.abc import A, B, C
1894 >>> is_dnf(A | B | C)
1895 True
1896 >>> is_dnf(A & B & C)
1897 True
1898 >>> is_dnf((A & B) | C)
1899 True
1900 >>> is_dnf(A & (B | C))
1901 False
1903 """
1904 return _is_form(expr, Or, And)
1907def _is_form(expr, function1, function2):
1908 """
1909 Test whether or not an expression is of the required form.
1911 """
1912 expr = sympify(expr)
1914 vals = function1.make_args(expr) if isinstance(expr, function1) else [expr]
1915 for lit in vals:
1916 if isinstance(lit, function2):
1917 vals2 = function2.make_args(lit) if isinstance(lit, function2) else [lit]
1918 for l in vals2:
1919 if is_literal(l) is False:
1920 return False
1921 elif is_literal(lit) is False:
1922 return False
1924 return True
1927def eliminate_implications(expr):
1928 """
1929 Change :py:class:`~.Implies` and :py:class:`~.Equivalent` into
1930 :py:class:`~.And`, :py:class:`~.Or`, and :py:class:`~.Not`.
1931 That is, return an expression that is equivalent to ``expr``, but has only
1932 ``&``, ``|``, and ``~`` as logical
1933 operators.
1935 Examples
1936 ========
1938 >>> from sympy.logic.boolalg import Implies, Equivalent, \
1939 eliminate_implications
1940 >>> from sympy.abc import A, B, C
1941 >>> eliminate_implications(Implies(A, B))
1942 B | ~A
1943 >>> eliminate_implications(Equivalent(A, B))
1944 (A | ~B) & (B | ~A)
1945 >>> eliminate_implications(Equivalent(A, B, C))
1946 (A | ~C) & (B | ~A) & (C | ~B)
1948 """
1949 return to_nnf(expr, simplify=False)
1952def is_literal(expr):
1953 """
1954 Returns True if expr is a literal, else False.
1956 Examples
1957 ========
1959 >>> from sympy import Or, Q
1960 >>> from sympy.abc import A, B
1961 >>> from sympy.logic.boolalg import is_literal
1962 >>> is_literal(A)
1963 True
1964 >>> is_literal(~A)
1965 True
1966 >>> is_literal(Q.zero(A))
1967 True
1968 >>> is_literal(A + B)
1969 True
1970 >>> is_literal(Or(A, B))
1971 False
1973 """
1974 from sympy.assumptions import AppliedPredicate
1976 if isinstance(expr, Not):
1977 return is_literal(expr.args[0])
1978 elif expr in (True, False) or isinstance(expr, AppliedPredicate) or expr.is_Atom:
1979 return True
1980 elif not isinstance(expr, BooleanFunction) and all(
1981 (isinstance(expr, AppliedPredicate) or a.is_Atom) for a in expr.args):
1982 return True
1983 return False
1986def to_int_repr(clauses, symbols):
1987 """
1988 Takes clauses in CNF format and puts them into an integer representation.
1990 Examples
1991 ========
1993 >>> from sympy.logic.boolalg import to_int_repr
1994 >>> from sympy.abc import x, y
1995 >>> to_int_repr([x | y, y], [x, y]) == [{1, 2}, {2}]
1996 True
1998 """
2000 # Convert the symbol list into a dict
2001 symbols = dict(zip(symbols, range(1, len(symbols) + 1)))
2003 def append_symbol(arg, symbols):
2004 if isinstance(arg, Not):
2005 return -symbols[arg.args[0]]
2006 else:
2007 return symbols[arg]
2009 return [{append_symbol(arg, symbols) for arg in Or.make_args(c)}
2010 for c in clauses]
2013def term_to_integer(term):
2014 """
2015 Return an integer corresponding to the base-2 digits given by *term*.
2017 Parameters
2018 ==========
2020 term : a string or list of ones and zeros
2022 Examples
2023 ========
2025 >>> from sympy.logic.boolalg import term_to_integer
2026 >>> term_to_integer([1, 0, 0])
2027 4
2028 >>> term_to_integer('100')
2029 4
2031 """
2033 return int(''.join(list(map(str, list(term)))), 2)
2036integer_to_term = ibin # XXX could delete?
2039def truth_table(expr, variables, input=True):
2040 """
2041 Return a generator of all possible configurations of the input variables,
2042 and the result of the boolean expression for those values.
2044 Parameters
2045 ==========
2047 expr : Boolean expression
2049 variables : list of variables
2051 input : bool (default ``True``)
2052 Indicates whether to return the input combinations.
2054 Examples
2055 ========
2057 >>> from sympy.logic.boolalg import truth_table
2058 >>> from sympy.abc import x,y
2059 >>> table = truth_table(x >> y, [x, y])
2060 >>> for t in table:
2061 ... print('{0} -> {1}'.format(*t))
2062 [0, 0] -> True
2063 [0, 1] -> True
2064 [1, 0] -> False
2065 [1, 1] -> True
2067 >>> table = truth_table(x | y, [x, y])
2068 >>> list(table)
2069 [([0, 0], False), ([0, 1], True), ([1, 0], True), ([1, 1], True)]
2071 If ``input`` is ``False``, ``truth_table`` returns only a list of truth values.
2072 In this case, the corresponding input values of variables can be
2073 deduced from the index of a given output.
2075 >>> from sympy.utilities.iterables import ibin
2076 >>> vars = [y, x]
2077 >>> values = truth_table(x >> y, vars, input=False)
2078 >>> values = list(values)
2079 >>> values
2080 [True, False, True, True]
2082 >>> for i, value in enumerate(values):
2083 ... print('{0} -> {1}'.format(list(zip(
2084 ... vars, ibin(i, len(vars)))), value))
2085 [(y, 0), (x, 0)] -> True
2086 [(y, 0), (x, 1)] -> False
2087 [(y, 1), (x, 0)] -> True
2088 [(y, 1), (x, 1)] -> True
2090 """
2091 variables = [sympify(v) for v in variables]
2093 expr = sympify(expr)
2094 if not isinstance(expr, BooleanFunction) and not is_literal(expr):
2095 return
2097 table = product((0, 1), repeat=len(variables))
2098 for term in table:
2099 value = expr.xreplace(dict(zip(variables, term)))
2101 if input:
2102 yield list(term), value
2103 else:
2104 yield value
2107def _check_pair(minterm1, minterm2):
2108 """
2109 Checks if a pair of minterms differs by only one bit. If yes, returns
2110 index, else returns `-1`.
2111 """
2112 # Early termination seems to be faster than list comprehension,
2113 # at least for large examples.
2114 index = -1
2115 for x, i in enumerate(minterm1): # zip(minterm1, minterm2) is slower
2116 if i != minterm2[x]:
2117 if index == -1:
2118 index = x
2119 else:
2120 return -1
2121 return index
2124def _convert_to_varsSOP(minterm, variables):
2125 """
2126 Converts a term in the expansion of a function from binary to its
2127 variable form (for SOP).
2128 """
2129 temp = [variables[n] if val == 1 else Not(variables[n])
2130 for n, val in enumerate(minterm) if val != 3]
2131 return And(*temp)
2134def _convert_to_varsPOS(maxterm, variables):
2135 """
2136 Converts a term in the expansion of a function from binary to its
2137 variable form (for POS).
2138 """
2139 temp = [variables[n] if val == 0 else Not(variables[n])
2140 for n, val in enumerate(maxterm) if val != 3]
2141 return Or(*temp)
2144def _convert_to_varsANF(term, variables):
2145 """
2146 Converts a term in the expansion of a function from binary to its
2147 variable form (for ANF).
2149 Parameters
2150 ==========
2152 term : list of 1's and 0's (complementation pattern)
2153 variables : list of variables
2155 """
2156 temp = [variables[n] for n, t in enumerate(term) if t == 1]
2158 if not temp:
2159 return true
2161 return And(*temp)
2164def _get_odd_parity_terms(n):
2165 """
2166 Returns a list of lists, with all possible combinations of n zeros and ones
2167 with an odd number of ones.
2168 """
2169 return [e for e in [ibin(i, n) for i in range(2**n)] if sum(e) % 2 == 1]
2172def _get_even_parity_terms(n):
2173 """
2174 Returns a list of lists, with all possible combinations of n zeros and ones
2175 with an even number of ones.
2176 """
2177 return [e for e in [ibin(i, n) for i in range(2**n)] if sum(e) % 2 == 0]
2180def _simplified_pairs(terms):
2181 """
2182 Reduces a set of minterms, if possible, to a simplified set of minterms
2183 with one less variable in the terms using QM method.
2184 """
2185 if not terms:
2186 return []
2188 simplified_terms = []
2189 todo = list(range(len(terms)))
2191 # Count number of ones as _check_pair can only potentially match if there
2192 # is at most a difference of a single one
2193 termdict = defaultdict(list)
2194 for n, term in enumerate(terms):
2195 ones = sum([1 for t in term if t == 1])
2196 termdict[ones].append(n)
2198 variables = len(terms[0])
2199 for k in range(variables):
2200 for i in termdict[k]:
2201 for j in termdict[k+1]:
2202 index = _check_pair(terms[i], terms[j])
2203 if index != -1:
2204 # Mark terms handled
2205 todo[i] = todo[j] = None
2206 # Copy old term
2207 newterm = terms[i][:]
2208 # Set differing position to don't care
2209 newterm[index] = 3
2210 # Add if not already there
2211 if newterm not in simplified_terms:
2212 simplified_terms.append(newterm)
2214 if simplified_terms:
2215 # Further simplifications only among the new terms
2216 simplified_terms = _simplified_pairs(simplified_terms)
2218 # Add remaining, non-simplified, terms
2219 simplified_terms.extend([terms[i] for i in todo if i is not None])
2220 return simplified_terms
2223def _rem_redundancy(l1, terms):
2224 """
2225 After the truth table has been sufficiently simplified, use the prime
2226 implicant table method to recognize and eliminate redundant pairs,
2227 and return the essential arguments.
2228 """
2230 if not terms:
2231 return []
2233 nterms = len(terms)
2234 nl1 = len(l1)
2236 # Create dominating matrix
2237 dommatrix = [[0]*nl1 for n in range(nterms)]
2238 colcount = [0]*nl1
2239 rowcount = [0]*nterms
2240 for primei, prime in enumerate(l1):
2241 for termi, term in enumerate(terms):
2242 # Check prime implicant covering term
2243 if all(t == 3 or t == mt for t, mt in zip(prime, term)):
2244 dommatrix[termi][primei] = 1
2245 colcount[primei] += 1
2246 rowcount[termi] += 1
2248 # Keep track if anything changed
2249 anythingchanged = True
2250 # Then, go again
2251 while anythingchanged:
2252 anythingchanged = False
2254 for rowi in range(nterms):
2255 # Still non-dominated?
2256 if rowcount[rowi]:
2257 row = dommatrix[rowi]
2258 for row2i in range(nterms):
2259 # Still non-dominated?
2260 if rowi != row2i and rowcount[rowi] and (rowcount[rowi] <= rowcount[row2i]):
2261 row2 = dommatrix[row2i]
2262 if all(row2[n] >= row[n] for n in range(nl1)):
2263 # row2 dominating row, remove row2
2264 rowcount[row2i] = 0
2265 anythingchanged = True
2266 for primei, prime in enumerate(row2):
2267 if prime:
2268 # Make corresponding entry 0
2269 dommatrix[row2i][primei] = 0
2270 colcount[primei] -= 1
2272 colcache = {}
2274 for coli in range(nl1):
2275 # Still non-dominated?
2276 if colcount[coli]:
2277 if coli in colcache:
2278 col = colcache[coli]
2279 else:
2280 col = [dommatrix[i][coli] for i in range(nterms)]
2281 colcache[coli] = col
2282 for col2i in range(nl1):
2283 # Still non-dominated?
2284 if coli != col2i and colcount[col2i] and (colcount[coli] >= colcount[col2i]):
2285 if col2i in colcache:
2286 col2 = colcache[col2i]
2287 else:
2288 col2 = [dommatrix[i][col2i] for i in range(nterms)]
2289 colcache[col2i] = col2
2290 if all(col[n] >= col2[n] for n in range(nterms)):
2291 # col dominating col2, remove col2
2292 colcount[col2i] = 0
2293 anythingchanged = True
2294 for termi, term in enumerate(col2):
2295 if term and dommatrix[termi][col2i]:
2296 # Make corresponding entry 0
2297 dommatrix[termi][col2i] = 0
2298 rowcount[termi] -= 1
2300 if not anythingchanged:
2301 # Heuristically select the prime implicant covering most terms
2302 maxterms = 0
2303 bestcolidx = -1
2304 for coli in range(nl1):
2305 s = colcount[coli]
2306 if s > maxterms:
2307 bestcolidx = coli
2308 maxterms = s
2310 # In case we found a prime implicant covering at least two terms
2311 if bestcolidx != -1 and maxterms > 1:
2312 for primei, prime in enumerate(l1):
2313 if primei != bestcolidx:
2314 for termi, term in enumerate(colcache[bestcolidx]):
2315 if term and dommatrix[termi][primei]:
2316 # Make corresponding entry 0
2317 dommatrix[termi][primei] = 0
2318 anythingchanged = True
2319 rowcount[termi] -= 1
2320 colcount[primei] -= 1
2322 return [l1[i] for i in range(nl1) if colcount[i]]
2325def _input_to_binlist(inputlist, variables):
2326 binlist = []
2327 bits = len(variables)
2328 for val in inputlist:
2329 if isinstance(val, int):
2330 binlist.append(ibin(val, bits))
2331 elif isinstance(val, dict):
2332 nonspecvars = list(variables)
2333 for key in val.keys():
2334 nonspecvars.remove(key)
2335 for t in product((0, 1), repeat=len(nonspecvars)):
2336 d = dict(zip(nonspecvars, t))
2337 d.update(val)
2338 binlist.append([d[v] for v in variables])
2339 elif isinstance(val, (list, tuple)):
2340 if len(val) != bits:
2341 raise ValueError("Each term must contain {bits} bits as there are"
2342 "\n{bits} variables (or be an integer)."
2343 "".format(bits=bits))
2344 binlist.append(list(val))
2345 else:
2346 raise TypeError("A term list can only contain lists,"
2347 " ints or dicts.")
2348 return binlist
2351def SOPform(variables, minterms, dontcares=None):
2352 """
2353 The SOPform function uses simplified_pairs and a redundant group-
2354 eliminating algorithm to convert the list of all input combos that
2355 generate '1' (the minterms) into the smallest sum-of-products form.
2357 The variables must be given as the first argument.
2359 Return a logical :py:class:`~.Or` function (i.e., the "sum of products" or
2360 "SOP" form) that gives the desired outcome. If there are inputs that can
2361 be ignored, pass them as a list, too.
2363 The result will be one of the (perhaps many) functions that satisfy
2364 the conditions.
2366 Examples
2367 ========
2369 >>> from sympy.logic import SOPform
2370 >>> from sympy import symbols
2371 >>> w, x, y, z = symbols('w x y z')
2372 >>> minterms = [[0, 0, 0, 1], [0, 0, 1, 1],
2373 ... [0, 1, 1, 1], [1, 0, 1, 1], [1, 1, 1, 1]]
2374 >>> dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]]
2375 >>> SOPform([w, x, y, z], minterms, dontcares)
2376 (y & z) | (~w & ~x)
2378 The terms can also be represented as integers:
2380 >>> minterms = [1, 3, 7, 11, 15]
2381 >>> dontcares = [0, 2, 5]
2382 >>> SOPform([w, x, y, z], minterms, dontcares)
2383 (y & z) | (~w & ~x)
2385 They can also be specified using dicts, which does not have to be fully
2386 specified:
2388 >>> minterms = [{w: 0, x: 1}, {y: 1, z: 1, x: 0}]
2389 >>> SOPform([w, x, y, z], minterms)
2390 (x & ~w) | (y & z & ~x)
2392 Or a combination:
2394 >>> minterms = [4, 7, 11, [1, 1, 1, 1]]
2395 >>> dontcares = [{w : 0, x : 0, y: 0}, 5]
2396 >>> SOPform([w, x, y, z], minterms, dontcares)
2397 (w & y & z) | (~w & ~y) | (x & z & ~w)
2399 See also
2400 ========
2402 POSform
2404 References
2405 ==========
2407 .. [1] https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm
2408 .. [2] https://en.wikipedia.org/wiki/Don%27t-care_term
2410 """
2411 if not minterms:
2412 return false
2414 variables = tuple(map(sympify, variables))
2417 minterms = _input_to_binlist(minterms, variables)
2418 dontcares = _input_to_binlist((dontcares or []), variables)
2419 for d in dontcares:
2420 if d in minterms:
2421 raise ValueError('%s in minterms is also in dontcares' % d)
2423 return _sop_form(variables, minterms, dontcares)
2426def _sop_form(variables, minterms, dontcares):
2427 new = _simplified_pairs(minterms + dontcares)
2428 essential = _rem_redundancy(new, minterms)
2429 return Or(*[_convert_to_varsSOP(x, variables) for x in essential])
2432def POSform(variables, minterms, dontcares=None):
2433 """
2434 The POSform function uses simplified_pairs and a redundant-group
2435 eliminating algorithm to convert the list of all input combinations
2436 that generate '1' (the minterms) into the smallest product-of-sums form.
2438 The variables must be given as the first argument.
2440 Return a logical :py:class:`~.And` function (i.e., the "product of sums"
2441 or "POS" form) that gives the desired outcome. If there are inputs that can
2442 be ignored, pass them as a list, too.
2444 The result will be one of the (perhaps many) functions that satisfy
2445 the conditions.
2447 Examples
2448 ========
2450 >>> from sympy.logic import POSform
2451 >>> from sympy import symbols
2452 >>> w, x, y, z = symbols('w x y z')
2453 >>> minterms = [[0, 0, 0, 1], [0, 0, 1, 1], [0, 1, 1, 1],
2454 ... [1, 0, 1, 1], [1, 1, 1, 1]]
2455 >>> dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]]
2456 >>> POSform([w, x, y, z], minterms, dontcares)
2457 z & (y | ~w)
2459 The terms can also be represented as integers:
2461 >>> minterms = [1, 3, 7, 11, 15]
2462 >>> dontcares = [0, 2, 5]
2463 >>> POSform([w, x, y, z], minterms, dontcares)
2464 z & (y | ~w)
2466 They can also be specified using dicts, which does not have to be fully
2467 specified:
2469 >>> minterms = [{w: 0, x: 1}, {y: 1, z: 1, x: 0}]
2470 >>> POSform([w, x, y, z], minterms)
2471 (x | y) & (x | z) & (~w | ~x)
2473 Or a combination:
2475 >>> minterms = [4, 7, 11, [1, 1, 1, 1]]
2476 >>> dontcares = [{w : 0, x : 0, y: 0}, 5]
2477 >>> POSform([w, x, y, z], minterms, dontcares)
2478 (w | x) & (y | ~w) & (z | ~y)
2480 See also
2481 ========
2483 SOPform
2485 References
2486 ==========
2488 .. [1] https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm
2489 .. [2] https://en.wikipedia.org/wiki/Don%27t-care_term
2491 """
2492 if not minterms:
2493 return false
2495 variables = tuple(map(sympify, variables))
2496 minterms = _input_to_binlist(minterms, variables)
2497 dontcares = _input_to_binlist((dontcares or []), variables)
2498 for d in dontcares:
2499 if d in minterms:
2500 raise ValueError('%s in minterms is also in dontcares' % d)
2502 maxterms = []
2503 for t in product((0, 1), repeat=len(variables)):
2504 t = list(t)
2505 if (t not in minterms) and (t not in dontcares):
2506 maxterms.append(t)
2508 new = _simplified_pairs(maxterms + dontcares)
2509 essential = _rem_redundancy(new, maxterms)
2510 return And(*[_convert_to_varsPOS(x, variables) for x in essential])
2513def ANFform(variables, truthvalues):
2514 """
2515 The ANFform function converts the list of truth values to
2516 Algebraic Normal Form (ANF).
2518 The variables must be given as the first argument.
2520 Return True, False, logical :py:class:`~.And` function (i.e., the
2521 "Zhegalkin monomial") or logical :py:class:`~.Xor` function (i.e.,
2522 the "Zhegalkin polynomial"). When True and False
2523 are represented by 1 and 0, respectively, then
2524 :py:class:`~.And` is multiplication and :py:class:`~.Xor` is addition.
2526 Formally a "Zhegalkin monomial" is the product (logical
2527 And) of a finite set of distinct variables, including
2528 the empty set whose product is denoted 1 (True).
2529 A "Zhegalkin polynomial" is the sum (logical Xor) of a
2530 set of Zhegalkin monomials, with the empty set denoted
2531 by 0 (False).
2533 Parameters
2534 ==========
2536 variables : list of variables
2537 truthvalues : list of 1's and 0's (result column of truth table)
2539 Examples
2540 ========
2541 >>> from sympy.logic.boolalg import ANFform
2542 >>> from sympy.abc import x, y
2543 >>> ANFform([x], [1, 0])
2544 x ^ True
2545 >>> ANFform([x, y], [0, 1, 1, 1])
2546 x ^ y ^ (x & y)
2548 References
2549 ==========
2551 .. [1] https://en.wikipedia.org/wiki/Zhegalkin_polynomial
2553 """
2555 n_vars = len(variables)
2556 n_values = len(truthvalues)
2558 if n_values != 2 ** n_vars:
2559 raise ValueError("The number of truth values must be equal to 2^%d, "
2560 "got %d" % (n_vars, n_values))
2562 variables = tuple(map(sympify, variables))
2564 coeffs = anf_coeffs(truthvalues)
2565 terms = []
2567 for i, t in enumerate(product((0, 1), repeat=n_vars)):
2568 if coeffs[i] == 1:
2569 terms.append(t)
2571 return Xor(*[_convert_to_varsANF(x, variables) for x in terms],
2572 remove_true=False)
2575def anf_coeffs(truthvalues):
2576 """
2577 Convert a list of truth values of some boolean expression
2578 to the list of coefficients of the polynomial mod 2 (exclusive
2579 disjunction) representing the boolean expression in ANF
2580 (i.e., the "Zhegalkin polynomial").
2582 There are `2^n` possible Zhegalkin monomials in `n` variables, since
2583 each monomial is fully specified by the presence or absence of
2584 each variable.
2586 We can enumerate all the monomials. For example, boolean
2587 function with four variables ``(a, b, c, d)`` can contain
2588 up to `2^4 = 16` monomials. The 13-th monomial is the
2589 product ``a & b & d``, because 13 in binary is 1, 1, 0, 1.
2591 A given monomial's presence or absence in a polynomial corresponds
2592 to that monomial's coefficient being 1 or 0 respectively.
2594 Examples
2595 ========
2596 >>> from sympy.logic.boolalg import anf_coeffs, bool_monomial, Xor
2597 >>> from sympy.abc import a, b, c
2598 >>> truthvalues = [0, 1, 1, 0, 0, 1, 0, 1]
2599 >>> coeffs = anf_coeffs(truthvalues)
2600 >>> coeffs
2601 [0, 1, 1, 0, 0, 0, 1, 0]
2602 >>> polynomial = Xor(*[
2603 ... bool_monomial(k, [a, b, c])
2604 ... for k, coeff in enumerate(coeffs) if coeff == 1
2605 ... ])
2606 >>> polynomial
2607 b ^ c ^ (a & b)
2609 """
2611 s = '{:b}'.format(len(truthvalues))
2612 n = len(s) - 1
2614 if len(truthvalues) != 2**n:
2615 raise ValueError("The number of truth values must be a power of two, "
2616 "got %d" % len(truthvalues))
2618 coeffs = [[v] for v in truthvalues]
2620 for i in range(n):
2621 tmp = []
2622 for j in range(2 ** (n-i-1)):
2623 tmp.append(coeffs[2*j] +
2624 list(map(lambda x, y: x^y, coeffs[2*j], coeffs[2*j+1])))
2625 coeffs = tmp
2627 return coeffs[0]
2630def bool_minterm(k, variables):
2631 """
2632 Return the k-th minterm.
2634 Minterms are numbered by a binary encoding of the complementation
2635 pattern of the variables. This convention assigns the value 1 to
2636 the direct form and 0 to the complemented form.
2638 Parameters
2639 ==========
2641 k : int or list of 1's and 0's (complementation pattern)
2642 variables : list of variables
2644 Examples
2645 ========
2647 >>> from sympy.logic.boolalg import bool_minterm
2648 >>> from sympy.abc import x, y, z
2649 >>> bool_minterm([1, 0, 1], [x, y, z])
2650 x & z & ~y
2651 >>> bool_minterm(6, [x, y, z])
2652 x & y & ~z
2654 References
2655 ==========
2657 .. [1] https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_minterms
2659 """
2660 if isinstance(k, int):
2661 k = ibin(k, len(variables))
2662 variables = tuple(map(sympify, variables))
2663 return _convert_to_varsSOP(k, variables)
2666def bool_maxterm(k, variables):
2667 """
2668 Return the k-th maxterm.
2670 Each maxterm is assigned an index based on the opposite
2671 conventional binary encoding used for minterms. The maxterm
2672 convention assigns the value 0 to the direct form and 1 to
2673 the complemented form.
2675 Parameters
2676 ==========
2678 k : int or list of 1's and 0's (complementation pattern)
2679 variables : list of variables
2681 Examples
2682 ========
2683 >>> from sympy.logic.boolalg import bool_maxterm
2684 >>> from sympy.abc import x, y, z
2685 >>> bool_maxterm([1, 0, 1], [x, y, z])
2686 y | ~x | ~z
2687 >>> bool_maxterm(6, [x, y, z])
2688 z | ~x | ~y
2690 References
2691 ==========
2693 .. [1] https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_maxterms
2695 """
2696 if isinstance(k, int):
2697 k = ibin(k, len(variables))
2698 variables = tuple(map(sympify, variables))
2699 return _convert_to_varsPOS(k, variables)
2702def bool_monomial(k, variables):
2703 """
2704 Return the k-th monomial.
2706 Monomials are numbered by a binary encoding of the presence and
2707 absences of the variables. This convention assigns the value
2708 1 to the presence of variable and 0 to the absence of variable.
2710 Each boolean function can be uniquely represented by a
2711 Zhegalkin Polynomial (Algebraic Normal Form). The Zhegalkin
2712 Polynomial of the boolean function with `n` variables can contain
2713 up to `2^n` monomials. We can enumerate all the monomials.
2714 Each monomial is fully specified by the presence or absence
2715 of each variable.
2717 For example, boolean function with four variables ``(a, b, c, d)``
2718 can contain up to `2^4 = 16` monomials. The 13-th monomial is the
2719 product ``a & b & d``, because 13 in binary is 1, 1, 0, 1.
2721 Parameters
2722 ==========
2724 k : int or list of 1's and 0's
2725 variables : list of variables
2727 Examples
2728 ========
2729 >>> from sympy.logic.boolalg import bool_monomial
2730 >>> from sympy.abc import x, y, z
2731 >>> bool_monomial([1, 0, 1], [x, y, z])
2732 x & z
2733 >>> bool_monomial(6, [x, y, z])
2734 x & y
2736 """
2737 if isinstance(k, int):
2738 k = ibin(k, len(variables))
2739 variables = tuple(map(sympify, variables))
2740 return _convert_to_varsANF(k, variables)
2743def _find_predicates(expr):
2744 """Helper to find logical predicates in BooleanFunctions.
2746 A logical predicate is defined here as anything within a BooleanFunction
2747 that is not a BooleanFunction itself.
2749 """
2750 if not isinstance(expr, BooleanFunction):
2751 return {expr}
2752 return set().union(*(map(_find_predicates, expr.args)))
2755def simplify_logic(expr, form=None, deep=True, force=False, dontcare=None):
2756 """
2757 This function simplifies a boolean function to its simplified version
2758 in SOP or POS form. The return type is an :py:class:`~.Or` or
2759 :py:class:`~.And` object in SymPy.
2761 Parameters
2762 ==========
2764 expr : Boolean
2766 form : string (``'cnf'`` or ``'dnf'``) or ``None`` (default).
2767 If ``'cnf'`` or ``'dnf'``, the simplest expression in the corresponding
2768 normal form is returned; if ``None``, the answer is returned
2769 according to the form with fewest args (in CNF by default).
2771 deep : bool (default ``True``)
2772 Indicates whether to recursively simplify any
2773 non-boolean functions contained within the input.
2775 force : bool (default ``False``)
2776 As the simplifications require exponential time in the number
2777 of variables, there is by default a limit on expressions with
2778 8 variables. When the expression has more than 8 variables
2779 only symbolical simplification (controlled by ``deep``) is
2780 made. By setting ``force`` to ``True``, this limit is removed. Be
2781 aware that this can lead to very long simplification times.
2783 dontcare : Boolean
2784 Optimize expression under the assumption that inputs where this
2785 expression is true are don't care. This is useful in e.g. Piecewise
2786 conditions, where later conditions do not need to consider inputs that
2787 are converted by previous conditions. For example, if a previous
2788 condition is ``And(A, B)``, the simplification of expr can be made
2789 with don't cares for ``And(A, B)``.
2791 Examples
2792 ========
2794 >>> from sympy.logic import simplify_logic
2795 >>> from sympy.abc import x, y, z
2796 >>> b = (~x & ~y & ~z) | ( ~x & ~y & z)
2797 >>> simplify_logic(b)
2798 ~x & ~y
2799 >>> simplify_logic(x | y, dontcare=y)
2800 x
2802 References
2803 ==========
2805 .. [1] https://en.wikipedia.org/wiki/Don%27t-care_term
2807 """
2809 if form not in (None, 'cnf', 'dnf'):
2810 raise ValueError("form can be cnf or dnf only")
2811 expr = sympify(expr)
2812 # check for quick exit if form is given: right form and all args are
2813 # literal and do not involve Not
2814 if form:
2815 form_ok = False
2816 if form == 'cnf':
2817 form_ok = is_cnf(expr)
2818 elif form == 'dnf':
2819 form_ok = is_dnf(expr)
2821 if form_ok and all(is_literal(a)
2822 for a in expr.args):
2823 return expr
2824 from sympy.core.relational import Relational
2825 if deep:
2826 variables = expr.atoms(Relational)
2827 from sympy.simplify.simplify import simplify
2828 s = tuple(map(simplify, variables))
2829 expr = expr.xreplace(dict(zip(variables, s)))
2830 if not isinstance(expr, BooleanFunction):
2831 return expr
2832 # Replace Relationals with Dummys to possibly
2833 # reduce the number of variables
2834 repl = {}
2835 undo = {}
2836 from sympy.core.symbol import Dummy
2837 variables = expr.atoms(Relational)
2838 if dontcare is not None:
2839 dontcare = sympify(dontcare)
2840 variables.update(dontcare.atoms(Relational))
2841 while variables:
2842 var = variables.pop()
2843 if var.is_Relational:
2844 d = Dummy()
2845 undo[d] = var
2846 repl[var] = d
2847 nvar = var.negated
2848 if nvar in variables:
2849 repl[nvar] = Not(d)
2850 variables.remove(nvar)
2852 expr = expr.xreplace(repl)
2854 if dontcare is not None:
2855 dontcare = dontcare.xreplace(repl)
2857 # Get new variables after replacing
2858 variables = _find_predicates(expr)
2859 if not force and len(variables) > 8:
2860 return expr.xreplace(undo)
2861 if dontcare is not None:
2862 # Add variables from dontcare
2863 dcvariables = _find_predicates(dontcare)
2864 variables.update(dcvariables)
2865 # if too many restore to variables only
2866 if not force and len(variables) > 8:
2867 variables = _find_predicates(expr)
2868 dontcare = None
2869 # group into constants and variable values
2870 c, v = sift(ordered(variables), lambda x: x in (True, False), binary=True)
2871 variables = c + v
2872 # standardize constants to be 1 or 0 in keeping with truthtable
2873 c = [1 if i == True else 0 for i in c]
2874 truthtable = _get_truthtable(v, expr, c)
2875 if dontcare is not None:
2876 dctruthtable = _get_truthtable(v, dontcare, c)
2877 truthtable = [t for t in truthtable if t not in dctruthtable]
2878 else:
2879 dctruthtable = []
2880 big = len(truthtable) >= (2 ** (len(variables) - 1))
2881 if form == 'dnf' or form is None and big:
2882 return _sop_form(variables, truthtable, dctruthtable).xreplace(undo)
2883 return POSform(variables, truthtable, dctruthtable).xreplace(undo)
2886def _get_truthtable(variables, expr, const):
2887 """ Return a list of all combinations leading to a True result for ``expr``.
2888 """
2889 _variables = variables.copy()
2890 def _get_tt(inputs):
2891 if _variables:
2892 v = _variables.pop()
2893 tab = [[i[0].xreplace({v: false}), [0] + i[1]] for i in inputs if i[0] is not false]
2894 tab.extend([[i[0].xreplace({v: true}), [1] + i[1]] for i in inputs if i[0] is not false])
2895 return _get_tt(tab)
2896 return inputs
2897 res = [const + k[1] for k in _get_tt([[expr, []]]) if k[0]]
2898 if res == [[]]:
2899 return []
2900 else:
2901 return res
2904def _finger(eq):
2905 """
2906 Assign a 5-item fingerprint to each symbol in the equation:
2907 [
2908 # of times it appeared as a Symbol;
2909 # of times it appeared as a Not(symbol);
2910 # of times it appeared as a Symbol in an And or Or;
2911 # of times it appeared as a Not(Symbol) in an And or Or;
2912 a sorted tuple of tuples, (i, j, k), where i is the number of arguments
2913 in an And or Or with which it appeared as a Symbol, and j is
2914 the number of arguments that were Not(Symbol); k is the number
2915 of times that (i, j) was seen.
2916 ]
2918 Examples
2919 ========
2921 >>> from sympy.logic.boolalg import _finger as finger
2922 >>> from sympy import And, Or, Not, Xor, to_cnf, symbols
2923 >>> from sympy.abc import a, b, x, y
2924 >>> eq = Or(And(Not(y), a), And(Not(y), b), And(x, y))
2925 >>> dict(finger(eq))
2926 {(0, 0, 1, 0, ((2, 0, 1),)): [x],
2927 (0, 0, 1, 0, ((2, 1, 1),)): [a, b],
2928 (0, 0, 1, 2, ((2, 0, 1),)): [y]}
2929 >>> dict(finger(x & ~y))
2930 {(0, 1, 0, 0, ()): [y], (1, 0, 0, 0, ()): [x]}
2932 In the following, the (5, 2, 6) means that there were 6 Or
2933 functions in which a symbol appeared as itself amongst 5 arguments in
2934 which there were also 2 negated symbols, e.g. ``(a0 | a1 | a2 | ~a3 | ~a4)``
2935 is counted once for a0, a1 and a2.
2937 >>> dict(finger(to_cnf(Xor(*symbols('a:5')))))
2938 {(0, 0, 8, 8, ((5, 0, 1), (5, 2, 6), (5, 4, 1))): [a0, a1, a2, a3, a4]}
2940 The equation must not have more than one level of nesting:
2942 >>> dict(finger(And(Or(x, y), y)))
2943 {(0, 0, 1, 0, ((2, 0, 1),)): [x], (1, 0, 1, 0, ((2, 0, 1),)): [y]}
2944 >>> dict(finger(And(Or(x, And(a, x)), y)))
2945 Traceback (most recent call last):
2946 ...
2947 NotImplementedError: unexpected level of nesting
2949 So y and x have unique fingerprints, but a and b do not.
2950 """
2951 f = eq.free_symbols
2952 d = dict(list(zip(f, [[0]*4 + [defaultdict(int)] for fi in f])))
2953 for a in eq.args:
2954 if a.is_Symbol:
2955 d[a][0] += 1
2956 elif a.is_Not:
2957 d[a.args[0]][1] += 1
2958 else:
2959 o = len(a.args), sum(isinstance(ai, Not) for ai in a.args)
2960 for ai in a.args:
2961 if ai.is_Symbol:
2962 d[ai][2] += 1
2963 d[ai][-1][o] += 1
2964 elif ai.is_Not:
2965 d[ai.args[0]][3] += 1
2966 else:
2967 raise NotImplementedError('unexpected level of nesting')
2968 inv = defaultdict(list)
2969 for k, v in ordered(iter(d.items())):
2970 v[-1] = tuple(sorted([i + (j,) for i, j in v[-1].items()]))
2971 inv[tuple(v)].append(k)
2972 return inv
2975def bool_map(bool1, bool2):
2976 """
2977 Return the simplified version of *bool1*, and the mapping of variables
2978 that makes the two expressions *bool1* and *bool2* represent the same
2979 logical behaviour for some correspondence between the variables
2980 of each.
2981 If more than one mappings of this sort exist, one of them
2982 is returned.
2984 For example, ``And(x, y)`` is logically equivalent to ``And(a, b)`` for
2985 the mapping ``{x: a, y: b}`` or ``{x: b, y: a}``.
2986 If no such mapping exists, return ``False``.
2988 Examples
2989 ========
2991 >>> from sympy import SOPform, bool_map, Or, And, Not, Xor
2992 >>> from sympy.abc import w, x, y, z, a, b, c, d
2993 >>> function1 = SOPform([x, z, y],[[1, 0, 1], [0, 0, 1]])
2994 >>> function2 = SOPform([a, b, c],[[1, 0, 1], [1, 0, 0]])
2995 >>> bool_map(function1, function2)
2996 (y & ~z, {y: a, z: b})
2998 The results are not necessarily unique, but they are canonical. Here,
2999 ``(w, z)`` could be ``(a, d)`` or ``(d, a)``:
3001 >>> eq = Or(And(Not(y), w), And(Not(y), z), And(x, y))
3002 >>> eq2 = Or(And(Not(c), a), And(Not(c), d), And(b, c))
3003 >>> bool_map(eq, eq2)
3004 ((x & y) | (w & ~y) | (z & ~y), {w: a, x: b, y: c, z: d})
3005 >>> eq = And(Xor(a, b), c, And(c,d))
3006 >>> bool_map(eq, eq.subs(c, x))
3007 (c & d & (a | b) & (~a | ~b), {a: a, b: b, c: d, d: x})
3009 """
3011 def match(function1, function2):
3012 """Return the mapping that equates variables between two
3013 simplified boolean expressions if possible.
3015 By "simplified" we mean that a function has been denested
3016 and is either an And (or an Or) whose arguments are either
3017 symbols (x), negated symbols (Not(x)), or Or (or an And) whose
3018 arguments are only symbols or negated symbols. For example,
3019 ``And(x, Not(y), Or(w, Not(z)))``.
3021 Basic.match is not robust enough (see issue 4835) so this is
3022 a workaround that is valid for simplified boolean expressions
3023 """
3025 # do some quick checks
3026 if function1.__class__ != function2.__class__:
3027 return None # maybe simplification makes them the same?
3028 if len(function1.args) != len(function2.args):
3029 return None # maybe simplification makes them the same?
3030 if function1.is_Symbol:
3031 return {function1: function2}
3033 # get the fingerprint dictionaries
3034 f1 = _finger(function1)
3035 f2 = _finger(function2)
3037 # more quick checks
3038 if len(f1) != len(f2):
3039 return False
3041 # assemble the match dictionary if possible
3042 matchdict = {}
3043 for k in f1.keys():
3044 if k not in f2:
3045 return False
3046 if len(f1[k]) != len(f2[k]):
3047 return False
3048 for i, x in enumerate(f1[k]):
3049 matchdict[x] = f2[k][i]
3050 return matchdict
3052 a = simplify_logic(bool1)
3053 b = simplify_logic(bool2)
3054 m = match(a, b)
3055 if m:
3056 return a, m
3057 return m
3060def _apply_patternbased_simplification(rv, patterns, measure,
3061 dominatingvalue,
3062 replacementvalue=None,
3063 threeterm_patterns=None):
3064 """
3065 Replace patterns of Relational
3067 Parameters
3068 ==========
3070 rv : Expr
3071 Boolean expression
3073 patterns : tuple
3074 Tuple of tuples, with (pattern to simplify, simplified pattern) with
3075 two terms.
3077 measure : function
3078 Simplification measure.
3080 dominatingvalue : Boolean or ``None``
3081 The dominating value for the function of consideration.
3082 For example, for :py:class:`~.And` ``S.false`` is dominating.
3083 As soon as one expression is ``S.false`` in :py:class:`~.And`,
3084 the whole expression is ``S.false``.
3086 replacementvalue : Boolean or ``None``, optional
3087 The resulting value for the whole expression if one argument
3088 evaluates to ``dominatingvalue``.
3089 For example, for :py:class:`~.Nand` ``S.false`` is dominating, but
3090 in this case the resulting value is ``S.true``. Default is ``None``.
3091 If ``replacementvalue`` is ``None`` and ``dominatingvalue`` is not
3092 ``None``, ``replacementvalue = dominatingvalue``.
3094 threeterm_patterns : tuple, optional
3095 Tuple of tuples, with (pattern to simplify, simplified pattern) with
3096 three terms.
3098 """
3099 from sympy.core.relational import Relational, _canonical
3101 if replacementvalue is None and dominatingvalue is not None:
3102 replacementvalue = dominatingvalue
3103 # Use replacement patterns for Relationals
3104 Rel, nonRel = sift(rv.args, lambda i: isinstance(i, Relational),
3105 binary=True)
3106 if len(Rel) <= 1:
3107 return rv
3108 Rel, nonRealRel = sift(Rel, lambda i: not any(s.is_real is False
3109 for s in i.free_symbols),
3110 binary=True)
3111 Rel = [i.canonical for i in Rel]
3113 if threeterm_patterns and len(Rel) >= 3:
3114 Rel = _apply_patternbased_threeterm_simplification(Rel,
3115 threeterm_patterns, rv.func, dominatingvalue,
3116 replacementvalue, measure)
3118 Rel = _apply_patternbased_twoterm_simplification(Rel, patterns,
3119 rv.func, dominatingvalue, replacementvalue, measure)
3121 rv = rv.func(*([_canonical(i) for i in ordered(Rel)]
3122 + nonRel + nonRealRel))
3123 return rv
3126def _apply_patternbased_twoterm_simplification(Rel, patterns, func,
3127 dominatingvalue,
3128 replacementvalue,
3129 measure):
3130 """ Apply pattern-based two-term simplification."""
3131 from sympy.functions.elementary.miscellaneous import Min, Max
3132 from sympy.core.relational import Ge, Gt, _Inequality
3133 changed = True
3134 while changed and len(Rel) >= 2:
3135 changed = False
3136 # Use only < or <=
3137 Rel = [r.reversed if isinstance(r, (Ge, Gt)) else r for r in Rel]
3138 # Sort based on ordered
3139 Rel = list(ordered(Rel))
3140 # Eq and Ne must be tested reversed as well
3141 rtmp = [(r, ) if isinstance(r, _Inequality) else (r, r.reversed) for r in Rel]
3142 # Create a list of possible replacements
3143 results = []
3144 # Try all combinations of possibly reversed relational
3145 for ((i, pi), (j, pj)) in combinations(enumerate(rtmp), 2):
3146 for pattern, simp in patterns:
3147 res = []
3148 for p1, p2 in product(pi, pj):
3149 # use SymPy matching
3150 oldexpr = Tuple(p1, p2)
3151 tmpres = oldexpr.match(pattern)
3152 if tmpres:
3153 res.append((tmpres, oldexpr))
3155 if res:
3156 for tmpres, oldexpr in res:
3157 # we have a matching, compute replacement
3158 np = simp.xreplace(tmpres)
3159 if np == dominatingvalue:
3160 # if dominatingvalue, the whole expression
3161 # will be replacementvalue
3162 return [replacementvalue]
3163 # add replacement
3164 if not isinstance(np, ITE) and not np.has(Min, Max):
3165 # We only want to use ITE and Min/Max replacements if
3166 # they simplify to a relational
3167 costsaving = measure(func(*oldexpr.args)) - measure(np)
3168 if costsaving > 0:
3169 results.append((costsaving, ([i, j], np)))
3170 if results:
3171 # Sort results based on complexity
3172 results = sorted(results,
3173 key=lambda pair: pair[0], reverse=True)
3174 # Replace the one providing most simplification
3175 replacement = results[0][1]
3176 idx, newrel = replacement
3177 idx.sort()
3178 # Remove the old relationals
3179 for index in reversed(idx):
3180 del Rel[index]
3181 if dominatingvalue is None or newrel != Not(dominatingvalue):
3182 # Insert the new one (no need to insert a value that will
3183 # not affect the result)
3184 if newrel.func == func:
3185 for a in newrel.args:
3186 Rel.append(a)
3187 else:
3188 Rel.append(newrel)
3189 # We did change something so try again
3190 changed = True
3191 return Rel
3194def _apply_patternbased_threeterm_simplification(Rel, patterns, func,
3195 dominatingvalue,
3196 replacementvalue,
3197 measure):
3198 """ Apply pattern-based three-term simplification."""
3199 from sympy.functions.elementary.miscellaneous import Min, Max
3200 from sympy.core.relational import Le, Lt, _Inequality
3201 changed = True
3202 while changed and len(Rel) >= 3:
3203 changed = False
3204 # Use only > or >=
3205 Rel = [r.reversed if isinstance(r, (Le, Lt)) else r for r in Rel]
3206 # Sort based on ordered
3207 Rel = list(ordered(Rel))
3208 # Create a list of possible replacements
3209 results = []
3210 # Eq and Ne must be tested reversed as well
3211 rtmp = [(r, ) if isinstance(r, _Inequality) else (r, r.reversed) for r in Rel]
3212 # Try all combinations of possibly reversed relational
3213 for ((i, pi), (j, pj), (k, pk)) in permutations(enumerate(rtmp), 3):
3214 for pattern, simp in patterns:
3215 res = []
3216 for p1, p2, p3 in product(pi, pj, pk):
3217 # use SymPy matching
3218 oldexpr = Tuple(p1, p2, p3)
3219 tmpres = oldexpr.match(pattern)
3220 if tmpres:
3221 res.append((tmpres, oldexpr))
3223 if res:
3224 for tmpres, oldexpr in res:
3225 # we have a matching, compute replacement
3226 np = simp.xreplace(tmpres)
3227 if np == dominatingvalue:
3228 # if dominatingvalue, the whole expression
3229 # will be replacementvalue
3230 return [replacementvalue]
3231 # add replacement
3232 if not isinstance(np, ITE) and not np.has(Min, Max):
3233 # We only want to use ITE and Min/Max replacements if
3234 # they simplify to a relational
3235 costsaving = measure(func(*oldexpr.args)) - measure(np)
3236 if costsaving > 0:
3237 results.append((costsaving, ([i, j, k], np)))
3238 if results:
3239 # Sort results based on complexity
3240 results = sorted(results,
3241 key=lambda pair: pair[0], reverse=True)
3242 # Replace the one providing most simplification
3243 replacement = results[0][1]
3244 idx, newrel = replacement
3245 idx.sort()
3246 # Remove the old relationals
3247 for index in reversed(idx):
3248 del Rel[index]
3249 if dominatingvalue is None or newrel != Not(dominatingvalue):
3250 # Insert the new one (no need to insert a value that will
3251 # not affect the result)
3252 if newrel.func == func:
3253 for a in newrel.args:
3254 Rel.append(a)
3255 else:
3256 Rel.append(newrel)
3257 # We did change something so try again
3258 changed = True
3259 return Rel
3262@cacheit
3263def _simplify_patterns_and():
3264 """ Two-term patterns for And."""
3266 from sympy.core import Wild
3267 from sympy.core.relational import Eq, Ne, Ge, Gt, Le, Lt
3268 from sympy.functions.elementary.complexes import Abs
3269 from sympy.functions.elementary.miscellaneous import Min, Max
3270 a = Wild('a')
3271 b = Wild('b')
3272 c = Wild('c')
3273 # Relationals patterns should be in alphabetical order
3274 # (pattern1, pattern2, simplified)
3275 # Do not use Ge, Gt
3276 _matchers_and = ((Tuple(Eq(a, b), Lt(a, b)), false),
3277 #(Tuple(Eq(a, b), Lt(b, a)), S.false),
3278 #(Tuple(Le(b, a), Lt(a, b)), S.false),
3279 #(Tuple(Lt(b, a), Le(a, b)), S.false),
3280 (Tuple(Lt(b, a), Lt(a, b)), false),
3281 (Tuple(Eq(a, b), Le(b, a)), Eq(a, b)),
3282 #(Tuple(Eq(a, b), Le(a, b)), Eq(a, b)),
3283 #(Tuple(Le(b, a), Lt(b, a)), Gt(a, b)),
3284 (Tuple(Le(b, a), Le(a, b)), Eq(a, b)),
3285 #(Tuple(Le(b, a), Ne(a, b)), Gt(a, b)),
3286 #(Tuple(Lt(b, a), Ne(a, b)), Gt(a, b)),
3287 (Tuple(Le(a, b), Lt(a, b)), Lt(a, b)),
3288 (Tuple(Le(a, b), Ne(a, b)), Lt(a, b)),
3289 (Tuple(Lt(a, b), Ne(a, b)), Lt(a, b)),
3290 # Sign
3291 (Tuple(Eq(a, b), Eq(a, -b)), And(Eq(a, S.Zero), Eq(b, S.Zero))),
3292 # Min/Max/ITE
3293 (Tuple(Le(b, a), Le(c, a)), Ge(a, Max(b, c))),
3294 (Tuple(Le(b, a), Lt(c, a)), ITE(b > c, Ge(a, b), Gt(a, c))),
3295 (Tuple(Lt(b, a), Lt(c, a)), Gt(a, Max(b, c))),
3296 (Tuple(Le(a, b), Le(a, c)), Le(a, Min(b, c))),
3297 (Tuple(Le(a, b), Lt(a, c)), ITE(b < c, Le(a, b), Lt(a, c))),
3298 (Tuple(Lt(a, b), Lt(a, c)), Lt(a, Min(b, c))),
3299 (Tuple(Le(a, b), Le(c, a)), ITE(Eq(b, c), Eq(a, b), ITE(b < c, false, And(Le(a, b), Ge(a, c))))),
3300 (Tuple(Le(c, a), Le(a, b)), ITE(Eq(b, c), Eq(a, b), ITE(b < c, false, And(Le(a, b), Ge(a, c))))),
3301 (Tuple(Lt(a, b), Lt(c, a)), ITE(b < c, false, And(Lt(a, b), Gt(a, c)))),
3302 (Tuple(Lt(c, a), Lt(a, b)), ITE(b < c, false, And(Lt(a, b), Gt(a, c)))),
3303 (Tuple(Le(a, b), Lt(c, a)), ITE(b <= c, false, And(Le(a, b), Gt(a, c)))),
3304 (Tuple(Le(c, a), Lt(a, b)), ITE(b <= c, false, And(Lt(a, b), Ge(a, c)))),
3305 (Tuple(Eq(a, b), Eq(a, c)), ITE(Eq(b, c), Eq(a, b), false)),
3306 (Tuple(Lt(a, b), Lt(-b, a)), ITE(b > 0, Lt(Abs(a), b), false)),
3307 (Tuple(Le(a, b), Le(-b, a)), ITE(b >= 0, Le(Abs(a), b), false)),
3308 )
3309 return _matchers_and
3312@cacheit
3313def _simplify_patterns_and3():
3314 """ Three-term patterns for And."""
3316 from sympy.core import Wild
3317 from sympy.core.relational import Eq, Ge, Gt
3319 a = Wild('a')
3320 b = Wild('b')
3321 c = Wild('c')
3322 # Relationals patterns should be in alphabetical order
3323 # (pattern1, pattern2, pattern3, simplified)
3324 # Do not use Le, Lt
3325 _matchers_and = ((Tuple(Ge(a, b), Ge(b, c), Gt(c, a)), false),
3326 (Tuple(Ge(a, b), Gt(b, c), Gt(c, a)), false),
3327 (Tuple(Gt(a, b), Gt(b, c), Gt(c, a)), false),
3328 # (Tuple(Ge(c, a), Gt(a, b), Gt(b, c)), S.false),
3329 # Lower bound relations
3330 # Commented out combinations that does not simplify
3331 (Tuple(Ge(a, b), Ge(a, c), Ge(b, c)), And(Ge(a, b), Ge(b, c))),
3332 (Tuple(Ge(a, b), Ge(a, c), Gt(b, c)), And(Ge(a, b), Gt(b, c))),
3333 # (Tuple(Ge(a, b), Gt(a, c), Ge(b, c)), And(Ge(a, b), Ge(b, c))),
3334 (Tuple(Ge(a, b), Gt(a, c), Gt(b, c)), And(Ge(a, b), Gt(b, c))),
3335 # (Tuple(Gt(a, b), Ge(a, c), Ge(b, c)), And(Gt(a, b), Ge(b, c))),
3336 (Tuple(Ge(a, c), Gt(a, b), Gt(b, c)), And(Gt(a, b), Gt(b, c))),
3337 (Tuple(Ge(b, c), Gt(a, b), Gt(a, c)), And(Gt(a, b), Ge(b, c))),
3338 (Tuple(Gt(a, b), Gt(a, c), Gt(b, c)), And(Gt(a, b), Gt(b, c))),
3339 # Upper bound relations
3340 # Commented out combinations that does not simplify
3341 (Tuple(Ge(b, a), Ge(c, a), Ge(b, c)), And(Ge(c, a), Ge(b, c))),
3342 (Tuple(Ge(b, a), Ge(c, a), Gt(b, c)), And(Ge(c, a), Gt(b, c))),
3343 # (Tuple(Ge(b, a), Gt(c, a), Ge(b, c)), And(Gt(c, a), Ge(b, c))),
3344 (Tuple(Ge(b, a), Gt(c, a), Gt(b, c)), And(Gt(c, a), Gt(b, c))),
3345 # (Tuple(Gt(b, a), Ge(c, a), Ge(b, c)), And(Ge(c, a), Ge(b, c))),
3346 (Tuple(Ge(c, a), Gt(b, a), Gt(b, c)), And(Ge(c, a), Gt(b, c))),
3347 (Tuple(Ge(b, c), Gt(b, a), Gt(c, a)), And(Gt(c, a), Ge(b, c))),
3348 (Tuple(Gt(b, a), Gt(c, a), Gt(b, c)), And(Gt(c, a), Gt(b, c))),
3349 # Circular relation
3350 (Tuple(Ge(a, b), Ge(b, c), Ge(c, a)), And(Eq(a, b), Eq(b, c))),
3351 )
3352 return _matchers_and
3355@cacheit
3356def _simplify_patterns_or():
3357 """ Two-term patterns for Or."""
3359 from sympy.core import Wild
3360 from sympy.core.relational import Eq, Ne, Ge, Gt, Le, Lt
3361 from sympy.functions.elementary.complexes import Abs
3362 from sympy.functions.elementary.miscellaneous import Min, Max
3363 a = Wild('a')
3364 b = Wild('b')
3365 c = Wild('c')
3366 # Relationals patterns should be in alphabetical order
3367 # (pattern1, pattern2, simplified)
3368 # Do not use Ge, Gt
3369 _matchers_or = ((Tuple(Le(b, a), Le(a, b)), true),
3370 #(Tuple(Le(b, a), Lt(a, b)), true),
3371 (Tuple(Le(b, a), Ne(a, b)), true),
3372 #(Tuple(Le(a, b), Lt(b, a)), true),
3373 #(Tuple(Le(a, b), Ne(a, b)), true),
3374 #(Tuple(Eq(a, b), Le(b, a)), Ge(a, b)),
3375 #(Tuple(Eq(a, b), Lt(b, a)), Ge(a, b)),
3376 (Tuple(Eq(a, b), Le(a, b)), Le(a, b)),
3377 (Tuple(Eq(a, b), Lt(a, b)), Le(a, b)),
3378 #(Tuple(Le(b, a), Lt(b, a)), Ge(a, b)),
3379 (Tuple(Lt(b, a), Lt(a, b)), Ne(a, b)),
3380 (Tuple(Lt(b, a), Ne(a, b)), Ne(a, b)),
3381 (Tuple(Le(a, b), Lt(a, b)), Le(a, b)),
3382 #(Tuple(Lt(a, b), Ne(a, b)), Ne(a, b)),
3383 (Tuple(Eq(a, b), Ne(a, c)), ITE(Eq(b, c), true, Ne(a, c))),
3384 (Tuple(Ne(a, b), Ne(a, c)), ITE(Eq(b, c), Ne(a, b), true)),
3385 # Min/Max/ITE
3386 (Tuple(Le(b, a), Le(c, a)), Ge(a, Min(b, c))),
3387 #(Tuple(Ge(b, a), Ge(c, a)), Ge(Min(b, c), a)),
3388 (Tuple(Le(b, a), Lt(c, a)), ITE(b > c, Lt(c, a), Le(b, a))),
3389 (Tuple(Lt(b, a), Lt(c, a)), Gt(a, Min(b, c))),
3390 #(Tuple(Gt(b, a), Gt(c, a)), Gt(Min(b, c), a)),
3391 (Tuple(Le(a, b), Le(a, c)), Le(a, Max(b, c))),
3392 #(Tuple(Le(b, a), Le(c, a)), Le(Max(b, c), a)),
3393 (Tuple(Le(a, b), Lt(a, c)), ITE(b >= c, Le(a, b), Lt(a, c))),
3394 (Tuple(Lt(a, b), Lt(a, c)), Lt(a, Max(b, c))),
3395 #(Tuple(Lt(b, a), Lt(c, a)), Lt(Max(b, c), a)),
3396 (Tuple(Le(a, b), Le(c, a)), ITE(b >= c, true, Or(Le(a, b), Ge(a, c)))),
3397 (Tuple(Le(c, a), Le(a, b)), ITE(b >= c, true, Or(Le(a, b), Ge(a, c)))),
3398 (Tuple(Lt(a, b), Lt(c, a)), ITE(b > c, true, Or(Lt(a, b), Gt(a, c)))),
3399 (Tuple(Lt(c, a), Lt(a, b)), ITE(b > c, true, Or(Lt(a, b), Gt(a, c)))),
3400 (Tuple(Le(a, b), Lt(c, a)), ITE(b >= c, true, Or(Le(a, b), Gt(a, c)))),
3401 (Tuple(Le(c, a), Lt(a, b)), ITE(b >= c, true, Or(Lt(a, b), Ge(a, c)))),
3402 (Tuple(Lt(b, a), Lt(a, -b)), ITE(b >= 0, Gt(Abs(a), b), true)),
3403 (Tuple(Le(b, a), Le(a, -b)), ITE(b > 0, Ge(Abs(a), b), true)),
3404 )
3405 return _matchers_or
3408@cacheit
3409def _simplify_patterns_xor():
3410 """ Two-term patterns for Xor."""
3412 from sympy.functions.elementary.miscellaneous import Min, Max
3413 from sympy.core import Wild
3414 from sympy.core.relational import Eq, Ne, Ge, Gt, Le, Lt
3415 a = Wild('a')
3416 b = Wild('b')
3417 c = Wild('c')
3418 # Relationals patterns should be in alphabetical order
3419 # (pattern1, pattern2, simplified)
3420 # Do not use Ge, Gt
3421 _matchers_xor = (#(Tuple(Le(b, a), Lt(a, b)), true),
3422 #(Tuple(Lt(b, a), Le(a, b)), true),
3423 #(Tuple(Eq(a, b), Le(b, a)), Gt(a, b)),
3424 #(Tuple(Eq(a, b), Lt(b, a)), Ge(a, b)),
3425 (Tuple(Eq(a, b), Le(a, b)), Lt(a, b)),
3426 (Tuple(Eq(a, b), Lt(a, b)), Le(a, b)),
3427 (Tuple(Le(a, b), Lt(a, b)), Eq(a, b)),
3428 (Tuple(Le(a, b), Le(b, a)), Ne(a, b)),
3429 (Tuple(Le(b, a), Ne(a, b)), Le(a, b)),
3430 # (Tuple(Lt(b, a), Lt(a, b)), Ne(a, b)),
3431 (Tuple(Lt(b, a), Ne(a, b)), Lt(a, b)),
3432 # (Tuple(Le(a, b), Lt(a, b)), Eq(a, b)),
3433 # (Tuple(Le(a, b), Ne(a, b)), Ge(a, b)),
3434 # (Tuple(Lt(a, b), Ne(a, b)), Gt(a, b)),
3435 # Min/Max/ITE
3436 (Tuple(Le(b, a), Le(c, a)),
3437 And(Ge(a, Min(b, c)), Lt(a, Max(b, c)))),
3438 (Tuple(Le(b, a), Lt(c, a)),
3439 ITE(b > c, And(Gt(a, c), Lt(a, b)),
3440 And(Ge(a, b), Le(a, c)))),
3441 (Tuple(Lt(b, a), Lt(c, a)),
3442 And(Gt(a, Min(b, c)), Le(a, Max(b, c)))),
3443 (Tuple(Le(a, b), Le(a, c)),
3444 And(Le(a, Max(b, c)), Gt(a, Min(b, c)))),
3445 (Tuple(Le(a, b), Lt(a, c)),
3446 ITE(b < c, And(Lt(a, c), Gt(a, b)),
3447 And(Le(a, b), Ge(a, c)))),
3448 (Tuple(Lt(a, b), Lt(a, c)),
3449 And(Lt(a, Max(b, c)), Ge(a, Min(b, c)))),
3450 )
3451 return _matchers_xor
3454def simplify_univariate(expr):
3455 """return a simplified version of univariate boolean expression, else ``expr``"""
3456 from sympy.functions.elementary.piecewise import Piecewise
3457 from sympy.core.relational import Eq, Ne
3458 if not isinstance(expr, BooleanFunction):
3459 return expr
3460 if expr.atoms(Eq, Ne):
3461 return expr
3462 c = expr
3463 free = c.free_symbols
3464 if len(free) != 1:
3465 return c
3466 x = free.pop()
3467 ok, i = Piecewise((0, c), evaluate=False
3468 )._intervals(x, err_on_Eq=True)
3469 if not ok:
3470 return c
3471 if not i:
3472 return false
3473 args = []
3474 for a, b, _, _ in i:
3475 if a is S.NegativeInfinity:
3476 if b is S.Infinity:
3477 c = true
3478 else:
3479 if c.subs(x, b) == True:
3480 c = (x <= b)
3481 else:
3482 c = (x < b)
3483 else:
3484 incl_a = (c.subs(x, a) == True)
3485 incl_b = (c.subs(x, b) == True)
3486 if incl_a and incl_b:
3487 if b.is_infinite:
3488 c = (x >= a)
3489 else:
3490 c = And(a <= x, x <= b)
3491 elif incl_a:
3492 c = And(a <= x, x < b)
3493 elif incl_b:
3494 if b.is_infinite:
3495 c = (x > a)
3496 else:
3497 c = And(a < x, x <= b)
3498 else:
3499 c = And(a < x, x < b)
3500 args.append(c)
3501 return Or(*args)
3504# Classes corresponding to logic gates
3505# Used in gateinputcount method
3506BooleanGates = (And, Or, Xor, Nand, Nor, Not, Xnor, ITE)
3508def gateinputcount(expr):
3509 """
3510 Return the total number of inputs for the logic gates realizing the
3511 Boolean expression.
3513 Returns
3514 =======
3516 int
3517 Number of gate inputs
3519 Note
3520 ====
3522 Not all Boolean functions count as gate here, only those that are
3523 considered to be standard gates. These are: :py:class:`~.And`,
3524 :py:class:`~.Or`, :py:class:`~.Xor`, :py:class:`~.Not`, and
3525 :py:class:`~.ITE` (multiplexer). :py:class:`~.Nand`, :py:class:`~.Nor`,
3526 and :py:class:`~.Xnor` will be evaluated to ``Not(And())`` etc.
3528 Examples
3529 ========
3531 >>> from sympy.logic import And, Or, Nand, Not, gateinputcount
3532 >>> from sympy.abc import x, y, z
3533 >>> expr = And(x, y)
3534 >>> gateinputcount(expr)
3535 2
3536 >>> gateinputcount(Or(expr, z))
3537 4
3539 Note that ``Nand`` is automatically evaluated to ``Not(And())`` so
3541 >>> gateinputcount(Nand(x, y, z))
3542 4
3543 >>> gateinputcount(Not(And(x, y, z)))
3544 4
3546 Although this can be avoided by using ``evaluate=False``
3548 >>> gateinputcount(Nand(x, y, z, evaluate=False))
3549 3
3551 Also note that a comparison will count as a Boolean variable:
3553 >>> gateinputcount(And(x > z, y >= 2))
3554 2
3556 As will a symbol:
3557 >>> gateinputcount(x)
3558 0
3560 """
3561 if not isinstance(expr, Boolean):
3562 raise TypeError("Expression must be Boolean")
3563 if isinstance(expr, BooleanGates):
3564 return len(expr.args) + sum(gateinputcount(x) for x in expr.args)
3565 return 0