From 0fe12327675b645c9df2e52d30df89d055551e38 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Wed, 22 Nov 2023 10:39:07 -0800
Subject: [PATCH] Drop tests that are not supported by solvers

---
 Data/SBV/List.hs                           |  6 ---
 Data/SBV/String.hs                         |  6 ---
 Documentation/SBV/Examples/Lists/Nested.hs | 45 ----------------------
 sbv.cabal                                  |  1 -
 4 files changed, 58 deletions(-)
 delete mode 100644 Documentation/SBV/Examples/Lists/Nested.hs

diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs
index 519adb0c3..a1be62b58 100644
--- a/Data/SBV/List.hs
+++ b/Data/SBV/List.hs
@@ -157,9 +157,6 @@ listToListAt s offset = subList s offset 1
 --
 -- >>> prove $ \i -> i `inRange` (0, 4) .=> [1,1,1,1,1] `elemAt` i .== (1::SInteger)
 -- Q.E.D.
---
--- ->>> prove $ \(l :: SList Integer) i e -> i `inRange` (0, length l - 1) .&& l `elemAt` i .== e .=> indexOf l (singleton e) .<= i
--- Q.E.D.
 elemAt :: SymVal a => SList a -> SInteger -> SBV a
 elemAt l i
   | Just xs <- unliteral l, Just ci <- unliteral i, ci >= 0, ci < genericLength xs, let x = xs `genericIndex` ci
@@ -330,9 +327,6 @@ replace l src dst
 -- | @`indexOf` l sub@. Retrieves first position of @sub@ in @l@, @-1@ if there are no occurrences.
 -- Equivalent to @`offsetIndexOf` l sub 0@.
 --
--- ->>> prove $ \(l :: SList Int8) i -> i .> 0 .&& i .< length l .=> indexOf l (subList l i 1) .<= i
--- Q.E.D.
---
 -- >>> prove $ \(l1 :: SList Word16) l2 -> length l2 .> length l1 .=> indexOf l1 l2 .== -1
 -- Q.E.D.
 indexOf :: (Eq a, SymVal a) => SList a -> SList a -> SInteger
diff --git a/Data/SBV/String.hs b/Data/SBV/String.hs
index e311f47a2..f8c517335 100644
--- a/Data/SBV/String.hs
+++ b/Data/SBV/String.hs
@@ -145,9 +145,6 @@ strToStrAt s offset = subStr s offset 1
 --
 -- >>> prove $ \i -> i .>= 0 .&& i .<= 4 .=> "AAAAA" `strToCharAt` i .== literal 'A'
 -- Q.E.D.
---
--- ->>> prove $ \s i c -> i `inRange` (0, length s - 1) .&& s `strToCharAt` i .== c .=> indexOf s (singleton c) .<= i
--- Q.E.D.
 strToCharAt :: SString -> SInteger -> SChar
 strToCharAt s i
   | Just cs <- unliteral s, Just ci <- unliteral i, ci >= 0, ci < genericLength cs, let c = C.ord (cs `genericIndex` ci)
@@ -314,9 +311,6 @@ replace s src dst
 -- | @`indexOf` s sub@. Retrieves first position of @sub@ in @s@, @-1@ if there are no occurrences.
 -- Equivalent to @`offsetIndexOf` s sub 0@.
 --
--- ->>> prove $ \s i -> i .> 0 .&& i .< length s .=> indexOf s (subStr s i 1) .<= i
--- Q.E.D.
---
 -- >>> prove $ \s1 s2 -> length s2 .> length s1 .=> indexOf s1 s2 .== -1
 -- Q.E.D.
 indexOf :: SString -> SString -> SInteger
diff --git a/Documentation/SBV/Examples/Lists/Nested.hs b/Documentation/SBV/Examples/Lists/Nested.hs
deleted file mode 100644
index bb57b3127..000000000
--- a/Documentation/SBV/Examples/Lists/Nested.hs
+++ /dev/null
@@ -1,45 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module    : Documentation.SBV.Examples.Lists.Nested
--- Copyright : (c) Levent Erkok
--- License   : BSD3
--- Maintainer: erkokl@gmail.com
--- Stability : experimental
---
--- Demonstrates nested lists
------------------------------------------------------------------------------
-
-{-# LANGUAGE OverloadedLists     #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-
-{-# OPTIONS_GHC -Wall -Werror #-}
-
-module Documentation.SBV.Examples.Lists.Nested where
-
-import Data.SBV
-import Data.SBV.Control
-
-import Prelude hiding ((!!))
-import Data.SBV.List ((!!))
-import qualified Data.SBV.List as L
-
--- | Simple example demonstrating the use of nested lists. We have:
---
--- Turned off. See: https://github.com/Z3Prover/z3/issues/2820
--- nestedExample
--- [[1,2,3],[4,5,6,7],[8,9,10],[11,12,13]]
-nestedExample :: IO ()
-nestedExample = runSMT $ do a :: SList [Integer] <- free "a"
-
-                            constrain $ a !! 0 .== [1, 2, 3]
-                            constrain $ a !! 1 .== [4, 5, 6, 7]
-                            constrain $ L.tail (L.tail a) .== [[8, 9, 10], [11, 12, 13]]
-                            constrain $ L.length a .== 4
-
-                            query $ do cs <- checkSat
-                                       case cs of
-                                         Unk    -> error "Solver said unknown!"
-                                         DSat{} -> error "Unexpected dsat result.."
-                                         Unsat  -> io $ putStrLn "Unsat"
-                                         Sat    -> do v <- getValue a
-                                                      io $ print v
diff --git a/sbv.cabal b/sbv.cabal
index bdaa1481c..d55accf13 100644
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -138,7 +138,6 @@ Library
                   , Documentation.SBV.Examples.Existentials.CRCPolynomial
                   , Documentation.SBV.Examples.Existentials.Diophantine
                   , Documentation.SBV.Examples.Lists.Fibonacci
-                  , Documentation.SBV.Examples.Lists.Nested
                   , Documentation.SBV.Examples.Lists.BoundedMutex
                   , Documentation.SBV.Examples.Lists.CountOutAndTransfer
                   , Documentation.SBV.Examples.Misc.Definitions