Keep set of defined terms in SideCondition (#2354)

Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>

Author: ana-pantilie

kore/src/Debug.hs

@@ -41,6 +41,10 @@ import Data.HashMap.Strict
     ( HashMap
     )
 import qualified Data.HashMap.Strict as HashMap
+import Data.HashSet
+    ( HashSet
+    )
+import qualified Data.HashSet as HashSet
 import Data.Int
 import Data.Map.Strict
     ( Map
@@ -346,6 +350,11 @@ instance Debug a => Debug (Set a) where
         (parens (precOut >= 10) . Pretty.sep)
         ["Data.Set.fromList", debug (Set.toList as)]
 
+instance Debug a => Debug (HashSet a) where
+    debugPrec as precOut =
+        (parens (precOut >= 10) . Pretty.sep)
+        ["Data.HashSet.fromList", debug (HashSet.toList as)]
+
 instance Debug a => Debug (Seq a) where
     debugPrec as precOut =
         (parens (precOut >= 10) . Pretty.sep)
@@ -620,6 +629,13 @@ instance (Debug a, Diff a) => Diff (Set a) where
         wrapFromList diff' precOut =
             parens (precOut >= 10) $ "Data.Set.fromList" <+> diff' 10
 
+instance (Debug a, Diff a) => Diff (HashSet a) where
+    diffPrec as bs =
+        fmap wrapFromList $ diffPrec (HashSet.toList as) (HashSet.toList bs)
+      where
+        wrapFromList diff' precOut =
+            parens (precOut >= 10) $ "Data.HashSet.fromList" <+> diff' 10
+
 instance Diff ExitCode
 
 instance (Debug a, Debug b, Diff a, Diff b) => Diff (Either a b)

kore/src/Kore/Builtin/AssocComm/CeilSimplifier.hs

@@ -17,15 +17,11 @@ import Prelude.Kore
 import Control.Error
     ( MaybeT
     )
-import qualified Control.Lens as Lens
-import Control.Monad
-    ( zipWithM
-    )
 import Control.Monad.Reader
     ( MonadReader
     )
 import qualified Control.Monad.Reader as Reader
-import qualified Data.List as List
+import qualified Data.Bifunctor as Bifunctor
 import qualified Data.Map.Strict as Map
 
 import Kore.Attribute.Pattern.FreeVariables
@@ -175,6 +171,8 @@ generalizeMapElement freeVariables' element =
 newBuiltinAssocCommCeilSimplifier
     :: forall normalized variable simplifier
     .   InternalVariable variable
+    =>  Ord (Element normalized (TermLike variable))
+    =>  Ord (Value normalized (TermLike variable))
     =>  MonadReader (SideCondition variable) simplifier
     =>  MonadSimplify simplifier
     =>  Traversable (Value normalized)
@@ -188,112 +186,95 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
     CeilSimplifier $ \Ceil { ceilChild } -> do
         let internalAc@InternalAc { builtinAcChild } = ceilChild
         sideCondition <- Reader.ask
-        let normalizedAc :: NormalizedAc normalized Key (TermLike variable)
-            normalizedAc = unwrapAc builtinAcChild
-            NormalizedAc
-                { elementsWithVariables = abstractElements
-                , concreteElements
-                , opaque
-                }
-              = normalizedAc
-
-        let defineOpaquePair
-                :: TermLike variable
-                -> TermLike variable
-                -> MultiAnd (OrCondition variable)
-            defineOpaquePair opaque1 opaque2 =
-                internalAc
-                    { builtinAcChild =
-                        wrapAc
-                        emptyNormalizedAc { opaque = [opaque1, opaque2] }
-                    }
-                & mkBuiltin
-                & makeCeilPredicate
-                -- TODO (thomas.tuegel): Do not mark this simplified.
-                -- Marking here may prevent user-defined axioms from applying.
-                -- At present, we wouldn't apply such an axiom, anyway.
-                & Predicate.markSimplifiedMaybeConditional Nothing
-                & OrCondition.fromPredicate
-                & MultiAnd.singleton
-
-            defineOpaquePairs
-                :: TermLike variable
-                -> [TermLike variable]
-                -> MultiAnd (OrCondition variable)
-            defineOpaquePairs this others =
-                foldMap (defineOpaquePair this) others
-
-            definedOpaquePairs :: MultiAnd (OrCondition variable)
-            definedOpaquePairs =
-                mconcat
-                $ zipWith defineOpaquePairs opaque
-                $ tail $ List.tails opaque
-
-        let abstractKeys, concreteKeys
-                :: [TermLike variable]
-            abstractValues, concreteValues, allValues
-                :: [Value normalized (TermLike variable)]
-            (abstractKeys, abstractValues) =
-                unzip (unwrapElement <$> abstractElements)
-            concreteKeys = from @Key <$> Map.keys concreteElements
-            concreteValues = Map.elems concreteElements
-            allValues = concreteValues <> abstractValues
-
-        let makeEvaluateTerm, defineAbstractKey, defineOpaque
-                :: TermLike variable -> MaybeT simplifier (OrCondition variable)
-            makeEvaluateTerm = makeEvaluateTermCeil sideCondition
-            defineAbstractKey = makeEvaluateTerm
-            defineOpaque = makeEvaluateTerm
-
-            defineValue
-                ::  Value normalized (TermLike variable)
-                ->  MaybeT simplifier (MultiAnd (OrCondition variable))
-            defineValue = foldlM worker mempty
-              where
-                worker multiAnd termLike = do
-                    evaluated <- makeEvaluateTerm termLike
-                    return (multiAnd <> MultiAnd.singleton evaluated)
-
-        TermLike.assertConstructorLikeKeys concreteKeys $ return ()
-
-        -- concreteKeys are defined by assumption
-        definedKeys <- traverse defineAbstractKey abstractKeys
-        definedOpaque <- traverse defineOpaque opaque
-        definedValues <- traverse defineValue allValues
-        -- concreteKeys are distinct by assumption
-        distinctConcreteKeys <-
-            traverse (flip distinctKey concreteKeys) abstractKeys
-        distinctAbstractKeys <-
-            zipWithM distinctKey
-                abstractKeys
-                (tail $ List.tails abstractKeys)
-        let conditions :: MultiAnd (OrCondition variable)
-            conditions =
-                mconcat
-                    [ MultiAnd.make definedKeys
-                    , MultiAnd.make definedOpaque
-                    , mconcat definedValues
-                    , mconcat distinctConcreteKeys
-                    , mconcat distinctAbstractKeys
-                    , foldMap (notMembers normalizedAc) opaque
-                    , definedOpaquePairs
-                    ]
-
+        let symbolicKeys = getSymbolicKeysOfAc builtinAcChild
+            symbolicValues = getSymbolicValuesOfAc builtinAcChild
+            concreteValues = getConcreteValuesOfAc builtinAcChild
+            opaqueElements = opaque . unwrapAc $ builtinAcChild
+        definedKeysAndOpaque <-
+            traverse
+                (makeEvaluateTermCeil sideCondition)
+                (symbolicKeys <> opaqueElements)
+            & fmap MultiAnd.make
+        definedValues <-
+            traverse
+                (defineValue sideCondition)
+                (symbolicValues <> concreteValues)
+            & fmap mconcat
+        definedSubCollections <-
+            definePairWiseElements mkBuiltin mkNotMember internalAc
+            . generatePairWiseElements
+            $ builtinAcChild
+        let conditions =
+                definedKeysAndOpaque
+                <> definedValues
+                <> definedSubCollections
         And.simplifyEvaluatedMultiPredicate sideCondition conditions
   where
+    defineValue
+        :: SideCondition variable
+        -> Value normalized (TermLike variable)
+        -> MaybeT simplifier (MultiAnd (OrCondition variable))
+    defineValue sideCondition = foldlM worker mempty
+      where
+        worker multiAnd termLike = do
+            evaluated <- makeEvaluateTermCeil sideCondition termLike
+            return (multiAnd <> MultiAnd.singleton evaluated)
 
-    distinctKey
-        ::  TermLike variable
-        ->  [TermLike variable]
-        ->  MaybeT simplifier (MultiAnd (OrCondition variable))
-    distinctKey thisKey otherKeys =
-        MultiAnd.make <$> traverse (notEquals thisKey) otherKeys
+definePairWiseElements
+    :: forall variable normalized simplifier
+    .  MonadSimplify simplifier
+    => InternalVariable variable
+    => MonadReader (SideCondition variable) simplifier
+    => AcWrapper normalized
+    => MkBuiltinAssocComm normalized variable
+    -> MkNotMember normalized variable
+    -> InternalAc Key normalized (TermLike variable)
+    -> PairWiseElements normalized Key (TermLike variable)
+    -> MaybeT simplifier (MultiAnd (OrCondition variable))
+definePairWiseElements mkBuiltin mkNotMember internalAc pairWiseElements = do
+    definedKeyPairs <-
+        traverse
+            distinctKey
+            (symbolicKeyPairs <> symbolicConcreteKeyPairs)
+            & fmap MultiAnd.make
+    let definedElementOpaquePairs =
+            foldMap
+                notMember
+                (symbolicOpaquePairs <> concreteOpaquePairs')
+        definedOpaquePairs =
+            foldMap defineOpaquePair opaquePairs
+    return . fold $
+        [ definedKeyPairs
+        , definedElementOpaquePairs
+        , definedOpaquePairs
+        ]
+  where
+    PairWiseElements
+        { symbolicPairs
+        , opaquePairs
+        , symbolicConcretePairs
+        , symbolicOpaquePairs
+        , concreteOpaquePairs
+        } = pairWiseElements
+    symbolicKeyPairs =
+        Bifunctor.bimap
+            (fst . unwrapElement)
+            (fst . unwrapElement)
+        <$> symbolicPairs
+    symbolicConcreteKeyPairs =
+        Bifunctor.bimap
+            (fst . unwrapElement)
+            (from @Key @(TermLike variable) . fst)
+        <$> symbolicConcretePairs
+    concreteOpaquePairs' =
+        Bifunctor.first
+            wrapConcreteElement
+        <$> concreteOpaquePairs
 
-    notEquals
-        ::  TermLike variable
-        ->  TermLike variable
-        ->  MaybeT simplifier (OrCondition variable)
-    notEquals t1 t2 = do
+    distinctKey
+        :: (TermLike variable, TermLike variable)
+        -> MaybeT simplifier (OrCondition variable)
+    distinctKey (t1, t2) = do
         sideCondition <- Reader.ask
         Equals.makeEvaluateTermsToPredicate tMin tMax sideCondition
             >>= Not.simplifyEvaluatedPredicate
@@ -302,37 +283,30 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
         (tMin, tMax) = minMax t1 t2
 
     notMember
-        :: TermLike variable
-        -> Element normalized (TermLike variable)
+        :: (Element normalized (TermLike variable), TermLike variable)
         -> MultiAnd (OrCondition variable)
-    notMember termLike element =
+    notMember (element, termLike) =
         mkNotMember element termLike
         & OrCondition.fromPredicate
         & MultiAnd.singleton
 
-    notMembers
-        :: NormalizedAc normalized Key (TermLike variable)
-        -> TermLike variable
+    defineOpaquePair
+        :: (TermLike variable, TermLike variable)
         -> MultiAnd (OrCondition variable)
-    notMembers normalizedAc termLike =
-        Lens.foldMapOf foldElements (notMember termLike) normalizedAc
-
-foldElements
-    ::  AcWrapper collection
-    =>  InternalVariable variable
-    =>  Lens.Fold
-            (NormalizedAc collection Key (TermLike variable))
-            (Element collection (TermLike variable))
-foldElements =
-    Lens.folding $ \normalizedAc ->
-        let
-            concreteElements' =
-                concreteElements normalizedAc
-                & Map.toList
-                & map wrapConcreteElement
-            symbolicElements' = elementsWithVariables normalizedAc
-        in
-            concreteElements' <> symbolicElements'
+    defineOpaquePair (opaque1, opaque2) =
+        internalAc
+            { builtinAcChild =
+                wrapAc
+                emptyNormalizedAc { opaque = [opaque1, opaque2] }
+            }
+        & mkBuiltin
+        & makeCeilPredicate
+        -- TODO (thomas.tuegel): Do not mark this simplified.
+        -- Marking here may prevent user-defined axioms from applying.
+        -- At present, we wouldn't apply such an axiom, anyway.
+        & Predicate.markSimplifiedMaybeConditional Nothing
+        & OrCondition.fromPredicate
+        & MultiAnd.singleton
 
 fromElement
     :: AcWrapper normalized

kore/src/Kore/Internal/NormalizedAc.hs

@@ -28,6 +28,8 @@ module Kore.Internal.NormalizedAc
     , normalizedAcConstructorLike
     , normalizedAcFunctional
     , unparseInternalAc
+    , PairWiseElements (..)
+    , generatePairWiseElements
     ) where
 
 import Prelude.Kore
@@ -39,6 +41,9 @@ import Control.Lens.Iso
 import Data.Kind
     ( Type
     )
+import Data.List.Extra
+    ( nubOrdBy
+    )
 import Data.Map.Strict
     ( Map
     )
@@ -489,3 +494,54 @@ normalizedAcConstructorLike ac@(NormalizedAc _ _ _) =
                 pairIsConstructorLike (key, value) =
                     assertConstructorLike "" key $ isConstructorLike value
         _ -> ConstructorLike Nothing
+
+-- | 'PairWiseElements' is a representation of the elements of all subcollections
+-- necessary for proving the definedness of a collection.
+data PairWiseElements normalized key child =
+    PairWiseElements
+        { symbolicPairs
+            :: [(Element normalized child, Element normalized child)]
+        , concretePairs
+            :: [((key, Value normalized child), (key, Value normalized child))]
+        , opaquePairs
+            :: [(child, child)]
+        , symbolicConcretePairs
+            :: [(Element normalized child, (key, Value normalized child))]
+        , symbolicOpaquePairs
+            :: [(Element normalized child, child)]
+        , concreteOpaquePairs
+            :: [((key, Value normalized child), child)]
+        }
+
+-- | Generates the 'PairWiseElements' for a 'AcWrapper' collection.
+generatePairWiseElements
+    :: AcWrapper normalized
+    => Ord key
+    => Ord child
+    => Ord (Element normalized child)
+    => Ord (Value normalized child)
+    => normalized key child
+    -> PairWiseElements normalized key child
+generatePairWiseElements (unwrapAc -> normalized) =
+    PairWiseElements
+        { symbolicPairs = pairWiseElemsOfSameType symbolicElems
+        , concretePairs = pairWiseElemsOfSameType concreteElems
+        , opaquePairs   = pairWiseElemsOfSameType opaqueElems
+        , symbolicConcretePairs =
+            (,) <$> symbolicElems <*> concreteElems
+        , symbolicOpaquePairs =
+            (,) <$> symbolicElems <*> opaqueElems
+        , concreteOpaquePairs =
+            (,) <$> concreteElems <*> opaqueElems
+        }
+  where
+    symbolicElems = elementsWithVariables normalized
+    concreteElems = Map.toList . concreteElements $ normalized
+    opaqueElems = opaque normalized
+    pairWiseElemsOfSameType elems =
+        [ (x, y) | x <- elems, y <- elems, x /= y ]
+        & nubOrdBy applyComm
+    applyComm p1 p2
+      | p1 == p2 = EQ
+      | swap p1 == p2 = EQ
+      | otherwise = compare p1 p2