Theory.Tools.LoopBreakers

Computate the loop-breakers in the premise-conclusion graph of a set of multiset rewriting rules.

Computing loop breakers for solving premises

useAutoLoopBreakersAC

Arguments

:: Ord a

=> (a -> [(PremIdx, LNFact)])

Enumerate premises

-> (a -> [(ConcIdx, LNFact)])

Enumerate conclusions

-> (a -> [LNSubstVFresh])

Enumerate variants

-> ([PremIdx] -> a -> a)

Add annotation

-> [a]

Original rules

-> WithMaude ([a], Relation (a, PremIdx), [(a, PremIdx)])

Annotated rules and the premise solving relation

Replace all loop-breaker information with loop-breakers computed automatically from the dataflow relation dataflowRelAC.