search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 60 forks source link

refactor Set->Array elaboration #696

Closed clayrat closed 1 month ago

clayrat commented 2 months ago

This PR compacts multiple local sort coercions introduced in #688 (currently for Set->Array, upcoming PR will also add Bag/Map->Array coercions) into a few recursive coercions on the arguments passed to instances of Elaborate and Checkable type classes. This reduces the possibility of some code paths not being covered by necessary coercions, e.g. when using PLE.

Additionally, this PR adds a more intuitive synonym --ple for --rewriteaxioms command line key that enables PLE.

Lastly, there's a change in the way errors are reported in Language.Fixpoint.Solver.crashResult - previously this function would only display a generic Sorry, unexpected panic in liquid-fixpoint! error message if its error argument could not be found in the supplied ErrorMap; after the change this message will contain all available information, making debugging easier.

clayrat commented 2 months ago

Added performance charts to https://github.com/ucsd-progsys/liquidhaskell/pull/2302. It seems we have significant slowdowns in ~5 tests, out of which esop2013, bytestring, vector-algorithms have large SMT encodings (10-100s Mb) and ListSetDemo is the only one actually using a Set encoding.

clayrat commented 2 months ago

I've added an environment coercion to isUnsat to fix an SMT serialization error triggered in the new test added to LH; I haven't encountered this in any other test before.