diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 3361468180..10582495d9 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -36,6 +36,7 @@ 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 @@ -63,21 +64,25 @@ 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 Set +import qualified Kore.Builtin.Set as Builtin.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 - ( Pattern + ( Condition + , Pattern ) import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( makeCeilPredicate ) +import qualified Kore.Internal.SideCondition as SideCondition import Kore.Internal.Symbol - ( symbolHook + ( Symbol (..) + , symbolHook ) import Kore.Internal.TermLike ( pattern App_ @@ -89,6 +94,7 @@ 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 @@ -97,6 +103,7 @@ 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 @@ -186,7 +193,7 @@ symbolVerifiers = , Builtin.verifySymbol Bool.assertSort [acceptAnySort, assertSort] ) , ( Map.keysKey - , Builtin.verifySymbol Set.assertSort [assertSort] + , Builtin.verifySymbol Builtin.Set.assertSort [assertSort] ) , ( Map.keys_listKey , Builtin.verifySymbol Builtin.List.assertSort [assertSort] @@ -195,7 +202,7 @@ symbolVerifiers = , Builtin.verifySymbol assertSort [assertSort, acceptAnySort] ) , ( Map.removeAllKey - , Builtin.verifySymbol assertSort [assertSort, Set.assertSort] + , Builtin.verifySymbol assertSort [assertSort, Builtin.Set.assertSort] ) , ( Map.sizeKey , Builtin.verifySymbol Int.assertSort [assertSort] @@ -384,7 +391,7 @@ evalKeys :: Builtin.Function evalKeys resultSort [_map] = do _map <- expectConcreteBuiltinMap Map.keysKey _map fmap (const Domain.SetValue) _map - & Set.returnConcreteSet resultSort + & Builtin.Set.returnConcreteSet resultSort evalKeys _ _ = Builtin.wrongArity Map.keysKey evalKeysList :: Builtin.Function @@ -420,7 +427,7 @@ evalRemoveAll resultSort [_map, _set] = do bothConcrete = do _map <- expectConcreteBuiltinMap Map.removeAllKey _map _set <- - Set.expectConcreteBuiltinSet + Builtin.Set.expectConcreteBuiltinSet Map.removeAllKey _set Map.difference _map _set @@ -568,26 +575,30 @@ unifyEquals unifyEqualsChildren first second = do :: Ac.NormalizedOrBottom Domain.NormalizedMap variable normalizedOrBottom = Ac.toNormalized patt -newtype InKeys term = InKeys { getInKeys :: Set.InKeys term } +data InKeys term = + InKeys + { symbol :: !Symbol + , keyTerm, mapTerm :: !term + } instance InternalVariable variable => Injection (TermLike variable) (InKeys (TermLike variable)) where - inject ( InKeys Set.InKeys { symbol, keyTerm, mapTerm } ) = + inject 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 Set.InKeys { symbol, keyTerm, mapTerm } + return InKeys { symbol, keyTerm, mapTerm } retract _ = empty matchInKeys :: InternalVariable variable => TermLike variable - -> Maybe (Set.InKeys (TermLike variable)) -matchInKeys = fmap getInKeys . retract + -> Maybe (InKeys (TermLike variable)) +matchInKeys = retract unifyNotInKeys :: forall variable unifier @@ -598,8 +609,73 @@ unifyNotInKeys -> TermLike variable -> TermLike variable -> MaybeT unifier (Pattern variable) -unifyNotInKeys = - Set.unifyNotInKeys - (Ac.toNormalized @Domain.NormalizedMap) - matchInKeys - (inject . InKeys) +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 diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs index 0e3c04c193..bc7533c8e9 100644 --- a/kore/src/Kore/Builtin/Set.hs +++ b/kore/src/Kore/Builtin/Set.hs @@ -19,7 +19,6 @@ module Kore.Builtin.Set , verifiers , builtinFunctions , Domain.Builtin - , InKeys (..) , returnConcreteSet , Set.asTermLike , internalize @@ -31,8 +30,6 @@ module Kore.Builtin.Set , evalDifference -- * Unification , unifyEquals - , unifyNotInKeys - , unifyNotIn ) where import Prelude.Kore @@ -44,6 +41,8 @@ import Control.Error ) import qualified Control.Monad as Monad import qualified Data.Foldable as Foldable + ( toList + ) import qualified Data.HashMap.Strict as HashMap import Data.Map.Strict ( Map @@ -55,7 +54,6 @@ import Data.Text ( Text ) import qualified Data.Text as Text -import qualified Data.Traversable as Traversable import qualified Kore.Attribute.Symbol as Attribute ( Symbol ) @@ -71,10 +69,6 @@ import qualified Kore.Builtin.Builtin as Builtin import qualified Kore.Builtin.Int as Int import qualified Kore.Builtin.List as List import qualified Kore.Builtin.Set.Set as Set - -import Kore.Attribute.Hook - ( Hook (..) - ) import qualified Kore.Domain.Builtin as Domain import Kore.IndexedModule.MetadataTools ( SmtMetadataTools @@ -83,21 +77,14 @@ import Kore.Internal.ApplicationSorts ( ApplicationSorts (..) ) import qualified Kore.Internal.Conditional as Conditional -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 , makeMultipleAndPredicate ) -import qualified Kore.Internal.SideCondition as SideCondition -import Kore.Internal.Symbol - ( Symbol (..) - , symbolHook - ) import Kore.Internal.TermLike ( pattern App_ , pattern Builtin_ @@ -110,8 +97,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 ( SentenceSort (SentenceSort) @@ -122,7 +107,6 @@ import qualified Kore.Syntax.Sentence as Sentence.DoNotUse import Kore.Unification.Unify ( MonadUnify ) -import qualified Kore.Unification.Unify as Unify import qualified Kore.Unification.Unify as Monad.Unify {- | Builtin name of the @Set@ sort. @@ -600,138 +584,3 @@ unifyEquals normalizedOrBottom :: Ac.NormalizedOrBottom Domain.NormalizedSet variable normalizedOrBottom = Ac.toNormalized patt - -data InKeys term = - InKeys - { symbol :: !Symbol - , keyTerm, mapTerm :: !term - } - -newtype InSet term = InSet { getIn :: InKeys term} - -instance - InternalVariable variable - => Injection (TermLike variable) (InSet (TermLike variable)) - where - inject ( InSet InKeys { symbol, keyTerm, mapTerm = setTerm } ) = - TermLike.mkApplySymbol symbol [keyTerm, setTerm] - - retract (App_ symbol [keyTerm, setTerm]) = do - hook2 <- (getHook . symbolHook) symbol - Monad.guard (hook2 == Set.inKey) - return $ InSet InKeys { symbol, keyTerm, mapTerm = setTerm } - retract _ = empty - -matchSetIn - :: InternalVariable variable - => TermLike variable - -> Maybe (InKeys (TermLike variable)) -matchSetIn = fmap getIn . retract - -unifyNotIn - :: forall variable unifier - . InternalVariable variable - => MonadUnify unifier - => TermSimplifier variable unifier - -> NotSimplifier unifier - -> TermLike variable - -> TermLike variable - -> MaybeT unifier (Pattern variable) -unifyNotIn = - unifyNotInKeys - (Ac.toNormalized @Domain.NormalizedSet) - matchSetIn - (inject . InSet) - -unifyNotInKeys - :: forall normalized variable unifier - . InternalVariable variable - => Ac.TermWrapper normalized - => MonadUnify unifier - => (TermLike variable -> Ac.NormalizedOrBottom normalized variable) - -> (TermLike variable -> Maybe (InKeys (TermLike variable))) - -> (InKeys (TermLike variable) -> TermLike variable) - -> TermSimplifier variable unifier - -> NotSimplifier unifier - -> TermLike variable - -> TermLike variable - -> MaybeT unifier (Pattern variable) -unifyNotInKeys - normalizedOrBottom - matchInKeys - inject' - unifyChildren - (NotSimplifier notSimplifier) - a - b - = - worker a b <|> worker b a - where - defineTerm :: TermLike variable -> unifier (Condition variable) - defineTerm termLike = - makeEvaluateTermCeil SideCondition.topTODO Sort.predicateSort termLike - >>= Unify.scatter - - eraseTerm = - Pattern.fromCondition_ . Pattern.withoutTerm - - unifyAndNegate - :: TermLike variable - -> TermLike variable - -> unifier (Pattern variable) - 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 () - lift $ do - definedKey <- defineTerm keyTerm - definedMap <- defineTerm mapTerm - notInKnownKeys <- - traverse (unifyAndNegate keyTerm) mapKeys - & fmap (map Pattern.withoutTerm) - notInOpaqueKeys <- - Traversable.for opaqueElements - (\term -> - inject' inKeys { mapTerm = term } - & unifyChildren termLike1 - ) - & fmap (map Pattern.withoutTerm) - let conditions = - notInKnownKeys <> notInOpaqueKeys - <> [definedKey, definedMap] - return $ collectConditions conditions - - worker _ _ = empty diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index b4b73e5db0..9d4ff54cbd 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -245,7 +245,6 @@ andEqualsFunctions notSimplifier = , (BothT, \_ _ _ -> Builtin.Signedness.unifyEquals) , (BothT, \_ _ s -> unifyDefinedModifier (Builtin.Map.unifyEquals s)) , (EqualsT, \_ _ s -> Builtin.Map.unifyNotInKeys s notSimplifier) - , (EqualsT, \_ _ s -> Builtin.Set.unifyNotIn s notSimplifier) , (BothT, \_ _ s -> unifyDefinedModifier (Builtin.Set.unifyEquals s)) , (BothT, \_ t s -> Builtin.List.unifyEquals t s) , (BothT, \_ _ _ -> domainValueAndConstructorErrors) diff --git a/kore/test/Test/Kore/Step/MockSymbols.hs b/kore/test/Test/Kore/Step/MockSymbols.hs index 88650f4d4b..b015a8191c 100644 --- a/kore/test/Test/Kore/Step/MockSymbols.hs +++ b/kore/test/Test/Kore/Step/MockSymbols.hs @@ -630,10 +630,6 @@ unitSetSymbol :: Symbol unitSetSymbol = symbol unitSetId [] setSort & functional & hook "SET.unit" -inSetSymbol :: Internal.Symbol -inSetSymbol = - symbol "inSet" [testSort, setSort] boolSort & hook "SET.in" - opaqueSetSymbol :: Symbol opaqueSetSymbol = symbol opaqueSetId [testSort] setSort @@ -1237,14 +1233,6 @@ concatSet -> TermLike variable concatSet s1 s2 = Internal.mkApplySymbol concatSetSymbol [s1, s2] -inSet - :: InternalVariable variable - => HasCallStack - => TermLike variable - -> TermLike variable - -> TermLike variable -inSet element set = Internal.mkApplySymbol inSetSymbol [element, set] - opaqueSet :: InternalVariable variable => HasCallStack diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 275a8a4721..c2d7892034 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -1280,7 +1280,7 @@ test_equalsTermsSimplification = (Mock.f (mkElemVar Mock.x)) ) ( makeEqualsPredicate_ - ( mkElemVar Mock.y ) + (mkElemVar Mock.y) ( Mock.f (mkElemVar Mock.x) ) ) ) @@ -1300,157 +1300,6 @@ test_equalsTermsSimplification = ) ) assertEqual "" (Just [expect]) actual - , testCase "opaque value in map" $ do - let expect = - makeAndPredicate - ( makeNotPredicate - ( makeEqualsPredicate_ - ( mkElemVar Mock.x ) - Mock.a - ) - ) - ( makeAndPredicate - ( makeEqualsPredicate_ - ( Mock.builtinBool False ) - ( mkApplySymbol - Mock.inKeysMapSymbol - [ mkElemVar Mock.x, opaque] - ) - ) - ( mkForall Mock.x <$> - makeCeilPredicate Mock.testSort - ( Mock.framedMap - [(Mock.a, mkElemVar Mock.x)] - [opaque] - ) - ) - ) - & Condition.fromPredicate - opaque = mkElemVar Mock.xMap - actual <- - simplifyEquals - mempty - ( Mock.builtinBool False ) - ( Mock.inKeysMap - ( mkElemVar Mock.x ) - ( Mock.framedMap [(Mock.a, Mock.a)] [opaque] ) - ) - assertEqual "" (Just [expect]) actual - ] - , testGroup "builtin Set" - [ testCase "no keys in empty Set" $ do - let expect = Condition.top - actual <- - simplifyEquals - mempty - (Mock.builtinBool False) - (Mock.inSet (mkElemVar Mock.x) (Mock.builtinSet [])) - assertEqual "" (Just [expect]) actual - , testCase "key not in singleton Set" $ do - let expect = - makeEqualsPredicate_ - (mkElemVar Mock.x) - (mkElemVar Mock.y) - & makeNotPredicate - & Condition.fromPredicate - actual <- - simplifyEquals - mempty - ( Mock.builtinBool False ) - ( Mock.inSet - ( mkElemVar Mock.x) - ( Mock.builtinSet [mkElemVar Mock.y] ) - ) - assertEqual "" (Just [expect]) actual - , testCase "key not in two-element Set" $ do - let expect = - foldr1 - makeAndPredicate - [ makeNotPredicate - $ makeEqualsPredicate_ - (mkElemVar Mock.x) - (mkElemVar Mock.y) - , makeNotPredicate - $ makeEqualsPredicate_ - (mkElemVar Mock.x) - (mkElemVar Mock.z) - -- Definedness condition - , makeNotPredicate - $ makeEqualsPredicate_ - (mkElemVar Mock.y) - (mkElemVar Mock.z) - ] - & Condition.fromPredicate - actual <- - simplifyEquals - mempty - (Mock.builtinBool False) - ( Mock.inSet - ( mkElemVar Mock.x ) - ( Mock.builtinSet - [ mkElemVar Mock.y , mkElemVar Mock.z ] - ) - ) - assertEqual "" (Just [expect]) actual - , testCase "unevaluated function key in singleton Set" $ do - let expect = - makeAndPredicate - ( makeNotPredicate - ( makeAndPredicate - ( makeCeilPredicate_ - (Mock.f (mkElemVar Mock.x)) - ) - ( makeEqualsPredicate_ - ( mkElemVar Mock.y ) - ( Mock.f (mkElemVar Mock.x) ) - ) - ) - ) - ( makeCeilPredicate_ - (Mock.f (mkElemVar Mock.x)) - ) - & Condition.fromPredicate - actual <- - simplifyEquals - mempty - ( Mock.builtinBool False ) - ( Mock.inSet - ( Mock.f (mkElemVar Mock.x) ) - ( Mock.builtinSet [mkElemVar Mock.y] ) - ) - assertEqual "" (Just [expect]) actual - , testCase "opaque value in set" $ do - let expect = - makeAndPredicate - ( makeNotPredicate - ( makeEqualsPredicate_ - ( mkElemVar Mock.x ) - Mock.a - ) - ) - ( makeAndPredicate - ( makeEqualsPredicate_ - ( Mock.builtinBool False ) - ( mkApplySymbol - Mock.inSetSymbol - [ mkElemVar Mock.x, opaque] - ) - ) - ( makeCeilPredicate Mock.testSort - ( Mock.framedSet [Mock.a] [opaque] ) - ) - ) - & Condition.fromPredicate - opaque = mkElemVar Mock.xSet - actual <- - simplifyEquals - mempty - ( Mock.builtinBool False ) - ( Mock.inSet - ( mkElemVar Mock.x ) - ( Mock.framedSet [Mock.a] [opaque] ) - ) - assertEqual "" (Just [expect]) actual ] ]