Do not ignore antiLeft if argument is Nothing (#2366)

* Do not ignore antiLeft if argument is Nothing

* Add integration test

Author: ana-pantilie

kore/src/Kore/Equation/Application.hs

@@ -158,28 +158,7 @@ attemptEquation
 attemptEquation sideCondition termLike equation =
     whileDebugAttemptEquation' $ runExceptT $ do
         let Equation { left, argument, antiLeft } = equationRenamed
-        (equation', predicate) <-
-            case argument of
-                Nothing -> do
-                    matchResult <- match left termLike & whileMatch
-                    applyMatchResult equationRenamed matchResult
-                        & whileApplyMatchResult
-                Just argument' -> do
-                    (matchPredicate, matchSubstitution) <-
-                        match left termLike
-                        & whileMatch
-                    matchResults <-
-                        applySubstitutionAndSimplify
-                            argument'
-                            antiLeft
-                            matchSubstitution
-                        & whileMatch
-                    (equation', predicate) <-
-                        applyAndSelectMatchResult matchResults
-                    return
-                        ( equation'
-                        , makeAndPredicate predicate matchPredicate
-                        )
+        (equation', predicate) <- matchAndApplyResults left argument antiLeft
         let Equation { requires } = equation'
         checkRequires sideCondition predicate requires & whileCheckRequires
         let Equation { right, ensures } = equation'
@@ -195,6 +174,29 @@ attemptEquation sideCondition termLike equation =
         matchIncremental term1 term2
         & MaybeT & noteT matchError
 
+    matchAndApplyResults left' argument' antiLeft'
+      | isNothing argument'
+      , isNothing antiLeft' = do
+          matchResult <- match left' termLike & whileMatch
+          applyMatchResult equationRenamed matchResult
+              & whileApplyMatchResult
+      | otherwise = do
+          (matchPredicate, matchSubstitution) <-
+              match left' termLike
+              & whileMatch
+          matchResults <-
+              applySubstitutionAndSimplify
+                  argument'
+                  antiLeft'
+                  matchSubstitution
+              & whileMatch
+          (equation', predicate) <-
+              applyAndSelectMatchResult matchResults
+          return
+              ( equation'
+              , makeAndPredicate predicate matchPredicate
+              )
+
     applyAndSelectMatchResult
         :: [MatchResult variable]
         -> ExceptT
@@ -227,7 +229,7 @@ applySubstitutionAndSimplify
     :: HasCallStack
     => MonadSimplify simplifier
     => InternalVariable variable
-    => Predicate variable
+    => Maybe (Predicate variable)
     -> Maybe (Predicate variable)
     -> Map (SomeVariableName variable) (TermLike variable)
     -> ExceptT
@@ -244,7 +246,7 @@ applySubstitutionAndSimplify
                 (predicate, Substitution.toMap substitution)
         Substitution.mergePredicatesAndSubstitutions
             SideCondition.top
-            (argument : maybeToList antiLeft)
+            (maybeToList argument <> maybeToList antiLeft)
             [from @_ @(Substitution _) matchSubstitution]
             & Logic.observeAllT
             & (fmap . fmap) toMatchResult

kore/test/Test/Kore/Equation/Application.hs

@@ -501,7 +501,7 @@ test_applySubstitutionAndSimplify =
                 )
         (Right [actual]) <-
             applySubstitutionAndSimplify
-                mockArgument
+                (Just mockArgument)
                 Nothing
                 mempty
             & runExceptT

test/priority/priority-1-spec.k

@@ -0,0 +1,17 @@
+module VERIFICATION
+    imports PRIORITY
+
+    syntax KItem ::= runTest  ( S )
+                   | doneTest ( S )
+
+    rule runTest ( T ) => doneTest ( T )
+
+endmodule
+
+module PRIORITY-1-SPEC
+    imports VERIFICATION
+
+    // This claim should not be provable.
+    claim <k> runTest ( func4(X:Int) ) => doneTest ( seven ) ... </k>
+
+endmodule

test/priority/priority-1-spec.k.out.golden

@@ -0,0 +1,11 @@
+  #Ceil ( func4 ( X ) )
+#And
+  #Not ( {
+    seven
+  #Equals
+    func4 ( X )
+  } )
+#And
+  <k>
+    doneTest ( func4 ( X ) ) ~> _DotVar1 ~> .
+  </k>

test/priority/priority.k

@@ -33,4 +33,9 @@ module PRIORITY
   rule func3(6)     => six
   rule func3(_:Int) => seven  [owise]
 
+  syntax S ::= func4(Int)     [function]
+  rule func4(X:Int) => four
+    requires func3(X) ==K four
+  rule func4(_:Int) => seven  [owise]
+
 endmodule