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

Question

На самом деле, стандарт 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, который поддерживает рациональные значения на входном уровне?

Answer 1

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

(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))