Z3 中的可判定 sqrt 函数
Decidable sqrt function in Z3
自 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)
此 returns sat 与 Z3 4.4.1，但 unknown 与 master。
如果我将问题定义更改为使用 Nikolaj 在 this question 中定义的 is_sqrt，则 Z3 master 将 return sat。使用is_sqrt的方法表明可以通过引入辅助变量将所有实根推入QF_NRA，所以我认为Z3应该能够解决所有涉及实数根的问题。
假设模型的其余部分在 QF_NRA 中，我如何定义实数中的平方根函数，从而得出可判定的理论？
(assert (= y (^ x 0.5))) 和 (assert (and (= x (* y y)) (> y 0.0))) 之间存在细微差别。不同之处在于要求 Z3（和 SMT-LIB）中的所有功能都是完整的。这意味着，例如 。鉴于 ^ 在 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（伪代码），那么它的优点是 return unsat。 To return unsat 这个例子更符合我的用例。
自 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)
此 returns sat 与 Z3 4.4.1，但 unknown 与 master。
如果我将问题定义更改为使用 Nikolaj 在 this question 中定义的 is_sqrt，则 Z3 master 将 return sat。使用is_sqrt的方法表明可以通过引入辅助变量将所有实根推入QF_NRA，所以我认为Z3应该能够解决所有涉及实数根的问题。
假设模型的其余部分在 QF_NRA 中，我如何定义实数中的平方根函数，从而得出可判定的理论？
(assert (= y (^ x 0.5))) 和 (assert (and (= x (* y y)) (> y 0.0))) 之间存在细微差别。不同之处在于要求 Z3（和 SMT-LIB）中的所有功能都是完整的。这意味着，例如 ^ 在 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（伪代码），那么它的优点是 return unsat。 To return unsat 这个例子更符合我的用例。