Various issues with remainders have been identified in kore recently see #3948. These issues should not be addressed in kore due to various reasons, including kore not being actively maintained and the difficulties associated with reasoning/debugging of the kore backend. Instead, we need to implement remainder computation in booster where we can then more efficiently explore various optimisations suggested in the aforementioned issue. This issue should serve as the design document for implementing the remainder computation algorithm.
Currently, the booster aborts in the following scenarios and what i think we should do:
when the match is indeterminate, e.g. matching C(...) with f(...) where f is a function and C is a constructor (only aborts if this happens after a round of configuration simplification)
action: split the current state by
adding C(...) == f(...) to path constraints and continue with current rule and then try all remaining rules
adding C(...) =/= f(...) to path constraints and then try all remaining rules
rule does not preserve definedness
action: add #Ceil(<term>) to path conditions for the sub<term> which does not preserve definedness and continue
requires clause C could not be determined to be true
action: split the current state by
adding C to path constraints and continue with current rule and then try all remaining rules
adding notBool C to path constraints and then try all remaining rules
Various issues with remainders have been identified in kore recently see #3948. These issues should not be addressed in kore due to various reasons, including kore not being actively maintained and the difficulties associated with reasoning/debugging of the kore backend. Instead, we need to implement remainder computation in booster where we can then more efficiently explore various optimisations suggested in the aforementioned issue. This issue should serve as the design document for implementing the remainder computation algorithm.
Currently, the booster aborts in the following scenarios and what i think we should do:
C(...)withf(...)wherefis a function andCis a constructor (only aborts if this happens after a round of configuration simplification) action: split the current state byC(...) == f(...)to path constraints and continue with current rule and then try all remaining rulesC(...) =/= f(...)to path constraints and then try all remaining rulesadd #Ceil(<term>)to path conditions for the sub<term>which does not preserve definedness and continueCcould not be determined to be true action: split the current state byCto path constraints and continue with current rule and then try all remaining rulesnotBool Cto path constraints and then try all remaining rulesThe changes above should mean we no longer abort and fall back to kore. However, this design is still incomplete/incorrect in the face of applying multiple rules with different priorities: https://github.com/runtimeverification/haskell-backend/blob/master/docs/2019-08-29-Remainders-for-priority-rules.md