← Back to branch summary

~dinko-metalac/calculus-app2/trunk

« back to all changes in this revision

Viewing changes to lib/py/sympy/logic/boolalg.py

  • Committer: dinko.metalac at gmail
  • Date: 2015-04-14 13:28:14 UTC
  • Revision ID: dinko.metalac@gmail.com-20150414132814-j25k3qd7sq3warup
new sympy

Show diffs side-by-side

added added

removed removed

Lines of Context:
lib/py/sympy/logic/boolalg.py
1
 
"""Boolean algebra module for SymPy"""
 
1
"""
 
2
Boolean algebra module for SymPy
 
3
"""
 
4
from __future__ import print_function, division
 
5
 
2
6
from collections import defaultdict
 
7
from itertools import combinations, product
3
8
 
4
9
from sympy.core.basic import Basic
 
10
from sympy.core.cache import cacheit
 
11
from sympy.core.core import C
5
12
from sympy.core.numbers import Number
6
13
from sympy.core.decorators import deprecated
7
14
from sympy.core.operations import LatticeOp
8
 
from sympy.core.function import Application, sympify
9
 
from sympy.core.compatibility import ordered, product
 
15
from sympy.core.function import Application
 
16
from sympy.core.compatibility import ordered, xrange, with_metaclass
 
17
from sympy.core.sympify import converter, _sympify, sympify
 
18
from sympy.core.singleton import Singleton, S
10
19
 
11
20
 
12
21
class Boolean(Basic):
18
27
        """Overloading for & operator"""
19
28
        return And(self, other)
20
29
 
 
30
    __rand__ = __and__
 
31
 
21
32
    def __or__(self, other):
22
33
        """Overloading for |"""
23
34
        return Or(self, other)
24
35
 
 
36
    __ror__ = __or__
 
37
 
25
38
    def __invert__(self):
26
39
        """Overloading for ~"""
27
40
        return Not(self)
34
47
        """Overloading for <<"""
35
48
        return Implies(other, self)
36
49
 
 
50
    __rrshift__ = __lshift__
 
51
    __rlshift__ = __rshift__
 
52
 
37
53
    def __xor__(self, other):
38
54
        return Xor(self, other)
39
55
 
 
56
    __rxor__ = __xor__
 
57
 
 
58
    def equals(self, other):
 
59
        """
 
60
        Returns if the given formulas have the same truth table.
 
61
        For two formulas to be equal they must have the same literals.
 
62
 
 
63
        Examples
 
64
        ========
 
65
 
 
66
        >>> from sympy.abc import A, B, C
 
67
        >>> from sympy.logic.boolalg import And, Or, Not
 
68
        >>> (A >> B).equals(~B >> ~A)
 
69
        True
 
70
        >>> Not(And(A, B, C)).equals(And(Not(A), Not(B), Not(C)))
 
71
        False
 
72
        >>> Not(And(A, Not(A))).equals(Or(B, Not(B)))
 
73
        False
 
74
        """
 
75
 
 
76
        from sympy.logic.inference import satisfiable
 
77
        return self.atoms() == other.atoms() and \
 
78
                not satisfiable(Not(Equivalent(self, other)))
 
79
 
 
80
 
 
81
# Developer note: There is liable to be some confusion as to when True should
 
82
# be used and when S.true should be used in various contexts throughout SymPy.
 
83
# An important thing to remember is that sympify(True) returns S.true.  This
 
84
# means that for the most part, you can just use True and it will
 
85
# automatically be converted to S.true when necessary, similar to how you can
 
86
# generally use 1 instead of S.One.
 
87
 
 
88
# The rule of thumb is:
 
89
 
 
90
#   "If the boolean in question can be replaced by an arbitrary symbolic
 
91
#   Boolean, like Or(x, y) or x > 1, use S.true. Otherwise, use True"
 
92
 
 
93
# In other words, use S.true only on those contexts where the boolean is being
 
94
# used as a symbolic representation of truth.  For example, if the object ends
 
95
# up in the .args of any expression, then it must necessarily be S.true
 
96
# instead of True, as elements of .args must be Basic.  On the other hand, ==
 
97
# is not a symbolic operation in SymPy, since it always returns True or False,
 
98
# and does so in terms of structural equality rather than mathematical, so it
 
99
# should return True. The assumptions system should use True and False. Aside
 
100
# from not satisfying the above rule of thumb, the assumptions system uses a
 
101
# three-valued logic (True, False, None), whereas S.true and S.false represent
 
102
# a two-valued logic.  When it doubt, use True.
 
103
 
 
104
# 2. "S.true == True" is True.
 
105
 
 
106
# While "S.true is True" is False, "S.true == True" is True, so if there is
 
107
# any doubt over whether a function or expression will return S.true or True,
 
108
# just use "==" instead of "is" to do the comparison, and it will work in
 
109
# either case.  Finally, for boolean flags, it's better to just use "if x"
 
110
# instead of "if x is True". To quote PEP 8:
 
111
 
 
112
#     Don't compare boolean values to True or False using ==.
 
113
 
 
114
#       Yes:   if greeting:
 
115
#       No:    if greeting == True:
 
116
#       Worse: if greeting is True:
 
117
 
 
118
class BooleanAtom(Boolean):
 
119
    """
 
120
    Base class of BooleanTrue and BooleanFalse.
 
121
    """
 
122
 
 
123
class BooleanTrue(with_metaclass(Singleton, BooleanAtom)):
 
124
    """
 
125
    SymPy version of True.
 
126
 
 
127
    The instances of this class are singletonized and can be accessed via
 
128
    S.true.
 
129
 
 
130
    This is the SymPy version of True, for use in the logic module. The
 
131
    primary advantage of using true instead of True is that shorthand boolean
 
132
    operations like ~ and >> will work as expected on this class, whereas with
 
133
    True they act bitwise on 1. Functions in the logic module will return this
 
134
    class when they evaluate to true.
 
135
 
 
136
    Examples
 
137
    ========
 
138
 
 
139
    >>> from sympy import sympify, true, Or
 
140
    >>> sympify(True)
 
141
    True
 
142
    >>> ~true
 
143
    False
 
144
    >>> ~True
 
145
    -2
 
146
    >>> Or(True, False)
 
147
    True
 
148
 
 
149
    See Also
 
150
    ========
 
151
    sympy.logic.boolalg.BooleanFalse
 
152
 
 
153
    """
 
154
    def __nonzero__(self):
 
155
        return True
 
156
 
 
157
    __bool__ = __nonzero__
 
158
 
 
159
    def __hash__(self):
 
160
        return hash(True)
 
161
 
 
162
    def as_set(self):
 
163
        """
 
164
        Rewrite logic operators and relationals in terms of real sets.
 
165
 
 
166
        Examples
 
167
        ========
 
168
 
 
169
        >>> from sympy import true
 
170
        >>> true.as_set()
 
171
        UniversalSet()
 
172
        """
 
173
        return S.UniversalSet
 
174
 
 
175
 
 
176
class BooleanFalse(with_metaclass(Singleton, BooleanAtom)):
 
177
    """
 
178
    SymPy version of False.
 
179
 
 
180
    The instances of this class are singletonized and can be accessed via
 
181
    S.false.
 
182
 
 
183
    This is the SymPy version of False, for use in the logic module. The
 
184
    primary advantage of using false instead of False is that shorthand boolean
 
185
    operations like ~ and >> will work as expected on this class, whereas with
 
186
    False they act bitwise on 0. Functions in the logic module will return this
 
187
    class when they evaluate to false.
 
188
 
 
189
    Examples
 
190
    ========
 
191
 
 
192
    >>> from sympy import sympify, false, Or, true
 
193
    >>> sympify(False)
 
194
    False
 
195
    >>> false >> false
 
196
    True
 
197
    >>> False >> False
 
198
    0
 
199
    >>> Or(True, False)
 
200
    True
 
201
 
 
202
    See Also
 
203
    ========
 
204
    sympy.logic.boolalg.BooleanTrue
 
205
 
 
206
    """
 
207
    def __nonzero__(self):
 
208
        return False
 
209
 
 
210
    __bool__ = __nonzero__
 
211
 
 
212
    def __hash__(self):
 
213
        return hash(False)
 
214
 
 
215
    def as_set(self):
 
216
        """
 
217
        Rewrite logic operators and relationals in terms of real sets.
 
218
 
 
219
        Examples
 
220
        ========
 
221
 
 
222
        >>> from sympy import false
 
223
        >>> false.as_set()
 
224
        EmptySet()
 
225
        """
 
226
        from sympy.sets.sets import EmptySet
 
227
        return EmptySet()
 
228
 
 
229
true = BooleanTrue()
 
230
false = BooleanFalse()
 
231
# We want S.true and S.false to work, rather than S.BooleanTrue and
 
232
# S.BooleanFalse, but making the class and instance names the same causes some
 
233
# major issues (like the inability to import the class directly from this
 
234
# file).
 
235
S.true = true
 
236
S.false = false
 
237
 
 
238
converter[bool] = lambda x: S.true if x else S.false
40
239
 
41
240
class BooleanFunction(Application, Boolean):
42
241
    """Boolean function is a function that lives in a boolean space
50
249
    def _eval_simplify(self, ratio, measure):
51
250
        return simplify_logic(self)
52
251
 
 
252
    def to_nnf(self, simplify=True):
 
253
        return self._to_nnf(*self.args, simplify=simplify)
 
254
 
 
255
    @classmethod
 
256
    def _to_nnf(cls, *args, **kwargs):
 
257
        simplify = kwargs.get('simplify', True)
 
258
        argset = set([])
 
259
        for arg in args:
 
260
            if not is_literal(arg):
 
261
                arg = arg.to_nnf(simplify)
 
262
            if simplify:
 
263
                if isinstance(arg, cls):
 
264
                    arg = arg.args
 
265
                else:
 
266
                    arg = (arg,)
 
267
                for a in arg:
 
268
                    if Not(a) in argset:
 
269
                        return cls.zero
 
270
                    argset.add(a)
 
271
            else:
 
272
                argset.add(arg)
 
273
        return cls(*argset)
 
274
 
53
275
 
54
276
class And(LatticeOp, BooleanFunction):
55
277
    """
70
292
    Notes
71
293
    =====
72
294
 
73
 
    The operator operator ``&`` will perform bitwise operations
74
 
    on integers and for convenience will construct an Add when
75
 
    the arguments are symbolic, but the And function does not
76
 
    perform bitwise operations and when any argument is True it
77
 
    is simply removed from the arguments:
 
295
    The ``&`` operator is provided as a convenience, but note that its use
 
296
    here is different from its normal use in Python, which is bitwise
 
297
    and. Hence, ``And(a, b)`` and ``a & b`` will return different things if
 
298
    ``a`` and ``b`` are integers.
78
299
 
79
300
    >>> And(x, y).subs(x, 1)
80
301
    y
 
302
 
81
303
    """
82
 
    zero = False
83
 
    identity = True
 
304
    zero = false
 
305
    identity = true
 
306
 
 
307
    nargs = None
84
308
 
85
309
    @classmethod
86
310
    def _new_args_filter(cls, args):
92
316
                newargs.append(x)
93
317
        return LatticeOp._new_args_filter(newargs, And)
94
318
 
 
319
    def as_set(self):
 
320
        """
 
321
        Rewrite logic operators and relationals in terms of real sets.
 
322
 
 
323
        Examples
 
324
        ========
 
325
 
 
326
        >>> from sympy import And, Symbol
 
327
        >>> x = Symbol('x', real=True)
 
328
        >>> And(x<2, x>-2).as_set()
 
329
        (-2, 2)
 
330
        """
 
331
        from sympy.sets.sets import Intersection
 
332
        if len(self.free_symbols) == 1:
 
333
            return Intersection(*[arg.as_set() for arg in self.args])
 
334
        else:
 
335
            raise NotImplementedError("Sorry, And.as_set has not yet been"
 
336
                                      " implemented for multivariate"
 
337
                                      " expressions")
 
338
 
95
339
 
96
340
class Or(LatticeOp, BooleanFunction):
97
341
    """
112
356
    Notes
113
357
    =====
114
358
 
115
 
    The operator operator ``|`` will perform bitwise operations
116
 
    on integers and for convenience will construct an Or when
117
 
    the arguments are symbolic, but the Or function does not
118
 
    perform bitwise operations and when any argument is False it
119
 
    is simply removed from the arguments:
 
359
    The ``|`` operator is provided as a convenience, but note that its use
 
360
    here is different from its normal use in Python, which is bitwise
 
361
    or. Hence, ``Or(a, b)`` and ``a | b`` will return different things if
 
362
    ``a`` and ``b`` are integers.
120
363
 
121
364
    >>> Or(x, y).subs(x, 0)
122
365
    y
 
366
 
123
367
    """
124
 
    zero = True
125
 
    identity = False
 
368
    zero = true
 
369
    identity = false
126
370
 
127
371
    @classmethod
128
372
    def _new_args_filter(cls, args):
134
378
                newargs.append(x)
135
379
        return LatticeOp._new_args_filter(newargs, Or)
136
380
 
 
381
    def as_set(self):
 
382
        """
 
383
        Rewrite logic operators and relationals in terms of real sets.
 
384
 
 
385
        Examples
 
386
        ========
 
387
 
 
388
        >>> from sympy import Or, Symbol
 
389
        >>> x = Symbol('x', real=True)
 
390
        >>> Or(x>2, x<-2).as_set()
 
391
        (-oo, -2) U (2, oo)
 
392
        """
 
393
        from sympy.sets.sets import Union
 
394
        if len(self.free_symbols) == 1:
 
395
            return Union(*[arg.as_set() for arg in self.args])
 
396
        else:
 
397
            raise NotImplementedError("Sorry, Or.as_set has not yet been"
 
398
                                      " implemented for multivariate"
 
399
                                      " expressions")
 
400
 
137
401
 
138
402
class Not(BooleanFunction):
139
403
    """
140
404
    Logical Not function (negation)
141
405
 
 
406
 
 
407
    Returns True if the statement is False
 
408
    Returns False if the statement is True
 
409
 
 
410
    Examples
 
411
    ========
 
412
 
 
413
    >>> from sympy.logic.boolalg import Not, And, Or
 
414
    >>> from sympy.abc import x, A, B
 
415
    >>> Not(True)
 
416
    False
 
417
    >>> Not(False)
 
418
    True
 
419
    >>> Not(And(True, False))
 
420
    True
 
421
    >>> Not(Or(True, False))
 
422
    False
 
423
    >>> Not(And(And(True, x), Or(x, False)))
 
424
    Not(x)
 
425
    >>> ~x
 
426
    Not(x)
 
427
    >>> Not(And(Or(A, B), Or(~A, ~B)))
 
428
    Not(And(Or(A, B), Or(Not(A), Not(B))))
 
429
 
142
430
    Notes
143
431
    =====
144
432
 
145
 
    De Morgan rules are applied automatically.
 
433
    - The ``~`` operator is provided as a convenience, but note that its use
 
434
      here is different from its normal use in Python, which is bitwise
 
435
      not. In particular, ``~a`` and ``Not(a)`` will be different if ``a`` is
 
436
      an integer. Furthermore, since bools in Python subclass from ``int``,
 
437
      ``~True`` is the same as ``~1`` which is ``-2``, which has a boolean
 
438
      value of True.  To avoid this issue, use the SymPy boolean types
 
439
      ``true`` and ``false``.
 
440
 
 
441
    >>> from sympy import true
 
442
    >>> ~True
 
443
    -2
 
444
    >>> ~true
 
445
    False
 
446
 
146
447
    """
147
448
 
148
449
    is_Not = True
149
450
 
150
451
    @classmethod
151
452
    def eval(cls, arg):
152
 
        """
153
 
        Logical Not function (negation)
154
 
 
155
 
        Returns True if the statement is False
156
 
        Returns False if the statement is True
157
 
 
158
 
        Examples
159
 
        ========
160
 
 
161
 
        >>> from sympy.logic.boolalg import Not, And, Or
162
 
        >>> from sympy.abc import x
163
 
        >>> Not(True)
164
 
        False
165
 
        >>> Not(False)
166
 
        True
167
 
        >>> Not(And(True, False))
168
 
        True
169
 
        >>> Not(Or(True, False))
170
 
        False
171
 
        >>> Not(And(And(True, x), Or(x, False)))
172
 
        Not(x)
173
 
        """
174
 
        if isinstance(arg, Number) or arg in (0, 1):
175
 
            return False if arg else True
176
 
        # apply De Morgan Rules
177
 
        if arg.func is And:
178
 
            return Or(*[Not(a) for a in arg.args])
179
 
        if arg.func is Or:
180
 
            return And(*[Not(a) for a in arg.args])
181
 
        if arg.func is Not:
 
453
        if isinstance(arg, Number) or arg in (True, False):
 
454
            return false if arg else true
 
455
        if arg.is_Not:
182
456
            return arg.args[0]
 
457
        # Simplify Relational objects.
 
458
        if isinstance(arg, C.Equality):
 
459
            return C.Unequality(*arg.args)
 
460
        if isinstance(arg, C.Unequality):
 
461
            return C.Equality(*arg.args)
 
462
        if isinstance(arg, C.StrictLessThan):
 
463
            return C.GreaterThan(*arg.args)
 
464
        if isinstance(arg, C.StrictGreaterThan):
 
465
            return C.LessThan(*arg.args)
 
466
        if isinstance(arg, C.LessThan):
 
467
            return C.StrictGreaterThan(*arg.args)
 
468
        if isinstance(arg, C.GreaterThan):
 
469
            return C.StrictLessThan(*arg.args)
 
470
 
 
471
    def as_set(self):
 
472
        """
 
473
        Rewrite logic operators and relationals in terms of real sets.
 
474
 
 
475
        Examples
 
476
        ========
 
477
 
 
478
        >>> from sympy import Not, Symbol
 
479
        >>> x = Symbol('x', real=True)
 
480
        >>> Not(x>0).as_set()
 
481
        (-oo, 0]
 
482
        """
 
483
        if len(self.free_symbols) == 1:
 
484
            return self.args[0].as_set().complement
 
485
        else:
 
486
            raise NotImplementedError("Sorry, Not.as_set has not yet been"
 
487
                                      " implemented for mutivariate"
 
488
                                      " expressions")
 
489
 
 
490
    def to_nnf(self, simplify=True):
 
491
        if is_literal(self):
 
492
            return self
 
493
 
 
494
        expr = self.args[0]
 
495
 
 
496
        func, args = expr.func, expr.args
 
497
 
 
498
        if func == And:
 
499
            return Or._to_nnf(*[~arg for arg in args], simplify=simplify)
 
500
 
 
501
        if func == Or:
 
502
            return And._to_nnf(*[~arg for arg in args], simplify=simplify)
 
503
 
 
504
        if func == Implies:
 
505
            a, b = args
 
506
            return And._to_nnf(a, ~b, simplify=simplify)
 
507
 
 
508
        if func == Equivalent:
 
509
            return And._to_nnf(Or(*args), Or(*[~arg for arg in args]), simplify=simplify)
 
510
 
 
511
        if func == Xor:
 
512
            result = []
 
513
            for i in xrange(1, len(args)+1, 2):
 
514
                for neg in combinations(args, i):
 
515
                    clause = [~s if s in neg else s for s in args]
 
516
                    result.append(Or(*clause))
 
517
            return And._to_nnf(*result, simplify=simplify)
 
518
 
 
519
        if func == ITE:
 
520
            a, b, c = args
 
521
            return And._to_nnf(Or(a, ~c), Or(~a, ~b), simplify=simplify)
 
522
 
 
523
        raise ValueError("Illegal operator %s in expression" % func)
183
524
 
184
525
 
185
526
class Xor(BooleanFunction):
186
527
    """
187
528
    Logical XOR (exclusive OR) function.
 
529
 
 
530
 
 
531
    Returns True if an odd number of the arguments are True and the rest are
 
532
    False.
 
533
 
 
534
    Returns False if an even number of the arguments are True and the rest are
 
535
    False.
 
536
 
 
537
    Examples
 
538
    ========
 
539
 
 
540
    >>> from sympy.logic.boolalg import Xor
 
541
    >>> from sympy import symbols
 
542
    >>> x, y = symbols('x y')
 
543
    >>> Xor(True, False)
 
544
    True
 
545
    >>> Xor(True, True)
 
546
    False
 
547
    >>> Xor(True, False, True, True, False)
 
548
    True
 
549
    >>> Xor(True, False, True, False)
 
550
    False
 
551
    >>> x ^ y
 
552
    Xor(x, y)
 
553
 
 
554
    Notes
 
555
    =====
 
556
 
 
557
    The ``^`` operator is provided as a convenience, but note that its use
 
558
    here is different from its normal use in Python, which is bitwise xor. In
 
559
    particular, ``a ^ b`` and ``Xor(a, b)`` will be different if ``a`` and
 
560
    ``b`` are integers.
 
561
 
 
562
    >>> Xor(x, y).subs(y, 0)
 
563
    x
 
564
 
188
565
    """
189
 
    @classmethod
190
 
    def eval(cls, *args):
191
 
        """
192
 
        Logical XOR (exclusive OR) function.
193
 
 
194
 
        Returns True if an odd number of the arguments are True
195
 
            and the rest are False.
196
 
        Returns False if an even number of the arguments are True
197
 
            and the rest are False.
198
 
 
199
 
        Examples
200
 
        ========
201
 
 
202
 
        >>> from sympy.logic.boolalg import Xor
203
 
        >>> Xor(True, False)
204
 
        True
205
 
        >>> Xor(True, True)
206
 
        False
207
 
 
208
 
        >>> Xor(True, False, True, True, False)
209
 
        True
210
 
        >>> Xor(True, False, True, False)
211
 
        False
212
 
        """
213
 
        if not args:
214
 
            return False
215
 
        args = list(args)
216
 
        A = args.pop()
217
 
        while args:
218
 
            B = args.pop()
219
 
            A = Or(And(A, Not(B)), And(Not(A), B))
220
 
        return A
 
566
    def __new__(cls, *args, **kwargs):
 
567
        argset = set([])
 
568
        obj = super(Xor, cls).__new__(cls, *args, **kwargs)
 
569
        for arg in obj._args:
 
570
            if isinstance(arg, Number) or arg in (True, False):
 
571
                if arg:
 
572
                    arg = true
 
573
                else:
 
574
                    continue
 
575
            if isinstance(arg, Xor):
 
576
                for a in arg.args:
 
577
                    argset.remove(a) if a in argset else argset.add(a)
 
578
            elif arg in argset:
 
579
                argset.remove(arg)
 
580
            else:
 
581
                argset.add(arg)
 
582
        if len(argset) == 0:
 
583
            return false
 
584
        elif len(argset) == 1:
 
585
            return argset.pop()
 
586
        elif True in argset:
 
587
            argset.remove(True)
 
588
            return Not(Xor(*argset))
 
589
        else:
 
590
            obj._args = tuple(ordered(argset))
 
591
            obj._argset = frozenset(argset)
 
592
            return obj
 
593
 
 
594
    @property
 
595
    @cacheit
 
596
    def args(self):
 
597
        return tuple(ordered(self._argset))
 
598
 
 
599
    def to_nnf(self, simplify=True):
 
600
        args = []
 
601
        for i in xrange(0, len(self.args)+1, 2):
 
602
            for neg in combinations(self.args, i):
 
603
                clause = [~s if s in neg else s for s in self.args]
 
604
                args.append(Or(*clause))
 
605
        return And._to_nnf(*args, simplify=simplify)
221
606
 
222
607
 
223
608
class Nand(BooleanFunction):
226
611
 
227
612
    It evaluates its arguments in order, giving True immediately if any
228
613
    of them are False, and False if they are all True.
 
614
 
 
615
    Returns True if any of the arguments are False
 
616
    Returns False if all arguments are True
 
617
 
 
618
    Examples
 
619
    ========
 
620
 
 
621
    >>> from sympy.logic.boolalg import Nand
 
622
    >>> from sympy import symbols
 
623
    >>> x, y = symbols('x y')
 
624
    >>> Nand(False, True)
 
625
    True
 
626
    >>> Nand(True, True)
 
627
    False
 
628
    >>> Nand(x, y)
 
629
    Not(And(x, y))
 
630
 
229
631
    """
230
632
    @classmethod
231
633
    def eval(cls, *args):
232
 
        """
233
 
        Logical NAND function.
234
 
 
235
 
        Returns True if any of the arguments are False
236
 
        Returns False if all arguments are True
237
 
 
238
 
        Examples
239
 
        ========
240
 
 
241
 
        >>> from sympy.logic.boolalg import Nand
242
 
        >>> Nand(False, True)
243
 
        True
244
 
        >>> Nand(True, True)
245
 
        False
246
 
        """
247
634
        return Not(And(*args))
248
635
 
249
636
 
253
640
 
254
641
    It evaluates its arguments in order, giving False immediately if any
255
642
    of them are True, and True if they are all False.
 
643
 
 
644
    Returns False if any argument is True
 
645
    Returns True if all arguments are False
 
646
 
 
647
    Examples
 
648
    ========
 
649
 
 
650
    >>> from sympy.logic.boolalg import Nor
 
651
    >>> from sympy import symbols
 
652
    >>> x, y = symbols('x y')
 
653
 
 
654
    >>> Nor(True, False)
 
655
    False
 
656
    >>> Nor(True, True)
 
657
    False
 
658
    >>> Nor(False, True)
 
659
    False
 
660
    >>> Nor(False, False)
 
661
    True
 
662
    >>> Nor(x, y)
 
663
    Not(Or(x, y))
 
664
 
256
665
    """
257
666
    @classmethod
258
667
    def eval(cls, *args):
259
 
        """
260
 
        Logical NOR function.
261
 
 
262
 
        Returns False if any argument is True
263
 
        Returns True if all arguments are False
264
 
 
265
 
        Examples
266
 
        ========
267
 
 
268
 
        >>> from sympy.logic.boolalg import Nor
269
 
        >>> Nor(True, False)
270
 
        False
271
 
        >>> Nor(True, True)
272
 
        False
273
 
        >>> Nor(False, True)
274
 
        False
275
 
        >>> Nor(False, False)
276
 
        True
277
 
        """
278
668
        return Not(Or(*args))
279
669
 
280
670
 
283
673
    Logical implication.
284
674
 
285
675
    A implies B is equivalent to !A v B
 
676
 
 
677
    Accepts two Boolean arguments; A and B.
 
678
    Returns False if A is True and B is False
 
679
    Returns True otherwise.
 
680
 
 
681
    Examples
 
682
    ========
 
683
 
 
684
    >>> from sympy.logic.boolalg import Implies
 
685
    >>> from sympy import symbols
 
686
    >>> x, y = symbols('x y')
 
687
 
 
688
    >>> Implies(True, False)
 
689
    False
 
690
    >>> Implies(False, False)
 
691
    True
 
692
    >>> Implies(True, True)
 
693
    True
 
694
    >>> Implies(False, True)
 
695
    True
 
696
    >>> x >> y
 
697
    Implies(x, y)
 
698
    >>> y << x
 
699
    Implies(x, y)
 
700
 
 
701
    Notes
 
702
    =====
 
703
 
 
704
    The ``>>`` and ``<<`` operators are provided as a convenience, but note
 
705
    that their use here is different from their normal use in Python, which is
 
706
    bit shifts. Hence, ``Implies(a, b)`` and ``a >> b`` will return different
 
707
    things if ``a`` and ``b`` are integers.  In particular, since Python
 
708
    considers ``True`` and ``False`` to be integers, ``True >> True`` will be
 
709
    the same as ``1 >> 1``, i.e., 0, which has a truth value of False.  To
 
710
    avoid this issue, use the SymPy objects ``true`` and ``false``.
 
711
 
 
712
    >>> from sympy import true, false
 
713
    >>> True >> False
 
714
    1
 
715
    >>> true >> false
 
716
    False
 
717
 
286
718
    """
287
719
    @classmethod
288
720
    def eval(cls, *args):
289
 
        """
290
 
        Logical implication.
291
 
 
292
 
        Accepts two Boolean arguments; A and B.
293
 
        Returns False if A is True and B is False
294
 
        Returns True otherwise.
295
 
 
296
 
        Examples
297
 
        ========
298
 
 
299
 
        >>> from sympy.logic.boolalg import Implies
300
 
        >>> Implies(True, False)
301
 
        False
302
 
        >>> Implies(False, False)
303
 
        True
304
 
        >>> Implies(True, True)
305
 
        True
306
 
        >>> Implies(False, True)
307
 
        True
308
 
        """
309
721
        try:
310
722
            newargs = []
311
723
            for x in args:
318
730
            raise ValueError(
319
731
                "%d operand(s) used for an Implies "
320
732
                "(pairs are required): %s" % (len(args), str(args)))
321
 
        if A is True or A is False or B is True or B is False:
 
733
        if A == True or A == False or B == True or B == False:
322
734
            return Or(Not(A), B)
323
735
        else:
324
736
            return Basic.__new__(cls, *args)
325
737
 
 
738
    def to_nnf(self, simplify=True):
 
739
        a, b = self.args
 
740
        return Or._to_nnf(~a, b, simplify=simplify)
 
741
 
326
742
 
327
743
class Equivalent(BooleanFunction):
328
744
    """
329
745
    Equivalence relation.
330
746
 
331
747
    Equivalent(A, B) is True iff A and B are both True or both False
 
748
 
 
749
    Returns True if all of the arguments are logically equivalent.
 
750
    Returns False otherwise.
 
751
 
 
752
    Examples
 
753
    ========
 
754
 
 
755
    >>> from sympy.logic.boolalg import Equivalent, And
 
756
    >>> from sympy.abc import x, y
 
757
    >>> Equivalent(False, False, False)
 
758
    True
 
759
    >>> Equivalent(True, False, False)
 
760
    False
 
761
    >>> Equivalent(x, And(x, True))
 
762
    True
332
763
    """
333
 
    @classmethod
334
 
    def eval(cls, *args):
335
 
        """
336
 
        Equivalence relation.
337
 
 
338
 
        Returns True if all of the arguments are logically equivalent.
339
 
        Returns False otherwise.
340
 
 
341
 
        Examples
342
 
        ========
343
 
 
344
 
        >>> from sympy.logic.boolalg import Equivalent, And
345
 
        >>> from sympy.abc import x
346
 
        >>> Equivalent(False, False, False)
347
 
        True
348
 
        >>> Equivalent(True, False, False)
349
 
        False
350
 
        >>> Equivalent(x, And(x, True))
351
 
        True
352
 
 
353
 
        """
354
 
 
355
 
        newargs = []
 
764
    def __new__(cls, *args, **options):
 
765
        args = [_sympify(arg) for arg in args]
 
766
 
 
767
        argset = set(args)
356
768
        for x in args:
357
 
            if isinstance(x, Number) or x in (0, 1):
358
 
                newargs.append(True if x else False)
359
 
            else:
360
 
                newargs.append(x)
361
 
        argset = set(newargs)
 
769
            if isinstance(x, Number) or x in [True, False]: # Includes 0, 1
 
770
                argset.discard(x)
 
771
                argset.add(True if x else False)
362
772
        if len(argset) <= 1:
363
 
            return True
 
773
            return true
364
774
        if True in argset:
365
775
            argset.discard(True)
366
776
            return And(*argset)
367
777
        if False in argset:
368
778
            argset.discard(False)
369
 
            return Nor(*argset)
370
 
        return Basic.__new__(cls, *set(args))
 
779
            return And(*[~arg for arg in argset])
 
780
        _args = frozenset(argset)
 
781
        obj = super(Equivalent, cls).__new__(cls, _args)
 
782
        obj._argset = _args
 
783
        return obj
 
784
 
 
785
    @property
 
786
    @cacheit
 
787
    def args(self):
 
788
        return tuple(ordered(self._argset))
 
789
 
 
790
    def to_nnf(self, simplify=True):
 
791
        args = []
 
792
        for a, b in zip(self.args, self.args[1:]):
 
793
            args.append(Or(~a, b))
 
794
        args.append(Or(~self.args[-1], self.args[0]))
 
795
        return And._to_nnf(*args, simplify=simplify)
371
796
 
372
797
 
373
798
class ITE(BooleanFunction):
374
799
    """
375
800
    If then else clause.
 
801
 
 
802
    ITE(A, B, C) evaluates and returns the result of B if A is true
 
803
    else it returns the result of C
 
804
 
 
805
    Examples
 
806
    ========
 
807
 
 
808
    >>> from sympy.logic.boolalg import ITE, And, Xor, Or
 
809
    >>> from sympy.abc import x, y, z
 
810
    >>> ITE(True, False, True)
 
811
    False
 
812
    >>> ITE(Or(True, False), And(True, True), Xor(True, True))
 
813
    True
 
814
    >>> ITE(x, y, z)
 
815
    ITE(x, y, z)
 
816
    >>> ITE(True, x, y)
 
817
    x
 
818
    >>> ITE(False, x, y)
 
819
    y
 
820
    >>> ITE(x, y, y)
 
821
    y
376
822
    """
377
823
    @classmethod
378
824
    def eval(cls, *args):
379
 
        """
380
 
        If then else clause
381
 
 
382
 
        ITE(A, B, C) evaluates and returns the result of B if A is true
383
 
        else it returns the result of C
384
 
 
385
 
        Examples
386
 
        ========
387
 
 
388
 
        >>> from sympy.logic.boolalg import ITE, And, Xor, Or
389
 
        >>> from sympy.abc import x, y, z
390
 
        >>> x = True
391
 
        >>> y = False
392
 
        >>> z = True
393
 
        >>> ITE(x, y, z)
394
 
        False
395
 
        >>> ITE(Or(x, y), And(x, z), Xor(z, x))
396
 
        True
397
 
        """
398
 
        args = list(args)
399
 
        if len(args) == 3:
400
 
            return Or(And(args[0], args[1]), And(Not(args[0]), args[2]))
401
 
        raise ValueError("ITE expects 3 arguments, but got %d: %s" %
402
 
                         (len(args), str(args)))
 
825
        try:
 
826
            a, b, c = args
 
827
        except ValueError:
 
828
            raise ValueError("ITE expects exactly 3 arguments")
 
829
        if a == True:
 
830
            return b
 
831
        if a == False:
 
832
            return c
 
833
        if b == c:
 
834
            return b
 
835
 
 
836
    def to_nnf(self, simplify=True):
 
837
        a, b, c = self.args
 
838
        return And._to_nnf(Or(~a, b), Or(a, c), simplify=simplify)
403
839
 
404
840
### end class definitions. Some useful methods
405
841
 
485
921
            return info[0]
486
922
        rest = info[2](*[a for a in info[0].args if a is not conj])
487
923
        return info[1](*list(map(_distribute,
488
 
                   [(info[2](c, rest), info[1], info[2]) for c in conj.args])))
 
924
            [(info[2](c, rest), info[1], info[2]) for c in conj.args])))
489
925
    elif info[0].func is info[1]:
490
926
        return info[1](*list(map(_distribute,
491
 
                            [(x, info[1], info[2]) for x in info[0].args])))
 
927
            [(x, info[1], info[2]) for x in info[0].args])))
492
928
    else:
493
929
        return info[0]
494
930
 
495
931
 
 
932
def to_nnf(expr, simplify=True):
 
933
    """
 
934
    Converts expr to Negation Normal Form.
 
935
    A logical expression is in Negation Normal Form (NNF) if it
 
936
    contains only And, Or and Not, and Not is applied only to literals.
 
937
    If simpify is True, the result contains no redundant clauses.
 
938
 
 
939
    Examples
 
940
    ========
 
941
 
 
942
    >>> from sympy.abc import A, B, C, D
 
943
    >>> from sympy.logic.boolalg import Not, Equivalent, to_nnf
 
944
    >>> to_nnf(Not((~A & ~B) | (C & D)))
 
945
    And(Or(A, B), Or(Not(C), Not(D)))
 
946
    >>> to_nnf(Equivalent(A >> B, B >> A))
 
947
    And(Or(A, And(A, Not(B)), Not(B)), Or(And(B, Not(A)), B, Not(A)))
 
948
    """
 
949
    if is_nnf(expr, simplify):
 
950
        return expr
 
951
    return expr.to_nnf(simplify)
 
952
 
 
953
 
496
954
def to_cnf(expr, simplify=False):
497
955
    """
498
956
    Convert a propositional logical sentence s to conjunctive normal form.
499
957
    That is, of the form ((A | ~B | ...) & (B | C | ...) & ...)
 
958
    If simplify is True, the expr is evaluated to its simplest CNF form.
500
959
 
501
960
    Examples
502
961
    ========
505
964
    >>> from sympy.abc import A, B, D
506
965
    >>> to_cnf(~(A | B) | D)
507
966
    And(Or(D, Not(A)), Or(D, Not(B)))
 
967
    >>> to_cnf((A | B) & (A | ~A), True)
 
968
    Or(A, B)
508
969
 
509
970
    """
510
971
    expr = sympify(expr)
512
973
        return expr
513
974
 
514
975
    if simplify:
515
 
        simplified_expr = distribute_and_over_or(simplify_logic(expr))
516
 
        if len(simplified_expr.args) < len(to_cnf(expr).args):
517
 
            return simplified_expr
518
 
        else:
519
 
            return to_cnf(expr)
 
976
        return simplify_logic(expr, 'cnf', True)
520
977
 
521
978
    # Don't convert unless we have to
522
979
    if is_cnf(expr):
530
987
    """
531
988
    Convert a propositional logical sentence s to disjunctive normal form.
532
989
    That is, of the form ((A & ~B & ...) | (B & C & ...) | ...)
 
990
    If simplify is True, the expr is evaluated to its simplest DNF form.
533
991
 
534
992
    Examples
535
993
    ========
536
994
 
537
995
    >>> from sympy.logic.boolalg import to_dnf
538
 
    >>> from sympy.abc import A, B, C, D
 
996
    >>> from sympy.abc import A, B, C
539
997
    >>> to_dnf(B & (A | C))
540
998
    Or(And(A, B), And(B, C))
 
999
    >>> to_dnf((A & B) | (A & ~B) | (B & C) | (~B & C), True)
 
1000
    Or(A, C)
541
1001
 
542
1002
    """
543
1003
    expr = sympify(expr)
545
1005
        return expr
546
1006
 
547
1007
    if simplify:
548
 
        simplified_expr = distribute_or_over_and(simplify_logic(expr))
549
 
        if len(simplified_expr.args) < len(to_dnf(expr).args):
550
 
            return simplified_expr
551
 
        else:
552
 
            return to_dnf(expr)
 
1008
        return simplify_logic(expr, 'dnf', True)
553
1009
 
554
1010
    # Don't convert unless we have to
555
1011
    if is_dnf(expr):
559
1015
    return distribute_or_over_and(expr)
560
1016
 
561
1017
 
 
1018
def is_nnf(expr, simplified=True):
 
1019
    """
 
1020
    Checks if expr is in Negation Normal Form.
 
1021
    A logical expression is in Negation Normal Form (NNF) if it
 
1022
    contains only And, Or and Not, and Not is applied only to literals.
 
1023
    If simpified is True, checks if result contains no redundant clauses.
 
1024
 
 
1025
    Examples
 
1026
    ========
 
1027
 
 
1028
    >>> from sympy.abc import A, B, C
 
1029
    >>> from sympy.logic.boolalg import Not, is_nnf
 
1030
    >>> is_nnf(A & B | ~C)
 
1031
    True
 
1032
    >>> is_nnf((A | ~A) & (B | C))
 
1033
    False
 
1034
    >>> is_nnf((A | ~A) & (B | C), False)
 
1035
    True
 
1036
    >>> is_nnf(Not(A & B) | C)
 
1037
    False
 
1038
    >>> is_nnf((A >> B) & (B >> A))
 
1039
    False
 
1040
    """
 
1041
 
 
1042
    expr = sympify(expr)
 
1043
    if is_literal(expr):
 
1044
        return True
 
1045
 
 
1046
    stack = [expr]
 
1047
 
 
1048
    while stack:
 
1049
        expr = stack.pop()
 
1050
        if expr.func in (And, Or):
 
1051
            if simplified:
 
1052
                args = expr.args
 
1053
                for arg in args:
 
1054
                    if Not(arg) in args:
 
1055
                        return False
 
1056
            stack.extend(expr.args)
 
1057
 
 
1058
        elif not is_literal(expr):
 
1059
            return False
 
1060
 
 
1061
    return True
 
1062
 
 
1063
 
562
1064
def is_cnf(expr):
563
1065
    """
564
1066
    Test whether or not an expression is in conjunctive normal form.
666
1168
    Or(B, Not(A))
667
1169
    >>> eliminate_implications(Equivalent(A, B))
668
1170
    And(Or(A, Not(B)), Or(B, Not(A)))
669
 
    """
670
 
    expr = sympify(expr)
671
 
    if expr.is_Atom:
672
 
        return expr  # (Atoms are unchanged.)
673
 
    args = list(map(eliminate_implications, expr.args))
674
 
    if expr.func is Implies:
675
 
        a, b = args[0], args[-1]
676
 
        return (~a) | b
677
 
    elif expr.func is Equivalent:
678
 
        a, b = args[0], args[-1]
679
 
        return (a | Not(b)) & (b | Not(a))
 
1171
    >>> eliminate_implications(Equivalent(A, B, C))
 
1172
    And(Or(A, Not(C)), Or(B, Not(A)), Or(C, Not(B)))
 
1173
    """
 
1174
    return to_nnf(expr)
 
1175
 
 
1176
 
 
1177
def is_literal(expr):
 
1178
    """
 
1179
    Returns True if expr is a literal, else False.
 
1180
 
 
1181
    Examples
 
1182
    ========
 
1183
 
 
1184
    >>> from sympy import Or, Q
 
1185
    >>> from sympy.abc import A, B
 
1186
    >>> from sympy.logic.boolalg import is_literal
 
1187
    >>> is_literal(A)
 
1188
    True
 
1189
    >>> is_literal(~A)
 
1190
    True
 
1191
    >>> is_literal(Q.zero(A))
 
1192
    True
 
1193
    >>> is_literal(A + B)
 
1194
    True
 
1195
    >>> is_literal(Or(A, B))
 
1196
    False
 
1197
    """
 
1198
    if isinstance(expr, Not):
 
1199
        return not isinstance(expr.args[0], BooleanFunction)
680
1200
    else:
681
 
        return expr.func(*args)
 
1201
        return not isinstance(expr, BooleanFunction)
682
1202
 
683
1203
 
684
1204
@deprecated(
685
 
    useinstead="sympify", issue=3451, deprecated_since_version="0.7.3")
 
1205
    useinstead="sympify", issue=6550, deprecated_since_version="0.7.3")
686
1206
def compile_rule(s):
687
1207
    """
688
1208
    Transforms a rule into a SymPy expression
710
1230
    """
711
1231
 
712
1232
    # Convert the symbol list into a dict
713
 
    symbols = dict(list(zip(symbols, list(range(1, len(symbols) + 1)))))
 
1233
    symbols = dict(list(zip(symbols, list(xrange(1, len(symbols) + 1)))))
714
1234
 
715
1235
    def append_symbol(arg, symbols):
716
1236
        if arg.func is Not:
728
1248
    index, else returns -1.
729
1249
    """
730
1250
    index = -1
731
 
    for x, (i, j) in enumerate(list(zip(minterm1, minterm2))):
 
1251
    for x, (i, j) in enumerate(zip(minterm1, minterm2)):
732
1252
        if i != j:
733
1253
            if index == -1:
734
1254
                index = x
863
1383
    """
864
1384
    from sympy.core.symbol import Symbol
865
1385
 
866
 
    variables = [Symbol(v) if not isinstance(v, Symbol) else v
867
 
                 for v in variables]
 
1386
    variables = [sympify(v) for v in variables]
868
1387
    if minterms == []:
869
 
        return False
 
1388
        return false
870
1389
 
871
1390
    minterms = [list(i) for i in minterms]
872
1391
    dontcares = [list(i) for i in (dontcares or [])]
916
1435
    """
917
1436
    from sympy.core.symbol import Symbol
918
1437
 
919
 
    variables = [Symbol(v) if not isinstance(v, Symbol) else v
920
 
                 for v in variables]
 
1438
    variables = [sympify(v) for v in variables]
921
1439
    if minterms == []:
922
 
        return False
 
1440
        return false
923
1441
 
924
1442
    minterms = [list(i) for i in minterms]
925
1443
    dontcares = [list(i) for i in (dontcares or [])]
941
1459
    return And(*[_convert_to_varsPOS(x, variables) for x in essential])
942
1460
 
943
1461
 
944
 
def simplify_logic(expr):
945
 
    """
946
 
    This function simplifies a boolean function to its
947
 
    simplified version in SOP or POS form. The return type is an
948
 
    Or or And object in SymPy. The input can be a string or a boolean
949
 
    expression.
 
1462
def _find_predicates(expr):
 
1463
    """Helper to find logical predicates in BooleanFunctions.
 
1464
 
 
1465
    A logical predicate is defined here as anything within a BooleanFunction
 
1466
    that is not a BooleanFunction itself.
 
1467
 
 
1468
    """
 
1469
    if not isinstance(expr, BooleanFunction):
 
1470
        return set([expr])
 
1471
    return set.union(*(_find_predicates(i) for i in expr.args))
 
1472
 
 
1473
 
 
1474
def simplify_logic(expr, form=None, deep=True):
 
1475
    """
 
1476
    This function simplifies a boolean function to its simplified version
 
1477
    in SOP or POS form. The return type is an Or or And object in SymPy.
 
1478
 
 
1479
    Parameters
 
1480
    ==========
 
1481
 
 
1482
    expr : string or boolean expression
 
1483
    form : string ('cnf' or 'dnf') or None (default).
 
1484
        If 'cnf' or 'dnf', the simplest expression in the corresponding
 
1485
        normal form is returned; if None, the answer is returned
 
1486
        according to the form with fewest args (in CNF by default).
 
1487
    deep : boolean (default True)
 
1488
        indicates whether to recursively simplify any
 
1489
        non-boolean functions contained within the input.
950
1490
 
951
1491
    Examples
952
1492
    ========
954
1494
    >>> from sympy.logic import simplify_logic
955
1495
    >>> from sympy.abc import x, y, z
956
1496
    >>> from sympy import S
957
 
 
958
1497
    >>> b = '(~x & ~y & ~z) | ( ~x & ~y & z)'
959
1498
    >>> simplify_logic(b)
960
1499
    And(Not(x), Not(y))
965
1504
    And(Not(x), Not(y))
966
1505
 
967
1506
    """
968
 
    expr = sympify(expr)
969
 
    if not isinstance(expr, BooleanFunction):
970
 
        return expr
971
 
    variables = list(expr.free_symbols)
972
 
    truthtable = []
973
 
    for t in product([0, 1], repeat=len(variables)):
974
 
        t = list(t)
975
 
        if expr.subs(list(zip(variables, t))) == True:
976
 
            truthtable.append(t)
977
 
    if (len(truthtable) >= (2 ** (len(variables) - 1))):
978
 
        return SOPform(variables, truthtable)
 
1507
 
 
1508
    if form == 'cnf' or form == 'dnf' or form is None:
 
1509
        expr = sympify(expr)
 
1510
        if not isinstance(expr, BooleanFunction):
 
1511
            return expr
 
1512
        variables = _find_predicates(expr)
 
1513
        truthtable = []
 
1514
        for t in product([0, 1], repeat=len(variables)):
 
1515
            t = list(t)
 
1516
            if expr.xreplace(dict(zip(variables, t))) == True:
 
1517
                truthtable.append(t)
 
1518
        if deep:
 
1519
            from sympy.simplify.simplify import simplify
 
1520
            variables = [simplify(v) for v in variables]
 
1521
        if form == 'dnf' or \
 
1522
           (form is None and len(truthtable) >= (2 ** (len(variables) - 1))):
 
1523
            return SOPform(variables, truthtable)
 
1524
        elif form == 'cnf' or form is None:
 
1525
            return POSform(variables, truthtable)
979
1526
    else:
980
 
        return POSform(variables, truthtable)
 
1527
        raise ValueError("form can be cnf or dnf only")
981
1528
 
982
1529
 
983
1530
def _finger(eq):
1023
1570
    return inv
1024
1571
 
1025
1572
 
1026
 
def bool_equal(bool1, bool2, info=False):
1027
 
    """Return True if the two expressions represent the same logical
1028
 
    behavior for some correspondence between the variables of each
1029
 
    (which may be different). For example, And(x, y) is logically
1030
 
    equivalent to And(a, b) for {x: a, y: b} (or vice versa). If the
1031
 
    mapping is desired, then set ``info`` to True and the simplified
1032
 
    form of the functions and the mapping of variables will be
1033
 
    returned.
 
1573
def bool_map(bool1, bool2):
 
1574
    """
 
1575
    Return the simplified version of bool1, and the mapping of variables
 
1576
    that makes the two expressions bool1 and bool2 represent the same
 
1577
    logical behaviour for some correspondence between the variables
 
1578
    of each.
 
1579
    If more than one mappings of this sort exist, one of them
 
1580
    is returned.
 
1581
    For example, And(x, y) is logically equivalent to And(a, b) for
 
1582
    the mapping {x: a, y:b} or {x: b, y:a}.
 
1583
    If no such mapping exists, return False.
1034
1584
 
1035
1585
    Examples
1036
1586
    ========
1037
1587
 
1038
 
    >>> from sympy import SOPform, bool_equal, Or, And, Not, Xor
 
1588
    >>> from sympy import SOPform, bool_map, Or, And, Not, Xor
1039
1589
    >>> from sympy.abc import w, x, y, z, a, b, c, d
1040
1590
    >>> function1 = SOPform(['x','z','y'],[[1, 0, 1], [0, 0, 1]])
1041
1591
    >>> function2 = SOPform(['a','b','c'],[[1, 0, 1], [1, 0, 0]])
1042
 
    >>> bool_equal(function1, function2, info=True)
 
1592
    >>> bool_map(function1, function2)
1043
1593
    (And(Not(z), y), {y: a, z: b})
1044
1594
 
1045
1595
    The results are not necessarily unique, but they are canonical. Here,
1047
1597
 
1048
1598
    >>> eq =  Or(And(Not(y), w), And(Not(y), z), And(x, y))
1049
1599
    >>> eq2 = Or(And(Not(c), a), And(Not(c), d), And(b, c))
1050
 
    >>> bool_equal(eq, eq2)
1051
 
    True
1052
 
    >>> bool_equal(eq, eq2, info=True)
 
1600
    >>> bool_map(eq, eq2)
1053
1601
    (Or(And(Not(y), w), And(Not(y), z), And(x, y)), {w: a, x: b, y: c, z: d})
1054
1602
    >>> eq = And(Xor(a, b), c, And(c,d))
1055
 
    >>> bool_equal(eq, eq.subs(c, x), info=True)
 
1603
    >>> bool_map(eq, eq.subs(c, x))
1056
1604
    (And(Or(Not(a), Not(b)), Or(a, b), c, d), {a: a, b: b, c: d, d: x})
1057
1605
 
1058
1606
    """
1067
1615
        arguments are only symbols or negated symbols. For example,
1068
1616
        And(x, Not(y), Or(w, Not(z))).
1069
1617
 
1070
 
        Basic.match is not robust enough (see issue 1736) so this is
 
1618
        Basic.match is not robust enough (see issue 4835) so this is
1071
1619
        a workaround that is valid for simplified boolean expressions
1072
1620
        """
1073
1621
 
1089
1637
 
1090
1638
        # assemble the match dictionary if possible
1091
1639
        matchdict = {}
1092
 
        for k in list(f1.keys()):
 
1640
        for k in f1.keys():
1093
1641
            if k not in f2:
1094
1642
                return False
1095
1643
            if len(f1[k]) != len(f2[k]):
1101
1649
    a = simplify_logic(bool1)
1102
1650
    b = simplify_logic(bool2)
1103
1651
    m = match(a, b)
1104
 
    if m and info:
 
1652
    if m:
1105
1653
        return a, m
1106
1654
    return m is not None
 
1655
 
 
1656
 
 
1657
@deprecated(
 
1658
    useinstead="bool_map", issue=7197, deprecated_since_version="0.7.4")
 
1659
def bool_equal(bool1, bool2, info=False):
 
1660
    """Return True if the two expressions represent the same logical
 
1661
    behaviour for some correspondence between the variables of each
 
1662
    (which may be different). For example, And(x, y) is logically
 
1663
    equivalent to And(a, b) for {x: a, y: b} (or vice versa). If the
 
1664
    mapping is desired, then set ``info`` to True and the simplified
 
1665
    form of the functions and mapping of variables will be returned.
 
1666
    """
 
1667
 
 
1668
    mapping = bool_map(bool1, bool2)
 
1669
    if not mapping:
 
1670
        return False
 
1671
    if info:
 
1672
        return mapping
 
1673
    return True