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

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{smtLibVersion} = case smtLibVersion of
                                      SMTLib2 -> toSMTLib2

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

-- | Convert to SMTLib-2 format
toSMTLib2 :: SMTLibConverter SMTLibPgm
toSMTLib2 = cvt SMTLib2
  where cvt v ctx kindInfo isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out config
         | KUnbounded `Set.member` kindInfo && not (supportsUnboundedInts solverCaps)
         = unsupported "unbounded integers"
         | KReal `Set.member` kindInfo  && not (supportsReals solverCaps)
         = unsupported "algebraic reals"
         | (needsFloats || needsDoubles) && not (supportsIEEE754 solverCaps)
         = unsupported "floating-point numbers"
         | needsQuantifiers && not (supportsQuantifiers solverCaps)
         = unsupported "quantifiers"
         | not (null sorts) && not (supportsUninterpretedSorts solverCaps)
         = unsupported "uninterpreted sorts"
         | True
         = SMTLibPgm v pgm
         where sorts = [s | KUninterpreted s _ <- Set.toList kindInfo]
               solverCaps = capabilities (solver config)
               unsupported w = error $ unlines [ "SBV: Given problem needs " ++ w
                                               , "*** Which is not supported by SBV for the chosen solver: " ++ show (name (solver config))
                                               ]
               converter = case v of
                             SMTLib2 -> SMT2.cvt
               pgm = converter ctx kindInfo isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out config

               needsFloats  = KFloat  `Set.member` kindInfo
               needsDoubles = KDouble `Set.member` kindInfo
               needsQuantifiers
                 | isSat = ALL `elem` quantifiers
                 | True  = EX  `elem` quantifiers
                 where quantifiers = map fst (fst qinps)

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