From dc358ed8e64e1332549a66513d0e6434dd71218a Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 2 Sep 2020 20:27:40 -0500 Subject: [PATCH] Revert "Symbolic rules for SET.in (#2073)" This reverts commit 1ced2ee6fbada9038406feaa602031f50e1dbbcd. The symbolic rules applied to the negative case, but not the positive case. We need to keep the duality between negative and positive cases so that the SMT solver can reason about them. (The SMT solver has no knowledge of SET.) --- kore/src/Kore/Builtin/Map.hs | 110 ++++++++++-- kore/src/Kore/Builtin/Set.hs | 157 +----------------- kore/src/Kore/Step/Simplification/AndTerms.hs | 1 - kore/test/Test/Kore/Step/MockSymbols.hs | 12 -- .../Test/Kore/Step/Simplification/AndTerms.hs | 153 +---------------- 5 files changed, 97 insertions(+), 336 deletions(-) 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 ] ]