1

我有一个简单的公式，在数组集上带有量词，Z3(4.3.2) 返回“未知”。

(assert (forall ((a (Array Int Int)) (b (Array Int Int))) (=> (forall ((i Int)) (= (select a i) (select b i))) (= a b))))
(check-sat)

详细的是：

(simplifier :num-exprs 12 :num-asts 185 :time 0.00 :before-memory 2.49 :after-memory 2.49)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi)
(smt.simplifier-done)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 1)
(smt.simplifier-done)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 1)
(smt.mbqi :failed k!1)
(smt.restarting :propagations 0 :decisions 0 :conflicts 0 :restart 100 :agility 0.00)
(tactic-exception "smt tactic failed to show goal to be sat/unsat")

似乎 Z3 允许这种公式。由于我对冗长的不完全理解，我是否错过了一些可以使用的策略？你能帮忙解决这个公式吗？

4

2 回答 2

3

Z3 教程（Section Quantifiers）描述了 Z3 完成的片段。一般问题是无法确定的。

关于您的示例，Z3 将在包含数组范围内的量词的可满足实例上失败。请注意，您的公式是可满足的。如果我们否定它，那么 Z3 自动证明它是不可满足的。

(assert (not (forall ((a (Array Int Int)) (b (Array Int Int))) 
             (=> (forall ((i Int)) (= (select a i) (select b i))) (= a b)))))
(check-sat)

备注：Z3 本质上是一个可满足性检查器。为了证明一个公式F，我们证明否定是不可满足的。

于 2013-10-13T17:22:08.490 回答
1

实际上，您可以先尝试消除量词。使用战术“qe”、“qe-sat”或“qe-light”可能会有所帮助。我试过了，它似乎变成了“真”。

于 2014-11-06T07:07:35.377 回答