Quantified BV formula, significant performance regression

[LeventErkok]

The below benchmark has started exhibiting extremely terrible performance. I'm not exactly sure when this started, unfortunately. However, I do know that using z3 that I built on Jun 26th of 2018, it can be solved in about 10 seconds:

$ time z3_Jun26_2018 perf.smt2
sat
(model
  (define-fun s1 () (_ BitVec 64)
    #x0002040810204081)
  (define-fun s0 () (_ BitVec 64)
    #x8080808080808080)
)
z3_Jun26_2018 perf.smt2  9.71s user 0.14s system 99% cpu 9.903 total

Unfortunately, a fresh build of z3 takes 22 times more, about 3 minutes and 42 seconds:

$ time z3 perf.smt2
sat
(model
  (define-fun s1 () (_ BitVec 64)
    #x0002040810204081)
  (define-fun s0 () (_ BitVec 64)
    #x8080808080808080)
)
z3 perf.smt2  219.21s user 1.30s system 99% cpu 3:42.33 total

(Generated models are the same; so at least there's no soundness concern.)

Here's the benchmark:

(set-option :produce-models true)
(set-logic BV)
(define-fun s4 () (_ BitVec 1) #b0)
(declare-fun s0 () (_ BitVec 64))
(declare-fun s1 () (_ BitVec 64))
(assert (forall ((s2 (_ BitVec 64)))
            (let ((s3 ((_ extract 7 7) s2)))
            (let ((s5 (distinct s3 s4)))
            (let ((s6 (bvand s0 s2)))
            (let ((s7 (bvmul s1 s6)))
            (let ((s8 ((_ extract 56 56) s7)))
            (let ((s9 (distinct s4 s8)))
            (let ((s10 (= s5 s9)))
            (let ((s11 ((_ extract 15 15) s2)))
            (let ((s12 (distinct s4 s11)))
            (let ((s13 ((_ extract 57 57) s7)))
            (let ((s14 (distinct s4 s13)))
            (let ((s15 (= s12 s14)))
            (let ((s16 ((_ extract 23 23) s2)))
            (let ((s17 (distinct s4 s16)))
            (let ((s18 ((_ extract 58 58) s7)))
            (let ((s19 (distinct s4 s18)))
            (let ((s20 (= s17 s19)))
            (let ((s21 ((_ extract 31 31) s2)))
            (let ((s22 (distinct s4 s21)))
            (let ((s23 ((_ extract 59 59) s7)))
            (let ((s24 (distinct s4 s23)))
            (let ((s25 (= s22 s24)))
            (let ((s26 ((_ extract 39 39) s2)))
            (let ((s27 (distinct s4 s26)))
            (let ((s28 ((_ extract 60 60) s7)))
            (let ((s29 (distinct s4 s28)))
            (let ((s30 (= s27 s29)))
            (let ((s31 ((_ extract 47 47) s2)))
            (let ((s32 (distinct s4 s31)))
            (let ((s33 ((_ extract 61 61) s7)))
            (let ((s34 (distinct s4 s33)))
            (let ((s35 (= s32 s34)))
            (let ((s36 ((_ extract 55 55) s2)))
            (let ((s37 (distinct s4 s36)))
            (let ((s38 ((_ extract 62 62) s7)))
            (let ((s39 (distinct s4 s38)))
            (let ((s40 (= s37 s39)))
            (let ((s41 ((_ extract 63 63) s2)))
            (let ((s42 (distinct s4 s41)))
            (let ((s43 ((_ extract 63 63) s7)))
            (let ((s44 (distinct s4 s43)))
            (let ((s45 (= s42 s44)))
            (let ((s46 (and s40 s45)))
            (let ((s47 (and s35 s46)))
            (let ((s48 (and s30 s47)))
            (let ((s49 (and s25 s48)))
            (let ((s50 (and s20 s49)))
            (let ((s51 (and s15 s50)))
            (let ((s52 (and s10 s51)))
            s52)))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
(get-model)

[LeventErkok]

@NikolajBjorner

This benchmark has gotten a lot worse, sometime today. Now it doesn't complete even after running for 10 minutes. It's rather disconcerting as it used to be a mere 10 seconds but now seems to run forever.

[NikolajBjorner]

smt.auto_config=false smt.relevancy=0 works much better on this.

[LeventErkok]

Indeed it does much better! 25s on my machine now. Thanks!

I'm closing this ticket; but feel free to reopen if necessary.

[NikolajBjorner]

I get "unknown" wtih some random seeds or internal code variants, not sure why. Overall, it could be that we just need to change the auto-config for this class to avoid relevancy which is both overhead and hides potentially useful lemmas. @nunoplopes - can you try relevancy=0?

[nunoplopes]

I see a ~7% speedup with my custom solver stack and a slight reduction of timeouts.
So, from this quick round of benchmarks, /me likes it!

[nunoplopes]

FYI I'm trying now with relevancy=2 but auto_config=false to see if there's any difference.

[nunoplopes]

Ok, I run my BV benchmarks with relevancy=2 and auto_config=false and got very similar results.
So it seems the speedup is coming from somewhere else..

[NikolajBjorner]

another example where smtfd smokes other approaches