简化模型中的函数解释

Question

在SMT中：检查函数的唯一性和整体性 我给出了一个函数公理化，并要求Z3提供一个模型。 但是，由于解决带有量词的内容通常是不可判定的，因此 Z3 超时。

下面是一个修改版本，其中"int"大小写被建模为单个值：

(declare-datatypes () ((ABC int error none)))
(declare-fun f (ABC ABC) ABC)
(assert (forall ((x ABC)) (=> (or (= x int) (= x error) (= x none)) (= (f none x) none))))
(assert (forall ((x ABC)) (=> (or (= x int) (= x error) (= x none)) (= (f x none) none))))
(assert (forall ((x ABC)) (=> (or (= x int) (= x error)) (= (f error x) error))))
(assert (forall ((x ABC)) (=> (or (= x int) (= x error)) (= (f x error) error))))
(assert (forall ((x ABC) (y ABC)) (=> (and (= x int) (= y int)) (= (f x y) int))))
(check-sat)
(get-model)

因为现在有有限种情况，Z3 很快就给出了答案：

sat
(model
  (define-fun k!26 ((x!0 ABC)) ABC
    (ite (= x!0 error) error
    (ite (= x!0 int) int
      none)))
  (define-fun f!28 ((x!0 ABC) (x!1 ABC)) ABC
    (ite (and (= x!0 error) (= x!1 int)) error
    (ite (and (= x!0 int) (= x!1 error)) error
    (ite (and (= x!0 error) (= x!1 error)) error
    (ite (and (= x!0 int) (= x!1 int)) int
      none)))))
  (define-fun k!27 ((x!0 ABC)) ABC
    (ite (= x!0 error) error
    (ite (= x!0 int) int
      none)))
  (define-fun f ((x!0 ABC) (x!1 ABC)) ABC
    (f!28 (k!27 x!0) (k!26 x!1)))
)

k!26 和 k!27 实际上都只返回它们的输入（通过检查所有三种情况很容易看到这一点）。 是否有可能通过自动消除这两个功能来简化模型？

理想情况下，我希望有类似以下内容的东西，尽管我认为这可能是不可能的：

(define-fun f ((x!0 ABC) (x!1 ABC)) ABC
  (ite (or (= x!0 none) (= x!1 none)) none
  (ite (or (= x!0 error) (= x!1 error)) error
    int)))

我使用的是 Z3Py，但欢迎通用的 Z3 特定和 Z3Py 特定的答案。

Answer 1

我认为你没有太多可以指导 Z3 在这里提供一个"更简单"的答案;因为生成的模型取决于证明是如何完成的，即使是对问题的简单更改也可能产生不可预测的结果。特别是，您获得的模型可能会随着下一个版本的 Z3 而更改。

话虽如此，一个常见的技巧是在模型中eval项。由于您当前的问题仅涉及有限域，因此您可以枚举它。如果在脚本末尾添加以下行：

(eval (f int   int))
(eval (f int   error))
(eval (f int   none))
(eval (f error int))
(eval (f error error))
(eval (f error none))
(eval (f none  int))
(eval (f none  error))
(eval (f none  none))

然后 Z3 将打印：

int
error
none
error
error
none
none
none
none

也许您可以使用该输出自己构建一个"更简单"的模型。当然，这仅在域有限的情况下才有效;但是，您可以使用相同的技巧来评估输入域的"有趣"部分，具体取决于您的问题。