SMTComparison.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
{- |
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.foldWithKey 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.foldWithKey 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, ")"])
-}