-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Transformers.SymbolicEval
-- Copyright : (c) Brian Schroeder
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A demonstration of the use of the 'SymbolicT' and 'QueryT' transformers in
-- the setting of symbolic program evaluation.
--
-- In this example, we perform symbolic evaluation across three steps:
--
-- 1. allocate free variables, so we can extract a model after evaluation
-- 2. perform symbolic evaluation of a program and an associated property
-- 3. querying the solver for whether it's possible to find a set of program
--    inputs that falsify the property. if there is, we extract a model.
--
-- To simplify the example, our programs always have exactly two integer inputs
-- named @x@ and @y@.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures             #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Transformers.SymbolicEval where

import Control.Monad.Except   (Except, ExceptT, MonadError, mapExceptT, runExceptT, throwError)
import Control.Monad.Identity (Identity(runIdentity))
import Control.Monad.IO.Class (MonadIO)
import Control.Monad.Reader   (MonadReader(reader), asks, ReaderT, runReaderT)
import Control.Monad.Trans    (lift)
import Data.Kind              (Type)

import Data.SBV.Dynamic   (SVal)
import Data.SBV.Internals (SBV(SBV), unSBV)
import Data.SBV.Trans.Control

-- Starting with base 4.16; Data.Bits exports And, which conflicts with the definition here
#if MIN_VERSION_base(4,16,0)
import Data.SBV.Trans hiding(And)
#else
import Data.SBV.Trans
#endif

-- * Allocation of symbolic variables, so we can extract a model later.

-- | Monad for allocating free variables.
newtype Alloc a = Alloc { forall a. Alloc a -> SymbolicT (ExceptT String IO) a
runAlloc :: SymbolicT (ExceptT String IO) a }
    deriving (forall a b. a -> Alloc b -> Alloc a
forall a b. (a -> b) -> Alloc a -> Alloc b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Alloc b -> Alloc a
$c<$ :: forall a b. a -> Alloc b -> Alloc a
fmap :: forall a b. (a -> b) -> Alloc a -> Alloc b
$cfmap :: forall a b. (a -> b) -> Alloc a -> Alloc b
Functor, Functor Alloc
forall a. a -> Alloc a
forall a b. Alloc a -> Alloc b -> Alloc a
forall a b. Alloc a -> Alloc b -> Alloc b
forall a b. Alloc (a -> b) -> Alloc a -> Alloc b
forall a b c. (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. Alloc a -> Alloc b -> Alloc a
$c<* :: forall a b. Alloc a -> Alloc b -> Alloc a
*> :: forall a b. Alloc a -> Alloc b -> Alloc b
$c*> :: forall a b. Alloc a -> Alloc b -> Alloc b
liftA2 :: forall a b c. (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
$cliftA2 :: forall a b c. (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
<*> :: forall a b. Alloc (a -> b) -> Alloc a -> Alloc b
$c<*> :: forall a b. Alloc (a -> b) -> Alloc a -> Alloc b
pure :: forall a. a -> Alloc a
$cpure :: forall a. a -> Alloc a
Applicative, Applicative Alloc
forall a. a -> Alloc a
forall a b. Alloc a -> Alloc b -> Alloc b
forall a b. Alloc a -> (a -> Alloc b) -> Alloc b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> Alloc a
$creturn :: forall a. a -> Alloc a
>> :: forall a b. Alloc a -> Alloc b -> Alloc b
$c>> :: forall a b. Alloc a -> Alloc b -> Alloc b
>>= :: forall a b. Alloc a -> (a -> Alloc b) -> Alloc b
$c>>= :: forall a b. Alloc a -> (a -> Alloc b) -> Alloc b
Monad, Monad Alloc
forall a. IO a -> Alloc a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> Alloc a
$cliftIO :: forall a. IO a -> Alloc a
MonadIO,
              MonadError String, MonadIO Alloc
Alloc State
forall (m :: * -> *). MonadIO m -> m State -> MonadSymbolic m
symbolicEnv :: Alloc State
$csymbolicEnv :: Alloc State
MonadSymbolic)

-- | Environment holding allocated variables.
data Env = Env { Env -> SBV Integer
envX   :: SBV Integer
               , Env -> SBV Integer
envY   :: SBV Integer
               , Env -> Maybe SVal
result :: Maybe SVal -- could be integer or bool. during
                                      -- program evaluation, this is Nothing.
                                      -- we only have a value during property
                                      -- evaluation.
               }
    deriving (Env -> Env -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Env -> Env -> Bool
$c/= :: Env -> Env -> Bool
== :: Env -> Env -> Bool
$c== :: Env -> Env -> Bool
Eq, Int -> Env -> ShowS
[Env] -> ShowS
Env -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Env] -> ShowS
$cshowList :: [Env] -> ShowS
show :: Env -> String
$cshow :: Env -> String
showsPrec :: Int -> Env -> ShowS
$cshowsPrec :: Int -> Env -> ShowS
Show)

-- | Allocate an integer variable with the provided name.
alloc :: String -> Alloc (SBV Integer)
alloc :: String -> Alloc (SBV Integer)
alloc String
"" = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"tried to allocate unnamed value"
alloc String
nm = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
free String
nm

-- | Allocate an 'Env' holding all input variables for the program.
allocEnv :: Alloc Env
allocEnv :: Alloc Env
allocEnv = do
    SBV Integer
x <- String -> Alloc (SBV Integer)
alloc String
"x"
    SBV Integer
y <- String -> Alloc (SBV Integer)
alloc String
"y"
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SBV Integer -> SBV Integer -> Maybe SVal -> Env
Env SBV Integer
x SBV Integer
y forall a. Maybe a
Nothing

-- * Symbolic term evaluation

-- | The term language we use to express programs and properties.
data Term :: Type -> Type where
    Var         :: String                       -> Term r
    Lit         :: Integer                      -> Term Integer
    Plus        :: Term Integer -> Term Integer -> Term Integer
    LessThan    :: Term Integer -> Term Integer -> Term Bool
    GreaterThan :: Term Integer -> Term Integer -> Term Bool
    Equals      :: Term Integer -> Term Integer -> Term Bool
    Not         :: Term Bool                    -> Term Bool
    Or          :: Term Bool    -> Term Bool    -> Term Bool
    And         :: Term Bool    -> Term Bool    -> Term Bool
    Implies     :: Term Bool    -> Term Bool    -> Term Bool

-- | Monad for performing symbolic evaluation.
newtype Eval a = Eval { forall a. Eval a -> ReaderT Env (Except String) a
unEval :: ReaderT Env (Except String) a }
    deriving (forall a b. a -> Eval b -> Eval a
forall a b. (a -> b) -> Eval a -> Eval b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Eval b -> Eval a
$c<$ :: forall a b. a -> Eval b -> Eval a
fmap :: forall a b. (a -> b) -> Eval a -> Eval b
$cfmap :: forall a b. (a -> b) -> Eval a -> Eval b
Functor, Functor Eval
forall a. a -> Eval a
forall a b. Eval a -> Eval b -> Eval a
forall a b. Eval a -> Eval b -> Eval b
forall a b. Eval (a -> b) -> Eval a -> Eval b
forall a b c. (a -> b -> c) -> Eval a -> Eval b -> Eval c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. Eval a -> Eval b -> Eval a
$c<* :: forall a b. Eval a -> Eval b -> Eval a
*> :: forall a b. Eval a -> Eval b -> Eval b
$c*> :: forall a b. Eval a -> Eval b -> Eval b
liftA2 :: forall a b c. (a -> b -> c) -> Eval a -> Eval b -> Eval c
$cliftA2 :: forall a b c. (a -> b -> c) -> Eval a -> Eval b -> Eval c
<*> :: forall a b. Eval (a -> b) -> Eval a -> Eval b
$c<*> :: forall a b. Eval (a -> b) -> Eval a -> Eval b
pure :: forall a. a -> Eval a
$cpure :: forall a. a -> Eval a
Applicative, Applicative Eval
forall a. a -> Eval a
forall a b. Eval a -> Eval b -> Eval b
forall a b. Eval a -> (a -> Eval b) -> Eval b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> Eval a
$creturn :: forall a. a -> Eval a
>> :: forall a b. Eval a -> Eval b -> Eval b
$c>> :: forall a b. Eval a -> Eval b -> Eval b
>>= :: forall a b. Eval a -> (a -> Eval b) -> Eval b
$c>>= :: forall a b. Eval a -> (a -> Eval b) -> Eval b
Monad, MonadReader Env, MonadError String)

-- | Unsafe cast for symbolic values. In production code, we would check types instead.
unsafeCastSBV :: SBV a -> SBV b
unsafeCastSBV :: forall a b. SBV a -> SBV b
unsafeCastSBV = forall a. SVal -> SBV a
SBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SBV a -> SVal
unSBV

-- | Symbolic evaluation function for 'Term'.
eval :: Term r -> Eval (SBV r)
eval :: forall r. Term r -> Eval (SBV r)
eval (Var String
"x")           = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall a b. SBV a -> SBV b
unsafeCastSBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> SBV Integer
envX
eval (Var String
"y")           = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall a b. SBV a -> SBV b
unsafeCastSBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> SBV Integer
envY
eval (Var String
"result")      = do Maybe SVal
mRes <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader Env -> Maybe SVal
result
                              case Maybe SVal
mRes of
                                Maybe SVal
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"unknown variable"
                                Just SVal
sv -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. SVal -> SBV a
SBV SVal
sv
eval (Var String
_)             = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"unknown variable"
eval (Lit Integer
i)             = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => a -> SBV a
literal Integer
i
eval (Plus        Term Integer
t1 Term Integer
t2) = forall a. Num a => a -> a -> a
(+)   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r. Term r -> Eval (SBV r)
eval Term Integer
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall r. Term r -> Eval (SBV r)
eval Term Integer
t2
eval (LessThan    Term Integer
t1 Term Integer
t2) = forall a. OrdSymbolic a => a -> a -> SBool
(.<)  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r. Term r -> Eval (SBV r)
eval Term Integer
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall r. Term r -> Eval (SBV r)
eval Term Integer
t2
eval (GreaterThan Term Integer
t1 Term Integer
t2) = forall a. OrdSymbolic a => a -> a -> SBool
(.>)  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r. Term r -> Eval (SBV r)
eval Term Integer
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall r. Term r -> Eval (SBV r)
eval Term Integer
t2
eval (Equals      Term Integer
t1 Term Integer
t2) = forall a. EqSymbolic a => a -> a -> SBool
(.==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r. Term r -> Eval (SBV r)
eval Term Integer
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall r. Term r -> Eval (SBV r)
eval Term Integer
t2
eval (Not         Term Bool
t)     = SBool -> SBool
sNot  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r. Term r -> Eval (SBV r)
eval Term Bool
t
eval (Or          Term Bool
t1 Term Bool
t2) = SBool -> SBool -> SBool
(.||) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r. Term r -> Eval (SBV r)
eval Term Bool
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall r. Term r -> Eval (SBV r)
eval Term Bool
t2
eval (And         Term Bool
t1 Term Bool
t2) = SBool -> SBool -> SBool
(.&&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r. Term r -> Eval (SBV r)
eval Term Bool
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall r. Term r -> Eval (SBV r)
eval Term Bool
t2
eval (Implies     Term Bool
t1 Term Bool
t2) = SBool -> SBool -> SBool
(.=>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r. Term r -> Eval (SBV r)
eval Term Bool
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall r. Term r -> Eval (SBV r)
eval Term Bool
t2

-- | Runs symbolic evaluation, sending a 'Term' to a symbolic value (or
-- failing). Used for symbolic evaluation of programs and properties.
runEval :: Env -> Term a -> Except String (SBV a)
runEval :: forall a. Env -> Term a -> Except String (SBV a)
runEval Env
env Term a
term = forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall a. Eval a -> ReaderT Env (Except String) a
unEval forall a b. (a -> b) -> a -> b
$ forall r. Term r -> Eval (SBV r)
eval Term a
term) Env
env

-- | A program that can reference two input variables, @x@ and @y@.
newtype Program a = Program (Term a)

-- | A symbolic value representing the result of running a program -- its
-- output.
newtype Result = Result SVal

-- | Makes a 'Result' from a symbolic value.
mkResult :: SBV a -> Result
mkResult :: forall a. SBV a -> Result
mkResult = SVal -> Result
Result forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SBV a -> SVal
unSBV

-- | Performs symbolic evaluation of a 'Program'.
runProgramEval :: Env -> Program a -> Except String Result
runProgramEval :: forall a. Env -> Program a -> Except String Result
runProgramEval Env
env (Program Term a
term) = forall a. SBV a -> Result
mkResult forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Env -> Term a -> Except String (SBV a)
runEval Env
env Term a
term

-- * Property evaluation

-- | A property describes a quality of a 'Program'. It is a 'Term' yields a
-- boolean value.
newtype Property = Property (Term Bool)

-- | Performs symbolic evaluation of a 'Property.
runPropertyEval :: Result -> Env -> Property -> Except String (SBV Bool)
runPropertyEval :: Result -> Env -> Property -> Except String SBool
runPropertyEval (Result SVal
res) Env
env (Property Term Bool
term) =
    forall a. Env -> Term a -> Except String (SBV a)
runEval (Env
env { result :: Maybe SVal
result = forall a. a -> Maybe a
Just SVal
res }) Term Bool
term

-- * Checking whether a program satisfies a property

-- | The result of 'check'ing the combination of a 'Program' and a 'Property'.
data CheckResult = Proved | Counterexample Integer Integer
    deriving (CheckResult -> CheckResult -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CheckResult -> CheckResult -> Bool
$c/= :: CheckResult -> CheckResult -> Bool
== :: CheckResult -> CheckResult -> Bool
$c== :: CheckResult -> CheckResult -> Bool
Eq, Int -> CheckResult -> ShowS
[CheckResult] -> ShowS
CheckResult -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CheckResult] -> ShowS
$cshowList :: [CheckResult] -> ShowS
show :: CheckResult -> String
$cshow :: CheckResult -> String
showsPrec :: Int -> CheckResult -> ShowS
$cshowsPrec :: Int -> CheckResult -> ShowS
Show)

-- | Sends an 'Identity' computation to an arbitrary monadic computation.
generalize :: Monad m => Identity a -> m a
generalize :: forall (m :: * -> *) a. Monad m => Identity a -> m a
generalize = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity

-- | Monad for querying a solver.
newtype Q a = Q { forall a. Q a -> QueryT (ExceptT String IO) a
runQ :: QueryT (ExceptT String IO) a }
    deriving (forall a b. a -> Q b -> Q a
forall a b. (a -> b) -> Q a -> Q b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Q b -> Q a
$c<$ :: forall a b. a -> Q b -> Q a
fmap :: forall a b. (a -> b) -> Q a -> Q b
$cfmap :: forall a b. (a -> b) -> Q a -> Q b
Functor, Functor Q
forall a. a -> Q a
forall a b. Q a -> Q b -> Q a
forall a b. Q a -> Q b -> Q b
forall a b. Q (a -> b) -> Q a -> Q b
forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. Q a -> Q b -> Q a
$c<* :: forall a b. Q a -> Q b -> Q a
*> :: forall a b. Q a -> Q b -> Q b
$c*> :: forall a b. Q a -> Q b -> Q b
liftA2 :: forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c
$cliftA2 :: forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c
<*> :: forall a b. Q (a -> b) -> Q a -> Q b
$c<*> :: forall a b. Q (a -> b) -> Q a -> Q b
pure :: forall a. a -> Q a
$cpure :: forall a. a -> Q a
Applicative, Applicative Q
forall a. a -> Q a
forall a b. Q a -> Q b -> Q b
forall a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> Q a
$creturn :: forall a. a -> Q a
>> :: forall a b. Q a -> Q b -> Q b
$c>> :: forall a b. Q a -> Q b -> Q b
>>= :: forall a b. Q a -> (a -> Q b) -> Q b
$c>>= :: forall a b. Q a -> (a -> Q b) -> Q b
Monad, Monad Q
forall a. IO a -> Q a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> Q a
$cliftIO :: forall a. IO a -> Q a
MonadIO, MonadError String, Monad Q
Q State
forall (m :: * -> *). Monad m -> m State -> MonadQuery m
queryState :: Q State
$cqueryState :: Q State
MonadQuery)

-- | Creates a computation that queries a solver and yields a 'CheckResult'.
mkQuery :: Env -> Q CheckResult
mkQuery :: Env -> Q CheckResult
mkQuery Env
env = do
    CheckSatResult
satResult <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
    case CheckSatResult
satResult of
        CheckSatResult
Sat    -> Integer -> Integer -> CheckResult
Counterexample forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue (Env -> SBV Integer
envX Env
env)
                                 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue (Env -> SBV Integer
envY Env
env)
        CheckSatResult
Unsat  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
Proved
        DSat{} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"delta-sat"
        CheckSatResult
Unk    -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"unknown"

-- | Checks a 'Property' of a 'Program' (or fails).
check :: Program a -> Property -> IO (Either String CheckResult)
check :: forall a. Program a -> Property -> IO (Either String CheckResult)
check Program a
program Property
prop = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
runSMTWith SMTConfig
z3 forall a b. (a -> b) -> a -> b
$ do
    Env
env <- forall a. Alloc a -> SymbolicT (ExceptT String IO) a
runAlloc Alloc Env
allocEnv
    SBool
test <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT forall (m :: * -> *) a. Monad m => Identity a -> m a
generalize forall a b. (a -> b) -> a -> b
$ do
        Result
res <- forall a. Env -> Program a -> Except String Result
runProgramEval Env
env Program a
program
        Result -> Env -> Property -> Except String SBool
runPropertyEval Result
res Env
env Property
prop
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot SBool
test
    forall (m :: * -> *) a. ExtractIO m => QueryT m a -> SymbolicT m a
query forall a b. (a -> b) -> a -> b
$ forall a. Q a -> QueryT (ExceptT String IO) a
runQ forall a b. (a -> b) -> a -> b
$ Env -> Q CheckResult
mkQuery Env
env

-- * Some examples

-- | Check that @x+1+y@ generates a counter-example for the property that the
-- result is less than @10@ when @x+y@ is at least @9@. We have:
--
-- >>> ex1
-- Right (Counterexample 0 9)
ex1 :: IO (Either String CheckResult)
ex1 :: IO (Either String CheckResult)
ex1 = forall a. Program a -> Property -> IO (Either String CheckResult)
check (forall a. Term a -> Program a
Program  forall a b. (a -> b) -> a -> b
$ forall r. String -> Term r
Var String
"x" Term Integer -> Term Integer -> Term Integer
`Plus` Integer -> Term Integer
Lit Integer
1 Term Integer -> Term Integer -> Term Integer
`Plus` forall r. String -> Term r
Var String
"y")
            (Term Bool -> Property
Property forall a b. (a -> b) -> a -> b
$ forall r. String -> Term r
Var String
"result" Term Integer -> Term Integer -> Term Bool
`LessThan` Integer -> Term Integer
Lit Integer
10)

-- | Check that the program @x+y@ correctly produces a result greater than @1@ when
-- both @x@ and @y@ are at least @1@. We have:
--
-- >>> ex2
-- Right Proved
ex2 :: IO (Either String CheckResult)
ex2 :: IO (Either String CheckResult)
ex2 = forall a. Program a -> Property -> IO (Either String CheckResult)
check (forall a. Term a -> Program a
Program  forall a b. (a -> b) -> a -> b
$ forall r. String -> Term r
Var String
"x" Term Integer -> Term Integer -> Term Integer
`Plus` forall r. String -> Term r
Var String
"y")
            (Term Bool -> Property
Property forall a b. (a -> b) -> a -> b
$ (Term Integer -> Term Bool
positive (forall r. String -> Term r
Var String
"x") Term Bool -> Term Bool -> Term Bool
`And` Term Integer -> Term Bool
positive (forall r. String -> Term r
Var String
"y"))
                Term Bool -> Term Bool -> Term Bool
`Implies` (forall r. String -> Term r
Var String
"result" Term Integer -> Term Integer -> Term Bool
`GreaterThan` Integer -> Term Integer
Lit Integer
1))
  where positive :: Term Integer -> Term Bool
positive Term Integer
t = Term Integer
t Term Integer -> Term Integer -> Term Bool
`GreaterThan` Integer -> Term Integer
Lit Integer
0

-- | Check that we catch the cases properly through the monad stack when there is a
-- syntax error, like an undefined variable. We have:
--
-- >>> ex3
-- Left "unknown variable"
ex3 :: IO (Either String CheckResult)
ex3 :: IO (Either String CheckResult)
ex3 = forall a. Program a -> Property -> IO (Either String CheckResult)
check (forall a. Term a -> Program a
Program  forall a b. (a -> b) -> a -> b
$ forall r. String -> Term r
Var String
"notAValidVar")
            (Term Bool -> Property
Property forall a b. (a -> b) -> a -> b
$ forall r. String -> Term r
Var String
"result" Term Integer -> Term Integer -> Term Bool
`LessThan` Integer -> Term Integer
Lit Integer
10)