为什么Z3不能用数组和量词解决这个简单的脚本呢？

Question

这是一个在本地构建的Z3 4.6.0和https://rise4fun.com/z3/tutorial上都返回未知(超时)的小型Z3问题

(declare-const m1 (Array String Int))
(declare-const m2 (Array String Int))
(declare-const c Int)
(assert (or (= c 11) (= c 12)))
(assert (forall ((x String)) (= (select m1 x) 0)))
(assert (= (select m2 "0") 42))
(assert (forall ((x String)) (or (= x "0") (= (select m2 x) 0))))
(assert (= m2 (ite (= c 11) (store m1 "1" 100) (store m1 "0" 42))))
(check-sat)

我很好奇为什么z3无法证明这一点。Z3是如何处理这个问题的，有没有一种方法可以确定Z3正在尝试做什么？当我使用-v:15运行时，我看到如下输出：

(smt.restarting :propagations 0 :decisions 903 :conflicts 1 :restart 100 :agility 0.00)
(smt.mbqi)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 84)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi :failed k!8)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 82)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi :failed k!10)
(smt.restarting :propagations 0 :decisions 946 :conflicts 1 :restart 100 :agility 0.00)
^C(tactic-exception "canceled")

我不能完全确定如何处理这个输出。有没有办法在这些点上查看Z3状态的更多信息？

当我稍微将问题更改为以下内容时，它会立即完成：

(declare-const m1 (Array String Int))
(declare-const m2 (Array String Int))
(declare-const c Int)
(assert (= c 12)) ; or (= c 11)
(assert (forall ((x String)) (= (select m1 x) 0)))
(assert (= (select m2 "0") 42))
(assert (forall ((x String)) (or (= x "0") (= (select m2 x) 0))))
(assert (= m2 (ite (= c 11) (store m1 "1" 100) (store m1 "0" 42))))
(check-sat)

第一个问题是否可以解决(同时让c不确定来解决)，同时仍然要求所有值的m1为0，除"0“之外的所有值的m2为0，例如，通过应用适当的策略或量词模式？

Answer 1

对于常量数组的声明，您应该首选const结构，而不是通过量词。也就是说，替换：

(assert (forall ((x String)) (= (select m1 x) 0)))

通过以下方式：

(assert (= m1 ((as const (Array String Int)) 0)))

您会注意到，z3现在可以轻松地处理您的查询。

常量数组在Z3指南：https://rise4fun.com/z3/tutorialcontent/guide#h26中进行了说明