Avoiding double QI across (pop)
fpoli opened this issue · 3 comments
@marcoeilers Does Silicon encode assert <expr>; ... to some SMT2 where <expr> is repeated twice, with a pop in between?
(push)
(assert !<expr>)
(check-sat)
(pop)
(assert <expr>)
...
If so, I suspect that the following can be more efficient for QI-heavy programs, up to 2 times faster in the best case, because quantifiers that match on <expr> should just be instantiated once before the push instead of twice across the pop. This because (as far as I understand) Z3's parser performs the "early" instantiations even before reaching a check-sat. (Orthogonally, for non-trivial <expr> the SMT2 code gets a bit shorter and the parser has to work a bit less.)
(assert a == <expr>)
(push)
(assert !a)
(check-sat)
(pop)
(assert a)
...
@marcoeilers Does Silicon encode
assert <expr>; ...to some SMT2 where<expr>is repeated twice, with a pop in between?
It does this for assertions that are directly asserted on the Viper-level, but not for intermediate assertions that come up durng symbolic execution (those aren't assumed after being asserted).
If so, I suspect that the following can be more efficient for QI-heavy programs, up to 2 times faster in the best case, because quantifiers that match on
<expr>should just be instantiated once before the push instead of twice across the pop.
Yes, interesting idea, we should definitely try that out.
This because (as far as I understand) Z3's parser performs the "early" instantiations even before reaching a check-sat.
Huh, I didn't know that. Is this documented somewhere or did you read the code?
Huh, I didn't know that. Is this documented somewhere or did you read the code?
Neither. I just noticed from some stack traces of Z3 that the solver performs simplifications while parsing, so I think that it's at that point that the early quantifications are triggered.
The proposed modification of the encoding doesn't help if QI is not the bottleneck. For example, I don't see any benefit when applying it on the first SMT file shown below. Version 1 takes 62s and version 2 (with the modified encoding) takes 54s. The number of reported QI in the second version is indeed half (30000 instead of 60000), but that's not enough to cut the verification time in half. Interestingly, increasing the complexity of the formula in the quantifier seems to increase the difference in the verification time between the two versions.
SMT files
Version 1:
(set-option :print-success true)
(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.qi.eager_threshold 30000)
(declare-fun f (Int Int Int) Bool)
(declare-fun a () Bool)
(assert (forall ((x Int) (y Int) (z Int)) (!
(=
(f x y z)
(f (* x 2) (* y 3) (* z 4)))
:pattern ((f x y z))
)))
(push)
(assert (not (f 1 1 1)))
(check-sat)
(get-info :all-statistics)
(pop)
(assert (f 1 1 1))
(check-sat)
(get-info :all-statistics)
Version 2:
(set-option :print-success true)
(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.qi.eager_threshold 30000)
(declare-fun f (Int Int Int) Bool)
(declare-fun a () Bool)
(assert (forall ((x Int) (y Int) (z Int)) (!
(=
(f x y z)
(f (* x 2) (* y 3) (* z 4)))
:pattern ((f x y z))
)))
(assert (= a (f 1 1 1)))
(push)
(assert (not a))
(check-sat)
(get-info :all-statistics)
(pop)
(assert a)
(check-sat)
(get-info :all-statistics)
Statistics
Stats version 1 (on a different run):
(:arith-make-feasible 30001
:arith-max-columns 75004
:del-clause 60000
:final-checks 1
:max-generation 30000
:max-memory 2737.76
:max-missed-qa-cost 30001.00
:memory 2721.65
:min-missed-qa-cost 30001.00
:missed-quant-instantiations 1
:mk-bool-var 60002
:mk-clause 60000
:num-allocs 60409095194.00
:num-checks 1
:propagations 30000
:quant-instantiations 30000
:rlimit-count 1080251
:time 26.90)
(:arith-make-feasible 60001
:arith-max-columns 75004
:binary-propagations 30000
:del-clause 60000
:final-checks 2
:max-generation 30000
:max-memory 2747.43
:max-missed-qa-cost 30001.00
:memory 2725.12
:min-missed-qa-cost 30001.00
:missed-quant-instantiations 1
:mk-bool-var 120003
:mk-clause 60000
:num-allocs 336187351538.00
:num-checks 2
:propagations 60000
:quant-instantiations 60000
:rlimit-count 2160308
:time 27.68)
Stats version 2 (on a different run):
(:arith-make-feasible 30001
:arith-max-columns 75004
:binary-propagations 1
:final-checks 1
:max-generation 30000
:max-memory 2737.58
:max-missed-qa-cost 30001.00
:memory 2721.47
:min-missed-qa-cost 30001.00
:missed-quant-instantiations 1
:mk-bool-var 60003
:mk-clause 120000
:num-allocs 60577419513.00
:num-checks 1
:propagations 30001
:quant-instantiations 30000
:rlimit-count 1020278
:time 26.06)
(:arith-make-feasible 30002
:arith-max-columns 75004
:binary-propagations 2
:del-clause 120000
:final-checks 2
:max-generation 30000
:max-memory 2744.65
:max-missed-qa-cost 30001.00
:memory 2722.34
:min-missed-qa-cost 30001.00
:missed-quant-instantiations 1
:mk-bool-var 60003
:mk-clause 120000
:num-allocs 101204546256.00
:num-checks 2
:propagations 60002
:quant-instantiations 30000
:rlimit-count 1080323
:time 25.14)
Here is an hand-crafted example where QI seems to be the true bottleneck. In this case, the modified encoding takes 44% less time.
Version 1: 45s
(set-option :print-success true)
(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.qi.eager_threshold 1000000)
(declare-fun f (Int Int) Bool)
(declare-fun a () Bool)
(assert (forall ((x Int) (y Int)) (!
(and
(=> (= x 1000000) false)
(f (+ x 1) y)
)
:pattern ((f x y))
)))
(push)
(assert (not (f 1 1)))
(check-sat)
(get-info :all-statistics)
(pop)
(assert (f 1 1))
(check-sat)
(get-info :all-statistics)
Version 2: 25s, or 44% time less
(set-option :print-success true)
(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.qi.eager_threshold 1000000)
(declare-fun f (Int Int) Bool)
(declare-fun a () Bool)
(assert (forall ((x Int) (y Int)) (!
(and
(=> (= x 1000000) false)
(f (+ x 1) y)
)
:pattern ((f x y))
)))
(assert (= a (f 1 1)))
(push)
(assert (not a))
(check-sat)
(get-info :all-statistics)
(pop)
(assert a)
(check-sat)
(get-info :all-statistics)