search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
204 stars 39 forks source link

NOT READY Compute syntactic transitive closure for select relational symbols #3940

Closed geo2a closed 2 weeks ago

geo2a commented 2 weeks ago

Related to https://github.com/runtimeverification/haskell-backend/issues/3861

This PR adds a routine to compute a syntactic transitive closure if a certain relational symbol in a given set of applications of this symbol.

See module Booster.Pattern.PartialOrder for the implementation and [Test.Booster.Pattern.PartialOrder(https://github.com/runtimeverification/haskell-backend/blob/georgy%2Fpartial-order-transitive-closure/booster/unit-tests/Test/Booster/Pattern/PartialOrder.hs#L13) for the unit-tests.

Application

This routine, in conjunction with syntactic inference of requires from the path condition, should allow us to solve some side-conditions completely syntactically, i.e. without calling the SMT solver or event the applying equations.

geo2a commented 2 weeks ago

Opened this draft too early.