CODEWITHSUNDEEP
pythonsympy
Ariel
Ariel

Reputation: 376

Simultaneous replacement of SymPy logic function

I came across a problem substituting variables in logical formulas in Sympy. Here's a minimal example - 

from sympy import *
x, y = symbols('x y')
Nand(x, y).subs({x: Nand(x, y)}, simultaneous=True)

This fails both in my local interperter, and in the live shell on SymPy Docs, with the error message 

Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/base/data/home/apps/s~sympy-live-hrd/49.400254913747479351/sympy/sympy/core/basic.py", line 889, in subs
    d = Dummy(commutative=new.is_commutative)
  File "/base/data/home/apps/s~sympy-live-hrd/49.400254913747479351/sympy/sympy/core/symbol.py", line 205, in __new__
    cls._sanitize(assumptions, cls)
  File "/base/data/home/apps/s~sympy-live-hrd/49.400254913747479351/sympy/sympy/core/symbol.py", line 65, in _sanitize
    '%scommutativity must be True or False.' % whose)
ValueError: Dummy commutativity must be True or False.

Other formulations I've tried, like replacing "Nand"s with "And", don't fail. Setting simultaneous=False also doesn't fail, but will not give the desired result if I want to replace y at the same time (see this question for details why).

Is this a bug in SymPy, or am misunderstanding something?

Upvotes: 2

Views: 165

Answers (1)

user6655984
user6655984

Reputation:

This is a bug in SymPy. Class Not does not have is_commutative property set, and does not inherit it either. As a result, Nand(x, y) (which is Not(And(x, y)) has "None" for "commutative" assumption, and this is not acceptable for Dummy creation method, which attempts to create a dummy symbol with the same assumptions. This problem does not occur for And, because And inherits is_commutative=True from LatticeOp class.

The way to fix this in SymPy seems to be to add is_commutative=True to class Not.

Workarounds on user side include: using Or(Not(x), Not(y)) instead of Nand(x, y)

Nand(x, y).subs({x: Or(Not(x), Not(y))}, simultaneous=True)

(this returns ~(y & (~x | ~y)))

and fixing the classes on your own:

class Not(Not):
    is_commutative = True

class Nand(Nand):
    @classmethod
    def eval(cls, *args):
        return Not(And(*args))      

Nand(x, y).subs({x: Nand(x, y)}, simultaneous=True)

(returns ~(y & ~(x & y)).)

Upvotes: 1

Related Questions