Drop setHasSize

not supported by solvers, nor it's likely it'll ever be

CHANGES.md

@@ -28,6 +28,13 @@
     we choose to follow SMTLib here for portability purposes. If you need separate overflow/underflow checking you can
     use the encodings from earlier implementations, please get in touch if this proves problematic.
 
+  * [BACKWARDS COMPATIBILITY] Dropped hasSize, which checked cardinality of sets. This call hasn't been supported by
+    z3 for some time, and its uses were thus limited, and behavior was problematic even when supported due to finiteness
+    issues.
+
+  * Removed 'Documentation.SBV.Examples.Lists.Nested'. It contained an example that was no longer supported
+    by z3, so no point in keeping it in the documentation.
+
 ### Version 10.2, 2023-06-09
 
   * Improve HLint pragmas. Thanks to George Thomas for the patch.

Data/SBV/Core/Symbolic.hs

@@ -536,7 +536,6 @@ data SetOp = SetEqual
            | SetSubset
            | SetDifference
            | SetComplement
-           | SetHasSize
         deriving (Eq, Ord, G.Data)
 
 -- The show instance for 'SetOp' is merely for debugging, we map them separately so
@@ -551,7 +550,6 @@ instance Show SetOp where
   show SetSubset     = "Set.subset"
   show SetDifference = "Set.difference"
   show SetComplement = "Set.complement"
-  show SetHasSize    = "Set.setHasSize"
 
 -- Show instance for 'Op'. Note that this is largely for debugging purposes, not used
 -- for being read by any tool.

Data/SBV/SMT/SMTLib2.hs

@@ -1057,7 +1057,6 @@ cvtExp curProgInfo caps rm tableMap functionMap expr@(SBVApp _ arguments) = sh e
         sh (SBVApp (SetOp SetSubset)     args)   = "(subset "       ++ unwords (map cvtSV args) ++ ")"
         sh (SBVApp (SetOp SetDifference) args)   = "(setminus "     ++ unwords (map cvtSV args) ++ ")"
         sh (SBVApp (SetOp SetComplement) args)   = "(complement "   ++ unwords (map cvtSV args) ++ ")"
-        sh (SBVApp (SetOp SetHasSize)    args)   = "(set-has-size " ++ unwords (map cvtSV args) ++ ")"
 
         sh (SBVApp (TupleConstructor 0)   [])    = "mkSBVTuple0"
         sh (SBVApp (TupleConstructor n)   args)  = "((as mkSBVTuple" ++ show n ++ " " ++ smtType (KTuple (map kindOf args)) ++ ") " ++ unwords (map cvtSV args) ++ ")"

Data/SBV/Set.hs

@@ -19,10 +19,6 @@
 -- which is something you cannot do in Haskell! Conversely, you cannot compute
 -- the size of a symbolic set (as it can be infinite!), nor you can turn
 -- it into a list or necessarily enumerate its elements.
---
--- __A note on cardinality__: You can indirectly talk about cardinality: 'Data.SBV.Set.hasSize'
--- can be used to state that the set is finite and has size @k@ for a user-specified symbolic
--- integer @k@.
 -----------------------------------------------------------------------------
 
 {-# LANGUAGE Rank2Types          #-}
@@ -42,7 +38,7 @@ module Data.SBV.Set (
         , insert, delete
 
         -- * Query
-        , member, notMember, null, isEmpty, isFull, isUniversal, hasSize, isSubsetOf, isProperSubsetOf, disjoint
+        , member, notMember, null, isEmpty, isFull, isUniversal, isSubsetOf, isProperSubsetOf, disjoint
 
         -- * Combinations
         , union, unions, intersection, intersections, difference, (\\)
@@ -310,49 +306,6 @@ isFull = (.== full)
 isUniversal :: HasKind a => SSet a -> SBool
 isUniversal = isFull
 
--- | Does the set have the given size? It implicitly asserts that the set
--- it is operating on is finite. NB. Only z3 supported this call, and as
--- discussed in http://github.com/Z3Prover/z3/issues/3854, recent versions
--- of z3 doesn't support size calls either. So, you can only use this if you have
--- a sufficiently old version of z3.
---
--- >>> prove $ \i -> hasSize (empty :: SSet Integer) i .== (i .== 0)
--- Q.E.D.
---
--- >>> sat $ \i -> hasSize (full :: SSet Integer) i
--- Unsatisfiable
---
--- The following tests are commented out since z3 no longer supports size:
---
--- > >>> prove $ \a b i j k -> hasSize (a :: SSet Integer) i .&& hasSize (b :: SSet Integer) j .&& hasSize (a `union` b) k .=> k .>= i `smax` j
--- > Q.E.D.
---
--- > >>> prove $ \a b i j k -> hasSize (a :: SSet Integer) i .&& hasSize (b :: SSet Integer) j .&& hasSize (a `intersection` b) k .=> k .<= i `smin` j
--- > Q.E.D.
---
--- > >>> prove $ \a k -> hasSize (a :: SSet Integer) k .=> k .>= 0
--- > Q.E.D.
-hasSize :: (Ord a, SymVal a) => SSet a -> SInteger -> SBool
-hasSize sa si
-  -- Case 1: Constant regular set, see if the size matches
-  | Just (RegularSet a) <- unliteral sa
-  = literal (fromIntegral (Set.size a)) .== si
-
-  -- Case 2: Constant complement set, will never have finite size
-  | Just (ComplementSet _) <- unliteral sa
-  = sFalse
-
-  -- Case 3: Integer is constant, and is negative:
-  | Just i <- unliteral si, i < 0
-  = sFalse
-
-  -- Otherwise, go symbolic
-  | True
-  = SBV $ SVal KBool $ Right $ cache r
-  where r st = do sva <- sbvToSV st sa
-                  svi <- sbvToSV st si
-                  newExpr st KBool $ SBVApp (SetOp SetHasSize) [sva, svi]
-
 -- | Subset test.
 --
 -- >>> prove $ empty `isSubsetOf` (full :: SSet Integer)