一起使用浮点数和实数时 z3 返回未知？

Question

由于我在同一个 .smt2 文件中使用浮点数和实数，我注意到这通常会导致结果“未知”。我在此处看到了这一点，但自这个答案以来已经过去了一段时间，我想询问我是否可能根本没有使用正确的设置（例如，我是否应该在 check-sat 行中传递策略作为参数？或者缩小设置逻辑范围？）

这是一个展示该行为的示例：

(set-logic ALL)
(set-option :produce-models true)
(set-info :smt-lib-version 2.6)

(set-info :status unknown)
(define-sort FPN () (_ FloatingPoint  8  24))

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)

(declare-fun x0 () FPN)
(declare-fun y0 () FPN)
(declare-fun z0 () FPN)

(declare-fun x1 () FPN)
(declare-fun y1 () FPN)
(declare-fun z1 () FPN)

(define-fun fun ( (x FPN) (y FPN) (z FPN) (arg0 Real) (arg1 Real) (arg2 Real)) FPN (fp.add RNE 
                                                                                           (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE arg0) x)
                                                                                                       (fp.mul RNE ((_ to_fp 8 24) RNE arg1) y))
                                                                                           (fp.mul RNE ((_ to_fp 8 24) RNE arg2) z)) )

(assert (fp.eq x0 ((_ to_fp 8 24) RNE 1)))
(assert (fp.eq y0 ((_ to_fp 8 24) RNE 0)))
(assert (fp.eq z0 ((_ to_fp 8 24) RNE 0)))

(assert (fp.eq x1 ((_ to_fp 8 24) RNE 0)))
(assert (fp.eq y1 ((_ to_fp 8 24) RNE 0)))
(assert (fp.eq z1 ((_ to_fp 8 24) RNE 0)))

(assert
  (fp.gt (fun x0 y0 z0 a b c) (fun x1 y1 z1 a b c))
)


(check-sat)
(get-info :reason-unknown)
(get-model)
(exit)

非常感谢非常适合任何回应！

Answer 1

恐怕从那时起并没有太大变化。像这样混合浮点数和实数会给 SMT 求解器带来非常棘手的问题。您可以在 z3 问题跟踪器 (https://github.com/Z3Prover/z3/issues ）提醒开发人员，可惜我怀疑很快就会有很大的改进。

请注意，尝试其他求解器总是一个好主意。 CVC5 和 MathSAT 都支持浮点数和实数。不幸的是，当我在你的问题上调用 mathsat 时，它因语法错误而出错（我认为这是 mathsat 本身的错误），但 CVC5 确实找到了以下模型：

(
(define-fun a () Real (/ 1 4294967296))
(define-fun b () Real (- 1.0))
(define-fun c () Real (- 1.0))
(define-fun x0 () (_ FloatingPoint 8 24) (fp #b0 #b01111111 #b00000000000000000000000))
(define-fun y0 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
(define-fun z0 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
(define-fun x1 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
(define-fun y1 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
(define-fun z1 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
)

我还没有检查该模型是否实际上有效，但它是好消息是 CVC5 可以开箱即用（而且速度也很快）处理这个问题。