Fix Ac Unification error and Add new integration test

kore/src/Kore/Builtin/AssociativeCommutative.hs

@@ -803,25 +803,25 @@ unifyEqualsNormalizedAc
                             allElements1
                             allElements2
                             Nothing
-                ([opaque], []) ->
-                    lift $
-                        unifyEqualsElementLists'
-                            allElements1
-                            allElements2
-                            (Just opaque)
-                ([], [opaque]) ->
-                    lift $
-                        unifyEqualsElementLists'
-                            allElements2
-                            allElements1
-                            (Just opaque)
                 ([ElemVar_ v1], _)
+                    | null opaqueDifference2 ->
+                        lift $
+                            unifyEqualsElementLists'
+                                allElements1
+                                allElements2
+                                (Just v1)
                     | null allElements1 ->
                         unifyOpaqueVariable' v1 allElements2 opaqueDifference2
                 (_, [ElemVar_ v2])
+                    | null opaqueDifference1 ->
+                        lift $
+                            unifyEqualsElementLists'
+                                allElements2
+                                allElements1
+                                (Just v2)
                     | null allElements2 ->
                         unifyOpaqueVariable' v2 allElements1 opaqueDifference1
-                (_, _) -> empty
+                _ -> empty
             let (unifiedElements, unifierCondition) =
                     Conditional.splitTerm simpleUnifier
             lift $ do
@@ -1204,8 +1204,8 @@ unifyEqualsElementLists ::
     [ConcreteOrWithVariable normalized variable] ->
     -- | Second structure elements
     [ConcreteOrWithVariable normalized variable] ->
-    -- | Opaque part of the first structure
-    Maybe (TermLike variable) ->
+    -- | Opaque element variable of the first structure
+    Maybe (ElementVariable variable) ->
     unifier
         ( Conditional
             variable
@@ -1274,7 +1274,7 @@ unifyEqualsElementLists
     unifyEqualsChildren
     firstElements
     secondElements
-    (Just opaque)
+    (Just opaqueElemVar)
         | length firstElements > length secondElements =
             -- The second structure does not include an opaque term, so all the
             -- elements in the first structure must be matched by elements in the second
@@ -1301,26 +1301,26 @@ unifyEqualsElementLists
                         "Duplicated element in unification results"
                         first
                         second
-                Just remainderTerm -> case opaque of
-                    ElemVar_ _
-                        | TermLike.isFunctionPattern remainderTerm -> do
-                            opaqueUnifier <- unifyEqualsChildren opaque remainderTerm
-                            let (opaqueTerm, opaqueCondition) =
-                                    Pattern.splitTerm opaqueUnifier
-                                result = unifier `andCondition` opaqueCondition
-
-                            return (result, [opaqueTerm])
-                    _ ->
-                        error . show . Pretty.vsep $
-                            [ "Unification case that should be handled somewhere else: \
-                              \attempting normalized unification with a \
-                              \non-element-variable opaque term or \
-                              \non-function maps could lead to infinite loops."
-                            , Pretty.indent 2 "first="
-                            , Pretty.indent 4 (unparse first)
-                            , Pretty.indent 2 "second="
-                            , Pretty.indent 4 (unparse second)
-                            ]
+                Just remainderTerm
+                    | TermLike.isFunctionPattern remainderTerm -> do
+                        opaqueUnifier <-
+                            unifyEqualsChildren
+                                (mkElemVar opaqueElemVar)
+                                remainderTerm
+                        let (opaqueTerm, opaqueCondition) =
+                                Pattern.splitTerm opaqueUnifier
+                            result = unifier `andCondition` opaqueCondition
+                        return (result, [opaqueTerm])
+                _ ->
+                    error . show . Pretty.vsep $
+                        [ "Unification case that should be handled somewhere else: \
+                          \attempting normalized unification with \
+                          \non-function maps could lead to infinite loops."
+                        , Pretty.indent 2 "first="
+                        , Pretty.indent 4 (unparse first)
+                        , Pretty.indent 2 "second="
+                        , Pretty.indent 4 (unparse second)
+                        ]
       where
         unifyWithPermutations =
             unifyEqualsElementPermutations

kore/src/Kore/Builtin/Map.hs

@@ -499,10 +499,9 @@ internalize ::
     TermLike variable ->
     TermLike variable
 internalize tools termLike
-    | fromMaybe False (isMapSort tools sort')
-      , -- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
-        -- apply it if we know the term head is a constructor-like symbol.
-        App_ symbol _ <- termLike
+    -- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
+    -- apply it if we know the term head is a constructor-like symbol.
+    | App_ symbol _ <- termLike
       , isConstructorModulo_ symbol =
         case Ac.toNormalized @NormalizedMap termLike of
             Ac.Bottom -> TermLike.mkBottom sort'

kore/src/Kore/Builtin/Set.hs

@@ -501,10 +501,9 @@ internalize ::
     TermLike variable ->
     TermLike variable
 internalize tools termLike
-    | fromMaybe False (isSetSort tools sort')
-      , -- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
-        -- apply it if we know the term head is a constructor-like symbol.
-        App_ symbol _ <- termLike
+    -- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
+    -- apply it if we know the term head is a constructor-like symbol.
+    | App_ symbol _ <- termLike
       , isConstructorModulo_ symbol =
         case Ac.toNormalized @NormalizedSet termLike of
             Ac.Bottom -> TermLike.mkBottom sort'

test/issue-2378/Makefile

@@ -0,0 +1 @@
+include $(CURDIR)/../include.mk

test/issue-2378/test-spec.k

@@ -0,0 +1,11 @@
+module VERIFICATION
+  imports TEST
+
+endmodule
+
+module TEST-SPEC
+  imports VERIFICATION
+
+  claim b(keys(_M:Map)) => c
+
+endmodule

test/issue-2378/test-spec.k.out.golden

@@ -0,0 +1,16 @@
+  #Not ( #Exists _0 . #Exists S . {
+    keys ( _M )
+  #Equals
+    S
+    SetItem ( _0 )
+  } )
+#And
+  #Not ( {
+    .Set
+  #Equals
+    keys ( _M )
+  } )
+#And
+  <k>
+    b ( keys ( _M ) ) ~> _DotVar1 ~> .
+  </k>

test/issue-2378/test.k

@@ -0,0 +1,14 @@
+// Copyright (c) 2020 K Team. All Rights Reserved.
+
+module TEST
+  imports SET
+  imports MAP
+
+  syntax B  ::= b(Set)
+            | "c"
+  syntax KItem ::= B
+
+  rule b(.Set) => c
+  rule b(SetItem(_:KItem) S:Set) => b(S)
+
+endmodule