7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzDescription : SMT interface for set comparison
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzLicense : GPLv2 or higher, see LICENSE.txt
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzMaintainer : ewaryst.schulz@dfki.de
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzStability : experimental
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzPortability : portable
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzThis module defines an interface to the SMT solver yices for solving comparison
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulzrequests for integer sets defined by the usual boolean operations on the usual
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulzcomparison predicates.
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzThe yices input is generated by producing input text files in yices format,
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulzsee http://yices.csl.sri.com/language.shtml for the syntax description.
38fcf05bbfbd232891783fdf7c136f5efa0f095eEwaryst SchulzThere is also the yices-easy hackage entry which uses the C-API of yices.
38fcf05bbfbd232891783fdf7c136f5efa0f095eEwaryst SchulzThis could be an alternative if speed and robustness will be a problem.
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulzimport qualified Data.Map as Map
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederSMT output generation for SMT based comparison
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- | This maps are assumed to have distinct values in [1..Map.size varmap],
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederi.e., v::VarMap => Set.fromList (Map.elems v) = {1..Map.size v} -}
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulztype VarMap = Map.Map String Int
5815bdce64892624676670501231b62f3d534898Ewaryst Schulztype VarTypes = Map.Map String BoolRep
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulzdata VarEnv = VarEnv { varmap :: VarMap
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst Schulz , vartypes :: VarTypes
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst Schulz , loghandle :: Maybe Handle }
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtVars :: VarEnv -> String -> [String]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersmtVars m s = smtGenericVars m ((s ++) . show)
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtGenericVars :: VarEnv -> (Int -> a) -> [a]
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtGenericVars m f = map f [1 .. Map.size $ varmap m]
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtGenericStmt :: VarEnv -> String -> String -> String -> String
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtGenericStmt m s a b =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let vl = concatMap (" " ++) $ smtVars m "x"
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz in concat ["(assert+ (not (", s, " (", a, vl, ") (", b, vl, "))))"]
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtEQStmt :: VarEnv -> String -> String -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersmtEQStmt m = smtGenericStmt m "="
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtLEStmt :: VarEnv -> String -> String -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersmtLEStmt m = smtGenericStmt m "=>"
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtDisjStmt :: VarEnv -> String -> String -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersmtDisjStmt m a b =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let vl = concatMap (" " ++) $ smtVars m "x"
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz in concat ["(assert+ (and (", a, vl, ") (", b, vl, ")))"]
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtAllScript :: VarEnv -> BoolRep -> BoolRep -> String
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtAllScript m r1 r2 =
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz unlines [ smtScriptHead m r1 r2
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz , smtEQStmt m "A" "B", "(check) (retract 1)"
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz , smtLEStmt m "A" "B", "(check) (retract 2)"
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz , smtLEStmt m "B" "A", "(check) (retract 3)"
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz , smtDisjStmt m "A" "B", "(check)" ]
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtScriptHead :: VarEnv -> BoolRep -> BoolRep -> String
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst SchulzsmtScriptHead = smtScriptHead'
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulzdata SMTStatus = Sat | Unsat deriving (Show, Eq)
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtCheck :: VarEnv -> BoolRep -> BoolRep -> IO [SMTStatus]
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst SchulzsmtCheck m r1 r2 = smtMultiResponse (loghandle m) $ smtAllScript m r1 r2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- | The result states of the smt solver are translated to the
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederadequate compare outcome. The boolean value is true if the corresponding
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederset is empty. -}
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtStatusCompareTable :: [SMTStatus] -> (SetOrdering, Bool, Bool)
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtStatusCompareTable l =
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz [Unsat, Unsat, Unsat, x] -> let b = x == Unsat in (Comparable EQ, b, b)
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz [Sat, Unsat, Sat, x] -> let b = x == Unsat in (Comparable LT, b, b)
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz [Sat, Sat, Unsat, x] -> let b = x == Unsat in (Comparable GT, b, b)
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz [Sat, Sat, Sat, Unsat] -> (Incomparable Disjoint, False, False)
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz [Sat, Sat, Sat, Sat] -> (Incomparable Overlap, False, False)
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz x -> error $ "smtStatusCompareTable: malformed status " ++ show x
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtCompare :: VarEnv -> BoolRep -> BoolRep -> IO (SetOrdering, Bool, Bool)
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtCompare m r1 r2 = liftM smtStatusCompareTable $ smtCheck m r1 r2
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtResponseToStatus :: String -> SMTStatus
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst SchulzsmtResponseToStatus s
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz | s == "sat" = Sat
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz | s == "unsat" = Unsat
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz | s == "" = Sat
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz | isInfixOf "Error" s = error $ "yices-error: " ++ s
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | otherwise = error "unknown yices error"
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst SchulzmaybeWrite :: Maybe Handle -> String -> IO ()
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst SchulzmaybeWrite mH s = case mH of
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst Schulz Just hdl -> hPutStrLn hdl s
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst Schulz _ -> return ()
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst SchulzsmtMultiResponse :: Maybe Handle -> String -> IO [SMTStatus]
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst SchulzsmtMultiResponse mH inp = do
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst Schulz maybeWrite mH $ "---------- Yices input ----------\n" ++ inp
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz s <- readProcess "yices" [] inp
365265548c9db5d9743e418aec0c82e65b3e5a51Ewaryst Schulz maybeWrite mH $ "---------- Yices raw output ----------\n" ++ s
7171a8d5453e29a741ff1a77fa5eeb5f0ef323d1Ewaryst Schulz return $ map smtResponseToStatus $ lines s
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz-- * Alternative Script Generation (without subtypes)
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst SchulzsmtScriptHead' :: VarEnv -> BoolRep -> BoolRep -> String
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst SchulzsmtScriptHead' m r1 r2 =
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz unlines [ "(set-arith-only! true)"
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz , smtPredDef' m "A" r1
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz , smtPredDef' m "B" r2
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz , smtVarDef' m
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz , smtVarConstraint' m
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz-- | Predicate definition
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst SchulzsmtPredDef' :: VarEnv -> String -> BoolRep -> String
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst SchulzsmtPredDef' m s b = concat [ "(define ", s, "::(->"
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz , concat $ smtGenericVars m $ const " int"
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz , " bool) (lambda ("
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz , concat $ smtGenericVars m
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz (\ i -> let j = show i
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz in concat [" x", j, "::int"])
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz , ") ", smtBoolExp b, "))" ]
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst SchulzsmtVarDef' :: VarEnv -> String
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst SchulzsmtVarDef' m =
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz $ smtGenericVars m (\ i -> let j = show i
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz in concat ["(define x", j, "::int)"])
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz-- | Subtype constraints
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst SchulzsmtVarConstraint' :: VarEnv -> String
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst SchulzsmtVarConstraint' m = h l where
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz h l' = concat ["(assert (and ", concat l' , "))"]
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz l = Map.foldWithKey f [] $ varmap m
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz g k = case Map.lookup k $ vartypes m of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just br -> ' ' : smtBoolExp br
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz Nothing -> ""
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz f k _ l' = case g k of
50a0d6d602b727c3239bca57bee5bfecbd86857aEwaryst Schulz x -> l' ++ [x]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtAllScripts :: VarEnv -> BoolRep -> BoolRep -> [String]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtAllScripts m r1 r2 =
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz let h = smtScriptHead m r1 r2
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz in [ unlines [h, smtEQStmt m "A" "B", "(check)"]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , unlines [h, smtLEStmt m "A" "B", "(check)"]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , unlines [h, smtLEStmt m "B" "A", "(check)"]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , unlines [h, smtDisjStmt m "A" "B", "(check)"]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtCheck' :: VarEnv -> BoolRep -> BoolRep -> IO [SMTStatus]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtCheck' m r1 r2 = mapM smtResponse $ smtAllScripts m r1 r2
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtResponse :: String -> IO SMTStatus
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtResponse inp = do
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz s <- readProcess "yices" [] inp
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz-- putStrLn "------ yices output ------"
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz return $ smtResponseToStatus $
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz case lines s of
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtScriptHeadOrig :: VarEnv -> BoolRep -> BoolRep -> String
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtScriptHeadOrig m r1 r2 =
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz unlines [ smtTypeDef m
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , smtPredDef m "A" r1
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , smtPredDef m "B" r2
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , smtVarDef m ]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtGenericScript :: VarEnv -> (VarEnv -> String -> String -> String)
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz -> BoolRep -> BoolRep -> String
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtGenericScript m f r1 r2 = smtScriptHead m r1 r2 ++ "\n" ++ f m "A" "B"
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtEQScript :: VarEnv -> BoolRep -> BoolRep -> String
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtEQScript m r1 r2 = smtGenericScript m smtEQStmt r1 r2
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtLEScript :: VarEnv -> BoolRep -> BoolRep -> String
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtLEScript m r1 r2 = smtGenericScript m smtLEStmt r1 r2
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtDisjScript :: VarEnv -> BoolRep -> BoolRep -> String
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtDisjScript m r1 r2 = smtGenericScript m smtDisjStmt r1 r2
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzemptyVarEnv :: Maybe Handle -> VarEnv
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzemptyVarEnv mHdl = VarEnv { varmap = Map.empty
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , loghandle = mHdl }
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz-- | Type alias and subtype definitions for the domain of the extended params
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtTypeDef :: VarEnv -> String
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtTypeDef m = Map.foldWithKey f "" $ varmap m
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz where g k a = case Map.lookup k $ vartypes m of
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz concat [ "(define-type t", show a, " (subtype (x"
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , show a, "::int) ", smtBoolExp br, "))" ]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz concat [ "(define-type t", show a, " int)" ]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz f k a s = s ++ g k a ++ "\n"
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz-- | Predicate definition
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtPredDef :: VarEnv -> String -> BoolRep -> String
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtPredDef m s b = concat [ "(define ", s, "::(->"
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , concat $ smtVars m " t"
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , " bool) (lambda ("
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , concat $ smtGenericVars m
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz (\ i -> let j = show i
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz in concat [" x", j, "::t", j])
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz , ") ", smtBoolExp b, "))" ]
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzsmtVarDef :: VarEnv -> String
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz $ smtGenericVars m (\ i -> let j = show i
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz in concat ["(define x", j, "::t", j, ")"])