Python And Z3: Integers And Floating, How To Manage Them In The Correct Way?

need help with Z3 and Python...it looks I'm too dumb for this. My code: from z3 import * num1 = Int('num1') num2 = Int('num2') num3 = Int('num3') s = Solver() s.add( 2 * num1 - n

Solution 1:

You're absolutely correct that Python bindings to Z3 suffer from weakly typing. This comes back to bite quite often, when least expected.

In these cases, sexpr() method is your friend. Add print s.sexpr() to the end of your program. It prints the following:

(declare-funnum3()Int)
(declare-funnum2()Int)
(declare-funnum1()Int)
(assert (= (+ (- (* 2 num1) num2) (* 0 num3)) 5412))
(assert (= (+ (* 2 num1) (* 3 num2) (* 4 num3)) 28312))

And you can see your 0.5 became 0! Which is totally not what you wanted. Welcome to the world of "I'll coerce to make things fit behind your back."

To solve this, you really need to be very clear on conversions. Z3 supports floating-point and also real numbers. (i.e., with infinite precision.) And arithmetic doesn't mix-and-match in the SMTLib land, so you have to be very careful on how you construct the proper constants.

Solution 2:

Int declares (mathematical) integers, nothing else, so the model value will always be an integer. The expression 0.5 * num3 is automatically converted to integers (there's an option to disable these automatic conversions and instead throw an error). If you need fractional values, use Real instead of Int.