0
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add((2 * y ** 3 + x * y + 5 * x) % 11223344 == 33445566)
s.add((2 * y + x ** 3) % 11223344 == 33445566)

Upon running s.check(), z3 throws an error z3.z3types.Z3Exception: Z3 integer expression expected. I do not understand why as everything I used is an integer. I also tried BitVector however that gave a different error: unsupported operand type(s) for ** or pow(): 'BitVecRef' and 'BitRefValue'

I'm sorry that I could not provide the actual values here as it is sensitive data - but I simply replaced integer values and kept everything else the same.

alias
  • 28,120
  • 2
  • 23
  • 40
Billy Cao
  • 335
  • 4
  • 15

1 Answers1

2

In z3, power operator always returns a Real value. Which makes your arithmetic use mixed-types, and z3 rightfully complains.

There's a very recent discussion of this on stack-overflow, see here: Why does the type change to Real in z3 python?

You can avoid the issue by casting to integer explicitly:

from z3 import *

x = Int('x')
y = Int('y')
s = Solver()
s.add((2 * ToInt(y ** 3) + x * y + 5 * x) % 11223344 == 33445566)
s.add((2 * y + ToInt(x ** 3)) % 11223344 == 33445566)

The above goes through without any complaints.

However, keep in mind the caveats that come with using the power-operator in the linked answer. If you're always raising to the third power, I'd recommend simply writing x * x * x (or define a function that does that for you). Your problem will still be non-linear, but at least you'll avoid the issues due to the further complexity of exponentiation.

alias
  • 28,120
  • 2
  • 23
  • 40
  • Thanks! I expanded it into x * x * x, however now it is giving me unsat model(), but since I generated this equation, i know for sure there exists an answer. Do you know any possible cause for it? – Billy Cao Jun 10 '22 at 01:37
  • You essentially have `expression % modulo == number`, where `number > modulo`. Which is not satisfiable regardless of what the numbers involved are. (Any number reduced modulo `K` will be a number less than `K`.) – alias Jun 10 '22 at 03:58
  • Oh the integers are abitary. The real equation have the modulo smaller than the number. I can solve this using wolfram mathematical but I would like to learn if z3 can solve it too since its easier to use for me – Billy Cao Jun 10 '22 at 04:30
  • So, you're asking why something is `unsat` without telling us what that thing is? I'm confused as to what your real question is. – alias Jun 10 '22 at 04:36