GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-12-01 20:23:10 +03:00
Code Issues Projects Releases Wiki Activity

Remove unneeded arguments to nameResult and versionResult.

Browse Source
This commit is contained in:
Kevin Quick 2021-03-15 11:42:23 -07:00
parent f6f66f949e
commit ed9a24efbd
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
2 changed files with 7 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
what4/src/What4/Protocol/SMTLib2.hs
View File

@ -1192,8 +1192,8 @@ ppSolverVersionError err =
na Nothing = "n/a" na Nothing = "n/a"
-- | Get the result of a version query -- | Get the result of a version query
nameResult :: f h -> Streams.InputStream Text -> IO Text nameResult :: Streams.InputStream Text -> IO Text
nameResult _ s = nameResult s =
let cmd = SMT2.getName let cmd = SMT2.getName
in in
tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) >>= tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) >>=
@ -1220,8 +1220,8 @@ queryErrorBehavior conn resp =
-- | Get the result of a version query -- | Get the result of a version query
versionResult :: f h -> Streams.InputStream Text -> IO Text versionResult :: Streams.InputStream Text -> IO Text
versionResult _ s = versionResult s =
let cmd = SMT2.getVersion let cmd = SMT2.getVersion
in in
tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) >>= tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) >>=
@ -1246,7 +1246,7 @@ checkSolverVersion' boundsMap proc =
Nothing -> done Nothing -> done
Just bnds -> Just bnds ->
do getVersion conn do getVersion conn
res <- versionResult conn (solverResponse proc) res <- versionResult (solverResponse proc)
case Versions.version res of case Versions.version res of
Left e -> pure (Left (UnparseableVersion e)) Left e -> pure (Left (UnparseableVersion e))
Right actualVer -> Right actualVer ->

4
what4/test/ExprBuilderSMTLib2.hs
View File

@ -885,12 +885,12 @@ testSolverInfo = testGroup "solver info queries" $
[ testCase "test get solver version" $ withOnlineZ3 $ \_ proc -> do [ testCase "test get solver version" $ withOnlineZ3 $ \_ proc -> do
let conn = solverConn proc let conn = solverConn proc
getVersion conn getVersion conn
_ <- versionResult conn (solverResponse proc) _ <- versionResult (solverResponse proc)
pure () pure ()
, testCase "test get solver name" $ withOnlineZ3 $ \_ proc -> do , testCase "test get solver name" $ withOnlineZ3 $ \_ proc -> do
let conn = solverConn proc let conn = solverConn proc
getName conn getName conn
nm <- nameResult conn (solverResponse proc) nm <- nameResult (solverResponse proc)
nm @?= "Z3" nm @?= "Z3"
] ]