------------------------------------------------------------------------
-- |
-- Module      : What4.Solver.CVC4
-- Description : Solver adapter code for CVC4
-- Copyright   : (c) Galois, Inc 2015-2020
-- License     : BSD3
-- Maintainer  : Rob Dockins <rdockins@galois.com>
-- Stability   : provisional
--
-- CVC4-specific tweaks to the basic SMTLib2 solver interface.
------------------------------------------------------------------------
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}

module What4.Solver.CVC4
  ( CVC4(..)
  , cvc4Features
  , cvc4Adapter
  , cvc4Path
  , cvc4Timeout
  , cvc4Options
  , runCVC4InOverride
  , withCVC4
  , writeCVC4SMT2File
  , writeMultiAsmpCVC4SMT2File
  ) where

import           Control.Monad (forM_, when)
import           Data.Bits
import           Data.String
import           System.IO
import qualified System.IO.Streams as Streams

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


intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt ConfigOption BaseIntegerType
nm Integer
lo Integer
hi = ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
nm OptionStyle BaseIntegerType
sty Maybe (Doc Void)
forall a. Maybe a
Nothing Maybe (ConcreteVal BaseIntegerType)
forall a. Maybe a
Nothing
  where sty :: OptionStyle BaseIntegerType
sty = Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType
integerWithRangeOptSty (Integer -> Bound Integer
forall r. r -> Bound r
Inclusive Integer
lo) (Integer -> Bound Integer
forall r. r -> Bound r
Inclusive Integer
hi)

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

-- | Path to cvc4
cvc4Path :: ConfigOption (BaseStringType Unicode)
cvc4Path :: ConfigOption (BaseStringType Unicode)
cvc4Path = 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
"cvc4_path"

cvc4RandomSeed :: ConfigOption BaseIntegerType
cvc4RandomSeed :: ConfigOption BaseIntegerType
cvc4RandomSeed = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"cvc4.random-seed"

-- | Per-check timeout, in milliseconds (zero is none)
cvc4Timeout :: ConfigOption BaseIntegerType
cvc4Timeout :: ConfigOption BaseIntegerType
cvc4Timeout = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"cvc4_timeout"

cvc4Options :: [ConfigDesc]
cvc4Options :: [ConfigDesc]
cvc4Options =
  [ 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)
cvc4Path
          OptionStyle (BaseStringType Unicode)
executablePathOptSty
          (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Path to CVC4 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
"cvc4"))
  , ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt ConfigOption BaseIntegerType
cvc4RandomSeed (Integer -> Integer
forall a. Num a => a -> a
negate (Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)) (Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)
  , ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
cvc4Timeout
          OptionStyle BaseIntegerType
integerOptSty
          (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Per-check timeout in milliseconds (zero is none)")
          (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
0))
  ]

cvc4Adapter :: SolverAdapter st
cvc4Adapter :: SolverAdapter st
cvc4Adapter =
  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
"cvc4"
  , solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
cvc4Options
  , 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
runCVC4InOverride
  , solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 = forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeCVC4SMT2File
  }

indexType :: [SMT2.Sort] -> SMT2.Sort
indexType :: [Sort] -> Sort
indexType [Sort
i] = Sort
i
indexType [Sort]
il = [Sort] -> Sort
forall a. SMTLib2Tweaks a => [Sort] -> Sort
SMT2.smtlib2StructSort @CVC4 [Sort]
il

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

  smtlib2arrayType :: [Sort] -> Sort -> Sort
smtlib2arrayType [Sort]
il Sort
r = Sort -> Sort -> Sort
SMT2.arraySort ([Sort] -> Sort
indexType [Sort]
il) Sort
r

  smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term)
smtlib2arrayConstant = ([Sort] -> Sort -> Term -> Term)
-> Maybe ([Sort] -> Sort -> Term -> Term)
forall a. a -> Maybe a
Just (([Sort] -> Sort -> Term -> Term)
 -> Maybe ([Sort] -> Sort -> Term -> Term))
-> ([Sort] -> Sort -> Term -> Term)
-> Maybe ([Sort] -> Sort -> Term -> Term)
forall a b. (a -> b) -> a -> b
$ \[Sort]
idx Sort
rtp Term
v ->
    Sort -> Sort -> Term -> Term
SMT2.arrayConst ([Sort] -> Sort
indexType [Sort]
idx) Sort
rtp Term
v

  smtlib2declareStructCmd :: Int -> Maybe Command
smtlib2declareStructCmd Int
_ = Maybe Command
forall a. Maybe a
Nothing

  smtlib2StructSort :: [Sort] -> Sort
smtlib2StructSort []  = Symbol -> Sort
Syntax.varSort Symbol
"Tuple"
  smtlib2StructSort [Sort]
tps = Builder -> Sort
Syntax.Sort (Builder -> Sort) -> Builder -> Sort
forall a b. (a -> b) -> a -> b
$ Builder
"(Tuple" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (Sort -> Builder) -> [Sort] -> Builder
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Sort -> Builder
f [Sort]
tps Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    where f :: Sort -> Builder
f Sort
x = Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Sort -> Builder
Syntax.unSort Sort
x

  smtlib2StructCtor :: [Term] -> Term
smtlib2StructCtor [Term]
args = Builder -> [Term] -> Term
Syntax.term_app Builder
"mkTuple" [Term]
args

  smtlib2StructProj :: Int -> Int -> Term -> Term
smtlib2StructProj Int
_n Int
i Term
x = Builder -> [Term] -> Term
Syntax.term_app ([Builder] -> Builder
Syntax.builder_list [Builder
"_", Builder
"tupSel", String -> Builder
forall a. IsString a => String -> a
fromString (Int -> String
forall a. Show a => a -> String
show Int
i)]) [ Term
x ]

cvc4Features :: ProblemFeatures
cvc4Features :: ProblemFeatures
cvc4Features = ProblemFeatures
useComputableReals
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useIntegerArithmetic
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useSymbolicArrays
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStrings
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStructs
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useFloatingPoint
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useQuantifiers

writeMultiAsmpCVC4SMT2File
   :: ExprBuilder t st fs
   -> Handle
   -> [BoolExpr t]
   -> IO ()
writeMultiAsmpCVC4SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeMultiAsmpCVC4SMT2File ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps = do
  SymbolVarBimap t
bindings <- ExprBuilder t st fs -> IO (SymbolVarBimap t)
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SymbolVarBimap t)
getSymbolVarBimap ExprBuilder t st fs
sym
  OutputStream Symbol
out_str  <- OutputStream ByteString -> IO (OutputStream Symbol)
Streams.encodeUtf8 (OutputStream ByteString -> IO (OutputStream Symbol))
-> IO (OutputStream ByteString) -> IO (OutputStream Symbol)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
h
  InputStream Symbol
in_str <- IO (InputStream Symbol)
forall a. IO (InputStream a)
Streams.nullInput
  WriterConn t (Writer CVC4)
c <- CVC4
-> OutputStream Symbol
-> InputStream Symbol
-> AcknowledgementAction t (Writer CVC4)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer CVC4))
forall a t.
a
-> OutputStream Symbol
-> InputStream Symbol
-> AcknowledgementAction t (Writer a)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
SMT2.newWriter CVC4
CVC4 OutputStream Symbol
out_str InputStream Symbol
in_str AcknowledgementAction t (Writer CVC4)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction String
"CVC4"
         Bool
True ProblemFeatures
cvc4Features Bool
True SymbolVarBimap t
bindings
  WriterConn t (Writer CVC4) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer CVC4)
c Logic
SMT2.allSupported
  WriterConn t (Writer CVC4) -> Bool -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer CVC4)
c Bool
True
  [BoolExpr t] -> (BoolExpr t -> IO ()) -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [BoolExpr t]
ps ((BoolExpr t -> IO ()) -> IO ()) -> (BoolExpr t -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ WriterConn t (Writer CVC4) -> BoolExpr t -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT2.assume WriterConn t (Writer CVC4)
c
  WriterConn t (Writer CVC4) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeCheckSat WriterConn t (Writer CVC4)
c
  WriterConn t (Writer CVC4) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeExit WriterConn t (Writer CVC4)
c

writeCVC4SMT2File
   :: ExprBuilder t st fs
   -> Handle
   -> [BoolExpr t]
   -> IO ()
writeCVC4SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeCVC4SMT2File ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps = ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeMultiAsmpCVC4SMT2File ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps

instance SMT2.SMTLib2GenericSolver CVC4 where
  defaultSolverPath :: CVC4 -> ExprBuilder t st fs -> IO String
defaultSolverPath CVC4
_ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
cvc4Path (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 :: CVC4 -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs CVC4
_ ExprBuilder t st fs
sym = do
    let cfg :: Config
cfg = ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
    Maybe (ConcreteVal BaseIntegerType)
timeout <- OptionSetting BaseIntegerType
-> IO (Maybe (ConcreteVal BaseIntegerType))
forall (tp :: BaseType).
OptionSetting tp -> IO (Maybe (ConcreteVal tp))
getOption (OptionSetting BaseIntegerType
 -> IO (Maybe (ConcreteVal BaseIntegerType)))
-> IO (OptionSetting BaseIntegerType)
-> IO (Maybe (ConcreteVal BaseIntegerType))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
cvc4Timeout Config
cfg
    let extraOpts :: [String]
extraOpts = case Maybe (ConcreteVal BaseIntegerType)
timeout of
                      Just (ConcreteInteger Integer
n) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> [String
"--tlimit-per=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n]
                      Maybe (ConcreteVal BaseIntegerType)
_ -> []
    [String] -> IO [String]
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ [String
"--lang", String
"smt2", String
"--incremental", String
"--strings-exp", String
"--fp-exp"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
extraOpts

  getErrorBehavior :: CVC4
-> WriterConn t (Writer CVC4)
-> InputStream Symbol
-> IO ErrorBehavior
getErrorBehavior CVC4
_ = WriterConn t (Writer CVC4)
-> InputStream Symbol -> IO ErrorBehavior
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> InputStream Symbol -> IO ErrorBehavior
SMT2.queryErrorBehavior

  defaultFeatures :: CVC4 -> ProblemFeatures
defaultFeatures CVC4
_ = ProblemFeatures
cvc4Features

  supportsResetAssertions :: CVC4 -> Bool
supportsResetAssertions CVC4
_ = Bool
True

  setDefaultLogicAndOptions :: WriterConn t (Writer CVC4) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer CVC4)
writer = do
    -- Tell CVC4 to use all supported logics.
    WriterConn t (Writer CVC4) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer CVC4)
writer Logic
SMT2.allSupported
    -- Tell CVC4 to produce models
    WriterConn t (Writer CVC4) -> Bool -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer CVC4)
writer Bool
True

runCVC4InOverride
  :: ExprBuilder t st fs
  -> LogData
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
runCVC4InOverride :: ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runCVC4InOverride = CVC4
-> AcknowledgementAction t (Writer CVC4)
-> 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 CVC4
CVC4 AcknowledgementAction t (Writer CVC4)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction (CVC4 -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC4
CVC4)

-- | Run CVC4 in a session. CVC4 will be configured to produce models, but
-- otherwise left with the default configuration.
withCVC4
  :: ExprBuilder t st fs
  -> FilePath
    -- ^ Path to CVC4 executable
  -> LogData
  -> (SMT2.Session t CVC4 -> IO a)
    -- ^ Action to run
  -> IO a
withCVC4 :: ExprBuilder t st fs
-> String -> LogData -> (Session t CVC4 -> IO a) -> IO a
withCVC4 = CVC4
-> AcknowledgementAction t (Writer CVC4)
-> ProblemFeatures
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t CVC4 -> 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 CVC4
CVC4 AcknowledgementAction t (Writer CVC4)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction (CVC4 -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC4
CVC4)

setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
  WriterConn t (SMT2.Writer a) ->
  IO ()
setInteractiveLogicAndOptions :: WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions WriterConn t (Writer a)
writer = do
    -- Tell CVC4 to acknowledge successful commands
    WriterConn t (Writer a) -> Symbol -> Symbol -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Symbol -> Symbol -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Symbol
"print-success"  Symbol
"true"
    -- Tell CVC4 to produce models
    WriterConn t (Writer a) -> Symbol -> Symbol -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Symbol -> Symbol -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Symbol
"produce-models" Symbol
"true"
    -- Tell CVC4 to make declaraions global, so they are not removed by 'pop' commands
    WriterConn t (Writer a) -> Symbol -> Symbol -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Symbol -> Symbol -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Symbol
"global-declarations" Symbol
"true"
    -- Tell CVC4 to compute UNSAT cores, if that feature is enabled
    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
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) -> Symbol -> Symbol -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Symbol -> Symbol -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Symbol
"produce-unsat-cores" Symbol
"true"
    -- Tell CVC4 to use all supported logics.
    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 CVC4) where
  startSolverProcess :: ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer CVC4))
startSolverProcess ProblemFeatures
feat Maybe Handle
mbIOh ExprBuilder scope st fs
sym = do
    SolverProcess scope (Writer CVC4)
sp <- CVC4
-> AcknowledgementAction scope (Writer CVC4)
-> (WriterConn scope (Writer CVC4) -> IO ())
-> ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer CVC4))
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 CVC4
CVC4 AcknowledgementAction scope (Writer CVC4)
forall t a. AcknowledgementAction t (Writer a)
SMT2.smtAckResult WriterConn scope (Writer CVC4) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions ProblemFeatures
feat Maybe Handle
mbIOh ExprBuilder scope st fs
sym
    SolverGoalTimeout
timeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout (Integer -> SolverGoalTimeout)
-> IO Integer -> IO SolverGoalTimeout
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
               (OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting BaseIntegerType -> IO Integer)
-> IO (OptionSetting BaseIntegerType) -> IO Integer
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
cvc4Timeout (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym))
    SolverProcess scope (Writer CVC4)
-> IO (SolverProcess scope (Writer CVC4))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SolverProcess scope (Writer CVC4)
 -> IO (SolverProcess scope (Writer CVC4)))
-> SolverProcess scope (Writer CVC4)
-> IO (SolverProcess scope (Writer CVC4))
forall a b. (a -> b) -> a -> b
$ SolverProcess scope (Writer CVC4)
sp { solverGoalTimeout :: SolverGoalTimeout
solverGoalTimeout = SolverGoalTimeout
timeout }

  shutdownSolverProcess :: SolverProcess scope (Writer CVC4) -> IO (ExitCode, Text)
shutdownSolverProcess = CVC4 -> SolverProcess scope (Writer CVC4) -> IO (ExitCode, Text)
forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
SMT2.shutdownSolver CVC4
CVC4