{-# LANGUAGE CApiFFI #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}

-- | A module providing a backend that sends commands to Z3 using its C API.
module SMTLIB.Backends.Z3
  ( Config (..),
    Handle,
    defaultConfig,
    new,
    close,
    with,
    toBackend,
  )
where

import Control.Exception (bracket)
import Control.Monad (forM_, void)
import qualified Data.ByteString as BS
import Data.ByteString.Builder.Extra
  ( defaultChunkSize,
    smallChunkSize,
    toLazyByteStringWith,
    untrimmedStrategy,
  )
import qualified Data.ByteString.Lazy.Char8 as LBS
import qualified Data.ByteString.Unsafe
import Foreign.C.String (CString)
import Foreign.ForeignPtr (ForeignPtr, finalizeForeignPtr, newForeignPtr, withForeignPtr)
import Foreign.Ptr (FunPtr, Ptr, nullPtr)
import SMTLIB.Backends (Backend (..))

data Z3Context

data Z3Config

newtype Config = Config
  { -- | A list of options to set during the solver's initialization.
    -- Each pair is of the form @(paramId, paramValue)@, e.g.
    -- @(":produce-models", "true")@.
    Config -> [(ByteString, ByteString)]
parameters :: [(BS.ByteString, BS.ByteString)]
  }

-- | By default, don't set any options during initialization.
defaultConfig :: Config
defaultConfig :: Config
defaultConfig = [(ByteString, ByteString)] -> Config
Config []

newtype Handle = Handle
  { -- | A black-box representing the internal state of the solver.
    Handle -> ForeignPtr Z3Context
context :: ForeignPtr Z3Context
  }

foreign import capi unsafe "z3.h &Z3_del_context" c_Z3_del_context :: FunPtr (Ptr Z3Context -> IO ())

foreign import capi unsafe "z3.h Z3_set_param_value" c_Z3_set_param_value :: Ptr Z3Config -> CString -> CString -> IO ()

foreign import capi unsafe "z3.h Z3_mk_config" c_Z3_mk_config :: IO (Ptr Z3Config)

foreign import capi unsafe "z3.h Z3_mk_context" c_Z3_mk_context :: Ptr Z3Config -> IO (Ptr Z3Context)

foreign import capi unsafe "z3.h Z3_del_config" c_Z3_del_config :: Ptr Z3Config -> IO ()

foreign import capi unsafe "z3.h Z3_set_error_handler" c_Z3_set_error_handler :: Ptr Z3Context -> Ptr () -> IO ()

-- We use ccall to avoid warnings about constness in the C side
-- In the meantime we check in cbits/z3.c that the type of the function is
-- compatible.
foreign import ccall unsafe "z3.h Z3_eval_smtlib2_string" c_Z3_eval_smtlib2_string :: Ptr Z3Context -> CString -> IO CString

-- | Create a new solver instance.
new :: Config -> IO Handle
new :: Config -> IO Handle
new Config
config = do
  -- we don't set a finalizer for this object as we manually delete it during the
  -- context's creation
  Ptr Z3Config
cfg <- IO (Ptr Z3Config)
c_Z3_mk_config
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Config -> [(ByteString, ByteString)]
parameters Config
config) forall a b. (a -> b) -> a -> b
$ \(ByteString
paramId, ByteString
paramValue) ->
    forall a. ByteString -> (CString -> IO a) -> IO a
BS.useAsCString ByteString
paramId forall a b. (a -> b) -> a -> b
$ \CString
cparamId ->
      forall a. ByteString -> (CString -> IO a) -> IO a
BS.useAsCString ByteString
paramValue forall a b. (a -> b) -> a -> b
$ \CString
cparamValue ->
        Ptr Z3Config -> CString -> CString -> IO ()
c_Z3_set_param_value Ptr Z3Config
cfg CString
cparamId CString
cparamValue
  {-
  We set the error handler to ignore errors. That way if an error happens it doesn't
  cause the whole program to crash, and the error message is simply transmitted to
  the Haskell layer inside the output of the 'send' method.
  -}
  Ptr Z3Context
pctx <- Ptr Z3Config -> IO (Ptr Z3Context)
c_Z3_mk_context Ptr Z3Config
cfg
  Ptr Z3Config -> IO ()
c_Z3_del_config Ptr Z3Config
cfg
  Ptr Z3Context -> Ptr () -> IO ()
c_Z3_set_error_handler Ptr Z3Context
pctx forall a. Ptr a
nullPtr
  ForeignPtr Z3Context
ctx <- forall a. FinalizerPtr a -> Ptr a -> IO (ForeignPtr a)
newForeignPtr FunPtr (Ptr Z3Context -> IO ())
c_Z3_del_context Ptr Z3Context
pctx
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ForeignPtr Z3Context -> Handle
Handle ForeignPtr Z3Context
ctx

-- | Release the resources associated with a Z3 instance.
close :: Handle -> IO ()
close :: Handle -> IO ()
close = forall a. ForeignPtr a -> IO ()
finalizeForeignPtr forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> ForeignPtr Z3Context
context

-- | Create a Z3 instance, use it to run a computation and release its resources.
with :: Config -> (Handle -> IO a) -> IO a
with :: forall a. Config -> (Handle -> IO a) -> IO a
with Config
config = forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket (Config -> IO Handle
new Config
config) Handle -> IO ()
close

-- | Create a solver backend out of a Z3 instance.
toBackend :: Handle -> Backend
toBackend :: Handle -> Backend
toBackend Handle
handle = (Builder -> IO ByteString) -> (Builder -> IO ()) -> Backend
Backend Builder -> IO ByteString
backendSend Builder -> IO ()
backendSend_
  where
    backendSend :: Builder -> IO ByteString
backendSend Builder
cmd = do
      let ctx :: ForeignPtr Z3Context
ctx = Handle -> ForeignPtr Z3Context
context Handle
handle
      let cmd' :: ByteString
cmd' =
            ByteString -> ByteString
LBS.toStrict forall a b. (a -> b) -> a -> b
$
              AllocationStrategy -> ByteString -> Builder -> ByteString
toLazyByteStringWith
                (Int -> Int -> AllocationStrategy
untrimmedStrategy Int
smallChunkSize Int
defaultChunkSize)
                ByteString
"\NUL"
                Builder
cmd
      forall a. ByteString -> (CString -> IO a) -> IO a
Data.ByteString.Unsafe.unsafeUseAsCString ByteString
cmd' forall a b. (a -> b) -> a -> b
$ \CString
ccmd' ->
        forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr Z3Context
ctx forall a b. (a -> b) -> a -> b
$ \Ptr Z3Context
pctx -> do
          CString
resp <- Ptr Z3Context -> CString -> IO CString
c_Z3_eval_smtlib2_string Ptr Z3Context
pctx CString
ccmd'
          ByteString -> ByteString
LBS.fromStrict forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CString -> IO ByteString
BS.packCString CString
resp

    backendSend_ :: Builder -> IO ()
backendSend_ = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> IO ByteString
backendSend