-----------------------------------------------------------------------------
-- |
-- 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
import           Data.Text            (Text)

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

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