当试图证明自己是有名无实时的令人惊讶的行为

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给了我WARNING: auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5，尽管事实上(set-option :auto_config false)。

Answer 1

情况如下：

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

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

• case_split=3指示Z3在选择平等匹配的候选者
• 断言（not（for all（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）永远不会被激活

你可以通过在连接词上分布通用量词，并在每种情况下提供模式来绕过这个问题。因此，您（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输入中设置了多个顶级配置，则会重置一些顶级配置。