2

我已经设法使用 Z3 创建了一个记录数组，但现在正在努力查看在数组上执行 $\forall$ 操作所需的语法......这是我到目前为止的 SMT-LIB2 代码片段示例.

(declare-datatypes () ((rec (mk-R5 (age Int) (area Int) (married Bool)))))
(declare-const recs (Array Int rec))
(declare-const r1 rec)
(assert(= (age r1) 15))
(assert(= (area r1) 10001))
(assert(= (married r1) true))
(declare-const r2 rec)
(assert(= (age r2) 35))
(assert(= (area r2) 2845))
(assert(= (married r2) true))
(declare-const x Int)
(declare-const y Int)
(assert (= recs (store recs x r1)))
(assert (= recs (store recs y r2)))
(assert(forall ((i rec)) (= (married i) true)))
(check-sat)
(get-model)

我想倒数第三行应该对数组有一些参考，但我已经尝试了一切，教程并没有帮助我解决这个问题。

如何对这里的数组执行 $\forall$ 操作？

4

1 回答 1

3

看来您正试图将两条记录放在一个数组中，然后对这些元素说些什么。不幸的是，您的编码并不完全意味着这一点。

首先要注意的是以下行的含义：

   (declare-const recs (Array Int rec))

这表示这是一个由所有整数recs索引的数组。也就是说，域是所有Int值的集合。这可能不是你的意思。

此外，这些行：

(assert (= recs (store recs x r1)))
(assert (= recs (store recs y r2)))

最好这样写：

(assert (= (select recs x) r1))
(assert (= (select recs y) r2))

可以将其视为说明您对 indexx和y;的了解 recs与您尝试编写时要“修改”的一些命令式赋值语句相反。没有修改 smt-lib 中任何值的概念；您只需说明您所知道的关于您正在构建的模型的真实情况。

修复你的 forall-assertion 的一种方法是这样写：

(assert (forall ((i Int)) 
                (implies (or (= i x) (= i y)) 
                         (= (married (select recs i)) true))))

我们对索引进行量化，并说如果索引是i或y，那么这些记录就married有人。通过这些修改，Z3 回应：

sat
(model
  (define-fun r2 () rec
    (mk-R5 35 2845 true))
  (define-fun recs () (Array Int rec)
    (_ as-array k!0))
  (define-fun y () Int
    1)
  (define-fun x () Int
    0)
  (define-fun r1 () rec
    (mk-R5 15 10001 true))
  (define-fun k!0!2 ((x!0 Int)) rec
    (ite (= x!0 1) (mk-R5 35 2845 true)
      (mk-R5 15 10001 true)))
  (define-fun k!1 ((x!0 Int)) Int
    (ite (= x!0 0) 0
      1))
  (define-fun k!0 ((x!0 Int)) rec
    (k!0!2 (k!1 x!0)))
)

这有点难以阅读，但它确实为您提供了您指定的模型。

然而，在我看来，这并不是你真正想要建模的。但很难从你的问题中看出。如果您描述了您要解决的实际问题，那么答案可能会更有帮助。

于 2017-01-06T06:58:22.857 回答