From 6ba0f3d282714fa60be2634fbdf48a8ab5a3997d Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Wed, 25 Oct 2023 21:30:31 +0200 Subject: [analysis] Add a FullLattice concept and Inverted lattice (#6038) The FullLattice concept extends the base Lattice with `getTop` and `meet` operations. The `Inverted` lattice uses these operations to reverse the order of an arbitrary full lattice, for example to create a lattice of integers ordered by `>` rather than by `<`. --- src/analysis/lattice.h | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'src/analysis/lattice.h') diff --git a/src/analysis/lattice.h b/src/analysis/lattice.h index ab75e0829..977bea0d5 100644 --- a/src/analysis/lattice.h +++ b/src/analysis/lattice.h @@ -59,9 +59,29 @@ concept Lattice = requires(const L& lattice, { lattice.join(elem, constElem) } noexcept -> std::same_as; }; +// The analysis framework only uses bottom elements and least upper bounds (i.e. +// joins) directly, so lattices do not necessarily need to implement top +// elements and greatest lower bounds (i.e. meets) to be useable, even though +// they are required for mathematical lattices. Implementing top elements and +// meets does have the benefit of making a lattice generically invertable, +// though. See lattices/inverted.h. +template +concept FullLattice = + Lattice && requires(const L& lattice, + const typename L::Element& constElem, + typename L::Element& elem) { + // Get the top element of this lattice. + { lattice.getTop() } noexcept -> std::same_as; + // Modify `elem` in-place to be the meet (aka greatest lower bound) of + // `elem` and `constEleme`, returning true iff `elem` was modified, i.e. if + // it was not already a lower bound of `constElem`. + { lattice.meet(elem, constElem) } noexcept -> std::same_as; + }; + #else // __cplusplus >= 202002L #define Lattice typename +#define FullLattice typename #endif // __cplusplus >= 202002L -- cgit v1.2.3