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

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.ADT.Param 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 nm val = Val val
                 | Var nm
                 | Add (Expr nm val) (Expr nm val)
                 | Mul (Expr nm val) (Expr nm val)
                 | Let nm (Expr nm val) (Expr nm val)

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

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

-- | Show instance for 'Expr', specialized when name is string.
instance {-# OVERLAPPING #-} Show val => Show (Expr String val) where
  show :: Expr String val -> String
show (Val val
i)     = val -> String
forall a. Show a => a -> String
show val
i
  show (Var String
a)     = String
a
  show (Add Expr String val
l Expr String val
r)   = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr String val -> String
forall a. Show a => a -> String
show Expr String val
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr String val -> String
forall a. Show a => a -> String
show Expr String val
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Mul Expr String val
l Expr String val
r)   = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr String val -> String
forall a. Show a => a -> String
show Expr String val
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" * " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr String val -> String
forall a. Show a => a -> String
show Expr String val
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Let String
s Expr String val
a Expr String val
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 val -> String
forall a. Show a => a -> String
show Expr String val
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr String val -> String
forall a. Show a => a -> String
show Expr String val
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

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

-- | Validity: We require each variable appearing to be an identifier to satisfy the predicate given.
-- 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 :: (SymVal nm, Eq nm, SymVal val) => (SBV nm -> SBool) -> SExpr nm val -> SBool
isValid :: forall nm val.
(SymVal nm, Eq nm, SymVal val) =>
(SBV nm -> SBool) -> SExpr nm val -> SBool
isValid SBV nm -> SBool
nmChk = SList nm -> SBV (Expr nm val) -> SBool
go SList nm
forall a. SymVal a => SList a
SL.nil
  where go :: SList nm -> SBV (Expr nm val) -> SBool
go = String
-> (SList nm -> SBV (Expr nm val) -> SBool)
-> SList nm
-> SBV (Expr nm val)
-> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda (SymbolicT IO) a) =>
String -> a -> a
smtFunction String
"valid" ((SList nm -> SBV (Expr nm val) -> SBool)
 -> SList nm -> SBV (Expr nm val) -> SBool)
-> (SList nm -> SBV (Expr nm val) -> SBool)
-> SList nm
-> SBV (Expr nm val)
-> SBool
forall a b. (a -> b) -> a -> b
$ \SList nm
env SBV (Expr nm val)
expr -> [sCase|Expr expr of
                                                   Var s     -> nmChk 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 -> nmChk s  .&& go env a .&& go (s SL..: env) b
                                                |]

-- | Evaluate an expression.
eval :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val
eval :: forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval = SList (nm, val) -> SBV (Expr nm val) -> SBV val
go SList (nm, val)
forall a. SymVal a => SList a
SL.nil
 where go :: SList (nm, val) -> SBV (Expr nm val) -> SBV val
go = String
-> (SList (nm, val) -> SBV (Expr nm val) -> SBV val)
-> SList (nm, val)
-> SBV (Expr nm val)
-> SBV val
forall a.
(SMTDefinable a, Typeable a, Lambda (SymbolicT IO) a) =>
String -> a -> a
smtFunction String
"eval" ((SList (nm, val) -> SBV (Expr nm val) -> SBV val)
 -> SList (nm, val) -> SBV (Expr nm val) -> SBV val)
-> (SList (nm, val) -> SBV (Expr nm val) -> SBV val)
-> SList (nm, val)
-> SBV (Expr nm val)
-> SBV val
forall a b. (a -> b) -> a -> b
$ \SList (nm, val)
env SBV (Expr nm val)
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 (nm, val) -> SBV nm -> SBV val
get = String
-> (SList (nm, val) -> SBV nm -> SBV val)
-> SList (nm, val)
-> SBV nm
-> SBV val
forall a.
(SMTDefinable a, Typeable a, Lambda (SymbolicT IO) a) =>
String -> a -> a
smtFunction String
"get" ((SList (nm, val) -> SBV nm -> SBV val)
 -> SList (nm, val) -> SBV nm -> SBV val)
-> (SList (nm, val) -> SBV nm -> SBV val)
-> SList (nm, val)
-> SBV nm
-> SBV val
forall a b. (a -> b) -> a -> b
$ \SList (nm, val)
env SBV nm
s -> SBool -> SBV val -> SBV val -> SBV val
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList (nm, val) -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList (nm, val)
env) SBV val
0
                                         (SBV val -> SBV val) -> SBV val -> SBV val
forall a b. (a -> b) -> a -> b
$ let (SBV nm
k, SBV val
v) = SBV (nm, val) -> (SBV nm, SBV val)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SList (nm, val) -> SBV (nm, val)
forall a. SymVal a => SList a -> SBV a
SL.head SList (nm, val)
env)
                                           in SBool -> SBV val -> SBV val -> SBV val
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV nm
s SBV nm -> SBV nm -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV nm
k) SBV val
v (SList (nm, val) -> SBV nm -> SBV val
get (SList (nm, val) -> SList (nm, val)
forall a. SymVal a => SList a -> SList a
SL.tail SList (nm, val)
env) SBV nm
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 SExpr String Integer
e :: SExpr String Integer <- String -> Symbolic (SExpr String Integer)
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
$ SExpr String Integer -> SBV Integer
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval (SExpr String Integer
e SExpr String Integer
-> SExpr String Integer -> SExpr String Integer
forall a. Num a => a -> a -> a
+ SExpr String Integer
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
+ SExpr String Integer -> SBV Integer
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval SExpr String Integer
e

-- | Is this a string identifier? Lowercase letter followed by any number of upeer-lower case letters nd digits.
isId :: SString -> SBool
isId :: SString -> SBool
isId SString
s = SString
s SString -> 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))

-- | A simple sat result example.
--
-- >>> evalSat
-- Satisfiable. Model:
--   e = Let "h" (Val 1) (Var "h") :: Expr String Integer
--   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 SExpr String Integer
e :: SExpr String Integer  <- String -> Symbolic (SExpr String Integer)
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
$ (SString -> SBool) -> SExpr String Integer -> SBool
forall nm val.
(SymVal nm, Eq nm, SymVal val) =>
(SBV nm -> SBool) -> SExpr nm val -> SBool
isValid SString -> SBool
isId SExpr String Integer
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
$ SExpr String Integer -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isLet   SExpr String Integer
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
$ SExpr String Integer -> SBV Integer
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval (SExpr String Integer
e SExpr String Integer
-> SExpr String Integer -> SExpr String Integer
forall a. Num a => a -> a -> a
+ SBV Integer -> SExpr String Integer
forall nm val.
(SymVal nm, SymVal val) =>
SBV val -> SBV (Expr nm val)
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
* SExpr String Integer -> SBV Integer
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval SExpr String Integer
e

-- | Another test, generating some (mildly) interesting examples.
--
-- >>> genE
-- Satisfiable. Model:
--   e1 =                      Let "s" (Val 6) (Val 3) :: Expr String Integer
--   e2 = Let "h" (Val (-1)) (Add (Var "h") (Var "h")) :: Expr String Integer
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 SExpr String Integer
e1 :: SExpr String Integer <- String -> Symbolic (SExpr String Integer)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"e1"
                SExpr String Integer
e2 :: SExpr String Integer <- String -> Symbolic (SExpr String Integer)
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
$ (SString -> SBool) -> SExpr String Integer -> SBool
forall nm val.
(SymVal nm, Eq nm, SymVal val) =>
(SBV nm -> SBool) -> SExpr nm val -> SBool
isValid SString -> SBool
isId SExpr String Integer
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
$ (SString -> SBool) -> SExpr String Integer -> SBool
forall nm val.
(SymVal nm, Eq nm, SymVal val) =>
(SBV nm -> SBool) -> SExpr nm val -> SBool
isValid SString -> SBool
isId SExpr String Integer
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
$ SExpr String Integer
e1 SExpr String Integer -> SExpr String Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./== SExpr String Integer
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
$ SExpr String Integer -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isLet SExpr String Integer
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
$ SExpr String Integer -> SBV Integer
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval SExpr String Integer
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
$ SExpr String Integer -> SBV Integer
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval SExpr String Integer
e1 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SExpr String Integer -> SBV Integer
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval SExpr String Integer
e2 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
5

-- | Query mode example.
--
-- >>> queryE
-- e1: (let p = (-3 * -1) in (1 * p))
-- e2: -2
-- e3: (let q = 96 % 97 in q)
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
           SExpr String Integer
e1 :: SExpr String Integer <- String -> Symbolic (SExpr String Integer)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"e1"
           SExpr String Integer
e2 :: SExpr String Integer <- String -> Symbolic (SExpr String Integer)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"e2"

           SExpr String Rational
e3 :: SExpr String Rational <- String -> Symbolic (SExpr String Rational)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"e3"

           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
$ (SString -> SBool) -> SExpr String Integer -> SBool
forall nm val.
(SymVal nm, Eq nm, SymVal val) =>
(SBV nm -> SBool) -> SExpr nm val -> SBool
isValid SString -> SBool
isId SExpr String Integer
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
$ (SString -> SBool) -> SExpr String Integer -> SBool
forall nm val.
(SymVal nm, Eq nm, SymVal val) =>
(SBV nm -> SBool) -> SExpr nm val -> SBool
isValid SString -> SBool
isId SExpr String Integer
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
$ (SString -> SBool) -> SExpr String Rational -> SBool
forall nm val.
(SymVal nm, Eq nm, SymVal val) =>
(SBV nm -> SBool) -> SExpr nm val -> SBool
isValid SString -> SBool
isId SExpr String Rational
e3

           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
$ SExpr String Integer
e1 SExpr String Integer -> SExpr String Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./== SExpr String Integer
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
$ SExpr String Integer -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isLet SExpr String Integer
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
$ SExpr String Integer -> SBV Integer
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval SExpr String Integer
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
$ SExpr String Integer -> SBV Integer
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval SExpr String Integer
e1 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SExpr String Integer -> SBV Integer
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
eval SExpr String Integer
e2 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
5

           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
$ SExpr String Rational -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isLet SExpr String Rational
e3
           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
$ SExpr String Integer -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isMul (SExpr String Integer -> SExpr String Integer
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
getLet_2 SExpr String Integer
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
$ SExpr String Integer -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isMul (SExpr String Integer -> SExpr String Integer
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
getLet_3 SExpr String Integer
e1)

           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 String Integer
e1v <- SExpr String Integer -> Query (Expr String Integer)
forall a. SymVal a => SBV a -> Query a
getValue SExpr String Integer
e1
                                  Expr String Integer
e2v <- SExpr String Integer -> Query (Expr String Integer)
forall a. SymVal a => SBV a -> Query a
getValue SExpr String Integer
e2
                                  Expr String Rational
e3v <- SExpr String Rational -> Query (Expr String Rational)
forall a. SymVal a => SBV a -> Query a
getValue SExpr String Rational
e3
                                  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 Integer -> String
forall a. Show a => a -> String
show Expr String Integer
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 Integer -> String
forall a. Show a => a -> String
show Expr String Integer
e2v
                                  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
"e3: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr String Rational -> String
forall a. Show a => a -> String
show Expr String Rational
e3v
                        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