Amazing behavior when trying to prove
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|
)))
Trying to assert that the axiom holds bar
, i.e.
(push)
(assert (not (forall ((a Int) (b Int) (c Int))
(and
(trigG a)
(trigF a b c)))))
(check-sat)
(pop)
doesn't work (Z3 4.3.2 - build hashcode 47ac5c06333b):
unknown
[quantifier_instances] limited-G : 1 : 0 : 1
Question 1: Why did Z3 only instantiate limited-G
, but neither limited-F
, nor bar
(to prove the claim)?
Question 2: Commenting on any of the (useless) statements foo
, limited-F
or limited-G
allows Z3 to prove the statement - why? (Depending on which is commented out, instances of only bar
or bar
and are created limited-F
.)
In case it has to do with observable behavior: I would like to set smt.case_split
to 3
(my config follows what Boogie MSR omitted ), but Z3 gives me WARNING: auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5
despite that (set-option :auto_config false)
.
source to share
The situation is as follows:
-
when using a template-based instance exclusively, Z3 takes a somewhat quick approach to finding quantifier instances.
-
by disabling MBQI, you are relying on a match matching engine.
- case_split = 3 instructs Z3 to use the relevance heuristic when selecting candidates for equality matching.
- The statement (not (forall (a, b, c) (and (trigG a) (trigF abc)))) expands (not (trigger a! 0)) (not (trigger a! 0 b! 1 c! 2)) ).
- only one of the two clauses is applicable to satisfy the formula.
- The search sets (trigG a! 0) are false, so the statement is executed. Therefore the trigger (abc trigger) is never activated.
You can work around this problem by scattering in universal quantifiers over conjunctions and supplying templates in each case. So you (r tool) can 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|
)))
to two axioms.
(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|
)))
The problem with setting autocomplete seems to be fixed. I recently fixed the bug that some top-level configurations were reset if multiple top-level configurations were set in the smt-lib entry.
source to share