search

ucsd-progsys / liquid-fixpoint

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

Split out Bag theory, elaborate Maps and Bags into Arrays #703

Closed clayrat closed 2 months ago

clayrat commented 2 months ago

As a continuation of https://github.com/ucsd-progsys/liquid-fixpoint/pull/688, this PR elaborates Map operations into Array ones, allowing for the correct handling of polymorphic Map values.

It also separates Bags (i.e., integer-valued maps) from generic Maps and removes some ad-hoc Map operations that are currently only implementable as Z3 lambdas (prj, shift and to_set). This is a precursor to adding CVC5 support, as the latter does not support arbitrary Array operations, but instead has a generic SMTLIB Array theory (with const, store and select) and separate theories of Sets and Bags.

clayrat commented 2 months ago

For the reference, the Map operations we're removing here were first introduced in https://github.com/ucsd-progsys/liquid-fixpoint/pull/624