Python и Z3: целые и плавающие, как правильно ими управлять?

Question

нужна помощь с Z3 и Python ... похоже, я слишком туп для этого. Мой код:

from z3 import *

num1 = Int('num1')
num2 = Int('num2')
num3 = Int('num3')

s = Solver()
s.add( 2 * num1 - num2 + 0.5 * num3 == 5412.0)
s.add( 2 * num1 + 3 * num2 + 4 * num3 == 28312.0)

Результат следующий:

[num3 = 1, num1 = 5568, num2 = 5724]

Что не совсем правильно: первое выражение на самом деле возвращает 5412.5, а не 5412.0. Я предполагаю, что это связано со смешанным использованием «Int» с некоторыми «точечными числами» (0.5). На самом деле мне нужно оставить «numX» как «Int», так как они являются целыми числами (это ограничение). Думаю, мне не хватает, как справиться с этой смешанной ситуацией. Кто-нибудь может мне помочь?

Спасибо,

Отредактировано

Благодаря ответу "псевдоним" я получил правильное направление:

добавив

cc1 = RealVal(0.5)

и затем используя эту константу в выражении, я получил правильный результат.

Спасибо всем!

Answer 1

Вы абсолютно правы, что привязки Python к Z3 страдают от слабой типизации. Это возвращается к укусу довольно часто, когда меньше всего ожидается.

В этих случаях метод sexpr() - ваш друг. Добавьте print s.sexpr() в конец вашей программы. Он печатает следующее:

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

И вы можете видеть, что ваш 0.5 стал 0! Что совсем не то, что вы хотели. Добро пожаловать в мир «Я буду принуждать, чтобы все было у вас за спиной».

Чтобы решить эту проблему, вам действительно нужно быть очень чёткими в конверсиях. Z3 поддерживает с плавающей точкой, а также действительные числа. (т. е. с бесконечной точностью.) Арифметика c не смешивается и не совпадает в земле SMTLib, поэтому вы должны быть очень осторожны при создании правильных констант.

Answer 2

Int объявляет (математические) целые числа, больше ничего, поэтому значение модели всегда будет целым числом. Выражение 0.5 * num3 автоматически преобразуется в целые числа (есть возможность отключить эти автоматические c преобразования и вместо этого выдать ошибку). Если вам нужны дробные значения, используйте Real вместо Int.