Expressions for the SMT solver grow with the path length

[facundominguez]

Roughly, each rewrite that REST applies has a constraint that states whether there is some ordering that can ensure termination, which avoids infinite sequences of rewrites. The constraint for each rewrite is in turn constructed from the constraints of earlier rewrites via the refine method of ordering constraint algebras.

The sequence of constraints look as

C0, refine(C0, t0, t1), refine(refine(C0, t0, t1), t1, t2), refine(refine(refine(C0, t0, t1), t1, t2), t2, t3), ...

Perhaps it is evident from the above sequence that if not careful, C0 and refine(C0, t0, t1) will be sent multiple times to the SMT solver as sub-expressions of larger and larger constraints. This adds up to a quadratic communication protocol with the SMT solver as the length of the sequence grows. I've observed this when debugging some tests after refactorings in ucsd-progsys/liquid-fixpoint#500.

Ideally, C0 would be defined as a constant, and then refine(C0, t0, t1) would be defined as a constant, and so every ordering constraint that is ever concocted, so instead of writing the above sequence we write

(define-fun R0 () Bool C0)
(define-fun R1 () Bool (refine(R0, t0, t1)))
(define-fun R2 () Bool (refine(R1, t1, t2)))
(define-fun R3 () Bool (refine(R2, t2, t3)))
...

and the sequence of constraints becomes

R0, R1, R2, R3, ...

and so we keep the size of our expressions bounded.

[zgrannan]

@facundominguez I think this solution is do-able technically, although it would require a bit of engineering.

Another approach to consider would be to attempt to simplify the constraints. I think currently the SMT expressions being generated contain clauses that can be simplified (for example f > g and f > g should be f > g, and f > g and g > h and f > h) should be f > g and g > h). I don't have data to back this up, but I suspect that in many cases the refine operation should not generate a larger formula (in fact sometimes it could be smaller).

The implementation of constraints used in LiquidHaskell (and the one that has best results so far) is represented as an ADT describing constraints on well-quasi-orders, here: https://github.com/zgrannan/rest/blob/master/src/Language/REST/WQOConstraints/ADT.hs. The existing optimization steps help a bit but I suspect there is more that can be done.