From ebd41e104bd81d41b9b12ae528dd393088ca3127 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Mon, 17 Aug 2020 16:46:43 +0300 Subject: [PATCH 01/29] Symbolic rules for SET.in --- kore/src/Kore/Builtin/Map.hs | 104 ++----------- kore/src/Kore/Builtin/Set.hs | 139 +++++++++++++++++- kore/src/Kore/Step/Simplification/AndTerms.hs | 1 + 3 files changed, 150 insertions(+), 94 deletions(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 410d03ab87..a942bb303a 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,71 +598,4 @@ 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 - - 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 matchInKeys (inject . InKeys) diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs index bc7533c8e9..e4583e6e49 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 @@ -69,6 +70,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 +82,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 +109,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 +121,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 +599,121 @@ unifyEquals normalizedOrBottom :: Ac.NormalizedOrBottom Domain.NormalizedSet variable normalizedOrBottom = Ac.toNormalized patt + +data InKeys term = + InKeys + { symbol :: !Symbol + , keyTerm, mapTerm :: !term + } + +newtype In term = In { getIn :: InKeys term} + +instance + InternalVariable variable + => Injection (TermLike variable) (In (TermLike variable)) + where + inject ( In 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 $ In 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 matchSetIn (inject . In) + +unifyNotInKeys + :: forall variable unifier + . InternalVariable variable + => MonadUnify unifier + => (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 matchInKeys inject' 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 + + 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' 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/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) From f4739c58af64f89023346ecd91785c388cd43c08 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Wed, 19 Aug 2020 15:40:42 +0300 Subject: [PATCH 02/29] wip: Test --- kore/test/Test/Kore/Step/MockSymbols.hs | 12 ++++++++++++ .../Test/Kore/Step/Simplification/AndTerms.hs | 18 ++++++++++++++++++ 2 files changed, 30 insertions(+) diff --git a/kore/test/Test/Kore/Step/MockSymbols.hs b/kore/test/Test/Kore/Step/MockSymbols.hs index 5e108d801d..13628641ef 100644 --- a/kore/test/Test/Kore/Step/MockSymbols.hs +++ b/kore/test/Test/Kore/Step/MockSymbols.hs @@ -623,6 +623,10 @@ unitSetSymbol :: Symbol unitSetSymbol = symbol unitSetId [] setSort & functional & hook "SET.unit" +inSetSymbol :: Internal.Symbol +inSetSymbol = + symbol "inSet" [intSort, setSort] boolSort & hook "SET.in" + opaqueSetSymbol :: Symbol opaqueSetSymbol = symbol opaqueSetId [testSort] setSort @@ -1218,6 +1222,14 @@ concatSet -> TermLike variable concatSet s1 s2 = Internal.mkApplySymbol concatSetSymbol [s1, s2] +inSet + :: InternalVariable variable + => HasCallStack + => TermLike variable + -> TermLike variable + -> TermLike variable +inSet e s = Internal.mkApplySymbol inSetSymbol [e, s] + 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 540baacc06..8afa03155b 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -9,6 +9,8 @@ module Test.Kore.Step.Simplification.AndTerms import Prelude.Kore +import Kore.Unparser + import Test.Tasty import Control.Error @@ -17,6 +19,7 @@ import Control.Error import qualified Data.List as List import qualified Data.Map.Strict as Map import qualified Data.Set as Set +import qualified Data.Foldable as Foldable import Data.Text ( Text ) @@ -34,6 +37,7 @@ import Kore.Internal.Predicate , makeEqualsPredicate , makeEqualsPredicate_ , makeTruePredicate + , makeMultipleAndPredicate ) import Kore.Internal.SideCondition ( SideCondition @@ -67,6 +71,9 @@ import qualified Kore.Unification.UnifierT as Monad.Unify import Test.Kore import qualified Test.Kore.Step.MockSymbols as Mock import Test.Kore.Step.Simplification +import Test.Kore.Builtin.Definition + ( inSetSymbol + ) import Test.Tasty.HUnit.Ext test_andTermsSimplification :: [TestTree] @@ -1046,6 +1053,17 @@ test_andTermsSimplification = ) testSet assertEqual "" expected actual + , testCase "qq" $ do + let expect = + (\x -> (x, x)) undefined + actual <- + simplifyUnify + (Mock.builtinBool False) + (Mock.inSet (mkElemVar Mock.xInt) Mock.unitSet) + traceM $ show (length (fst actual)) <> " List:\n" + Foldable.traverse_ (traceM . unparseToString) (fst actual) + Foldable.traverse_ (traceM . unparseToString) (snd actual) + assertEqual "" expect actual ] , testGroup "alias expansion" [ testCase "alias() vs top" $ do From e0e3eb7806957b9275e0a2c162a819a4736cb7b1 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Wed, 19 Aug 2020 16:21:10 +0300 Subject: [PATCH 03/29] Test --- kore/test/Test/Kore/Step/MockSymbols.hs | 14 ++++++++++++++ .../test/Test/Kore/Step/Simplification/AndTerms.hs | 12 ++++++++++++ 2 files changed, 26 insertions(+) diff --git a/kore/test/Test/Kore/Step/MockSymbols.hs b/kore/test/Test/Kore/Step/MockSymbols.hs index 5e108d801d..79e01f6e87 100644 --- a/kore/test/Test/Kore/Step/MockSymbols.hs +++ b/kore/test/Test/Kore/Step/MockSymbols.hs @@ -247,6 +247,8 @@ concatMapId :: Id concatMapId = testId "concatMap" opaqueMapId :: Id opaqueMapId = testId "opaqueMap" +inKeysMapId :: Id +inKeysMapId = testId "inKeys" lessIntId :: Id lessIntId = testId "lessIntId" greaterEqIntId :: Id @@ -580,6 +582,10 @@ opaqueMapSymbol = symbol opaqueMapId [testSort] mapSort & function +inKeysMapSymbol :: Symbol +inKeysMapSymbol = + symbol inKeysMapId [testSort, mapSort] boolSort + lessIntSymbol :: Symbol lessIntSymbol = symbol lessIntId [intSort, intSort] boolSort @@ -1200,6 +1206,14 @@ opaqueMap -> TermLike variable opaqueMap term = Internal.mkApplySymbol opaqueMapSymbol [term] +inKeysMap + :: InternalVariable variable + => HasCallStack + => TermLike variable + -> TermLike variable + -> TermLike variable +inKeysMap element m1 = Internal.mkApplySymbol inKeysMapSymbol [element, m1] + unitSet :: InternalVariable variable => TermLike variable unitSet = Internal.mkApplySymbol unitSetSymbol [] diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 540baacc06..d8b1a6f46a 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -15,6 +15,8 @@ import Control.Error ( MaybeT (..) ) import qualified Data.List as List +import qualified Data.Foldable as Foldable +import Kore.Unparser import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Data.Text @@ -837,6 +839,16 @@ test_andTermsSimplification = (mkElemVar Mock.m) ) assertEqual "" expected actual + , testCase "qq" $ do + let expect = undefined + actual <- + simplifyUnify + (Mock.builtinBool False) + (Mock.inKeysMap (mkElemVar Mock.x) Mock.unitMap) + traceM "HERE:\n" + Foldable.traverse_ (traceM . unparseToString) (fst actual) + assertEqual "" expect actual + -- TODO: Add tests with non-trivial predicates. ] From 87c4320b98dcef68bb140a6746f71c9191903a55 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Wed, 19 Aug 2020 16:26:59 +0300 Subject: [PATCH 04/29] Stylish --- kore/test/Test/Kore/Step/Simplification/AndTerms.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index d8b1a6f46a..1899bb44b2 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -14,14 +14,14 @@ import Test.Tasty import Control.Error ( MaybeT (..) ) -import qualified Data.List as List import qualified Data.Foldable as Foldable -import Kore.Unparser +import qualified Data.List as List import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Data.Text ( Text ) +import Kore.Unparser import qualified Kore.Builtin.AssociativeCommutative as Ac import qualified Kore.Domain.Builtin as Domain From ceb12605c98699ec8919402aeaa2223e4de5200d Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Wed, 19 Aug 2020 17:50:55 +0300 Subject: [PATCH 05/29] Hook symbol --- kore/test/Test/Kore/Step/MockSymbols.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/kore/test/Test/Kore/Step/MockSymbols.hs b/kore/test/Test/Kore/Step/MockSymbols.hs index 79e01f6e87..d040fa5d46 100644 --- a/kore/test/Test/Kore/Step/MockSymbols.hs +++ b/kore/test/Test/Kore/Step/MockSymbols.hs @@ -585,6 +585,7 @@ opaqueMapSymbol = inKeysMapSymbol :: Symbol inKeysMapSymbol = symbol inKeysMapId [testSort, mapSort] boolSort + & hook "MAP.in_keys" lessIntSymbol :: Symbol lessIntSymbol = From 640ee3c8556f9d941e88bbc467190b08d369fd14 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Wed, 19 Aug 2020 21:29:01 +0300 Subject: [PATCH 06/29] Use Mock.builtinMap [] --- kore/test/Test/Kore/Step/Simplification/AndTerms.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 1899bb44b2..9b9410507a 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -844,7 +844,7 @@ test_andTermsSimplification = actual <- simplifyUnify (Mock.builtinBool False) - (Mock.inKeysMap (mkElemVar Mock.x) Mock.unitMap) + (Mock.inKeysMap (mkElemVar Mock.x) (Mock.builtinMap [])) traceM "HERE:\n" Foldable.traverse_ (traceM . unparseToString) (fst actual) assertEqual "" expect actual From 03d6052a9fece896be288715e5776ca1eaad36da Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 14:23:48 +0300 Subject: [PATCH 07/29] Use simplifyEquals in test and make it pass --- kore/src/Kore/Builtin/Map.hs | 47 ++++++++++--------- kore/src/Kore/Step/Simplification/AndTerms.hs | 2 +- .../Test/Kore/Step/Simplification/AndTerms.hs | 20 ++++---- 3 files changed, 37 insertions(+), 32 deletions(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 410d03ab87..0b07219747 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -29,7 +29,9 @@ module Kore.Builtin.Map ) where import Prelude.Kore - +import Kore.Unparser + ( unparseToString + ) import Control.Error ( MaybeT (MaybeT) , hoistMaybe @@ -657,23 +659,26 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = <$> Domain.getConcreteKeysOfAc normalizedMap mapKeys = symbolicKeys <> concreteKeys opaqueElements = Domain.opaque . Domain.unwrapAc $ normalizedMap - - 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 + if null mapKeys then + return Pattern.top + else do + -- 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 _ _ = do + traceM "Otherwise" + empty diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index cdd67cb04f..d78ba867a7 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -198,7 +198,7 @@ equalsFunctions => HasCallStack => NotSimplifier unifier -> [TermTransformationOld variable unifier] -equalsFunctions notSimplifier = +equalsFunctions notSimplifier = trace "equalsFunctions" $ forEquals . snd <$> filter appliesToEquals (andEqualsFunctions notSimplifier) where diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 63acf30464..a2953ed2ca 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -36,6 +36,7 @@ import Kore.Internal.Predicate , makeEqualsPredicate , makeEqualsPredicate_ , makeTruePredicate + , makeNotPredicate ) import Kore.Internal.SideCondition ( SideCondition @@ -839,15 +840,6 @@ test_andTermsSimplification = (mkElemVar Mock.m) ) assertEqual "" expected actual - , testCase "qq" $ do - let expect = undefined - actual <- - simplifyUnify - (Mock.builtinBool False) - (Mock.inKeysMap (mkElemVar Mock.x) (Mock.builtinMap [])) - traceM "HERE:\n" - Foldable.traverse_ (traceM . unparseToString) (fst actual) - assertEqual "" expect actual -- TODO: Add tests with non-trivial predicates. , testCase "unifies functions in keys" $ do @@ -859,7 +851,15 @@ test_andTermsSimplification = & Pattern.withCondition concrete actual <- simplifyUnify concrete symbolic assertEqual "" ([expect], [expect]) actual - ] + + , testCase "qq\\equals(false, X in []) = \\top" $ do + let expect = Condition.top + actual <- + simplifyEquals + mempty + (Mock.builtinBool False) + (Mock.inKeysMap (mkElemVar Mock.x) (Mock.builtinMap [])) + assertEqual "" (Just [expect]) actual ] , testGroup "builtin List domain" [ testCase "[same head, same head]" $ do From f7074c98a256e504fe38c6828003c6b11cc6ef58 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 14:25:42 +0300 Subject: [PATCH 08/29] Small cleanup --- kore/src/Kore/Step/Simplification/AndTerms.hs | 2 +- kore/test/Test/Kore/Step/Simplification/AndTerms.hs | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index d78ba867a7..cdd67cb04f 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -198,7 +198,7 @@ equalsFunctions => HasCallStack => NotSimplifier unifier -> [TermTransformationOld variable unifier] -equalsFunctions notSimplifier = trace "equalsFunctions" $ +equalsFunctions notSimplifier = forEquals . snd <$> filter appliesToEquals (andEqualsFunctions notSimplifier) where diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index a2953ed2ca..7f14219fe2 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -859,7 +859,8 @@ test_andTermsSimplification = mempty (Mock.builtinBool False) (Mock.inKeysMap (mkElemVar Mock.x) (Mock.builtinMap [])) - assertEqual "" (Just [expect]) actual ] + assertEqual "" (Just [expect]) actual + ] , testGroup "builtin List domain" [ testCase "[same head, same head]" $ do From 9814276b6450b3a5b3a3c81d74255516fab89ef0 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 14:30:00 +0300 Subject: [PATCH 09/29] Add passing test --- .../Test/Kore/Step/Simplification/AndTerms.hs | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 7f14219fe2..efd8140b00 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -860,6 +860,27 @@ test_andTermsSimplification = (Mock.builtinBool False) (Mock.inKeysMap (mkElemVar Mock.x) (Mock.builtinMap [])) assertEqual "" (Just [expect]) actual + + , testCase + "qq\\equals(false, X in [(Y, a)]) = \\not \\equals(X, Y)" + $ do + let expect = + makeEqualsPredicate_ + (mkElemVar Mock.x) + (mkElemVar Mock.y) + & makeNotPredicate + & Condition.fromPredicate + actual <- + simplifyEquals + mempty + ( Mock.builtinBool False ) + ( Mock.inKeysMap + ( mkElemVar Mock.x) + ( Mock.builtinMap + [ ( mkElemVar Mock.y, Mock.a ) ] + ) + ) + assertEqual "" (Just [expect]) actual ] , testGroup "builtin List domain" From 8a213ead71034ef04b14e69482c31e837786ce9c Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 16:20:07 +0300 Subject: [PATCH 10/29] Add failing test: map wiith two elements --- kore/src/Kore/Builtin/Map.hs | 13 ++++--- .../Test/Kore/Step/Simplification/AndTerms.hs | 36 +++++++++++++++---- 2 files changed, 39 insertions(+), 10 deletions(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 0b07219747..66b26b8143 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -28,10 +28,6 @@ module Kore.Builtin.Map , evalInKeys ) where -import Prelude.Kore -import Kore.Unparser - ( unparseToString - ) import Control.Error ( MaybeT (MaybeT) , hoistMaybe @@ -49,6 +45,10 @@ import Data.Text ( Text ) import qualified Data.Text as Text +import Kore.Unparser + ( unparseToString + ) +import Prelude.Kore import Kore.Attribute.Hook ( Hook (..) @@ -664,10 +664,15 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = else do -- Concrete keys are constructor-like, therefore they are defined TermLike.assertConstructorLikeKeys concreteKeys $ return () + traceM $ "MAP TERM" + traceM $ unparseToString mapTerm definedKey <- defineTerm keyTerm definedMap <- defineTerm mapTerm keyConditions <- lift $ traverse (unifyAndNegate keyTerm) mapKeys + traceM $ "DEFINED MAP TERM" + traceM $ unparseToString definedMap + let keyInKeysOpaque = (\term -> inject @(TermLike _) inKeys { mapTerm = term }) <$> opaqueElements diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index efd8140b00..dd493c7d8f 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -35,8 +35,8 @@ import Kore.Internal.Predicate ( makeCeilPredicate , makeEqualsPredicate , makeEqualsPredicate_ - , makeTruePredicate , makeNotPredicate + , makeTruePredicate ) import Kore.Internal.SideCondition ( SideCondition @@ -852,7 +852,7 @@ test_andTermsSimplification = actual <- simplifyUnify concrete symbolic assertEqual "" ([expect], [expect]) actual - , testCase "qq\\equals(false, X in []) = \\top" $ do + , testCase "\\equals(false, X in []) = \\top" $ do let expect = Condition.top actual <- simplifyEquals @@ -860,9 +860,9 @@ test_andTermsSimplification = (Mock.builtinBool False) (Mock.inKeysMap (mkElemVar Mock.x) (Mock.builtinMap [])) assertEqual "" (Just [expect]) actual - + , testCase - "qq\\equals(false, X in [(Y, a)]) = \\not \\equals(X, Y)" + "\\equals(false, X in [(Y, a)]) = \\not \\equals(X, Y)" $ do let expect = makeEqualsPredicate_ @@ -875,13 +875,37 @@ test_andTermsSimplification = mempty ( Mock.builtinBool False ) ( Mock.inKeysMap - ( mkElemVar Mock.x) + ( mkElemVar Mock.x) ( Mock.builtinMap [ ( mkElemVar Mock.y, Mock.a ) ] ) ) assertEqual "" (Just [expect]) actual - ] + , testCase + "qq\\equals(false, X in [Y Z])\ + \ = \\not \\equals(X, Y) \\and \\not \\equals(X, Z)" + $ do + actual <- + simplifyEquals + mempty + (Mock.builtinBool False) + ( Mock.inKeysMap + (mkElemVar Mock.x) + ( Mock.builtinMap + [ ( mkElemVar Mock.y, Mock.a ) + , ( mkElemVar Mock.z, Mock.a ) + ] + ) + ) + {- + traceM "expect" + traceM $ unparseToString expect + -} + traceM "actual" + (Foldable.traverse_ . Foldable.traverse_) + (traceM . unparseToString) + actual + assertEqual "" actual actual ] , testGroup "builtin List domain" [ testCase "[same head, same head]" $ do From 793966d3c40ade7112f221204eeca9c459a7726e Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 16:38:41 +0300 Subject: [PATCH 11/29] Some cleanup --- kore/src/Kore/Builtin/Map.hs | 3 ++- kore/test/Test/Kore/Step/Simplification/AndTerms.hs | 8 ++------ 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 66b26b8143..ee83a404db 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -28,6 +28,8 @@ module Kore.Builtin.Map , evalInKeys ) where +import Prelude.Kore + import Control.Error ( MaybeT (MaybeT) , hoistMaybe @@ -48,7 +50,6 @@ import qualified Data.Text as Text import Kore.Unparser ( unparseToString ) -import Prelude.Kore import Kore.Attribute.Hook ( Hook (..) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index dd493c7d8f..ca4048e3c8 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -841,7 +841,6 @@ test_andTermsSimplification = ) assertEqual "" expected actual - -- TODO: Add tests with non-trivial predicates. , testCase "unifies functions in keys" $ do let concrete = Mock.builtinMap [(Mock.a , Mock.a)] symbolic = Mock.builtinMap [(Mock.f Mock.b, Mock.a)] @@ -897,15 +896,12 @@ test_andTermsSimplification = ] ) ) - {- - traceM "expect" - traceM $ unparseToString expect - -} traceM "actual" (Foldable.traverse_ . Foldable.traverse_) (traceM . unparseToString) actual - assertEqual "" actual actual ] + assertEqual "" undefined actual + ] , testGroup "builtin List domain" [ testCase "[same head, same head]" $ do From 54b32cf204ee5d14635d120a2f4f8c44d89ecc98 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 16:40:15 +0300 Subject: [PATCH 12/29] Lint --- kore/src/Kore/Builtin/Map.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index ee83a404db..316a8d6628 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -665,13 +665,13 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = else do -- Concrete keys are constructor-like, therefore they are defined TermLike.assertConstructorLikeKeys concreteKeys $ return () - traceM $ "MAP TERM" + traceM "MAP TERM" traceM $ unparseToString mapTerm definedKey <- defineTerm keyTerm definedMap <- defineTerm mapTerm keyConditions <- lift $ traverse (unifyAndNegate keyTerm) mapKeys - traceM $ "DEFINED MAP TERM" + traceM "DEFINED MAP TERM" traceM $ unparseToString definedMap let keyInKeysOpaque = From ef9d6a814fec456a67f27f29e824f16d9b785d9c Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 17:35:19 +0300 Subject: [PATCH 13/29] Fix test --- .../Test/Kore/Step/Simplification/AndTerms.hs | 31 +++++++++++++------ 1 file changed, 22 insertions(+), 9 deletions(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index ca4048e3c8..329c578adf 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -14,14 +14,12 @@ import Test.Tasty import Control.Error ( MaybeT (..) ) -import qualified Data.Foldable as Foldable import qualified Data.List as List import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Data.Text ( Text ) -import Kore.Unparser import qualified Kore.Builtin.AssociativeCommutative as Ac import qualified Kore.Domain.Builtin as Domain @@ -32,7 +30,8 @@ import qualified Kore.Internal.MultiOr as MultiOr ) import Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate - ( makeCeilPredicate + ( makeAndPredicate + , makeCeilPredicate , makeEqualsPredicate , makeEqualsPredicate_ , makeNotPredicate @@ -881,9 +880,27 @@ test_andTermsSimplification = ) assertEqual "" (Just [expect]) actual , testCase - "qq\\equals(false, X in [Y Z])\ + "\\equals(false, X in [Y Z])\ \ = \\not \\equals(X, Y) \\and \\not \\equals(X, Z)" $ 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 @@ -896,11 +913,7 @@ test_andTermsSimplification = ] ) ) - traceM "actual" - (Foldable.traverse_ . Foldable.traverse_) - (traceM . unparseToString) - actual - assertEqual "" undefined actual + assertEqual "" (Just [expect]) actual ] , testGroup "builtin List domain" From 12d01b688e6446dabdb66c623f3b73c43b06819c Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 18:17:35 +0300 Subject: [PATCH 14/29] Add test. It doesn't look exacly right --- kore/src/Kore/Builtin/Map.hs | 11 +------ .../Test/Kore/Step/Simplification/AndTerms.hs | 31 ++++++++++++++++++- 2 files changed, 31 insertions(+), 11 deletions(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 316a8d6628..70c0a642e7 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -47,9 +47,6 @@ import Data.Text ( Text ) import qualified Data.Text as Text -import Kore.Unparser - ( unparseToString - ) import Kore.Attribute.Hook ( Hook (..) @@ -665,15 +662,10 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = else do -- Concrete keys are constructor-like, therefore they are defined TermLike.assertConstructorLikeKeys concreteKeys $ return () - traceM "MAP TERM" - traceM $ unparseToString mapTerm definedKey <- defineTerm keyTerm definedMap <- defineTerm mapTerm keyConditions <- lift $ traverse (unifyAndNegate keyTerm) mapKeys - traceM "DEFINED MAP TERM" - traceM $ unparseToString definedMap - let keyInKeysOpaque = (\term -> inject @(TermLike _) inKeys { mapTerm = term }) <$> opaqueElements @@ -685,6 +677,5 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = <> [definedKey, definedMap] return $ collectConditions conditions - worker _ _ = do - traceM "Otherwise" + worker _ _ = empty diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 329c578adf..0166e6f0b3 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -906,7 +906,7 @@ test_andTermsSimplification = mempty (Mock.builtinBool False) ( Mock.inKeysMap - (mkElemVar Mock.x) + ( mkElemVar Mock.x ) ( Mock.builtinMap [ ( mkElemVar Mock.y, Mock.a ) , ( mkElemVar Mock.z, Mock.a ) @@ -914,6 +914,35 @@ test_andTermsSimplification = ) ) assertEqual "" (Just [expect]) actual + , testCase "\\equals(false, f(X) in [Y]) = \\not \\equals(f(X), Y)" $ 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.inKeysMap + ( Mock.f (mkElemVar Mock.x) ) + ( Mock.builtinMap + [ (mkElemVar Mock.y, Mock.a ) ] + ) + ) + assertEqual "" (Just [expect]) actual ] , testGroup "builtin List domain" From ae5ad3149a998442248784b5e80fb9f2af28dc31 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 18:22:58 +0300 Subject: [PATCH 15/29] Remove extra newlines --- kore/src/Kore/Builtin/Map.hs | 3 +-- kore/test/Test/Kore/Step/Simplification/AndTerms.hs | 3 --- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 70c0a642e7..3c227aca51 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -677,5 +677,4 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = <> [definedKey, definedMap] return $ collectConditions conditions - worker _ _ = - empty + worker _ _ = empty diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 0166e6f0b3..4ee0dec13f 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -839,7 +839,6 @@ test_andTermsSimplification = (mkElemVar Mock.m) ) assertEqual "" expected actual - , testCase "unifies functions in keys" $ do let concrete = Mock.builtinMap [(Mock.a , Mock.a)] symbolic = Mock.builtinMap [(Mock.f Mock.b, Mock.a)] @@ -849,7 +848,6 @@ test_andTermsSimplification = & Pattern.withCondition concrete actual <- simplifyUnify concrete symbolic assertEqual "" ([expect], [expect]) actual - , testCase "\\equals(false, X in []) = \\top" $ do let expect = Condition.top actual <- @@ -858,7 +856,6 @@ test_andTermsSimplification = (Mock.builtinBool False) (Mock.inKeysMap (mkElemVar Mock.x) (Mock.builtinMap [])) assertEqual "" (Just [expect]) actual - , testCase "\\equals(false, X in [(Y, a)]) = \\not \\equals(X, Y)" $ do From 8340cafd9572b807ae4bdf3956bcb9f396325d22 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 20:24:28 +0300 Subject: [PATCH 16/29] Revert the "fix" for the first test --- kore/src/Kore/Builtin/Map.hs | 37 +++++++++---------- .../Test/Kore/Step/Simplification/AndTerms.hs | 2 +- 2 files changed, 19 insertions(+), 20 deletions(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 3c227aca51..872407a829 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -657,24 +657,23 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = <$> Domain.getConcreteKeysOfAc normalizedMap mapKeys = symbolicKeys <> concreteKeys opaqueElements = Domain.opaque . Domain.unwrapAc $ normalizedMap - if null mapKeys then - return Pattern.top - else do - -- 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 + + 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/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 4ee0dec13f..631e784510 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -848,7 +848,7 @@ test_andTermsSimplification = & Pattern.withCondition concrete actual <- simplifyUnify concrete symbolic assertEqual "" ([expect], [expect]) actual - , testCase "\\equals(false, X in []) = \\top" $ do + , testCase "qq\\equals(false, X in []) = \\top" $ do let expect = Condition.top actual <- simplifyEquals From f7ce7a87052f6e28a9d8a434af83fd97bb942a53 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 20:26:02 +0300 Subject: [PATCH 17/29] Stylish --- kore/src/Kore/Builtin/Map.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 872407a829..410d03ab87 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -657,7 +657,7 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = <$> Domain.getConcreteKeysOfAc normalizedMap mapKeys = symbolicKeys <> concreteKeys opaqueElements = Domain.opaque . Domain.unwrapAc $ normalizedMap - + Monad.guard (not (null mapKeys) || (length opaqueElements > 1)) -- Concrete keys are constructor-like, therefore they are defined TermLike.assertConstructorLikeKeys concreteKeys $ return () From 9916257172fdac567fad0e4097803d3bf68657fb Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 21:07:29 +0300 Subject: [PATCH 18/29] Find better fix --- kore/src/Kore/Builtin/Map.hs | 38 +++++++++++++++++++----------------- 1 file changed, 20 insertions(+), 18 deletions(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 410d03ab87..10582495d9 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -657,23 +657,25 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = <$> Domain.getConcreteKeysOfAc normalizedMap mapKeys = symbolicKeys <> concreteKeys opaqueElements = Domain.opaque . Domain.unwrapAc $ normalizedMap - - 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 + 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 From f43223fa9e1372cbb53296827e4e9b8d840d9359 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 20 Aug 2020 23:27:12 +0300 Subject: [PATCH 19/29] Addressed comments --- .../Test/Kore/Step/Simplification/AndTerms.hs | 183 +++++++++--------- 1 file changed, 91 insertions(+), 92 deletions(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 631e784510..63b4587b0d 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -848,98 +848,6 @@ test_andTermsSimplification = & Pattern.withCondition concrete actual <- simplifyUnify concrete symbolic assertEqual "" ([expect], [expect]) actual - , testCase "qq\\equals(false, X in []) = \\top" $ do - let expect = Condition.top - actual <- - simplifyEquals - mempty - (Mock.builtinBool False) - (Mock.inKeysMap (mkElemVar Mock.x) (Mock.builtinMap [])) - assertEqual "" (Just [expect]) actual - , testCase - "\\equals(false, X in [(Y, a)]) = \\not \\equals(X, Y)" - $ do - let expect = - makeEqualsPredicate_ - (mkElemVar Mock.x) - (mkElemVar Mock.y) - & makeNotPredicate - & Condition.fromPredicate - actual <- - simplifyEquals - mempty - ( Mock.builtinBool False ) - ( Mock.inKeysMap - ( mkElemVar Mock.x) - ( Mock.builtinMap - [ ( mkElemVar Mock.y, Mock.a ) ] - ) - ) - assertEqual "" (Just [expect]) actual - , testCase - "\\equals(false, X in [Y Z])\ - \ = \\not \\equals(X, Y) \\and \\not \\equals(X, Z)" - $ 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.inKeysMap - ( mkElemVar Mock.x ) - ( Mock.builtinMap - [ ( mkElemVar Mock.y, Mock.a ) - , ( mkElemVar Mock.z, Mock.a ) - ] - ) - ) - assertEqual "" (Just [expect]) actual - , testCase "\\equals(false, f(X) in [Y]) = \\not \\equals(f(X), Y)" $ 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.inKeysMap - ( Mock.f (mkElemVar Mock.x) ) - ( Mock.builtinMap - [ (mkElemVar Mock.y, Mock.a ) ] - ) - ) - assertEqual "" (Just [expect]) actual ] , testGroup "builtin List domain" @@ -1304,6 +1212,97 @@ test_equalsTermsSimplification = & Condition.fromPredicate actual <- simplifyEquals mempty concrete symbolic assertEqual "" (Just [expect]) actual + , testCase "\\equals(false, X in []) = \\top" $ do + let expect = Condition.top + actual <- + simplifyEquals + mempty + (Mock.builtinBool False) + (Mock.inKeysMap (mkElemVar Mock.x) (Mock.builtinMap [])) + assertEqual "" (Just [expect]) actual + , testCase "\\equals(false, X in [(Y, a)]) = \\not \\equals(X, Y)" $ do + let expect = + makeEqualsPredicate_ + (mkElemVar Mock.x) + (mkElemVar Mock.y) + & makeNotPredicate + & Condition.fromPredicate + actual <- + simplifyEquals + mempty + ( Mock.builtinBool False ) + ( Mock.inKeysMap + ( mkElemVar Mock.x) + ( Mock.builtinMap + [ ( mkElemVar Mock.y, Mock.a ) ] + ) + ) + assertEqual "" (Just [expect]) actual + , testCase + "\\equals(false, X in [Y Z])\ + \ = \\not \\equals(X, Y) \\and \\not \\equals(X, Z)\ + \ \\and \\not \\equals(Y, Z)" + $ 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.inKeysMap + ( mkElemVar Mock.x ) + ( Mock.builtinMap + [ ( mkElemVar Mock.y, Mock.a ) + , ( mkElemVar Mock.z, Mock.a ) + ] + ) + ) + assertEqual "" (Just [expect]) actual + , testCase "\\equals(false, f(X) in [Y]) = \\not \\equals(f(X), Y)" $ 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.inKeysMap + ( Mock.f (mkElemVar Mock.x) ) + ( Mock.builtinMap + [ (mkElemVar Mock.y, Mock.a ) ] + ) + ) + assertEqual "" (Just [expect]) actual ] ] From 87e7f11379ad17acb7279d86e5af102b245a3639 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Fri, 21 Aug 2020 12:21:15 +0300 Subject: [PATCH 20/29] Empty set test + fix --- kore/src/Kore/Builtin/Map.hs | 6 ++++- kore/src/Kore/Builtin/Set.hs | 27 ++++++++++++------- kore/test/Test/Kore/Step/MockSymbols.hs | 4 +-- .../Test/Kore/Step/Simplification/AndTerms.hs | 20 ++++++++------ 4 files changed, 37 insertions(+), 20 deletions(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index a942bb303a..3361468180 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -598,4 +598,8 @@ unifyNotInKeys -> TermLike variable -> TermLike variable -> MaybeT unifier (Pattern variable) -unifyNotInKeys = Set.unifyNotInKeys matchInKeys (inject . InKeys) +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 51e8bac3fe..f60a7b78c1 100644 --- a/kore/src/Kore/Builtin/Set.hs +++ b/kore/src/Kore/Builtin/Set.hs @@ -636,27 +636,36 @@ unifyNotIn -> TermLike variable -> TermLike variable -> MaybeT unifier (Pattern variable) -unifyNotIn = unifyNotInKeys matchSetIn (inject . In) +unifyNotIn = + unifyNotInKeys + (Ac.toNormalized @Domain.NormalizedSet) + matchSetIn + (inject . In) unifyNotInKeys - :: forall variable unifier + :: forall normalized variable unifier . InternalVariable variable + => Ac.TermWrapper normalized => MonadUnify unifier - => (TermLike variable -> Maybe (InKeys (TermLike variable))) + => (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 matchInKeys inject' unifyChildren (NotSimplifier notSimplifier) a b = +unifyNotInKeys + normalizedOrBottom + matchInKeys + inject' + 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 diff --git a/kore/test/Test/Kore/Step/MockSymbols.hs b/kore/test/Test/Kore/Step/MockSymbols.hs index 1ef422bdb0..88650f4d4b 100644 --- a/kore/test/Test/Kore/Step/MockSymbols.hs +++ b/kore/test/Test/Kore/Step/MockSymbols.hs @@ -632,7 +632,7 @@ unitSetSymbol = inSetSymbol :: Internal.Symbol inSetSymbol = - symbol "inSet" [intSort, setSort] boolSort & hook "SET.in" + symbol "inSet" [testSort, setSort] boolSort & hook "SET.in" opaqueSetSymbol :: Symbol opaqueSetSymbol = @@ -1243,7 +1243,7 @@ inSet => TermLike variable -> TermLike variable -> TermLike variable -inSet e s = Internal.mkApplySymbol inSetSymbol [e, s] +inSet element set = Internal.mkApplySymbol inSetSymbol [element, set] opaqueSet :: InternalVariable variable diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 8afc1eb79f..2985a9de1a 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -9,14 +9,11 @@ module Test.Kore.Step.Simplification.AndTerms import Prelude.Kore -import Kore.Unparser - import Test.Tasty import Control.Error ( MaybeT (..) ) -import qualified Data.Foldable as Foldable import qualified Data.List as List import qualified Data.Map.Strict as Map import qualified Data.Set as Set @@ -37,7 +34,6 @@ import Kore.Internal.Predicate , makeCeilPredicate , makeEqualsPredicate , makeEqualsPredicate_ - , makeMultipleAndPredicate , makeNotPredicate , makeTruePredicate ) @@ -71,9 +67,6 @@ import Kore.Syntax.Sentence import qualified Kore.Unification.UnifierT as Monad.Unify import Test.Kore -import Test.Kore.Builtin.Definition - ( inSetSymbol - ) import qualified Test.Kore.Step.MockSymbols as Mock import Test.Kore.Step.Simplification import Test.Tasty.HUnit.Ext @@ -1290,7 +1283,7 @@ test_equalsTermsSimplification = (Mock.f (mkElemVar Mock.x)) ) ( makeEqualsPredicate_ - (mkElemVar Mock.y) + ( mkElemVar Mock.y ) ( Mock.f (mkElemVar Mock.x) ) ) ) @@ -1311,6 +1304,17 @@ test_equalsTermsSimplification = ) assertEqual "" (Just [expect]) actual ] + , testGroup "setbuiltin Set" + [ testCase "\\equals(false, X in []) = \\top" $ do + let expect = Condition.top + actual <- + simplifyEquals + mempty + (Mock.builtinBool False) + (Mock.inSet (mkElemVar Mock.x) (Mock.builtinSet [])) + assertEqual "" (Just [expect]) actual + + ] ] test_functionAnd :: [TestTree] From 51aab5d8820a2b28ef15fc91f56f3a595c3facaf Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Fri, 21 Aug 2020 12:31:32 +0300 Subject: [PATCH 21/29] Add tests --- .../Test/Kore/Step/Simplification/AndTerms.hs | 78 ++++++++++++++++++- 1 file changed, 77 insertions(+), 1 deletion(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 2985a9de1a..d617fc24f1 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -1313,7 +1313,83 @@ test_equalsTermsSimplification = (Mock.builtinBool False) (Mock.inSet (mkElemVar Mock.x) (Mock.builtinSet [])) assertEqual "" (Just [expect]) actual - + , testCase "\\equals(false, X in [Y]) = \\not \\equals(X, Y)" $ 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 + "\\equals(false, X in [Y Z])\ + \ = \\not \\equals(X, Y) \\and \\not \\equals(X, Z)\ + \ \\and \\not \\equals(Y, Z)" + $ 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 "\\equals(false, f(X) in [Y]) = \\not \\equals(f(X), Y)" $ 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 ] ] From 1633696a5e70c9772d6d8aceda544a3f2f70b266 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Fri, 21 Aug 2020 12:33:45 +0300 Subject: [PATCH 22/29] Fix test names --- kore/test/Test/Kore/Step/Simplification/AndTerms.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 63b4587b0d..3dffae909d 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -1239,7 +1239,7 @@ test_equalsTermsSimplification = ) assertEqual "" (Just [expect]) actual , testCase - "\\equals(false, X in [Y Z])\ + "\\equals(false, X in [(Y, a), (Z, a)])\ \ = \\not \\equals(X, Y) \\and \\not \\equals(X, Z)\ \ \\and \\not \\equals(Y, Z)" $ do @@ -1274,7 +1274,7 @@ test_equalsTermsSimplification = ) ) assertEqual "" (Just [expect]) actual - , testCase "\\equals(false, f(X) in [Y]) = \\not \\equals(f(X), Y)" $ do + , testCase "\\equals(false, f(X) in [(Y, a)]) = \\not \\equals(f(X), Y)" $ do let expect = makeAndPredicate ( makeNotPredicate From a974656801654f0b7ac211ee53a3a4722f264026 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Fri, 21 Aug 2020 12:40:05 +0300 Subject: [PATCH 23/29] Fix test group name --- kore/test/Test/Kore/Step/Simplification/AndTerms.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index c269e4145e..e3770b6410 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -1304,7 +1304,7 @@ test_equalsTermsSimplification = ) assertEqual "" (Just [expect]) actual ] - , testGroup "setbuiltin Set" + , testGroup "builtin Set" [ testCase "\\equals(false, X in []) = \\top" $ do let expect = Condition.top actual <- From 698038c809155b6ac7e2714a8b3b757465fc1b29 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Mon, 24 Aug 2020 14:00:25 +0300 Subject: [PATCH 24/29] Rename In to InSet --- kore/src/Kore/Builtin/Set.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs index f60a7b78c1..753847c2d3 100644 --- a/kore/src/Kore/Builtin/Set.hs +++ b/kore/src/Kore/Builtin/Set.hs @@ -606,19 +606,19 @@ data InKeys term = , keyTerm, mapTerm :: !term } -newtype In term = In { getIn :: InKeys term} +newtype InSet term = InSet { getIn :: InKeys term} instance InternalVariable variable - => Injection (TermLike variable) (In (TermLike variable)) + => Injection (TermLike variable) (InSet (TermLike variable)) where - inject ( In InKeys { symbol, keyTerm, mapTerm = setTerm } ) = + 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 $ In InKeys { symbol, keyTerm, mapTerm = setTerm } + return $ InSet InKeys { symbol, keyTerm, mapTerm = setTerm } retract _ = empty matchSetIn @@ -640,7 +640,7 @@ unifyNotIn = unifyNotInKeys (Ac.toNormalized @Domain.NormalizedSet) matchSetIn - (inject . In) + (inject . InSet) unifyNotInKeys :: forall normalized variable unifier From d2ddb6b8a2e9665dead2cf4fff5310d97dd11750 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Mon, 24 Aug 2020 17:57:17 +0300 Subject: [PATCH 25/29] Add tests: opaque --- .../Test/Kore/Step/Simplification/AndTerms.hs | 70 ++++++++++++++++++- 1 file changed, 69 insertions(+), 1 deletion(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 78d3d117fd..5472bb4645 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -1299,6 +1299,42 @@ 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 @@ -1376,12 +1412,44 @@ test_equalsTermsSimplification = actual <- simplifyEquals mempty - (Mock.builtinBool False) + ( 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 ] ] From 7f5214e34edcbccf74c6d174b687b3df6ee6e302 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 25 Aug 2020 16:44:32 -0500 Subject: [PATCH 26/29] unifyNotInKeys: Use one lift --- kore/src/Kore/Builtin/Set.hs | 55 ++++++++++++++++++++---------------- 1 file changed, 30 insertions(+), 25 deletions(-) diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs index 753847c2d3..b19b66f94f 100644 --- a/kore/src/Kore/Builtin/Set.hs +++ b/kore/src/Kore/Builtin/Set.hs @@ -666,25 +666,27 @@ unifyNotInKeys = worker a b <|> worker b a where - defineTerm :: TermLike variable -> MaybeT unifier (Condition variable) + defineTerm :: TermLike variable -> unifier (Condition variable) defineTerm termLike = makeEvaluateTermCeil SideCondition.topTODO Sort.predicateSort termLike >>= Unify.scatter - & lift 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) + fmap eraseTerm <$> Unify.gather (unifyChildren t1 t2) notSimplifier SideCondition.top (OrPattern.fromPatterns unificationSolutions) - >>= Unify.scatter + >>= Unify.scatter collectConditions terms = Foldable.fold terms @@ -706,25 +708,28 @@ unifyNotInKeys <$> 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' inKeys { mapTerm = term }) - <$> opaqueElements - - opaqueConditions <- - lift $ traverse (unifyChildren termLike1) keyInKeysOpaque - let conditions = - fmap Pattern.withoutTerm (keyConditions <> opaqueConditions) - <> [definedKey, definedMap] - return $ collectConditions conditions + 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 + keyConditions <- traverse (unifyAndNegate keyTerm) mapKeys + + let keyInKeysOpaque = + (\term -> inject' inKeys { mapTerm = term }) + <$> opaqueElements + + opaqueConditions <- + traverse (unifyChildren termLike1) keyInKeysOpaque + let conditions = + fmap Pattern.withoutTerm + (keyConditions <> opaqueConditions) + <> [definedKey, definedMap] + return $ collectConditions conditions worker _ _ = empty From d7f74afe69bebcd2a59ff80e82ce0983b108cbb4 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 25 Aug 2020 16:53:22 -0500 Subject: [PATCH 27/29] unifyNotInKeys: Refactor --- kore/src/Kore/Builtin/Set.hs | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs index b19b66f94f..4feddd6d1c 100644 --- a/kore/src/Kore/Builtin/Set.hs +++ b/kore/src/Kore/Builtin/Set.hs @@ -55,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 ) @@ -688,10 +689,6 @@ unifyNotInKeys (OrPattern.fromPatterns unificationSolutions) >>= Unify.scatter - collectConditions terms = - Foldable.fold terms - & Pattern.fromCondition_ - worker :: TermLike variable -> TermLike variable @@ -718,18 +715,22 @@ unifyNotInKeys lift $ do definedKey <- defineTerm keyTerm definedMap <- defineTerm mapTerm - keyConditions <- traverse (unifyAndNegate keyTerm) mapKeys - - let keyInKeysOpaque = - (\term -> inject' inKeys { mapTerm = term }) - <$> opaqueElements - - opaqueConditions <- - traverse (unifyChildren termLike1) keyInKeysOpaque - let conditions = - fmap Pattern.withoutTerm - (keyConditions <> opaqueConditions) - <> [definedKey, definedMap] - return $ collectConditions conditions + notInKnownKeys <- + traverse (unifyAndNegate keyTerm) mapKeys + & fmap (map Pattern.withoutTerm) + notInOpaqueMaps <- + Traversable.for opaqueElements + (\term -> + unifyChildren + termLike1 + (inject' inKeys { mapTerm = term }) + ) + & fmap (map Pattern.withoutTerm) + pure $ Pattern.fromCondition_ $ mconcat + [ mconcat notInKnownKeys + , mconcat notInOpaqueMaps + , definedKey + , definedMap + ] worker _ _ = empty From 306bab4b1af4b50a9b83004de01167e1ae3b7eb2 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 26 Aug 2020 09:21:18 -0500 Subject: [PATCH 28/29] Revert "unifyNotInKeys: Refactor" This reverts commit d7f74afe69bebcd2a59ff80e82ce0983b108cbb4. --- kore/src/Kore/Builtin/Set.hs | 35 +++++++++++++++++------------------ 1 file changed, 17 insertions(+), 18 deletions(-) diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs index 4feddd6d1c..b19b66f94f 100644 --- a/kore/src/Kore/Builtin/Set.hs +++ b/kore/src/Kore/Builtin/Set.hs @@ -55,7 +55,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 ) @@ -689,6 +688,10 @@ unifyNotInKeys (OrPattern.fromPatterns unificationSolutions) >>= Unify.scatter + collectConditions terms = + Foldable.fold terms + & Pattern.fromCondition_ + worker :: TermLike variable -> TermLike variable @@ -715,22 +718,18 @@ unifyNotInKeys lift $ do definedKey <- defineTerm keyTerm definedMap <- defineTerm mapTerm - notInKnownKeys <- - traverse (unifyAndNegate keyTerm) mapKeys - & fmap (map Pattern.withoutTerm) - notInOpaqueMaps <- - Traversable.for opaqueElements - (\term -> - unifyChildren - termLike1 - (inject' inKeys { mapTerm = term }) - ) - & fmap (map Pattern.withoutTerm) - pure $ Pattern.fromCondition_ $ mconcat - [ mconcat notInKnownKeys - , mconcat notInOpaqueMaps - , definedKey - , definedMap - ] + keyConditions <- traverse (unifyAndNegate keyTerm) mapKeys + + let keyInKeysOpaque = + (\term -> inject' inKeys { mapTerm = term }) + <$> opaqueElements + + opaqueConditions <- + traverse (unifyChildren termLike1) keyInKeysOpaque + let conditions = + fmap Pattern.withoutTerm + (keyConditions <> opaqueConditions) + <> [definedKey, definedMap] + return $ collectConditions conditions worker _ _ = empty From a0f688ef2c704c21a3301300b159509827b1aca6 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 26 Aug 2020 09:43:11 -0500 Subject: [PATCH 29/29] unifyNotInKeys: Refactor opaqueConditions --- kore/src/Kore/Builtin/Set.hs | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs index b19b66f94f..0e3c04c193 100644 --- a/kore/src/Kore/Builtin/Set.hs +++ b/kore/src/Kore/Builtin/Set.hs @@ -55,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 ) @@ -718,17 +719,18 @@ unifyNotInKeys lift $ do definedKey <- defineTerm keyTerm definedMap <- defineTerm mapTerm - keyConditions <- traverse (unifyAndNegate keyTerm) mapKeys - - let keyInKeysOpaque = - (\term -> inject' inKeys { mapTerm = term }) - <$> opaqueElements - - opaqueConditions <- - traverse (unifyChildren termLike1) keyInKeysOpaque + 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 = - fmap Pattern.withoutTerm - (keyConditions <> opaqueConditions) + notInKnownKeys <> notInOpaqueKeys <> [definedKey, definedMap] return $ collectConditions conditions