尝试证明 forall 时的令人惊讶的行为答案

【问题标题】：Surprising behaviour when trying to prove a forall尝试证明 forall 时的令人惊讶的行为
【发布时间】：2014-10-26 16:38:44
【问题描述】：

考虑以下 SMT-LIB 代码：

(set-option :auto_config false)
(set-option :smt.mbqi false)
; (set-option :smt.case_split 3)
(set-option :smt.qi.profile true)

(declare-const x Int)

(declare-fun trigF (Int Int Int) Bool)
(declare-fun trigF$ (Int Int Int) Bool)
(declare-fun trigG (Int) Bool)
(declare-fun trigG$ (Int) Bool)

; Essentially noise
(declare-const y Int)
(assert (!
  (not (= x y))
  :named foo
))

; Essentially noise
(assert (forall ((x Int) (y Int) (z Int)) (!
  (= (trigF$ x y z) (trigF x y z))
  :pattern ((trigF x y z))
  :qid |limited-F|
)))

; Essentially noise
(assert (forall ((x Int)) (!
  (= (trigG$ x) (trigG x))
  :pattern ((trigG x))
  :qid |limited-G|
)))

; This assumption is relevant
(assert (forall ((a Int) (b Int) (c Int)) (!
  (and
    (trigG a)
    (trigF a b c))
  :pattern ((trigF a b c))
  :qid |bar|
)))

试图断言公理bar成立，即，

(push)
(assert (not (forall ((a Int) (b Int) (c Int))
  (and
    (trigG a)
    (trigF a b c)))))
(check-sat)
(pop)

失败（Z3 4.3.2 - 构建哈希码 47ac5c06333b）：

unknown
[quantifier_instances]  limited-G :      1 :   0 : 1

问题 1： 为什么 Z3 只实例化 limited-G 而既没有实例化 limited-F 也没有实例化 bar（这将证明断言）？

问题 2： 评论任何（无用的）断言 foo、limited-F 或 limited-G 允许 Z3 证明断言 - 为什么会这样？（取决于注释的内容，仅实例化 bar 或 bar 和 limited-F。）

如果它与观察到的行为有关：我想将smt.case_split 设置为3（我的配置遵循MSR 的Boogie 工具省略的配置），但Z3 给了我WARNING: auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5，尽管@ 987654339@.

【问题讨论】：

您的问题还没有答案，但是已经有一些与参数问题相关的错误修正，这也是您看到的警告消息的来源。您能否验证问题是否仍然存在？
@ChristophWintersteiger 我刚用 Z3 4.4.0 9bff93279f75 x64 试过，结果是一样的
@ChristophWintersteiger 仅供参考：官方 Z3 4.4.0 版本 (github.com/Z3Prover/bin/blob/master/releases/…) 仍然显示相同的行为

标签： triggers z3 smt quantifiers

【解决方案1】：

情况如下：

当仅使用基于模式的实例化时，Z3 采用某种操作方法来查找量词实例化。
通过禁用 MBQI，您可以依赖相等匹配引擎。
case_split = 3 指示 Z3 在以下情况下使用关联启发式选择平等匹配的候选人。
断言 (not (forall (a, b, c) (and (trigG a) (trigF a b c)))) 展开变成一个析取（or (not (trigG a!0)) (not (trigF a!0 b!1 c!2)))）。
两个析取项中只有一个与满足公式有关。
搜索将 (trigG a!0) 设置为 false，因此满足子句。因此，触发器 (trigF a b c) 永远不会被激活。

您可以通过在连词上分配全称量词并在每种情况下提供模式来绕过此问题。因此，你（r 工具）可以重写公理：

(assert (forall ((a Int) (b Int) (c Int)) (!
  (and
    (trigG a)
    (trigF a b c))
  :pattern ((trigF a b c))
  :qid |bar|
 )))

两个公理。

(assert (forall ((a Int)) (! (trigG a) :pattern ((trigG a))))
(assert (forall ((a Int) (b Int) (c Int)) (!
    (trigF a b c)
  :pattern ((trigF a b c))
  :qid |bar|
 )))

设置自动完成的问题似乎已解决。如果在 smt-lib 输入中设置了多个顶级配置，我最近修复了一些顶级配置被重置的方式的错误。

【讨论】：