{-# 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
  , ackCommand
  , simpleCommand
  , simpleCommandMaybe
  , loadFile
  , loadString

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

    -- ** Logging and Debugging
  , Logger(..)
  , newLogger
  , 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)
import System.IO (hFlush, hGetLine, hGetContents, 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
/= :: Result -> Result -> Bool
$c/= :: Result -> Result -> Bool
== :: Result -> Result -> Bool
$c== :: 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
showList :: [Result] -> ShowS
$cshowList :: [Result] -> ShowS
show :: Result -> String
$cshow :: Result -> String
showsPrec :: Int -> Result -> ShowS
$cshowsPrec :: Int -> 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
/= :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c== :: 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
showList :: [Value] -> ShowS
$cshowList :: [Value] -> ShowS
show :: Value -> String
$cshow :: Value -> String
showsPrec :: Int -> Value -> ShowS
$cshowsPrec :: Int -> 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
/= :: SExpr -> SExpr -> Bool
$c/= :: SExpr -> SExpr -> Bool
== :: SExpr -> SExpr -> Bool
$c== :: 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
min :: SExpr -> SExpr -> SExpr
$cmin :: SExpr -> SExpr -> SExpr
max :: SExpr -> SExpr -> SExpr
$cmax :: SExpr -> SExpr -> SExpr
>= :: SExpr -> SExpr -> Bool
$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
compare :: SExpr -> SExpr -> Ordering
$ccompare :: SExpr -> SExpr -> Ordering
$cp1Ord :: Eq 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
showList :: [SExpr] -> ShowS
$cshowList :: [SExpr] -> ShowS
show :: SExpr -> String
$cshow :: SExpr -> String
showsPrec :: Int -> SExpr -> ShowS
$cshowsPrec :: Int -> SExpr -> ShowS
Show)

-- | Show an s-expression.
showsSExpr :: SExpr -> ShowS
showsSExpr :: SExpr -> ShowS
showsSExpr SExpr
ex =
  case SExpr
ex of
    Atom String
x  -> String -> ShowS
showString String
x
    List [SExpr]
es -> Char -> ShowS
showChar Char
'(' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                (SExpr -> ShowS -> ShowS) -> ShowS -> [SExpr] -> ShowS
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\SExpr
e ShowS
m -> SExpr -> ShowS
showsSExpr SExpr
e ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' 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 readbale fashion.
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 (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 :: 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 (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 (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 (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 (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 (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
    -- ^ Terminate the solver.
  }


-- | 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
n [String]
xs Maybe Logger
l = String
-> [String]
-> Maybe Logger
-> Maybe (ExitCode -> IO ())
-> IO Solver
newSolverNotify String
n [String]
xs Maybe Logger
l Maybe (ExitCode -> IO ())
forall a. Maybe a
Nothing

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 =
  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

     let info :: String -> IO ()
info String
a = case Maybe Logger
mbLog of
                    Maybe Logger
Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                    Just Logger
l  -> Logger -> String -> IO ()
logMessage Logger
l String
a

     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
                               String -> IO ()
info (String
"[stderr] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
errs))
                    IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` \X.SomeException {} -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

     case Maybe (ExitCode -> IO ())
mbOnExit of
       Maybe (ExitCode -> IO ())
Nothing -> () -> IO ()
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 (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
""
                    String -> IO ()
info (String
"[send->] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
txt)
                    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 String -> IO ()
info (String
"[<-recv] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> ShowS
showsSExpr SExpr
res String
"")
                               SExpr -> IO SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SExpr
res
                Maybe SExpr
Nothing  -> String -> IO SExpr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Missing response from solver"

         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 (f :: * -> *) a. Applicative f => a -> f a
pure ())
              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)
                      (\IOException
ex -> String -> IO ()
info (IOException -> String
forall a. Show a => a -> String
show (IOException
ex::X.IOException)))
              ExitCode -> IO ExitCode
forall (m :: * -> *) a. Monad m => a -> m a
return ExitCode
ec

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

     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 (m :: * -> *) a. Monad m => a -> m a
return Solver
solver


-- | 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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
go String
rest
        Maybe (SExpr, String)
Nothing       -> String -> IO ()
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 (m :: * -> *) a. Monad m => a -> m a
return ()
       SExpr
_  -> String -> IO ()
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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       Atom String
"unsupported" -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
       SExpr
_                  -> String -> IO Bool
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 :: 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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return Result
Unsat
       Atom String
"unknown" -> Result -> IO Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
Unknown
       Atom String
"sat"     -> Result -> IO Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
Sat
       SExpr
_ -> String -> IO Result
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 (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 (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)
mapM Char -> Maybe Integer
forall a. Num a => Char -> Maybe a
binDigit String
cs
                 Integer -> Maybe Integer
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 (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)
mapM SExpr -> IO (SExpr, Value)
forall (m :: * -> *). MonadFail m => SExpr -> m (SExpr, Value)
getAns [SExpr]
xs
       SExpr
_ -> String -> IO [(SExpr, Value)]
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 (m :: * -> *) a. Monad m => a -> m a
return (SExpr
e, SExpr -> Value
sexprToVal SExpr
v)
      SExpr
_             -> String -> m (SExpr, Value)
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 (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 (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)
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 (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 (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 (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, Show 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 (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 (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 (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 (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 (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 :: Logger -> Int -> IO a -> IO a
withLogLevel Logger { IO Int
IO ()
Int -> IO ()
String -> IO ()
logUntab :: IO ()
logTab :: IO ()
logSetLevel :: Int -> IO ()
logLevel :: IO Int
logMessage :: String -> IO ()
logUntab :: Logger -> IO ()
logTab :: Logger -> IO ()
logSetLevel :: Logger -> Int -> IO ()
logLevel :: Logger -> IO Int
logMessage :: Logger -> String -> 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 :: Logger -> IO a -> IO a
logIndented Logger { IO Int
IO ()
Int -> IO ()
String -> IO ()
logUntab :: IO ()
logTab :: IO ()
logSetLevel :: Int -> IO ()
logLevel :: IO Int
logMessage :: String -> IO ()
logUntab :: Logger -> IO ()
logTab :: Logger -> IO ()
logSetLevel :: Logger -> Int -> IO ()
logLevel :: Logger -> IO Int
logMessage :: Logger -> String -> 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 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
              String -> IO ()
putStr (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
stdout

         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 (m :: * -> *) a. Monad m => a -> m a
return Logger :: (String -> IO ())
-> IO Int -> (Int -> IO ()) -> IO () -> IO () -> Logger
Logger { IO Int
IO ()
Int -> IO ()
String -> IO ()
logUntab :: IO ()
logTab :: IO ()
logMessage :: String -> IO ()
logSetLevel :: Int -> IO ()
logLevel :: IO Int
logUntab :: IO ()
logTab :: IO ()
logSetLevel :: Int -> IO ()
logLevel :: IO Int
logMessage :: String -> IO ()
.. }