试图证明所有人时令人惊讶的行为 [英] Surprising behaviour when trying to prove a forall

问题描述

请考虑以下SMT-LIB代码:

Consider the following SMT-LIB code:

(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):

fails (Z3 4.3.2 - build hashcode 47ac5c06333b):

unknown
[quantifier_instances]  limited-G :      1 :   0 : 1

问题1:为什么Z3只实例化limited-G而不实例化limited-F或bar(这将证明断言)?

Question 1: Why did Z3 only instantiate limited-G but neither limited-F nor bar (which would prove the assertion)?

问题2:评论任何(无用的)断言foo，limited-F或limited-G都可以让Z3证明该断言-为什么? (根据要注释的内容，仅实例化bar或bar和limited-F.)

Question 2: Commenting any of the (useless) assertions foo, limited-F or limited-G allows Z3 to prove the assertion - why is that? (Depending on which are commented, either only bar or bar and limited-F are instantiated.)

如果它与观察到的行为有关:我想将smt.case_split设置为3(我的配置遵循MSR的

In case it is related to the observed behaviour: I would like to set smt.case_split to 3 (my configuration follows the one omitted by MSR's Boogie tool), but Z3 gives me WARNING: auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5, despite the fact that (set-option :auto_config false).

推荐答案

情况如下:

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

• when using pattern based instantiation exclusively Z3 takes a somewhat operational approach to finding quantifier instantiations.

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

by disabling MBQI you rely on the equality matching engine.

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

You can bypass this issue by distributing in universal quantifiers over conjunctions, and supplying patterns in each case. Thus, you(r tool) could rewrite the axiom:

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

The issue of setting auto-completion seems fixed. I somewhat recently fixed bug in the way that some top-level configurations were reset if multiple top-level configurations were set in the smt-lib input.

这篇关于试图证明所有人时令人惊讶的行为的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！