Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Python: Improve BoolRef addition #7045

Merged
merged 1 commit into from
Dec 5, 2023

Conversation

tyilo
Copy link
Contributor

@tyilo tyilo commented Dec 5, 2023

Currently adding an ArithRef and a BoolRef works, but not the other way around:

>>> import z3
>>> a = z3.Int("a")
>>> b = z3.Bool("b")
>>> a + b
a + If(b, 1, 0)
>>> b + a
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1575, in __add__
    return If(self, 1, 0) + If(other, 1, 0)
                            ^^^^^^^^^^^^^^^
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1415, in If
    a = s.cast(a)
        ^^^^^^^^^
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1555, in cast
    _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 107, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value

Furthermore adding a python int to a BoolRef doesn't work at all:

>>> import z3
>>> b = z3.Bool("b")
>>> 1 + b
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: unsupported operand type(s) for +: 'int' and 'BoolRef'
>>> b + 1
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1575, in __add__
    return If(self, 1, 0) + If(other, 1, 0)
                            ^^^^^^^^^^^^^^^
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1415, in If
    a = s.cast(a)
        ^^^^^^^^^
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1553, in cast
    _z3_assert(is_expr(val), msg % (val, type(val)))
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 107, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: True, False or Z3 Boolean expression expected. Received 1 of type <class 'int'>

This fixes both of these issues.

@NikolajBjorner NikolajBjorner merged commit a9513c1 into Z3Prover:master Dec 5, 2023
1 of 15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants