-----------------------------------------------------------------------------
-- |
-- 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 t'SymbolicT' and t'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 -> b) -> Alloc a -> Alloc b)
-> (forall a b. a -> Alloc b -> Alloc a) -> Functor Alloc
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
$cfmap :: forall a b. (a -> b) -> Alloc a -> Alloc b
fmap :: forall a b. (a -> b) -> Alloc a -> Alloc b
$c<$ :: forall a b. a -> Alloc b -> Alloc a
<$ :: forall a b. a -> Alloc b -> Alloc a
Functor, Functor Alloc
Functor Alloc =>
(forall a. a -> Alloc a)
-> (forall a b. Alloc (a -> b) -> Alloc a -> Alloc b)
-> (forall a b c. (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c)
-> (forall a b. Alloc a -> Alloc b -> Alloc b)
-> (forall a b. Alloc a -> Alloc b -> Alloc a)
-> Applicative 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
$cpure :: forall a. a -> Alloc a
pure :: forall a. a -> Alloc a
$c<*> :: forall a b. Alloc (a -> b) -> Alloc a -> Alloc b
<*> :: forall a b. Alloc (a -> b) -> Alloc a -> Alloc b
$cliftA2 :: forall a b c. (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
liftA2 :: forall a b c. (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
$c*> :: forall a b. Alloc a -> Alloc b -> Alloc b
*> :: forall a b. Alloc a -> Alloc b -> Alloc b
$c<* :: forall a b. Alloc a -> Alloc b -> Alloc a
<* :: forall a b. Alloc a -> Alloc b -> Alloc a
Applicative, Applicative Alloc
Applicative Alloc =>
(forall a b. Alloc a -> (a -> Alloc b) -> Alloc b)
-> (forall a b. Alloc a -> Alloc b -> Alloc b)
-> (forall a. a -> Alloc a)
-> Monad 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
$c>>= :: forall a b. Alloc a -> (a -> Alloc b) -> Alloc b
>>= :: forall a b. Alloc a -> (a -> Alloc b) -> Alloc b
$c>> :: forall a b. Alloc a -> Alloc b -> Alloc b
>> :: forall a b. Alloc a -> Alloc b -> Alloc b
$creturn :: forall a. a -> Alloc a
return :: forall a. a -> Alloc a
Monad, Monad Alloc
Monad Alloc => (forall a. IO a -> Alloc a) -> MonadIO Alloc
forall a. IO a -> Alloc a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> Alloc a
liftIO :: forall a. IO a -> Alloc a
MonadIO,
              MonadError String, MonadIO Alloc
Alloc State
MonadIO Alloc => Alloc State -> MonadSymbolic Alloc
forall (m :: * -> *). MonadIO m => m State -> MonadSymbolic m
$csymbolicEnv :: Alloc State
symbolicEnv :: 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
(Env -> Env -> Bool) -> (Env -> Env -> Bool) -> Eq Env
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Env -> Env -> Bool
== :: Env -> Env -> Bool
$c/= :: Env -> Env -> Bool
/= :: Env -> Env -> Bool
Eq, Int -> Env -> ShowS
[Env] -> ShowS
Env -> String
(Int -> Env -> ShowS)
-> (Env -> String) -> ([Env] -> ShowS) -> Show Env
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Env -> ShowS
showsPrec :: Int -> Env -> ShowS
$cshow :: Env -> String
show :: Env -> String
$cshowList :: [Env] -> ShowS
showList :: [Env] -> ShowS
Show)

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

-- | Allocate an t'Env' holding all input variables for the program.
allocEnv :: Alloc Env
allocEnv :: Alloc Env
allocEnv = do
    x <- String -> Alloc (SBV Integer)
alloc String
"x"
    y <- alloc "y"
    pure $ Env x y 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 -> b) -> Eval a -> Eval b)
-> (forall a b. a -> Eval b -> Eval a) -> Functor Eval
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
$cfmap :: forall a b. (a -> b) -> Eval a -> Eval b
fmap :: forall a b. (a -> b) -> Eval a -> Eval b
$c<$ :: forall a b. a -> Eval b -> Eval a
<$ :: forall a b. a -> Eval b -> Eval a
Functor, Functor Eval
Functor Eval =>
(forall a. a -> Eval a)
-> (forall a b. Eval (a -> b) -> Eval a -> Eval b)
-> (forall a b c. (a -> b -> c) -> Eval a -> Eval b -> Eval c)
-> (forall a b. Eval a -> Eval b -> Eval b)
-> (forall a b. Eval a -> Eval b -> Eval a)
-> Applicative 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
$cpure :: forall a. a -> Eval a
pure :: forall a. a -> Eval a
$c<*> :: forall a b. Eval (a -> b) -> Eval a -> Eval b
<*> :: forall a b. Eval (a -> b) -> Eval a -> Eval b
$cliftA2 :: forall a b c. (a -> b -> c) -> Eval a -> Eval b -> Eval c
liftA2 :: forall a b c. (a -> b -> c) -> Eval a -> Eval b -> Eval c
$c*> :: forall a b. Eval a -> Eval b -> Eval b
*> :: forall a b. Eval a -> Eval b -> Eval b
$c<* :: forall a b. Eval a -> Eval b -> Eval a
<* :: forall a b. Eval a -> Eval b -> Eval a
Applicative, Applicative Eval
Applicative Eval =>
(forall a b. Eval a -> (a -> Eval b) -> Eval b)
-> (forall a b. Eval a -> Eval b -> Eval b)
-> (forall a. a -> Eval a)
-> Monad 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
$c>>= :: forall a b. Eval a -> (a -> Eval b) -> Eval b
>>= :: forall a b. Eval a -> (a -> Eval b) -> Eval b
$c>> :: forall a b. Eval a -> Eval b -> Eval b
>> :: forall a b. Eval a -> Eval b -> Eval b
$creturn :: forall a. a -> Eval a
return :: forall a. a -> Eval a
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 = SVal -> SBV b
forall a. SVal -> SBV a
SBV (SVal -> SBV b) -> (SBV a -> SVal) -> SBV a -> SBV b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SVal
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")           = (Env -> SBV r) -> Eval (SBV r)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Env -> SBV r) -> Eval (SBV r)) -> (Env -> SBV r) -> Eval (SBV r)
forall a b. (a -> b) -> a -> b
$ SBV Integer -> SBV r
forall a b. SBV a -> SBV b
unsafeCastSBV (SBV Integer -> SBV r) -> (Env -> SBV Integer) -> Env -> SBV r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> SBV Integer
envX
eval (Var String
"y")           = (Env -> SBV r) -> Eval (SBV r)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Env -> SBV r) -> Eval (SBV r)) -> (Env -> SBV r) -> Eval (SBV r)
forall a b. (a -> b) -> a -> b
$ SBV Integer -> SBV r
forall a b. SBV a -> SBV b
unsafeCastSBV (SBV Integer -> SBV r) -> (Env -> SBV Integer) -> Env -> SBV r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> SBV Integer
envY
eval (Var String
"result")      = do mRes <- (Env -> Maybe SVal) -> Eval (Maybe SVal)
forall a. (Env -> a) -> Eval a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader Env -> Maybe SVal
result
                              case mRes of
                                Maybe SVal
Nothing -> String -> Eval (SBV r)
forall a. String -> Eval a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"unknown variable"
                                Just SVal
sv -> SBV r -> Eval (SBV r)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBV r -> Eval (SBV r)) -> SBV r -> Eval (SBV r)
forall a b. (a -> b) -> a -> b
$ SVal -> SBV r
forall a. SVal -> SBV a
SBV SVal
sv
eval (Var String
_)             = String -> Eval (SBV r)
forall a. String -> Eval a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"unknown variable"
eval (Lit Integer
i)             = SBV r -> Eval (SBV r)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBV r -> Eval (SBV r)) -> SBV r -> Eval (SBV r)
forall a b. (a -> b) -> a -> b
$ r -> SBV r
forall a. SymVal a => a -> SBV a
literal r
Integer
i
eval (Plus        Term Integer
t1 Term Integer
t2) = SBV r -> SBV r -> SBV r
forall a. Num a => a -> a -> a
(+)   (SBV r -> SBV r -> SBV r) -> Eval (SBV r) -> Eval (SBV r -> SBV r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term r -> Eval (SBV r)
forall r. Term r -> Eval (SBV r)
eval Term r
Term Integer
t1 Eval (SBV r -> SBV r) -> Eval (SBV r) -> Eval (SBV r)
forall a b. Eval (a -> b) -> Eval a -> Eval b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term r -> Eval (SBV r)
forall r. Term r -> Eval (SBV r)
eval Term r
Term Integer
t2
eval (LessThan    Term Integer
t1 Term Integer
t2) = SBV Integer -> SBV Integer -> SBV r
SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
(.<)  (SBV Integer -> SBV Integer -> SBV r)
-> Eval (SBV Integer) -> Eval (SBV Integer -> SBV r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Integer -> Eval (SBV Integer)
forall r. Term r -> Eval (SBV r)
eval Term Integer
t1 Eval (SBV Integer -> SBV r) -> Eval (SBV Integer) -> Eval (SBV r)
forall a b. Eval (a -> b) -> Eval a -> Eval b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term Integer -> Eval (SBV Integer)
forall r. Term r -> Eval (SBV r)
eval Term Integer
t2
eval (GreaterThan Term Integer
t1 Term Integer
t2) = SBV Integer -> SBV Integer -> SBV r
SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
(.>)  (SBV Integer -> SBV Integer -> SBV r)
-> Eval (SBV Integer) -> Eval (SBV Integer -> SBV r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Integer -> Eval (SBV Integer)
forall r. Term r -> Eval (SBV r)
eval Term Integer
t1 Eval (SBV Integer -> SBV r) -> Eval (SBV Integer) -> Eval (SBV r)
forall a b. Eval (a -> b) -> Eval a -> Eval b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term Integer -> Eval (SBV Integer)
forall r. Term r -> Eval (SBV r)
eval Term Integer
t2
eval (Equals      Term Integer
t1 Term Integer
t2) = SBV Integer -> SBV Integer -> SBV r
SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
(.==) (SBV Integer -> SBV Integer -> SBV r)
-> Eval (SBV Integer) -> Eval (SBV Integer -> SBV r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Integer -> Eval (SBV Integer)
forall r. Term r -> Eval (SBV r)
eval Term Integer
t1 Eval (SBV Integer -> SBV r) -> Eval (SBV Integer) -> Eval (SBV r)
forall a b. Eval (a -> b) -> Eval a -> Eval b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term Integer -> Eval (SBV Integer)
forall r. Term r -> Eval (SBV r)
eval Term Integer
t2
eval (Not         Term Bool
t)     = SBool -> SBV r
SBool -> SBool
sNot  (SBool -> SBV r) -> Eval SBool -> Eval (SBV r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Bool -> Eval SBool
forall r. Term r -> Eval (SBV r)
eval Term Bool
t
eval (Or          Term Bool
t1 Term Bool
t2) = SBool -> SBool -> SBV r
SBool -> SBool -> SBool
(.||) (SBool -> SBool -> SBV r) -> Eval SBool -> Eval (SBool -> SBV r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Bool -> Eval SBool
forall r. Term r -> Eval (SBV r)
eval Term Bool
t1 Eval (SBool -> SBV r) -> Eval SBool -> Eval (SBV r)
forall a b. Eval (a -> b) -> Eval a -> Eval b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term Bool -> Eval SBool
forall r. Term r -> Eval (SBV r)
eval Term Bool
t2
eval (And         Term Bool
t1 Term Bool
t2) = SBool -> SBool -> SBV r
SBool -> SBool -> SBool
(.&&) (SBool -> SBool -> SBV r) -> Eval SBool -> Eval (SBool -> SBV r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Bool -> Eval SBool
forall r. Term r -> Eval (SBV r)
eval Term Bool
t1 Eval (SBool -> SBV r) -> Eval SBool -> Eval (SBV r)
forall a b. Eval (a -> b) -> Eval a -> Eval b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term Bool -> Eval SBool
forall r. Term r -> Eval (SBV r)
eval Term Bool
t2
eval (Implies     Term Bool
t1 Term Bool
t2) = SBool -> SBool -> SBV r
SBool -> SBool -> SBool
(.=>) (SBool -> SBool -> SBV r) -> Eval SBool -> Eval (SBool -> SBV r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Bool -> Eval SBool
forall r. Term r -> Eval (SBV r)
eval Term Bool
t1 Eval (SBool -> SBV r) -> Eval SBool -> Eval (SBV r)
forall a b. Eval (a -> b) -> Eval a -> Eval b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term Bool -> Eval SBool
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 = ReaderT Env (Except String) (SBV a)
-> Env -> ExceptT String Identity (SBV a)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Eval (SBV a) -> ReaderT Env (Except String) (SBV a)
forall a. Eval a -> ReaderT Env (Except String) a
unEval (Eval (SBV a) -> ReaderT Env (Except String) (SBV a))
-> Eval (SBV a) -> ReaderT Env (Except String) (SBV a)
forall a b. (a -> b) -> a -> b
$ Term a -> Eval (SBV a)
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 t'Result' from a symbolic value.
mkResult :: SBV a -> Result
mkResult :: forall a. SBV a -> Result
mkResult = SVal -> Result
Result (SVal -> Result) -> (SBV a -> SVal) -> SBV a -> Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SVal
forall a. SBV a -> SVal
unSBV

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

-- * Property evaluation

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

-- | Performs symbolic evaluation of a t'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) =
    Env -> Term Bool -> Except String SBool
forall a. Env -> Term a -> Except String (SBV a)
runEval (Env
env { result = Just res }) Term Bool
term

-- * Checking whether a program satisfies a property

-- | The result of 'check'ing the combination of a t'Program' and a t'Property'.
data CheckResult = Proved | Counterexample Integer Integer
    deriving (CheckResult -> CheckResult -> Bool
(CheckResult -> CheckResult -> Bool)
-> (CheckResult -> CheckResult -> Bool) -> Eq CheckResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CheckResult -> CheckResult -> Bool
== :: CheckResult -> CheckResult -> Bool
$c/= :: CheckResult -> CheckResult -> Bool
/= :: CheckResult -> CheckResult -> Bool
Eq, Int -> CheckResult -> ShowS
[CheckResult] -> ShowS
CheckResult -> String
(Int -> CheckResult -> ShowS)
-> (CheckResult -> String)
-> ([CheckResult] -> ShowS)
-> Show CheckResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CheckResult -> ShowS
showsPrec :: Int -> CheckResult -> ShowS
$cshow :: CheckResult -> String
show :: CheckResult -> String
$cshowList :: [CheckResult] -> ShowS
showList :: [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 = a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> (Identity a -> a) -> Identity a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
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 -> b) -> Q a -> Q b)
-> (forall a b. a -> Q b -> Q a) -> Functor Q
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
$cfmap :: forall a b. (a -> b) -> Q a -> Q b
fmap :: forall a b. (a -> b) -> Q a -> Q b
$c<$ :: forall a b. a -> Q b -> Q a
<$ :: forall a b. a -> Q b -> Q a
Functor, Functor Q
Functor Q =>
(forall a. a -> Q a)
-> (forall a b. Q (a -> b) -> Q a -> Q b)
-> (forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c)
-> (forall a b. Q a -> Q b -> Q b)
-> (forall a b. Q a -> Q b -> Q a)
-> Applicative 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
$cpure :: forall a. a -> Q a
pure :: forall a. a -> Q a
$c<*> :: forall a b. Q (a -> b) -> Q a -> Q b
<*> :: forall a b. Q (a -> b) -> Q a -> Q b
$cliftA2 :: forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c
liftA2 :: forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c
$c*> :: forall a b. Q a -> Q b -> Q b
*> :: forall a b. Q a -> Q b -> Q b
$c<* :: forall a b. Q a -> Q b -> Q a
<* :: forall a b. Q a -> Q b -> Q a
Applicative, Applicative Q
Applicative Q =>
(forall a b. Q a -> (a -> Q b) -> Q b)
-> (forall a b. Q a -> Q b -> Q b)
-> (forall a. a -> Q a)
-> Monad 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
$c>>= :: forall a b. Q a -> (a -> Q b) -> Q b
>>= :: forall a b. Q a -> (a -> Q b) -> Q b
$c>> :: forall a b. Q a -> Q b -> Q b
>> :: forall a b. Q a -> Q b -> Q b
$creturn :: forall a. a -> Q a
return :: forall a. a -> Q a
Monad, Monad Q
Monad Q => (forall a. IO a -> Q a) -> MonadIO Q
forall a. IO a -> Q a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> Q a
liftIO :: forall a. IO a -> Q a
MonadIO, MonadError String, Monad Q
Q State
Monad Q => Q State -> MonadQuery Q
forall (m :: * -> *). Monad m => m State -> MonadQuery m
$cqueryState :: Q State
queryState :: 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
    satResult <- Q CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
    case satResult of
        CheckSatResult
Sat    -> Integer -> Integer -> CheckResult
Counterexample (Integer -> Integer -> CheckResult)
-> Q Integer -> Q (Integer -> CheckResult)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV Integer -> Q Integer
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue (Env -> SBV Integer
envX Env
env)
                                 Q (Integer -> CheckResult) -> Q Integer -> Q CheckResult
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBV Integer -> Q Integer
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue (Env -> SBV Integer
envY Env
env)
        CheckSatResult
Unsat  -> CheckResult -> Q CheckResult
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
Proved
        DSat{} -> String -> Q CheckResult
forall a. String -> Q a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"delta-sat"
        CheckSatResult
Unk    -> String -> Q CheckResult
forall a. String -> Q a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"unknown"

-- | Checks a t'Property' of a t'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 = ExceptT String IO CheckResult -> IO (Either String CheckResult)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT String IO CheckResult -> IO (Either String CheckResult))
-> ExceptT String IO CheckResult -> IO (Either String CheckResult)
forall a b. (a -> b) -> a -> b
$ SMTConfig
-> SymbolicT (ExceptT String IO) CheckResult
-> ExceptT String IO CheckResult
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
runSMTWith SMTConfig
z3 (SymbolicT (ExceptT String IO) CheckResult
 -> ExceptT String IO CheckResult)
-> SymbolicT (ExceptT String IO) CheckResult
-> ExceptT String IO CheckResult
forall a b. (a -> b) -> a -> b
$ do
    env <- Alloc Env -> SymbolicT (ExceptT String IO) Env
forall a. Alloc a -> SymbolicT (ExceptT String IO) a
runAlloc Alloc Env
allocEnv
    test <- lift $ mapExceptT generalize $ do
        res <- runProgramEval env program
        runPropertyEval res env prop
    constrain $ sNot test
    query $ runQ $ mkQuery 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 = Program Integer -> Property -> IO (Either String CheckResult)
forall a. Program a -> Property -> IO (Either String CheckResult)
check (Term Integer -> Program Integer
forall a. Term a -> Program a
Program  (Term Integer -> Program Integer)
-> Term Integer -> Program Integer
forall a b. (a -> b) -> a -> b
$ String -> Term Integer
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` String -> Term Integer
forall r. String -> Term r
Var String
"y")
            (Term Bool -> Property
Property (Term Bool -> Property) -> Term Bool -> Property
forall a b. (a -> b) -> a -> b
$ String -> Term Integer
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 = Program Integer -> Property -> IO (Either String CheckResult)
forall a. Program a -> Property -> IO (Either String CheckResult)
check (Term Integer -> Program Integer
forall a. Term a -> Program a
Program  (Term Integer -> Program Integer)
-> Term Integer -> Program Integer
forall a b. (a -> b) -> a -> b
$ String -> Term Integer
forall r. String -> Term r
Var String
"x" Term Integer -> Term Integer -> Term Integer
`Plus` String -> Term Integer
forall r. String -> Term r
Var String
"y")
            (Term Bool -> Property
Property (Term Bool -> Property) -> Term Bool -> Property
forall a b. (a -> b) -> a -> b
$ (Term Integer -> Term Bool
positive (String -> Term Integer
forall r. String -> Term r
Var String
"x") Term Bool -> Term Bool -> Term Bool
`And` Term Integer -> Term Bool
positive (String -> Term Integer
forall r. String -> Term r
Var String
"y"))
                Term Bool -> Term Bool -> Term Bool
`Implies` (String -> Term Integer
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 = Program (ZonkAny 0) -> Property -> IO (Either String CheckResult)
forall a. Program a -> Property -> IO (Either String CheckResult)
check (Term (ZonkAny 0) -> Program (ZonkAny 0)
forall a. Term a -> Program a
Program  (Term (ZonkAny 0) -> Program (ZonkAny 0))
-> Term (ZonkAny 0) -> Program (ZonkAny 0)
forall a b. (a -> b) -> a -> b
$ String -> Term (ZonkAny 0)
forall r. String -> Term r
Var String
"notAValidVar")
            (Term Bool -> Property
Property (Term Bool -> Property) -> Term Bool -> Property
forall a b. (a -> b) -> a -> b
$ String -> Term Integer
forall r. String -> Term r
Var String
"result" Term Integer -> Term Integer -> Term Bool
`LessThan` Integer -> Term Integer
Lit Integer
10)

{- HLint ignore module "Use fewer imports" -}