    -----------------------------------------------------------------------------
    -- |
    -- 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 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 :: SMTLibVersion
    smtLibVersion :: SMTConfig -> SMTLibVersion
    smtLibVersion} = case SMTLibVersion
    smtLibVersion of
                                          SMTLibVersion
    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 :: SMTConfig -> SMTLibVersion
    smtLibVersion :: SMTLibVersion
    smtLibVersion} = case SMTLibVersion
    smtLibVersion of
                                             SMTLibVersion
    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 SMTLibVersion
    v QueryContext
    ctx ProgInfo
    progInfo Set Kind
    kindInfo Bool
    isSat [String]
    comments ResultInp
    qinps (CnstMap, [(SV, CV)])
    consts [((Int, Kind, Kind), [SV])]
    tbls [(Int, ArrayInfo)]
    arrs [(String, (Maybe [String], SBVType))]
    uis [SMTDef]
    axs SBVPgm
    asgnsSeq Seq (Bool, [(String, String)], SV)
    cstrs SV
    out SMTConfig
    config = SMTLibVersion -> [String] -> SMTLibPgm
    SMTLibPgm SMTLibVersion
    v [String]
    pgm
             where converter :: SMTLibConverter [String]
    converter = case SMTLibVersion
    v of
                                 SMTLibVersion
    SMTLib2 -> SMTLibConverter [String]
    SMT2.cvt
                   pgm :: [String]
    pgm = SMTLibConverter [String]
    converter QueryContext
    ctx ProgInfo
    progInfo Set Kind
    kindInfo Bool
    isSat [String]
    comments ResultInp
    qinps (CnstMap, [(SV, CV)])
    consts [((Int, Kind, Kind), [SV])]
    tbls [(Int, ArrayInfo)]
    arrs [(String, (Maybe [String], SBVType))]
    uis [SMTDef]
    axs SBVPgm
    asgnsSeq Seq (Bool, [(String, String)], SV)
    cstrs SV
    out SMTConfig
    config

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