berraschendes Verhalten beim Versuch, ein Forall zu beweis
Betrachten Sie den folgenden 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|
)))
Versuch, dieses Axiom zu behauptenbar
gilt, d. h.,
(push)
(assert (not (forall ((a Int) (b Int) (c Int))
(and
(trigG a)
(trigF a b c)))))
(check-sat)
(pop)
fails (Z3 4.3.2 - Build-Hashcode 47ac5c06333b):
unknown
[quantifier_instances] limited-G : 1 : 0 : 1
Frage 1 Warum hat Z3 nur @ instanziierlimited-G
doch keinslimited-F
Nochbar
(was würde die Behauptung beweisen)?
Frage 2 Kommentieren einer der (nutzlosen) Behauptungenfoo
, limited-F
oderlimited-G
erlaubt Z3, die Behauptung zu beweisen - warum ist das so? (Je nachdem welche kommentiert sind, kann entweder nurbar
oderbar
undlimited-F
werden instanziiert.)
Falls es mit dem beobachteten Verhalten zusammenhängt: Ich möchte @ setzsmt.case_split
zu3
(meine Konfiguration folgt der von MSRs @ weggelassene Boogie Tool), aber Z3 gibt mirWARNING: auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5
, trotz der Tatsache dass(set-option :auto_config false)
.