如何在集合上的量词公式上使用Z3？

Question

对于数组集合，我有一个带有量词的简单公式，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似乎允许这种公式。从我对细节的不完全理解来看，我是不是错过了一些战术？你能帮我解一下这个公式吗？

Answer 1

Z3教程 (区段量词)描述了哪个片段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，证明了否定是不可满足的。

Answer 2

实际上，一开始你可以尝试消除量词。使用“qe”、“qe”或“”可能会有所帮助。我试过了，它似乎变成了“真”。