record - 在 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 绑定(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 .

我想这里面有四个问题:

有没有办法调用 z3 来解决第一个实例和第二个实例？

我应该以不同的方式编码我的记录/结构吗？

我是否应该以不同的方式编码我的 let 表达式(正是这些导致存在量化)？

或者，我是否应该直接扩展 let-expressions(我可以自己做，但如果有很多引用，它可能会导致大术语)。

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)