------------------------------------------------------------------------
-- |
-- 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
  , boolectorTimeout
  , boolectorOptions
  , boolectorAdapter
  , runBoolectorInOverride
  , withBoolector
  , boolectorFeatures
  ) where

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

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


data Boolector = Boolector deriving Show

-- | Path to boolector
boolectorPath :: ConfigOption (BaseStringType Unicode)
boolectorPath = configOption knownRepr "solver.boolector.path"

boolectorPathOLD :: ConfigOption (BaseStringType Unicode)
boolectorPathOLD = configOption knownRepr "boolector_path"

-- | Per-check timeout, in milliseconds (zero is none)
boolectorTimeout :: ConfigOption BaseIntegerType
boolectorTimeout = configOption knownRepr "solver.boolector.timeout"

-- | Control strict parsing for Boolector solver responses (defaults
-- to solver.strict-parsing option setting).
boolectorStrictParsing :: ConfigOption BaseBoolType
boolectorStrictParsing = configOption knownRepr "solver.boolector.strict_parsing"

boolectorOptions :: [ConfigDesc]
boolectorOptions =
  let bpOpt co = mkOpt
                 co
                 executablePathOptSty
                 (Just "Path to boolector executable")
                 (Just (ConcreteString "boolector"))
      mkTmo co = mkOpt co
                 integerOptSty
                 (Just "Per-check timeout in milliseconds (zero is none)")
                 (Just (ConcreteInteger 0))
      bp = bpOpt boolectorPath
      bp2 = deprecatedOpt [bp] $ bpOpt boolectorPathOLD
  in [ bp, bp2
     , mkTmo boolectorTimeout
     , copyOpt (const $ configOptionText boolectorStrictParsing) strictSMTParseOpt
     ] <> SMT2.smtlib2Options

boolectorAdapter :: SolverAdapter st
boolectorAdapter =
  SolverAdapter
  { solver_adapter_name = "boolector"
  , solver_adapter_config_options = boolectorOptions
  , solver_adapter_check_sat = runBoolectorInOverride
  , solver_adapter_write_smt2 =
      SMT2.writeDefaultSMT2 () "Boolector" defaultWriteSMTLIB2Features
      (Just boolectorStrictParsing)
  }

instance SMT2.SMTLib2Tweaks Boolector where
  smtlib2tweaks = Boolector

runBoolectorInOverride ::
  ExprBuilder t st fs ->
  LogData ->
  [BoolExpr t] ->
  (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) ->
  IO a
runBoolectorInOverride =
  SMT2.runSolverInOverride Boolector SMT2.nullAcknowledgementAction
  boolectorFeatures (Just boolectorStrictParsing)

-- | 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 = SMT2.withSolver Boolector SMT2.nullAcknowledgementAction
                boolectorFeatures (Just boolectorStrictParsing)


boolectorFeatures :: ProblemFeatures
boolectorFeatures = useSymbolicArrays
                .|. useBitvectors

instance SMT2.SMTLib2GenericSolver Boolector where
  defaultSolverPath _ = findSolverPath boolectorPath . getConfiguration
  defaultSolverArgs _ _ = return ["--smt2", "--incremental", "--output-format=smt2", "-e=0"]
  defaultFeatures _ = boolectorFeatures
  setDefaultLogicAndOptions writer = do
    SMT2.setLogic writer Syntax.allLogic
    SMT2.setProduceModels writer True

setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
  SMT2.WriterConn t (SMT2.Writer a) ->
  IO ()
setInteractiveLogicAndOptions writer = do
    SMT2.setOption writer "print-success"  "true"
    SMT2.setOption writer "produce-models" "true"
    SMT2.setOption writer "global-declarations" "true"
    when (SMT2.supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do
      SMT2.setOption writer "produce-unsat-cores" "true"
    SMT2.setLogic writer Syntax.allLogic

instance OnlineSolver (SMT2.Writer Boolector) where
  startSolverProcess feat mbIOh sym = do
    timeout <- SolverGoalTimeout <$>
               (getOpt =<< getOptionSetting boolectorTimeout (getConfiguration sym))
    SMT2.startSolver Boolector SMT2.smtAckResult
                            setInteractiveLogicAndOptions
                            timeout
                            feat
                            (Just boolectorStrictParsing) mbIOh sym
  shutdownSolverProcess = SMT2.shutdownSolver Boolector