module Data.SBV.Provers.Yices(yices, timeout) where
import Control.Monad (foldM)
import Data.Char (isDigit)
import Data.List (sortBy, isPrefixOf)
import System.Environment (getEnv)
import Data.SBV.BitVectors.Data
import Data.SBV.Provers.SExpr
import Data.SBV.SMT.SMT
yices :: SMTSolver
yices = SMTSolver {
name = "Yices"
, executable = "yices"
, options = ["-m", "-f"]
, engine = \cfg inps pgm -> do
execName <- getEnv "SBV_YICES" `catch` (\_ -> return (executable (solver cfg)))
execOpts <- (words `fmap` (getEnv "SBV_YICES_OPTIONS")) `catch` (\_ -> return (options (solver cfg)))
let cfg' = cfg { solver = (solver cfg) {executable = execName, options = execOpts} }
standardSolver cfg' pgm (ProofError cfg) (interpret cfg inps)
}
timeout :: Int -> SMTSolver -> SMTSolver
timeout n s
| n <= 0 = error $ "Yices.timeout value should be > 0, received: " ++ show n
| True = s{options = options s ++ ["-t", show n]}
sortByNodeId :: [(Int, a)] -> [(Int, a)]
sortByNodeId = sortBy (\(x, _) (y, _) -> compare x y)
interpret :: SMTConfig -> [NamedSymVar] -> [String] -> SMTResult
interpret cfg _ ("unsat":_) = Unsatisfiable cfg
interpret cfg inps ("unknown":rest) = Unknown cfg $ extractMap inps rest
interpret cfg inps ("sat":rest) = Satisfiable cfg $ extractMap inps rest
interpret cfg _ ("timeout":_) = TimeOut cfg
interpret cfg _ ls = ProofError cfg $ ls
extractMap :: [NamedSymVar] -> [String] -> SMTModel
extractMap inps solverLines =
SMTModel { modelAssocs = map (\(_, y) -> y) $ sortByNodeId $ concatMap (getCounterExample inps) modelLines
, modelUninterps = extractUnints unintLines
}
where (modelLines, unintLines) = break ("--- uninterpreted_" `isPrefixOf`) solverLines
getCounterExample :: [NamedSymVar] -> String -> [(Int, (String, CW))]
getCounterExample inps line
| isComment line = []
| True = either err extract (parseSExpr line)
where err r = error $ "*** Failed to parse Yices model output from: "
++ "*** " ++ show line ++ "\n"
++ "*** Reason: " ++ r ++ "\n"
isInput ('s':v)
| all isDigit v = let inpId :: Int
inpId = read v
in case [(s, nm) | (s@(SW _ (NodeId n)), nm) <- inps, n == inpId] of
[] -> Nothing
[(s, nm)] -> Just (inpId, s, nm)
matches -> error $ "SBV.Yices: Cannot uniquely identify value for "
++ 's':v ++ " in " ++ show matches
isInput _ = Nothing
extract (S_App [S_Con "=", S_Con v, S_Num i]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (hasSign s, sizeOf s) i))]
extract (S_App [S_Con "=", S_Num i, S_Con v]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (hasSign s, sizeOf s) i))]
extract _ = []
isComment :: String -> Bool
isComment s = any (`isPrefixOf` s) prefixes
where prefixes = ["---", "default"]
extractUnints :: [String] -> [(String, [String])]
extractUnints [] = []
extractUnints xs = case extractUnint first of
Nothing -> extractUnints rest
Just x -> x : extractUnints rest
where first = takeWhile p xs
rest = tail' (dropWhile p xs)
p = not . ("----" `isPrefixOf`)
tail' [] = []
tail' (_ : rs) = rs
extractUnint :: [String] -> Maybe (String, [String])
extractUnint [] = Nothing
extractUnint (tag : rest)
| null tag' = Nothing
| True = foldM (getUIVal f) (0, []) rest >>= \(_, xs) -> return (f, reverse xs)
where tag' = dropWhile (/= '_') tag
f = takeWhile (/= ' ') (tail tag')
getUIVal :: String -> (Int, [String]) -> String -> Maybe (Int, [String])
getUIVal f (cnt, sofar) s
| "default: " `isPrefixOf` s
= getDefaultVal cnt f (dropWhile (/= ' ') s) >>= \d -> return (cnt, d : sofar)
| True
= case parseSExpr s of
Right (S_App [S_Con "=", (S_App (S_Con v : args)), S_Num i]) | v == "uninterpreted_" ++ f
-> getCallVal cnt f args i >>= \(cnt', d) -> return (cnt', d : sofar)
_ -> Nothing
getDefaultVal :: Int -> String -> String -> Maybe String
getDefaultVal cnt f n = case parseSExpr n of
Right (S_Num i) -> Just $ f ++ " " ++ unwords (replicate cnt "_") ++ " = " ++ show i
_ -> Nothing
getCallVal :: Int -> String -> [SExpr] -> Integer -> Maybe (Int, String)
getCallVal cnt f args res = mapM getArg args >>= \as -> return (cnt `max` length as, f ++ " " ++ unwords as ++ " = " ++ show res)
getArg :: SExpr -> Maybe String
getArg (S_Num i) = Just (show i)
getArg _ = Nothing