-----------------------------------------------------------------------------
-- |
-- 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 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 :: IO ()
nestedExample = Symbolic () -> IO ()
forall a. Symbolic a -> IO a
runSMT (Symbolic () -> IO ()) -> Symbolic () -> IO ()
forall a b. (a -> b) -> a -> b
$ do SList [Integer]
a :: SList [Integer] <- String -> Symbolic (SList [Integer])
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"a"

                            SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SList [Integer]
a SList [Integer] -> SInteger -> SBV [Integer]
forall a. SymVal a => SList a -> SInteger -> SBV a
.!! SInteger
0 SBV [Integer] -> SBV [Integer] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== [Item (SBV [Integer])
1, Item (SBV [Integer])
2, Item (SBV [Integer])
3]
                            SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SList [Integer]
a SList [Integer] -> SInteger -> SBV [Integer]
forall a. SymVal a => SList a -> SInteger -> SBV a
.!! SInteger
1 SBV [Integer] -> SBV [Integer] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== [Item (SBV [Integer])
4, Item (SBV [Integer])
5, Item (SBV [Integer])
6, Item (SBV [Integer])
7]
                            SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SList [Integer] -> SList [Integer]
forall a. SymVal a => SList a -> SList a
L.tail (SList [Integer] -> SList [Integer]
forall a. SymVal a => SList a -> SList a
L.tail SList [Integer]
a) SList [Integer] -> SList [Integer] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== [[Item [Integer]
8, Item [Integer]
9, Item [Integer]
10], [Item [Integer]
11, Item [Integer]
12, Item [Integer]
13]]
                            SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SList [Integer] -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList [Integer]
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
4

                            Query () -> Symbolic ()
forall a. Query a -> Symbolic a
query (Query () -> Symbolic ()) -> Query () -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
                                       case CheckSatResult
cs of
                                         CheckSatResult
Unk    -> String -> Query ()
forall a. HasCallStack => String -> a
error String
"Solver said unknown!"
                                         DSat{} -> String -> Query ()
forall a. HasCallStack => String -> a
error String
"Unexpected dsat result.."
                                         CheckSatResult
Unsat  -> IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Unsat"
                                         CheckSatResult
Sat    -> do [[Integer]]
v <- SList [Integer] -> Query [[Integer]]
forall a. SymVal a => SBV a -> Query a
getValue SList [Integer]
a
                                                      IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ [[Integer]] -> IO ()
forall a. Show a => a -> IO ()
print [[Integer]]
v