Compute remainders in booster

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

The 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

Start by reading the remainder design document at docs/2019-08-29-Remainders-for-priority-rules.md and the related issue #3948, then inspect the booster remainder-handling paths. The work is complete when booster handles the listed indeterminate matches, definedness failures, and unresolved requires clauses without aborting or falling back to kore, including the priority-rule behavior still noted as incomplete.