Make the "simplify" endpoint in Booster evaluate inconsisten predicates and patterns to #Bottom

[geo2a]

The "simplify" endpoint in Booster, is different from what Kore does. When asked to simplify the state state-vacuous-but-rewritten.execute:

Term:
    <generatedTop>(
        <k>(kseq("b", dotk())),
        <int>(N:SortInt{}),
        <generatedCounter>("0")
    )
Conditions:
    _=/=Int_(N:SortInt{}, "0")
    _==Int_(N:SortInt{}, "0")

which is a pattern with contradictory constraints, booster-dev returns the pattern almost unchanged:

Term:
    <generatedTop>(
        <k>(kseq("b", dotk())),
        <int>(N:SortInt{}),
        <generatedCounter>("0")
    )
Conditions:
    _==Int_(N:SortInt{}, "0")
    notBool_(_==Int_(N:SortInt{}, "0"))

while kore-rpc-booster will return #Bottom (via Kore):

[request 1][proxy][timing] Performed SimplifyM in 0.45s (0.41s kore time)
[request 1][proxy][abort][detail] Kore simplification: Diff (< before - > after)
*** /tmp/extra-dir-51565986628734/diff_file1.txt	2024-08-01 08:37:36.610508904 +0200
--- /tmp/extra-dir-51565986628734/diff_file2.txt	2024-08-01 08:37:36.610508904 +0200
***************
*** 1,9 ****
- Term:
-     <generatedTop>(
-         <k>(kseq("b", dotk())),
-         <int>(N:SortInt{}),
-         <generatedCounter>("0")
-     )
  Conditions:
!     _==Int_(N:SortInt{}, "0")
!     notBool_(_==Int_(N:SortInt{}, "0"))
\ No newline at end of file
--- 1,4 ----
  Conditions:
! Ceil conditions:
! Substitutions:Unsupported parts:
! {"sort":{"args":[],"name":"SortGeneratedTopCell","tag":"SortApp"},"tag":"Bottom"}

that means that ApplyEquations.evaluatePattern --- the function behind the "simplify" endpoint in Booster, is unable to detect a contradiction in constraints. And this is indeed the case, since it evaluates every constraint assuming all the others, but never calls Z3 on them together as we do when rewriting.

Same happens if we isolate the constraints and ask the servers to simplify that:

request 1][proxy][timing] Performed SimplifyM in 0.49s (0.47s kore time)
[request 1][proxy][abort][detail] Kore simplification: Diff (< before - > after)
*** /tmp/extra-dir-51565986628735/diff_file1.txt	2024-08-01 08:40:47.352321295 +0200
--- /tmp/extra-dir-51565986628735/diff_file2.txt	2024-08-01 08:40:47.352321295 +0200
***************
*** 1,5 ****
  Conditions:
-     _==Int_(N:SortInt{}, "0")
-     notBool_(_==Int_(N:SortInt{}, "0"))
  Ceil conditions:
! Substitutions:
\ No newline at end of file
--- 1,4 ----
  Conditions:
  Ceil conditions:
! Substitutions:Unsupported parts:
! {"sort":{"args":[],"name":"SortGeneratedTopCell","tag":"SortApp"},"tag":"Bottom"}

and indeed, the "simplify" endpoint, when it receives predicates only, simplifies them in isolation and never checks their combined consistency.

I understand that this behaviour of the "simplify" endpoint in Booster is intentional, since, for most of its lifetime, Booster did not have an SMT solver and thus we've geared to towards simplifying constraints in isolation. It's time to change that.