Merge pull request #2577 from ucsd-progsys/CVC5-cardinality

add CVC5 cardinality support

Author: nikivazou

liquid-fixpoint

@@ -113,6 +113,7 @@ wiredTheorySortedSyms =
       , "Set_sub"
       , "Set_add"
       , "Set_com"
+      , "Set_card"
 
       , "Bag_count"
       , "Bag_empty"

liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs

@@ -17,6 +17,7 @@ embed Set as Set_Set
 assume isSubsetOf    :: (Ord a) => x:(Set a) -> y:(Set a) -> {v:Bool | v <=> Set_sub x y}
 assume member        :: Ord a => x:a -> xs:(Set a) -> {v:Bool | v <=> Set_mem x xs}
 assume null          :: Ord a => xs:(Set a) -> {v:Bool | v <=> Set_emp xs}
+assume size          :: xs:(Set a) -> {v:Nat | v = Set_card xs}
 
 assume empty         :: {v:(Set a) | Set_emp v}
 assume singleton     :: x:a -> {v:(Set a) | v = (Set_sng x)}
@@ -44,6 +45,7 @@ define intersection x y = (Set_cap x y)
 define difference x y   = (Set_dif x y)
 define empty            = (Set_empty 0)
 define null x           = (Set_emp x)
+define size x           = (Set_card x)
 define member x xs      = (Set_mem x xs)
 define isSubsetOf x y   = (Set_sub x y)
 define fromList xs      = (Data.Set_LHAssumptions.listElts xs)

src/Data/Set_LHAssumptions.hs

@@ -0,0 +1,11 @@
+{-@ LIQUID "--expect-any-error" @-}
+{-@ LIQUID "--smtsolver=CVC5" @-}
+module Card where
+
+import Data.Set 
+import qualified Data.Set as Set
+
+
+{-@ insert :: x:Int -> xs:[Int] -> {v:[Int] | Set.size (Set.fromList v) == Set.size (Set.fromList xs)} @-} 
+insert :: Int -> [Int] -> [Int] 
+insert x xs = x:xs

tests/neg/Card.hs

@@ -0,0 +1,17 @@
+{-@ LIQUID "--smtsolver=CVC5" @-}
+module Card where
+
+import Data.Set 
+import qualified Data.Set as Set
+
+
+{-@ insert :: x:Int -> xs:[Int] -> {v:[Int] | Set.size (Set.fromList v) >= Set.size (Set.fromList xs)} @-} 
+insert :: Int -> [Int] -> [Int] 
+insert x xs = x:xs
+
+
+
+{-@ insert' :: x:Int -> xs:{[Int] | not (member x (fromList xs))} 
+            -> {v:[Int] | Set.size (Set.fromList v) = 1 + Set.size (Set.fromList xs)} @-} 
+insert' :: Int -> [Int] -> [Int] 
+insert' x xs = x:xs

tests/pos/Card.hs

@@ -1102,6 +1102,7 @@ executable unit-neg
                     , BigNum
                     , BinarySearchOverflow
                     , Books
+                    -- , Card
                     , CastedTotality
                     , CharLiterals
                     , CheckedNum
@@ -1440,6 +1441,7 @@ executable unit-pos-2
       buildable:      False
 
     other-modules:
+                     --  Card
                       ExactADT6
                     , ExactGADT0
                     , ExactGADT1