-----------------------------------------------------------------------------
-- |
-- 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 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
import Data.SBV.Trans.Control

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

-- | Monad for allocating free variables.
newtype Alloc a = Alloc { Alloc a -> SymbolicT (ExceptT String IO) a
runAlloc :: SymbolicT (ExceptT String IO) a }
    deriving (a -> Alloc b -> Alloc a
(a -> b) -> Alloc a -> Alloc b
(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
<$ :: a -> Alloc b -> Alloc a
$c<$ :: forall a b. a -> Alloc b -> Alloc a
fmap :: (a -> b) -> Alloc a -> Alloc b
$cfmap :: forall a b. (a -> b) -> Alloc a -> Alloc b
Functor, Functor Alloc
a -> Alloc a
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
Alloc a -> Alloc b -> Alloc b
Alloc a -> Alloc b -> Alloc a
Alloc (a -> b) -> Alloc a -> Alloc b
(a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
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
<* :: Alloc a -> Alloc b -> Alloc a
$c<* :: forall a b. Alloc a -> Alloc b -> Alloc a
*> :: Alloc a -> Alloc b -> Alloc b
$c*> :: forall a b. Alloc a -> Alloc b -> Alloc b
liftA2 :: (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
$cliftA2 :: forall a b c. (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
<*> :: Alloc (a -> b) -> Alloc a -> Alloc b
$c<*> :: forall a b. Alloc (a -> b) -> Alloc a -> Alloc b
pure :: a -> Alloc a
$cpure :: forall a. a -> Alloc a
$cp1Applicative :: Functor Alloc
Applicative, Applicative Alloc
a -> Alloc a
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
Alloc a -> (a -> Alloc b) -> Alloc b
Alloc a -> Alloc b -> Alloc b
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 :: a -> Alloc a
$creturn :: forall a. a -> Alloc a
>> :: Alloc a -> Alloc b -> Alloc b
$c>> :: forall a b. Alloc a -> Alloc b -> Alloc b
>>= :: Alloc a -> (a -> Alloc b) -> Alloc b
$c>>= :: forall a b. Alloc a -> (a -> Alloc b) -> Alloc b
$cp1Monad :: Applicative Alloc
Monad, Monad Alloc
Monad Alloc -> (forall a. IO a -> Alloc a) -> MonadIO Alloc
IO a -> Alloc a
forall a. IO a -> Alloc a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> Alloc a
$cliftIO :: forall a. IO a -> Alloc a
$cp1MonadIO :: Monad Alloc
MonadIO,
              MonadError String, MonadIO Alloc
Alloc State
MonadIO Alloc -> Alloc State -> MonadSymbolic Alloc
forall (m :: * -> *). MonadIO m -> m State -> MonadSymbolic m
symbolicEnv :: Alloc State
$csymbolicEnv :: Alloc State
$cp1MonadSymbolic :: MonadIO Alloc
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
/= :: Env -> Env -> Bool
$c/= :: Env -> Env -> Bool
== :: Env -> Env -> Bool
$c== :: 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
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
"" = String -> Alloc (SBV Integer)
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)
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"
    Env -> Alloc Env
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env -> Alloc Env) -> Env -> Alloc Env
forall a b. (a -> b) -> a -> b
$ SBV Integer -> SBV Integer -> Maybe SVal -> Env
Env SBV Integer
x SBV Integer
y Maybe SVal
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 { Eval a -> ReaderT Env (Except String) a
unEval :: ReaderT Env (Except String) a }
    deriving (a -> Eval b -> Eval a
(a -> b) -> Eval a -> Eval b
(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
<$ :: a -> Eval b -> Eval a
$c<$ :: forall a b. a -> Eval b -> Eval a
fmap :: (a -> b) -> Eval a -> Eval b
$cfmap :: forall a b. (a -> b) -> Eval a -> Eval b
Functor, Functor Eval
a -> Eval a
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
Eval a -> Eval b -> Eval b
Eval a -> Eval b -> Eval a
Eval (a -> b) -> Eval a -> Eval b
(a -> b -> c) -> Eval a -> Eval b -> Eval c
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
<* :: Eval a -> Eval b -> Eval a
$c<* :: forall a b. Eval a -> Eval b -> Eval a
*> :: Eval a -> Eval b -> Eval b
$c*> :: forall a b. Eval a -> Eval b -> Eval b
liftA2 :: (a -> b -> c) -> Eval a -> Eval b -> Eval c
$cliftA2 :: forall a b c. (a -> b -> c) -> Eval a -> Eval b -> Eval c
<*> :: Eval (a -> b) -> Eval a -> Eval b
$c<*> :: forall a b. Eval (a -> b) -> Eval a -> Eval b
pure :: a -> Eval a
$cpure :: forall a. a -> Eval a
$cp1Applicative :: Functor Eval
Applicative, Applicative Eval
a -> Eval a
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
Eval a -> (a -> Eval b) -> Eval b
Eval a -> Eval b -> Eval b
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 :: a -> Eval a
$creturn :: forall a. a -> Eval a
>> :: Eval a -> Eval b -> Eval b
$c>> :: forall a b. Eval a -> Eval b -> Eval b
>>= :: Eval a -> (a -> Eval b) -> Eval b
$c>>= :: forall a b. Eval a -> (a -> Eval b) -> Eval b
$cp1Monad :: Applicative Eval
Monad, MonadReader Env, MonadError String)

-- | Unsafe cast for symbolic values. In production code, we would check types instead.
unsafeCastSBV :: SBV a -> SBV b
unsafeCastSBV :: 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 :: 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 Maybe SVal
mRes <- (Env -> Maybe SVal) -> Eval (Maybe SVal)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader Env -> Maybe SVal
result
                              case Maybe SVal
mRes of
                                Maybe SVal
Nothing -> String -> Eval (SBV r)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"unknown variable"
                                Just SVal
sv -> SBV r -> Eval (SBV r)
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 e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"unknown variable"
eval (Lit Integer
i)             = SBV Integer -> Eval (SBV Integer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBV Integer -> Eval (SBV Integer))
-> SBV Integer -> Eval (SBV Integer)
forall a b. (a -> b) -> a -> b
$ Integer -> SBV Integer
forall a. SymVal a => a -> SBV a
literal Integer
i
eval (Plus        Term Integer
t1 Term Integer
t2) = SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
(+)   (SBV Integer -> SBV Integer -> SBV Integer)
-> Eval (SBV Integer) -> Eval (SBV Integer -> SBV Integer)
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 Integer)
-> Eval (SBV Integer) -> Eval (SBV Integer)
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 (LessThan    Term Integer
t1 Term Integer
t2) = SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
(.<)  (SBV Integer -> SBV Integer -> SBool)
-> Eval (SBV Integer) -> Eval (SBV Integer -> SBool)
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 -> SBool) -> Eval (SBV Integer) -> Eval SBool
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 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
(.>)  (SBV Integer -> SBV Integer -> SBool)
-> Eval (SBV Integer) -> Eval (SBV Integer -> SBool)
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 -> SBool) -> Eval (SBV Integer) -> Eval SBool
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 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
(.==) (SBV Integer -> SBV Integer -> SBool)
-> Eval (SBV Integer) -> Eval (SBV Integer -> SBool)
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 -> SBool) -> Eval (SBV Integer) -> Eval SBool
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 -> SBool
sNot  (SBool -> SBool) -> Eval SBool -> Eval SBool
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 -> SBool
(.||) (SBool -> SBool -> SBool) -> Eval SBool -> Eval (SBool -> SBool)
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 -> SBool) -> Eval SBool -> Eval SBool
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 -> SBool
(.&&) (SBool -> SBool -> SBool) -> Eval SBool -> Eval (SBool -> SBool)
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 -> SBool) -> Eval SBool -> Eval SBool
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 -> SBool
(.=>) (SBool -> SBool -> SBool) -> Eval SBool -> Eval (SBool -> SBool)
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 -> SBool) -> Eval SBool -> Eval SBool
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 :: Env -> Term a -> Except String (SBV a)
runEval Env
env Term a
term = ReaderT Env (Except String) (SBV a) -> Env -> Except String (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 'Result' from a symbolic value.
mkResult :: SBV a -> Result
mkResult :: 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 'Program'.
runProgramEval :: Env -> Program a -> Except String Result
runProgramEval :: 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 '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) =
    Env -> Term Bool -> Except String SBool
forall a. Env -> Term a -> Except String (SBV a)
runEval (Env
env { result :: Maybe SVal
result = SVal -> Maybe SVal
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
(CheckResult -> CheckResult -> Bool)
-> (CheckResult -> CheckResult -> Bool) -> Eq CheckResult
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
(Int -> CheckResult -> ShowS)
-> (CheckResult -> String)
-> ([CheckResult] -> ShowS)
-> Show CheckResult
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 :: Identity a -> m a
generalize = 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 { Q a -> QueryT (ExceptT String IO) a
runQ :: QueryT (ExceptT String IO) a }
    deriving (a -> Q b -> Q a
(a -> b) -> Q a -> Q b
(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
<$ :: a -> Q b -> Q a
$c<$ :: forall a b. a -> Q b -> Q a
fmap :: (a -> b) -> Q a -> Q b
$cfmap :: forall a b. (a -> b) -> Q a -> Q b
Functor, Functor Q
a -> Q a
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
Q a -> Q b -> Q b
Q a -> Q b -> Q a
Q (a -> b) -> Q a -> Q b
(a -> b -> c) -> Q a -> Q b -> Q c
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
<* :: Q a -> Q b -> Q a
$c<* :: forall a b. Q a -> Q b -> Q a
*> :: Q a -> Q b -> Q b
$c*> :: forall a b. Q a -> Q b -> Q b
liftA2 :: (a -> b -> c) -> Q a -> Q b -> Q c
$cliftA2 :: forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c
<*> :: Q (a -> b) -> Q a -> Q b
$c<*> :: forall a b. Q (a -> b) -> Q a -> Q b
pure :: a -> Q a
$cpure :: forall a. a -> Q a
$cp1Applicative :: Functor Q
Applicative, Applicative Q
a -> Q a
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
Q a -> (a -> Q b) -> Q b
Q a -> Q b -> Q b
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 :: a -> Q a
$creturn :: forall a. a -> Q a
>> :: Q a -> Q b -> Q b
$c>> :: forall a b. Q a -> Q b -> Q b
>>= :: Q a -> (a -> Q b) -> Q b
$c>>= :: forall a b. Q a -> (a -> Q b) -> Q b
$cp1Monad :: Applicative Q
Monad, Monad Q
Monad Q -> (forall a. IO a -> Q a) -> MonadIO Q
IO a -> Q a
forall a. IO a -> Q a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> Q a
$cliftIO :: forall a. IO a -> Q a
$cp1MonadIO :: Monad Q
MonadIO, MonadError String, Monad Q
Q State
Monad Q -> Q State -> MonadQuery Q
forall (m :: * -> *). Monad m -> m State -> MonadQuery m
queryState :: Q State
$cqueryState :: Q State
$cp1MonadQuery :: Monad Q
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 <- Q CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
    case CheckSatResult
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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
Proved
        DSat{} -> String -> Q CheckResult
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"delta-sat"
        CheckSatResult
Unk    -> String -> Q CheckResult
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 :: 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
env <- Alloc Env -> SymbolicT (ExceptT String IO) Env
forall a. Alloc a -> SymbolicT (ExceptT String IO) a
runAlloc Alloc Env
allocEnv
    SBool
test <- ExceptT String IO SBool -> SymbolicT (ExceptT String IO) SBool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT String IO SBool -> SymbolicT (ExceptT String IO) SBool)
-> ExceptT String IO SBool -> SymbolicT (ExceptT String IO) SBool
forall a b. (a -> b) -> a -> b
$ (Identity (Either String SBool) -> IO (Either String SBool))
-> Except String SBool -> ExceptT String IO SBool
forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT Identity (Either String SBool) -> IO (Either String SBool)
forall (m :: * -> *) a. Monad m => Identity a -> m a
generalize (Except String SBool -> ExceptT String IO SBool)
-> Except String SBool -> ExceptT String IO SBool
forall a b. (a -> b) -> a -> b
$ do
        Result
res <- Env -> Program a -> Except String Result
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
    SBool -> SymbolicT (ExceptT String IO) ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT (ExceptT String IO) ())
-> SBool -> SymbolicT (ExceptT String IO) ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot SBool
test
    QueryT (ExceptT String IO) CheckResult
-> SymbolicT (ExceptT String IO) CheckResult
forall (m :: * -> *) a. ExtractIO m => QueryT m a -> SymbolicT m a
query (QueryT (ExceptT String IO) CheckResult
 -> SymbolicT (ExceptT String IO) CheckResult)
-> QueryT (ExceptT String IO) CheckResult
-> SymbolicT (ExceptT String IO) CheckResult
forall a b. (a -> b) -> a -> b
$ Q CheckResult -> QueryT (ExceptT String IO) CheckResult
forall a. Q a -> QueryT (ExceptT String IO) a
runQ (Q CheckResult -> QueryT (ExceptT String IO) CheckResult)
-> Q CheckResult -> QueryT (ExceptT String IO) CheckResult
forall a b. (a -> b) -> a -> b
$ Env -> Q CheckResult
mkQuery Env
env

-- * Some examples

-- | Check that @x+y+1@ 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 Any -> Property -> IO (Either String CheckResult)
forall a. Program a -> Property -> IO (Either String CheckResult)
check (Term Any -> Program Any
forall a. Term a -> Program a
Program  (Term Any -> Program Any) -> Term Any -> Program Any
forall a b. (a -> b) -> a -> b
$ String -> Term Any
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)