Declare all Bool combinator equations simplifications (to disambiguate cases) #3786
Conversation
jberthold
force-pushed
the
jb/disambiguate-bool-combinator-rules
branch
from
88b593b to
2b93d97
Compare
| Note that only `andThenBool` and `orElseBool` are short-circuiting. `andBool` | ||
| and `orBool` may be short-circuited in concrete backends, but in symbolic | ||
| and `orBool` may be short-circuited in concrete backends, but in symbolic | ||
| ackends, both arguments will be evaluated. |
There was a problem hiding this comment.
As a side note, this statement about shortcut evaluation is probably not correct, given we have rules/simplifications like rule _:Bool andBool false => false that focus only on the 2nd argument.
|
...not sure why but the build was re-triggered when I edited the PR description. The first build was green so this is presumably ready for review comments. |
Comparison of timings for
|
| rule true andBool B:Bool => B:Bool [simplification] | ||
| rule B:Bool andBool true => B:Bool [simplification] | ||
| rule false andBool _:Bool => false [simplification] | ||
| rule _:Bool andBool false => false [simplification] |
There was a problem hiding this comment.
Why do we mark them all as simplification rules? I guess this is so that we will always optimistically try them, allowing any of them to apply? My intuition would be to provide a set of complete rules for booleans (non simplification), then add simplification rules as well as needed.
So maybe we have a sepraate module with a set of complete and mutually exclusive rules for boolean (for concrete simplifications)?
rule true andBool B => B
rule false andBool _ => false
rule notBool true => false
rule notBool false => true
rule true orBool _ => true
rule false orBool B => B
....
Then have this separate module with all the rules as simplificatino rules.
Maybe there should also be a way for the user to declare that this set of rules are confluent, so that the booster can just assume that?
There was a problem hiding this comment.
That would be possible, too. I don' thave a full set of measurements for it but I tested the performance for a variant where all rules that focus on the 2nd argument were declared [simplification], leaving the other rules (the ones you quote above, focussing on the 1st arg) as they were.
OTOH all these rules become obsolete as soon as a backend with an implemented hook is used. Therefore I kept all rules together in one module and made them all [simplification] for homogenous appearance.
If the variant with both simplification rules and defining equations is desired, I can change the code.
Co-authored-by: Bruce Collie <[email protected]>
This is a variant of #3786 which turns all equations that focus on the 2nd argument of a `Bool` combinator as `simplification`s. In doing this, we retain a complete set of defining equations but avoid the problem described below. Equations are kept in groups by combinator, rather than splitting them into defining and simplification equations in different modules. ------------------- Rules like this pair ``` rule false andBool _:Bool => false rule _:Bool andBool false => false ``` were previously in `BOOL-COMMON` and were said to demonstrate the implemented semantics of the hooks. As `kore-rpc-booster` does not have its own hooks, the rules now come into effect themselves. This causes issues because of the obvious overlap of rule matches (consider subject term `false andBool false` which matches both rule LHSs). This PR addresses the `kore-rpc-booster` issue by declaring some of the rules for `Bool` combinators as `simplification`s (whose application is optional - simplifications are trusted to be sound regardless of their (priority) order, whereas function equations with overlapping cases or uncertain matches lead to aborting evaluation in `kore-rpc-booster` to avoid unsoundness). Also removed some trailing whitespace from the `domains.md` file. --------- Co-authored-by: Bruce Collie <[email protected]>
|
Closed in favour of #3789 |
Rules like this pair
were previously in
BOOL-COMMONand were said to demonstrate the implemented semantics of the hooks.As
kore-rpc-boosterdoes not have its own hooks, the rules now come into effect themselves.This causes issues because of the obvious overlap of rule matches (consider subject term
false andBool falsewhich matches both rule LHSs).This PR addresses the
kore-rpc-boosterissue by declaring the rules forBoolcombinators assimplifications (whose application is optional - simplifications are trusted to be sound regardless of their (priority) order, whereas function equations with overlapping cases or uncertain matches lead to aborting evaluation inkore-rpc-boosterto avoid unsoundness).Also removed some trailing whitespace from the
domains.mdfile.