Поддерживает ли z3 рациональную арифметику для входных ограничений?

В самом деле, есть ли в стандарте SMT-LIB рациональная (а не только реальная) сортировка? Судя по его веб-сайту, это не так.
Если x — рациональное число, и мы есть ограничение x^2 = 2, тогда мы должны вернуться к ``неудовлетворительному''. Самое близкое, что я мог бы получить для кодирования этого ограничения, это следующее:

;;(set-logic QF_NRA) ;; intentionally commented out  
(declare-const x Real)  
(assert (= (* x x) 2.0))  
(check-sat)  
(get-model)

для которого z3 возвращает решение, так как есть решение (иррациональное) в вещественных числах. Я понимаю, что у z3 есть своя рациональная библиотека, которую он использует, например, при решении ограничений QF_LRA с помощью адаптации алгоритма Simplex. Кстати, есть ли решатель SMT, который поддерживает рациональные числа на входном уровне?


z3 smt cvc4
person user1779685    schedule 29.06.2015    source источник
comment
SMT-LIB не имеет рациональных типов. Вы можете эмулировать рациональные числа, используя два целых числа.   -  person Nikolaj Bjorner    schedule 29.06.2015
comment
Спасибо за ответ.   -  person user1779685    schedule 29.06.2015

Ответы (1)


arrow_upward
2
arrow_downward

Я уверен, что можно определить сортировку Rational с использованием двух целых чисел, как предложил Николай, - мне было бы интересно это увидеть. Может быть проще просто использовать сортировку Real, и каждый раз, когда вам нужно рациональное значение, утверждайте, что оно равно отношению двух целых чисел. Например:

(set-option :pp.decimal true)
(declare-const x Real)
(declare-const p Int)
(declare-const q Int)
(assert (> q 0))
(assert (= x (/ p q)))
(assert (= x 0.5))
(check-sat)
(get-value (x p q))

Это быстро возвращается с

sat
((x 0.5)
 (p 1)
 (q 2))
person Douglas B. Staple    schedule 22.03.2016
comment
Пробуя это на 4.8.7, я обнаружил, что мне нужно (assert (= (* x q) p), чтобы это было удовлетворительно. - person Jay Kominek; 20.12.2019