{-# 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
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
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
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
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