smtlib2 0.3 → 0.3.1

raw patch · 2 files changed

+9/−17 lines, 2 files

Files

• Language/SMTLib2/Pipe.hs +8/−16
• smtlib2.cabal +1/−1

@@ -1,4 +1,4 @@-{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE ViewPatterns, ImpredicativeTypes #-} module Language.SMTLib2.Pipe        (SMTPipe(),         FunctionParser(..),@@ -317,7 +317,7 @@     Just (Just x) -> return (x,pipe)     _ -> error $ "smtlib2: Couldn't parse proof "++show res   where-    findProof [] = Nothing+    findProof [] = Nothing :: Maybe L.Lisp     findProof ((L.List [L.Symbol "proof",proof]):_) = Just proof     findProof (x:xs) = findProof xs handleRequest pipe SMTGetUnsatCore = do@@ -378,7 +378,7 @@         Just rtp' -> let argMp = Map.fromList [ (name,(i,sort))                                               | (i,(name,sort)) <- zip [0..] args' ]                          funId = case unescapeName (T.unpack fname) of-                           Nothing -> Nothing+                           Nothing -> Nothing :: Maybe Integer                            Just (Right idx) -> Just idx                            Just (Left name) -> case Map.lookup name (namedVars $ smtState pipe) of                              Just idx -> Just idx@@ -470,18 +470,10 @@               -> [String] -- ^ Command line arguments to be passed to the SMT solver               -> IO SMTPipe createSMTPipe solver args = do-  let cmd = CreateProcess { cmdspec = RawCommand solver args-                          , cwd = Nothing-                          , env = Nothing-                          , std_in = CreatePipe-                          , std_out = CreatePipe-                          , std_err = Inherit-                          , close_fds = False-                          , create_group = True-#if MIN_VERSION_process(1,2,0)-                          , delegate_ctlc = False-#endif-                          }+  let cmd = (proc solver args) { std_in = CreatePipe+                               , std_out = CreatePipe+                               , std_err = Inherit+                               , create_group = True }   (Just hin,Just hout,_,handle) <- createProcess cmd   return $ SMTPipe { channelIn = hin                    , channelOut = hout@@ -1272,7 +1264,7 @@               ,fun]) rec dts #ifdef SMTLIB2_WITH_CONSTRAINTS       = case parseFun rec fun rec dts of-        Nothing -> Nothing+        Nothing -> Nothing :: Maybe FunctionParser'         Just (DefinedParser _ ret_sig parse)           -> Just $ OverloadedParser             { sortConstraint = const True

@@ -1,5 +1,5 @@ Name:           smtlib2-Version:        0.3+Version:        0.3.1 Author:         Henning Günther <guenther@forsyte.at> Maintainer:     guenther@forsyte.at Synopsis:       A type-safe interface to communicate with an SMT solver.