z3 是否支持其输入约束的有理算术? [英] Does z3 support rational arithmetic for its input constraints?

问题描述

事实上，SMT-LIB 标准是否具有合理的(不仅仅是真实的)排序?通过其网站，它没有.
如果 x 是有理数并且我们有一个约束 x^2 = 2，那么我们应该得到不可满足".我能得到的最接近该约束的编码如下:

In fact, does the SMT-LIB standard have a rational (not just real) sort? Going by its website, it does not.
If x is a rational and we have a constraint x^2 = 2, then we should get back ``unsatisfiable''. The closest I could get to encoding that constraint is the following:

;;(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 求解器?

for which z3 returns a solution, as there is a solution (irrational) in the reals. I do understand that z3 has its own rational library, which it uses, for instance, when solving QF_LRA constraints using an adaptation of the Simplex algorithm. On a related note, is there an SMT solver that supports rationals at the input level?

推荐答案

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

I'm sure it's possible to define a Rational sort using two integers as suggested by Nikolaj -- I would be interested to see that. It might be easier to just use the Real sort, and any time you want a rational, assert that it's equal to the ratio of two Ints. For example:

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

这篇关于z3 是否支持其输入约束的有理算术?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！