runtimeverification / pyk

Python tools for the K Framework
BSD 3-Clause "New" or "Revised" License
13 stars 2 forks source link

Add class `POSet` #991

Closed tothtamas28 closed 6 months ago

tothtamas28 commented 6 months ago

Adds a class POSet that takes a binary relation, computes it's transitive closure and stores the image of the resulting relation. The sort ordering is re-implemented to use POSet for both KAST and KORE.

Note that technically, that the name Proset would be more fitting for the current implementation as neither antisymmetry, nor asymmetry is enforced. (Reflexivity isn't either, but that's easy to work around.)