Simplify right-hand side of claims

kore/src/Kore/Strategies/Goal.hs

@@ -846,16 +846,33 @@ simplify'
     => Lens' goal ClaimPattern
     -> goal
     -> Strategy.TransitionT (AppliedRule goal) m goal
-simplify' lensClaimPattern =
-    Lens.traverseOf (lensClaimPattern . field @"left") $ \config -> do
-        let definedConfig =
-                Pattern.andCondition (mkDefined <$> config)
-                $ from $ makeCeilPredicate_ (Conditional.term config)
-        configs <-
-            simplifyTopConfiguration definedConfig
-            >>= SMT.Evaluator.filterMultiOr
-            & lift
-        Foldable.asum (pure <$> configs)
+simplify' lensClaimPattern goal = do
+    goal' <- simplifyLeftHandSide goal
+    let sideCondition = extractSideCondition goal'
+    simplifyRightHandSide sideCondition goal'
+  where
+    extractSideCondition =
+        SideCondition.assumeTrueCondition
+        . Pattern.withoutTerm
+        . Lens.view (lensClaimPattern . field @"left")
+
+    simplifyLeftHandSide =
+        Lens.traverseOf (lensClaimPattern . field @"left") $ \config -> do
+            let definedConfig =
+                    Pattern.andCondition (mkDefined <$> config)
+                    $ from $ makeCeilPredicate_ (Conditional.term config)
+            configs <-
+                simplifyTopConfiguration definedConfig
+                >>= SMT.Evaluator.filterMultiOr
+                & lift
+            Foldable.asum (pure <$> configs)
+
+    simplifyRightHandSide sideCondition =
+        Lens.traverseOf (lensClaimPattern . field @"right") $ \dest ->
+            OrPattern.observeAllT
+            $ Logic.scatter dest
+            >>= Pattern.simplify sideCondition
+            >>= Logic.scatter
 
 isTriviallyValid' :: Lens' goal ClaimPattern -> goal -> Bool
 isTriviallyValid' lensClaimPattern =

test/all-path/00-basic/01-one-rule/all-path-b-or-c-spec.k

@@ -7,7 +7,6 @@ module ALL-PATH-B-OR-C-SPEC
   import PATH
 
   // This should be provable as transiting to b suffices
-  // TODO (#1278): ... => ?X ensures ?X ==K b orBool ?X ==K c
   rule <k> a => b #Or c </k> [all-path]
 
 endmodule

test/all-path/03-unification/set-select/all-path-b-or-c-spec.k

@@ -7,7 +7,6 @@ module ALL-PATH-B-OR-C-SPEC
   imports VERIFICATION
   imports PATH
 
-  // TODO (#1278): ... => ?X ensures ?X ==K b orBool ?X ==K c
   rule <k> select => b #Or c </k>
        <state> SetItem(b) SetItem(c) </state>
     [all-path]

test/all-path/03-unification/set-select/one-path-b-or-c-spec.k

@@ -7,7 +7,6 @@ module ONE-PATH-B-OR-C-SPEC
   imports VERIFICATION
   imports PATH
 
-  // TODO (#1278): ... => ?X ensures ?X ==K b orBool ?X ==K c
   rule <k> select => b #Or c </k>
        <state> SetItem(b) SetItem(c) </state>
     [one-path]

test/simplify-rhs/Makefile

@@ -0,0 +1,2 @@
+DEF = test
+include $(CURDIR)/../include.mk

test/simplify-rhs/test-1-repl-script-spec.k

@@ -0,0 +1,11 @@
+module VERIFICATION
+    imports TEST
+
+endmodule
+
+module TEST-1-REPL-SCRIPT-SPEC
+    imports VERIFICATION
+
+    rule a => f(c)
+
+endmodule

test/simplify-rhs/test-1-repl-script-spec.k.out.golden

@@ -0,0 +1,10 @@
+Kore (0)> ProveSteps 1
+    #Top
+  #And
+    <k>
+      evaluated ~> _DotVar1 ~> .
+    </k>
+#Implies
+  #wAF ( <k>
+    evaluated ~> _DotVar1 ~> .
+  </k> )

test/simplify-rhs/test-1-repl-script-spec.k.repl

@@ -0,0 +1 @@
+step

test/simplify-rhs/test.k

@@ -0,0 +1,10 @@
+module TEST
+
+    syntax S ::= "a" | "b" | "c" | "evaluated"
+               | f(S) [function]
+
+    rule f(_:S) => evaluated
+
+    rule a => f(b)
+
+endmodule