------------------------------------------------------------------------
-- |
-- Module           : What4.Solver.Boolector
-- Description      : Interface for running Boolector
-- Copyright        : (c) Galois, Inc 2014-2020
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
-- This module provides an interface for running Boolector and parsing
-- the results back.
------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module What4.Solver.Boolector
  ( Boolector(..)
  , boolectorPath
  , boolectorOptions
  , boolectorAdapter
  , runBoolectorInOverride
  , withBoolector
  , boolectorFeatures
  ) where

import           Control.Monad
import           Data.Bits ( (.|.) )

import           What4.BaseTypes
import           What4.Config
import           What4.Concrete
import           What4.Interface
import           What4.ProblemFeatures
import           What4.SatResult
import           What4.Expr.Builder
import           What4.Expr.GroundEval
import           What4.Solver.Adapter
import           What4.Protocol.Online
import qualified What4.Protocol.SMTLib2 as SMT2
import           What4.Utils.Process




data Boolector = Boolector deriving Int -> Boolector -> ShowS
[Boolector] -> ShowS
Boolector -> String
(Int -> Boolector -> ShowS)
-> (Boolector -> String)
-> ([Boolector] -> ShowS)
-> Show Boolector
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Boolector] -> ShowS
$cshowList :: [Boolector] -> ShowS
show :: Boolector -> String
$cshow :: Boolector -> String
showsPrec :: Int -> Boolector -> ShowS
$cshowsPrec :: Int -> Boolector -> ShowS
Show

-- | Path to boolector
boolectorPath :: ConfigOption (BaseStringType Unicode)
boolectorPath :: ConfigOption (BaseStringType Unicode)
boolectorPath = BaseTypeRepr (BaseStringType Unicode)
-> String -> ConfigOption (BaseStringType Unicode)
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr (BaseStringType Unicode)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"boolector_path"

boolectorOptions :: [ConfigDesc]
boolectorOptions :: [ConfigDesc]
boolectorOptions =
  [ ConfigOption (BaseStringType Unicode)
-> OptionStyle (BaseStringType Unicode)
-> Maybe (Doc Void)
-> Maybe (ConcreteVal (BaseStringType Unicode))
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
      ConfigOption (BaseStringType Unicode)
boolectorPath
      OptionStyle (BaseStringType Unicode)
executablePathOptSty
      (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Path to boolector executable")
      (ConcreteVal (BaseStringType Unicode)
-> Maybe (ConcreteVal (BaseStringType Unicode))
forall a. a -> Maybe a
Just (StringLiteral Unicode -> ConcreteVal (BaseStringType Unicode)
forall (si :: StringInfo).
StringLiteral si -> ConcreteVal (BaseStringType si)
ConcreteString StringLiteral Unicode
"boolector"))
  ]

boolectorAdapter :: SolverAdapter st
boolectorAdapter :: SolverAdapter st
boolectorAdapter =
  SolverAdapter :: forall (st :: Type -> Type).
String
-> [ConfigDesc]
-> (forall t fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a)
-> (forall t fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())
-> SolverAdapter st
SolverAdapter
  { solver_adapter_name :: String
solver_adapter_name = String
"boolector"
  , solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
boolectorOptions
  , solver_adapter_check_sat :: forall t fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
solver_adapter_check_sat = forall t fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runBoolectorInOverride
  , solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 =
      ()
-> String
-> ProblemFeatures
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
SMT2.writeDefaultSMT2 () String
"Boolector" ProblemFeatures
defaultWriteSMTLIB2Features
  }

instance SMT2.SMTLib2Tweaks Boolector where
  smtlib2tweaks :: Boolector
smtlib2tweaks = Boolector
Boolector

runBoolectorInOverride ::
  ExprBuilder t st fs ->
  LogData ->
  [BoolExpr t] ->
  (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) ->
  IO a
runBoolectorInOverride :: ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runBoolectorInOverride =
  Boolector
-> AcknowledgementAction t (Writer Boolector)
-> ProblemFeatures
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
forall a t (st :: Type -> Type) fs b.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO b)
-> IO b
SMT2.runSolverInOverride Boolector
Boolector AcknowledgementAction t (Writer Boolector)
forall t h. AcknowledgementAction t h
SMT2.nullAcknowledgementAction ProblemFeatures
boolectorFeatures

-- | Run Boolector in a session. Boolector will be configured to produce models, but
-- otherwise left with the default configuration.
withBoolector
  :: ExprBuilder t st fs
  -> FilePath
    -- ^ Path to Boolector executable
  -> LogData
  -> (SMT2.Session t Boolector -> IO a)
    -- ^ Action to run
  -> IO a
withBoolector :: ExprBuilder t st fs
-> String -> LogData -> (Session t Boolector -> IO a) -> IO a
withBoolector = Boolector
-> AcknowledgementAction t (Writer Boolector)
-> ProblemFeatures
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t Boolector -> IO a)
-> IO a
forall a t (st :: Type -> Type) fs b.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t a -> IO b)
-> IO b
SMT2.withSolver Boolector
Boolector AcknowledgementAction t (Writer Boolector)
forall t h. AcknowledgementAction t h
SMT2.nullAcknowledgementAction ProblemFeatures
boolectorFeatures


boolectorFeatures :: ProblemFeatures
boolectorFeatures :: ProblemFeatures
boolectorFeatures = ProblemFeatures
useSymbolicArrays
                ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors

instance SMT2.SMTLib2GenericSolver Boolector where
  defaultSolverPath :: Boolector -> ExprBuilder t st fs -> IO String
defaultSolverPath Boolector
_ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
boolectorPath (Config -> IO String)
-> (ExprBuilder t st fs -> Config)
-> ExprBuilder t st fs
-> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration
  defaultSolverArgs :: Boolector -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs Boolector
_ ExprBuilder t st fs
_ = [String] -> IO [String]
forall (m :: Type -> Type) a. Monad m => a -> m a
return [String
"--smt2", String
"--smt2-model", String
"--incremental", String
"--output-format=smt2", String
"-e=0"]
  defaultFeatures :: Boolector -> ProblemFeatures
defaultFeatures Boolector
_ = ProblemFeatures
boolectorFeatures
  setDefaultLogicAndOptions :: WriterConn t (Writer Boolector) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer Boolector)
writer = do
    WriterConn t (Writer Boolector) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer Boolector)
writer Logic
SMT2.allSupported
    WriterConn t (Writer Boolector) -> Bool -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer Boolector)
writer Bool
True

setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
  SMT2.WriterConn t (SMT2.Writer a) ->
  IO ()
setInteractiveLogicAndOptions :: WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions WriterConn t (Writer a)
writer = do
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"print-success"  Text
"true"
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-models" Text
"true"
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"global-declarations" Text
"true"
    Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (WriterConn t (Writer a) -> ProblemFeatures
forall t h. WriterConn t h -> ProblemFeatures
SMT2.supportedFeatures WriterConn t (Writer a)
writer ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-unsat-cores" Text
"true"
    WriterConn t (Writer a) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer a)
writer Logic
SMT2.allSupported

instance OnlineSolver (SMT2.Writer Boolector) where
  startSolverProcess :: ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer Boolector))
startSolverProcess = Boolector
-> AcknowledgementAction scope (Writer Boolector)
-> (WriterConn scope (Writer Boolector) -> IO ())
-> ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer Boolector))
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> (WriterConn t (Writer a) -> IO ())
-> ProblemFeatures
-> Maybe Handle
-> ExprBuilder t st fs
-> IO (SolverProcess t (Writer a))
SMT2.startSolver Boolector
Boolector AcknowledgementAction scope (Writer Boolector)
forall t a. AcknowledgementAction t (Writer a)
SMT2.smtAckResult WriterConn scope (Writer Boolector) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions
  shutdownSolverProcess :: SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text)
shutdownSolverProcess = Boolector
-> SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text)
forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
SMT2.shutdownSolver Boolector
Boolector