事实上，SMT-LIB标准是否有理性的（不仅仅是真实的）排序？按其website http://smtlib.cs.uiowa.edu/theories.shtml， 它不是。
如果 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 求解器支持输入级别的有理数？
我确信可以按照 Nikolaj 的建议使用两个整数来定义有理排序——我对此很感兴趣。使用实数排序可能会更容易，并且任何时候您想要有理数，就断言它等于两个整数的比率。例如：
(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))
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
