what4-1.2: test/OnlineSolverTest.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
import Control.Exception ( try, SomeException )
import Control.Lens (folded)
import Control.Monad ( forM, void )
import Data.Char ( toLower )
import Data.Proxy
import System.Exit ( ExitCode(..) )
import System.Process ( readProcessWithExitCode )
import Test.Tasty
import Test.Tasty.HUnit
import qualified Data.BitVector.Sized as BV
import Data.Parameterized.Nonce
import What4.Config
import What4.Interface
import What4.Expr
import What4.ProblemFeatures
import What4.Solver
import What4.Protocol.Online
import What4.Protocol.SMTWriter
import qualified What4.Protocol.SMTLib2 as SMT2
import qualified What4.Solver.Yices as Yices
data State t = State
allOnlineSolvers :: [(String, AnOnlineSolver, ProblemFeatures, [ConfigDesc])]
allOnlineSolvers =
[ ("Z3", AnOnlineSolver @(SMT2.Writer Z3) Proxy, z3Features, z3Options)
, ("CVC4", AnOnlineSolver @(SMT2.Writer CVC4) Proxy, cvc4Features, cvc4Options)
, ("Yices", AnOnlineSolver @Yices.Connection Proxy, yicesDefaultFeatures, yicesOptions)
, ("Boolector", AnOnlineSolver @(SMT2.Writer Boolector) Proxy, boolectorFeatures, boolectorOptions)
#ifdef TEST_STP
, ("STP", AnOnlineSolver @(SMT2.Writer STP) Proxy, stpFeatures, stpOptions)
#endif
]
mkSmokeTest :: (String, AnOnlineSolver, ProblemFeatures, [ConfigDesc]) -> TestTree
mkSmokeTest (nm, AnOnlineSolver (Proxy :: Proxy s), features, opts) = testCase nm $
withIONonceGenerator $ \gen ->
do sym <- newExprBuilder FloatUninterpretedRepr State gen
extendConfig opts (getConfiguration sym)
proc <- startSolverProcess @s features Nothing sym
let conn = solverConn proc
inNewFrame proc $
do assume conn (falsePred sym)
check proc "smoke test" >>= \case
Unknown -> fail "Solver returned UNKNOWN"
Sat _ -> fail "Should be UNSAT"
Unsat _ -> return ()
----------------------------------------------------------------------
mkFormula1 :: IsSymExprBuilder sym
=> sym
-> IO ( SymExpr sym BaseBoolType
, SymExpr sym BaseBoolType
, SymExpr sym BaseBoolType
, SymExpr sym BaseBoolType
)
mkFormula1 sym = do
-- Let's determine if the following formula is satisfiable:
-- f(p, q, r) = (p | !q) & (q | r) & (!p | !r) & (!p | !q | r)
-- First, declare fresh constants for each of the three variables p, q, r.
p <- freshConstant sym (safeSymbol "p") BaseBoolRepr
q <- freshConstant sym (safeSymbol "q") BaseBoolRepr
r <- freshConstant sym (safeSymbol "r") BaseBoolRepr
-- Next, create terms for the negation of p, q, and r.
not_p <- notPred sym p
not_q <- notPred sym q
not_r <- notPred sym r
-- Next, build up each clause of f individually.
clause1 <- orPred sym p not_q
clause2 <- orPred sym q r
clause3 <- orPred sym not_p not_r
clause4 <- orPred sym not_p =<< orPred sym not_q r
-- Finally, create f out of the conjunction of all four clauses.
f <- andPred sym clause1 =<<
andPred sym clause2 =<<
andPred sym clause3 clause4
return (p,q,r,f)
-- Checks that the only valid model for Formula1 was found, and then
-- returns an expression that (as an assumption) disallows that model.
checkFormula1Model :: (IsExprBuilder sym, SymExpr sym ~ Expr t)
=> sym
-> Expr t BaseBoolType
-> Expr t BaseBoolType
-> Expr t BaseBoolType
-> GroundEvalFn t
-> IO (SymExpr sym BaseBoolType)
checkFormula1Model sym p q r eval =
do p' <- groundEval eval p
q' <- groundEval eval q
r' <- groundEval eval r
-- This is the unique satisfiable model
p' == False @? "p value"
q' == False @? "q value"
r' == True @? "r value"
-- Return an assumption that blocks this model
bs <- forM [(p,p'),(q,q'),(r,r')] $ \(x,v) -> eqPred sym x (backendPred sym v)
block <- notPred sym =<< andAllOf sym folded bs
return block
-- Solve Formula1 using a frame (push/pop) for each of the good and
-- bad cases
quickstartTest :: (String, AnOnlineSolver, ProblemFeatures, [ConfigDesc]) -> TestTree
quickstartTest (nm, AnOnlineSolver (Proxy :: Proxy s), features, opts) = testCaseSteps nm $ \step ->
withIONonceGenerator $ \gen ->
do sym <- newExprBuilder FloatUninterpretedRepr State gen
extendConfig opts (getConfiguration sym)
(p,q,r,f) <- mkFormula1 sym
step "Start Solver"
proc <- startSolverProcess @s features Nothing sym
let conn = solverConn proc
-- Check that formula f is satisfiable, and get the values from
-- the model that satisifies it
step "Check Satisfiability"
block <- inNewFrame proc $
do assume conn f
res <- check proc "framed formula1 satisfiable"
case res of
Unsat _ -> fail "Unsatisfiable"
Unknown -> fail "Solver returned UNKNOWN"
Sat _ ->
checkFormula1Model sym p q r =<< getModel proc
-- Now check that the formula is unsatisfiable when the blocking
-- predicate is added. Re-use the existing solver connection
step "Check Unsatisfiable"
inNewFrame proc $
do assume conn f
assume conn block
res <- check proc "framed formula1 unsatisfiable"
case res of
Unsat _ -> return ()
Unknown -> fail "Solver returned UNKNOWN"
Sat _ -> fail "Should be a unique model!"
-- Solve Formula1 directly, with a solver reset between good and bad cases
quickstartTestAlt :: (String, AnOnlineSolver, ProblemFeatures, [ConfigDesc]) -> TestTree
quickstartTestAlt (nm, AnOnlineSolver (Proxy :: Proxy s), features, opts) = testCaseSteps nm $ \step ->
withIONonceGenerator $ \gen ->
do sym <- newExprBuilder FloatUninterpretedRepr State gen
extendConfig opts (getConfiguration sym)
(p,q,r,f) <- mkFormula1 sym
step "Start Solver"
proc <- startSolverProcess @s features Nothing sym
let conn = solverConn proc
-- Check that formula f is satisfiable, and get the values from
-- the model that satisifies it
step "Check Satisfiability"
block <-
do assume conn f
res <- check proc "direct formula1 satisfiable"
case res of
Unsat _ -> fail "Unsatisfiable"
Unknown -> fail "Solver returned UNKNOWN"
Sat _ ->
checkFormula1Model sym p q r =<< getModel proc
-- Now check that the formula is unsatisfiable when the blocking
-- predicate is added. Re-use the existing solver connection
reset proc
step "Check Unsatisfiable"
assume conn f
assume conn block
res <- check proc "direct formula1 unsatisfiable"
case res of
Unsat _ -> return ()
Unknown -> fail "Solver returned UNKNOWN"
Sat _ -> fail "Should be a unique model!"
----------------------------------------------------------------------
getSolverVersion :: String -> IO String
getSolverVersion solver =
let args = case toLower <$> solver of
-- n.b. abc will return a non-zero exit code if asked
-- for command usage.
"abc" -> ["s", "-q", "version;quit"]
_ -> ["--version"]
in try (readProcessWithExitCode (toLower <$> solver) args "") >>= \case
Right (r,o,e) ->
if r == ExitSuccess
then let ol = lines o in
return $ if null ol then (solver <> " v??") else head ol
else return $ solver <> " version error: " <> show r <> " /;/ " <> e
Left (err :: SomeException) -> return $ solver <> " invocation error: " <> show err
reportSolverVersions :: IO ()
reportSolverVersions = do putStrLn "SOLVER VERSIONS::"
void $ mapM rep allOnlineSolvers
where rep (s,_,_,_) = disp s =<< getSolverVersion s
disp s v = putStrLn $ " Solver " <> s <> " == " <> v
main :: IO ()
main = do
reportSolverVersions
defaultMain $
localOption (mkTimeout (10 * 1000 * 1000)) $
testGroup "OnlineSolverTests"
[
testGroup "SmokeTest" $ map mkSmokeTest allOnlineSolvers
, testGroup "QuickStart Framed" $ map quickstartTest allOnlineSolvers
, testGroup "QuickStart Direct" $ map quickstartTestAlt allOnlineSolvers
]