Exponential blowup in skolem_intro

[BrunoDutertre]

In the CVC5 signatures: skolem_intro calls sc_mk_skolem which calls sc_to_original.

With the current lfscc, evaluation of sc_to_original can cause an exponential blowup (in term size and in runtime).

Here's the relevant fragment:

(program sc_to_original ((t term)) term
  (match t
    ((apply t1 t2) (apply (sc_to_original t1) (sc_to_original t2)))
     ... 
  ))

The recursive calls do no preserve sharing of common sub-terms (i.e., they convert a DAG to a tree). Also, the match t requires beta reduction (a call to CExpr::whr) which may create more occurrences of sub-terms and make things worse.

Here's an example that illustrates this problem:

(define y (var 0 String))
(define t278 (int 0))
(define t311 (int (~ 1)))
(define t310 (str.len y))
(define t313 (str.substr y t278 (a.+ t311 (a.+ t310 t278)))
(define t352 (str.len t313))
(define t354 (str.substr t313 t278 (a.+ t311 (a.+ t352 t278)))
(define t380 (str.len t354))
(define t381 (str.substr t354 t278 (a.+ t311 (a.+ t380 t278))))
(define t410 (str.len t381))
(define t411 (str.substr t381 t278 (a.+ t311 (a.+ t410 t278))))
(define t443 (str.len t411))
(define t444 (str.substr t411 t278 (a.+ t311 (a.+ t443 t278))))
(define t479 (str.len t444))
(define t480 (str.substr t444 t278 (a.+ t311 (a.+ t479 t278))))
(define t517 (str.len t480))
(define t518 (str.substr t480 t278 (a.+ t311 (a.+ t517 t278))))
(define t559 (str.len t518))
(define t560 (str.substr t518 t278 (a.+ t311 (a.+ t559 t278))))
(define t604 (str.len t560))
(define t605 (str.substr t560 t278 (a.+ t311 (a.+ t604 t278))))
(define t652 (str.len t605))
(define t653 (str.substr t605 t278 (a.+ t311 (a.+ t652 t278))))
(define t702 (str.len t653))
(define t703 (str.substr t653 t278 (a.+ t311 (a.+ t702 t278))))
(define t756 (str.len t703))
(define t757 (str.substr t703 t278 (a.+ t311 (a.+ t756 t278))))
(define t813 (str.len t757))
(define t814 (str.substr t757 t278 (a.+ t311 (a.+ t813 t278))))
(define t872 (str.len t814))
(define t873 (str.substr t814 t278 (a.+ t311 (a.+ t872 t278))))
(define t934 (str.len t873))
(define t935 (str.substr t873 t278 (a.+ t311 (a.+ t934 t278))))
(define t999 (str.len t935))
(define t1000 (str.substr t935 t278 (a.+ t311 (a.+ t999 t278))))
(define t1067 (str.len t1000))
(define t1068 (str.substr t1000 t278 (a.+ t311 (a.+ t1067 t278))))
(define t1137 (str.len t1068))
(define t1138 (str.substr t1068 t278 (a.+ t311 (a.+ t1137 t278))))
(define t1212 (str.len t1138))
(define t1213 (str.substr t1138 t278 (a.+ t311 (a.+ t1212 t278))))
(define t1289 (str.len t1213))
(define t1290 (str.substr t1213 t278 (a.+ t311 (a.+ t1289 t278))))
(define t1369 (str.len t1290))
(define t1370 (str.substr t1290 t278 (a.+ t311 (a.+ t1369 t278))))

(run (sc_mk_skolem t313))
(run (sc_mk_skolem t354))
(run (sc_mk_skolem t381))
(run (sc_mk_skolem t411))
(run (sc_mk_skolem t444))
(run (sc_mk_skolem t480))
(run (sc_mk_skolem t518))
(run (sc_mk_skolem t560))
(run (sc_mk_skolem t605))
(run (sc_mk_skolem t653))
(run (sc_mk_skolem t703))
(run (sc_mk_skolem t757))
(run (sc_mk_skolem t814))
(run (sc_mk_skolem t873))
(run (sc_mk_skolem t935))
(run (sc_mk_skolem t1000))
(run (sc_mk_skolem t1068))
(run (sc_mk_skolem t1138))
(run (sc_mk_skolem t1213))
(run (sc_mk_skolem t1290))
(run (sc_mk_skolem t1370))

I've instrumented lfscc to print size of terms (measured as number of nodes in the DAG representation). Here's the blow-up on this input:

; WARNING: Empty proof!!!
[Running-sc: input size = 80 output size = 23]
[Running-sc: input size = 86 output size = 39]
[Running-sc: input size = 92 output size = 71]
[Running-sc: input size = 98 output size = 135]
[Running-sc: input size = 104 output size = 263]
[Running-sc: input size = 110 output size = 519]
[Running-sc: input size = 116 output size = 1031]
[Running-sc: input size = 122 output size = 2055]
[Running-sc: input size = 128 output size = 4103]
[Running-sc: input size = 134 output size = 8199]
[Running-sc: input size = 140 output size = 16391]
[Running-sc: input size = 146 output size = 32775]
[Running-sc: input size = 152 output size = 65543]
[Running-sc: input size = 158 output size = 131079]
[Running-sc: input size = 164 output size = 262151]
[Running-sc: input size = 170 output size = 524295]
[Running-sc: input size = 176 output size = 1048583]
[Running-sc: input size = 182 output size = 2097159]
[Running-sc: input size = 188 output size = 4194311]
[Running-sc: input size = 194 output size = 8388615]
[Running-sc: input size = 200 output size = 16777223]

[ajreynol]

Thanks for pointing this out.

Out of curiosity, is this exponential behavior being triggered in proofs generated from cvc5? I've done some preventative measures to avoid this blowup in the cvc5 proof post-processor, although perhaps it is best to simplify the usage of this side condition altogether.

[BrunoDutertre]

Yes. This happens with real cvc5 proofs. The example above was extracted from a proof that can't be checked (even on a server with more than 200G of memory).

[BrunoDutertre]

I've hacked a memoization trick to bypass this issue. That may be good to add in general to lfscc.

[ajreynol]

The memoization is in the side condition evaluator I assume? Or is it in the construction of expressions?

[BrunoDutertre]

In the evaluator. I also used hash-consing to avoid duplicating (app ..) terms, but that was not enough.

[ajreynol]

There is a clean solution that avoids the need for this side condition altogether. I've opened https://github.com/cvc5/cvc5/pull/8699 which modifies our policy on how Skolems are defined and makes this side condition unecessary.

[BrunoDutertre]

OK. I'll give it a try.

[BrunoDutertre]

It's helping. I'm still running tests. It looks like memory usage is no longer the bottleneck, but now I see timeouts. I'll investigate more but my guess is that checks for equality (defeq) are too expensive. (Caching may help for that too and it's less hawkish than memoization of run_code :smiley:).

I'll have more data by tomorrow.

[ajreynol]

Good to hear, keep me posted. I would be interested in investigating further bottlenecks at the LFSC level.