Added xor operation

[zvasicek]

Minor modification that adds support for XOR operator available in Python.

[johnyf]

Not sure about this change to use the infix operator ^ as XOR, because /\ is conjunction in TLA+ syntax (and typesets as ∧), which could lead to ambiguity. In the methods BDD.apply() and BDD.add_expr() the TLA+ syntax for XOR is # (i.e., \neq which typesets as "≠").

[zvasicek]

I don't understand, how is the expression c=a^b in Python related to TLA+? The lack of an XOR operator in Python means that the library cannot be used to create logical nets specified by an expression.

[johnyf]

Currently the ways to use XOR are via BDD.apply() and BDD.add_expr(), for example:

import dd.autoref as _bdd

bdd = _bdd.BDD()
bdd.declare('x', 'y', 'z')
u = bdd.add_expr(r'x /\ y')
v = bdd.add_expr(r'x \/ z')

# current alternatives for XOR
w = bdd.add_expr(f'{u} # {v}')
w = bdd.add_expr(f'{u} ^ {v}')
w = bdd.apply('#', u, v)
w = bdd.apply('xor', u, v)
w = bdd.apply('^', u, v)

The intention in add_expr() is to use either the operators /\, \/, #, or the operators &, |, ^ (or &, |, #). Using both /\ and ^ could lead to confusion, due to how similar the shapes are, so bdd.add_expr(r'x /\ y ^ z') is not intended. The Python operator ^ is defined by the method __xor__(), which explicitly mentions "xor", but this is implicit when using the operator. In principle it could be implemented as conjunction, to resemble the /\, which can cause ambiguity.

On the other hand, since &, |, ^ form a group of operators, and &, | (and ~) are already implemented in Python, adding ^ would make more complete this group of operators. Also, since the symbol ^ already means XOR in BDD.add_expr() and BDD.apply(), implementing it the same way in Python is consistent with existing usage. I am considering merging this change.

In TLA+ the operator ^ is definable (/\ is builtin syntax), and defined in the module ProtoReals as exponentiation, and instantiated in the module Naturals.

[johnyf]

Rebased and merged. Thank you for the addition.