faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian Maeder{- |

faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian MaederModule : $Header$

faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian MaederDescription : SMT interface for set comparison

faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian MaederCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010

faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

aa1c971871ba8f793a9e2e62189369cbfbbe0054Christian Maeder

9db48b4604636bfdf03e60890fc094b7bec775dcChristian MaederMaintainer : ewaryst.schulz@dfki.de

9db48b4604636bfdf03e60890fc094b7bec775dcChristian MaederStability : experimental

9db48b4604636bfdf03e60890fc094b7bec775dcChristian MaederPortability : portable

faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian Maeder

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 where

import Control.Monad

import qualified Data.Map as Map

import Data.List

import System.Process

import CSL.TreePO

import CSL.EPBasic

-- ----------------------------------------------------------------------

-- * 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 }

-- | 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, ")"])

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 = concat $ map (" "++) $ smtVars m "x"

in concat ["(assert+ (not (", s, " (", a, vl, ") (", b, vl, "))))"]

smtEQStmt :: VarEnv -> String -> String -> String

smtEQStmt m a b = smtGenericStmt m "=" a b

smtLEStmt :: VarEnv -> String -> String -> String

smtLEStmt m a b = smtGenericStmt m "=>" a b

smtDisjStmt :: VarEnv -> String -> String -> String

smtDisjStmt m a b =

let vl = concat $ map (" "++) $ 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)" ]

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)"]

]

smtScriptHead :: VarEnv -> BoolRep -> BoolRep -> String

smtScriptHead = smtScriptHead'

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

data SMTStatus = Sat | Unsat deriving (Show, Eq)

smtCheck :: VarEnv -> BoolRep -> BoolRep -> IO [SMTStatus]

smtCheck m r1 r2 = smtMultiResponse $ smtAllScript m r1 r2

smtCheck' :: VarEnv -> BoolRep -> BoolRep -> IO [SMTStatus]

smtCheck' m r1 r2 = mapM smtResponse $ smtAllScripts 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] -> (EPCompare, 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

tripleFst :: (a, b, c) -> a

tripleFst (x, _, _) = x

smtCompare :: VarEnv -> BoolRep -> BoolRep -> IO (EPCompare, 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"

smtMultiResponse :: String -> IO [SMTStatus]

smtMultiResponse inp = do

-- putStrLn $ "\n\n" ++ inp ++ "\n\n\n\n\n\n\n\n\n\n"

s <- readProcess "yices" [] inp

-- putStrLn "---------------- DONE ----------------\n\n"

return $ map smtResponseToStatus $ lines s

smtResponse :: String -> IO SMTStatus

smtResponse inp = do

s <- readProcess "yices" [] inp

-- putStrLn "------ yices output ------"

-- putStrLn s

return $ smtResponseToStatus $

case lines s of

[] -> ""

x:_ -> x

-- * 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]