Implement SET.intersection

docs/hooks.md

@@ -592,6 +592,15 @@ The union of both arguments.
         [hook{}("SET.concat")]
 ~~~
 
+### SET.intersection
+
+The intersection of both arguments
+
+~~~
+    hooked-symbol intersect{}(Set{}, Set{}) : Set{}
+        [hook{}("SET.intersection")]
+~~~
+
 ### SET.in
 
 Is the element a member of the given set?

kore/src/Kore/Builtin/Set.hs

@@ -39,6 +39,7 @@ module Kore.Builtin.Set
     , differenceKey
     , toListKey
     , sizeKey
+    , intersectionKey
       -- * Unification
     , unifyEquals
     ) where
@@ -171,6 +172,9 @@ symbolVerifiers =
     , ( sizeKey
       , Builtin.verifySymbol Int.assertSort [assertSort]
       )
+    , ( intersectionKey
+      , Builtin.verifySymbol assertSort [assertSort, assertSort]
+      )
     ]
 
 type Builtin = Set (TermLike Concrete)
@@ -350,6 +354,22 @@ evalSize = Builtin.functionEvaluator evalSize0
                 . Set.size
                 $ _set
 
+evalIntersection :: Builtin.Function
+evalIntersection =
+    Builtin.functionEvaluator evalIntersection0
+  where
+    ctx = intersectionKey
+    evalIntersection0 :: Builtin.FunctionImplementation
+    evalIntersection0 tools _ resultSort = \arguments ->
+        Builtin.getAttemptedAxiom $ do
+            let (_set1, _set2) =
+                    case arguments of
+                        [_set1, _set2] -> (_set1, _set2)
+                        _ -> Builtin.wrongArity intersectionKey
+            _set1 <- expectBuiltinSet ctx tools _set1
+            _set2 <- expectBuiltinSet ctx tools _set2
+            returnSet tools resultSort (Set.intersection _set1 _set2)
+
 {- | Implement builtin function evaluation.
  -}
 builtinFunctions :: Map Text Builtin.Function
@@ -362,6 +382,7 @@ builtinFunctions =
         , (differenceKey, evalDifference)
         , (toListKey, evalToList)
         , (sizeKey, evalSize)
+        , (intersectionKey, evalIntersection)
         ]
 
 {- | Render a 'Set' as an internal domain value pattern of the given sort.
@@ -452,6 +473,9 @@ toListKey = "SET.set2list"
 sizeKey :: IsString s => s
 sizeKey = "SET.size"
 
+intersectionKey :: IsString s => s
+intersectionKey = "SET.intersection"
+
 {- | Find the symbol hooked to @SET.get@ in an indexed module.
  -}
 lookupSymbolIn

kore/test/Test/Kore/Builtin/Definition.hs

@@ -269,6 +269,9 @@ pairSymbol lSort rSort =
 unitSetSymbol :: SymbolOrAlias
 unitSetSymbol = builtinSymbol "unitSet"
 
+unitSet :: TermLike Variable
+unitSet = mkApp setSort unitSetSymbol []
+
 elementSetSymbol :: SymbolOrAlias
 elementSetSymbol = builtinSymbol "elementSet"
 
@@ -287,6 +290,16 @@ toListSetSymbol = builtinSymbol "toListSet"
 sizeSetSymbol :: SymbolOrAlias
 sizeSetSymbol = builtinSymbol "sizeSet"
 
+intersectionSetSymbol :: SymbolOrAlias
+intersectionSetSymbol = builtinSymbol "intersectionSet"
+
+intersectionSet
+    :: TermLike Variable
+    -> TermLike Variable
+    -> TermLike Variable
+intersectionSet set1 set2 =
+    mkApp setSort intersectionSetSymbol [set1, set2]
+
 -- ** String
 
 ltStringSymbol :: SymbolOrAlias
@@ -1112,6 +1125,11 @@ setModule =
                 intSort
                 [setSort]
                 [hookAttribute Set.sizeKey]
+            , hookedSymbolDecl
+                intersectionSetSymbol
+                setSort
+                [setSort, setSort]
+                [hookAttribute Set.intersectionKey]
             ]
         }
 

kore/test/Test/Kore/Builtin/Set.hs

@@ -218,6 +218,27 @@ test_size =
             (===) Pattern.top =<< evaluate predicate
         )
 
+test_intersection_unit :: TestTree
+test_intersection_unit =
+    testPropertyWithSolver "intersection(as, unit()) === unit()" $ do
+        as <- forAll genSetPattern
+        let
+            original = intersectionSet as unitSet
+            expect = Pattern.fromTermLike (asInternal Set.empty)
+        (===) expect      =<< evaluate original
+        (===) Pattern.top =<< evaluate (mkEquals_ original unitSet)
+
+test_intersection_idem :: TestTree
+test_intersection_idem =
+    testPropertyWithSolver "intersection(as, as) === as" $ do
+        as <- forAll genConcreteSet
+        let
+            termLike = asTermLike as
+            original = intersectionSet termLike termLike
+            expect = Pattern.fromTermLike (asInternal as)
+        (===) expect      =<< evaluate original
+        (===) Pattern.top =<< evaluate (mkEquals_ original termLike)
+
 setVariableGen :: Sort -> Gen (Set Variable)
 setVariableGen sort =
     Gen.set (Range.linear 0 32) (standaloneGen $ variableGen sort)