-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.ADT.Expr
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A basic expression ADT example.
-----------------------------------------------------------------------------

{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE QuasiQuotes         #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.ADT.Expr where

import Data.SBV
import Data.SBV.Control
import Data.SBV.RegExp
import Data.SBV.Tuple
import qualified Data.SBV.List as SL

-- | A basic arithmetic expression type.
data Expr = Val Integer
          | Var String
          | Add Expr Expr
          | Mul Expr Expr
          | Let String Expr Expr

-- | Create a symbolic version of expressions.
mkSymbolic [''Expr]

-- | Show instance for 'Expr'.
instance Show Expr where
  show :: Expr -> String
show (Val Integer
i)     = Integer -> String
forall a. Show a => a -> String
show Integer
i
  show (Var String
a)     = String
a
  show (Add Expr
l Expr
r)   = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Mul Expr
l Expr
r)   = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" * " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Let String
s Expr
a Expr
b) = String
"(let " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Num instance, simplifies construction of values
instance Num Expr where
  fromInteger :: Integer -> Expr
fromInteger = Integer -> Expr
Val
  + :: Expr -> Expr -> Expr
(+)         = Expr -> Expr -> Expr
Add
  * :: Expr -> Expr -> Expr
(*)         = Expr -> Expr -> Expr
Mul
  abs :: Expr -> Expr
abs         = String -> Expr -> Expr
forall a. HasCallStack => String -> a
error String
"Num Expr: undefined abs"
  signum :: Expr -> Expr
signum      = String -> Expr -> Expr
forall a. HasCallStack => String -> a
error String
"Num Expr: undefined signum"
  negate :: Expr -> Expr
negate      = String -> Expr -> Expr
forall a. HasCallStack => String -> a
error String
"Num Expr: undefined negate"

-- | Num instance for the symbolic version
instance Num SExpr where
  fromInteger :: Integer -> SBV Expr
fromInteger = SBV Integer -> SBV Expr
sVal (SBV Integer -> SBV Expr)
-> (Integer -> SBV Integer) -> Integer -> SBV Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SBV Integer
forall a. SymVal a => a -> SBV a
literal
  + :: SBV Expr -> SBV Expr -> SBV Expr
(+)         = SBV Expr -> SBV Expr -> SBV Expr
sAdd
  * :: SBV Expr -> SBV Expr -> SBV Expr
(*)         = SBV Expr -> SBV Expr -> SBV Expr
sMul
  abs :: SBV Expr -> SBV Expr
abs         = String -> SBV Expr -> SBV Expr
forall a. HasCallStack => String -> a
error String
"Num SExpr: undefined abs"
  signum :: SBV Expr -> SBV Expr
signum      = String -> SBV Expr -> SBV Expr
forall a. HasCallStack => String -> a
error String
"Num SExpr: undefined signum"
  negate :: SBV Expr -> SBV Expr
negate      = String -> SBV Expr -> SBV Expr
forall a. HasCallStack => String -> a
error String
"Num SExpr: undefined negate"

-- | Validity: We require each variable appearing to be an identifier (lowercase letter followed by
-- any number of upper-lower case letters and digits), and all expressions are closed; i.e., any
-- variable referenced is introduced by an enclosing let expression.
isValid :: SExpr -> SBool
isValid :: SBV Expr -> SBool
isValid = SList String -> SBV Expr -> SBool
go SList String
forall a. SymVal a => SList a
SL.nil
  where isId :: a -> SBool
isId a
s = a
s a -> RegExp -> SBool
forall a. RegExpMatchable a => a -> RegExp -> SBool
`match` (RegExp
asciiLower RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
KStar (RegExp
asciiLetter RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
digit))
        go :: SList String -> SExpr -> SBool
        go :: SList String -> SBV Expr -> SBool
go = String
-> (SList String -> SBV Expr -> SBool)
-> SList String
-> SBV Expr
-> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"valid" ((SList String -> SBV Expr -> SBool)
 -> SList String -> SBV Expr -> SBool)
-> (SList String -> SBV Expr -> SBool)
-> SList String
-> SBV Expr
-> SBool
forall a b. (a -> b) -> a -> b
$ \SList String
env SBV Expr
expr -> [sCase|Expr expr of
                                                   Var s     -> isId s .&& s `SL.elem` env
                                                   Val _     -> sTrue
                                                   Add l r   -> go env l .&& go env r
                                                   Mul l r   -> go env l .&& go env r
                                                   Let s a b -> isId s .&& go env a .&& go (s SL..: env) b
                                                |]

-- | Evaluate an expression.
eval :: SExpr -> SInteger
eval :: SBV Expr -> SBV Integer
eval = SList (String, Integer) -> SBV Expr -> SBV Integer
go SList (String, Integer)
forall a. SymVal a => SList a
SL.nil
 where go :: SList (String, Integer) -> SExpr -> SInteger
       go :: SList (String, Integer) -> SBV Expr -> SBV Integer
go = String
-> (SList (String, Integer) -> SBV Expr -> SBV Integer)
-> SList (String, Integer)
-> SBV Expr
-> SBV Integer
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"eval" ((SList (String, Integer) -> SBV Expr -> SBV Integer)
 -> SList (String, Integer) -> SBV Expr -> SBV Integer)
-> (SList (String, Integer) -> SBV Expr -> SBV Integer)
-> SList (String, Integer)
-> SBV Expr
-> SBV Integer
forall a b. (a -> b) -> a -> b
$ \SList (String, Integer)
env SBV Expr
expr -> [sCase|Expr expr of
                                                 Val i     -> i
                                                 Var s     -> get env s
                                                 Add l r   -> go env l + go env r
                                                 Mul l r   -> go env l * go env r
                                                 Let s e r -> go (tuple (s, go env e) SL..: env) r
                                              |]

       get :: SList (String, Integer) -> SString -> SInteger
       get :: SList (String, Integer) -> SBV String -> SBV Integer
get = String
-> (SList (String, Integer) -> SBV String -> SBV Integer)
-> SList (String, Integer)
-> SBV String
-> SBV Integer
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"get" ((SList (String, Integer) -> SBV String -> SBV Integer)
 -> SList (String, Integer) -> SBV String -> SBV Integer)
-> (SList (String, Integer) -> SBV String -> SBV Integer)
-> SList (String, Integer)
-> SBV String
-> SBV Integer
forall a b. (a -> b) -> a -> b
$ \SList (String, Integer)
env SBV String
s -> SBool -> SBV Integer -> SBV Integer -> SBV Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList (String, Integer) -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList (String, Integer)
env) SBV Integer
0
                                         (SBV Integer -> SBV Integer) -> SBV Integer -> SBV Integer
forall a b. (a -> b) -> a -> b
$ let (SBV String
k, SBV Integer
v) = SBV (String, Integer) -> (SBV String, SBV Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SList (String, Integer) -> SBV (String, Integer)
forall a. SymVal a => SList a -> SBV a
SL.head SList (String, Integer)
env)
                                           in SBool -> SBV Integer -> SBV Integer -> SBV Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV String
s SBV String -> SBV String -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV String
k) SBV Integer
v (SList (String, Integer) -> SBV String -> SBV Integer
get (SList (String, Integer) -> SList (String, Integer)
forall a. SymVal a => SList a -> SList a
SL.tail SList (String, Integer)
env) SBV String
s)

-- | A basic theorem about 'eval'.
-- >>> evalPlus5
-- Q.E.D.
evalPlus5 :: IO ThmResult
evalPlus5 :: IO ThmResult
evalPlus5 = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do SBV Expr
e :: SExpr <- String -> Symbolic (SBV Expr)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"e"
                       SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBV Integer
eval (SBV Expr
e SBV Expr -> SBV Expr -> SBV Expr
forall a. Num a => a -> a -> a
+ SBV Expr
5) SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
5 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Expr -> SBV Integer
eval SBV Expr
e

-- | A simple sat result example.
--
-- >>> evalSat
-- Satisfiable. Model:
--   e = Let "k" (Val 1) (Var "k") :: Expr
--   a =                         9 :: Integer
--   b =                        10 :: Integer
evalSat :: IO SatResult
evalSat :: IO SatResult
evalSat = SymbolicT IO SBool -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SBV Expr
e :: SExpr    <- String -> Symbolic (SBV Expr)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"e"
                   SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBool
isValid SBV Expr
e
                   SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBool
isLet   SBV Expr
e

                   SBV Integer
a :: SInteger <- String -> Symbolic (SBV Integer)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"a"
                   SBV Integer
b :: SInteger <- String -> Symbolic (SBV Integer)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"b"
                   SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Integer
a SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
4
                   SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Integer
b SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
10

                   SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBV Integer
eval (SBV Expr
e SBV Expr -> SBV Expr -> SBV Expr
forall a. Num a => a -> a -> a
+ SBV Integer -> SBV Expr
sVal SBV Integer
a) SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Expr -> SBV Integer
eval SBV Expr
e

-- | Another test, generating some (mildly) interesting examples.
--
-- >>> genE
-- Satisfiable. Model:
--   e1 = Let "p" (Val 5) (Val 3) :: Expr
--   e2 =                Val (-2) :: Expr
genE :: IO SatResult
genE :: IO SatResult
genE = SymbolicT IO () -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SymbolicT IO () -> IO SatResult)
-> SymbolicT IO () -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SBV Expr
e1 :: SExpr <- String -> Symbolic (SBV Expr)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"e1"
                SBV Expr
e2 :: SExpr <- String -> Symbolic (SBV Expr)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"e2"

                SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBool
isValid SBV Expr
e1
                SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBool
isValid SBV Expr
e2

                SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr
e1 SBV Expr -> SBV Expr -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./== SBV Expr
e2
                SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBool
isLet SBV Expr
e1
                SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBV Integer
eval SBV Expr
e1 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
3
                SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBV Integer
eval SBV Expr
e1 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Expr -> SBV Integer
eval SBV Expr
e2 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
5

-- | Query mode example.
--
-- >>> queryE
-- e1: (let p = 5 in 3)
-- e2: -2
queryE :: IO ()
queryE :: IO ()
queryE = SymbolicT IO () -> IO ()
forall a. Symbolic a -> IO a
runSMT (SymbolicT IO () -> IO ()) -> SymbolicT IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
           SBV Expr
e1 :: SExpr <- String -> Symbolic (SBV Expr)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"e1"
           SBV Expr
e2 :: SExpr <- String -> Symbolic (SBV Expr)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"e2"

           SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBool
isValid SBV Expr
e1
           SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBool
isValid SBV Expr
e2

           SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr
e1 SBV Expr -> SBV Expr -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./== SBV Expr
e2
           SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBool
isLet SBV Expr
e1
           SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBV Integer
eval SBV Expr
e1 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
3
           SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Expr -> SBV Integer
eval SBV Expr
e1 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Expr -> SBV Integer
eval SBV Expr
e2 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
5

           Query () -> SymbolicT IO ()
forall a. Query a -> Symbolic a
query (Query () -> SymbolicT IO ()) -> Query () -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
                      case CheckSatResult
cs of
                        CheckSatResult
Sat -> do Expr
e1v <- SBV Expr -> Query Expr
forall a. SymVal a => SBV a -> Query a
getValue SBV Expr
e1
                                  Expr
e2v <- SBV Expr -> Query Expr
forall a. SymVal a => SBV a -> Query a
getValue SBV Expr
e2
                                  IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"e1: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e1v
                                  IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"e2: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e2v
                        CheckSatResult
_   -> String -> Query ()
forall a. HasCallStack => String -> a
error (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"Unexpected result: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CheckSatResult -> String
forall a. Show a => a -> String
show CheckSatResult
cs