CVC5.hs

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

module What4.Solver.CVC5
  ( CVC5(..)
  , cvc5Features
  , cvc5Adapter
  , cvc5Path
  , cvc5Timeout
  , cvc5Options
  , runCVC5InOverride
  , withCVC5
  , writeCVC5SMT2File
  , writeMultiAsmpCVC5SMT2File
  , runCVC5SyGuS
  , withCVC5_SyGuS
  , writeCVC5SyFile
  ) where

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

import           Data.Parameterized.Map (MapF)
import           Data.Parameterized.Some
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           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
import qualified What4.Protocol.SMTLib2.Response as RSP
import qualified What4.Protocol.SMTLib2.Syntax as Syntax
import           What4.Protocol.SMTWriter
import           What4.SatResult
import           What4.Solver.Adapter
import           What4.Utils.Process


intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt nm lo hi = mkOpt nm sty Nothing Nothing
  where sty = integerWithRangeOptSty (Inclusive lo) (Inclusive hi)

data CVC5 = CVC5 deriving Show

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

cvc5RandomSeed :: ConfigOption BaseIntegerType
cvc5RandomSeed = configOption knownRepr "solver.cvc5.random-seed"

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

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

cvc5Options :: [ConfigDesc]
cvc5Options =
  let pathOpt co = mkOpt co
                   executablePathOptSty
                   (Just "Path to CVC5 executable")
                   (Just (ConcreteString "cvc5"))
      p1 = pathOpt cvc5Path
      r1 = intWithRangeOpt cvc5RandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1)
      tmOpt co = mkOpt co
                 integerOptSty
                 (Just "Per-check timeout in milliseconds (zero is none)")
                 (Just (ConcreteInteger 0))
      t1 = tmOpt cvc5Timeout
  in [ p1, r1, t1
     , copyOpt (const $ configOptionText cvc5StrictParsing) strictSMTParseOpt
     ] <> SMT2.smtlib2Options

cvc5Adapter :: SolverAdapter st
cvc5Adapter =
  SolverAdapter
  { solver_adapter_name = "cvc5"
  , solver_adapter_config_options = cvc5Options
  , solver_adapter_check_sat = runCVC5InOverride
  , solver_adapter_write_smt2 = writeCVC5SMT2File
  }

indexType :: [SMT2.Sort] -> SMT2.Sort
indexType [i] = i
indexType il = SMT2.smtlib2StructSort @CVC5 il

indexCtor :: [SMT2.Term] -> SMT2.Term
indexCtor [i] = i
indexCtor il = SMT2.smtlib2StructCtor @CVC5 il

instance SMT2.SMTLib2Tweaks CVC5 where
  smtlib2tweaks = CVC5

  smtlib2arrayType il r = SMT2.arraySort (indexType il) r

  smtlib2arrayConstant = Just $ \idx rtp v ->
    SMT2.arrayConst (indexType idx) rtp v
  smtlib2arraySelect a i = SMT2.arraySelect a (indexCtor i)
  smtlib2arrayUpdate a i = SMT2.arrayStore a (indexCtor i)

cvc5Features :: ProblemFeatures
cvc5Features = useComputableReals
           .|. useIntegerArithmetic
           .|. useSymbolicArrays
           .|. useStrings
           .|. useStructs
           .|. useFloatingPoint
           .|. useUnsatCores
           .|. useUnsatAssumptions
           .|. useUninterpFunctions
           .|. useDefinedFunctions
           .|. useBitvectors
           .|. useQuantifiers
           .|. useProduceAbducts

writeMultiAsmpCVC5SMT2File
   :: ExprBuilder t st fs
   -> Handle
   -> [BoolExpr t]
   -> IO ()
writeMultiAsmpCVC5SMT2File sym h ps = do
  bindings <- getSymbolVarBimap sym
  out_str  <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
  in_str <- Streams.nullInput
  let cfg = getConfiguration sym
  strictness <- maybe Strict
                (\c -> if fromConcreteBool c then Strict else Lenient) <$>
                (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)
  c <- SMT2.newWriter CVC5 out_str in_str nullAcknowledgementAction strictness "CVC5"
         True cvc5Features True bindings
  SMT2.setLogic c Syntax.allLogic
  SMT2.setProduceModels c True
  forM_ ps $ SMT2.assume c
  SMT2.writeCheckSat c
  SMT2.writeExit c

writeCVC5SMT2File
   :: ExprBuilder t st fs
   -> Handle
   -> [BoolExpr t]
   -> IO ()
writeCVC5SMT2File sym h ps = writeMultiAsmpCVC5SMT2File sym h ps

instance SMT2.SMTLib2GenericSolver CVC5 where
  defaultSolverPath _ = findSolverPath cvc5Path . getConfiguration

  defaultSolverArgs _ sym = do
    let cfg = getConfiguration sym
    timeout <- getOption =<< getOptionSetting cvc5Timeout cfg
    let extraOpts = case timeout of
                      Just (ConcreteInteger n) | n > 0 -> ["--tlimit-per=" ++ show n]
                      _ -> []
    return $ ["--lang", "smt2", "--incremental", "--strings-exp", "--fp-exp"] ++ extraOpts

  getErrorBehavior _ = SMT2.queryErrorBehavior

  defaultFeatures _ = cvc5Features

  supportsResetAssertions _ = True

  setDefaultLogicAndOptions writer = do
    -- Tell cvc5 to use all supported logics.
    SMT2.setLogic writer Syntax.allLogic
    -- Tell cvc5 to produce models
    SMT2.setProduceModels writer True
    -- Tell cvc5 to produce abducts
    SMT2.setOption writer "produce-abducts" "true"

runCVC5InOverride
  :: ExprBuilder t st fs
  -> LogData
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
runCVC5InOverride = SMT2.runSolverInOverride CVC5 nullAcknowledgementAction
                    (SMT2.defaultFeatures CVC5) (Just cvc5StrictParsing)

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

setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
  WriterConn t (SMT2.Writer a) ->
  IO ()
setInteractiveLogicAndOptions writer = do
    -- Tell cvc5 to acknowledge successful commands
    SMT2.setOption writer "print-success"  "true"
    -- Tell cvc5 to produce models
    SMT2.setOption writer "produce-models" "true"
    -- Tell cvc5 to make declarations global, so they are not removed by 'pop' commands
    SMT2.setOption writer "global-declarations" "true"
    -- Tell cvc5 to compute UNSAT cores, if that feature is enabled
    when (supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do
      SMT2.setOption writer "produce-unsat-cores" "true"
    -- Tell cvc5 to produce abducts, if that feature is enabled
    when (supportedFeatures writer `hasProblemFeature` useProduceAbducts) $ do
      SMT2.setOption writer "produce-abducts" "true"
    -- Tell cvc5 to use all supported logics.
    SMT2.setLogic writer Syntax.allLogic

instance OnlineSolver (SMT2.Writer CVC5) where
  startSolverProcess feat mbIOh sym = do
    timeout <- SolverGoalTimeout <$>
               (getOpt =<< getOptionSetting cvc5Timeout (getConfiguration sym))
    SMT2.startSolver CVC5 SMT2.smtAckResult setInteractiveLogicAndOptions
          timeout feat (Just cvc5StrictParsing) mbIOh sym

  shutdownSolverProcess = SMT2.shutdownSolver CVC5


-- | `CVC5_SyGuS` implements a `SMT2.SMTLib2GenericSolver` instance that is
-- different from `CVC5` in that it provides SyGuS specific implementations for
-- `defaultSolverArgs` and `setDefaultLogicAndOptions`.
data CVC5_SyGuS = CVC5_SyGuS deriving Show

instance SMT2.SMTLib2Tweaks CVC5_SyGuS where
  smtlib2tweaks = CVC5_SyGuS

  smtlib2arrayType = SMT2.smtlib2arrayType @CVC5

  smtlib2arrayConstant = SMT2.smtlib2arrayConstant @CVC5
  smtlib2arraySelect = SMT2.smtlib2arraySelect @CVC5
  smtlib2arrayUpdate = SMT2.smtlib2arrayUpdate @CVC5

  smtlib2declareStructCmd = SMT2.smtlib2declareStructCmd @CVC5
  smtlib2StructSort = SMT2.smtlib2StructSort @CVC5
  smtlib2StructCtor = SMT2.smtlib2StructCtor @CVC5
  smtlib2StructProj = SMT2.smtlib2StructProj @CVC5

instance SMT2.SMTLib2GenericSolver CVC5_SyGuS where
  defaultSolverPath _ = SMT2.defaultSolverPath CVC5

  defaultSolverArgs _ sym = do
    let cfg = getConfiguration sym
    timeout <- getOption =<< getOptionSetting cvc5Timeout cfg
    let extraOpts = case timeout of
                      Just (ConcreteInteger n) | n > 0 -> ["--tlimit-per=" ++ show n]
                      _ -> []
    return $ ["--sygus", "--lang", "sygus2", "--strings-exp", "--fp-exp"] ++ extraOpts

  getErrorBehavior _ = SMT2.queryErrorBehavior

  defaultFeatures _ = SMT2.defaultFeatures CVC5

  supportsResetAssertions _ = SMT2.supportsResetAssertions CVC5

  setDefaultLogicAndOptions writer = do
    -- Tell cvc5 to use all supported logics.
    SMT2.setLogic writer Syntax.allLogic

-- | Find a solution to a Syntax-Guided Synthesis (SyGuS) problem.
--
-- For more information, see the [SyGuS standard](https://sygus.org/).
runCVC5SyGuS ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  LogData ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
runCVC5SyGuS sym log_data synth_fns constraints = do
  logSolverEvent sym
    (SolverStartSATQuery $ SolverStartSATQueryRec
      { satQuerySolverName = show CVC5_SyGuS
      , satQueryReason = logReason log_data
      })

  path <- SMT2.defaultSolverPath CVC5_SyGuS sym
  withCVC5_SyGuS sym path (log_data { logVerbosity = 2 }) $ \session -> do
    writeSyGuSProblem sym (SMT2.sessionWriter session) synth_fns constraints
    result <- RSP.getLimitedSolverResponse "check-synth"
      (\case
        RSP.AckSuccessSExp sexp -> Just $ Sat sexp
        RSP.AckInfeasible -> Just $ Unsat ()
        RSP.AckFail -> Just Unknown
        _ -> Nothing)
      (SMT2.sessionWriter session)
      Syntax.checkSynth

    logSolverEvent sym
      (SolverEndSATQuery $ SolverEndSATQueryRec
        { satQueryResult = forgetModelAndCore result
        , satQueryError = Nothing
        })

    traverseSatResult
      (\sexp -> SMT2.parseFnModel sym (SMT2.sessionWriter session) synth_fns sexp)
      return
      result

-- | Run CVC5 SyGuS in a session, with the default configuration.
withCVC5_SyGuS ::
  ExprBuilder t st fs ->
  FilePath ->
  LogData ->
  (SMT2.Session t CVC5_SyGuS -> IO a) ->
  IO a
withCVC5_SyGuS =
  SMT2.withSolver
    CVC5_SyGuS
    nullAcknowledgementAction
    (SMT2.defaultFeatures CVC5_SyGuS)
    (Just cvc5StrictParsing)

writeCVC5SyFile ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  Handle ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO ()
writeCVC5SyFile sym h synth_fns constraints = do
  writer <- SMT2.defaultFileWriter
    CVC5_SyGuS
    (show CVC5_SyGuS)
    (SMT2.defaultFeatures CVC5_SyGuS)
    (Just cvc5StrictParsing)
    sym
    h
  SMT2.setDefaultLogicAndOptions writer
  writeSyGuSProblem sym writer synth_fns constraints
  SMT2.writeExit writer

writeSyGuSProblem ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  WriterConn t (SMT2.Writer CVC5_SyGuS) ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO ()
writeSyGuSProblem sym writer synth_fns constraints = do
  mapM_ (\(SomeSymFn fn) -> addSynthFun writer fn) synth_fns
  mapM_ (viewSome $ addDeclareVar writer) $ foldMap (exprUninterpConstants sym) constraints
  mapM_ (addConstraint writer) constraints
  SMT2.writeCheckSynth writer