Significant slowdown from 4.8.5 to 4.8.6

[smoelius]

Here are timings for the attached prob.txt using z3 4.8.5 and 4.8.6. Note the slowdown: less than 1 second to almost 7 minutes.

$ time z3 prob.txt 
sat
(:version "4.8.5")

real	0m0.630s
user	0m0.622s
sys	0m0.008s

$ time z3 prob.txt 
sat
(:version "4.8.6")

real	6m50.631s
user	6m50.536s
sys	0m0.037s

These experiments were performed on an Ubuntu 18.04.4 machine. z3 was installed using the PyPi package.

prob.txt is pasted here for convenience:

(declare-fun SVALUE_3 () (_ BitVec 256))
(declare-fun SVALUE_1 () (_ BitVec 256))
(declare-fun BV () (_ BitVec 256))
(declare-fun a_414 () (_ BitVec 256))(assert (= a_414 #x0000000000000000000000000000000000000000000000008ac7230489e80000))
(declare-fun a_415 () (_ BitVec 256))(assert (= a_415 (bvneg SVALUE_1)))
(declare-fun a_416 () (_ BitVec 256))(assert (= a_416 (bvadd a_414 a_415)))
(declare-fun a_417 () Bool)(assert (= a_417 (bvuge a_416 SVALUE_3)))
(declare-fun a_418 () (_ BitVec 256))(assert (= a_418 (bvadd SVALUE_1 SVALUE_3)))
(declare-fun a_419 () (_ BitVec 256))(assert (= a_419 #x0000000000000000000000000000000000000000000000000000000000000000))
(declare-fun a_420 () Bool)(assert (= a_420 (bvugt a_418 a_419)))
(declare-fun a_421 () Bool)(assert (= a_421 (not a_420)))
(declare-fun a_422 () (_ BitVec 256))(assert (= a_422 #x000000000000000000000000000000000000000000000000000000000000015a))
(declare-fun a_423 () (_ BitVec 256))(assert (= a_423 #x00000000000000000000000000000000000000000000000000000000000000bf))
(declare-fun a_424 () (_ BitVec 256))(assert (= a_424 (ite a_421 a_422 a_423)))
(declare-fun a_425 () (_ BitVec 256))(assert (= a_425 #x00000000000000000000000000000000000000000000000000000000000003e8))
(declare-fun a_426 () (_ BitVec 256))(assert (= a_426 (bvadd SVALUE_1 SVALUE_3)))
(declare-fun a_427 () (_ BitVec 256))(assert (= a_427 #x00000000000000000000000000000000000000000000000000000000000003e8))
(declare-fun a_428 () (_ BitVec 256))(assert (= a_428 #x0000000000000000000000000000000000000000000000008ac7230489e80000))
(declare-fun a_429 () Bool)(assert (= a_429 (bvule SVALUE_1 a_428)))
(assert (= a_429 true))
(assert (bvult a_426 a_427))
(assert (bvult SVALUE_1 a_425))
(assert (= BV a_424))
(assert (= a_417 true))
(check-sat)
(get-info :version)

[bradlarsen]

I can reproduce the performance regression on an x64 Ubuntu 18.04 machine.

To elaborate a bit, in this scenario, z3 runs in less than a second:

$ python3.8 -mvenv venv && source venv/bin/activate && pip install z3-solver==4.8.5 && time z3 prob.txt

In this case, z3 runs for several minutes:

$ python3.8 -mvenv venv && source venv/bin/activate && pip install z3-solver==4.8.7 && time z3 prob.txt

I will note that I also can reproduce the performance regression when building z3 from source on an x64 Ubuntu 18.04 machine, but on the HEAD of master, the performance regression is much less pronounced (~5s instead of several minutes).

I bisected the performance regression, building z3 from source, between the z3-4.8.4 tag and the z3-4.8.7 tag. (There is no z3-4.8.5 tag?) It looks like commit 3e53b6f introduced the performance regression. That commit changed the default value for tactic.solve_eqs.context_solve. Indeed, @smoelius noted that with a v4.8.7 z3, disabling that makes the performance on this example back to what it was in v4.8.5:

$ time z3 tactic.solve_eqs.context_solve=false prob.txt
sat
(:version "4.8.7")

real    0m0.315s
user    0m0.315s
sys     0m0.000s

[bradlarsen]

A reduced version of the original prob.txt input:

(declare-fun a () (_ BitVec 256))
(declare-fun b () (_ BitVec 256))
(declare-fun c () (_ BitVec 256))
(declare-fun d () (_ BitVec 256))
(declare-fun e () (_ BitVec 256))
(assert (bvuge b a))
(assert (= c (bvadd e a)))
(assert (= d #x0000000000000000000000000000000000000000000000000000000000000008 e))
(assert (bvult c d))
(check-sat)

[NikolajBjorner]

It inspires some tuning. Currently:

(ast-table :prev-capacity 40960 :capacity 5120 :size 2189)
(sat-status
:inconsistent false
:vars 69
:elim-vars 0
:lits 455
:assigned 0
:binary-clauses 81
:ternary-clauses 83
:clauses 10
:del-clause 0
:avg-clause-size 2.61
:memory 4.06)
(sat.solver)
sat
(:version "4.8.8")
(:eliminated-vars 509
:max-memory 5.66
:memory 3.88
:mk-bool-var 5
:num-allocs 19982971
:rlimit-count 724593
:sat-decisions 20
:sat-mk-clause-2ary 81
:sat-mk-clause-3ary 83
:sat-mk-clause-nary 10
:sat-mk-var 69
:sat-propagations-2ary 32
:sat-propagations-3ary 17
:time 0.55
:total-time 0.56)

[NikolajBjorner]

The equality solver could also be tuned (or as a workaround turned off)

[NikolajBjorner]

Thanks, at this point I have added some tuning to also the equality solver.
The most significant fix is the bit-blaster that missed an important simplification.
I can't backport to previous versions, but you can either use a nightly build or the next release (which I will then prepare by next week as there are now multiple reasons for this).

[smoelius]

@NikolajBjorner Thanks a lot for looking into this.