在 Z3 中编码 let 表达式

Question

以下代码对包含两个字段array-fld 和blist-fld 的“记录”进行编码。我已经为这些字段定义了更新函数，然后断言了一个应该为 true 的属性（但 z3 报告为 unknown）。这是Z3 4.0版本，运行z3 -smt2 -in：

(declare-datatypes ()
                   ((mystruct (mk-mystruct
                                 (array-fld (Array Int Int))
                                 (blist-fld (List Bool))))))
(define-fun array-fld-upd ((v (Array Int Int)) (obj mystruct)) mystruct
  (mk-mystruct v (blist-fld obj)))
(define-fun blist-fld-upd ((v (List Bool)) (obj mystruct)) mystruct
  (mk-mystruct (array-fld obj) v))

(push)
(assert
 (forall ((z0 mystruct))
         (exists ((array-val (Array Int Int)))
                 (and (= array-val (array-fld z0))
                      (= (select (array-fld
                                  (array-fld-upd (store array-val 2 4) z0)) 3)
                         (select (array-fld z0) 3))))))
(check-sat)

如果我通过替换方程式 array-val 绑定手动展开/消除存在，我得到

(pop)
(assert
 (forall ((z0 mystruct))
         (= (select (array-fld (array-fld-upd (store (array-fld z0) 2 4) z0)) 3)
            (select (array-fld z0) 3))))
(check-sat)

这很高兴解决为sat。

我想这里面有四个问题：

1. 有没有办法调用 z3 来解决第一个实例和第二个实例？
2. 我应该对我的记录/结构进行不同的编码吗？
3. 我是否应该以不同的方式编码我的 let 表达式（正是这些导致存在量化）？
4. 或者，我是否应该直接展开 let 表达式（我可以自己做，但如果有很多引用，它可能会导致大术语）。

Answer 1

从问题看来，您可以使用正确的 let 表达式。 那么Z3会更轻松：

(declare-datatypes ()
               ((mystruct (mk-mystruct
                             (array-fld (Array Int Int))
                             (blist-fld (List Bool))))))
(define-fun array-fld-upd ((v (Array Int Int)) (obj mystruct)) mystruct
  (mk-mystruct v (blist-fld obj)))
(define-fun blist-fld-upd ((v (List Bool)) (obj mystruct)) mystruct
  (mk-mystruct (array-fld obj) v))

(push)
(assert
 (forall ((z0 mystruct))
    (let ((array-val (array-fld z0)))
                  (= (select (array-fld
                              (array-fld-upd (store array-val 2 4) z0)) 3)
                     (select (array-fld z0) 3)))))
 (check-sat)