Avoiding double QI across (pop)

[fpoli]

@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]

@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?

[fpoli]

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)

[fpoli]

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)