Symbolic rules for SET.in

kore/src/Kore/Builtin/Map.hs

@@ -36,7 +36,6 @@ import Control.Error
     , runMaybeT
     )
 import qualified Control.Monad as Monad
-import qualified Data.Foldable as Foldable
 import qualified Data.HashMap.Strict as HashMap
 import Data.Map.Strict
     ( Map
@@ -64,25 +63,21 @@ import qualified Kore.Builtin.Builtin as Builtin
 import qualified Kore.Builtin.Int as Int
 import qualified Kore.Builtin.List as Builtin.List
 import qualified Kore.Builtin.Map.Map as Map
-import qualified Kore.Builtin.Set as Builtin.Set
+import qualified Kore.Builtin.Set as Set
 import qualified Kore.Domain.Builtin as Domain
 import Kore.IndexedModule.MetadataTools
     ( SmtMetadataTools
     )
 import qualified Kore.Internal.Condition as Condition
-import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
-    ( Condition
-    , Pattern
+    ( Pattern
     )
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( makeCeilPredicate
     )
-import qualified Kore.Internal.SideCondition as SideCondition
 import Kore.Internal.Symbol
-    ( Symbol (..)
-    , symbolHook
+    ( symbolHook
     )
 import Kore.Internal.TermLike
     ( pattern App_
@@ -94,7 +89,6 @@ import qualified Kore.Internal.TermLike as TermLike
 import Kore.Sort
     ( Sort
     )
-import qualified Kore.Sort as Sort
 import Kore.Step.Simplification.NotSimplifier
 import Kore.Step.Simplification.Simplify as Simplifier
 import Kore.Syntax.Sentence
@@ -103,7 +97,6 @@ import Kore.Syntax.Sentence
 import Kore.Unification.Unify
     ( MonadUnify
     )
-import qualified Kore.Unification.Unify as Unify
 import qualified Kore.Unification.Unify as Monad.Unify
 import Kore.Variables.Fresh
 
@@ -193,7 +186,7 @@ symbolVerifiers =
       , Builtin.verifySymbol Bool.assertSort [acceptAnySort, assertSort]
       )
     , ( Map.keysKey
-      , Builtin.verifySymbol Builtin.Set.assertSort [assertSort]
+      , Builtin.verifySymbol Set.assertSort [assertSort]
       )
     , ( Map.keys_listKey
       , Builtin.verifySymbol Builtin.List.assertSort [assertSort]
@@ -202,7 +195,7 @@ symbolVerifiers =
       , Builtin.verifySymbol assertSort [assertSort, acceptAnySort]
       )
     , ( Map.removeAllKey
-      , Builtin.verifySymbol assertSort [assertSort, Builtin.Set.assertSort]
+      , Builtin.verifySymbol assertSort [assertSort, Set.assertSort]
       )
     , ( Map.sizeKey
       , Builtin.verifySymbol Int.assertSort [assertSort]
@@ -391,7 +384,7 @@ evalKeys :: Builtin.Function
 evalKeys resultSort [_map] = do
     _map <- expectConcreteBuiltinMap Map.keysKey _map
     fmap (const Domain.SetValue) _map
-        & Builtin.Set.returnConcreteSet resultSort
+        & Set.returnConcreteSet resultSort
 evalKeys _ _ = Builtin.wrongArity Map.keysKey
 
 evalKeysList :: Builtin.Function
@@ -427,7 +420,7 @@ evalRemoveAll resultSort [_map, _set] = do
         bothConcrete = do
             _map <- expectConcreteBuiltinMap Map.removeAllKey _map
             _set <-
-                Builtin.Set.expectConcreteBuiltinSet
+                Set.expectConcreteBuiltinSet
                     Map.removeAllKey
                     _set
             Map.difference _map _set
@@ -575,30 +568,26 @@ unifyEquals unifyEqualsChildren first second = do
                 :: Ac.NormalizedOrBottom Domain.NormalizedMap variable
             normalizedOrBottom = Ac.toNormalized patt
 
-data InKeys term =
-    InKeys
-        { symbol :: !Symbol
-        , keyTerm, mapTerm :: !term
-        }
+newtype InKeys term = InKeys { getInKeys :: Set.InKeys term }
 
 instance
     InternalVariable variable
     => Injection (TermLike variable) (InKeys (TermLike variable))
   where
-    inject InKeys { symbol, keyTerm, mapTerm } =
+    inject ( InKeys Set.InKeys { symbol, keyTerm, mapTerm } ) =
         TermLike.mkApplySymbol symbol [keyTerm, mapTerm]
 
     retract (App_ symbol [keyTerm, mapTerm]) = do
         hook2 <- (getHook . symbolHook) symbol
         Monad.guard (hook2 == Map.in_keysKey)
-        return InKeys { symbol, keyTerm, mapTerm }
+        return $ InKeys Set.InKeys { symbol, keyTerm, mapTerm }
     retract _ = empty
 
 matchInKeys
     :: InternalVariable variable
     => TermLike variable
-    -> Maybe (InKeys (TermLike variable))
-matchInKeys = retract
+    -> Maybe (Set.InKeys (TermLike variable))
+matchInKeys = fmap getInKeys . retract
 
 unifyNotInKeys
     :: forall variable unifier
@@ -609,73 +598,8 @@ unifyNotInKeys
     -> TermLike variable
     -> TermLike variable
     -> MaybeT unifier (Pattern variable)
-unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b =
-    worker a b <|> worker b a
-  where
-    normalizedOrBottom
-       :: TermLike variable
-       -> Ac.NormalizedOrBottom Domain.NormalizedMap variable
-    normalizedOrBottom = Ac.toNormalized
-
-    defineTerm :: TermLike variable -> MaybeT unifier (Condition variable)
-    defineTerm termLike =
-        makeEvaluateTermCeil SideCondition.topTODO Sort.predicateSort termLike
-        >>= Unify.scatter
-        & lift
-
-    eraseTerm =
-        Pattern.fromCondition_ . Pattern.withoutTerm
-
-    unifyAndNegate t1 t2 = do
-        -- Erasing the unified term is valid here because
-        -- the terms are all wrapped in \ceil below.
-        unificationSolutions <-
-            fmap eraseTerm
-            <$> Unify.gather (unifyChildren t1 t2)
-        notSimplifier
-            SideCondition.top
-            (OrPattern.fromPatterns unificationSolutions)
-        >>= Unify.scatter
-
-    collectConditions terms =
-        Foldable.fold terms
-        & Pattern.fromCondition_
-
-    worker
-        :: TermLike variable
-        -> TermLike variable
-        -> MaybeT unifier (Pattern variable)
-    worker termLike1 termLike2
-      | Just boolValue <- Bool.matchBool termLike1
-      , not boolValue
-      , Just inKeys@InKeys { keyTerm, mapTerm } <- matchInKeys termLike2
-      , Ac.Normalized normalizedMap <- normalizedOrBottom mapTerm
-      = do
-        let symbolicKeys = Domain.getSymbolicKeysOfAc normalizedMap
-            concreteKeys =
-                TermLike.fromConcrete
-                <$> Domain.getConcreteKeysOfAc normalizedMap
-            mapKeys = symbolicKeys <> concreteKeys
-            opaqueElements = Domain.opaque . Domain.unwrapAc $ normalizedMap
-        if null mapKeys && null opaqueElements then
-            return Pattern.top
-        else do
-            Monad.guard (not (null mapKeys) || (length opaqueElements > 1))
-            -- Concrete keys are constructor-like, therefore they are defined
-            TermLike.assertConstructorLikeKeys concreteKeys $ return ()
-            definedKey <- defineTerm keyTerm
-            definedMap <- defineTerm mapTerm
-            keyConditions <- lift $ traverse (unifyAndNegate keyTerm) mapKeys
-
-            let keyInKeysOpaque =
-                    (\term -> inject @(TermLike _) inKeys { mapTerm = term })
-                    <$> opaqueElements
-
-            opaqueConditions <-
-                lift $ traverse (unifyChildren termLike1) keyInKeysOpaque
-            let conditions =
-                    fmap Pattern.withoutTerm (keyConditions <> opaqueConditions)
-                    <> [definedKey, definedMap]
-            return $ collectConditions conditions
-
-    worker _ _ = empty
+unifyNotInKeys =
+    Set.unifyNotInKeys
+        (Ac.toNormalized @Domain.NormalizedMap)
+        matchInKeys
+        (inject . InKeys)