module SATPred(
  SATPredState,
  initSATPredState,
  solvePred
  ) where

import Flags
import Pred

import qualified Pred2STP as STP
         (SState, initSState, solvePred)
import qualified Pred2Yices as Yices
         (YState, initYState, solvePred)

-- -------------------------

-- A single data type for any of the solver state
-- For now, we always use STP for this
data SATPredState =
           SATPredS_STP STP.SState
         | SATPredS_Yices Yices.YState

-- -------------------------

initSATPredState :: Flags -> IO SATPredState
initSATPredState flags = do
    case (satBackend flags) of
      SAT_STP -> do
        stp_state <- STP.initSState
        return (SATPredS_STP stp_state)
      SAT_Yices -> do
        yices_state <- Yices.initYState
        return (SATPredS_Yices yices_state)

-- -------------------------

{-
checkPreds :: SATPredState -> [Pred] -> IO ([EMsg], SATPredState)
checkPreds (SATPredS_STP stp_state) ps = do
    (res, stp_state') <- STP.checkPreds stp_state ps
    return (res, SATPredS_STP stp_state')
checkPreds (SATPredS_Yices yices_state) ps = do
    (res, yices_state') <- Yices.checkPreds yices_state ps
    return (res, SATPredS_Yices yices_state')
-}

-- -------------------------

solvePred :: SATPredState -> [Pred] -> Pred -> IO (Maybe Pred, SATPredState)
solvePred (SATPredS_STP stp_state) ps p = do
    (res, stp_state') <- STP.solvePred stp_state ps p
    return (res, SATPredS_STP stp_state')
solvePred (SATPredS_Yices yices_state) ps p = do
    (res, yices_state') <- Yices.solvePred yices_state ps p
    return (res, SATPredS_Yices yices_state')

-- -------------------------