Здесь есть несколько проблем, но фундаментальная проблема заключается в том, что ваша аксиоматизация недостаточно ограничивает значение mod / quot значений, чтобы получить то, что, по вашему мнению, должно быть. В частности, существует бесконечное количество способов удовлетворить ваши предположения, и z3 просто выбирает один. Позвольте мне уточнить.
Я собираюсь исключить Java кодирование здесь, так как оно не добавляет ничего ценного. Но прямо кодируйте то, что вы написали в SMTLib. Пока код написан на SMTLib, заключение относится и к вашей программе.
В нотации SMTLib это то, что вы заявляете. (Вычеркнуто из вашего вывода, после добавления факта, что remainder совпадает с modxk и упрощен для удобства чтения):
(declare-fun mod (Real Real) Real)
(declare-fun quot (Real Real) Real)
(define-fun X () Real (+ 6.0 (/ 1.0 10.0)))
(define-fun k () Real 6.0)
; Implies(k != 0, 0 <= mod(X,k))
(assert (=> (distinct k 0.0) (<= 0 (mod X k))))
; Implies(k > 0, mod(X,k) < k)
(assert (=> (> k 0.0) (< (mod X k) k)))
; Implies(k < 0, mod(X,k) < -k)
(assert (=> (< k 0.0) (< (mod X k) (- 0 k))))
; Implies(k != 0, k*quot(X,k) + mod(X,k) == X))
(assert (=> (distinct k 0.0) (= X (+ (mod X k) (* k (quot X k))))))
Это код, который вы будете морально генерировать из вашего Программа Java, как только вы разберетесь со всеми глюками и, возможно, дадите имена X и k для удобства чтения.
Давайте посмотрим, что выдаст z3 для этой программы. Добавьте в конце следующие строки:
(check-sat)
(get-value ((mod X k)))
(get-value ((quot X k)))
Запуск z3 в этой окончательной программе SMTLib дает:
sat
(((mod X k) (/ 11.0 2.0)))
(((quot X k) (/ 1.0 10.0)))
В более привычной записи это означает, что mod равно 5.5 и quot - это 0.1.
Вы, конечно, будете протестовать, так как вы хотели, чтобы mod было 0.1! Действительно, если вы go пройдете через все введенные вами утверждения, вы увидите, что эти значения удовлетворяют всем им. Давайте go по ним один за другим:
Implies(k != 0, 0 <= mod(X,k)) Да, у нас есть k=6, и 0 <= 5.5 имеет место. Implies(k > 0, mod(X,k) < k) Да, мы есть k=6 и 5.5 < 6 содержит Implies(k < 0, mod(X,k) < -k) Поскольку у нас есть k=6, это утверждение тривиально верно. Implies(k != 0, k*quot(X,k) + mod(X,k) == X). У нас есть k=6, и последующее говорит, что 6 * 0.1 + 5.5 должно быть 6.1, и это действительно правильно.
Итак, z3 нашел значения, которые удовлетворяют вашим ограничениям, и вот что решатель SMT предназначен для этого.
Чтобы обозначить точку, добавьте следующее ограничение в программу и запустите ее снова:
(assert (distinct (mod X k) 5.5))
Теперь z3 говорит:
sat
(((mod X k) 5.0))
(((quot X k) (/ 11.0 60.0)))
Что мы сделали, так это сказали z3, что мы хотим, чтобы mod X k было чем-то отличным от 5.5. И он сказал: «Хорошо, я сделаю это 5 и установлю quot X k равным 11/60, и все ваши аксиомы снова будут удовлетворены. Мы можем продолжать играть в эту игру вечно, так как момент размышления показывает, что существует бесконечное количество значений, которые удовлетворяют вашим ограничениям.
Здесь важно отметить, что нет никаких утверждений, что это только значения, которые удовлетворяют вашим ограничениям. Действительно, вы ожидали, что z3 выберет 0.1 для quot и 1 для mod, удовлетворяя уравнению 6 * 1 + 0.1 = 6.1. Но в вашей аксиоматизации нет ничего, что требовало бы выбора этих значений. На этом этапе вам нужно спросить себя, как (если возможно!) Вы можете добавить больше аксиом о mod и quot для действительных чисел, чтобы решение было уникальным. Я бы порекомендовал использовать бумагу и карандаш, чтобы записать, какие должны быть ваши аксиомы, чтобы значения были однозначно определены. (Между прочим, я не говорю, что это выполнимо. Я не уверен, действительно ли quot / mod имеет большой смысл для реалов.)
Если вы действительно можете придумать такой уникальный Аксиоматизация, затем попробуйте с z3, чтобы решить эту проблему для вас. Если вы не имеете в виду уникальную аксиоматизацию, z3 всегда будет выбирать некоторое назначение для переменных, которые удовлетворяют тому, что вы бросаете в нее, что вряд ли будет соответствовать вашим ожиданиям.
В обход целые числа
Одним из решений, которое я могу придумать, является ограничение значения quot целым числом. То есть, сделайте его функцией со следующей сигнатурой:
(declare-fun quot (Real Real) Int)
Если вы попробуете эту аксиоматизацию вместо этого, вы обнаружите, что z3 теперь производит:
sat
(((mod X k) (/ 1.0 10.0)))
(((quot X k) 1))
, что, вероятно, ты имел в виду. Обратите внимание, что когда вы смешиваете целые и действительные числа, как это, вы можете создавать ограничения, которые слишком сложны для решения SMT-решателя. (В данном конкретном случае это работает, потому что все, что у вас есть, это константы. ) Но мы можем обсудить последствия этого, если вы столкнетесь с проблемами.