------------------------------------------------------------------------
-- |
-- 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 :: 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 CVC5 = CVC5 deriving Int -> CVC5 -> ShowS
[CVC5] -> ShowS
CVC5 -> String
(Int -> CVC5 -> ShowS)
-> (CVC5 -> String) -> ([CVC5] -> ShowS) -> Show CVC5
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CVC5 -> ShowS
showsPrec :: Int -> CVC5 -> ShowS
$cshow :: CVC5 -> String
show :: CVC5 -> String
$cshowList :: [CVC5] -> ShowS
showList :: [CVC5] -> ShowS
Show

-- | Path to cvc5
cvc5Path :: ConfigOption (BaseStringType Unicode)
cvc5Path :: ConfigOption (BaseStringType Unicode)
cvc5Path = 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
"solver.cvc5.path"

cvc5RandomSeed :: ConfigOption BaseIntegerType
cvc5RandomSeed :: ConfigOption BaseIntegerType
cvc5RandomSeed = 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
"solver.cvc5.random-seed"

-- | Per-check timeout, in milliseconds (zero is none)
cvc5Timeout :: ConfigOption BaseIntegerType
cvc5Timeout :: ConfigOption BaseIntegerType
cvc5Timeout = 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
"solver.cvc5.timeout"

-- | Control strict parsing for cvc5 solver responses (defaults
-- to solver.strict-parsing option setting).
cvc5StrictParsing :: ConfigOption BaseBoolType
cvc5StrictParsing :: ConfigOption BaseBoolType
cvc5StrictParsing = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.cvc5.strict_parsing"

cvc5Options :: [ConfigDesc]
cvc5Options :: [ConfigDesc]
cvc5Options =
  let pathOpt :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
pathOpt ConfigOption (BaseStringType Unicode)
co = 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)
co
                   OptionStyle (BaseStringType Unicode)
executablePathOptSty
                   (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Path to CVC5 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
"cvc5"))
      p1 :: ConfigDesc
p1 = ConfigOption (BaseStringType Unicode) -> ConfigDesc
pathOpt ConfigOption (BaseStringType Unicode)
cvc5Path
      r1 :: ConfigDesc
r1 = ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt ConfigOption BaseIntegerType
cvc5RandomSeed (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)
      tmOpt :: ConfigOption BaseIntegerType -> ConfigDesc
tmOpt ConfigOption BaseIntegerType
co = 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
co
                 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))
      t1 :: ConfigDesc
t1 = ConfigOption BaseIntegerType -> ConfigDesc
tmOpt ConfigOption BaseIntegerType
cvc5Timeout
  in [ ConfigDesc
p1, ConfigDesc
r1, ConfigDesc
t1
     , (Text -> Text) -> ConfigDesc -> ConfigDesc
copyOpt (Text -> Text -> Text
forall a b. a -> b -> a
const (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. (a -> b) -> a -> b
$ ConfigOption BaseBoolType -> Text
forall (tp :: BaseType). ConfigOption tp -> Text
configOptionText ConfigOption BaseBoolType
cvc5StrictParsing) ConfigDesc
strictSMTParseOpt
     ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
forall a. Semigroup a => a -> a -> a
<> [ConfigDesc]
SMT2.smtlib2Options

cvc5Adapter :: SolverAdapter st
cvc5Adapter :: forall (st :: Type -> Type). SolverAdapter st
cvc5Adapter =
  SolverAdapter
  { solver_adapter_name :: String
solver_adapter_name = String
"cvc5"
  , solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
cvc5Options
  , 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 = ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
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
runCVC5InOverride
  , solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 = ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
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 ()
writeCVC5SMT2File
  }

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

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

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

  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
  smtlib2arraySelect :: Term -> [Term] -> Term
smtlib2arraySelect Term
a [Term]
i = Term -> Term -> Term
SMT2.arraySelect Term
a ([Term] -> Term
indexCtor [Term]
i)
  smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term
smtlib2arrayUpdate Term
a [Term]
i = Term -> Term -> Term -> Term
SMT2.arrayStore Term
a ([Term] -> Term
indexCtor [Term]
i)

cvc5Features :: ProblemFeatures
cvc5Features :: ProblemFeatures
cvc5Features = 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
useUnsatCores
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useUnsatAssumptions
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useUninterpFunctions
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useDefinedFunctions
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useQuantifiers
           ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useProduceAbducts

writeMultiAsmpCVC5SMT2File
   :: ExprBuilder t st fs
   -> Handle
   -> [BoolExpr t]
   -> IO ()
writeMultiAsmpCVC5SMT2File :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeMultiAsmpCVC5SMT2File 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 Text
out_str  <- OutputStream ByteString -> IO (OutputStream Text)
Streams.encodeUtf8 (OutputStream ByteString -> IO (OutputStream Text))
-> IO (OutputStream ByteString) -> IO (OutputStream Text)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
h
  InputStream Text
in_str <- IO (InputStream Text)
forall a. IO (InputStream a)
Streams.nullInput
  let cfg :: Config
cfg = ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
  ResponseStrictness
strictness <- ResponseStrictness
-> (ConcreteVal BaseBoolType -> ResponseStrictness)
-> Maybe (ConcreteVal BaseBoolType)
-> ResponseStrictness
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ResponseStrictness
Strict
                (\ConcreteVal BaseBoolType
c -> if ConcreteVal BaseBoolType -> Bool
fromConcreteBool ConcreteVal BaseBoolType
c then ResponseStrictness
Strict else ResponseStrictness
Lenient) (Maybe (ConcreteVal BaseBoolType) -> ResponseStrictness)
-> IO (Maybe (ConcreteVal BaseBoolType)) -> IO ResponseStrictness
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
                (OptionSetting BaseBoolType -> IO (Maybe (ConcreteVal BaseBoolType))
forall (tp :: BaseType).
OptionSetting tp -> IO (Maybe (ConcreteVal tp))
getOption (OptionSetting BaseBoolType
 -> IO (Maybe (ConcreteVal BaseBoolType)))
-> IO (OptionSetting BaseBoolType)
-> IO (Maybe (ConcreteVal BaseBoolType))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
RSP.strictSMTParsing Config
cfg)
  WriterConn t (Writer CVC5)
c <- CVC5
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer CVC5)
-> ResponseStrictness
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer CVC5))
forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> ResponseStrictness
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
SMT2.newWriter CVC5
CVC5 OutputStream Text
out_str InputStream Text
in_str AcknowledgementAction t (Writer CVC5)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction ResponseStrictness
strictness String
"CVC5"
         Bool
True ProblemFeatures
cvc5Features Bool
True SymbolVarBimap t
bindings
  WriterConn t (Writer CVC5) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer CVC5)
c Logic
Syntax.allLogic
  WriterConn t (Writer CVC5) -> Bool -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer CVC5)
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 CVC5) -> BoolExpr t -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT2.assume WriterConn t (Writer CVC5)
c
  WriterConn t (Writer CVC5) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeCheckSat WriterConn t (Writer CVC5)
c
  WriterConn t (Writer CVC5) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeExit WriterConn t (Writer CVC5)
c

writeCVC5SMT2File
   :: ExprBuilder t st fs
   -> Handle
   -> [BoolExpr t]
   -> IO ()
writeCVC5SMT2File :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeCVC5SMT2File 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 ()
writeMultiAsmpCVC5SMT2File ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps

instance SMT2.SMTLib2GenericSolver CVC5 where
  defaultSolverPath :: forall t (st :: Type -> Type) fs.
CVC5 -> ExprBuilder t st fs -> IO String
defaultSolverPath CVC5
_ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
cvc5Path (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 :: forall t (st :: Type -> Type) fs.
CVC5 -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs CVC5
_ 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
cvc5Timeout 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 a. a -> IO a
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 :: forall t. CVC5 -> WriterConn t (Writer CVC5) -> IO ErrorBehavior
getErrorBehavior CVC5
_ = WriterConn t (Writer CVC5) -> IO ErrorBehavior
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> IO ErrorBehavior
SMT2.queryErrorBehavior

  defaultFeatures :: CVC5 -> ProblemFeatures
defaultFeatures CVC5
_ = ProblemFeatures
cvc5Features

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

  setDefaultLogicAndOptions :: forall t. WriterConn t (Writer CVC5) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer CVC5)
writer = do
    -- Tell cvc5 to use all supported logics.
    WriterConn t (Writer CVC5) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer CVC5)
writer Logic
Syntax.allLogic
    -- Tell cvc5 to produce models
    WriterConn t (Writer CVC5) -> Bool -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer CVC5)
writer Bool
True
    -- Tell cvc5 to produce abducts
    WriterConn t (Writer CVC5) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer CVC5)
writer Text
"produce-abducts" Text
"true"

runCVC5InOverride
  :: ExprBuilder t st fs
  -> LogData
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
runCVC5InOverride :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runCVC5InOverride = CVC5
-> AcknowledgementAction t (Writer CVC5)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> 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
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO b)
-> IO b
forall t (st :: Type -> Type) fs b.
CVC5
-> AcknowledgementAction t (Writer CVC5)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO b)
-> IO b
SMT2.runSolverInOverride CVC5
CVC5 AcknowledgementAction t (Writer CVC5)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction
                    (CVC5 -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC5
CVC5) (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
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 :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t CVC5 -> IO a) -> IO a
withCVC5 = CVC5
-> AcknowledgementAction t (Writer CVC5)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t CVC5 -> IO a)
-> IO a
forall a t (st :: Type -> Type) fs b.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t a -> IO b)
-> IO b
forall t (st :: Type -> Type) fs b.
CVC5
-> AcknowledgementAction t (Writer CVC5)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t CVC5 -> IO b)
-> IO b
SMT2.withSolver CVC5
CVC5 AcknowledgementAction t (Writer CVC5)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction
           (CVC5 -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC5
CVC5) (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
cvc5StrictParsing)

setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
  WriterConn t (SMT2.Writer a) ->
  IO ()
setInteractiveLogicAndOptions :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions WriterConn t (Writer a)
writer = do
    -- Tell cvc5 to acknowledge successful commands
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"print-success"  Text
"true"
    -- Tell cvc5 to produce models
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-models" Text
"true"
    -- Tell cvc5 to make declarations global, so they are not removed by 'pop' commands
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"global-declarations" Text
"true"
    -- Tell cvc5 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) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-unsat-cores" Text
"true"
    -- Tell cvc5 to produce abducts, 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
useProduceAbducts) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-abducts" Text
"true"
    -- Tell cvc5 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
Syntax.allLogic

instance OnlineSolver (SMT2.Writer CVC5) where
  startSolverProcess :: forall scope (st :: Type -> Type) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer CVC5))
startSolverProcess ProblemFeatures
feat Maybe Handle
mbIOh ExprBuilder scope st fs
sym = do
    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
cvc5Timeout (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym))
    CVC5
-> AcknowledgementAction scope (Writer CVC5)
-> (WriterConn scope (Writer CVC5) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer CVC5))
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> (WriterConn t (Writer a) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> Maybe Handle
-> ExprBuilder t st fs
-> IO (SolverProcess t (Writer a))
SMT2.startSolver CVC5
CVC5 AcknowledgementAction scope (Writer CVC5)
forall t a. AcknowledgementAction t (Writer a)
SMT2.smtAckResult WriterConn scope (Writer CVC5) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions
          SolverGoalTimeout
timeout ProblemFeatures
feat (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
cvc5StrictParsing) Maybe Handle
mbIOh ExprBuilder scope st fs
sym

  shutdownSolverProcess :: forall scope.
SolverProcess scope (Writer CVC5) -> IO (ExitCode, Text)
shutdownSolverProcess = CVC5 -> SolverProcess scope (Writer CVC5) -> IO (ExitCode, Text)
forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
SMT2.shutdownSolver CVC5
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 Int -> CVC5_SyGuS -> ShowS
[CVC5_SyGuS] -> ShowS
CVC5_SyGuS -> String
(Int -> CVC5_SyGuS -> ShowS)
-> (CVC5_SyGuS -> String)
-> ([CVC5_SyGuS] -> ShowS)
-> Show CVC5_SyGuS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CVC5_SyGuS -> ShowS
showsPrec :: Int -> CVC5_SyGuS -> ShowS
$cshow :: CVC5_SyGuS -> String
show :: CVC5_SyGuS -> String
$cshowList :: [CVC5_SyGuS] -> ShowS
showList :: [CVC5_SyGuS] -> ShowS
Show

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

  smtlib2arrayType :: [Sort] -> Sort -> Sort
smtlib2arrayType = forall a. SMTLib2Tweaks a => [Sort] -> Sort -> Sort
SMT2.smtlib2arrayType @CVC5

  smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term)
smtlib2arrayConstant = forall a. SMTLib2Tweaks a => Maybe ([Sort] -> Sort -> Term -> Term)
SMT2.smtlib2arrayConstant @CVC5
  smtlib2arraySelect :: Term -> [Term] -> Term
smtlib2arraySelect = forall a. SMTLib2Tweaks a => Term -> [Term] -> Term
SMT2.smtlib2arraySelect @CVC5
  smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term
smtlib2arrayUpdate = forall a. SMTLib2Tweaks a => Term -> [Term] -> Term -> Term
SMT2.smtlib2arrayUpdate @CVC5

  smtlib2declareStructCmd :: Int -> Maybe Command
smtlib2declareStructCmd = forall a. SMTLib2Tweaks a => Int -> Maybe Command
SMT2.smtlib2declareStructCmd @CVC5
  smtlib2StructSort :: [Sort] -> Sort
smtlib2StructSort = forall a. SMTLib2Tweaks a => [Sort] -> Sort
SMT2.smtlib2StructSort @CVC5
  smtlib2StructCtor :: [Term] -> Term
smtlib2StructCtor = forall a. SMTLib2Tweaks a => [Term] -> Term
SMT2.smtlib2StructCtor @CVC5
  smtlib2StructProj :: Int -> Int -> Term -> Term
smtlib2StructProj = forall a. SMTLib2Tweaks a => Int -> Int -> Term -> Term
SMT2.smtlib2StructProj @CVC5

instance SMT2.SMTLib2GenericSolver CVC5_SyGuS where
  defaultSolverPath :: forall t (st :: Type -> Type) fs.
CVC5_SyGuS -> ExprBuilder t st fs -> IO String
defaultSolverPath CVC5_SyGuS
_ = CVC5 -> ExprBuilder t st fs -> IO String
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a -> ExprBuilder t st fs -> IO String
forall t (st :: Type -> Type) fs.
CVC5 -> ExprBuilder t st fs -> IO String
SMT2.defaultSolverPath CVC5
CVC5

  defaultSolverArgs :: forall t (st :: Type -> Type) fs.
CVC5_SyGuS -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs CVC5_SyGuS
_ 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
cvc5Timeout 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 a. a -> IO a
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
"--sygus", String
"--lang", String
"sygus2", String
"--strings-exp", String
"--fp-exp"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
extraOpts

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

  defaultFeatures :: CVC5_SyGuS -> ProblemFeatures
defaultFeatures CVC5_SyGuS
_ = CVC5 -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC5
CVC5

  supportsResetAssertions :: CVC5_SyGuS -> Bool
supportsResetAssertions CVC5_SyGuS
_ = CVC5 -> Bool
forall a. SMTLib2GenericSolver a => a -> Bool
SMT2.supportsResetAssertions CVC5
CVC5

  setDefaultLogicAndOptions :: forall t. WriterConn t (Writer CVC5_SyGuS) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer CVC5_SyGuS)
writer = do
    -- Tell cvc5 to use all supported logics.
    WriterConn t (Writer CVC5_SyGuS) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer CVC5_SyGuS)
writer Logic
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 :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> LogData
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
runCVC5SyGuS sym
sym LogData
log_data [SomeSymFn sym]
synth_fns [BoolExpr t]
constraints = do
  sym -> SolverEvent -> IO ()
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent sym
sym
    (SolverStartSATQuery -> SolverEvent
SolverStartSATQuery (SolverStartSATQuery -> SolverEvent)
-> SolverStartSATQuery -> SolverEvent
forall a b. (a -> b) -> a -> b
$ SolverStartSATQueryRec
      { satQuerySolverName :: String
satQuerySolverName = CVC5_SyGuS -> String
forall a. Show a => a -> String
show CVC5_SyGuS
CVC5_SyGuS
      , satQueryReason :: String
satQueryReason = LogData -> String
logReason LogData
log_data
      })

  String
path <- CVC5_SyGuS -> ExprBuilder t st fs -> IO String
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a -> ExprBuilder t st fs -> IO String
forall t (st :: Type -> Type) fs.
CVC5_SyGuS -> ExprBuilder t st fs -> IO String
SMT2.defaultSolverPath CVC5_SyGuS
CVC5_SyGuS sym
ExprBuilder t st fs
sym
  ExprBuilder t st fs
-> String
-> LogData
-> (Session t CVC5_SyGuS
    -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t CVC5_SyGuS -> IO a) -> IO a
withCVC5_SyGuS sym
ExprBuilder t st fs
sym String
path (LogData
log_data { logVerbosity = 2 }) ((Session t CVC5_SyGuS
  -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
 -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
-> (Session t CVC5_SyGuS
    -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall a b. (a -> b) -> a -> b
$ \Session t CVC5_SyGuS
session -> do
    sym
-> WriterConn t (Writer CVC5_SyGuS)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t (Writer CVC5_SyGuS)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
writeSyGuSProblem sym
sym (Session t CVC5_SyGuS -> WriterConn t (Writer CVC5_SyGuS)
forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t CVC5_SyGuS
session) [SomeSymFn sym]
synth_fns [BoolExpr t]
constraints
    SatResult SExp ()
result <- String
-> (SMTResponse -> Maybe (SatResult SExp ()))
-> WriterConn t (Writer CVC5_SyGuS)
-> Command
-> IO (SatResult SExp ())
forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
RSP.getLimitedSolverResponse String
"check-synth"
      (\case
        RSP.AckSuccessSExp SExp
sexp -> SatResult SExp () -> Maybe (SatResult SExp ())
forall a. a -> Maybe a
Just (SatResult SExp () -> Maybe (SatResult SExp ()))
-> SatResult SExp () -> Maybe (SatResult SExp ())
forall a b. (a -> b) -> a -> b
$ SExp -> SatResult SExp ()
forall mdl core. mdl -> SatResult mdl core
Sat SExp
sexp
        SMTResponse
RSP.AckInfeasible -> SatResult SExp () -> Maybe (SatResult SExp ())
forall a. a -> Maybe a
Just (SatResult SExp () -> Maybe (SatResult SExp ()))
-> SatResult SExp () -> Maybe (SatResult SExp ())
forall a b. (a -> b) -> a -> b
$ () -> SatResult SExp ()
forall mdl core. core -> SatResult mdl core
Unsat ()
        SMTResponse
RSP.AckFail -> SatResult SExp () -> Maybe (SatResult SExp ())
forall a. a -> Maybe a
Just SatResult SExp ()
forall mdl core. SatResult mdl core
Unknown
        SMTResponse
_ -> Maybe (SatResult SExp ())
forall a. Maybe a
Nothing)
      (Session t CVC5_SyGuS -> WriterConn t (Writer CVC5_SyGuS)
forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t CVC5_SyGuS
session)
      Command
Syntax.checkSynth

    sym -> SolverEvent -> IO ()
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent sym
sym
      (SolverEndSATQuery -> SolverEvent
SolverEndSATQuery (SolverEndSATQuery -> SolverEvent)
-> SolverEndSATQuery -> SolverEvent
forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec
        { satQueryResult :: SatResult () ()
satQueryResult = SatResult SExp () -> SatResult () ()
forall a b. SatResult a b -> SatResult () ()
forgetModelAndCore SatResult SExp ()
result
        , satQueryError :: Maybe String
satQueryError = Maybe String
forall a. Maybe a
Nothing
        })

    (SExp -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym)))
-> (() -> IO ())
-> SatResult SExp ()
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall (t :: Type -> Type) a q b r.
Applicative t =>
(a -> t q) -> (b -> t r) -> SatResult a b -> t (SatResult q r)
traverseSatResult
      (\SExp
sexp -> sym
-> WriterConn t (Writer CVC5_SyGuS)
-> [SomeSymFn sym]
-> SExp
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
forall sym t (st :: Type -> Type) fs h.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t h
-> [SomeSymFn sym]
-> SExp
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
SMT2.parseFnModel sym
sym (Session t CVC5_SyGuS -> WriterConn t (Writer CVC5_SyGuS)
forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t CVC5_SyGuS
session) [SomeSymFn sym]
synth_fns SExp
sexp)
      () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return
      SatResult SExp ()
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 :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t CVC5_SyGuS -> IO a) -> IO a
withCVC5_SyGuS =
  CVC5_SyGuS
-> AcknowledgementAction t (Writer CVC5_SyGuS)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t CVC5_SyGuS -> IO a)
-> IO a
forall a t (st :: Type -> Type) fs b.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t a -> IO b)
-> IO b
forall t (st :: Type -> Type) fs b.
CVC5_SyGuS
-> AcknowledgementAction t (Writer CVC5_SyGuS)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t CVC5_SyGuS -> IO b)
-> IO b
SMT2.withSolver
    CVC5_SyGuS
CVC5_SyGuS
    AcknowledgementAction t (Writer CVC5_SyGuS)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction
    (CVC5_SyGuS -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC5_SyGuS
CVC5_SyGuS)
    (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
cvc5StrictParsing)

writeCVC5SyFile ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  Handle ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO ()
writeCVC5SyFile :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO ()
writeCVC5SyFile sym
sym Handle
h [SomeSymFn sym]
synth_fns [BoolExpr t]
constraints = do
  WriterConn t (Writer CVC5_SyGuS)
writer <- CVC5_SyGuS
-> String
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> IO (WriterConn t (Writer CVC5_SyGuS))
forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> IO (WriterConn t (Writer a))
SMT2.defaultFileWriter
    CVC5_SyGuS
CVC5_SyGuS
    (CVC5_SyGuS -> String
forall a. Show a => a -> String
show CVC5_SyGuS
CVC5_SyGuS)
    (CVC5_SyGuS -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC5_SyGuS
CVC5_SyGuS)
    (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
cvc5StrictParsing)
    sym
ExprBuilder t st fs
sym
    Handle
h
  WriterConn t (Writer CVC5_SyGuS) -> IO ()
forall t. WriterConn t (Writer CVC5_SyGuS) -> IO ()
forall a t.
SMTLib2GenericSolver a =>
WriterConn t (Writer a) -> IO ()
SMT2.setDefaultLogicAndOptions WriterConn t (Writer CVC5_SyGuS)
writer
  sym
-> WriterConn t (Writer CVC5_SyGuS)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t (Writer CVC5_SyGuS)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
writeSyGuSProblem sym
sym WriterConn t (Writer CVC5_SyGuS)
writer [SomeSymFn sym]
synth_fns [BoolExpr t]
constraints
  WriterConn t (Writer CVC5_SyGuS) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeExit WriterConn t (Writer CVC5_SyGuS)
writer

writeSyGuSProblem ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  WriterConn t (SMT2.Writer CVC5_SyGuS) ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO ()
writeSyGuSProblem :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t (Writer CVC5_SyGuS)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
writeSyGuSProblem sym
sym WriterConn t (Writer CVC5_SyGuS)
writer [SomeSymFn sym]
synth_fns [BoolExpr t]
constraints = do
  (SomeSymFn sym -> IO ()) -> [SomeSymFn sym] -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(SomeSymFn SymFn sym args ret
fn) -> WriterConn t (Writer CVC5_SyGuS) -> ExprSymFn t args ret -> IO ()
forall h t (args :: Ctx BaseType) (ret :: BaseType).
SMTWriter h =>
WriterConn t h -> ExprSymFn t args ret -> IO ()
addSynthFun WriterConn t (Writer CVC5_SyGuS)
writer SymFn sym args ret
ExprSymFn t args ret
fn) [SomeSymFn sym]
synth_fns
  (Some (ExprBoundVar t) -> IO ())
-> Set (Some (ExprBoundVar t)) -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((forall (tp :: BaseType). ExprBoundVar t tp -> IO ())
-> Some (ExprBoundVar t) -> IO ()
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome ((forall (tp :: BaseType). ExprBoundVar t tp -> IO ())
 -> Some (ExprBoundVar t) -> IO ())
-> (forall (tp :: BaseType). ExprBoundVar t tp -> IO ())
-> Some (ExprBoundVar t)
-> IO ()
forall a b. (a -> b) -> a -> b
$ WriterConn t (Writer CVC5_SyGuS) -> ExprBoundVar t tp -> IO ()
forall h t (tp :: BaseType).
SMTWriter h =>
WriterConn t h -> ExprBoundVar t tp -> IO ()
addDeclareVar WriterConn t (Writer CVC5_SyGuS)
writer) (Set (Some (ExprBoundVar t)) -> IO ())
-> Set (Some (ExprBoundVar t)) -> IO ()
forall a b. (a -> b) -> a -> b
$ (BoolExpr t -> Set (Some (ExprBoundVar t)))
-> [BoolExpr t] -> Set (Some (ExprBoundVar t))
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (sym -> SymExpr sym BaseBoolType -> Set (Some (BoundVar sym))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
forall (tp :: BaseType).
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
exprUninterpConstants sym
sym) [BoolExpr t]
constraints
  (BoolExpr t -> IO ()) -> [BoolExpr t] -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (WriterConn t (Writer CVC5_SyGuS) -> BoolExpr t -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
addConstraint WriterConn t (Writer CVC5_SyGuS)
writer) [BoolExpr t]
constraints
  WriterConn t (Writer CVC5_SyGuS) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeCheckSynth WriterConn t (Writer CVC5_SyGuS)
writer