4100 Abort booster rewrite when matching subject variables

As demonstrated in #4100, booster should not report `stuck` when attempting to rewrite a term with variables that are required in a rule match.
Specifically, a subject variable may lead to branching with the rule content matches ending up as path conditions in the different branches.

Previously, booster would discard such cases as match failures and report `stuck` since no rule was applied.
This PR changes the behaviour to aborting the rewrite when a subject variable needs to be matched by anything but a rule variable.

Author: jberthold

booster/library/Booster/Pattern/Match.hs

@@ -216,9 +216,10 @@ match1 _       t1@DomainValue{}                           t2@KSet{}
 match1 _       t1@DomainValue{}                           t2@ConsApplication{}                       = failWith $ DifferentSymbols t1 t2
 match1 _       t1@DomainValue{}                           t2@FunctionApplication{}                   = addIndeterminate t1 t2
 -- match with var on the RHS must be indeterminate when evaluating functions. see: https://github.com/runtimeverification/hs-backend-booster/issues/231
+match1 Eval    t1@DomainValue{}                           t2@Var{}                                   = addIndeterminate t1 t2
+-- match with var on RHS is specially marked at the moment but must abort the rewriting (or lead to branching), see https://github.com/runtimeverification/haskell-backend/issues/4100
 match1 Rewrite t1@DomainValue{}                           (Var t2)                                   = failWith $ SubjectVariableMatch t1 t2
 match1 Implies t1@DomainValue{}                           (Var t2)                                   = failWith $ SubjectVariableMatch t1 t2
-match1 Eval    t1@DomainValue{}                           t2@Var{}                                   = addIndeterminate t1 t2
 match1 Eval    t1@Injection{}                             t2@AndTerm{}                               = addIndeterminate t1 t2
 match1 _       t1@Injection{}                             (AndTerm t2a t2b)                          = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
 match1 _       t1@Injection{}                             t2@DomainValue{}                           = failWith $ DifferentSymbols t1 t2
@@ -228,6 +229,7 @@ match1 _       t1@Injection{}                             t2@KList{}
 match1 _       t1@Injection{}                             t2@KSet{}                                  = failWith $ DifferentSymbols t1 t2
 match1 _       t1@Injection{}                             t2@ConsApplication{}                       = failWith $ DifferentSymbols t1 t2
 match1 _       t1@Injection{}                             t2@FunctionApplication{}                   = addIndeterminate t1 t2
+match1 Rewrite t1@Injection{}                             (Var t2)                                   = failWith $ SubjectVariableMatch t1 t2
 match1 _       t1@Injection{}                             t2@Var{}                                   = addIndeterminate t1 t2
 match1 Eval    t1@KMap{}                                  t2@AndTerm{}                               = addIndeterminate t1 t2
 match1 _       t1@KMap{}                                  (AndTerm t2a t2b)                          = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b

booster/library/Booster/Pattern/Rewrite.hs

@@ -64,7 +64,7 @@ import Booster.Pattern.Base
 import Booster.Pattern.Bool
 import Booster.Pattern.Index qualified as Idx
 import Booster.Pattern.Match (
-    FailReason (ArgLengthsDiffer, SubsortingError),
+    FailReason (ArgLengthsDiffer, SubjectVariableMatch, SubsortingError),
     MatchResult (MatchFailed, MatchIndeterminate, MatchSuccess),
     MatchType (Rewrite),
     SortError,
@@ -392,6 +392,10 @@ applyRule pat@Pattern{ceilConditions} rule =
                             withContext CtxError $
                                 logPretty' @mods err
                             failRewrite $ InternalMatchError $ renderText $ pretty' @mods err
+                        MatchFailed err@(SubjectVariableMatch t v) -> do
+                            withContext CtxError $
+                                logPretty' @mods err
+                            failRewrite $ RuleApplicationUnclear rule pat.term $ NE.singleton (t, Var v)
                         MatchFailed reason -> do
                             withContext CtxFailure $ logPretty' @mods reason
                             returnNotApplied

booster/unit-tests/Test/Booster/Pattern/Rewrite.hs

@@ -41,7 +41,7 @@ test_rewriteStep =
         "Rewriting"
         [ errorCases
         , rewriteSuccess
-        , unifyNotMatch
+        , subjectVariables
         , definednessUnclear
         , rewriteStuck
         , rulePriority
@@ -176,7 +176,7 @@ testConf = do
 ----------------------------------------
 errorCases
     , rewriteSuccess
-    , unifyNotMatch
+    , subjectVariables
     , definednessUnclear
     , rewriteStuck
     , rulePriority ::
@@ -207,10 +207,11 @@ rewriteSuccess =
             `rewritesTo` ( "con1-f1"
                          , [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}(   \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
                          )
-unifyNotMatch =
-    testCase "Stuck case when subject has variables" $
-        getsStuck
-            [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( X:SomeSort{}, \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
+subjectVariables =
+    testCase "Aborts case when subject has variables" $ do
+        let t = [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( X:SomeSort{}, \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
+        t `failsWith`
+            RuleApplicationUnclear rule3 t (NE.singleton ([trm| \dv{SomeSort{}}("otherThing")|], [trm| X:SomeSort{} |]))
 definednessUnclear =
     testCase "con4 rewrite to f2 might become undefined" $ do
         let pcon4 =