record - 在 Z3 中编码 let 表达式

Question

以下代码使用两个字段 array-fld 和 blist-fld 对“记录”进行编码。我已经为这些字段定义了更新函数，然后断言了一个应该为 true 的属性(但 z3 将其报告为未知)。这是 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 绑定(bind)来手动展开/消除存在式，我得到

(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)