z3 - 为什么连词的电子匹配对顺序/案例拆分策略敏感？

Question

鉴于以下简化的量词，根据 Boogie 生成的 Z3 选项设置(下面有完整的详细信息)，结果我得到“未知”:

(declare-fun F (Int) Bool)
(declare-fun G (Int) Bool)

(assert (forall ((x Int)) (! (and
  (F x) (G x))
  :pattern ((F x))
)))
(assert (not (forall ((x Int)) (! (and
  (G x) (F x))
  :pattern ((F x))
))))
(check-sat)

我对(我认为)Z3 将如何处理这个问题的理解是 skolemise the existential(不是 for all)，这将产生 F 和 G 的基础实例。鉴于电子图中的这些，我们应该能够实例化另一个量词，并获得不满意。我可以看到 Z3 可能必须进行大小写拆分才能执行此操作，但我希望在删除量词并填充电子图之后进行这种大小写拆分。

相反，第一个量词在上述问题中没有被实例化。我做了一些观察:

1. 交换第一个量词中 (F x) 和 (G x) 项的顺序会导致没有任何量词实例化的“unsat”(我想一些简化会发现两个量化断言之间的相似性？)。
2. 交换第二个量词(以及第一个量词)中的 (G x) 和 (F x) 项的顺序会导致“unsat”与单个量词实例化(这是我期望的行为一般而言)。
3. 更改 smt.case_split 选项会影响行为。设置为 3(由 Boogie 选择)或 5，我们得到“未知”。设置为 0、1、2 或 4，我会“不满意”。

如果能理解上述场景，以及为什么(在失败的情况下)这些术语在 skolemisation 后并不总是出现在电子图中，那就太好了。我不确定更改 case_split 选项的一般效果是什么。目前，我认为 Boogie 不允许对其进行更改(并覆盖在命令行上所做的任何选择)。但我觉得电子图应该在所有情况下都能获得信息，这是理想情况。

这是完整的文件(删除大部分选项集似乎对失败案例没有影响，除了 smt.case_split 那个):

(set-option :print-success false)
(set-info :smt-lib-version 2.0)
(set-option :AUTO_CONFIG false)
;(set-option :MODEL.V2 true)
(set-option :smt.PHASE_SELECTION 0)
(set-option :smt.RESTART_STRATEGY 0)
(set-option :smt.RESTART_FACTOR |1.5|)
(set-option :smt.ARITH.RANDOM_INITIAL_VALUE true)
(set-option :smt.DELAY_UNITS true)
(set-option :NNF.SK_HACK true)
(set-option :smt.MBQI false)
(set-option :smt.QI.EAGER_THRESHOLD 100)
(set-option :smt.QI.COST |"(+ weight generation)"|)
(set-option :TYPE_CHECK true)
(set-option :smt.BV.REFLECT true)
(set-option :TIMEOUT 0)
(set-option :smt.QI.PROFILE true)
(set-option :smt.CASE_SPLIT 3)
; done setting options


(declare-fun F (Int) Bool)
(declare-fun G (Int) Bool)

(assert (forall ((x Int)) (! (and
  (F x) (G x))
   :pattern ((F x))
)))
(assert (not (forall ((x Int)) (! (and
(G x) (F x))
  :pattern ((F x))
))))
(check-sat)

Answer 1

这由 https://stackoverflow.com/users/1096362/nikolaj-bjorner 的答案解决对于这个问题: Surprising behaviour when trying to prove a forall

将证明义务转换为析取，然后是子句的相应相关性，解释了为什么 Z3 没有将这两个连词视为潜在的触发因素。