Preserve clause ordering of requires and ensures when internalisig rules
#4028
Assignees
Comments
goodlyrottenapple
added a commit
that referenced
this issue
Aug 19, 2024
…g rules in booster (#4037) Fixes #4028 --------- Co-authored-by: github-actions <[email protected]>
rv-jenkins
added a commit
that referenced
this issue
Aug 19, 2024
Follow up to #4028, which further cleans up the code-base by removing internalisation of anti-left rules, as these are: a) unused for over a year now (since #3391) b) the previous PR essentially left the inernalisation of anti-left broken, but we wanted to remove it fully in a separate PR for ease of review. --------- Co-authored-by: rv-jenkins <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
To enable syntactic simplifications, Booster's internal representation of simplification rules must store the rule's
requiresclause as an ordered collection, and preserver the user-specified order of conjuncts (subterms if_andBool_).Currently, we internalise rules' LHS and RHS as
Patterns. Therequires/ensuresclause is then taken to be the patterns' constrains, which are aSet. Moreover, theinternalisePredicatesfunction also returns aSet.We may have to decouple the internalisation routines for rules and patterns a little more to implement this.
The text was updated successfully, but these errors were encountered: