Say I have a z3 expression:
c = z3.Int("x")
Expr = (-c) / 2
Is it possible to use Z3 to find any C so that the expression evaluates to an integer?
For example, if c==1, this whole equation should evaluates to -0.5 and thus not an integer.
I've tried to model the problem using reminder==0 approach
>>> from z3 import *
>>> c = Int("c")
>>> s = Solver()
>>> s.add(((-c) %2)==0)
>>> s.check()
sat
Which is obviously incorrect. Changing to c = Real("c") gives an exception:
>>> c = Real("c")
>>> s = Solver()
>>> s.add(((-c) %2)==0)
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "/usr/local/lib/python3.9/site-packages/z3/z3.py", line 2539, in __mod__
_z3_assert(a.is_int(), "Z3 integer expression expected")
File "/usr/local/lib/python3.9/site-packages/z3/z3.py", line 112, in _z3_assert
raise Z3Exception(msg)
z3.z3types.Z3Exception: Z3 integer expression expected
% over integers will be evaluated as integer remainder; so what you proposed actually works just fine:
from z3 import *
c = Int("c")
s = Solver()
s.add(((-c) %2)==0)
print(s.check())
print(s.model())
This prints:
sat
[c = 2]
and indeed, the model says c can be the integer 2, and -c%2 will be 0 as one would expect.
If you also add the assertion that c is 1:
from z3 import *
c = Int("c")
s = Solver()
s.add(((-c) %2)==0)
s.add(c == 1)
print(s.check())
then you get:
unsat
as expected. So, this all works just as required. Perhaps you're trying to ask something else?