-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Uninterpreted.UISortAllSat
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates uninterpreted sorts and how all-sat behaves for them.
-- Thanks to Eric Seidel for the idea.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveDataTypeable #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Uninterpreted.UISortAllSat where

import Data.Generics
import Data.SBV

-- | A "list-like" data type, but one we plan to uninterpret at the SMT level.
-- The actual shape is really immaterial for us, but could be used as a proxy
-- to generate test cases or explore data-space in some other part of a program.
-- Note that we neither rely on the shape of this data, nor need the actual
-- constructors.
data L = Nil
       | Cons Int L
       deriving (L -> L -> Bool
(L -> L -> Bool) -> (L -> L -> Bool) -> Eq L
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: L -> L -> Bool
$c/= :: L -> L -> Bool
== :: L -> L -> Bool
$c== :: L -> L -> Bool
Eq, Eq L
Eq L =>
(L -> L -> Ordering)
-> (L -> L -> Bool)
-> (L -> L -> Bool)
-> (L -> L -> Bool)
-> (L -> L -> Bool)
-> (L -> L -> L)
-> (L -> L -> L)
-> Ord L
L -> L -> Bool
L -> L -> Ordering
L -> L -> L
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: L -> L -> L
$cmin :: L -> L -> L
max :: L -> L -> L
$cmax :: L -> L -> L
>= :: L -> L -> Bool
$c>= :: L -> L -> Bool
> :: L -> L -> Bool
$c> :: L -> L -> Bool
<= :: L -> L -> Bool
$c<= :: L -> L -> Bool
< :: L -> L -> Bool
$c< :: L -> L -> Bool
compare :: L -> L -> Ordering
$ccompare :: L -> L -> Ordering
$cp1Ord :: Eq L
Ord, Int -> L -> ShowS
[L] -> ShowS
L -> String
(Int -> L -> ShowS) -> (L -> String) -> ([L] -> ShowS) -> Show L
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [L] -> ShowS
$cshowList :: [L] -> ShowS
show :: L -> String
$cshow :: L -> String
showsPrec :: Int -> L -> ShowS
$cshowsPrec :: Int -> L -> ShowS
Show, ReadPrec [L]
ReadPrec L
Int -> ReadS L
ReadS [L]
(Int -> ReadS L)
-> ReadS [L] -> ReadPrec L -> ReadPrec [L] -> Read L
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [L]
$creadListPrec :: ReadPrec [L]
readPrec :: ReadPrec L
$creadPrec :: ReadPrec L
readList :: ReadS [L]
$creadList :: ReadS [L]
readsPrec :: Int -> ReadS L
$creadsPrec :: Int -> ReadS L
Read, Typeable L
DataType
Constr
Typeable L =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> L -> c L)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c L)
-> (L -> Constr)
-> (L -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c L))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c L))
-> ((forall b. Data b => b -> b) -> L -> L)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> L -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> L -> r)
-> (forall u. (forall d. Data d => d -> u) -> L -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> L -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> L -> m L)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> L -> m L)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> L -> m L)
-> Data L
L -> DataType
L -> Constr
(forall b. Data b => b -> b) -> L -> L
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> L -> c L
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c L
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> L -> u
forall u. (forall d. Data d => d -> u) -> L -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> L -> m L
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> L -> m L
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c L
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> L -> c L
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c L)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c L)
$cCons :: Constr
$cNil :: Constr
$tL :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> L -> m L
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> L -> m L
gmapMp :: (forall d. Data d => d -> m d) -> L -> m L
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> L -> m L
gmapM :: (forall d. Data d => d -> m d) -> L -> m L
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> L -> m L
gmapQi :: Int -> (forall d. Data d => d -> u) -> L -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> L -> u
gmapQ :: (forall d. Data d => d -> u) -> L -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> L -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
gmapT :: (forall b. Data b => b -> b) -> L -> L
$cgmapT :: (forall b. Data b => b -> b) -> L -> L
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c L)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c L)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c L)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c L)
dataTypeOf :: L -> DataType
$cdataTypeOf :: L -> DataType
toConstr :: L -> Constr
$ctoConstr :: L -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c L
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c L
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> L -> c L
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> L -> c L
$cp1Data :: Typeable L
Data)

-- | Declare instances to make 'L' a usable uninterpreted sort. First we need the
-- 'SymVal' instance, with the default definition sufficing.
instance SymVal L

-- | Similarly, 'HasKind's default implementation is sufficient.
instance HasKind L

-- | An uninterpreted "classify" function. Really, we only care about
-- the fact that such a function exists, not what it does.
classify :: SBV L -> SInteger
classify :: SBV L -> SInteger
classify = String -> SBV L -> SInteger
forall a. Uninterpreted a => String -> a
uninterpret "classify"

-- | Formulate a query that essentially asserts a cardinality constraint on
-- the uninterpreted sort 'L'. The goal is to say there are precisely 3
-- such things, as it might be the case. We manage this by declaring four
-- elements, and asserting that for a free variable of this sort, the
-- shape of the data matches one of these three instances. That is, we
-- assert that all the instances of the data 'L' can be classified into
-- 3 equivalence classes. Then, allSat returns all the possible instances,
-- which of course are all uninterpreted.
--
-- As expected, we have:
--
-- >>> allSat genLs
-- Solution #1:
--   l  = L!val!0 :: L
--   l0 = L!val!0 :: L
--   l1 = L!val!1 :: L
--   l2 = L!val!2 :: L
-- <BLANKLINE>
--   classify :: L -> Integer
--   classify L!val!2 = 2
--   classify L!val!1 = 1
--   classify _       = 0
-- Solution #2:
--   l  = L!val!1 :: L
--   l0 = L!val!0 :: L
--   l1 = L!val!1 :: L
--   l2 = L!val!2 :: L
-- <BLANKLINE>
--   classify :: L -> Integer
--   classify L!val!2 = 2
--   classify L!val!1 = 1
--   classify _       = 0
-- Solution #3:
--   l  = L!val!2 :: L
--   l0 = L!val!0 :: L
--   l1 = L!val!1 :: L
--   l2 = L!val!2 :: L
-- <BLANKLINE>
--   classify :: L -> Integer
--   classify L!val!2 = 2
--   classify L!val!1 = 1
--   classify _       = 0
-- Found 3 different solutions.
genLs :: Predicate
genLs :: Predicate
genLs = do [l :: SBV L
l, l0 :: SBV L
l0, l1 :: SBV L
l1, l2 :: SBV L
l2] <- [String] -> Symbolic [SBV L]
forall a. SymVal a => [String] -> Symbolic [SBV a]
symbolics ["l", "l0", "l1", "l2"]
           SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV L -> SInteger
classify SBV L
l0 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 0
           SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV L -> SInteger
classify SBV L
l1 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 1
           SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV L -> SInteger
classify SBV L
l2 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 2
           SBool -> Predicate
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> Predicate) -> SBool -> Predicate
forall a b. (a -> b) -> a -> b
$ SBV L
l SBV L -> SBV L -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV L
l0 SBool -> SBool -> SBool
.|| SBV L
l SBV L -> SBV L -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV L
l1 SBool -> SBool -> SBool
.|| SBV L
l SBV L -> SBV L -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV L
l2