The booster simplification cache currently does not save the path condition for stored term simplifications.
This is still sound (function equations with undecided requires clauses abort the evaluation, simplifications are optional) but booster may miss opportunities to simplifiy terms using newly-acquired facts (from ensures clauses of applied rewrite rules).
In the simplest implementation, the simplification cache would be purged every time a new ensures clause is added to the path condition.
The path condition could be stored together with the result term, and the result re-verified if a new ensures clause has been added to the path condition (in an attempt to not throw the entire cache away). It is unclear how exactly this could be achieved.
This is especially important for terms that were found to be unsimplifiable with a given path condition. A new addition to the path condition could enable simplifications.
More elaborate experiments could involve storing a list of path conditions (hashes thereof, for instance) for which the simplification is known to hold.
The booster simplification cache currently does not save the path condition for stored term simplifications. This is still sound (function equations with undecided
requiresclauses abort the evaluation, simplifications are optional) butboostermay miss opportunities to simplifiy terms using newly-acquired facts (fromensuresclauses of applied rewrite rules).ensuresclause is added to the path condition.ensuresclause has been added to the path condition (in an attempt to not throw the entire cache away). It is unclear how exactly this could be achieved.