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