Documentation.SBV.Examples.Transformers.SymbolicEval

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.

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

newtype Alloc a

Monad for allocating free variables.

Constructors

Alloc

Fields

• runAlloc :: SymbolicT (ExceptT String IO) a

Instances

Monad Alloc

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

Functor Alloc

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

fmap :: (a -> b) -> Alloc a -> Alloc b

(<$) :: a -> Alloc b -> Alloc a

Applicative Alloc

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

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

liftIO :: IO a -> Alloc a

MonadSymbolic Alloc

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

symbolicEnv :: Alloc State

MonadError String Alloc

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

throwError :: String -> Alloc a

catchError :: Alloc a -> (String -> Alloc a) -> Alloc a

data Env

Environment holding allocated variables.

Constructors

Env

Fields

• envX :: SBV Integer
• envY :: SBV Integer
• result :: Maybe SVal

Instances

Eq Env

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

(==) :: Env -> Env -> Bool

(/=) :: Env -> Env -> Bool

Show Env

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

showsPrec :: Int -> Env -> ShowS

show :: Env -> String

showList :: [Env] -> ShowS

MonadReader Env Eval

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)

Allocate an integer variable with the provided name.

allocEnv :: Alloc Env

Allocate an Env holding all input variables for the program.

Symbolic term evaluation

data Term :: Type -> Type where

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

Monad for performing symbolic evaluation.

Constructors

Eval

Fields

• unEval :: ReaderT Env (Except String) a

Instances

Monad Eval

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

Functor Eval

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

fmap :: (a -> b) -> Eval a -> Eval b

(<$) :: a -> Eval b -> Eval a

Applicative Eval

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

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

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

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

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

Symbolic evaluation function for Term.

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

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

newtype Program a

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

Constructors

Program (Term a)

newtype Result

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

Constructors

Result SVal

mkResult :: SBV a -> Result

Makes a Result from a symbolic value.

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

Performs symbolic evaluation of a Program.

Property evaluation

newtype Property

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)

Performs symbolic evaluation of a 'Property.

Checking whether a program satisfies a property

data CheckResult

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

Constructors

Proved

Counterexample Integer Integer

Instances

Eq CheckResult

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

(==) :: CheckResult -> CheckResult -> Bool

(/=) :: CheckResult -> CheckResult -> Bool

Show CheckResult

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

Sends an Identity computation to an arbitrary monadic computation.

newtype Q a

Monad for querying a solver.

Constructors

Q

Fields

• runQ :: QueryT (ExceptT String IO) a

Instances

Monad Q

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

Functor Q

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

fmap :: (a -> b) -> Q a -> Q b

(<$) :: a -> Q b -> Q a

Applicative Q

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

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

liftIO :: IO a -> Q a

MonadQuery Q

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

queryState :: Q State

MonadError String Q

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

throwError :: String -> Q a

catchError :: Q a -> (String -> Q a) -> Q a

mkQuery :: Env -> Q CheckResult

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

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

Checks a Property of a Program (or fails).

Some examples

ex1 :: IO (Either String CheckResult)

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 9 0)

ex2 :: IO (Either String CheckResult)

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)

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"