Syntactic constraint filtering for equations/simplifications

Here, in this analysis: https://gist.github.com/jberthold/fc7b27699c1708cb34aceb1c8e4ec381#indeterminate-conditions-in-jumps, we've identified that perhaps recursive constraint evaluation for equational side conditions would help to avoid aborts in many cases.

In fact, it seems that the vast majority of the cases actually are #rangeUInt(W, X) predicates, which always simplify down to 0 <=Int X andBool X <Int (2 ^Int W) (as a macro, so the backend will not see the #rangeUINt or the ^Int symbols.

These constraints (0 <=Int X and X <Int ...), should always show up exactly syntactically in the existing path condition. So rather than full recursive equation evaluation, we can have a much faster first pass which may result in many pruned paths (and thus no need to invoke SMT solver or old backend in those cases). We can still later (if deemed necessary) have full recursive constraint evaluation for equations, but if the faster pass results in pruning a branch, then we are done and don't need that extra work.

What I propose to try: instantiate the equations conjuncts with the substitution from the LHS of the equation applying, and ese if each conjunct shows up exactly syntactically in the current path condition already. If all of them do show up exactly syntactically in the current path condition, then the equations side conditions are valid and the equation can be applied. We still need to apply all the logic about priorities of equations and multiple equations applying, but it should unlock more very simple simplificatinos directly in th ebooster, for example these ones: https://github.com/runtimeverification/evm-semantics/blob/1349ef9203534b80bd52577637060ceb5d4e0d24/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k#L56

runtimeverification / hs-backend-booster

Syntactic constraint filtering for equations/simplifications #433