-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Uninterpreted.Sort
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates uninterpreted sorts, together with axioms.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Uninterpreted.Sort where

import Data.Generics
import Data.SBV

-- | A new data-type that we expect to use in an uninterpreted fashion
-- in the backend SMT solver. Note the custom @deriving@ clause, which
-- takes care of most of the boilerplate. The () field is needed so
-- SBV will not translate it to an enumerated data-type
newtype Q = Q () deriving (Q -> Q -> Bool
(Q -> Q -> Bool) -> (Q -> Q -> Bool) -> Eq Q
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Q -> Q -> Bool
$c/= :: Q -> Q -> Bool
== :: Q -> Q -> Bool
$c== :: Q -> Q -> Bool
Eq, Eq Q
Eq Q =>
(Q -> Q -> Ordering)
-> (Q -> Q -> Bool)
-> (Q -> Q -> Bool)
-> (Q -> Q -> Bool)
-> (Q -> Q -> Bool)
-> (Q -> Q -> Q)
-> (Q -> Q -> Q)
-> Ord Q
Q -> Q -> Bool
Q -> Q -> Ordering
Q -> Q -> Q
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 :: Q -> Q -> Q
$cmin :: Q -> Q -> Q
max :: Q -> Q -> Q
$cmax :: Q -> Q -> Q
>= :: Q -> Q -> Bool
$c>= :: Q -> Q -> Bool
> :: Q -> Q -> Bool
$c> :: Q -> Q -> Bool
<= :: Q -> Q -> Bool
$c<= :: Q -> Q -> Bool
< :: Q -> Q -> Bool
$c< :: Q -> Q -> Bool
compare :: Q -> Q -> Ordering
$ccompare :: Q -> Q -> Ordering
$cp1Ord :: Eq Q
Ord, Typeable Q
DataType
Constr
Typeable Q =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Q -> c Q)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Q)
-> (Q -> Constr)
-> (Q -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Q))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q))
-> ((forall b. Data b => b -> b) -> Q -> Q)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r)
-> (forall u. (forall d. Data d => d -> u) -> Q -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Q -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Q -> m Q)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Q -> m Q)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Q -> m Q)
-> Data Q
Q -> DataType
Q -> Constr
(forall b. Data b => b -> b) -> Q -> Q
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Q -> c Q
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Q
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) -> Q -> u
forall u. (forall d. Data d => d -> u) -> Q -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Q -> m Q
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Q -> m Q
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Q
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Q -> c Q
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Q)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q)
$cQ :: Constr
$tQ :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Q -> m Q
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Q -> m Q
gmapMp :: (forall d. Data d => d -> m d) -> Q -> m Q
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Q -> m Q
gmapM :: (forall d. Data d => d -> m d) -> Q -> m Q
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Q -> m Q
gmapQi :: Int -> (forall d. Data d => d -> u) -> Q -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Q -> u
gmapQ :: (forall d. Data d => d -> u) -> Q -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Q -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
gmapT :: (forall b. Data b => b -> b) -> Q -> Q
$cgmapT :: (forall b. Data b => b -> b) -> Q -> Q
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Q)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Q)
dataTypeOf :: Q -> DataType
$cdataTypeOf :: Q -> DataType
toConstr :: Q -> Constr
$ctoConstr :: Q -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Q
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Q
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Q -> c Q
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Q -> c Q
$cp1Data :: Typeable Q
Data, ReadPrec [Q]
ReadPrec Q
Int -> ReadS Q
ReadS [Q]
(Int -> ReadS Q)
-> ReadS [Q] -> ReadPrec Q -> ReadPrec [Q] -> Read Q
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Q]
$creadListPrec :: ReadPrec [Q]
readPrec :: ReadPrec Q
$creadPrec :: ReadPrec Q
readList :: ReadS [Q]
$creadList :: ReadS [Q]
readsPrec :: Int -> ReadS Q
$creadsPrec :: Int -> ReadS Q
Read, Int -> Q -> ShowS
[Q] -> ShowS
Q -> String
(Int -> Q -> ShowS) -> (Q -> String) -> ([Q] -> ShowS) -> Show Q
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Q] -> ShowS
$cshowList :: [Q] -> ShowS
show :: Q -> String
$cshow :: Q -> String
showsPrec :: Int -> Q -> ShowS
$cshowsPrec :: Int -> Q -> ShowS
Show, Typeable Q
HasKind Q
(HasKind Q, Typeable Q) =>
(forall (m :: * -> *).
 MonadSymbolic m =>
 Maybe Quantifier -> Maybe String -> m (SBV Q))
-> (Q -> SBV Q)
-> (CV -> Q)
-> (SBV Q -> (Q -> Bool) -> Bool)
-> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q))
-> (forall (m :: * -> *). MonadSymbolic m => m (SBV Q))
-> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q])
-> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q))
-> (forall (m :: * -> *). MonadSymbolic m => m (SBV Q))
-> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q])
-> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q))
-> (forall (m :: * -> *). MonadSymbolic m => m (SBV Q))
-> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q])
-> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q))
-> (forall (m :: * -> *). MonadSymbolic m => [String] -> m [SBV Q])
-> (SBV Q -> Maybe Q)
-> (SBV Q -> Bool)
-> (SBV Q -> Bool)
-> SymVal Q
CV -> Q
SBV Q -> Bool
SBV Q -> Maybe Q
SBV Q -> (Q -> Bool) -> Bool
Q -> SBV Q
forall a.
(HasKind a, Typeable a) =>
(forall (m :: * -> *).
 MonadSymbolic m =>
 Maybe Quantifier -> Maybe String -> m (SBV a))
-> (a -> SBV a)
-> (CV -> a)
-> (SBV a -> (a -> Bool) -> Bool)
-> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV a))
-> (forall (m :: * -> *). MonadSymbolic m => m (SBV a))
-> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV a])
-> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV a))
-> (forall (m :: * -> *). MonadSymbolic m => m (SBV a))
-> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV a])
-> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV a))
-> (forall (m :: * -> *). MonadSymbolic m => m (SBV a))
-> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV a])
-> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV a))
-> (forall (m :: * -> *). MonadSymbolic m => [String] -> m [SBV a])
-> (SBV a -> Maybe a)
-> (SBV a -> Bool)
-> (SBV a -> Bool)
-> SymVal a
forall (m :: * -> *). MonadSymbolic m => m (SBV Q)
forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q]
forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q)
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SBV Q]
forall (m :: * -> *).
MonadSymbolic m =>
Maybe Quantifier -> Maybe String -> m (SBV Q)
isSymbolic :: SBV Q -> Bool
$cisSymbolic :: SBV Q -> Bool
isConcrete :: SBV Q -> Bool
$cisConcrete :: SBV Q -> Bool
unliteral :: SBV Q -> Maybe Q
$cunliteral :: SBV Q -> Maybe Q
symbolics :: [String] -> m [SBV Q]
$csymbolics :: forall (m :: * -> *). MonadSymbolic m => [String] -> m [SBV Q]
symbolic :: String -> m (SBV Q)
$csymbolic :: forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q)
mkFreeVars :: Int -> m [SBV Q]
$cmkFreeVars :: forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q]
free_ :: m (SBV Q)
$cfree_ :: forall (m :: * -> *). MonadSymbolic m => m (SBV Q)
free :: String -> m (SBV Q)
$cfree :: forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q)
mkExistVars :: Int -> m [SBV Q]
$cmkExistVars :: forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q]
exists_ :: m (SBV Q)
$cexists_ :: forall (m :: * -> *). MonadSymbolic m => m (SBV Q)
exists :: String -> m (SBV Q)
$cexists :: forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q)
mkForallVars :: Int -> m [SBV Q]
$cmkForallVars :: forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q]
forall_ :: m (SBV Q)
$cforall_ :: forall (m :: * -> *). MonadSymbolic m => m (SBV Q)
forall :: String -> m (SBV Q)
$cforall :: forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q)
isConcretely :: SBV Q -> (Q -> Bool) -> Bool
$cisConcretely :: SBV Q -> (Q -> Bool) -> Bool
fromCV :: CV -> Q
$cfromCV :: CV -> Q
literal :: Q -> SBV Q
$cliteral :: Q -> SBV Q
mkSymVal :: Maybe Quantifier -> Maybe String -> m (SBV Q)
$cmkSymVal :: forall (m :: * -> *).
MonadSymbolic m =>
Maybe Quantifier -> Maybe String -> m (SBV Q)
$cp2SymVal :: Typeable Q
$cp1SymVal :: HasKind Q
SymVal, Q -> Bool
Q -> Int
Q -> String
Q -> Kind
(Q -> Kind)
-> (Q -> Bool)
-> (Q -> Int)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> Bool)
-> (Q -> String)
-> HasKind Q
forall a.
(a -> Kind)
-> (a -> Bool)
-> (a -> Int)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> Bool)
-> (a -> String)
-> HasKind a
showType :: Q -> String
$cshowType :: Q -> String
isEither :: Q -> Bool
$cisEither :: Q -> Bool
isMaybe :: Q -> Bool
$cisMaybe :: Q -> Bool
isTuple :: Q -> Bool
$cisTuple :: Q -> Bool
isSet :: Q -> Bool
$cisSet :: Q -> Bool
isList :: Q -> Bool
$cisList :: Q -> Bool
isString :: Q -> Bool
$cisString :: Q -> Bool
isChar :: Q -> Bool
$cisChar :: Q -> Bool
isUninterpreted :: Q -> Bool
$cisUninterpreted :: Q -> Bool
isUnbounded :: Q -> Bool
$cisUnbounded :: Q -> Bool
isDouble :: Q -> Bool
$cisDouble :: Q -> Bool
isFloat :: Q -> Bool
$cisFloat :: Q -> Bool
isReal :: Q -> Bool
$cisReal :: Q -> Bool
isBounded :: Q -> Bool
$cisBounded :: Q -> Bool
isBoolean :: Q -> Bool
$cisBoolean :: Q -> Bool
intSizeOf :: Q -> Int
$cintSizeOf :: Q -> Int
hasSign :: Q -> Bool
$chasSign :: Q -> Bool
kindOf :: Q -> Kind
$ckindOf :: Q -> Kind
HasKind)

-- | Declare an uninterpreted function that works over Q's
f :: SBV Q -> SBV Q
f :: SBV Q -> SBV Q
f = String -> SBV Q -> SBV Q
forall a. Uninterpreted a => String -> a
uninterpret "f"

-- | A satisfiable example, stating that there is an element of the domain
-- 'Q' such that 'f' returns a different element. Note that this is valid only
-- when the domain 'Q' has at least two elements. We have:
--
-- >>> t1
-- Satisfiable. Model:
--   x = Q!val!0 :: Q
-- <BLANKLINE>
--   f :: Q -> Q
--   f _ = Q!val!1
t1 :: IO SatResult
t1 :: IO SatResult
t1 = SymbolicT IO SBool -> IO SatResult
forall a. Provable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SBV Q
x <- String -> Symbolic (SBV Q)
forall a. SymVal a => String -> Symbolic (SBV a)
free "x"
              SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV Q -> SBV Q
f SBV Q
x SBV Q -> SBV Q -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Q
x

-- | This is a variant on the first example, except we also add an axiom
-- for the sort, stating that the domain 'Q' has only one element. In this case
-- the problem naturally becomes unsat. We have:
--
-- >>> t2
-- Unsatisfiable
t2 :: IO SatResult
t2 :: IO SatResult
t2 = SymbolicT IO SBool -> IO SatResult
forall a. Provable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SBV Q
x <- String -> Symbolic (SBV Q)
forall a. SymVal a => String -> Symbolic (SBV a)
free "x"
              String -> [String] -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => String -> [String] -> m ()
addAxiom "Q" ["(assert (forall ((x Q) (y Q)) (= x y)))"]
              SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV Q -> SBV Q
f SBV Q
x SBV Q -> SBV Q -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Q
x