Simplification - Improvement Proposals

[ana-pantilie]

One major component of the Haskell backend is the simplifier. It takes care of:

• function evaluation
• lemma application (simplification rules)
• ML reasoning, simplifying predicates to some normalized form
• sending predicates to the SMT solver

We'd like to know what users' experiences with the simplifier are and what changes they would like to see.

Any ideas are welcome, so feel free to "think big". For example, I would like to be able to step through the simplification procedure, like a "functional" kore-repl.

[hjorthjort]

I would like to be able to quickly test if a simplification applies to an expression. From a user perspective, being able to click on a subexpression in my configuration, and then write a simplification for it and see if it applies, then being able to go back to the original configuration and see if it applies would be magnificent.

On the backend side I suspect this means being able to:

• store a point of execution
• inject a new simplification into the set of simplification rules
• run the simplifier on a subexpression only
• go back to the original configuration with ease
• ... and switch back and forth in this way

Essentially, being able to inject, manipulate and store points of execution and rules, in a way that is reliable and makes it easy to try things out, roll back, etc.

[PetarMax]

Branching on function rules

See runtimeverification/k#3108 (comment).