Bitwuzla.hs

------------------------------------------------------------------------
-- |
-- Module           : What4.Solver.Bitwuzla
-- Description      : Interface for running Bitwuzla
-- Copyright        : (c) Galois, Inc 2014-2023
-- License          : BSD3
-- Maintainer       : Ryan Scott <rscott@galois.com>
-- Stability        : provisional
--
-- This module provides an interface for running Bitwuzla and parsing
-- the results back.
------------------------------------------------------------------------
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
module What4.Solver.Bitwuzla
  ( Bitwuzla(..)
  , bitwuzlaPath
  , bitwuzlaTimeout
  , bitwuzlaOptions
  , bitwuzlaAdapter
  , runBitwuzlaInOverride
  , withBitwuzla
  , bitwuzlaFeatures
  ) 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 Bitwuzla = Bitwuzla deriving Show

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

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

-- | Control strict parsing for Bitwuzla solver responses (defaults
-- to solver.strict-parsing option setting).
bitwuzlaStrictParsing :: ConfigOption BaseBoolType
bitwuzlaStrictParsing = configOption knownRepr "solver.bitwuzla.strict_parsing"

bitwuzlaOptions :: [ConfigDesc]
bitwuzlaOptions =
  let bpOpt co = mkOpt
                 co
                 executablePathOptSty
                 (Just "Path to bitwuzla executable")
                 (Just (ConcreteString "bitwuzla"))
      mkTmo co = mkOpt co
                 integerOptSty
                 (Just "Per-check timeout in milliseconds (zero is none)")
                 (Just (ConcreteInteger 0))
      bp = bpOpt bitwuzlaPath
  in [ bp
     , mkTmo bitwuzlaTimeout
     , copyOpt (const $ configOptionText bitwuzlaStrictParsing) strictSMTParseOpt
     ] <> SMT2.smtlib2Options

bitwuzlaAdapter :: SolverAdapter st
bitwuzlaAdapter =
  SolverAdapter
  { solver_adapter_name = "bitwuzla"
  , solver_adapter_config_options = bitwuzlaOptions
  , solver_adapter_check_sat = runBitwuzlaInOverride
  , solver_adapter_write_smt2 =
      SMT2.writeDefaultSMT2 () "Bitwuzla" defaultWriteSMTLIB2Features
      (Just bitwuzlaStrictParsing)
  }

instance SMT2.SMTLib2Tweaks Bitwuzla where
  smtlib2tweaks = Bitwuzla

runBitwuzlaInOverride
  :: ExprBuilder t st fs
  -> LogData
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
runBitwuzlaInOverride =
  SMT2.runSolverInOverride Bitwuzla SMT2.nullAcknowledgementAction
  bitwuzlaFeatures (Just bitwuzlaStrictParsing)

-- | Run Bitwuzla in a session. Bitwuzla will be configured to produce models, but
-- otherwise left with the default configuration.
withBitwuzla
  :: ExprBuilder t st fs
  -> FilePath
    -- ^ Path to Bitwuzla executable
  -> LogData
  -> (SMT2.Session t Bitwuzla -> IO a)
    -- ^ Action to run
  -> IO a
withBitwuzla = SMT2.withSolver Bitwuzla SMT2.nullAcknowledgementAction
               bitwuzlaFeatures (Just bitwuzlaStrictParsing)

bitwuzlaFeatures :: ProblemFeatures
bitwuzlaFeatures = useBitvectors
               .|. useFloatingPoint
               .|. useQuantifiers
               .|. useSymbolicArrays
               .|. useUninterpFunctions
               .|. useUnsatCores
               .|. useUnsatAssumptions

instance SMT2.SMTLib2GenericSolver Bitwuzla where
  defaultSolverPath _ = findSolverPath bitwuzlaPath . getConfiguration
  defaultSolverArgs _ sym = do
    let cfg = getConfiguration sym
    timeout <- getOption =<< getOptionSetting bitwuzlaTimeout cfg
    let extraOpts = case timeout of
                      Just (ConcreteInteger n) | n > 0 -> ["-t", show n]
                      _ -> []
    return $ ["--lang", "smt2"] ++ extraOpts
  defaultFeatures _ = bitwuzlaFeatures
  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 Bitwuzla) where
  startSolverProcess feat mbIOh sym = do
    timeout <- SolverGoalTimeout <$>
               (getOpt =<< getOptionSetting bitwuzlaTimeout (getConfiguration sym))
    SMT2.startSolver Bitwuzla SMT2.smtAckResult
                            setInteractiveLogicAndOptions
                            timeout
                            feat
                            (Just bitwuzlaStrictParsing) mbIOh sym
  shutdownSolverProcess = SMT2.shutdownSolver Bitwuzla