content: {- |
  Module      :  ./CSL/SMTComparison.hs
  Description :  SMT interface for set comparison
  Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  ewaryst.schulz@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  This module defines an interface to the SMT solver yices for solving comparison
  requests for integer sets defined by the usual boolean operations on the usual
  comparison predicates.
  
  The yices input is generated by producing input text files in yices format,
  see http://yices.csl.sri.com/language.shtml for the syntax description.
  
  There is also the yices-easy hackage entry which uses the C-API of yices.
  This could be an alternative if speed and robustness will be a problem.
  -}
  
  module CSL.SMTComparison
      ( smtCompare
      , smtCheck
      , VarEnv (..)
      , VarMap
      ) where
  
  
  import Control.Monad
  import qualified Data.Map as Map
  import Data.List
  import System.IO
  import System.Process
  
  import CSL.TreePO
  import CSL.BoolBasic
  
  {- ----------------------------------------------------------------------
  SMT output generation for SMT based comparison
  ---------------------------------------------------------------------- -}
  
  {- | This maps are assumed to have distinct values in [1..Map.size varmap],
  i.e., v::VarMap => Set.fromList (Map.elems v) = {1..Map.size v} -}
  type VarMap = Map.Map String Int
  
  type VarTypes = Map.Map String BoolRep
  
  data VarEnv = VarEnv { varmap :: VarMap
                       , vartypes :: VarTypes
                       , loghandle :: Maybe Handle }
  
  smtVars :: VarEnv -> String -> [String]
  smtVars m s = smtGenericVars m ((s ++) . show)
  
  smtGenericVars :: VarEnv -> (Int -> a) -> [a]
  smtGenericVars m f = map f [1 .. Map.size $ varmap m]
  
  smtGenericStmt :: VarEnv -> String -> String -> String -> String
  smtGenericStmt m s a b =
      let vl = concatMap (" " ++) $ smtVars m "x"
      in concat ["(assert+ (not (", s, " (", a, vl, ") (", b, vl, "))))"]
  
  smtEQStmt :: VarEnv -> String -> String -> String
  smtEQStmt m = smtGenericStmt m "="
  
  smtLEStmt :: VarEnv -> String -> String -> String
  smtLEStmt m = smtGenericStmt m "=>"
  
  smtDisjStmt :: VarEnv -> String -> String -> String
  smtDisjStmt m a b =
      let vl = concatMap (" " ++) $ smtVars m "x"
      in concat ["(assert+ (and (", a, vl, ") (", b, vl, ")))"]
  
  
  smtAllScript :: VarEnv -> BoolRep -> BoolRep -> String
  smtAllScript m r1 r2 =
      unlines [ smtScriptHead m r1 r2
              , smtEQStmt m "A" "B", "(check) (retract 1)"
              , smtLEStmt m "A" "B", "(check) (retract 2)"
              , smtLEStmt m "B" "A", "(check) (retract 3)"
              , smtDisjStmt m "A" "B", "(check)" ]
  
  
  smtScriptHead :: VarEnv -> BoolRep -> BoolRep -> String
  smtScriptHead = smtScriptHead'
  
  
  data SMTStatus = Sat | Unsat deriving (Show, Eq)
  
  smtCheck :: VarEnv -> BoolRep -> BoolRep -> IO [SMTStatus]
  smtCheck m r1 r2 = smtMultiResponse (loghandle m) $ smtAllScript m r1 r2
  
  {- | The result states of the smt solver are translated to the
  adequate compare outcome. The boolean value is true if the corresponding
  set is empty. -}
  smtStatusCompareTable :: [SMTStatus] -> (SetOrdering, Bool, Bool)
  smtStatusCompareTable l =
      case l of
        [Unsat, Unsat, Unsat, x] -> let b = x == Unsat in (Comparable EQ, b, b)
        [Sat, Unsat, Sat, x] -> let b = x == Unsat in (Comparable LT, b, b)
        [Sat, Sat, Unsat, x] -> let b = x == Unsat in (Comparable GT, b, b)
        [Sat, Sat, Sat, Unsat] -> (Incomparable Disjoint, False, False)
        [Sat, Sat, Sat, Sat] -> (Incomparable Overlap, False, False)
        x -> error $ "smtStatusCompareTable: malformed status " ++ show x
  
  smtCompare :: VarEnv -> BoolRep -> BoolRep -> IO (SetOrdering, Bool, Bool)
  smtCompare m r1 r2 = liftM smtStatusCompareTable $ smtCheck m r1 r2
  
  smtResponseToStatus :: String -> SMTStatus
  smtResponseToStatus s
      | s == "sat" = Sat
      | s == "unsat" = Unsat
      | s == "" = Sat
      | isInfixOf "Error" s = error $ "yices-error: " ++ s
      | otherwise = error "unknown yices error"
  
  maybeWrite :: Maybe Handle -> String -> IO ()
  maybeWrite mH s = case mH of
                      Just hdl -> hPutStrLn hdl s
                      _ -> return ()
  
  smtMultiResponse :: Maybe Handle -> String -> IO [SMTStatus]
  smtMultiResponse mH inp = do
    maybeWrite mH $ "---------- Yices input ----------\n" ++ inp
    s <- readProcess "yices" [] inp
    maybeWrite mH $ "---------- Yices raw output ----------\n" ++ s
    return $ map smtResponseToStatus $ lines s
  
  
  -- * Alternative Script Generation (without subtypes)
  
  
  smtScriptHead' :: VarEnv -> BoolRep -> BoolRep -> String
  smtScriptHead' m r1 r2 =
      unlines [ "(set-arith-only! true)"
              , smtPredDef' m "A" r1
              , smtPredDef' m "B" r2
              , smtVarDef' m
              , smtVarConstraint' m
              ]
  
  -- | Predicate definition
  smtPredDef' :: VarEnv -> String -> BoolRep -> String
  smtPredDef' m s b = concat [ "(define ", s, "::(->"
                            , concat $ smtGenericVars m $ const " int"
                            , " bool) (lambda ("
                            , concat $ smtGenericVars m
                                         (\ i -> let j = show i
                                                 in concat [" x", j, "::int"])
                            , ") ", smtBoolExp b, "))" ]
  
  smtVarDef' :: VarEnv -> String
  smtVarDef' m =
      unlines
      $ smtGenericVars m (\ i -> let j = show i
                                 in concat ["(define x", j, "::int)"])
  
  -- | Subtype constraints
  smtVarConstraint' :: VarEnv -> String
  smtVarConstraint' m = h l where
      h [] = ""
      h l' = concat ["(assert (and ", concat l' , "))"]
      l = Map.foldrWithKey f [] $ varmap m
      g k = case Map.lookup k $ vartypes m of
              Just br -> ' ' : smtBoolExp br
              Nothing -> ""
      f k _ l' = case g k of
                  "" -> l'
                  x -> l' ++ [x]
  
  {-
  
  smtAllScripts :: VarEnv -> BoolRep -> BoolRep -> [String]
  smtAllScripts m r1 r2 =
      let h = smtScriptHead m r1 r2
      in [ unlines [h, smtEQStmt m "A" "B", "(check)"]
         , unlines [h, smtLEStmt m "A" "B", "(check)"]
         , unlines [h, smtLEStmt m "B" "A", "(check)"]
         , unlines [h, smtDisjStmt m "A" "B", "(check)"]
         ]
  
  smtCheck' :: VarEnv -> BoolRep -> BoolRep -> IO [SMTStatus]
  smtCheck' m r1 r2 = mapM smtResponse $ smtAllScripts m r1 r2
  
  smtResponse :: String -> IO SMTStatus
  smtResponse inp = do
    s <- readProcess "yices" [] inp
  --  putStrLn "------ yices output ------"
  --  putStrLn s
    return $ smtResponseToStatus $
           case lines s of
             [] -> ""
             x:_ ->  x
  
  
  smtScriptHeadOrig :: VarEnv -> BoolRep -> BoolRep -> String
  smtScriptHeadOrig m r1 r2 =
      unlines [ smtTypeDef m
              , smtPredDef m "A" r1
              , smtPredDef m "B" r2
              , smtVarDef m ]
  
  smtGenericScript :: VarEnv -> (VarEnv -> String -> String -> String)
                   -> BoolRep -> BoolRep -> String
  smtGenericScript m f r1 r2 = smtScriptHead m r1 r2 ++ "\n" ++ f m "A" "B"
  
  smtEQScript :: VarEnv -> BoolRep -> BoolRep -> String
  smtEQScript m r1 r2 = smtGenericScript m smtEQStmt r1 r2
  
  smtLEScript :: VarEnv -> BoolRep -> BoolRep -> String
  smtLEScript m r1 r2 = smtGenericScript m smtLEStmt r1 r2
  
  smtDisjScript :: VarEnv -> BoolRep -> BoolRep -> String
  smtDisjScript m r1 r2 = smtGenericScript m smtDisjStmt r1 r2
  
  -}
  
  {-
  emptyVarEnv :: Maybe Handle -> VarEnv
  emptyVarEnv mHdl =  VarEnv { varmap = Map.empty
                             , vartypes = Map.empty
                             , loghandle = mHdl }
  
  -- | Type alias and subtype definitions for the domain of the extended params
  smtTypeDef :: VarEnv -> String
  smtTypeDef m = Map.foldrWithKey f "" $ varmap m
      where g k a = case Map.lookup k $ vartypes m of
                      Just br ->
                          concat [ "(define-type t", show a, " (subtype (x"
                                 , show a, "::int) ", smtBoolExp br, "))" ]
                      Nothing ->
                          concat [ "(define-type t", show a, " int)" ]
            f k a s = s ++ g k a ++ "\n"
  
  -- | Predicate definition
  smtPredDef :: VarEnv -> String -> BoolRep -> String
  smtPredDef m s b = concat [ "(define ", s, "::(->"
                            , concat $ smtVars m " t"
                            , " bool) (lambda ("
                            , concat $ smtGenericVars m
                                         (\ i -> let j = show i
                                                 in concat [" x", j, "::t", j])
                            , ") ", smtBoolExp b, "))" ]
  
  smtVarDef :: VarEnv -> String
  smtVarDef m =
      unlines
      $ smtGenericVars m (\ i -> let j = show i
                                 in concat ["(define x", j, "::t", j, ")"])
  -}
  