鉴于以下简化量词，根据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会对这个问题做什么的理解是对存在主义（不是forall）的理解，它会产生F和G的基础实例 . 在电子图中给出这些，我们应该能够实例化其他量词，并得到不满 . 我可以看到Z3可能需要进行大小写分割，但我希望在删除量词并填充电子图之后进行这种情况分割 .
相反，第一个量词不会在上述问题中得到实例化 . 我做了一些观察：
-
交换第一个量词中（F x）和（G x）项的顺序导致"unsat"没有任何量词实例化（我想一些简化会发现两个量化断言之间的相似性？） .
-
交换第二个量词中的（G x）和（F x）项的顺序（以及第一个中的那些）导致"unsat"具有单个量词实例化（这是我通常期望的行为） .
-
更改smt.case_split选项会影响行为 . 设置为3（由Boogie选择）或5，我们得到"unknown" . 设置为0,1,2或4，我得到"unsat" .
理解上面的场景会很好，为什么（在失败的情况下）这些术语并不总是在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)
1 回答
这是通过https://stackoverflow.com/users/1096362/nikolaj-bjorner对这个问题的回答来解决的：Surprising behaviour when trying to prove a forall
将证明义务转换为分离，然后是相应的条款相关性，解释了为什么Z3不会将两个联合视为潜在的触发因素 .