-----------------------------------------------------------------------------
-- |
-- 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 [(String, (Bool, Maybe [String], SBVType))]
uis [(SMTDef, SBVType)]
axs SBVPgm
asgnsSeq Seq (Bool, [(String, String)], SV)
cstrs SV
out SMTConfig
config = SMTLibVersion -> [String] -> [String] -> SMTLibPgm
SMTLibPgm SMTLibVersion
v [String]
pgm [String]
defs
         where converter :: SMTLibConverter ([String], [String])
converter   = case SMTLibVersion
v of
                               SMTLibVersion
SMTLib2 -> SMTLibConverter ([String], [String])
SMT2.cvt
               ([String]
pgm, [String]
defs) = SMTLibConverter ([String], [String])
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 [(SMTDef, SBVType)]
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