2

下面的代码用两个字段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 表达式（我可以自己做，但如果有很多引用，它可能会导致大术语）。
4

1 回答 1

3

从问题看来，您可以使用正确的 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)
于 2013-01-18T06:00:45.650 回答