content: {-# LANGUAGE CPP #-}
  module SAT(
             SATState,
             initSATState,
             checkBiImplication,
             isConstExpr,
             checkEq,
             checkNotEq,
             checkSATFlags
            ) where
  
  import qualified Control.Exception as CE
  
  import Error(ErrorHandle, bsError, ErrMsg(..))
  import Flags
  import ASyntax
  import Position(cmdPosition)
  
  import qualified AExpr2STP as STP
           (SState, initSState, checkBiImplication, isConstExpr,
            checkEq, checkNotEq)
  import qualified AExpr2Yices as Yices
           (YState, initYState, checkBiImplication, isConstExpr,
            checkEq, checkNotEq)
  
  import STP(checkVersion)
  import Yices(checkVersion)
  
  -- -------------------------
  
  -- A single data type for either of the solver state
  data SATState = SATS_Yices Yices.YState
                | SATS_STP STP.SState
  
  -- -------------------------
  
  initSATState :: String -> ErrorHandle -> Flags -> Bool -> [ADef] -> [AVInst] ->
                  IO SATState
  initSATState str errh flags doHardFail ds avis =
      case (satBackend flags) of
        SAT_Yices -> do
            yices_state <- Yices.initYState str flags doHardFail ds avis []
            return (SATS_Yices yices_state)
        SAT_STP -> do
            stp_state <- STP.initSState str flags doHardFail ds avis []
            return (SATS_STP stp_state)
  
  
  checkSATFlags :: ErrorHandle -> Flags -> IO Flags
  checkSATFlags eh f =
    let
        hasYices :: IO Bool
        hasYices = let handler :: CE.SomeException -> IO Bool
                       handler _ = return False
                   in  CE.catch (Yices.checkVersion >> return True) handler
  
        hasSTP :: IO Bool
        hasSTP = STP.checkVersion
  
        checkFn :: String -> String -> IO Bool -> IO Flags
        checkFn flag_str lib_str hasFn = do
          res <- hasFn
          if res
            then return f
            else -- Rather than defaulting to another solver,
                 -- just report an error
                 bsError eh [(cmdPosition,
                              WSATNotAvailable flag_str lib_str Nothing)]
    in  case (satBackend f) of
          SAT_Yices -> checkFn "-sat-yices" "libyices.so.2" hasYices
          SAT_STP -> checkFn "-sat-stp" "libstp.so" hasSTP
  
  -- -------------------------
  
  checkBiImplication :: SATState -> AExpr -> AExpr -> IO ((Bool, Bool), SATState)
  checkBiImplication (SATS_Yices yices_state) e1 e2 = do
      (res, yices_state') <- Yices.checkBiImplication yices_state e1 e2
      return (res, SATS_Yices yices_state')
  checkBiImplication (SATS_STP stp_state) e1 e2 = do
      (res, stp_state') <- STP.checkBiImplication stp_state e1 e2
      return (res, SATS_STP stp_state')
  
  
  isConstExpr :: SATState -> AExpr -> IO (Maybe Bool, SATState)
  isConstExpr (SATS_Yices yices_state) e = do
      (res, yices_state') <- Yices.isConstExpr yices_state e
      return (res, SATS_Yices yices_state')
  isConstExpr (SATS_STP stp_state) e = do
      (res, stp_state') <- STP.isConstExpr stp_state e
      return (res, SATS_STP stp_state')
  
  
  checkEq :: SATState -> AExpr -> AExpr -> IO (Maybe Bool, SATState)
  checkEq (SATS_Yices yices_state) e1 e2 = do
      (res, yices_state') <- Yices.checkEq yices_state e1 e2
      return (res, SATS_Yices yices_state')
  checkEq (SATS_STP stp_state) e1 e2 = do
      (res, stp_state') <- STP.checkEq stp_state e1 e2
      return (res, SATS_STP stp_state')
  
  
  checkNotEq :: SATState -> AExpr -> AExpr -> IO (Maybe Bool, SATState)
  checkNotEq (SATS_Yices yices_state) e1 e2 = do
      (res, yices_state') <- Yices.checkNotEq yices_state e1 e2
      return (res, SATS_Yices yices_state')
  checkNotEq (SATS_STP stp_state) e1 e2 = do
      (res, stp_state') <- STP.checkNotEq stp_state e1 e2
      return (res, SATS_STP stp_state')
  
  -- -------------------------
  