Allow conditional rewriting

taktoa commented 6 years ago

Using the techniques described in From Conditional to Unconditional Rewriting by Grigore Roşu, we should be able to convert a conditional TRS (term-rewriting system) into an unconditional TRS, allowing us to expose an API that allows conditional rewriting without changing anything about our current matching or rewriting algorithms. This would probably be fairly useful in writing axioms, so we should support it.

[ ] Figure out how the Equation type should change to support conditional rewriting rules.
[ ] Read the papers and investigate which algorithm makes the most sense for our application.
[ ] Implement the algorithm.

EDIT: another related paper by the same research group

taktoa commented 6 years ago

Another bonus associated with this feature: it will make it much easier to use this library in optimizing code in languages specified in the K Framework.

taktoa commented 6 years ago

This also seems relevant to implementing the false/true sections of an axiom definition as defined around page 26 (PDF page 44) of the thesis.

taktoa / eqsat

Allow conditional rewriting #1