    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.SMT.SMTLib
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Conversion of symbolic programs to SMTLib format
    -----------------------------------------------------------------------------

    {-# LANGUAGE NamedFieldPuns #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.SMT.SMTLib (
              SMTLibPgm
            , toSMTLib
            , toIncSMTLib
            ) where

    import qualified Data.Set as Set (member, toList)

    import Data.SBV.Core.Data

    import Data.SBV.SMT.Utils
    import qualified Data.SBV.SMT.SMTLib2 as SMT2

    -- | Convert to SMT-Lib, in a full program context.
    toSMTLib :: SMTConfig -> SMTLibConverter SMTLibPgm
    toSMTLib :: SMTConfig -> SMTLibConverter SMTLibPgm
    toSMTLib SMTConfig{SMTLibVersion
    smtLibVersion :: SMTConfig -> SMTLibVersion
    smtLibVersion :: SMTLibVersion
    smtLibVersion} = case SMTLibVersion
    smtLibVersion of
                                          SMTLib2 -> SMTLibConverter SMTLibPgm
    toSMTLib2

    -- | Convert to SMT-Lib, in an incremental query context.
    toIncSMTLib :: SMTConfig -> SMTLibIncConverter [String]
    toIncSMTLib :: SMTConfig -> SMTLibIncConverter [String]
    toIncSMTLib SMTConfig{SMTLibVersion
    smtLibVersion :: SMTLibVersion
    smtLibVersion :: SMTConfig -> SMTLibVersion
    smtLibVersion} = case SMTLibVersion
    smtLibVersion of
                                             SMTLib2 -> SMTLibIncConverter [String]
    toIncSMTLib2

    -- | Convert to SMTLib-2 format
    toSMTLib2 :: SMTLibConverter SMTLibPgm
    toSMTLib2 :: SMTLibConverter SMTLibPgm
    toSMTLib2 = SMTLibVersion -> SMTLibConverter SMTLibPgm
    cvt SMTLibVersion
    SMTLib2
      where cvt :: SMTLibVersion -> SMTLibConverter SMTLibPgm
    cvt v :: SMTLibVersion
    v ctx :: QueryContext
    ctx kindInfo :: Set Kind
    kindInfo isSat :: Bool
    isSat comments :: [String]
    comments qinps :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
    qinps skolemMap :: [Either SV (SV, [SV])]
    skolemMap consts :: [(SV, CV)]
    consts tbls :: [((Int, Kind, Kind), [SV])]
    tbls arrs :: [(Int, ArrayInfo)]
    arrs uis :: [(String, SBVType)]
    uis axs :: [(String, [String])]
    axs asgnsSeq :: SBVPgm
    asgnsSeq cstrs :: Seq (Bool, [(String, String)], SV)
    cstrs out :: SV
    out config :: SMTConfig
    config
             | Kind
    KUnbounded Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo Bool -> Bool -> Bool
    && Bool -> Bool
    not (SolverCapabilities -> Bool
    supportsUnboundedInts SolverCapabilities
    solverCaps)
             = String -> SMTLibPgm
    forall a. String -> a
    unsupported "unbounded integers"
             | Kind
    KReal Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo  Bool -> Bool -> Bool
    && Bool -> Bool
    not (SolverCapabilities -> Bool
    supportsReals SolverCapabilities
    solverCaps)
             = String -> SMTLibPgm
    forall a. String -> a
    unsupported "algebraic reals"
             | (Bool
    needsFloats Bool -> Bool -> Bool
    || Bool
    needsDoubles) Bool -> Bool -> Bool
    && Bool -> Bool
    not (SolverCapabilities -> Bool
    supportsIEEE754 SolverCapabilities
    solverCaps)
             = String -> SMTLibPgm
    forall a. String -> a
    unsupported "floating-point numbers"
             | Bool
    needsQuantifiers Bool -> Bool -> Bool
    && Bool -> Bool
    not (SolverCapabilities -> Bool
    supportsQuantifiers SolverCapabilities
    solverCaps)
             = String -> SMTLibPgm
    forall a. String -> a
    unsupported "quantifiers"
             | Bool -> Bool
    not ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    sorts) Bool -> Bool -> Bool
    && Bool -> Bool
    not (SolverCapabilities -> Bool
    supportsUninterpretedSorts SolverCapabilities
    solverCaps)
             = String -> SMTLibPgm
    forall a. String -> a
    unsupported "uninterpreted sorts"
             | Bool
    True
             = SMTLibVersion -> [String] -> SMTLibPgm
    SMTLibPgm SMTLibVersion
    v [String]
    pgm
             where sorts :: [String]
    sorts = [String
    s | KUninterpreted s :: String
    s _ <- Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    kindInfo]
                   solverCaps :: SolverCapabilities
    solverCaps = SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    config)
                   unsupported :: String -> a
    unsupported w :: String
    w = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ "SBV: Given problem needs " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    w
                                                   , "*** Which is not supported by SBV for the chosen solver: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Solver -> String
    forall a. Show a => a -> String
    show (SMTSolver -> Solver
    name (SMTConfig -> SMTSolver
    solver SMTConfig
    config))
                                                   ]
                   converter :: SMTLibConverter [String]
    converter = case SMTLibVersion
    v of
                                 SMTLib2 -> SMTLibConverter [String]
    SMT2.cvt
                   pgm :: [String]
    pgm = SMTLibConverter [String]
    converter QueryContext
    ctx Set Kind
    kindInfo Bool
    isSat [String]
    comments ([(Quantifier, NamedSymVar)], [NamedSymVar])
    qinps [Either SV (SV, [SV])]
    skolemMap [(SV, CV)]
    consts [((Int, Kind, Kind), [SV])]
    tbls [(Int, ArrayInfo)]
    arrs [(String, SBVType)]
    uis [(String, [String])]
    axs SBVPgm
    asgnsSeq Seq (Bool, [(String, String)], SV)
    cstrs SV
    out SMTConfig
    config

                   needsFloats :: Bool
    needsFloats  = Kind
    KFloat  Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
                   needsDoubles :: Bool
    needsDoubles = Kind
    KDouble Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
                   needsQuantifiers :: Bool
    needsQuantifiers
                     | Bool
    isSat = Quantifier
    ALL Quantifier -> [Quantifier] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Quantifier]
    quantifiers
                     | Bool
    True  = Quantifier
    EX  Quantifier -> [Quantifier] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Quantifier]
    quantifiers
                     where quantifiers :: [Quantifier]
    quantifiers = ((Quantifier, NamedSymVar) -> Quantifier)
    -> [(Quantifier, NamedSymVar)] -> [Quantifier]
    forall a b. (a -> b) -> [a] -> [b]
    map (Quantifier, NamedSymVar) -> Quantifier
    forall a b. (a, b) -> a
    fst (([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> [(Quantifier, NamedSymVar)]
    forall a b. (a, b) -> a
    fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
    qinps)

    -- | Convert to SMTLib-2 format
    toIncSMTLib2 :: SMTLibIncConverter [String]
    toIncSMTLib2 :: SMTLibIncConverter [String]
    toIncSMTLib2 = SMTLibVersion -> SMTLibIncConverter [String]
    cvt SMTLibVersion
    SMTLib2
      where cvt :: SMTLibVersion -> SMTLibIncConverter [String]
    cvt SMTLib2 = SMTLibIncConverter [String]
    SMT2.cvtInc