{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Uninterpreted.UISortAllSat where
import Data.Generics
import Data.SBV
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)
instance SymVal L
instance HasKind L
classify :: SBV L -> SInteger
classify :: SBV L -> SInteger
classify = String -> SBV L -> SInteger
forall a. Uninterpreted a => String -> a
uninterpret "classify"
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