SET.difference for symbolic values (#2011)

andreiburdusa · ttuegel · web-flow · commit d544b821dbde · 2020-08-05T16:04:39.000-05:00
* Implement SET.difference for symbolic values

* Test

* Pedantic

* Addressed comments

* evalDifference: Definedness conditions include all arguments

* Add Test.Kore.Builtin.Difference.differenceSet

* Add Test.Kore.Builtin.Definition.builtinSet

* Export Kore.Builtin.Set.evalDifference

* RED test_difference_symbolic: Fix test case

* Fix tests and copy differenceSet's implementation to fix builtin implementation

* Lint

* Use applicationEvaluator

* functionEvaluator: Implement in terms of applicationEvaluator

* test_difference_symbolic: Improve test names

* test_difference_symbolic: Refactor

* test_difference_symbolic: leaves empty set

* Add Kore.Domain.Builtin.nullAc

* AUR evalDifference

Co-authored-by: Thomas Tuegel &lt;thomas.tuegel@runtimeverification.com&gt;
diff --git a/kore/src/Kore/Builtin/Builtin.hs b/kore/src/Kore/Builtin/Builtin.hs
@@ -22,6 +22,7 @@ module Kore.Builtin.Builtin
     , binaryOperator
     , ternaryOperator
     , functionEvaluator
+    , applicationEvaluator
     , verifierBug
     , wrongArity
     , runParser
@@ -270,6 +271,21 @@ type Function
 
 functionEvaluator :: Function -> BuiltinAndAxiomSimplifier
 functionEvaluator impl =
+    applicationEvaluator $ \app -> do
+        let Application { applicationSymbolOrAlias = symbol } = app
+            Application { applicationChildren = args } = app
+            resultSort = symbolSorts symbol & applicationSortsResult
+        impl resultSort args
+
+applicationEvaluator
+    ::  ( forall variable simplifier
+        .  InternalVariable variable
+        => MonadSimplify simplifier
+        => Application Symbol (TermLike variable)
+        -> MaybeT simplifier (Pattern variable)
+        )
+    -> BuiltinAndAxiomSimplifier
+applicationEvaluator impl =
     applicationAxiomSimplifier evaluator
   where
     evaluator
@@ -280,12 +296,9 @@ functionEvaluator impl =
             (Attribute.Pattern variable)
             (TermLike variable)
         -> simplifier (AttemptedAxiom variable)
-    evaluator (valid :< app) = do
-        let args = map TermLike.removeEvaluated applicationChildren
-        getAttemptedAxiom (impl resultSort args >>= appliedFunction)
-      where
-        Application { applicationChildren } = app
-        Attribute.Pattern { Attribute.patternSort = resultSort } = valid
+    evaluator (_ :< app) = do
+        let app' = fmap TermLike.removeEvaluated app
+        getAttemptedAxiom (impl app' >>= appliedFunction)
 
 {- | Run a parser on a verified domain value.
 
diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs
@@ -27,6 +27,7 @@ module Kore.Builtin.Set
     , evalConcat
     , evalElement
     , evalUnit
+    , evalDifference
       -- * Unification
     , unifyEquals
     ) where
@@ -48,6 +49,7 @@ import Data.Map.Strict
     )
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq
+import qualified Data.Set as Set
 import Data.Text
     ( Text
     )
@@ -71,13 +73,17 @@ import qualified Kore.Domain.Builtin as Domain
 import Kore.IndexedModule.MetadataTools
     ( SmtMetadataTools
     )
+import Kore.Internal.ApplicationSorts
+    ( ApplicationSorts (..)
+    )
 import qualified Kore.Internal.Conditional as Conditional
 import Kore.Internal.Pattern
     ( Pattern
     )
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( makeCeilPredicate
+    , makeMultipleAndPredicate
     )
 import Kore.Internal.TermLike
     ( pattern App_
@@ -324,8 +330,18 @@ evalConcat resultSort [set1, set2] =
         (Ac.toNormalized set2)
 evalConcat _ _ = Builtin.wrongArity Set.concatKey
 
-evalDifference :: Builtin.Function
-evalDifference resultSort [_set1, _set2] = do
+evalDifference
+        :: forall variable simplifier
+        .  InternalVariable variable
+        => MonadSimplify simplifier
+        => TermLike.Application TermLike.Symbol (TermLike variable)
+        -> MaybeT simplifier (Pattern variable)
+evalDifference
+    ( TermLike.Application
+        symbol@TermLike.Symbol { symbolSorts = ApplicationSorts _ resultSort }
+        args@[_set1, _set2]
+    )
+  = do
     let rightIdentity = do
             _set2 <- expectConcreteBuiltinSet ctx _set2
             if Map.null _set2
@@ -335,10 +351,66 @@ evalDifference resultSort [_set1, _set2] = do
             _set1 <- expectConcreteBuiltinSet ctx _set1
             _set2 <- expectConcreteBuiltinSet ctx _set2
             returnConcreteSet resultSort (Map.difference _set1 _set2)
-    rightIdentity <|> bothConcrete
+        symbolic = do
+            _set1 <- expectBuiltinSet ctx _set1
+            _set2 <- expectBuiltinSet ctx _set2
+            let definedArgs =
+                    filter (not . TermLike.isDefinedPattern) args
+                    & map (makeCeilPredicate resultSort)
+                    & makeMultipleAndPredicate
+                    & Conditional.fromPredicate
+            let Domain.NormalizedAc
+                    { concreteElements = concrete1
+                    , elementsWithVariables = symbolic1'
+                    , opaque = opaque1'
+                    }
+                  = Domain.unwrapAc _set1
+                symbolic1 =
+                    Domain.unwrapElement <$> symbolic1'
+                    & Map.fromList
+                opaque1 = Set.fromList opaque1'
+            let Domain.NormalizedAc
+                    { concreteElements = concrete2
+                    , elementsWithVariables = symbolic2'
+                    , opaque = opaque2'
+                    }
+                  = Domain.unwrapAc _set2
+                symbolic2 =
+                    Domain.unwrapElement <$> symbolic2'
+                    & Map.fromList
+                opaque2 = Set.fromList opaque2'
+            let set1' =
+                    Domain.NormalizedAc
+                    { concreteElements = Map.difference concrete1 concrete2
+                    , elementsWithVariables =
+                        Map.difference symbolic1 symbolic2
+                        & Map.toList
+                        & map Domain.wrapElement
+                    , opaque = Set.difference opaque1 opaque2 & Set.toList
+                    }
+                set2' =
+                    Domain.NormalizedAc
+                    { concreteElements = Map.difference concrete2 concrete1
+                    , elementsWithVariables =
+                        Map.difference symbolic2 symbolic1
+                        & Map.toList
+                        & map Domain.wrapElement
+                    , opaque = Set.difference opaque1 opaque1 & Set.toList
+                    }
+            pat1 <- Ac.returnAc resultSort (Domain.NormalizedSet set1')
+            pat2 <- Ac.returnAc resultSort (Domain.NormalizedSet set2')
+            let pat
+                  | (not . Domain.nullAc) set1', (not . Domain.nullAc) set2' =
+                    differenceSet <$> pat1 <*> pat2
+                  | otherwise = pat1
+            return (Pattern.andCondition pat definedArgs)
+
+    rightIdentity <|> bothConcrete <|> symbolic
   where
     ctx = Set.differenceKey
-evalDifference _ _ = Builtin.wrongArity Set.differenceKey
+    differenceSet set1 set2 = TermLike.mkApplySymbol symbol [set1, set2]
+evalDifference _ =
+    Builtin.wrongArity Set.differenceKey
 
 evalToList :: Builtin.Function
 evalToList resultSort [_set] = do
@@ -399,7 +471,7 @@ builtinFunctions =
         , (Set.elementKey, Builtin.functionEvaluator evalElement)
         , (Set.unitKey, Builtin.functionEvaluator evalUnit)
         , (Set.inKey, Builtin.functionEvaluator evalIn)
-        , (Set.differenceKey, Builtin.functionEvaluator evalDifference)
+        , (Set.differenceKey, Builtin.applicationEvaluator evalDifference)
         , (Set.toListKey, Builtin.functionEvaluator evalToList)
         , (Set.sizeKey, Builtin.functionEvaluator evalSize)
         , (Set.intersectionKey, Builtin.functionEvaluator evalIntersection)
diff --git a/kore/src/Kore/Domain/Builtin.hs b/kore/src/Kore/Domain/Builtin.hs
@@ -18,6 +18,7 @@ module Kore.Domain.Builtin
     , wrapConcreteElement
     , InternalAc (..)
     , NormalizedAc (..)
+    , nullAc
     , emptyNormalizedAc
     , asSingleOpaqueElem
     , isSymbolicKeyOfAc
@@ -176,6 +177,12 @@ data NormalizedAc (collection :: Type -> Type -> Type) key child = NormalizedAc
     }
     deriving (GHC.Generic)
 
+nullAc :: NormalizedAc normalized key child -> Bool
+nullAc normalizedAc =
+    null (elementsWithVariables normalizedAc)
+    && null (concreteElements normalizedAc)
+    && null (opaque normalizedAc)
+
 isSymbolicKeyOfAc
     :: AcWrapper normalized
     => Eq child
diff --git a/kore/test/Test/Kore/Builtin/Definition.hs b/kore/test/Test/Kore/Builtin/Definition.hs
@@ -7,6 +7,7 @@ import Prelude.Kore
 
 import qualified Data.Bifunctor as Bifunctor
 import qualified Data.Default as Default
+import qualified Data.Foldable as Foldable
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq
 import Data.Text
@@ -32,6 +33,7 @@ import Kore.Attribute.Synthetic
     ( synthesize
     )
 import qualified Kore.Builtin as Builtin
+import qualified Kore.Builtin.Builtin as Builtin
 import qualified Kore.Builtin.Endianness as Endianness
 import qualified Kore.Builtin.Signedness as Signedness
 import Kore.Domain.Builtin
@@ -614,6 +616,12 @@ differenceSetSymbol :: Internal.Symbol
 differenceSetSymbol =
     binarySymbol "differenceSet" setSort & hook "SET.difference"
 
+differenceSet
+    :: TermLike VariableName
+    -> TermLike VariableName
+    -> TermLike VariableName
+differenceSet set1 set2 = mkApplySymbol differenceSetSymbol [set1, set2]
+
 toListSetSymbol :: Internal.Symbol
 toListSetSymbol =
     builtinSymbol "toListSet" listSort [setSort] & hook "SET.set2list"
@@ -1165,38 +1173,37 @@ testSortDecl :: ParsedSentence
 testSortDecl = sortDecl testSort
 
 builtinSet
-    :: [TermLike Concrete]
-    -> InternalSet (TermLike Concrete) (TermLike VariableName)
-builtinSet children =
-    InternalAc
+    :: InternalVariable variable
+    => Foldable f
+    => f (TermLike variable)
+    -> [TermLike variable]
+    -> TermLike variable
+builtinSet elements opaque =
+    mkBuiltin $ Domain.BuiltinSet Domain.InternalAc
         { builtinAcSort = setSort
         , builtinAcUnit = unitSetSymbol
         , builtinAcElement = elementSetSymbol
         , builtinAcConcat = concatSetSymbol
         , builtinAcChild = Domain.NormalizedSet Domain.NormalizedAc
-            { elementsWithVariables = []
-            , concreteElements =
-                Map.fromList (map (\x -> (x, SetValue)) children)
-            , opaque = []
-            }
-        }
-
-builtinSymbolicSet
-    :: [TermLike VariableName]
-    -> InternalSet key (TermLike VariableName)
-builtinSymbolicSet children =
-    InternalAc
-        { builtinAcSort = setSort
-        , builtinAcUnit = unitSetSymbol
-        , builtinAcElement = elementSetSymbolTestSort
-        , builtinAcConcat = concatSetSymbol
-        , builtinAcChild = Domain.NormalizedSet Domain.NormalizedAc
-            { elementsWithVariables =
-                fmap (\x -> wrapElement (x, SetValue)) children
-            , concreteElements = Map.empty
-            , opaque = []
+            { elementsWithVariables = Domain.wrapElement <$> abstractElements
+            , concreteElements
+            , opaque
             }
         }
+  where
+    asKey key =
+        (,) <$> Builtin.toKey key <*> pure Domain.SetValue
+        & maybe (Left (key, Domain.SetValue)) Right
+    (abstractElements, Map.fromList -> concreteElements) =
+        asKey <$> Foldable.toList elements
+        & partitionEithers
+
+builtinSet_
+    :: InternalVariable variable
+    => Foldable f
+    => f (TermLike variable)
+    -> TermLike variable
+builtinSet_ items = builtinSet items []
 
 -- ** String
 
diff --git a/kore/test/Test/Kore/Builtin/Map.hs b/kore/test/Test/Kore/Builtin/Map.hs
@@ -294,8 +294,8 @@ test_removeAll =
             when (set == Set.empty) discard
             let key = Set.elemAt 0 set
                 diffSet = Set.delete key set
-                patSet = Test.Set.asTermLike set
-                patDiffSet = Test.Set.asTermLike diffSet
+                patSet = builtinSet_ set & fromConcrete
+                patDiffSet = builtinSet_ diffSet & fromConcrete
                 patKey = fromConcrete key
                 patRemoveAll1 = removeAllMap map' patSet
                 patRemoveAll2 = removeAllMap
@@ -426,7 +426,7 @@ test_keysUnit =
             let
                 patUnit = unitMap
                 patKeys = keysMap patUnit
-                patExpect = Test.Set.asTermLike Set.empty
+                patExpect = builtinSet_ Set.empty
                 predicate = mkEquals_ patExpect patKeys
             expect <- evaluate patExpect
             assertEqual "" expect =<< evaluate patKeys
@@ -440,7 +440,7 @@ test_keysElement =
             key <- forAll genConcreteIntegerPattern
             val <- forAll genIntegerPattern
             let patMap = asTermLike $ Map.singleton key val
-                patKeys = Test.Set.asTermLike $ Set.singleton key
+                patKeys = builtinSet_ (Set.singleton key) & fromConcrete
                 patSymbolic = keysMap patMap
                 predicate = mkEquals_ patKeys patSymbolic
             expect <- evaluateT patKeys
@@ -455,7 +455,7 @@ test_keys =
         (do
             map1 <- forAll (genConcreteMap genIntegerPattern)
             let keys1 = Map.keysSet map1
-                patConcreteKeys = Test.Set.asTermLike keys1
+                patConcreteKeys = builtinSet_ keys1 & fromConcrete
                 patMap = asTermLike map1
                 patSymbolicKeys = keysMap patMap
                 predicate = mkEquals_ patConcreteKeys patSymbolicKeys
diff --git a/kore/test/Test/Kore/Builtin/Set.hs b/kore/test/Test/Kore/Builtin/Set.hs
