triggers - 试图证明一个人时的令人惊讶的行为

Question

考虑以下 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 给我警告:必须禁用自动配置(选项 AUTO_CONFIG)才能使用选项 CASE_SPLIT=3、4 或 5，尽管 (set-option :auto_config false) >.

Answer 1

情况如下:

• 当专门使用基于模式的实例化时，Z3 会采取某种操作方法来查找量词实例化。

• 通过禁用 MBQI，您将依赖于相等匹配引擎。

• case_split = 3 指示 Z3 在以下情况下使用相关性启发式: 选择候选人进行平等匹配。
• 断言 (not (forall (a, b, c) (and (trigG a) (trigF a b c)))) 扩展 或 (not (trigG a!0)) (not (trigF a!0 b!1 c!2)))。
• 两个析取项中只有一个与满足公式有关。
• 搜索将 (trigG a!0) 设置为 false，因此满足该子句。因此，触发器 (trigF a b c) 永远不会被激活。

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

(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 输入中设置了多个顶级配置，则某些顶级配置会被重置。