Repository: sympy/sympy

Issue:
Incorrect simplification when mixing basic logical operators and equality
Have I misunderstood something about how sympy is supposed to work? This basic simplification of a small logical expression is incorrect.

`from sympy import *

a,b,c = symbols("a b c")

expr = Or(And(a,c), Eq(a,b))

# incorrectly simplifies to a & c
print(expr) # a & c

# counter-example

# Or(And(a,c), Eq(a,b)) with a=True, b=True, c=False

# The simplification incorrectly returns False
print(expr.subs({a:True, b:True, c:False})) # False

# The actual value is True
print(Or(And(True,False), Eq(True,True))) # True`

Discussion:

Patch:
diff --git a/.mailmap b/.mailmap
index 34c061d0b2..20c42ee993 100644
--- a/.mailmap
+++ b/.mailmap
@@ -1352,6 +1352,7 @@ Tanu Hari Dixit <tokencolour@gmail.com>
 Tarang Patel <tarangrockr@gmail.com> <tarang@ubuntu.ubuntu-domain>
 Tarun Gaba <tarun.gaba7@gmail.com>
 Tasha Kim <jae_young_kim@brown.edu>
+Taylan Sahin <info@taylansahin.net>
 Ted Dokos <tdokos@gmail.com> <t.dokos@gmail.com>
 Ted Horst <ted.horst@earthlink.net>
 Tejaswini Sanapathi <sastejaswini2002@gmail.com>
diff --git a/sympy/logic/boolalg.py b/sympy/logic/boolalg.py
index 27213a215b..ac190ac508 100644
--- a/sympy/logic/boolalg.py
+++ b/sympy/logic/boolalg.py
@@ -490,25 +490,7 @@ def __lt__(self, other):
 
     @classmethod
     def binary_check_and_simplify(self, *args):
-        from sympy.core.relational import Relational, Eq, Ne
-        args = [as_Boolean(i) for i in args]
-        bin_syms = set().union(*[i.binary_symbols for i in args])
-        rel = set().union(*[i.atoms(Relational) for i in args])
-        reps = {}
-        for x in bin_syms:
-            for r in rel:
-                if x in bin_syms and x in r.free_symbols:
-                    if isinstance(r, (Eq, Ne)):
-                        if not (
-                                true in r.args or
-                                false in r.args):
-                            reps[r] = false
-                    else:
-                        raise TypeError(filldedent('''
-                            Incompatible use of binary symbol `%s` as a
-                            real variable in `%s`
-                            ''' % (x, r)))
-        return [i.subs(reps) for i in args]
+        return [as_Boolean(i) for i in args]
 
     def to_nnf(self, simplify=True):
         return self._to_nnf(*self.args, simplify=simplify)


Test patch:
diff --git a/sympy/logic/tests/test_boolalg.py b/sympy/logic/tests/test_boolalg.py
index 7b50f8ebd7..f31ba25610 100644
--- a/sympy/logic/tests/test_boolalg.py
+++ b/sympy/logic/tests/test_boolalg.py
@@ -57,7 +57,6 @@ def test_And():
     assert And(True, False, A) is false
     assert And(1, A) == A
     raises(TypeError, lambda: And(2, A))
-    raises(TypeError, lambda: And(A < 2, A))
     assert And(A < 1, A >= 1) is false
     e = A > 1
     assert And(e, e.canonical) == e.canonical
@@ -82,7 +81,6 @@ def test_Or():
     assert Or(False, False, A) == A
     assert Or(1, A) is true
     raises(TypeError, lambda: Or(2, A))
-    raises(TypeError, lambda: Or(A < 2, A))
     assert Or(A < 1, A >= 1) is true
     e = A > 1
     assert Or(e, e.canonical) == e
@@ -304,7 +302,6 @@ def test_simplification_boolalg():
     assert simplify_logic(Equivalent(A, B)) == \
         Or(And(A, B), And(Not(A), Not(B)))
     assert simplify_logic(And(Equality(A, 2), C)) == And(Equality(A, 2), C)
-    assert simplify_logic(And(Equality(A, 2), A)) is S.false
     assert simplify_logic(And(Equality(A, 2), A)) == And(Equality(A, 2), A)
     assert simplify_logic(And(Equality(A, B), C)) == And(Equality(A, B), C)
     assert simplify_logic(Or(And(Equality(A, 3), B), And(Equality(A, 3), C))) \
@@ -676,7 +673,6 @@ def test_ITE():
     assert ITE(1, 1, 1) is S.true
     assert isinstance(ITE(1, 1, 1, evaluate=False), ITE)
 
-    raises(TypeError, lambda: ITE(x > 1, y, x))
     assert ITE(Eq(x, True), y, x) == ITE(x, y, x)
     assert ITE(Eq(x, False), y, x) == ITE(~x, y, x)
     assert ITE(Ne(x, True), y, x) == ITE(~x, y, x)
@@ -1345,3 +1341,9 @@ def test_relational_threeterm_simplification_patterns_numerically():
                 assert originalvalue == simplifiedvalue, "Original: {}\nand"\
                     " simplified: {}\ndo not evaluate to the same value for"\
                     "{}".format(pattern[0], simplified, sublist)
+
+
+def test_issue_25451():
+    x = Or(And(a, c), Eq(a, b))
+    assert isinstance(x, Or)
+    assert set(x.args) == {And(a, c), Eq(a, b)}