diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 10582495d9..3361468180 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/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) diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs index bc7533c8e9..0e3c04c193 100644 --- a/kore/src/Kore/Builtin/Set.hs +++ b/kore/src/Kore/Builtin/Set.hs @@ -19,6 +19,7 @@ module Kore.Builtin.Set , verifiers , builtinFunctions , Domain.Builtin + , InKeys (..) , returnConcreteSet , Set.asTermLike , internalize @@ -30,6 +31,8 @@ module Kore.Builtin.Set , evalDifference -- * Unification , unifyEquals + , unifyNotInKeys + , unifyNotIn ) where import Prelude.Kore @@ -41,8 +44,6 @@ 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 @@ -54,6 +55,7 @@ import Data.Text ( Text ) import qualified Data.Text as Text +import qualified Data.Traversable as Traversable import qualified Kore.Attribute.Symbol as Attribute ( Symbol ) @@ -69,6 +71,10 @@ 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 @@ -77,14 +83,21 @@ import Kore.Internal.ApplicationSorts ( ApplicationSorts (..) ) import qualified Kore.Internal.Conditional as Conditional +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 , makeMultipleAndPredicate ) +import qualified Kore.Internal.SideCondition as SideCondition +import Kore.Internal.Symbol + ( Symbol (..) + , symbolHook + ) import Kore.Internal.TermLike ( pattern App_ , pattern Builtin_ @@ -97,6 +110,8 @@ 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) @@ -107,6 +122,7 @@ 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. @@ -584,3 +600,138 @@ 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 cdd67cb04f..dac4fd0eec 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -245,6 +245,7 @@ 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 b015a8191c..88650f4d4b 100644 --- a/kore/test/Test/Kore/Step/MockSymbols.hs +++ b/kore/test/Test/Kore/Step/MockSymbols.hs @@ -630,6 +630,10 @@ 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 @@ -1233,6 +1237,14 @@ 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 0c58f700b5..5472bb4645 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -1279,7 +1279,7 @@ test_equalsTermsSimplification = (Mock.f (mkElemVar Mock.x)) ) ( makeEqualsPredicate_ - (mkElemVar Mock.y) + ( mkElemVar Mock.y ) ( Mock.f (mkElemVar Mock.x) ) ) ) @@ -1299,6 +1299,157 @@ 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.testSort + (Mock.f (mkElemVar Mock.x)) + ) + ( makeEqualsPredicate_ + ( mkElemVar Mock.y ) + ( Mock.f (mkElemVar Mock.x) ) + ) + ) + ) + ( makeCeilPredicate Mock.testSort + (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 ] ]