{-# LANGUAGE Safe #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternGuards #-}
-- | A module for interacting with an SMT solver, using SmtLib-2 format.
module SimpleSMT
  (
    -- * Basic Solver Interface
    Solver(..)
  , newSolver
  , newSolverNotify
  , newSolverWithConfig
  , Config(..)
  , SolverLogger(..)
  , defaultConfig
  , noSolverLogger
  , heraldSolverLogger
  , smtSolverLogger
  , ackCommand
  , simpleCommand
  , simpleCommandMaybe
  , loadFile
  , loadString

    -- ** S-Expressions
  , SExpr(..)
  , showsSExpr, ppSExpr, readSExpr

    -- ** Logging and Debugging
  , Logger(..)
  , newLogger
  , newLoggerWithHandle
  , withLogLevel
  , logMessageAt
  , logIndented

    -- * Common SmtLib-2 Commands
  , setLogic, setLogicMaybe
  , setOption, setOptionMaybe
  , produceUnsatCores
  , named
  , push, pushMany
  , pop, popMany
  , inNewScope
  , declare
  , declareFun
  , declareDatatype
  , define
  , defineFun
  , defineFunRec
  , defineFunsRec
  , assert
  , check
  , Result(..)
  , getExprs, getExpr
  , getConsts, getConst
  , getUnsatCore
  , Value(..)
  , sexprToVal

    -- * Convenience Functions for SmtLib-2 Expressions
  , fam
  , fun
  , const
  , app

    -- * Convenience Functions for SmtLib-2 identifiers
  , quoteSymbol
  , symbol
  , keyword
  , as

    -- ** Types
  , tInt
  , tBool
  , tReal
  , tArray
  , tBits

    -- ** Literals
  , int
  , real
  , bool
  , bvBin
  , bvHex
  , value

    -- ** Connectives
  , not
  , and
  , andMany
  , or
  , orMany
  , xor
  , implies

    -- ** If-then-else
  , ite

    -- ** Relational Predicates
  , eq
  , distinct
  , gt
  , lt
  , geq
  , leq
  , bvULt
  , bvULeq
  , bvSLt
  , bvSLeq

    -- ** Arithmetic
  , add
  , addMany
  , sub
  , neg
  , mul
  , abs
  , div
  , mod
  , divisible
  , realDiv
  , toInt
  , toReal

    -- ** Bit Vectors
  , concat
  , extract
  , bvNot
  , bvNeg
  , bvAnd
  , bvXOr
  , bvOr
  , bvAdd
  , bvSub
  , bvMul
  , bvUDiv
  , bvURem
  , bvSDiv
  , bvSRem
  , bvShl
  , bvLShr
  , bvAShr
  , signExtend
  , zeroExtend

    -- ** Arrays
  , select
  , store
  ) where

import Prelude hiding (not, and, or, abs, div, mod, concat, const)
import qualified Prelude as P
import Data.Char(isSpace, isDigit)
import Data.List(unfoldr,intersperse)
import Data.Bits(testBit)
import Data.IORef(newIORef, atomicModifyIORef, modifyIORef', readIORef,
                  writeIORef)
import System.Process(runInteractiveProcess, waitForProcess, terminateProcess)
import System.IO (Handle, hFlush, hGetLine, hGetContents, hPutStr, hPutStrLn,
                  stdout, hClose)
import System.Exit(ExitCode)
import qualified Control.Exception as X
import Control.Concurrent(forkIO)
import Control.Monad(forever,when,void)
import Text.Read(readMaybe)
import Data.Ratio((%), numerator, denominator)
import Numeric(showHex, readHex, showFFloat)


-- | Results of checking for satisfiability.
data Result = Sat         -- ^ The assertions are satisfiable
            | Unsat       -- ^ The assertions are unsatisfiable
            | Unknown     -- ^ The result is inconclusive
              deriving (Result -> Result -> Bool
(Result -> Result -> Bool)
-> (Result -> Result -> Bool) -> Eq Result
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Result -> Result -> Bool
== :: Result -> Result -> Bool
$c/= :: Result -> Result -> Bool
/= :: Result -> Result -> Bool
Eq,Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Result -> ShowS
showsPrec :: Int -> Result -> ShowS
$cshow :: Result -> String
show :: Result -> String
$cshowList :: [Result] -> ShowS
showList :: [Result] -> ShowS
Show)

-- | Common values returned by SMT solvers.
data Value =  Bool  !Bool           -- ^ Boolean value
            | Int   !Integer        -- ^ Integral value
            | Real  !Rational       -- ^ Rational value
            | Bits  !Int !Integer   -- ^ Bit vector: width, value
            | Other !SExpr          -- ^ Some other value
              deriving (Value -> Value -> Bool
(Value -> Value -> Bool) -> (Value -> Value -> Bool) -> Eq Value
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
/= :: Value -> Value -> Bool
Eq,Int -> Value -> ShowS
[Value] -> ShowS
Value -> String
(Int -> Value -> ShowS)
-> (Value -> String) -> ([Value] -> ShowS) -> Show Value
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Value -> ShowS
showsPrec :: Int -> Value -> ShowS
$cshow :: Value -> String
show :: Value -> String
$cshowList :: [Value] -> ShowS
showList :: [Value] -> ShowS
Show)

-- | S-expressions. These are the basic format for SmtLib-2.
data SExpr  = Atom String
            | List [SExpr]
              deriving (SExpr -> SExpr -> Bool
(SExpr -> SExpr -> Bool) -> (SExpr -> SExpr -> Bool) -> Eq SExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SExpr -> SExpr -> Bool
== :: SExpr -> SExpr -> Bool
$c/= :: SExpr -> SExpr -> Bool
/= :: SExpr -> SExpr -> Bool
Eq, Eq SExpr
Eq SExpr =>
(SExpr -> SExpr -> Ordering)
-> (SExpr -> SExpr -> Bool)
-> (SExpr -> SExpr -> Bool)
-> (SExpr -> SExpr -> Bool)
-> (SExpr -> SExpr -> Bool)
-> (SExpr -> SExpr -> SExpr)
-> (SExpr -> SExpr -> SExpr)
-> Ord SExpr
SExpr -> SExpr -> Bool
SExpr -> SExpr -> Ordering
SExpr -> SExpr -> SExpr
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SExpr -> SExpr -> Ordering
compare :: SExpr -> SExpr -> Ordering
$c< :: SExpr -> SExpr -> Bool
< :: SExpr -> SExpr -> Bool
$c<= :: SExpr -> SExpr -> Bool
<= :: SExpr -> SExpr -> Bool
$c> :: SExpr -> SExpr -> Bool
> :: SExpr -> SExpr -> Bool
$c>= :: SExpr -> SExpr -> Bool
>= :: SExpr -> SExpr -> Bool
$cmax :: SExpr -> SExpr -> SExpr
max :: SExpr -> SExpr -> SExpr
$cmin :: SExpr -> SExpr -> SExpr
min :: SExpr -> SExpr -> SExpr
Ord, Int -> SExpr -> ShowS
[SExpr] -> ShowS
SExpr -> String
(Int -> SExpr -> ShowS)
-> (SExpr -> String) -> ([SExpr] -> ShowS) -> Show SExpr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SExpr -> ShowS
showsPrec :: Int -> SExpr -> ShowS
$cshow :: SExpr -> String
show :: SExpr -> String
$cshowList :: [SExpr] -> ShowS
showList :: [SExpr] -> ShowS
Show)

-- | Show an s-expression.
--
-- >>> let Just (e, _) = readSExpr "(assert (= ((_ map (- (Int Int) Int)) a1Cl a1Cm) a1Cv))"
-- >>> putStrLn $ showsSExpr e ""
-- (assert (= ((_ map (- (Int Int) Int)) a1Cl a1Cm) a1Cv))
showsSExpr :: SExpr -> ShowS
showsSExpr :: SExpr -> ShowS
showsSExpr SExpr
ex =
  case SExpr
ex of
    Atom String
x  -> String -> ShowS
showString String
x
    List [] -> String -> ShowS
showString String
"()"
    List (SExpr
e0 : [SExpr]
es) -> Char -> ShowS
showChar Char
'(' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SExpr -> ShowS
showsSExpr SExpr
e0 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                       (SExpr -> ShowS -> ShowS) -> ShowS -> [SExpr] -> ShowS
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\SExpr
e ShowS
m -> Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SExpr -> ShowS
showsSExpr SExpr
e ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
m)
                       (Char -> ShowS
showChar Char
')') [SExpr]
es


-- | Show an s-expression in a somewhat readable fashion.
--
-- >>> let Just (e, _) = readSExpr "(assert (= ((_ map (- (Int Int) Int)) a1Cl a1Cm) a1Cv))"
-- >>> putStrLn $ ppSExpr e ""
-- (assert
--    (=
--       (
--         (_
--            map
--            (-
--               (Int Int)
--               Int))
--         a1Cl
--         a1Cm)
--       a1Cv))
ppSExpr :: SExpr -> ShowS
ppSExpr :: SExpr -> ShowS
ppSExpr = Int -> SExpr -> ShowS
go Int
0
  where
  tab :: Int -> ShowS
tab Int
n = String -> ShowS
showString (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n Char
' ')
  many :: [b -> b] -> b -> b
many  = ((b -> b) -> (b -> b) -> b -> b) -> (b -> b) -> [b -> b] -> b -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) b -> b
forall a. a -> a
id

  new :: Int -> SExpr -> ShowS
new Int
n SExpr
e = Char -> ShowS
showChar Char
'\n' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
tab Int
n ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SExpr -> ShowS
go Int
n SExpr
e

  small :: t -> [SExpr] -> Maybe [ShowS]
small t
n [SExpr]
es =
    case [SExpr]
es of
      [] -> [ShowS] -> Maybe [ShowS]
forall a. a -> Maybe a
Just []
      SExpr
e : [SExpr]
more
        | t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
0 -> Maybe [ShowS]
forall a. Maybe a
Nothing
        | Bool
otherwise -> case SExpr
e of
                         Atom String
x -> (String -> ShowS
showString String
x ShowS -> [ShowS] -> [ShowS]
forall a. a -> [a] -> [a]
:) ([ShowS] -> [ShowS]) -> Maybe [ShowS] -> Maybe [ShowS]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> [SExpr] -> Maybe [ShowS]
small (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) [SExpr]
more
                         SExpr
_      -> Maybe [ShowS]
forall a. Maybe a
Nothing

  go :: Int -> SExpr -> ShowS
  go :: Int -> SExpr -> ShowS
go Int
n SExpr
ex =
    case SExpr
ex of
      Atom String
x        -> String -> ShowS
showString String
x
      List [SExpr]
es
        | Just [ShowS]
fs <- Integer -> [SExpr] -> Maybe [ShowS]
forall {t}. (Ord t, Num t) => t -> [SExpr] -> Maybe [ShowS]
small Integer
5 [SExpr]
es ->
          Char -> ShowS
showChar Char
'(' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ShowS] -> ShowS
forall {b}. [b -> b] -> b -> b
many (ShowS -> [ShowS] -> [ShowS]
forall a. a -> [a] -> [a]
intersperse (Char -> ShowS
showChar Char
' ') [ShowS]
fs) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
')'

      List (Atom String
x : [SExpr]
es) -> String -> ShowS
showString String
"(" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                [ShowS] -> ShowS
forall {b}. [b -> b] -> b -> b
many ((SExpr -> ShowS) -> [SExpr] -> [ShowS]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> SExpr -> ShowS
new (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
3)) [SExpr]
es) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
")"

      List [SExpr]
es -> String -> ShowS
showString String
"(" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ShowS] -> ShowS
forall {b}. [b -> b] -> b -> b
many ((SExpr -> ShowS) -> [SExpr] -> [ShowS]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> SExpr -> ShowS
new (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2)) [SExpr]
es) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
")"

-- | Parse an s-expression.
--
-- >>> readSExpr "(_ map (- (Int Int) Int)) a1Cl a1Cm)"
-- Just (List [Atom "_",Atom "map",List [Atom "-",List [Atom "Int",Atom "Int"],Atom "Int"]]," a1Cl a1Cm)")
readSExpr :: String -> Maybe (SExpr, String)
readSExpr :: String -> Maybe (SExpr, String)
readSExpr (Char
c : String
more) | Char -> Bool
isSpace Char
c = String -> Maybe (SExpr, String)
readSExpr String
more
readSExpr (Char
';' : String
more) = String -> Maybe (SExpr, String)
readSExpr (String -> Maybe (SExpr, String))
-> String -> Maybe (SExpr, String)
forall a b. (a -> b) -> a -> b
$ Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
1 ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\n') String
more
readSExpr (Char
'|' : String
more) = do (String
sym, Char
'|' : String
rest) <- (String, String) -> Maybe (String, String)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Char
'|') String
more)
                            (SExpr, String) -> Maybe (SExpr, String)
forall a. a -> Maybe a
Just (String -> SExpr
Atom (Char
'|' Char -> ShowS
forall a. a -> [a] -> [a]
: String
sym String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char
'|']), String
rest)
readSExpr (Char
'(' : String
more) = do ([SExpr]
xs,String
more1) <- String -> Maybe ([SExpr], String)
list String
more
                            (SExpr, String) -> Maybe (SExpr, String)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([SExpr] -> SExpr
List [SExpr]
xs, String
more1)
  where
  list :: String -> Maybe ([SExpr], String)
list (Char
c : String
txt) | Char -> Bool
isSpace Char
c = String -> Maybe ([SExpr], String)
list String
txt
  list (Char
')' : String
txt) = ([SExpr], String) -> Maybe ([SExpr], String)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], String
txt)
  list String
txt         = do (SExpr
v,String
txt1) <- String -> Maybe (SExpr, String)
readSExpr String
txt
                        ([SExpr]
vs,String
txt2) <- String -> Maybe ([SExpr], String)
list String
txt1
                        ([SExpr], String) -> Maybe ([SExpr], String)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr
vSExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
:[SExpr]
vs, String
txt2)
readSExpr String
txt     = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
end String
txt of
                       (String
as,String
bs) | Bool -> Bool
P.not (String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
as) -> (SExpr, String) -> Maybe (SExpr, String)
forall a. a -> Maybe a
Just (String -> SExpr
Atom String
as, String
bs)
                       (String, String)
_ -> Maybe (SExpr, String)
forall a. Maybe a
Nothing
  where end :: Char -> Bool
end Char
x = Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')' Bool -> Bool -> Bool
|| Char -> Bool
isSpace Char
x


--------------------------------------------------------------------------------

-- | An interactive solver process.
data Solver = Solver
  { Solver -> SExpr -> IO SExpr
command   :: SExpr -> IO SExpr
    -- ^ Send a command to the solver.

  , Solver -> IO ExitCode
stop :: IO ExitCode
    -- ^ Wait for the solver to finish and exit gracefully.

  , Solver -> IO ExitCode
forceStop :: IO ExitCode
    -- ^ Terminate the solver without waiting for it to finish.
  }


-- | Start a new solver process.
newSolver :: String       {- ^ Executable -}            ->
             [String]     {- ^ Arguments -}             ->
             Maybe Logger {- ^ Optional logging here -} ->
             IO Solver
newSolver :: String -> [String] -> Maybe Logger -> IO Solver
newSolver String
exe [String]
opts Maybe Logger
mbLog = Config -> IO Solver
newSolverWithConfig (Config -> IO Solver) -> Config -> IO Solver
forall a b. (a -> b) -> a -> b
$
  (String -> [String] -> Config
defaultConfig String
exe [String]
opts)
    { solverLogger = maybe noSolverLogger heraldSolverLogger mbLog
    }

newSolverNotify ::
  String        {- ^ Executable -}            ->
  [String]      {- ^ Arguments -}             ->
  Maybe Logger  {- ^ Optional logging here -} ->
  Maybe (ExitCode -> IO ()) {- ^ Do this when the solver exits -} ->
  IO Solver
newSolverNotify :: String
-> [String]
-> Maybe Logger
-> Maybe (ExitCode -> IO ())
-> IO Solver
newSolverNotify String
exe [String]
opts Maybe Logger
mbLog Maybe (ExitCode -> IO ())
mbOnExit = Config -> IO Solver
newSolverWithConfig (Config -> IO Solver) -> Config -> IO Solver
forall a b. (a -> b) -> a -> b
$
  (String -> [String] -> Config
defaultConfig String
exe [String]
opts)
    { solverOnExit = mbOnExit
    , solverLogger = maybe noSolverLogger heraldSolverLogger mbLog
    }

-- | Start a new solver process using the provided 'Config' options.
newSolverWithConfig :: Config -> IO Solver
newSolverWithConfig :: Config -> IO Solver
newSolverWithConfig
  (Config { solverExecutable :: Config -> String
solverExecutable = String
exe
          , solverArguments :: Config -> [String]
solverArguments = [String]
opts
          , solverOnExit :: Config -> Maybe (ExitCode -> IO ())
solverOnExit = Maybe (ExitCode -> IO ())
mbOnExit
          , solverLogger :: Config -> SolverLogger
solverLogger = SolverLogger
log
          }) =
  do (Handle
hIn, Handle
hOut, Handle
hErr, ProcessHandle
h) <- String
-> [String]
-> Maybe String
-> Maybe [(String, String)]
-> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveProcess String
exe [String]
opts Maybe String
forall a. Maybe a
Nothing Maybe [(String, String)]
forall a. Maybe a
Nothing

     ThreadId
_ <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever (do String
errs <- Handle -> IO String
hGetLine Handle
hErr
                               SolverLogger -> String -> IO ()
solverLogStdErr SolverLogger
log String
errs)
                    IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` \X.SomeException {} -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

     case Maybe (ExitCode -> IO ())
mbOnExit of
       Maybe (ExitCode -> IO ())
Nothing -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
       Just ExitCode -> IO ()
this -> IO ThreadId -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO () -> IO ThreadId
forkIO (ExitCode -> IO ()
this (ExitCode -> IO ()) -> IO ExitCode -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
h))

     IO (Maybe SExpr)
getResponse <-
       do String
txt <- Handle -> IO String
hGetContents Handle
hOut                  -- Read *all* output
          IORef [SExpr]
ref <- [SExpr] -> IO (IORef [SExpr])
forall a. a -> IO (IORef a)
newIORef ((String -> Maybe (SExpr, String)) -> String -> [SExpr]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr String -> Maybe (SExpr, String)
readSExpr String
txt)  -- Parse, and store result
          IO (Maybe SExpr) -> IO (IO (Maybe SExpr))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IO (Maybe SExpr) -> IO (IO (Maybe SExpr)))
-> IO (Maybe SExpr) -> IO (IO (Maybe SExpr))
forall a b. (a -> b) -> a -> b
$ IORef [SExpr]
-> ([SExpr] -> ([SExpr], Maybe SExpr)) -> IO (Maybe SExpr)
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef [SExpr]
ref (([SExpr] -> ([SExpr], Maybe SExpr)) -> IO (Maybe SExpr))
-> ([SExpr] -> ([SExpr], Maybe SExpr)) -> IO (Maybe SExpr)
forall a b. (a -> b) -> a -> b
$ \[SExpr]
xs ->
                      case [SExpr]
xs of
                        []     -> ([SExpr]
xs, Maybe SExpr
forall a. Maybe a
Nothing)
                        SExpr
y : [SExpr]
ys -> ([SExpr]
ys, SExpr -> Maybe SExpr
forall a. a -> Maybe a
Just SExpr
y)

     let cmd :: SExpr -> IO ()
cmd SExpr
c = do let txt :: String
txt = SExpr -> ShowS
showsSExpr SExpr
c String
""
                    SolverLogger -> SExpr -> IO ()
solverLogSend SolverLogger
log SExpr
c
                    Handle -> String -> IO ()
hPutStrLn Handle
hIn String
txt
                    Handle -> IO ()
hFlush Handle
hIn

         command :: SExpr -> IO SExpr
command SExpr
c =
           do SExpr -> IO ()
cmd SExpr
c
              Maybe SExpr
mb <- IO (Maybe SExpr)
getResponse
              case Maybe SExpr
mb of
                Just SExpr
res -> do SolverLogger -> SExpr -> IO ()
solverLogRecv SolverLogger
log SExpr
res
                               SExpr -> IO SExpr
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SExpr
res
                Maybe SExpr
Nothing  -> String -> IO SExpr
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Missing response from solver"

         waitAndCleanup :: IO ExitCode
waitAndCleanup =
           do ExitCode
ec <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
h
              IO () -> (IOException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
X.catch (do Handle -> IO ()
hClose Handle
hIn
                          Handle -> IO ()
hClose Handle
hOut
                          Handle -> IO ()
hClose Handle
hErr)
                      (SolverLogger -> IOException -> IO ()
solverLogExcn SolverLogger
log)
              ExitCode -> IO ExitCode
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ExitCode
ec

         forceStop :: IO ExitCode
forceStop = ProcessHandle -> IO ()
terminateProcess ProcessHandle
h IO () -> IO ExitCode -> IO ExitCode
forall a b. IO a -> IO b -> IO b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> IO ExitCode
waitAndCleanup

         stop :: IO ExitCode
stop =
           do SExpr -> IO ()
cmd ([SExpr] -> SExpr
List [String -> SExpr
Atom String
"exit"])
                IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` (\X.SomeException{} -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
              IO ExitCode
waitAndCleanup

         solver :: Solver
solver = Solver { IO ExitCode
SExpr -> IO SExpr
command :: SExpr -> IO SExpr
stop :: IO ExitCode
forceStop :: IO ExitCode
command :: SExpr -> IO SExpr
forceStop :: IO ExitCode
stop :: IO ExitCode
.. }

     Solver -> String -> String -> IO ()
setOption Solver
solver String
":print-success" String
"true"
     Solver -> String -> String -> IO ()
setOption Solver
solver String
":produce-models" String
"true"

     Solver -> IO Solver
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
solver

-- | Options for configuring how to start, stop, and interact with an SMT
-- solver process.
data Config = Config
  { Config -> String
solverExecutable :: String
    -- ^ The SMT solver executable.
  , Config -> [String]
solverArguments :: [String]
    -- ^ The command-line arguments to pass to the SMT solver.
  , Config -> Maybe (ExitCode -> IO ())
solverOnExit :: Maybe (ExitCode -> IO ())
    -- ^ Do this when the SMT solver exits.
  , Config -> SolverLogger
solverLogger :: SolverLogger
    -- ^ How to log solver-related messages.
  }

-- | Options for logging SMT solver–related messages.
data SolverLogger = SolverLogger
  { SolverLogger -> SExpr -> IO ()
solverLogSend :: SExpr -> IO ()
    -- ^ Log an SMT query ('SExpr') being sent to the SMT solver.
  , SolverLogger -> SExpr -> IO ()
solverLogRecv :: SExpr -> IO ()
    -- ^ Log a response ('SExpr') being received from the SMT solver.
  , SolverLogger -> IOException -> IO ()
solverLogExcn :: X.IOException -> IO ()
    -- ^ Log the SMT solver throwing an 'X.IOException'.
  , SolverLogger -> String -> IO ()
solverLogStdErr :: String -> IO ()
    -- ^ Log the SMT solver displaying an error to @stderr@.
  }

-- | A reasonable default 'Config' value.
defaultConfig ::
  String   {- ^ Solver executable -} ->
  [String] {- ^ Solver arguments -}  ->
  Config
defaultConfig :: String -> [String] -> Config
defaultConfig String
exe [String]
opts = Config
  { solverExecutable :: String
solverExecutable = String
exe
  , solverArguments :: [String]
solverArguments = [String]
opts
  , solverOnExit :: Maybe (ExitCode -> IO ())
solverOnExit = Maybe (ExitCode -> IO ())
forall a. Maybe a
Nothing
  , solverLogger :: SolverLogger
solverLogger = SolverLogger
noSolverLogger
  }

-- | A trivial 'SolverLogger' that does not perform any logging.
noSolverLogger :: SolverLogger
noSolverLogger :: SolverLogger
noSolverLogger = SolverLogger
  { solverLogSend :: SExpr -> IO ()
solverLogSend = \SExpr
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , solverLogRecv :: SExpr -> IO ()
solverLogRecv = \SExpr
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , solverLogExcn :: IOException -> IO ()
solverLogExcn = \IOException
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , solverLogStdErr :: String -> IO ()
solverLogStdErr = \String
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  }

-- | A basic 'SolverLogger' that prints out heralds in front of sent and
-- received SMT queries, as well as messages to @stderr@. This is the approach
-- that 'newSolver' and 'newSolverNotify' use for logging.
heraldSolverLogger :: Logger -> SolverLogger
heraldSolverLogger :: Logger -> SolverLogger
heraldSolverLogger Logger
l = SolverLogger
  { solverLogSend :: SExpr -> IO ()
solverLogSend = \SExpr
c -> Logger -> String -> IO ()
logMessage Logger
l (String
"[send->] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> ShowS
showsSExpr SExpr
c String
"")
  , solverLogRecv :: SExpr -> IO ()
solverLogRecv = \SExpr
c -> Logger -> String -> IO ()
logMessage Logger
l (String
"[<-recv] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> ShowS
showsSExpr SExpr
c String
"")
  , solverLogExcn :: IOException -> IO ()
solverLogExcn = \IOException
exc -> Logger -> String -> IO ()
logMessage Logger
l (IOException -> String
forall a. Show a => a -> String
show IOException
exc)
  , solverLogStdErr :: String -> IO ()
solverLogStdErr = \String
errs -> Logger -> String -> IO ()
logMessage Logger
l (String
"[stderr] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
errs)
  }

-- | A 'SolverLogger' that formats log messages into the SMT-LIB file format so
-- that the resulting log can be parsed as input by an SMT solver.
smtSolverLogger :: Logger -> SolverLogger
smtSolverLogger :: Logger -> SolverLogger
smtSolverLogger Logger
l = SolverLogger
  { solverLogSend :: SExpr -> IO ()
solverLogSend = \SExpr
c -> Logger -> String -> IO ()
logMessage Logger
l (SExpr -> ShowS
showsSExpr SExpr
c String
"")
  , solverLogRecv :: SExpr -> IO ()
solverLogRecv = \SExpr
c -> Logger -> String -> IO ()
logMessage Logger
l (String
"; " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> ShowS
showsSExpr SExpr
c String
"")
  , solverLogExcn :: IOException -> IO ()
solverLogExcn = \IOException
exc -> Logger -> String -> IO ()
logMessage Logger
l (IOException -> String
forall a. Show a => a -> String
show IOException
exc)
  , solverLogStdErr :: String -> IO ()
solverLogStdErr = \String
errs -> Logger -> String -> IO ()
logMessage Logger
l String
errs
  }

-- | Load the contents of a file.
loadFile :: Solver -> FilePath -> IO ()
loadFile :: Solver -> String -> IO ()
loadFile Solver
s String
file = Solver -> String -> IO ()
loadString Solver
s (String -> IO ()) -> IO String -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> IO String
readFile String
file

-- | Load a raw SMT string.
loadString :: Solver -> String -> IO ()
loadString :: Solver -> String -> IO ()
loadString Solver
s String
str = String -> IO ()
go (ShowS
dropComments String
str)
  where
  go :: String -> IO ()
go String
txt
    | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
txt = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
otherwise =
      case String -> Maybe (SExpr, String)
readSExpr String
txt of
        Just (SExpr
e,String
rest) -> Solver -> SExpr -> IO SExpr
command Solver
s SExpr
e IO SExpr -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
go String
rest
        Maybe (SExpr, String)
Nothing       -> String -> IO ()
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Failed to parse SMT file."
                                        , String
txt
                                        ]

  dropComments :: ShowS
dropComments = [String] -> String
unlines ([String] -> String) -> (String -> [String]) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
dropComment ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines
  dropComment :: ShowS
dropComment String
xs = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
';') String
xs of
                     (String
as,Char
_:String
_) -> String
as
                     (String, String)
_ -> String
xs




-- | A command with no interesting result.
ackCommand :: Solver -> SExpr -> IO ()
ackCommand :: Solver -> SExpr -> IO ()
ackCommand Solver
proc SExpr
c =
  do SExpr
res <- Solver -> SExpr -> IO SExpr
command Solver
proc SExpr
c
     case SExpr
res of
       Atom String
"success" -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       SExpr
_  -> String -> IO ()
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                      [ String
"Unexpected result from the SMT solver:"
                      , String
"  Expected: success"
                      , String
"  Result: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> ShowS
showsSExpr SExpr
res String
""
                      ]

-- | A command entirely made out of atoms, with no interesting result.
simpleCommand :: Solver -> [String] -> IO ()
simpleCommand :: Solver -> [String] -> IO ()
simpleCommand Solver
proc = Solver -> SExpr -> IO ()
ackCommand Solver
proc (SExpr -> IO ()) -> ([String] -> SExpr) -> [String] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SExpr] -> SExpr
List ([SExpr] -> SExpr) -> ([String] -> [SExpr]) -> [String] -> SExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> SExpr) -> [String] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map String -> SExpr
Atom

-- | Run a command and return True if successful, and False if unsupported.
-- This is useful for setting options that unsupported by some solvers, but used
-- by others.
simpleCommandMaybe :: Solver -> [String] -> IO Bool
simpleCommandMaybe :: Solver -> [String] -> IO Bool
simpleCommandMaybe Solver
proc [String]
c =
  do SExpr
res <- Solver -> SExpr -> IO SExpr
command Solver
proc ([SExpr] -> SExpr
List ((String -> SExpr) -> [String] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map String -> SExpr
Atom [String]
c))
     case SExpr
res of
       Atom String
"success"     -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       Atom String
"unsupported" -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
       SExpr
_                  -> String -> IO Bool
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO Bool) -> String -> IO Bool
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                                      [ String
"Unexpected result from the SMT solver:"
                                      , String
"  Expected: success or unsupported"
                                      , String
"  Result: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> ShowS
showsSExpr SExpr
res String
""
                                      ]


-- | Set a solver option.
setOption :: Solver -> String -> String -> IO ()
setOption :: Solver -> String -> String -> IO ()
setOption Solver
s String
x String
y = Solver -> [String] -> IO ()
simpleCommand Solver
s [ String
"set-option", String
x, String
y ]

-- | Set a solver option, returning False if the option is unsupported.
setOptionMaybe :: Solver -> String -> String -> IO Bool
setOptionMaybe :: Solver -> String -> String -> IO Bool
setOptionMaybe Solver
s String
x String
y = Solver -> [String] -> IO Bool
simpleCommandMaybe Solver
s [ String
"set-option", String
x, String
y ]

-- | Set the solver's logic.  Usually, this should be done first.
setLogic :: Solver -> String -> IO ()
setLogic :: Solver -> String -> IO ()
setLogic Solver
s String
x = Solver -> [String] -> IO ()
simpleCommand Solver
s [ String
"set-logic", String
x ]


-- | Set the solver's logic, returning False if the logic is unsupported.
setLogicMaybe :: Solver -> String -> IO Bool
setLogicMaybe :: Solver -> String -> IO Bool
setLogicMaybe Solver
s String
x = Solver -> [String] -> IO Bool
simpleCommandMaybe Solver
s [ String
"set-logic", String
x ]

-- | Request unsat cores.  Returns if the solver supports them.
produceUnsatCores :: Solver -> IO Bool
produceUnsatCores :: Solver -> IO Bool
produceUnsatCores Solver
s = Solver -> String -> String -> IO Bool
setOptionMaybe Solver
s String
":produce-unsat-cores" String
"true"

-- | Checkpoint state.  A special case of 'pushMany'.
push :: Solver -> IO ()
push :: Solver -> IO ()
push Solver
proc = Solver -> Integer -> IO ()
pushMany Solver
proc Integer
1

-- | Restore to last check-point.  A special case of 'popMany'.
pop :: Solver -> IO ()
pop :: Solver -> IO ()
pop Solver
proc = Solver -> Integer -> IO ()
popMany Solver
proc Integer
1

-- | Push multiple scopes.
pushMany :: Solver -> Integer -> IO ()
pushMany :: Solver -> Integer -> IO ()
pushMany Solver
proc Integer
n = Solver -> [String] -> IO ()
simpleCommand Solver
proc [ String
"push", Integer -> String
forall a. Show a => a -> String
show Integer
n ]

-- | Pop multiple scopes.
popMany :: Solver -> Integer -> IO ()
popMany :: Solver -> Integer -> IO ()
popMany Solver
proc Integer
n = Solver -> [String] -> IO ()
simpleCommand Solver
proc [ String
"pop", Integer -> String
forall a. Show a => a -> String
show Integer
n ]

-- | Execute the IO action in a new solver scope (push before, pop after)
inNewScope :: Solver -> IO a -> IO a
inNewScope :: forall a. Solver -> IO a -> IO a
inNewScope Solver
s IO a
m =
  do Solver -> IO ()
push Solver
s
     IO a
m IO a -> IO () -> IO a
forall a b. IO a -> IO b -> IO a
`X.finally` Solver -> IO ()
pop Solver
s



-- | Declare a constant.  A common abbreviation for 'declareFun'.
-- For convenience, returns an the declared name as a constant expression.
declare :: Solver -> String -> SExpr -> IO SExpr
declare :: Solver -> String -> SExpr -> IO SExpr
declare Solver
proc String
f SExpr
t = Solver -> String -> [SExpr] -> SExpr -> IO SExpr
declareFun Solver
proc String
f [] SExpr
t

-- | Declare a function or a constant.
-- For convenience, returns an the declared name as a constant expression.
declareFun :: Solver -> String -> [SExpr] -> SExpr -> IO SExpr
declareFun :: Solver -> String -> [SExpr] -> SExpr -> IO SExpr
declareFun Solver
proc String
f [SExpr]
as SExpr
r =
  do Solver -> SExpr -> IO ()
ackCommand Solver
proc (SExpr -> IO ()) -> SExpr -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> [SExpr] -> SExpr
fun String
"declare-fun" [ String -> SExpr
Atom String
f, [SExpr] -> SExpr
List [SExpr]
as, SExpr
r ]
     SExpr -> IO SExpr
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> SExpr
const String
f)

-- | Declare an ADT using the format introduced in SmtLib 2.6.
declareDatatype ::
  Solver ->
  String {- ^ datatype name -} ->
  [String] {- ^ sort parameters -} ->
  [(String, [(String, SExpr)])] {- ^ constructors -} ->
  IO ()
declareDatatype :: Solver
-> String -> [String] -> [(String, [(String, SExpr)])] -> IO ()
declareDatatype Solver
proc String
t [] [(String, [(String, SExpr)])]
cs =
  Solver -> SExpr -> IO ()
ackCommand Solver
proc (SExpr -> IO ()) -> SExpr -> IO ()
forall a b. (a -> b) -> a -> b
$
    String -> [SExpr] -> SExpr
fun String
"declare-datatype" ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$
      [ String -> SExpr
Atom String
t
      , [SExpr] -> SExpr
List [ [SExpr] -> SExpr
List (String -> SExpr
Atom String
c SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [ [SExpr] -> SExpr
List [String -> SExpr
Atom String
s, SExpr
argTy] | (String
s, SExpr
argTy) <- [(String, SExpr)]
args]) | (String
c, [(String, SExpr)]
args) <- [(String, [(String, SExpr)])]
cs ]
      ]
declareDatatype Solver
proc String
t [String]
ps [(String, [(String, SExpr)])]
cs =
  Solver -> SExpr -> IO ()
ackCommand Solver
proc (SExpr -> IO ()) -> SExpr -> IO ()
forall a b. (a -> b) -> a -> b
$
    String -> [SExpr] -> SExpr
fun String
"declare-datatype" ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$
      [ String -> SExpr
Atom String
t
      , String -> [SExpr] -> SExpr
fun String
"par" ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$
          [ [SExpr] -> SExpr
List ((String -> SExpr) -> [String] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map String -> SExpr
Atom [String]
ps)
          , [SExpr] -> SExpr
List [ [SExpr] -> SExpr
List (String -> SExpr
Atom String
c SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [ [SExpr] -> SExpr
List [String -> SExpr
Atom String
s, SExpr
argTy] | (String
s, SExpr
argTy) <- [(String, SExpr)]
args]) | (String
c, [(String, SExpr)]
args) <- [(String, [(String, SExpr)])]
cs ]
          ]
      ]


-- | Declare a constant.  A common abbreviation for 'declareFun'.
-- For convenience, returns the defined name as a constant expression.
define :: Solver ->
          String {- ^ New symbol -} ->
          SExpr  {- ^ Symbol type -} ->
          SExpr  {- ^ Symbol definition -} ->
          IO SExpr
define :: Solver -> String -> SExpr -> SExpr -> IO SExpr
define Solver
proc String
f SExpr
t SExpr
e = Solver -> String -> [(String, SExpr)] -> SExpr -> SExpr -> IO SExpr
defineFun Solver
proc String
f [] SExpr
t SExpr
e

-- | Define a function or a constant.
-- For convenience, returns an the defined name as a constant expression.
defineFun :: Solver ->
             String           {- ^ New symbol -} ->
             [(String,SExpr)] {- ^ Parameters, with types -} ->
             SExpr            {- ^ Type of result -} ->
             SExpr            {- ^ Definition -} ->
             IO SExpr
defineFun :: Solver -> String -> [(String, SExpr)] -> SExpr -> SExpr -> IO SExpr
defineFun Solver
proc String
f [(String, SExpr)]
as SExpr
t SExpr
e =
  do Solver -> SExpr -> IO ()
ackCommand Solver
proc (SExpr -> IO ()) -> SExpr -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> [SExpr] -> SExpr
fun String
"define-fun"
                     ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ [ String -> SExpr
Atom String
f, [SExpr] -> SExpr
List [ [SExpr] -> SExpr
List [String -> SExpr
const String
x,SExpr
a] | (String
x,SExpr
a) <- [(String, SExpr)]
as ], SExpr
t, SExpr
e]
     SExpr -> IO SExpr
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> SExpr
const String
f)

-- | Define a recursive function or a constant.  For convenience,
-- returns an the defined name as a constant expression.  This body
-- takes the function name as an argument.
defineFunRec :: Solver ->
                String           {- ^ New symbol -} ->
                [(String,SExpr)] {- ^ Parameters, with types -} ->
                SExpr            {- ^ Type of result -} ->
                (SExpr -> SExpr) {- ^ Definition -} ->
                IO SExpr
defineFunRec :: Solver
-> String
-> [(String, SExpr)]
-> SExpr
-> (SExpr -> SExpr)
-> IO SExpr
defineFunRec Solver
proc String
f [(String, SExpr)]
as SExpr
t SExpr -> SExpr
e =
  do let fs :: SExpr
fs = String -> SExpr
const String
f
     Solver -> SExpr -> IO ()
ackCommand Solver
proc (SExpr -> IO ()) -> SExpr -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> [SExpr] -> SExpr
fun String
"define-fun-rec"
                     ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ [ String -> SExpr
Atom String
f, [SExpr] -> SExpr
List [ [SExpr] -> SExpr
List [String -> SExpr
const String
x,SExpr
a] | (String
x,SExpr
a) <- [(String, SExpr)]
as ], SExpr
t, SExpr -> SExpr
e SExpr
fs]
     SExpr -> IO SExpr
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SExpr
fs

-- | Define a recursive function or a constant.  For convenience,
-- returns an the defined name as a constant expression.  This body
-- takes the function name as an argument.
defineFunsRec :: Solver ->
                 [(String, [(String,SExpr)], SExpr, SExpr)] ->
                 IO ()
defineFunsRec :: Solver -> [(String, [(String, SExpr)], SExpr, SExpr)] -> IO ()
defineFunsRec Solver
proc [(String, [(String, SExpr)], SExpr, SExpr)]
ds = Solver -> SExpr -> IO ()
ackCommand Solver
proc (SExpr -> IO ()) -> SExpr -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> [SExpr] -> SExpr
fun String
"define-funs-rec" [ SExpr
decls, SExpr
bodies ]
  where
    oneArg :: (String, [(String, SExpr)], SExpr, d) -> SExpr
oneArg (String
f, [(String, SExpr)]
args, SExpr
t, d
_) = [SExpr] -> SExpr
List [ String -> SExpr
Atom String
f, [SExpr] -> SExpr
List [ [SExpr] -> SExpr
List [String -> SExpr
const String
x,SExpr
a] | (String
x,SExpr
a) <- [(String, SExpr)]
args ], SExpr
t]
    decls :: SExpr
decls  = [SExpr] -> SExpr
List (((String, [(String, SExpr)], SExpr, SExpr) -> SExpr)
-> [(String, [(String, SExpr)], SExpr, SExpr)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (String, [(String, SExpr)], SExpr, SExpr) -> SExpr
forall {d}. (String, [(String, SExpr)], SExpr, d) -> SExpr
oneArg [(String, [(String, SExpr)], SExpr, SExpr)]
ds)
    bodies :: SExpr
bodies = [SExpr] -> SExpr
List (((String, [(String, SExpr)], SExpr, SExpr) -> SExpr)
-> [(String, [(String, SExpr)], SExpr, SExpr)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
_, [(String, SExpr)]
_, SExpr
_, SExpr
body) -> SExpr
body) [(String, [(String, SExpr)], SExpr, SExpr)]
ds)


-- | Assume a fact.
assert :: Solver -> SExpr -> IO ()
assert :: Solver -> SExpr -> IO ()
assert Solver
proc SExpr
e = Solver -> SExpr -> IO ()
ackCommand Solver
proc (SExpr -> IO ()) -> SExpr -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> [SExpr] -> SExpr
fun String
"assert" [SExpr
e]

-- | Check if the current set of assertion is consistent.
check :: Solver -> IO Result
check :: Solver -> IO Result
check Solver
proc =
  do SExpr
res <- Solver -> SExpr -> IO SExpr
command Solver
proc ([SExpr] -> SExpr
List [ String -> SExpr
Atom String
"check-sat" ])
     case SExpr
res of
       Atom String
"unsat"   -> Result -> IO Result
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
Unsat
       Atom String
"unknown" -> Result -> IO Result
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
Unknown
       Atom String
"sat"     -> Result -> IO Result
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
Sat
       SExpr
_ -> String -> IO Result
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO Result) -> String -> IO Result
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
              [ String
"Unexpected result from the SMT solver:"
              , String
"  Expected: unsat, unknown, or sat"
              , String
"  Result: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> ShowS
showsSExpr SExpr
res String
""
              ]

-- | Convert an s-expression to a value.
sexprToVal :: SExpr -> Value
sexprToVal :: SExpr -> Value
sexprToVal SExpr
expr =
  case SExpr
expr of
    Atom String
"true"                    -> Bool -> Value
Bool Bool
True
    Atom String
"false"                   -> Bool -> Value
Bool Bool
False
    Atom (Char
'#' : Char
'b' : String
ds)
      | Just Integer
n <- String -> Maybe Integer
binLit String
ds         -> Int -> Integer -> Value
Bits (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
ds) Integer
n
    Atom (Char
'#' : Char
'x' : String
ds)
      | [(Integer
n,[])] <- ReadS Integer
forall a. (Eq a, Num a) => ReadS a
readHex String
ds      -> Int -> Integer -> Value
Bits (Int
4 Int -> Int -> Int
forall a. Num a => a -> a -> a
* String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
ds) Integer
n
    Atom String
txt
      | Just Integer
n <- String -> Maybe Integer
forall a. Read a => String -> Maybe a
readMaybe String
txt     -> Integer -> Value
Int Integer
n
    List [ Atom String
"-", SExpr
x ]
      | Int Integer
a <- SExpr -> Value
sexprToVal SExpr
x    -> Integer -> Value
Int (Integer -> Integer
forall a. Num a => a -> a
negate Integer
a)
    List [ Atom String
"/", SExpr
x, SExpr
y ]
      | Int Integer
a <- SExpr -> Value
sexprToVal SExpr
x
      , Int Integer
b <- SExpr -> Value
sexprToVal SExpr
y    -> Rational -> Value
Real (Integer
a Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
b)
    SExpr
_ -> SExpr -> Value
Other SExpr
expr

  where
  binLit :: String -> Maybe Integer
binLit String
cs = do [Integer]
ds <- (Char -> Maybe Integer) -> String -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Char -> Maybe Integer
forall {a}. Num a => Char -> Maybe a
binDigit String
cs
                 Integer -> Maybe Integer
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer)
-> [Integer] -> [Integer] -> [Integer]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) ([Integer] -> [Integer]
forall a. [a] -> [a]
reverse [Integer]
ds) [Integer]
powers2
  powers2 :: [Integer]
powers2   = Integer
1 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: (Integer -> Integer) -> [Integer] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*) [Integer]
powers2
  binDigit :: Char -> Maybe a
binDigit Char
'0' = a -> Maybe a
forall a. a -> Maybe a
Just a
0
  binDigit Char
'1' = a -> Maybe a
forall a. a -> Maybe a
Just a
1
  binDigit Char
_   = Maybe a
forall a. Maybe a
Nothing

-- | Get the values of some s-expressions.
-- Only valid after a 'Sat' result.
getExprs :: Solver -> [SExpr] -> IO [(SExpr, Value)]
getExprs :: Solver -> [SExpr] -> IO [(SExpr, Value)]
getExprs Solver
proc [SExpr]
vals =
  do SExpr
res <- Solver -> SExpr -> IO SExpr
command Solver
proc (SExpr -> IO SExpr) -> SExpr -> IO SExpr
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
List [ String -> SExpr
Atom String
"get-value", [SExpr] -> SExpr
List [SExpr]
vals ]
     case SExpr
res of
       List [SExpr]
xs -> (SExpr -> IO (SExpr, Value)) -> [SExpr] -> IO [(SExpr, Value)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SExpr -> IO (SExpr, Value)
forall {m :: * -> *}. MonadFail m => SExpr -> m (SExpr, Value)
getAns [SExpr]
xs
       SExpr
_ -> String -> IO [(SExpr, Value)]
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO [(SExpr, Value)]) -> String -> IO [(SExpr, Value)]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                 [ String
"Unexpected response from the SMT solver:"
                 , String
"  Exptected: a list"
                 , String
"  Result: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> ShowS
showsSExpr SExpr
res String
""
                 ]
  where
  getAns :: SExpr -> m (SExpr, Value)
getAns SExpr
expr =
    case SExpr
expr of
      List [ SExpr
e, SExpr
v ] -> (SExpr, Value) -> m (SExpr, Value)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr
e, SExpr -> Value
sexprToVal SExpr
v)
      SExpr
_             -> String -> m (SExpr, Value)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m (SExpr, Value)) -> String -> m (SExpr, Value)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                            [ String
"Unexpected response from the SMT solver:"
                            , String
"  Expected: (expr val)"
                            , String
"  Result: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> ShowS
showsSExpr SExpr
expr String
""
                            ]

-- | Get the values of some constants in the current model.
-- A special case of 'getExprs'.
-- Only valid after a 'Sat' result.
getConsts :: Solver -> [String] -> IO [(String, Value)]
getConsts :: Solver -> [String] -> IO [(String, Value)]
getConsts Solver
proc [String]
xs =
  do [(SExpr, Value)]
ans <- Solver -> [SExpr] -> IO [(SExpr, Value)]
getExprs Solver
proc ((String -> SExpr) -> [String] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map String -> SExpr
Atom [String]
xs)
     [(String, Value)] -> IO [(String, Value)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (String
x,Value
e) | (Atom String
x, Value
e) <- [(SExpr, Value)]
ans ]


-- | Get the value of a single expression.
getExpr :: Solver -> SExpr -> IO Value
getExpr :: Solver -> SExpr -> IO Value
getExpr Solver
proc SExpr
x =
  do [ (SExpr
_,Value
v) ] <- Solver -> [SExpr] -> IO [(SExpr, Value)]
getExprs Solver
proc [SExpr
x]
     Value -> IO Value
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v

-- | Get the value of a single constant.
getConst :: Solver -> String -> IO Value
getConst :: Solver -> String -> IO Value
getConst Solver
proc String
x = Solver -> SExpr -> IO Value
getExpr Solver
proc (String -> SExpr
Atom String
x)

-- | Returns the names of the (named) formulas involved in a contradiction.
getUnsatCore :: Solver -> IO [String]
getUnsatCore :: Solver -> IO [String]
getUnsatCore Solver
s =
  do SExpr
res <- Solver -> SExpr -> IO SExpr
command Solver
s (SExpr -> IO SExpr) -> SExpr -> IO SExpr
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
List [ String -> SExpr
Atom String
"get-unsat-core" ]
     case SExpr
res of
       List [SExpr]
xs -> (SExpr -> IO String) -> [SExpr] -> IO [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SExpr -> IO String
forall {m :: * -> *}. MonadFail m => SExpr -> m String
fromAtom [SExpr]
xs
       SExpr
_       -> String -> SExpr -> IO [String]
forall {m :: * -> *} {a}. MonadFail m => String -> SExpr -> m a
unexpected String
"a list of atoms" SExpr
res
  where
  fromAtom :: SExpr -> m String
fromAtom SExpr
x =
    case SExpr
x of
      Atom String
a -> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
a
      SExpr
_      -> String -> SExpr -> m String
forall {m :: * -> *} {a}. MonadFail m => String -> SExpr -> m a
unexpected String
"an atom" SExpr
x

  unexpected :: String -> SExpr -> m a
unexpected String
x SExpr
e =
    String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Unexpected response from the SMT Solver:"
                   , String
"  Expected: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x
                   , String
"  Result: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> ShowS
showsSExpr SExpr
e String
""
                   ]

--------------------------------------------------------------------------------


-- | A constant, corresponding to a family indexed by some integers.
fam :: String -> [Integer] -> SExpr
fam :: String -> [Integer] -> SExpr
fam String
f [Integer]
is = [SExpr] -> SExpr
List (String -> SExpr
Atom String
"_" SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: String -> SExpr
Atom String
f SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: (Integer -> SExpr) -> [Integer] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (String -> SExpr
Atom (String -> SExpr) -> (Integer -> String) -> Integer -> SExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show) [Integer]
is)

-- | An SMT function.
fun :: String -> [SExpr] -> SExpr
fun :: String -> [SExpr] -> SExpr
fun String
f [] = String -> SExpr
Atom String
f
fun String
f [SExpr]
as = [SExpr] -> SExpr
List (String -> SExpr
Atom String
f SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [SExpr]
as)

-- | An SMT constant.  A special case of 'fun'.
const :: String -> SExpr
const :: String -> SExpr
const String
f = String -> [SExpr] -> SExpr
fun String
f []

app :: SExpr -> [SExpr] -> SExpr
app :: SExpr -> [SExpr] -> SExpr
app SExpr
f [SExpr]
xs = [SExpr] -> SExpr
List (SExpr
f SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [SExpr]
xs)

-- Identifiers -----------------------------------------------------------------------

-- | Symbols are either simple or quoted (c.f. SMTLIB v2.6 S3.1).
-- This predicate indicates whether a character is allowed in a simple
-- symbol.  Note that only ASCII letters are allowed.
allowedSimpleChar :: Char -> Bool
allowedSimpleChar :: Char -> Bool
allowedSimpleChar Char
c =
  Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char
'a' .. Char
'z'] String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char
'A' .. Char
'Z'] String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"~!@$%^&*_-+=<>.?/")

isSimpleSymbol :: String -> Bool
isSimpleSymbol :: String -> Bool
isSimpleSymbol s :: String
s@(Char
c : String
_) = Bool -> Bool
P.not (Char -> Bool
isDigit Char
c) Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
allowedSimpleChar String
s
isSimpleSymbol String
_         = Bool
False

quoteSymbol :: String -> String
quoteSymbol :: ShowS
quoteSymbol String
s
  | String -> Bool
isSimpleSymbol String
s = String
s
  | Bool
otherwise        = Char
'|' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"

symbol :: String -> SExpr
symbol :: String -> SExpr
symbol = String -> SExpr
Atom (String -> SExpr) -> ShowS -> String -> SExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
quoteSymbol

keyword :: String -> SExpr
keyword :: String -> SExpr
keyword String
s = String -> SExpr
Atom (Char
':' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s)

-- | Generate a type annotation for a symbol
as :: SExpr -> SExpr -> SExpr
as :: SExpr -> SExpr -> SExpr
as SExpr
s SExpr
t = String -> [SExpr] -> SExpr
fun String
"as" [SExpr
s, SExpr
t]

-- Types -----------------------------------------------------------------------


-- | The type of integers.
tInt :: SExpr
tInt :: SExpr
tInt = String -> SExpr
const String
"Int"

-- | The type of booleans.
tBool :: SExpr
tBool :: SExpr
tBool = String -> SExpr
const String
"Bool"

-- | The type of reals.
tReal :: SExpr
tReal :: SExpr
tReal = String -> SExpr
const String
"Real"

-- | The type of arrays.
tArray :: SExpr {- ^ Type of indexes  -} ->
          SExpr {- ^ Type of elements -} ->
          SExpr
tArray :: SExpr -> SExpr -> SExpr
tArray SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"Array" [SExpr
x,SExpr
y]

-- | The type of bit vectors.
tBits :: Integer {- ^ Number of bits -} ->
         SExpr
tBits :: Integer -> SExpr
tBits Integer
w = String -> [Integer] -> SExpr
fam String
"BitVec" [Integer
w]



-- Literals --------------------------------------------------------------------

-- | Boolean literals.
bool :: Bool -> SExpr
bool :: Bool -> SExpr
bool Bool
b = String -> SExpr
const (if Bool
b then String
"true" else String
"false")

-- | Integer literals.
int :: Integer -> SExpr
int :: Integer -> SExpr
int Integer
x | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = SExpr -> SExpr
neg (Integer -> SExpr
int (Integer -> Integer
forall a. Num a => a -> a
negate Integer
x))
      | Bool
otherwise = String -> SExpr
Atom (Integer -> String
forall a. Show a => a -> String
show Integer
x)

-- | Real (well, rational) literals.
real :: Rational -> SExpr
real :: Rational -> SExpr
real Rational
x
  | Double -> Rational
forall a. Real a => a -> Rational
toRational Double
y Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
x = String -> SExpr
Atom (Maybe Int -> Double -> ShowS
forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat Maybe Int
forall a. Maybe a
Nothing Double
y String
"")
  | Bool
otherwise = SExpr -> SExpr -> SExpr
realDiv (Integer -> SExpr
int (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x)) (Integer -> SExpr
int (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x))
  where y :: Double
y = Rational -> Double
forall a. Fractional a => Rational -> a
fromRational Rational
x :: Double

-- | A bit vector represented in binary.
--
--     * If the value does not fit in the bits, then the bits will be increased.
--     * The width should be strictly positive.
bvBin :: Int {- ^ Width, in bits -} -> Integer {- ^ Value -} -> SExpr
bvBin :: Int -> Integer -> SExpr
bvBin Int
w Integer
v = String -> SExpr
const (String
"#b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
bits)
  where
  bits :: String
bits = ShowS
forall a. [a] -> [a]
reverse [ if Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
v Int
n then Char
'1' else Char
'0' | Int
n <- [ Int
0 .. Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 ] ]

-- | A bit vector represented in hex.
--
--    * If the value does not fit in the bits, the bits will be increased to
--      the next multiple of 4 that will fit the value.
--    * If the width is not a multiple of 4, it will be rounded
--      up so that it is.
--    * The width should be strictly positive.
bvHex :: Int {- ^ Width, in bits -} -> Integer {- ^ Value -} -> SExpr
bvHex :: Int -> Integer -> SExpr
bvHex Int
w Integer
v
  | Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    = String -> SExpr
const (String
"#x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
padding String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hex)
  | Bool
otherwise = Int -> Integer -> SExpr
bvHex Int
w (Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
v)
  where
  hex :: String
hex     = Integer -> ShowS
forall a. Integral a => a -> ShowS
showHex Integer
v String
""
  padding :: String
padding = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int -> Int -> Int
forall a. Integral a => a -> a -> a
P.div (Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
3) Int
4 Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hex) Char
'0'


-- | Render a value as an expression.  Bit-vectors are rendered in hex,
-- if their width is a multiple of 4, and in binary otherwise.
value :: Value -> SExpr
value :: Value -> SExpr
value Value
val =
  case Value
val of
    Bool Bool
b    -> Bool -> SExpr
bool Bool
b
    Int Integer
n     -> Integer -> SExpr
int Integer
n
    Real Rational
r    -> Rational -> SExpr
real Rational
r
    Bits Int
w Integer
v | Int -> Int -> Int
forall a. Integral a => a -> a -> a
P.mod Int
w Int
4 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 -> Int -> Integer -> SExpr
bvHex Int
w Integer
v
             | Bool
otherwise      -> Int -> Integer -> SExpr
bvBin Int
w Integer
v
    Other SExpr
o   -> SExpr
o

-- Connectives -----------------------------------------------------------------

-- | Logical negation.
not :: SExpr -> SExpr
not :: SExpr -> SExpr
not SExpr
p = String -> [SExpr] -> SExpr
fun String
"not" [SExpr
p]

-- | Conjunction.
and :: SExpr -> SExpr -> SExpr
and :: SExpr -> SExpr -> SExpr
and SExpr
p SExpr
q = String -> [SExpr] -> SExpr
fun String
"and" [SExpr
p,SExpr
q]

andMany :: [SExpr] -> SExpr
andMany :: [SExpr] -> SExpr
andMany [SExpr]
xs = if [SExpr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SExpr]
xs then Bool -> SExpr
bool Bool
True else String -> [SExpr] -> SExpr
fun String
"and" [SExpr]
xs

-- | Disjunction.
or :: SExpr -> SExpr -> SExpr
or :: SExpr -> SExpr -> SExpr
or SExpr
p SExpr
q = String -> [SExpr] -> SExpr
fun String
"or" [SExpr
p,SExpr
q]

orMany :: [SExpr] -> SExpr
orMany :: [SExpr] -> SExpr
orMany [SExpr]
xs = if [SExpr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SExpr]
xs then Bool -> SExpr
bool Bool
False else String -> [SExpr] -> SExpr
fun String
"or" [SExpr]
xs

-- | Exclusive-or.
xor :: SExpr -> SExpr -> SExpr
xor :: SExpr -> SExpr -> SExpr
xor SExpr
p SExpr
q = String -> [SExpr] -> SExpr
fun String
"xor" [SExpr
p,SExpr
q]

-- | Implication.
implies :: SExpr -> SExpr -> SExpr
implies :: SExpr -> SExpr -> SExpr
implies SExpr
p SExpr
q = String -> [SExpr] -> SExpr
fun String
"=>" [SExpr
p,SExpr
q]


-- If-then-else ----------------------------------------------------------------

-- | If-then-else.  This is polymorphic and can be used to construct any term.
ite :: SExpr -> SExpr -> SExpr -> SExpr
ite :: SExpr -> SExpr -> SExpr -> SExpr
ite SExpr
x SExpr
y SExpr
z = String -> [SExpr] -> SExpr
fun String
"ite" [SExpr
x,SExpr
y,SExpr
z]




-- Relations -------------------------------------------------------------------

-- | Equality.
eq :: SExpr -> SExpr -> SExpr
eq :: SExpr -> SExpr -> SExpr
eq SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"=" [SExpr
x,SExpr
y]

distinct :: [SExpr] -> SExpr
distinct :: [SExpr] -> SExpr
distinct [SExpr]
xs = if [SExpr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SExpr]
xs then Bool -> SExpr
bool Bool
True else String -> [SExpr] -> SExpr
fun String
"distinct" [SExpr]
xs

-- | Greater-then
gt :: SExpr -> SExpr -> SExpr
gt :: SExpr -> SExpr -> SExpr
gt SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
">" [SExpr
x,SExpr
y]

-- | Less-then.
lt :: SExpr -> SExpr -> SExpr
lt :: SExpr -> SExpr -> SExpr
lt SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"<" [SExpr
x,SExpr
y]

-- | Greater-than-or-equal-to.
geq :: SExpr -> SExpr -> SExpr
geq :: SExpr -> SExpr -> SExpr
geq SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
">=" [SExpr
x,SExpr
y]

-- | Less-than-or-equal-to.
leq :: SExpr -> SExpr -> SExpr
leq :: SExpr -> SExpr -> SExpr
leq SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"<=" [SExpr
x,SExpr
y]

-- | Unsigned less-than on bit-vectors.
bvULt :: SExpr -> SExpr -> SExpr
bvULt :: SExpr -> SExpr -> SExpr
bvULt SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvult" [SExpr
x,SExpr
y]

-- | Unsigned less-than-or-equal on bit-vectors.
bvULeq :: SExpr -> SExpr -> SExpr
bvULeq :: SExpr -> SExpr -> SExpr
bvULeq SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvule" [SExpr
x,SExpr
y]

-- | Signed less-than on bit-vectors.
bvSLt :: SExpr -> SExpr -> SExpr
bvSLt :: SExpr -> SExpr -> SExpr
bvSLt SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvslt" [SExpr
x,SExpr
y]

-- | Signed less-than-or-equal on bit-vectors.
bvSLeq :: SExpr -> SExpr -> SExpr
bvSLeq :: SExpr -> SExpr -> SExpr
bvSLeq SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvsle" [SExpr
x,SExpr
y]




-- | Addition.
-- See also 'bvAdd'
add :: SExpr -> SExpr -> SExpr
add :: SExpr -> SExpr -> SExpr
add SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"+" [SExpr
x,SExpr
y]

addMany :: [SExpr] -> SExpr
addMany :: [SExpr] -> SExpr
addMany [SExpr]
xs = if [SExpr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SExpr]
xs then Integer -> SExpr
int Integer
0 else String -> [SExpr] -> SExpr
fun String
"+" [SExpr]
xs

-- | Subtraction.
sub :: SExpr -> SExpr -> SExpr
sub :: SExpr -> SExpr -> SExpr
sub SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"-" [SExpr
x,SExpr
y]

-- | Arithmetic negation for integers and reals.
-- See also 'bvNeg'.
neg :: SExpr -> SExpr
neg :: SExpr -> SExpr
neg SExpr
x = String -> [SExpr] -> SExpr
fun String
"-" [SExpr
x]

-- | Multiplication.
mul :: SExpr -> SExpr -> SExpr
mul :: SExpr -> SExpr -> SExpr
mul SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"*" [SExpr
x,SExpr
y]

-- | Absolute value.
abs :: SExpr -> SExpr
abs :: SExpr -> SExpr
abs SExpr
x = String -> [SExpr] -> SExpr
fun String
"abs" [SExpr
x]

-- | Integer division.
div :: SExpr -> SExpr -> SExpr
div :: SExpr -> SExpr -> SExpr
div SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"div" [SExpr
x,SExpr
y]

-- | Modulus.
mod :: SExpr -> SExpr -> SExpr
mod :: SExpr -> SExpr -> SExpr
mod SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"mod" [SExpr
x,SExpr
y]

-- | Is the number divisible by the given constant.
divisible :: SExpr -> Integer -> SExpr
divisible :: SExpr -> Integer -> SExpr
divisible SExpr
x Integer
n = [SExpr] -> SExpr
List [ String -> [Integer] -> SExpr
fam String
"divisible" [Integer
n], SExpr
x ]

-- | Division of real numbers.
realDiv :: SExpr -> SExpr -> SExpr
realDiv :: SExpr -> SExpr -> SExpr
realDiv SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"/" [SExpr
x,SExpr
y]

-- | Bit vector concatenation.
concat :: SExpr -> SExpr -> SExpr
concat :: SExpr -> SExpr -> SExpr
concat SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"concat" [SExpr
x,SExpr
y]

-- | Extend to the signed equivalent bitvector by @i@ bits
signExtend :: Integer -> SExpr -> SExpr
signExtend :: Integer -> SExpr -> SExpr
signExtend Integer
i SExpr
x = [SExpr] -> SExpr
List [ String -> [Integer] -> SExpr
fam String
"sign_extend" [Integer
i], SExpr
x ]

-- | Extend with zeros to the unsigned equivalent bitvector
-- by @i@ bits
zeroExtend :: Integer -> SExpr -> SExpr
zeroExtend :: Integer -> SExpr -> SExpr
zeroExtend Integer
i SExpr
x = [SExpr] -> SExpr
List [ String -> [Integer] -> SExpr
fam String
"zero_extend" [Integer
i], SExpr
x ]

-- | Satisfies @toInt x <= x@ (i.e., this is like Haskell's 'floor')
toInt :: SExpr -> SExpr
toInt :: SExpr -> SExpr
toInt SExpr
e = String -> [SExpr] -> SExpr
fun String
"to_int" [SExpr
e]

-- | Promote an integer to a real
toReal :: SExpr -> SExpr
toReal :: SExpr -> SExpr
toReal SExpr
e = String -> [SExpr] -> SExpr
fun String
"to_real" [SExpr
e]

-- | Extract a sub-sequence of a bit vector.
extract :: SExpr -> Integer -> Integer -> SExpr
extract :: SExpr -> Integer -> Integer -> SExpr
extract SExpr
x Integer
y Integer
z = [SExpr] -> SExpr
List [ String -> [Integer] -> SExpr
fam String
"extract" [Integer
y,Integer
z], SExpr
x ]

-- | Bitwise negation.
bvNot :: SExpr -> SExpr
bvNot :: SExpr -> SExpr
bvNot SExpr
x = String -> [SExpr] -> SExpr
fun String
"bvnot" [SExpr
x]

-- | Bitwise conjuction.
bvAnd :: SExpr -> SExpr -> SExpr
bvAnd :: SExpr -> SExpr -> SExpr
bvAnd SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvand" [SExpr
x,SExpr
y]

-- | Bitwise disjunction.
bvOr :: SExpr -> SExpr -> SExpr
bvOr :: SExpr -> SExpr -> SExpr
bvOr SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvor" [SExpr
x,SExpr
y]

-- | Bitwise exclusive or.
bvXOr :: SExpr -> SExpr -> SExpr
bvXOr :: SExpr -> SExpr -> SExpr
bvXOr SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvxor" [SExpr
x,SExpr
y]

-- | Bit vector arithmetic negation.
bvNeg :: SExpr -> SExpr
bvNeg :: SExpr -> SExpr
bvNeg SExpr
x = String -> [SExpr] -> SExpr
fun String
"bvneg" [SExpr
x]

-- | Addition of bit vectors.
bvAdd :: SExpr -> SExpr -> SExpr
bvAdd :: SExpr -> SExpr -> SExpr
bvAdd SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvadd" [SExpr
x,SExpr
y]

-- | Subtraction of bit vectors.
bvSub :: SExpr -> SExpr -> SExpr
bvSub :: SExpr -> SExpr -> SExpr
bvSub SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvsub" [SExpr
x,SExpr
y]



-- | Multiplication of bit vectors.
bvMul :: SExpr -> SExpr -> SExpr
bvMul :: SExpr -> SExpr -> SExpr
bvMul SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvmul" [SExpr
x,SExpr
y]

-- | Bit vector unsigned division.
bvUDiv :: SExpr -> SExpr -> SExpr
bvUDiv :: SExpr -> SExpr -> SExpr
bvUDiv SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvudiv" [SExpr
x,SExpr
y]

-- | Bit vector unsigned reminder.
bvURem :: SExpr -> SExpr -> SExpr
bvURem :: SExpr -> SExpr -> SExpr
bvURem SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvurem" [SExpr
x,SExpr
y]

-- | Bit vector signed division.
bvSDiv :: SExpr -> SExpr -> SExpr
bvSDiv :: SExpr -> SExpr -> SExpr
bvSDiv SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvsdiv" [SExpr
x,SExpr
y]

-- | Bit vector signed reminder.
bvSRem :: SExpr -> SExpr -> SExpr
bvSRem :: SExpr -> SExpr -> SExpr
bvSRem SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvsrem" [SExpr
x,SExpr
y]




-- | Shift left.
bvShl :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr
bvShl :: SExpr -> SExpr -> SExpr
bvShl SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvshl" [SExpr
x,SExpr
y]

-- | Logical shift right.
bvLShr :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr
bvLShr :: SExpr -> SExpr -> SExpr
bvLShr SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvlshr" [SExpr
x,SExpr
y]

-- | Arithemti shift right (copies most significant bit).
bvAShr :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr
bvAShr :: SExpr -> SExpr -> SExpr
bvAShr SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"bvashr" [SExpr
x,SExpr
y]


-- | Get an elemeent of an array.
select :: SExpr {- ^ array -} -> SExpr {- ^ index -} -> SExpr
select :: SExpr -> SExpr -> SExpr
select SExpr
x SExpr
y = String -> [SExpr] -> SExpr
fun String
"select" [SExpr
x,SExpr
y]

-- | Update an array
store :: SExpr {- ^ array -}     ->
         SExpr {- ^ index -}     ->
         SExpr {- ^ new value -} ->
         SExpr
store :: SExpr -> SExpr -> SExpr -> SExpr
store SExpr
x SExpr
y SExpr
z = String -> [SExpr] -> SExpr
fun String
"store" [SExpr
x,SExpr
y,SExpr
z]


--------------------------------------------------------------------------------
-- Attributes

named :: String -> SExpr -> SExpr
named :: String -> SExpr -> SExpr
named String
x SExpr
e = String -> [SExpr] -> SExpr
fun String
"!" [SExpr
e, String -> SExpr
Atom String
":named", String -> SExpr
Atom String
x ]


--------------------------------------------------------------------------------

-- | Log messages with minimal formatting. Mostly for debugging.
data Logger = Logger
  { Logger -> String -> IO ()
logMessage :: String -> IO ()
    -- ^ Log a message.

  , Logger -> IO Int
logLevel   :: IO Int

  , Logger -> Int -> IO ()
logSetLevel:: Int -> IO ()

  , Logger -> IO ()
logTab     :: IO ()
    -- ^ Increase indentation.

  , Logger -> IO ()
logUntab   :: IO ()
    -- ^ Decrease indentation.
  }

-- | Run an IO action with the logger set to a specific level, restoring it when
-- done.
withLogLevel :: Logger -> Int -> IO a -> IO a
withLogLevel :: forall a. Logger -> Int -> IO a -> IO a
withLogLevel Logger { IO Int
IO ()
Int -> IO ()
String -> IO ()
logMessage :: Logger -> String -> IO ()
logLevel :: Logger -> IO Int
logSetLevel :: Logger -> Int -> IO ()
logTab :: Logger -> IO ()
logUntab :: Logger -> IO ()
logMessage :: String -> IO ()
logLevel :: IO Int
logSetLevel :: Int -> IO ()
logTab :: IO ()
logUntab :: IO ()
.. } Int
l IO a
m =
  do Int
l0 <- IO Int
logLevel
     IO () -> IO () -> IO a -> IO a
forall a b c. IO a -> IO b -> IO c -> IO c
X.bracket_ (Int -> IO ()
logSetLevel Int
l) (Int -> IO ()
logSetLevel Int
l0) IO a
m

logIndented :: Logger -> IO a -> IO a
logIndented :: forall a. Logger -> IO a -> IO a
logIndented Logger { IO Int
IO ()
Int -> IO ()
String -> IO ()
logMessage :: Logger -> String -> IO ()
logLevel :: Logger -> IO Int
logSetLevel :: Logger -> Int -> IO ()
logTab :: Logger -> IO ()
logUntab :: Logger -> IO ()
logMessage :: String -> IO ()
logLevel :: IO Int
logSetLevel :: Int -> IO ()
logTab :: IO ()
logUntab :: IO ()
.. } = IO () -> IO () -> IO a -> IO a
forall a b c. IO a -> IO b -> IO c -> IO c
X.bracket_ IO ()
logTab IO ()
logUntab

-- | Log a message at a specific log level.
logMessageAt :: Logger -> Int -> String -> IO ()
logMessageAt :: Logger -> Int -> String -> IO ()
logMessageAt Logger
logger Int
l String
msg = Logger -> Int -> IO () -> IO ()
forall a. Logger -> Int -> IO a -> IO a
withLogLevel Logger
logger Int
l (Logger -> String -> IO ()
logMessage Logger
logger String
msg)

-- | A simple stdout logger.  Shows only messages logged at a level that is
-- greater than or equal to the passed level.
newLogger :: Int -> IO Logger
newLogger :: Int -> IO Logger
newLogger = Handle -> Int -> IO Logger
newLoggerWithHandle Handle
stdout

-- | A simple logger that writes to a 'Handle'. Shows only messages logged at a
-- level that is greater than or equal to the passed level.
newLoggerWithHandle :: Handle -> Int -> IO Logger
newLoggerWithHandle :: Handle -> Int -> IO Logger
newLoggerWithHandle Handle
h Int
l =
  do IORef Int
tab <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
     IORef Int
lev <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
     let logLevel :: IO Int
logLevel    = IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
lev
         logSetLevel :: Int -> IO ()
logSetLevel = IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Int
lev

         shouldLog :: IO () -> IO ()
shouldLog IO ()
m =
           do Int
cl <- IO Int
logLevel
              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
cl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
l) IO ()
m

         logMessage :: String -> IO ()
logMessage String
x = IO () -> IO ()
shouldLog (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
           do let ls :: [String]
ls = String -> [String]
lines String
x
              Int
t <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
tab
              Handle -> String -> IO ()
hPutStr Handle
h (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
t Char
' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- [String]
ls ]
              Handle -> IO ()
hFlush Handle
h

         logTab :: IO ()
logTab   = IO () -> IO ()
shouldLog (IORef Int -> (Int -> Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Int
tab (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2))
         logUntab :: IO ()
logUntab = IO () -> IO ()
shouldLog (IORef Int -> (Int -> Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Int
tab (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
2))
     Logger -> IO Logger
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Logger { IO Int
IO ()
Int -> IO ()
String -> IO ()
logMessage :: String -> IO ()
logLevel :: IO Int
logSetLevel :: Int -> IO ()
logTab :: IO ()
logUntab :: IO ()
logLevel :: IO Int
logSetLevel :: Int -> IO ()
logMessage :: String -> IO ()
logTab :: IO ()
logUntab :: IO ()
.. }