Реализация функций пола и потолка в Z3

[Ваша кодировка не загружается в z3, она дает синтаксическую ошибку даже после удаления '..', так как ваш вызов Implies требует дополнительного аргумента. Но я проигнорирую все это.]

Короткий ответ: вы не можете делать такие вещи в SMT-Solver. Если бы вы могли, то вы могли бы решать произвольные диофантовы уравнения. Просто приведите его к действительным числам, решите его (есть процедура принятия решения для вещественных чисел), а затем добавьте дополнительное ограничение, что результат является целым числом, сказав Floor(solution) = solution. Итак, по этому аргументу вы можете видеть, что моделирование таких функций будет за пределами возможностей решателя SMT.

Подробности см. в этом ответе: QF_UFNRA

Сказав это, это не означает, что вы не можете закодировать это в Z3. Это просто означает, что это будет более или менее бесполезно. Вот как бы я поступил:

from z3 import *

s = Solver()

Floor = Function('Floor',RealSort(),IntSort())

r = Real('R')
f = Int('f')
s.add(ForAll([r, f], Implies(And(f <= r, r < f+1), Floor(r) == f)))

Теперь, если я сделаю это:

s.add(Not(Floor(0.5) == 0))
print(s.check())

вы получите unsat, что правильно. Если вы сделаете это вместо этого:

s.add(Not(Floor(0.5) == 1))
print(s.check())

вы увидите, что z3 просто зацикливается навсегда. Чтобы сделать это полезным, вы также хотите, чтобы работало следующее:

test = Real('test')
s.add(test == 2.4)
result = Int('result')
s.add(Floor(test) == result)
print(s.check())

но опять же, вы увидите, что z3 просто зацикливается навсегда.

Итак, итог: Да, моделировать такие конструкции можно, и z3 правильно ответит на самые простые запросы. Но с чем-нибудь интересным он просто зациклится навсегда. (По сути, всякий раз, когда вы ожидаете sat и большинство сценариев unsat, если только они не могут быть свернуты константами, я ожидаю, что z3 просто зациклится.) И для этого есть очень веская причина, как я уже упоминал: такие теории просто неразрешимы и выходят далеко за пределы того, что может сделать решатель SMT.

Если вы заинтересованы в моделировании таких функций, лучше всего использовать более традиционные средства доказательства теорем, такие как Isabelle, Coq, ACL2, HOL, HOL-Light и другие. Они гораздо больше подходят для работы над такого рода проблемами. А также прочтите Получить дробную часть реального в QF_UFNRA, так как он касается некоторых других деталей того, как вы можете моделировать такие функции, используя нелинейную вещественную арифметику.