由于disabling unsound simplification of root objects，Z3 现在将在这个涉及平方根的简单模型上失败：
(define-fun sqrt ((x Real)) Real (^ x 0.5))
(declare-fun y () Real)
(declare-fun x () Real)
(assert (= y (sqrt x)))
(check-sat)
这会在 Z3 4.4.1 中返回 sat，但在主版本中返回 unknown。
如果我将问题定义更改为使用 Nikolaj 在this question 中定义的is_sqrt，则 Z3 master 将返回sat。使用is_sqrt的方法表明通过引入辅助变量可以将所有实数根推入QF_NRA，所以我认为Z3应该能够解决所有涉及实数根的问题。
假设模型的其余部分在QF_NRA 中，我如何在实数中定义一个平方根函数以产生可判定的理论？
【问题讨论】：
标签： z3
(assert (= y (^ x 0.5))) 和 (assert (and (= x (* y y)) (> y 0.0))) 之间存在细微差别。不同之处在于要求 Z3（和 SMT-LIB）中的所有功能都是完整的。例如，这意味着y=1/x, x=0 is considered satisfiable。鉴于^ 是 Z3 中的总数，(assert (and (= y (^ x 0.5)) (< x 0.0))) 被认为是可满足的。我们无法将(= y (^ x 0.5)) 转换为(and (= x (* y y)) (> y 0.0))，因为如果x < 0 则认为前者是可满足的，而后者是不可满足的。同样，在 SMT-LIB 中定义的任何 sqrt 函数也将是总计的，因此我们不能通过任何其他方式定义 sqrt 函数，使得 (assert (= y (sqrt x))) 等效于 (assert (and (= x (* y y)) (> y 0.0)))。除了以上关于y = sqrt(x), x < 0（伪代码）是否被认为是可满足的区别之外，(assert (and (= x (* y y)) (> y 0.0)))也是可判定的（在QF_NRA中），而(assert (= y (^ x 0.5)))不是。
我的解决方案是不使用平方根的 Z3 或 SMT-LIB 函数定义。相反，我将使用(assert (and (= x (* y y)) (> y 0.0))) 形式的语句来表示y 是x 的平方根。此类断言在 QF_NRA 内，因此以这种方式构建的模型将是可判定的。此外，如果通过语句 (assert (and (= x (* y y)) (> y 0.0))) 和 (assert (< x 0.0)) 在 SMT-LIB 中表示 y = sqrt(x), x < 0（伪代码），它的优点是返回 unsat。在此示例中返回 unsat 更符合我的用例。
【讨论】：