Formulas are encoded multiple times when documentation says they should not be

[vgklein]

In the documentation of

class pysat.formula.Formula(*args, **kwargs) (see here),

the first example is

from pysat.formula import *

>>> x1, x2 = Atom('x'), Atom('x')
>>> id(x1) == id(x2)
True  # x1 and x2 refer to the same atom
>>> id(x1 & Atom('y')) == id(Atom('y') & x2)
True  # it holds if constructing complex formulas with them as subformulas

Contrary to the documentation, the last statement (id(x1 & Atom('y')) == id(Atom('y') & x2)) returns False and not True.
This could simply be an error in the documentation but could also point to a flaw in the implementation.

Versions:
python-sat 1.8.dev13
Python 3.10.3
Windows 11

[alexeyignatiev]

Thanks for reporting, @vgklein! Unfortunately, it seems like a bug because the formula objects are supposed to be the same and the documentation reflects the original expectations. In fact, it worked when I wrote it. I will try to investigate when I get time (this is a huge problem these days).

[vgklein]

thank you for your response and thank you for pysat in the first place.

…

________________________________ Von: Alexey Ignatiev ***@***.***> Gesendet: Montag, 30. September 2024 05:39 An: pysathq/pysat ***@***.***> Cc: Volker Klein ***@***.***>; Mention ***@***.***> Betreff: Re: [pysathq/pysat] Formulas are encoded multiple times when documentation says they should not be (Issue #179) Thanks for reporting, @vgklein<https://github.com/vgklein>! Unfortunately, it seems like a bug because the formula objects are supposed to be the same and the documentation reflects the original expectations. In fact, it worked when I wrote it. I will try to investigate when I get time (this is a huge problem these days). — Reply to this email directly, view it on GitHub<#179 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ATKKNKQ4BQO24HTTNLHS7T3ZZDBY7AVCNFSM6AAAAABOWGEJ56VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGOBRHE2DCOJSGU>. You are receiving this because you were mentioned.Message ID: ***@***.***>