Boolector.hs

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

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

boolectorOptions :: [ConfigDesc]
boolectorOptions =
  [ mkOpt
      boolectorPath
      executablePathOptSty
      (Just "Path to boolector executable")
      (Just (ConcreteString "boolector"))
  ]

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
  }

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

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


boolectorFeatures :: ProblemFeatures
boolectorFeatures = useSymbolicArrays
                .|. useBitvectors

instance SMT2.SMTLib2GenericSolver Boolector where
  defaultSolverPath _ = findSolverPath boolectorPath . getConfiguration
  defaultSolverArgs _ _ = return ["--smt2", "--smt2-model", "--incremental", "--output-format=smt2", "-e=0"]
  defaultFeatures _ = boolectorFeatures
  setDefaultLogicAndOptions writer = do
    SMT2.setLogic writer SMT2.allSupported
    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 SMT2.allSupported

instance OnlineSolver (SMT2.Writer Boolector) where
  startSolverProcess = SMT2.startSolver Boolector SMT2.smtAckResult setInteractiveLogicAndOptions
  shutdownSolverProcess = SMT2.shutdownSolver Boolector