While runtimeverification/haskell-backend#3779 is concerned with rewrite rules (and relatively straightforward), collecting #Ceil conditions introduced by simplifications and function-defining equations is complex because of
possible recursive evaluation of side conditions - the collected #Ceil conditions may have to be discarded if the recursive caller ends up failing for other reasons
when the #Ceil condition comes from simplifying a rewrite rule side condition, the negated condition becomes a remainder and rewriting needs to proceed with this remainder added to the assumed condition (unless it can be pruned - has to be simplified "soon"). This potentially leads to branching.
This extension is expected to considerably reduce the fall-back cases because many more simplifications can be applied.
While runtimeverification/haskell-backend#3779 is concerned with rewrite rules (and relatively straightforward), collecting
#Ceil
conditions introduced by simplifications and function-defining equations is complex because of#Ceil
conditions may have to be discarded if the recursive caller ends up failing for other reasons#Ceil
condition comes from simplifying a rewrite rule side condition, the negated condition becomes a remainder and rewriting needs to proceed with this remainder added to the assumed condition (unless it can be pruned - has to be simplified "soon"). This potentially leads to branching.This extension is expected to considerably reduce the fall-back cases because many more simplifications can be applied.