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

add internal Array theory, elaborate Set theory into it #688

Closed clayrat closed 4 months ago

clayrat commented 4 months ago

Fixes https://github.com/ucsd-progsys/liquidhaskell/issues/2272 by elaborating Set operations into Array operations which are "internally" polymorphic in Z3.

Currently, this only touches Sets but presumably Maps also need to undergo the same treatment.

clayrat commented 4 months ago

Performance charts (on LH test suite):

bot top filtered

facundominguez commented 4 months ago

by elaborating Set operations into Array operations which are "internally" polymorphic in Z3

Might require documentation: Does this PR narrow in some way the list of SMT solvers that LH/LF can work with?

clayrat commented 4 months ago

Might require documentation: Does this PR narrow in some way the list of SMT solvers that LH/LF can work with?

This uses the same SMTLIBv2-compliant ArraysEx theory encoding as before, we're just now inlining the definitions so that the LF elaborator can produce local signatures instead of hardcoding all Sets to be Array Int Bool. So in theory all the solvers that support SMTLIBv2 should still keep working.

However, the concern that by now we're pretty much vendor-locked into Z3 is valid; I've tried running the .smt files produced by LF even before this PR through CVC5 and failed; investigating this is our next step (after converting the Map theory to use Arrays as well).

clayrat commented 4 months ago

Looks good to me! But does it come with a relevant LH pull request to ensure that it does not break any tests?

The tests pass successfully after adapting LH to the develop branch: https://github.com/ucsd-progsys/liquidhaskell/pull/2282

nikivazou commented 4 months ago

@ranjitjhala we can merge this tomorrow (just checking it does not break flux or anything else)

ranjitjhala commented 4 months ago

Yes please merge, thanks @nikivazou and @clayrat -- this is a really huge step!!!

ranjitjhala commented 4 months ago

[I think its a big enough change to warrant a version number bump?]

nikivazou commented 4 months ago

Alex wants to apply the same inlining for Maps (for uniformity) so we can change the version number after this pending edit.