4

事实上，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 有自己的有理库，例如，在使用 Simplex 算法的改编解决 QF_LRA 约束时，它会使用它。在相关说明中，是否有支持输入级别有理数的 SMT 求解器？

4

1 回答 1

3

我确信可以按照 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))
于 2016-03-22T14:59:31.453 回答