简化模型中的函数解释答案

【问题标题】：Simplify function interpretation in model简化模型中的函数解释
【发布时间】：2016-05-28 17:37:35
【问题描述】：

在SMT: check uniqueness and totality of function 中，我给出了一个函数公理化，并要求 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 特定的一般答案。

【问题讨论】：

标签： z3 z3py

【解决方案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

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

【讨论】：