Repository: sympy/sympy
Pull request: Improve Logical Simplification Handling in sympy.logic.boolalg
<!-- Your title above should be a short description of what
was changed. Do not include the issue number in the title. -->

#### References to other Issues or PRs
Fixes #25451 
<!-- If this pull request fixes an issue, write "Fixes #NNNN" in that exact
format, e.g. "Fixes #1234" (see
https://tinyurl.com/auto-closing for more information). Also, please
write a comment on that issue linking back to this pull request once it is
open. -->


#### Brief description of what is fixed or changed

- Revised the `binary_check_and_simplify` function in the `boolalg` module to handle binary symbols more effectively in logical expressions.
- Eliminated unnecessary error raises for certain relational expressions that involve binary symbols.

#### Other comments
Separately we could consider improving the detection of erroneous mixing of symbols as Expr and Boolean but I don't think it is very important: time would be better spent adding a BooleanSymbol class and considering if we would ever be able to deprecate using Symbol as a Boolean.

#### Release Notes

<!-- Write the release notes for this release below between the BEGIN and END
statements. The basic format is a bulleted list with the name of the subpackage
and the release note for this PR. For example:

* solvers
  * Added a new solver for logarithmic equations.

* functions
  * Fixed a bug with log of integers. Formerly, `log(-x)` incorrectly gave `-log(x)`.

* physics.units
  * Corrected a semantical error in the conversion between volt and statvolt which
    reported the volt as being larger than the statvolt.

or if no release note(s) should be included use:

NO ENTRY

See https://github.com/sympy/sympy/wiki/Writing-Release-Notes for more
information on how to write release notes. The bot will check your release
notes automatically to see if they are formatted correctly. -->

<!-- BEGIN RELEASE NOTES -->

* logic
  * Improved handling of logical simplification involving binary symbols like `Eq`
 
<!-- END RELEASE NOTES -->


Problem statement:
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.

```python
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
```

Hints from issue discussion:
You are right that this simplification is incorrect:
```python
In [18]: c1 = And(a, c)

In [19]: c2 = Eq(a, b)

In [20]: c1
Out[20]: a ∧ c

In [21]: c2
Out[21]: a = b

In [22]: c1 | c2
Out[22]: a ∧ c
```
Probably somewhere this comes from mixing up the idea of Symbol as being both `Expr` and `Boolean` (there should be a separate `BooleanSymbol` type). In the case of `Eq(a, b)` both `a` and `b` would be implicitly assumed to be `Expr` whereas for `And(a, c)` both `a` and `c` would be implicitly assumed to be `Boolean`. We can see the confused code that tries to handle this here:
https://github.com/sympy/sympy/blob/221d773085642f7e30440ba6ffa122d5bfbb1042/sympy/logic/boolalg.py#L491-L511
That sets `Eq(a, b)` to false because true and false are not in its args. Apparently it expects that if the `Eq` contains "binary symbols" then it must only be something like `Eq(a, True)` or otherwise we can just set it to false?

I really can't fathom what the purpose of that code is. Usually at this point I would suggest a way to fix the code but maybe the whole function should just be deleted. It has two purposes, one of which is to set any `Eq` or `Ne` to false if it has binary symbols among its free symbols and does not contain true or false. I can't even imagine a situation where that is valid.

The other purpose of the code seems to be to raise an error if we have a relational that is not an `Eq` or `Ne` and that contains any binary symbol among its free symbols. I guess this is to raise an error for `a > 0` if `a` is also being used as a "binary" symbol:
```python
In [3]: a & (a > 0)
---------------------------------------------------------------------------
TypeError:
Incompatible use of binary symbol `a` as a real variable in `a > 0`
```
The check is flakey though because a relational can contain binary symbols that are used as binary symbols:
```python
In [4]: p = Piecewise((1, a), (2, True))

In [5]: p
Out[5]: 
⎧1    for a  
⎨            
⎩2  otherwise

In [6]: a & (p > sqrt(2))
---------------------------------------------------------------------------
TypeError
Incompatible use of binary symbol `a` as a real variable in
`Piecewise((1, a), (2, True)) > sqrt(2)`
```
My suggested fix is:
```diff
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)
```
Then we can have:
```python
In [1]: a, b, c, d = symbols('a, b, c, d')

In [2]: p = Piecewise((1, a), (2, True))

In [3]: a & (p > sqrt(2))
Out[3]: 
    ⎧1    for a       
a ∧ ⎨             > √2
    ⎩2  otherwise     

In [4]: expr = Or(And(a,c), Eq(a,b))

In [5]: expr
Out[5]: (a ∧ c) ∨ a = b
```
I imagine that somewhere there is a test that depends on this code doing this strange replacement but I might be wrong.

From the core and logic tests there were a few that failed because they expected an error to be raised. Potentially those could be changed or otherwise the code to raise an error could be improved to handle those cases without also mishandling others. Really though this just shows why we need a separate `BooleanSymbol` type: `Symbol` should not be be a simultaneous subclass of both `Boolean` and `Expr` because these are incompatible and it just confuses everything.

The other test that failed was this one:
https://github.com/sympy/sympy/blob/221d773085642f7e30440ba6ffa122d5bfbb1042/sympy/logic/tests/test_boolalg.py#L307
I don't think that is a very important test precisely because it is just testing what happens when Symbol is mixed up between Expr and Boolean which is something that should have never been allowed in the first place.

My suggested fix is:
```diff
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)
diff --git a/sympy/logic/tests/test_boolalg.py b/sympy/logic/tests/test_boolalg.py
index 7b50f8ebd7..f3ec5604a6 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)
```
I am marking this as "easy to fix" for someone to apply the diff shown although there might also be some other test failures (I didn't run the whole test suite).

Separately we could consider improving the detection of erroneous mixing of symbols as Expr and Boolean but I don't think it is very important: time would be better spent adding a `BooleanSymbol` class and considering if we would ever be able to deprecate using Symbol as a Boolean.
You can use `Or(And(a, c), Equivalent(a, b))` for fix meanwhile.
Maybe `Equivalent` is semantically better than `Eq` for users.
Thanks for the quick response @oscarbenjamin ! Unfortunately I'm not familiar enough with the internals to help out myself.

@sylee957 - This `Equivalent()` and `Not(Equivalent())` stand-in is very helpful, much appreciated!
> 

Hi @paulcalcraft 

`a, b, c = symbols("a b c")` - You're initializing the symbols correctly.

`expr = Or(And(a,c), Eq(a,b))` - Here's where the error is.

When you're constructing the expression using `Or(And(a,c), Eq(a,b))`, you're not actually using Sympy's logical operators. In Sympy, the logical "AND" is represented by `And(...)`, the logical "OR" is represented by `Or(...)`, and the logical "EQUALS" is represented by `Eq(...)`.

However, the issue arises because the `Eq(a,b)` actually returns a boolean (either `True` or `False`) if `a` and `b` can be determined as equivalent or not. So if `a` and `b` are both symbols and cannot be evaluated, then `Eq(a,b)` simply represents the symbolic equation 

a=b.

Let's see how to correctly construct and evaluate the expression.

```
from sympy import *

a, b, c = symbols("a b c")

expr = Or(And(a, c), Eq(a, b))

# This will print the entire expression, not just "a & c".
print(expr)  # And(a, c) | Eq(a, b)

# Now let's evaluate it with a=True, b=True, c=False
print(expr.subs({a:True, b:True, c:False})) # True
```
Hi @ManuPer3z, as far as I can tell, the code you've provided is identical to my original post? It does not print what you've suggested. What version are you using? I've just tested again with the latest stable release (SymPy 1.12) and I still get:

```
a & c
False
```

Perhaps you are using an older version that didn't have this bug?

Using `Equivalent` as suggested by @sylee957 is working well. I haven't closed the issue myself because presumably the SymPy maintainers want to decide whether to correct it or flag it as a gotcha.
The issue should not be closed until the diff I showed is applied or something similar. There is a bug to be fixed.

Commit message: Update .mailmap

Patch to review:
diff --git a/.mailmap b/.mailmap
index 34c061d0b266..20c42ee993f7 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 27213a215b73..ac190ac50883 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)
diff --git a/sympy/logic/tests/test_boolalg.py b/sympy/logic/tests/test_boolalg.py
index 7b50f8ebd773..65fe4d14691e 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,8 @@ 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 x != And(a, c)


Code review comments:
diff_hunk: @@ -1345,3 +1341,8 @@ 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 x != And(a, c)
path: sympy/logic/tests/test_boolalg.py
text: @user1:
Test with `!=` is not ideal because many possible objects would pass the test. A better test could be:
```
assert isinstance(x, Or)
assert set(x.args) == {And(a, c), Eq(a, b)}
```

@author:
Thank you, I will update it now. I appreciate your input.