1import itertools
2
3import pytest
4
5from diofant import (ITE, And, Dummy, EmptySet, Eq, Equality, Equivalent,
6                     Implies, Integer, Interval, Nand, Nor, Not, Or, POSform,
7                     S, SOPform, Unequality, Union, Xor, bool_map, false, oo,
8                     simplify, simplify_logic, sqrt, symbols, to_cnf, to_dnf,
9                     to_nnf, true)
10from diofant.abc import A, B, C, D, a, b, c, w, x, y, z
11from diofant.logic.boolalg import (Boolean, BooleanAtom, BooleanFunction,
12                                   conjuncts, disjuncts,
13                                   distribute_and_over_or,
14                                   distribute_or_over_and,
15                                   eliminate_implications, is_cnf, is_dnf,
16                                   is_literal, is_nnf, to_int_repr)
17
18
19__all__ = ()
20
21
22def test_overloading():
23    """Test that |, & are overloaded as expected."""
24    assert A & B == And(A, B)
25    assert A | B == Or(A, B)
26    assert (A & B) | C == Or(And(A, B), C)
27    assert A >> B == Implies(A, B)
28    assert A << B == Implies(B, A)
29    assert ~A == Not(A)
30    assert A ^ B == Xor(A, B)
31
32
33def test_And():
34
35    assert And() is true
36    assert And(A) == A
37    assert And(True) is true
38    assert And(False) is false
39    assert And(True, True) is true
40    assert And(True, False) is false
41    assert And(True, False, evaluate=False) is not false
42    assert And(False, False) is false
43    assert And(True, A) == A
44    assert And(False, A) is false
45    assert And(True, True, True) is true
46    assert And(True, True, A) == A
47    assert And(True, False, A) is false
48    assert And(2, A) == A
49    assert And(2, 3) is true
50    assert And(A < 1, A >= 1) is false
51    e = A > 1
52    assert And(e, e.canonical) == e.canonical
53    g, l, ge, le = A > B, B < A, A >= B, B <= A
54    assert And(g, l, ge, le) == And(l, le)
55
56
57def test_Or():
58
59    assert Or() is false
60    assert Or(A) == A
61    assert Or(True) is true
62    assert Or(False) is false
63    assert Or(True, True) is true
64    assert Or(True, False) is true
65    assert Or(False, False) is false
66    assert Or(True, A) is true
67    assert Or(False, A) == A
68    assert Or(True, False, False) is true
69    assert Or(True, False, A) is true
70    assert Or(False, False, A) == A
71    assert Or(2, A) is true
72    assert Or(A < 1, A >= 1) is true
73    e = A > 1
74    assert Or(e, e.canonical) == e
75    g, l, ge, le = A > B, B < A, A >= B, B <= A
76    assert Or(g, l, ge, le) == Or(g, ge)
77
78
79def test_Xor():
80
81    assert Xor() is false
82    assert Xor(A) == A
83    assert Xor(A, A) is false
84    assert Xor(True, A, A) is true
85    assert Xor(A, A, A, A, A) == A
86    assert Xor(True, False, False, A, B) == ~Xor(A, B)
87    assert Xor(True) is true
88    assert Xor(False) is false
89    assert Xor(True, True) is false
90    assert Xor(True, False) is true
91    assert Xor(False, False) is false
92    assert Xor(True, A) == ~A
93    assert Xor(False, A) == A
94    assert Xor(True, False, False) is true
95    assert Xor(True, False, A) == ~A
96    assert Xor(False, False, A) == A
97    assert isinstance(Xor(A, B), Xor)
98    assert Xor(A, B, Xor(C, D)) == Xor(A, B, C, D)
99    assert Xor(A, B, Xor(B, C)) == Xor(A, C)
100    assert Xor(A < 1, A >= 1, B) == Xor(0, 1, B) == Xor(1, 0, B)
101    e = A > 1
102    assert Xor(e, e.canonical) == Xor(0, 0) == Xor(1, 1)
103    e = Integer(1) < A
104    assert e != e.canonical and Xor(e, e.canonical) is false
105    assert Xor(A > 1, B > C) == Xor(A > 1, B > C, evaluate=False)
106
107
108def test_Not():
109
110    pytest.raises(TypeError, lambda: Not(True, False))
111    assert Not(True) is false
112    assert Not(False) is true
113    assert Not(0) is true
114    assert Not(1) is false
115    assert Not(2) is false
116    assert Not(Unequality(A, B)) == Equality(A, B)
117
118
119def test_Nand():
120
121    assert Nand() is false
122    assert Nand(A) == ~A
123    assert Nand(True) is false
124    assert Nand(False) is true
125    assert Nand(True, True) is false
126    assert Nand(True, False) is true
127    assert Nand(False, False) is true
128    assert Nand(True, A) == ~A
129    assert Nand(False, A) is true
130    assert Nand(True, True, True) is false
131    assert Nand(True, True, A) == ~A
132    assert Nand(True, False, A) is true
133
134
135def test_Nor():
136
137    assert Nor() is true
138    assert Nor(A) == ~A
139    assert Nor(True) is false
140    assert Nor(False) is true
141    assert Nor(True, True) is false
142    assert Nor(True, False) is false
143    assert Nor(False, False) is true
144    assert Nor(True, A) is false
145    assert Nor(False, A) == ~A
146    assert Nor(True, True, True) is false
147    assert Nor(True, True, A) is false
148    assert Nor(True, False, A) is false
149
150
151def test_Implies():
152
153    pytest.raises(ValueError, lambda: Implies(A, B, C))
154    assert Implies(True, True) is true
155    assert Implies(True, False) is false
156    assert Implies(False, True) is true
157    assert Implies(False, False) is true
158    assert Implies(0, A) is true
159    assert Implies(1, 1) is true
160    assert Implies(1, 0) is false
161    assert A >> B == B << A
162    assert (A < 1) >> (A >= 1) == (A >= 1)
163    assert (A < 1) >> (Integer(1) > A) is true
164    assert A >> A is true
165    assert ((A < 1) >> (B >= 1)) == Implies(A < 1, B >= 1, evaluate=False)
166
167
168def test_Equivalent():
169
170    assert Equivalent(A, B) == Equivalent(B, A) == Equivalent(A, B, A)
171    assert Equivalent() is true
172    assert Equivalent(A, A) == Equivalent(A) is true
173    assert Equivalent(True, True) == Equivalent(False, False) is true
174    assert Equivalent(True, False) == Equivalent(False, True) is false
175    assert Equivalent(A, True) == A
176    assert Equivalent(A, False) == Not(A)
177    assert Equivalent(A, B, True) == A & B
178    assert Equivalent(A, B, False) == ~A & ~B
179    assert Equivalent(1, A) == A
180    assert Equivalent(0, A) == Not(A)
181    assert Equivalent(A, Equivalent(B, C)) != Equivalent(Equivalent(A, B), C)
182    assert Equivalent(A < 1, A >= 1) is false
183    assert Equivalent(A < 1, A >= 1, 0) is false
184    assert Equivalent(A < 1, A >= 1, 1) is false
185    assert Equivalent(A < 1, Integer(1) > A) == Equivalent(1, 1) == Equivalent(0, 0)
186    assert Equivalent(A < 1, B >= 1) == Equivalent(B >= 1, A < 1, evaluate=False)
187
188
189def test_equals():
190    assert Not(Or(A, B)).equals(And(Not(A), Not(B))) is True
191    assert Equivalent(A, B).equals((A >> B) & (B >> A)) is True
192    assert ((A | ~B) & (~A | B)).equals((~A & ~B) | (A & B)) is True
193    assert (A >> B).equals(~A >> ~B) is False
194    assert (A >> (B >> A)).equals(A >> (C >> A)) is False
195    pytest.raises(NotImplementedError, lambda: And(A, A < B).equals(And(A, B > A)))
196
197
198def test_simplification():
199    """Test working of simplification methods."""
200    set1 = [[0, 0, 1], [0, 1, 1], [1, 0, 0], [1, 1, 0]]
201    set2 = [[0, 0, 0], [0, 1, 0], [1, 0, 1], [1, 1, 1]]
202    assert SOPform([x, y, z], set1) == Or(And(Not(x), z), And(Not(z), x))
203    assert Not(SOPform([x, y, z], set2)) == Not(Or(And(Not(x), Not(z)), And(x, z)))
204    assert POSform([x, y, z], set1 + set2) is true
205    assert SOPform([x, y, z], set1 + set2) is true
206    assert SOPform([Dummy(), Dummy(), Dummy()], set1 + set2) is true
207
208    minterms = [[0, 0, 0, 1], [0, 0, 1, 1], [0, 1, 1, 1], [1, 0, 1, 1],
209                [1, 1, 1, 1]]
210    dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]]
211    assert (
212        SOPform([w, x, y, z], minterms, dontcares) ==
213        Or(And(Not(w), z), And(y, z)))
214    assert POSform([w, x, y, z], minterms, dontcares) == And(Or(Not(w), y), z)
215
216    # test simplification
217    ans = And(A, Or(B, C))
218    assert simplify_logic(A & (B | C)) == ans
219    assert simplify_logic((A & B) | (A & C)) == ans
220    assert simplify_logic(Implies(A, B)) == Or(Not(A), B)
221    assert simplify_logic(Equivalent(A, B)) == \
222        Or(And(A, B), And(Not(A), Not(B)))
223    assert simplify_logic(And(Equality(A, 2), C)) == And(Equality(A, 2), C)
224    assert simplify_logic(And(Equality(A, 2), A)) == And(Equality(A, 2), A)
225    assert simplify_logic(And(Equality(A, B), C)) == And(Equality(A, B), C)
226    assert simplify_logic(Or(And(Equality(A, 3), B), And(Equality(A, 3), C))) \
227        == And(Equality(A, 3), Or(B, C))
228    e = And(A, x**2 - x)
229    assert simplify_logic(e) == And(A, x*(x - 1))
230    assert simplify_logic(e, deep=False) == e
231    pytest.raises(ValueError, lambda: simplify_logic(A & (B | C), form='spam'))
232
233    e = x & y ^ z | (z ^ x)
234    res = [(x & ~z) | (z & ~x) | (z & ~y), (x & ~y) | (x & ~z) | (z & ~x)]
235    assert simplify_logic(e) in res
236    assert SOPform([z, y, x], [[0, 0, 1], [0, 1, 1],
237                               [1, 0, 0], [1, 0, 1], [1, 1, 0]]) == res[1]
238
239    # check input
240    ans = SOPform([x, y], [[1, 0]])
241    assert SOPform([x, y], [[1, 0]]) == ans
242    assert POSform([x, y], [[1, 0]]) == ans
243
244    pytest.raises(ValueError, lambda: SOPform([x], [[1]], [[1]]))
245    assert SOPform([x], [[1]], [[0]]) is true
246    assert SOPform([x], [[0]], [[1]]) is true
247    assert SOPform([x], [], []) is false
248
249    pytest.raises(ValueError, lambda: POSform([x], [[1]], [[1]]))
250    assert POSform([x], [[1]], [[0]]) is true
251    assert POSform([x], [[0]], [[1]]) is true
252    assert POSform([x], [], []) is false
253
254    # check working of simplify
255    assert simplify((A & B) | (A & C)) == And(A, Or(B, C))
256    assert simplify(And(x, Not(x))) is false
257    assert simplify(Or(x, Not(x))) is true
258
259
260def test_bool_map():
261    """Test working of bool_map function."""
262    minterms = [[0, 0, 0, 1], [0, 0, 1, 1], [0, 1, 1, 1], [1, 0, 1, 1],
263                [1, 1, 1, 1]]
264    assert bool_map(Not(Not(a)), a) == (a, {a: a})
265    assert bool_map(SOPform([w, x, y, z], minterms),
266                    POSform([w, x, y, z], minterms)) == \
267        (And(Or(Not(w), y), Or(Not(x), y), z), {x: x, w: w, z: z, y: y})
268    assert bool_map(SOPform([x, z, y], [[1, 0, 1]]),
269                    SOPform([a, b, c], [[1, 0, 1]])) is not False
270    function1 = SOPform([x, z, y], [[1, 0, 1], [0, 0, 1]])
271    function2 = SOPform([a, b, c], [[1, 0, 1], [1, 0, 0]])
272    assert bool_map(function1, function2) == \
273        (function1, {y: a, z: b})
274    assert bool_map(And(x, Not(y)), Or(y, Not(x))) is False
275    assert bool_map(And(x, Not(y)), And(y, Not(x), z)) is False
276    assert bool_map(And(x, Not(y)), And(Or(y, z), Not(x))) is False
277    assert bool_map(Or(And(Not(y), a), And(Not(y), b), And(x, y)),
278                    Or(x, y, a)) is False
279
280
281def test_bool_symbol():
282    """Test that mixing symbols with boolean values works as expected."""
283    assert And(A, True) == A
284    assert And(A, True, True) == A
285    assert And(A, False) is false
286    assert And(A, True, False) is false
287    assert Or(A, True) is true
288    assert Or(A, False) == A
289
290
291def test_is_boolean():
292
293    assert true.is_Boolean
294    assert (A & B).is_Boolean
295    assert (A | B).is_Boolean
296    assert (~A).is_Boolean
297    assert (A ^ B).is_Boolean
298
299
300def test_subs():
301
302    assert (A & B).subs({A: True}) == B
303    assert (A & B).subs({A: False}) is false
304    assert (A & B).subs({B: True}) == A
305    assert (A & B).subs({B: False}) is false
306    assert (A & B).subs({A: True, B: True}) is true
307    assert (A | B).subs({A: True}) is true
308    assert (A | B).subs({A: False}) == B
309    assert (A | B).subs({B: True}) is true
310    assert (A | B).subs({B: False}) == A
311    assert (A | B).subs({A: True, B: True}) is true
312
313
314"""
315we test for axioms of boolean algebra
316see https://en.wikipedia.org/wiki/Boolean_algebra_(structure)
317"""
318
319
320def test_commutative():
321    """Test for commutativity of And and Or."""
322    A, B = map(Boolean, symbols('A,B'))
323
324    assert A & B == B & A
325    assert A | B == B | A
326
327
328def test_and_associativity():
329    """Test for associativity of And."""
330    assert (A & B) & C == A & (B & C)
331
332
333def test_or_assicativity():
334
335    assert ((A | B) | C) == (A | (B | C))
336
337
338def test_double_negation():
339    a = Boolean()
340    assert ~(~a) == a
341
342
343# test methods
344
345def test_eliminate_implications():
346    assert eliminate_implications(Implies(A, B, evaluate=False)) == (~A) | B
347    assert eliminate_implications(
348        A >> (C >> Not(B))) == Or(Or(Not(B), Not(C)), Not(A))
349    assert eliminate_implications(Equivalent(A, B, C, D)) == \
350        (~A | B) & (~B | C) & (~C | D) & (~D | A)
351
352
353def test_conjuncts():
354    assert conjuncts(A & B & C) == {A, B, C}
355    assert conjuncts((A | B) & C) == {A | B, C}
356    assert conjuncts(A) == {A}
357    assert conjuncts(True) == {True}
358    assert conjuncts(False) == {False}
359
360
361def test_disjuncts():
362    assert disjuncts(A | B | C) == {A, B, C}
363    assert disjuncts((A | B) & C) == {(A | B) & C}
364    assert disjuncts(A) == {A}
365    assert disjuncts(True) == {True}
366    assert disjuncts(False) == {False}
367
368
369def test_distribute():
370
371    assert distribute_and_over_or(Or(And(A, B), C)) == And(Or(A, C), Or(B, C))
372    assert distribute_or_over_and(And(A, Or(B, C))) == Or(And(A, B), And(A, C))
373
374
375def test_to_nnf():
376    assert to_nnf(true) is true
377    assert to_nnf(false) is false
378    assert to_nnf(A) == A
379    assert (~A).to_nnf() == ~A
380
381    class Boo(BooleanFunction):
382        pass
383
384    pytest.raises(ValueError, lambda: to_nnf(~Boo(A)))
385
386    assert to_nnf(A | ~A | B) is true
387    assert to_nnf(A & ~A & B) is false
388    assert to_nnf(A >> B) == ~A | B
389    assert to_nnf(Equivalent(A, B, C)) == (~A | B) & (~B | C) & (~C | A)
390    assert to_nnf(A ^ B ^ C) == \
391        (A | B | C) & (~A | ~B | C) & (A | ~B | ~C) & (~A | B | ~C)
392    assert to_nnf(ITE(A, B, C)) == (~A | B) & (A | C)
393    assert to_nnf(Not(A | B | C)) == ~A & ~B & ~C
394    assert to_nnf(Not(A & B & C)) == ~A | ~B | ~C
395    assert to_nnf(Not(A >> B)) == A & ~B
396    assert to_nnf(Not(Equivalent(A, B, C))) == And(Or(A, B, C), Or(~A, ~B, ~C))
397    assert to_nnf(Not(A ^ B ^ C)) == \
398        (~A | B | C) & (A | ~B | C) & (A | B | ~C) & (~A | ~B | ~C)
399    assert to_nnf(Not(ITE(A, B, C))) == (~A | ~B) & (A | ~C)
400    assert to_nnf((A >> B) ^ (B >> A)) == (A & ~B) | (~A & B)
401    assert to_nnf((A >> B) ^ (B >> A), False) == \
402        (~A | ~B | A | B) & ((A & ~B) | (~A & B))
403
404
405def test_to_cnf():
406
407    assert to_cnf(~(B | C)) == And(Not(B), Not(C))
408    assert to_cnf((A & B) | C) == And(Or(A, C), Or(B, C))
409    assert to_cnf(A >> B) == (~A) | B
410    assert to_cnf(A >> (B & C)) == (~A | B) & (~A | C)
411    assert to_cnf(A & (B | C) | ~A & (B | C), True) == B | C
412
413    assert to_cnf(Equivalent(A, B)) == And(Or(A, Not(B)), Or(B, Not(A)))
414    assert to_cnf(Equivalent(A, B & C)) == \
415        (~A | B) & (~A | C) & (~B | ~C | A)
416    assert to_cnf(Equivalent(A, B | C), True) == \
417        And(Or(Not(B), A), Or(Not(C), A), Or(B, C, Not(A)))
418    assert to_cnf(~(A | B) | C) == And(Or(Not(A), C), Or(Not(B), C))
419
420
421def test_to_dnf():
422    assert to_dnf(true) == true
423    assert to_dnf((~B) & (~C)) == (~B) & (~C)
424    assert to_dnf(~(B | C)) == And(Not(B), Not(C))
425    assert to_dnf(A & (B | C)) == Or(And(A, B), And(A, C))
426    assert to_dnf(A >> B) == (~A) | B
427    assert to_dnf(A >> (B & C)) == (~A) | (B & C)
428
429    assert to_dnf(Equivalent(A, B), True) == \
430        Or(And(A, B), And(Not(A), Not(B)))
431    assert to_dnf(Equivalent(A, B & C), True) == \
432        Or(And(A, B, C), And(Not(A), Not(B)), And(Not(A), Not(C)))
433
434
435def test_to_int_repr():
436    x, y, z = map(Boolean, symbols('x,y,z'))
437
438    def sorted_recursive(arg):
439        try:
440            return sorted(sorted_recursive(x) for x in arg)
441        except TypeError:  # arg is not a sequence
442            return arg
443
444    assert sorted_recursive(to_int_repr([x | y, z | x], [x, y, z])) == \
445        sorted_recursive([[1, 2], [1, 3]])
446    assert sorted_recursive(to_int_repr([x | y, z | ~x], [x, y, z])) == \
447        sorted_recursive([[1, 2], [3, -1]])
448
449
450def test_is_nnf():
451    assert is_nnf(true) is True
452    assert is_nnf(A) is True
453    assert is_nnf(~A) is True
454    assert is_nnf(A & B) is True
455    assert is_nnf((A & B) | (~A & A) | (~B & B) | (~A & ~B), False) is True
456    assert is_nnf((A | B) & (~A | ~B)) is True
457    assert is_nnf(Not(Or(A, B))) is False
458    assert is_nnf(A ^ B) is False
459    assert is_nnf((A & B) | (~A & A) | (~B & B) | (~A & ~B), True) is False
460
461
462def test_is_cnf():
463    assert is_cnf(x) is True
464    assert is_cnf(x | y | z) is True
465    assert is_cnf(x & y & z) is True
466    assert is_cnf((x | y) & z) is True
467    assert is_cnf((x & y) | z) is False
468    assert is_cnf(x & y & (z | ~(x ^ y))) is False
469    assert is_cnf(x & y & (z | (x ^ y))) is False
470
471
472def test_is_dnf():
473    assert is_dnf(x) is True
474    assert is_dnf(x | y | z) is True
475    assert is_dnf(x & y & z) is True
476    assert is_dnf((x & y) | z) is True
477    assert is_dnf((x | y) & z) is False
478
479
480def test_ITE():
481    A, B, C = map(Boolean, symbols('A,B,C'))
482
483    pytest.raises(ValueError, lambda: ITE(A, B))
484
485    assert ITE(True, False, True) is false
486    assert ITE(True, True, False) is true
487    assert ITE(False, True, False) is false
488    assert ITE(False, False, True) is true
489    assert isinstance(ITE(A, B, C), ITE)
490
491    assert ITE(True, B, C) == B
492    assert ITE(False, B, C) == C
493
494    assert ITE(A, B, B) == B
495
496    assert ITE(C, False, True) == Not(C)
497    assert ITE(C, True, False) == C
498
499
500def test_ITE_diff():
501    # analogous to Piecewise.diff
502    assert ITE(x > 0, x**2, x).diff(x) == ITE(x > 0, 2*x, 1)
503
504
505def test_is_literal():
506    assert is_literal(True) is True
507    assert is_literal(False) is True
508    assert is_literal(A) is True
509    assert is_literal(~A) is True
510    assert is_literal(Or(A, B)) is False
511    assert is_literal(Or(A, B)) is False
512
513
514def test_operators():
515    # Mostly test __and__, __rand__, and so on
516    assert True & A == (A & True) == A
517    assert False & A == (A & False) == false
518    assert A & B == And(A, B)
519    assert True | A == (A | True) == true
520    assert False | A == (A | False) == A
521    assert A | B == Or(A, B)
522    assert ~A == Not(A)
523    assert True >> A == (A << True) == A
524    assert False >> A == (A << False) == true
525    assert (A >> True) == (True << A) == true
526    assert (A >> False) == (False << A) == ~A
527    assert A >> B == B << A == Implies(A, B)
528    assert True ^ A == A ^ True == ~A
529    assert False ^ A == (A ^ False) == A
530    assert A ^ B == Xor(A, B)
531
532
533def test_true_false():
534    assert true is true
535    assert false is false
536    assert true is not True
537    assert false is not False
538    assert true
539    assert not false
540    assert true == True  # noqa: E712
541    assert false == False  # noqa: E712
542    assert not true == False  # noqa: E712
543    assert not false == True  # noqa: E712
544    assert not true == false
545
546    assert hash(true) == hash(True)
547    assert hash(false) == hash(False)
548    assert len({true, True}) == len({false, False}) == 1
549
550    assert int(true) == 1
551    assert int(false) == 0
552
553    assert isinstance(true, BooleanAtom)
554    assert isinstance(false, BooleanAtom)
555    # We don't want to subclass from bool, because bool subclasses from
556    # int. But operators like &, |, ^, <<, >>, and ~ act differently on 0 and
557    # 1 then we want them to on true and false.  See the docstrings of the
558    # various And, Or, etc. functions for examples.
559    assert not isinstance(true, bool)
560    assert not isinstance(false, bool)
561
562    # Note: using 'is' comparison is important here. We want these to return
563    # true and false, not True and False
564
565    assert Not(true) is false
566    assert Not(True) is false
567    assert Not(false) is true
568    assert Not(False) is true
569    assert ~true is false
570    assert ~false is true
571
572    for T, F in itertools.product([True, true], [False, false]):
573        assert And(T, F) is false
574        assert And(F, T) is false
575        assert And(F, F) is false
576        assert And(T, T) is true
577        assert And(T, x) == x
578        assert And(F, x) is false
579        if not (T is True and F is False):
580            assert T & F is false
581            assert F & T is false
582        if F is not False:
583            assert F & F is false
584        if T is not True:
585            assert T & T is true
586
587        assert Or(T, F) is true
588        assert Or(F, T) is true
589        assert Or(F, F) is false
590        assert Or(T, T) is true
591        assert Or(T, x) is true
592        assert Or(F, x) == x
593        if not (T is True and F is False):
594            assert T | F is true
595            assert F | T is true
596        if F is not False:
597            assert F | F is false
598        if T is not True:
599            assert T | T is true
600
601        assert Xor(T, F) is true
602        assert Xor(F, T) is true
603        assert Xor(F, F) is false
604        assert Xor(T, T) is false
605        assert Xor(T, x) == ~x
606        assert Xor(F, x) == x
607        if not (T is True and F is False):
608            assert T ^ F is true
609            assert F ^ T is true
610        if F is not False:
611            assert F ^ F is false
612        if T is not True:
613            assert T ^ T is false
614
615        assert Nand(T, F) is true
616        assert Nand(F, T) is true
617        assert Nand(F, F) is true
618        assert Nand(T, T) is false
619        assert Nand(T, x) == ~x
620        assert Nand(F, x) is true
621
622        assert Nor(T, F) is false
623        assert Nor(F, T) is false
624        assert Nor(F, F) is true
625        assert Nor(T, T) is false
626        assert Nor(T, x) is false
627        assert Nor(F, x) == ~x
628
629        assert Implies(T, F) is false
630        assert Implies(F, T) is true
631        assert Implies(F, F) is true
632        assert Implies(T, T) is true
633        assert Implies(T, x) == x
634        assert Implies(F, x) is true
635        assert Implies(x, T) is true
636        assert Implies(x, F) == ~x
637        if not (T is True and F is False):
638            assert T >> F is false
639            assert F << T is false
640            assert F >> T is true
641            assert T << F is true
642        if F is not False:
643            assert F >> F is true
644            assert F << F is true
645        if T is not True:
646            assert T >> T is true
647            assert T << T is true
648
649        assert Equivalent(T, F) is false
650        assert Equivalent(F, T) is false
651        assert Equivalent(F, F) is true
652        assert Equivalent(T, T) is true
653        assert Equivalent(T, x) == x
654        assert Equivalent(F, x) == ~x
655        assert Equivalent(x, T) == x
656        assert Equivalent(x, F) == ~x
657
658        assert ITE(T, T, T) is true
659        assert ITE(T, T, F) is true
660        assert ITE(T, F, T) is false
661        assert ITE(T, F, F) is false
662        assert ITE(F, T, T) is true
663        assert ITE(F, T, F) is false
664        assert ITE(F, F, T) is true
665        assert ITE(F, F, F) is false
666
667
668def test_bool_as_set():
669    assert And(x <= 2, x >= -2).as_set() == Interval(-2, 2)
670    assert Or(x >= 2, x <= -2).as_set() == (Interval(-oo, -2) +
671                                            Interval(2, oo, False))
672    assert Not(x > 2, evaluate=False).as_set() == Interval(-oo, 2, True)
673    # issue sympy/sympy#10240
674    assert Not(And(x > 2, x < 3)).as_set() == \
675        Union(Interval(-oo, 2, True), Interval(3, oo, False, True))
676    assert true.as_set() == S.UniversalSet
677    assert false.as_set() == EmptySet()
678
679
680@pytest.mark.xfail
681def test_multivariate_bool_as_set():
682    And(x >= 0, y >= 0).as_set()  # == Interval(0, oo)*Interval(0, oo)
683    Or(x >= 0, y >= 0).as_set()
684    # == S.Reals*S.Reals - Interval(-oo, 0, True, True)*Interval(-oo, 0, True, True)
685
686
687def test_all_or_nothing():
688    x = symbols('x', extended_real=True)
689    args = x >= - oo, x <= oo
690    v = And(*args)
691    if isinstance(v, And):
692        assert len(v.args) == len(args) - args.count(true)
693    else:
694        assert v
695    v = Or(*args)
696    if isinstance(v, Or):
697        assert len(v.args) == 2
698    else:
699        assert v
700
701
702def test_canonical_atoms():
703    assert true.canonical == true
704    assert false.canonical == false
705
706
707def test_sympyissue_8777():
708    assert And(x > 2, x < oo).as_set() == Interval(2, oo, True, True)
709    assert And(x >= 1, x < oo).as_set() == Interval(1, oo, False, True)
710    assert (x < oo).as_set() == Interval(-oo, oo, False, True)
711    assert (x > -oo).as_set() == Interval(-oo, oo, True)
712
713
714def test_sympyissue_8975():
715    assert Or(And(-oo < x, x <= -2), And(2 <= x, x < oo)).as_set() == \
716        Interval(-oo, -2, True) + Interval(2, oo, False, True)
717
718
719def test_sympyissue_12522():
720    assert Eq(1, 1).simplify() is true
721    assert true.simplify() is true
722    assert false.simplify() is false
723
724
725def test_sympyissue_10641():
726    assert str(Or(x < sqrt(3), x).evalf(2)) == 'x | (x < 1.7)'
727    assert str(And(x < sqrt(3), x).evalf(2)) == 'x & (x < 1.7)'
728