Unfold with undecided guards in PLE when new equalities are discovered

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types

BSD 3-Clause "New" or "Revised" License

141 stars 61 forks source link

Unfold with undecided guards in PLE when new equalities are discovered #716

Closed facundominguez closed 2 weeks ago

facundominguez commented 2 weeks ago

Merged this too soon. tests/ple/pos/Permutations.hs is the only test dramatically slowing down from 6 seconds to 18 seconds. I'm benchmarking an alternative fix.