3

考虑以下 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，尽管(set-option :auto_config false).

4

1 回答 1

3

情况如下：

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

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

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

您可以通过在连词上分配全称量词并在每种情况下提供模式来绕过此问题。因此，你（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 输入中设置了多个顶级配置，我最近修复了一些顶级配置被重置的方式的错误。

于 2015-05-19T16:04:14.343 回答