module Hsmtlib.Solvers.Cmd.Parser.CmdResult where
import Control.Applicative ((<|>),(<$>))
import Control.Monad
import Data.List (intercalate)
import Data.Map as M
import Data.Maybe (isJust)
import Hsmtlib.Solver as Solv
import Hsmtlib.Solvers.Cmd.Parser.Parsers hiding (numeral, symbol)
import Hsmtlib.Solvers.Cmd.Parser.Syntax as S
import Hsmtlib.Solvers.Cmd.Parser.Visualizers
import Prelude as P
import Text.ParserCombinators.Parsec.Prim (parse)
genResponse :: String -> GenResult
genResponse stg =
case result of
Left err -> Solv.GUError $ show err
Right cmdRep -> case cmdRep of
CmdGenResponse S.Success -> Solv.Success
CmdGenResponse S.Unsupported -> Solv.Unsupported
CmdGenResponse (S.Error err) -> Solv.Error err
where result = parse parseCmdGenResponse "" stg
checkSatResponse :: String -> SatResult
checkSatResponse stg =
case result of
Left err -> Solv.SUError $ show err
Right cmdRep -> case cmdRep of
S.Sat -> Solv.Sat
S.Unsat -> Solv.Unsat
S.Unknown -> Solv.Unknown
where result = parse parseCheckSatResponse "" stg
getValueResponse :: String -> GValResult
getValueResponse stg = case result of
Left err -> GVUError $ stg ++ "|"++show err
Right vals -> getVR' $ getValResponse vals
where result = parse parseGetValueResponse "" stg
getVR' :: [GValResult] -> GValResult
getVR' xs | length xs == 1 = head xs
| otherwise = Results xs
getValResponse::[ValuationPair] -> [GValResult]
getValResponse vp = arrays ++ errors
where res = getValResponses vp
errors = valErrors' vp res
cRes = P.filter isJust res
arrays = joinArrays cRes
valErrors' :: [ValuationPair] -> [Maybe GValResult] -> [GValResult]
valErrors' [] [] = []
valErrors' (x:xs) (Nothing:gs) =
GVUError (showValuationPair 0 x) : valErrors' xs gs
valErrors' (_:xs) (_:gs) = valErrors' xs gs
joinArrays :: [Maybe GValResult] -> [GValResult]
joinArrays = joinArrays' $ VArrays empty
joinArrays' :: GValResult -> [Maybe GValResult] -> [GValResult]
joinArrays' (VArrays n) [] | M.null n = []
| otherwise = [VArrays n]
joinArrays' res (x:xs) = case nVal of
(VArrays _) -> joinArrays' nVal xs
_ -> nVal : joinArrays' res xs
where nVal = checkGVal res x
checkGVal :: GValResult -> Maybe GValResult -> GValResult
checkGVal (VArrays oarr) (Just(VArrays arr)) =
VArrays $ unionWith union oarr arr
checkGVal _ (Just x) = x
getValResponses :: [ValuationPair] -> [Maybe GValResult]
getValResponses = fmap getGValResult
getGValResult :: ValuationPair -> Maybe GValResult
getGValResult vp = getVar vp
<|> getArray vp
<|> getFun vp
<|> getBitVec vp
getBitVec :: ValuationPair -> Maybe GValResult
getBitVec vp = getBitVec' name vhex
where name = getVarName vp
vhex = getHexVal vp
getBitVec' :: Maybe String -> Maybe String -> Maybe GValResult
getBitVec' (Just name) (Just vhex) = Just $ Res name $ VHex vhex
getBitVec' _ _ = Nothing
getFun :: ValuationPair -> Maybe GValResult
getFun vp = getFun' name value
where name = getFunName vp
value = getFunResult vp
getFun' :: Maybe String -> Maybe Value -> Maybe GValResult
getFun' (Just name) (Just res) = Just $ Res name res
getFun' _ _ = Nothing
getVar :: ValuationPair -> Maybe GValResult
getVar vp = getVar' name value
where name = getVarName vp
value = getVarValue vp
getVar' :: Maybe String -> Maybe Integer -> Maybe GValResult
getVar' Nothing _ = Nothing
getVar' _ Nothing = Nothing
getVar' (Just name) (Just value) = Just $ Res name $ VInt value
getArray :: ValuationPair -> Maybe GValResult
getArray vp =
case isArr of
Nothing -> Nothing
Just _ -> case res of
Just arr -> Just $ VArrays arr
Nothing -> Nothing
where name = arrayName vp
posInt = arrayIntPos vp
posVar = arrayVarPos vp
val = arrayVal vp
isArr = isArray vp
res = getArray' name posInt posVar val
getArray' :: Maybe String
-> Maybe Integer
-> Maybe String
-> Maybe Integer
-> Maybe Arrays
getArray' (Just name) (Just pos) Nothing (Just val) =
Just $ singleton name $ singleton (show pos) val
getArray' (Just name) Nothing (Just pos) (Just val) =
Just $ singleton name $ singleton pos val
getArray' _ _ _ _ = Nothing
isArray :: ValuationPair -> Maybe Bool
isArray = isArray'
<=< symbol
<=< qIdentifier
<=< fstTermQualIdentierT
<=< fstTerm
isArray' :: String -> Maybe Bool
isArray' "select" = Just True
isArray' _ = Nothing
arrayName :: ValuationPair -> Maybe String
arrayName = symbol
<=< qIdentifier
<=< termQualIdentifier
<=< fstValArray
<=< sndTermQualIdentierT
<=< fstTerm
where fstValArray x = Just $ head x
arrayIntPos :: ValuationPair -> Maybe Integer
arrayIntPos = numeral
<=< getTermSpecConstant
<=< sndValArray
<=< sndTermQualIdentierT
<=< fstTerm
where sndValArray x = Just $ x !! 1
arrayVarPos :: ValuationPair -> Maybe String
arrayVarPos = symbol
<=< qIdentifier
<=< termQualIdentifier
<=< sndValArray
<=< sndTermQualIdentierT
<=< fstTerm
where sndValArray x = Just $ x !! 1
arrayVal :: ValuationPair -> Maybe Integer
arrayVal = numeral <=< getTermSpecConstant <=< sndTerm
getVarName :: ValuationPair -> Maybe String
getVarName = symbol <=< qIdentifier <=< termQualIdentifier <=< fstTerm
getVarValue :: ValuationPair -> Maybe Integer
getVarValue = numeral <=< getTermSpecConstant <=< sndTerm
getFunName :: ValuationPair -> Maybe String
getFunName = symbol <=< qIdentifier <=< fstTermQualIdentierT <=< fstTerm
getFunResult :: ValuationPair -> Maybe Value
getFunResult vp = getFunResultBool vp <|> getFunResultInt vp
getFunResultBool :: ValuationPair -> Maybe Value
getFunResultBool = VBool <#> toBool <=< getFunResultBool'
getFunResultInt :: ValuationPair -> Maybe Value
getFunResultInt = VInt <#> getFunResultInt'
(<#>):: Functor m => (b -> c) -> (a -> m b) -> a -> m c
(<#>) f m = \x -> f <$> m x
toBool :: String -> Maybe Bool
toBool "true" = Just True
toBool "false" = Just False
toBool _ = Nothing
getFunResultInt' :: ValuationPair -> Maybe Integer
getFunResultInt' = numeral <=< getTermSpecConstant <=< sndTerm
getFunResultBool' :: ValuationPair -> Maybe String
getFunResultBool' = symbol <=< qIdentifier <=< termQualIdentifier <=< sndTerm
getHexVal :: ValuationPair -> Maybe String
getHexVal = hex <=< getTermSpecConstant <=< fstTerm
fstTerm :: ValuationPair -> Maybe Term
fstTerm (ValuationPair a _) = Just a
sndTerm :: ValuationPair -> Maybe Term
sndTerm (ValuationPair _ b) = Just b
sndTermQualIdentierT :: Term -> Maybe [Term]
sndTermQualIdentierT (TermQualIdentifierT _ ts) = Just ts
sndTermQualIdentierT _ = Nothing
fstTermQualIdentierT :: Term -> Maybe QualIdentifier
fstTermQualIdentierT (TermQualIdentifierT qi _) = Just qi
fstTermQualIdentierT _ = Nothing
termQualIdentifier :: Term -> Maybe QualIdentifier
termQualIdentifier (TermQualIdentifier a) = Just a
termQualIdentifier _ = Nothing
getTermSpecConstant :: Term -> Maybe SpecConstant
getTermSpecConstant (TermSpecConstant spc) = Just spc
getTermSpecConstant _ = Nothing
qIdentifier :: QualIdentifier -> Maybe Identifier
qIdentifier (QIdentifier a) = Just a
qIdentifier _ = Nothing
symbol :: Identifier -> Maybe String
symbol (ISymbol s) = Just s
symbol _ = Nothing
numeral :: SpecConstant -> Maybe Integer
numeral (SpecConstantNumeral n) = Just n
numeral _ = Nothing
hex :: SpecConstant -> Maybe String
hex (SpecConstantHexadecimal shex) = Just shex
hex _ = Nothing