Copyright	(c) Brian Schroeder
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.Transformers.SymbolicEval

Contents

Allocation of symbolic variables, so we can extract a model later.
Symbolic term evaluation
Property evaluation
Checking whether a program satisfies a property
Some examples

Description

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:

allocate free variables, so we can extract a model after evaluation
perform symbolic evaluation of a program and an associated property
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.

Synopsis

newtype Alloc a = Alloc {
- runAlloc :: SymbolicT (ExceptT String IO) a
}
data Env = Env {
- envX :: SBV Integer
- envY :: SBV Integer
- result :: Maybe SVal
}
alloc :: String -> Alloc (SBV Integer)
allocEnv :: Alloc Env
data Term :: * -> * 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
newtype Eval a = Eval {
- unEval :: ReaderT Env (Except String) a
}
unsafeCastSBV :: SBV a -> SBV b
eval :: Term r -> Eval (SBV r)
runEval :: Env -> Term a -> Except String (SBV a)
newtype Program a = Program (Term a)
newtype Result = Result SVal
mkResult :: SBV a -> Result
runProgramEval :: Env -> Program a -> Except String Result
newtype Property = Property (Term Bool)
runPropertyEval :: Result -> Env -> Property -> Except String (SBV Bool)
data CheckResult
- = Proved
- | Counterexample Integer Integer
generalize :: Monad m => Identity a -> m a
newtype Q a = Q {
- runQ :: QueryT (ExceptT String IO) a
}
mkQuery :: Env -> Q CheckResult
check :: Program a -> Property -> IO (Either String CheckResult)
ex1 :: IO (Either String CheckResult)
ex2 :: IO (Either String CheckResult)
ex3 :: IO (Either String CheckResult)

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

newtype Alloc a Source #

Monad for allocating free variables.

Constructors

Alloc
Fields runAlloc :: SymbolicT (ExceptT String IO) a

Instances

Monad Alloc Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods (>>=) :: Alloc a -> (a -> Alloc b) -> Alloc b # (>>) :: Alloc a -> Alloc b -> Alloc b # return :: a -> Alloc a # fail :: String -> Alloc a #
Functor Alloc Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods fmap :: (a -> b) -> Alloc a -> Alloc b # (<$) :: a -> Alloc b -> Alloc a #
Applicative Alloc Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods pure :: a -> Alloc a # (<>) :: Alloc (a -> b) -> Alloc a -> Alloc b # liftA2 :: (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c # (>) :: Alloc a -> Alloc b -> Alloc b # (<*) :: Alloc a -> Alloc b -> Alloc a #
MonadIO Alloc Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods liftIO :: IO a -> Alloc a #
MonadSymbolic Alloc Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods symbolicEnv :: Alloc State Source #
MonadError String Alloc Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods throwError :: String -> Alloc a # catchError :: Alloc a -> (String -> Alloc a) -> Alloc a #

data Env Source #

Environment holding allocated variables.

Constructors

Env
Fields envX :: SBV Integer envY :: SBV Integer result :: Maybe SVal

Instances

Eq Env Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods (==) :: Env -> Env -> Bool # (/=) :: Env -> Env -> Bool #
Show Env Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods showsPrec :: Int -> Env -> ShowS # show :: Env -> String # showList :: [Env] -> ShowS #
MonadReader Env Eval Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods ask :: Eval Env # local :: (Env -> Env) -> Eval a -> Eval a # reader :: (Env -> a) -> Eval a #

alloc :: String -> Alloc (SBV Integer) Source #

Allocate an integer variable with the provided name.

allocEnv :: Alloc Env Source #

Allocate an Env holding all input variables for the program.

Symbolic term evaluation

data Term :: * -> * where Source #

The term language we use to express programs and properties.

Constructors

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

newtype Eval a Source #

Monad for performing symbolic evaluation.

Constructors

Eval
Fields unEval :: ReaderT Env (Except String) a

Instances

Monad Eval Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods (>>=) :: Eval a -> (a -> Eval b) -> Eval b # (>>) :: Eval a -> Eval b -> Eval b # return :: a -> Eval a # fail :: String -> Eval a #
Functor Eval Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods fmap :: (a -> b) -> Eval a -> Eval b # (<$) :: a -> Eval b -> Eval a #
Applicative Eval Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods pure :: a -> Eval a # (<>) :: Eval (a -> b) -> Eval a -> Eval b # liftA2 :: (a -> b -> c) -> Eval a -> Eval b -> Eval c # (>) :: Eval a -> Eval b -> Eval b # (<*) :: Eval a -> Eval b -> Eval a #
MonadReader Env Eval Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods ask :: Eval Env # local :: (Env -> Env) -> Eval a -> Eval a # reader :: (Env -> a) -> Eval a #
MonadError String Eval Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods throwError :: String -> Eval a # catchError :: Eval a -> (String -> Eval a) -> Eval a #

unsafeCastSBV :: SBV a -> SBV b Source #

Unsafe cast for symbolic values. In production code, we would check types instead.

eval :: Term r -> Eval (SBV r) Source #

Symbolic evaluation function for Term.

runEval :: Env -> Term a -> Except String (SBV a) Source #

Runs symbolic evaluation, sending a Term to a symbolic value (or failing). Used for symbolic evaluation of programs and properties.

newtype Program a Source #

A program that can reference two input variables, x and y.

Constructors

Program (Term a)

newtype Result Source #

A symbolic value representing the result of running a program -- its output.

Constructors

Result SVal

mkResult :: SBV a -> Result Source #

Makes a Result from a symbolic value.

runProgramEval :: Env -> Program a -> Except String Result Source #

Performs symbolic evaluation of a Program.

Property evaluation

newtype Property Source #

A property describes a quality of a Program. It is a Term yields a boolean value.

Constructors

Property (Term Bool)

runPropertyEval :: Result -> Env -> Property -> Except String (SBV Bool) Source #

Performs symbolic evaluation of a 'Property.

Checking whether a program satisfies a property

data CheckResult Source #

The result of checking the combination of a Program and a Property.

Constructors

Proved
Counterexample Integer Integer

Instances

Eq CheckResult Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods (==) :: CheckResult -> CheckResult -> Bool # (/=) :: CheckResult -> CheckResult -> Bool #
Show CheckResult Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods showsPrec :: Int -> CheckResult -> ShowS # show :: CheckResult -> String # showList :: [CheckResult] -> ShowS #

generalize :: Monad m => Identity a -> m a Source #

Sends an Identity computation to an arbitrary monadic computation.

newtype Q a Source #

Monad for querying a solver.

Constructors

Q
Fields runQ :: QueryT (ExceptT String IO) a

Instances

Monad Q Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods (>>=) :: Q a -> (a -> Q b) -> Q b # (>>) :: Q a -> Q b -> Q b # return :: a -> Q a # fail :: String -> Q a #
Functor Q Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods fmap :: (a -> b) -> Q a -> Q b # (<$) :: a -> Q b -> Q a #
Applicative Q Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods pure :: a -> Q a # (<>) :: Q (a -> b) -> Q a -> Q b # liftA2 :: (a -> b -> c) -> Q a -> Q b -> Q c # (>) :: Q a -> Q b -> Q b # (<*) :: Q a -> Q b -> Q a #
MonadIO Q Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods liftIO :: IO a -> Q a #
MonadQuery Q Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods queryState :: Q State Source #
MonadError String Q Source #
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods throwError :: String -> Q a # catchError :: Q a -> (String -> Q a) -> Q a #

mkQuery :: Env -> Q CheckResult Source #

Creates a computation that queries a solver and yields a CheckResult.

check :: Program a -> Property -> IO (Either String CheckResult) Source #

Checks a Property of a Program (or fails).

Some examples

ex1 :: IO (Either String CheckResult) Source #

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)

ex2 :: IO (Either String CheckResult) Source #

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

ex3 :: IO (Either String CheckResult) Source #

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"