1

我有兴趣证明关于某些假设的陈述的有效性。然而，Z3 似乎默认采用“开放”模型。例如，假设我们假设

富（4）

关于这个陈述，我想表明“在” foo 中的东西是均匀的。所以我首先声明 foo

(declare-fun foo (Int) Bool)

接下来，因为我对假设很感兴趣。我构建了一个含义：

(implies (foo 4) (not (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))))

最后，因为我对有效性感兴趣，而不是可满足性，所以我想检查这个陈述的否定的不可满足性。 

(assert (not (implies (foo 4) (not (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))))))
(check-sat)

不过 Z3 报道称，这个说法确实是可以满足的：

sat
(model 
  (define-fun x!0 () Int
    (- 1))
  (define-fun foo ((x!1 Int)) Bool
    (ite (= x!1 4) true
    (ite (= x!1 (- 1)) true
      true)))
)

我大致了解这里发生了什么，但我不确定如何最好地表达 foo 在我的假设陈述下应该“关闭”。对于这个非常简单的示例，我可以通过告诉 Z3 foo 没有其他成员来做到这一点：

(assert (not (implies (and (foo 4) (not (exists ((x Int)) (and (not (= x 4)) (foo x))))) (not (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))))))

然而，当我转向更复杂的假设时，似乎很难自动生成公式来定义那些不在 foo 中的东西。

我错过了什么愚蠢的东西吗？

4

1 回答 1

1

当且仅当 x = 4 时，为什么不声明 (foo x)？您的第一条语句说（在反编译否定之后）：

(assert (foo 4))
(assert (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))

这可以通过将所有内容映射到“真”的函数 foo 来满足，并且可以使用 x = -1 来满足存在断言。这是标准的一阶语义。

说 foo 最多满足 4 的一种方式是：

(assert (forall ((x Int)) (=> (foo x) (= x 4))))

您也可以说 foo 仅在 4 处成立：

(assert (forall ((x Int)) (= (foo x) (= x 4))))
于 2013-11-04T03:45:00.727 回答