z3 - z3 是否支持其输入约束的有理算术？

Question

事实上，SMT-LIB 标准是否具有合理的(不仅仅是真实的)排序？按照它的 website ，它没有。
如果 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 有自己的合理库，例如，在使用 Simplex 算法的改编解决 QF_LRA 约束时，它会使用它。在相关说明中，是否有支持输入级别有理数的 SMT 求解器？

Answer 1

我确信可以按照 Nikolaj 的建议使用两个整数来定义 Rational 排序——我很想看到这一点。仅使用 Real 排序可能更容易，并且任何时候您想要一个有理数，请断言它等于两个 Int 的比率。例如:

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