what4-1.6: test/AdapterTest.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 ( displayException, try, SomeException(..), fromException )
import Control.Lens (folded)
import Control.Monad ( forM, unless )
import Control.Monad.Except ( runExceptT )
import Data.BitVector.Sized ( mkBV )
import Data.Char ( toLower )
import qualified Data.List as L
import Data.Maybe ( fromMaybe )
import Data.Text ( pack )
import System.Environment ( lookupEnv )
import ProbeSolvers
import Test.Tasty
import Test.Tasty.ExpectedFailure
import Test.Tasty.HUnit
import Data.Parameterized.Nonce
import Data.Parameterized.Some
import What4.Config
import What4.Expr
import What4.Expr.Builder ( asApp, pushMuxOpsOption )
import What4.Interface
import What4.Panic
import What4.Protocol.SMTLib2.Response ( strictSMTParsing )
import What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness(..) )
import What4.Protocol.VerilogWriter
import What4.Solver
allAdapters :: [SolverAdapter EmptyExprBuilderState]
allAdapters =
[ cvc4Adapter
, cvc5Adapter
, yicesAdapter
, z3Adapter
, bitwuzlaAdapter
, boolectorAdapter
, externalABCAdapter
#ifdef TEST_STP
, stpAdapter
#endif
] <> drealAdpt
drealAdpt :: [SolverAdapter EmptyExprBuilderState]
#ifdef TEST_DREAL
drealAdpt = [drealAdapter]
#else
drealAdpt = []
#endif
withSym ::
SolverAdapter EmptyExprBuilderState ->
(forall t . ExprBuilder t EmptyExprBuilderState (Flags FloatUninterpreted) -> IO a) ->
IO a
withSym adpt pred_gen = withIONonceGenerator $ \gen ->
do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
extendConfig (solver_adapter_config_options adpt) (getConfiguration sym)
pred_gen sym
mkSmokeTest :: SolverAdapter EmptyExprBuilderState -> TestTree
mkSmokeTest adpt = testCase (solver_adapter_name adpt) $
withSym adpt $ \sym ->
do res <- smokeTest sym adpt
case res of
Nothing -> return ()
Just ex -> fail $ displayException ex
----------------------------------------------------------------------
mkConfigTests :: [SolverAdapter EmptyExprBuilderState] -> [TestTree]
mkConfigTests adapters =
[
testGroup "deprecated configs" (deprecatedConfigTests adapters)
, testGroup "strict parsing config" (strictParseConfigTests adapters)
, testGroup "push mux ops config" (pushMuxOpsConfigTests adapters)
]
where
wantOptSetFailure withText res = case res of
Right r ->
assertFailure ("Expected '" <> withText <>
"' but completed successfully with: " <> show r)
Left err ->
case fromException err of
Just (e :: OptSetFailure) ->
withText `L.isInfixOf` (show e) @?
("Expected '" <> withText <> "' exception error but got: " <>
show e)
_ -> assertFailure $
"Expected OptSetFailure exception but got: " <> show err
wantOptGetFailure withText res = case res of
Right r ->
assertFailure ("Expected '" <> withText <>
"' but completed successfully with: " <> show r)
Left err ->
case fromException err of
Just (e :: OptGetFailure) ->
withText `L.isInfixOf` (show e) @?
("Expected '" <> withText <> "' exception error but got: " <>
show e)
_ -> assertFailure $
"Expected OptGetFailure exception but got: " <> show err
withAdapters :: [SolverAdapter EmptyExprBuilderState]
-> (forall t . ExprBuilder t EmptyExprBuilderState (Flags FloatUninterpreted) -> IO a)
-> IO a
withAdapters adptrs op = do
(cfgs, _getDefAdapter) <- solverAdapterOptions adptrs
withIONonceGenerator $ \gen ->
do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
extendConfig cfgs (getConfiguration sym)
op sym
cmpUnderSomes :: Some OptionSetting -> Some OptionSetting -> IO ()
cmpUnderSomes (Some setterX) (Some setterY) =
case testEquality
(configOptionType (optionSettingName setterX))
(BaseStringRepr UnicodeRepr) of
Just Refl ->
case testEquality
(configOptionType (optionSettingName setterY))
(BaseStringRepr UnicodeRepr) of
Just Refl -> do vX <- getMaybeOpt setterX
vY <- getMaybeOpt setterY
vX @=? vY
Nothing -> assertFailure "second some is not a unicode string"
Nothing -> assertFailure "first some is not a unicode string"
cmpUnderSomesI :: Some OptionSetting -> Some OptionSetting -> IO ()
cmpUnderSomesI (Some setterX) (Some setterY) =
case testEquality BaseIntegerRepr
(configOptionType (optionSettingName setterX)) of
Just Refl ->
case testEquality BaseIntegerRepr
(configOptionType (optionSettingName setterY)) of
Just Refl -> do vX <- getMaybeOpt setterX
vY <- getMaybeOpt setterY
vX @=? vY
Nothing -> assertFailure "second some is not an integer"
Nothing -> assertFailure "first some is not an integer"
cmpUnderSome :: Some OptionSetting
-> OptionSetting (BaseStringType Unicode) -> IO ()
cmpUnderSome (Some setterX) setterY =
case testEquality
(configOptionType (optionSettingName setterX))
(BaseStringRepr UnicodeRepr) of
Just Refl -> do vX <- getMaybeOpt setterX
vY <- getMaybeOpt setterY
vX @=? vY
Nothing -> assertFailure "first some is not a unicode string"
cmpUnderSomeI :: Some OptionSetting
-> OptionSetting BaseIntegerType -> IO ()
cmpUnderSomeI (Some setterX) setterY =
case testEquality BaseIntegerRepr
(configOptionType (optionSettingName setterX)) of
Just Refl -> do vX <- getMaybeOpt setterX
vY <- getMaybeOpt setterY
vX @=? vY
Nothing -> assertFailure "first some is not an integer"
cmpUnderSomeB :: Some OptionSetting
-> OptionSetting BaseBoolType -> IO ()
cmpUnderSomeB (Some setterX) setterY =
case testEquality BaseBoolRepr
(configOptionType (optionSettingName setterX)) of
Just Refl -> do vX <- getMaybeOpt setterX
vY <- getMaybeOpt setterY
vX @=? vY
Nothing -> assertFailure "first some is not a boolean"
strictParseConfigTests adaptrs =
let mkPCTest adaptr =
testGroup (solver_adapter_name adaptr) $
let setCommonStrictness cfg v = do
setter <- getOptionSetting strictSMTParsing cfg
show <$> setOpt setter v >>= (@?= "[]")
setSpecificStrictness cfg v = do
setter <- getOptionSettingFromText (pack cfgName) cfg
show <$> setBoolOpt setter v >>= (@?= "[]")
cfgName = "solver." <> (toLower <$> (solver_adapter_name adaptr)) <> ".strict_parsing"
in [
testCase "default val" $
withAdapters adaptrs $ \sym -> do
let cfg = getConfiguration sym
strictOpt = Just $ configOption knownRepr cfgName
parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Strict)
, testCase "common val" $
withAdapters adaptrs $ \sym -> do
let cfg = getConfiguration sym
strictOpt = Just $ configOption knownRepr cfgName
setCommonStrictness cfg False
parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Lenient)
, testCase "strict val" $
withAdapters adaptrs $ \sym -> do
let cfg = getConfiguration sym
strictOpt = Just $ configOption knownRepr cfgName
setSpecificStrictness cfg False
parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Lenient)
, testCase "strict overrides common val" $
withAdapters adaptrs $ \sym -> do
let cfg = getConfiguration sym
strictOpt = Just $ configOption knownRepr cfgName
setCommonStrictness cfg False
setSpecificStrictness cfg True
parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Strict)
]
in fmap mkPCTest adaptrs
pushMuxOpsConfigTests adaptrs =
let -- A basic test that ensures that pushMuxOps actually takes effect
-- when enabled or disabled.
mkPushZextMuxTest ::
forall a.
Bool ->
(forall t. Expr t (BaseBVType 64) -> IO a) ->
IO a
mkPushZextMuxTest pushMuxOpsVal k =
withAdapters adaptrs $ \sym -> do
pmo <- getOptionSetting pushMuxOpsOption (getConfiguration sym)
show <$> setOpt pmo pushMuxOpsVal >>= (@?= "[]")
let w = knownNat @32
a <- bvLit sym w $ mkBV w 27
b <- bvLit sym w $ mkBV w 42
c <- freshConstant sym (safeSymbol "c") BaseBoolRepr
ite <- bvIte sym c a b
zextIte <- bvZext sym (knownNat @64) ite
k zextIte
in [ testCase "enable pushMuxOps" $
mkPushZextMuxTest True $ \zextIte ->
case asApp zextIte of
Just (BaseIte {}) -> pure ()
_ -> assertFailure $ unlines
[ "zext not pushed down through ite"
, show $ printSymExpr zextIte
]
, testCase "disable pushMuxOps" $
mkPushZextMuxTest False $ \zextIte ->
case asApp zextIte of
Just (BVZext {}) -> pure ()
_ -> assertFailure $ unlines
[ "zext should be at the head of the application"
, show $ printSymExpr zextIte
]
]
deprecatedConfigTests adaptrs =
let firstAdapter adptrs =
case adptrs of
adptr:_ -> adptr
[] -> panic "deprecatedConfigTests" ["Empty list of adapters"]
in
[
testCaseSteps "deprecated default_solver is equivalent to solver.default" $
-- n.b. requires at least 2 entries in the adaptrs list
\step -> withAdapters adaptrs $ \sym -> do
step "Get OptionSetters, regular and deprecated, Text and ConfigOption"
settera <- getOptionSettingFromText "solver.default"
(getConfiguration sym)
setterb <- getOptionSettingFromText "default_solver"
(getConfiguration sym)
settera' <- getOptionSetting defaultSolverAdapter
(getConfiguration sym)
step "Get (same) initial value from regular and deprecated"
cmpUnderSomes settera setterb
step "Get (same) initial value from Text and ConfigOption identification"
cmpUnderSome settera settera'
v0 <- getMaybeOpt settera'
step "Update the value via deprecated"
res1 <- try $ setUnicodeOpt setterb $
pack $ solver_adapter_name $ last adaptrs
case res1 of
Right warns -> fmap show warns @?=
[ "DEPRECATED CONFIG OPTION USED: default_solver (renamed to: solver.default)"
]
Left (SomeException e) -> assertFailure $ show e
-- Get (same) updated value from regular and deprecated
cmpUnderSomes settera setterb
v1 <- getMaybeOpt settera'
(v0 /= v1) @? ("Update from " <> show v0 <> " failed for " <>
show (fmap solver_adapter_name adaptrs))
step "Update the value via regular (text identification)"
res2 <- try $ setUnicodeOpt settera $
pack $ solver_adapter_name $ firstAdapter adaptrs
case res2 of
Right warns -> fmap show warns @?= []
Left (SomeException e) -> assertFailure $ show e
v2 <- getMaybeOpt settera'
v0 @=? v2
step "Update the value via regular (ConfigOption identification)"
res3 <- try $ setOpt settera' $
pack $ solver_adapter_name $ last $ take 2 adaptrs
case res3 of
Right warns -> fmap show warns @?= []
Left (SomeException e) -> assertFailure $ show e
v3 <- getMaybeOpt settera'
(v0 /= v3) @? ("Update from " <> show v0 <> " failed for " <>
show (fmap solver_adapter_name adaptrs))
step "Attempt invalid update via deprecated"
wantOptSetFailure "invalid setting" =<<
try (setUnicodeOpt setterb "foo")
v4 <- getMaybeOpt settera'
v3 @=? v4
step "Reset to original value"
res4 <- try $ setOpt settera' $
pack $ solver_adapter_name $ firstAdapter adaptrs
case res4 of
Right warns -> fmap show warns @?= []
Left (SomeException e) -> assertFailure $ show e
v5 <- getMaybeOpt settera'
v0 @=? v5
cmpUnderSome settera settera'
, testCase "deprecated boolector_path is equivalent to solver.boolector.path" $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "boolector_path"
(getConfiguration sym)
setterb <- getOptionSetting boolectorPath
(getConfiguration sym)
cmpUnderSome settera setterb
res1 <- try $ setUnicodeOpt settera "/foo/bar"
case res1 of
Right warns -> fmap show warns @?=
[ "Could not find: /foo/bar"
, "DEPRECATED CONFIG OPTION USED: boolector_path (renamed to: solver.boolector.path)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSome settera setterb
, testCase "deprecated cvc4_path is equivalent to solver.cvc4.path" $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "cvc4_path"
(getConfiguration sym)
setterb <- getOptionSetting cvc4Path
(getConfiguration sym)
cmpUnderSome settera setterb
res1 <- try $ setUnicodeOpt settera "/foo/bar"
case res1 of
Right warns -> fmap show warns @?=
[ "Could not find: /foo/bar"
, "DEPRECATED CONFIG OPTION USED: cvc4_path (renamed to: solver.cvc4.path)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSome settera setterb
, testCase "deprecated cvc4_timeout is equivalent to solver.cvc4.timeout" $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "cvc4_timeout"
(getConfiguration sym)
setterb <- getOptionSetting cvc4Timeout
(getConfiguration sym)
cmpUnderSomeI settera setterb
res1 <- try $ setIntegerOpt settera 42
case res1 of
Right warns -> fmap show warns @?=
[ "DEPRECATED CONFIG OPTION USED: cvc4_timeout (renamed to: solver.cvc4.timeout)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSomeI settera setterb
, testCase "deprecated stp.random-seed is equivalent to solver.stp.random-seed" $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "cvc4.random-seed"
(getConfiguration sym)
setterb <- getOptionSettingFromText "solver.cvc4.random-seed"
(getConfiguration sym)
cmpUnderSomesI settera setterb
res1 <- try $ setIntegerOpt settera 99
case res1 of
Right warns -> fmap show warns @?=
[ "DEPRECATED CONFIG OPTION USED: cvc4.random-seed (renamed to: solver.cvc4.random-seed)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSomesI settera setterb
, (if "dreal" `elem` (solver_adapter_name <$> adapters)
then id else ignoreTestBecause "dreal not available") $
testCase "deprecated dreal_path is equivalent to solver.dreal.path" $
withAdapters adaptrs $ \sym -> do
#ifdef TEST_DREAL
settera <- getOptionSettingFromText "dreal_path"
(getConfiguration sym)
setterb <- getOptionSetting drealPath
(getConfiguration sym)
cmpUnderSome settera setterb
res1 <- try $ setUnicodeOpt settera "/foo/bar"
case res1 of
Right warns -> fmap show warns @?=
[ "Could not find: /foo/bar"
, "DEPRECATED CONFIG OPTION USED: dreal_path (renamed to: solver.dreal.path)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSome settera setterb
#else
settera <- try $ getOptionSettingFromText "dreal_path"
(getConfiguration sym)
wantOptGetFailure "not found" settera
#endif
, (if "abc" `elem` (solver_adapter_name <$> adapters)
then id else ignoreTestBecause "abc not available") $
testCase "deprecated abc_path is equivalent to solver.abc.path" $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "abc_path"
(getConfiguration sym)
setterb <- getOptionSetting abcPath
(getConfiguration sym)
cmpUnderSome settera setterb
res1 <- try $ setUnicodeOpt settera "/foo/bar"
case res1 of
Right warns -> fmap show warns @?=
[ "Could not find: /foo/bar"
, "DEPRECATED CONFIG OPTION USED: abc_path (renamed to: solver.abc.path)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSome settera setterb
, (if "stp" `elem` (solver_adapter_name <$> adapters)
then id else ignoreTestBecause "stp not available") $
testCase "deprecated stp_path is equivalent to solver.stp.path" $
withAdapters adaptrs $ \sym -> do
#ifdef TEST_STP
settera <- getOptionSettingFromText "stp_path"
(getConfiguration sym)
setterb <- getOptionSetting stpPath
(getConfiguration sym)
cmpUnderSome settera setterb
res1 <- try $ setUnicodeOpt settera "/foo/bar"
case res1 of
Right warns -> fmap show warns @?=
[ "Could not find: /foo/bar"
, "DEPRECATED CONFIG OPTION USED: stp_path (renamed to: solver.stp.path)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSome settera setterb
#else
settera <- try $ getOptionSettingFromText "stp_path"
(getConfiguration sym)
wantOptGetFailure "not found" settera
#endif
, (if "stp" `elem` (solver_adapter_name <$> adapters)
then id else ignoreTestBecause "stp not available") $
testCase "deprecated stp.random-seed is equivalent to solver.stp.random-seed" $
withAdapters adaptrs $ \sym -> do
#ifdef TEST_STP
settera <- getOptionSettingFromText "stp.random-seed"
(getConfiguration sym)
setterb <- getOptionSettingFromText "solver.stp.random-seed"
(getConfiguration sym)
cmpUnderSomesI settera setterb
res1 <- try $ setIntegerOpt settera 99
case res1 of
Right warns -> fmap show warns @?=
[ "DEPRECATED CONFIG OPTION USED: stp.random-seed (renamed to: solver.stp.random-seed)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSomesI settera setterb
#else
settera <- try $ getOptionSettingFromText "stp.random-seed"
(getConfiguration sym)
wantOptGetFailure "not found" settera
#endif
, testCase "deprecated yices_path is equivalent to solver.yices.path" $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "yices_path"
(getConfiguration sym)
setterb <- getOptionSetting yicesPath
(getConfiguration sym)
cmpUnderSome settera setterb
res1 <- try $ setUnicodeOpt settera "/foo/bar"
case res1 of
Right warns -> fmap show warns @?=
[ "Could not find: /foo/bar"
, "DEPRECATED CONFIG OPTION USED: yices_path (renamed to: solver.yices.path)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSome settera setterb
, testCase "deprecated yices_enable-interactive is equivalent to solver.yices.en.." $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "yices_enable-interactive"
(getConfiguration sym)
setterb <- getOptionSetting yicesEnableInteractive
(getConfiguration sym)
cmpUnderSomeB settera setterb
res1 <- try $ setBoolOpt settera True
case res1 of
Right warns -> fmap show warns @?=
[ "DEPRECATED CONFIG OPTION USED: yices_enable-interactive (renamed to: solver.yices.enable-interactive)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSomeB settera setterb
, testCase "deprecated yices_enable-mcsat is equivalent to solver.yices.enable-mcsat" $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "yices_enable-mcsat"
(getConfiguration sym)
setterb <- getOptionSetting yicesEnableMCSat
(getConfiguration sym)
cmpUnderSomeB settera setterb
res1 <- try $ setBoolOpt settera True
case res1 of
Right warns -> fmap show warns @?=
[ "DEPRECATED CONFIG OPTION USED: yices_enable-mcsat (renamed to: solver.yices.enable-mcsat)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSomeB settera setterb
, testCase "deprecated yices_goal-timeout is equivalent to solver.yices.goal-timeout" $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "yices_goal-timeout"
(getConfiguration sym)
setterb <- getOptionSetting yicesGoalTimeout
(getConfiguration sym)
cmpUnderSomeI settera setterb
res1 <- try $ setIntegerOpt settera 123
case res1 of
Right warns -> fmap show warns @?=
[ "DEPRECATED CONFIG OPTION USED: yices_goal-timeout (renamed to: solver.yices.goal-timeout)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSomeI settera setterb
, testCase "deprecated z3_path is equivalent to solver.z3.path" $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "z3_path"
(getConfiguration sym)
setterb <- getOptionSetting z3Path
(getConfiguration sym)
cmpUnderSome settera setterb
res1 <- try $ setUnicodeOpt settera "/bar/foo"
case res1 of
Right warns -> fmap show warns @?=
[ "Could not find: /bar/foo"
, "DEPRECATED CONFIG OPTION USED: z3_path (renamed to: solver.z3.path)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSome settera setterb
, testCase "deprecated z3_timeout is equivalent to solver.z3.timeout" $
withAdapters adaptrs $ \sym -> do
settera <- getOptionSettingFromText "z3_timeout"
(getConfiguration sym)
setterb <- getOptionSetting z3Timeout
(getConfiguration sym)
cmpUnderSomeI settera setterb
res1 <- try $ setIntegerOpt settera 123
case res1 of
Right warns -> fmap show warns @?=
[ "DEPRECATED CONFIG OPTION USED: z3_timeout (renamed to: solver.z3.timeout)"
]
Left (SomeException e) -> assertFailure $ show e
cmpUnderSomeI settera setterb
]
----------------------------------------------------------------------
nonlinearRealTest :: SolverAdapter EmptyExprBuilderState -> TestTree
nonlinearRealTest adpt =
let wrap = if solver_adapter_name adpt `elem` [ "ABC", "bitwuzla", "boolector", "stp" ]
then expectFailBecause
(solver_adapter_name adpt
<> " does not support this type of linear arithmetic term")
else id
in wrap $ testCase (solver_adapter_name adpt) $
withSym adpt $ \sym ->
do x <- freshConstant sym (safeSymbol "a") BaseRealRepr
y <- freshConstant sym (safeSymbol "b") BaseRealRepr
xabs <- realAbs sym x
x2 <- realMul sym x x
x2_1 <- realAdd sym x2 =<< realLit sym 1
x2_y <- realAdd sym x2 y
p1 <- realLt sym x2_1 =<< realLit sym 0
p2 <- realLe sym x2_y =<< realLit sym (-1)
p3 <- realGe sym x2_y =<< realLit sym (-2)
p4 <- realLe sym xabs =<< realLit sym 10
-- asking if `x^2 < 0` should be unsat
solver_adapter_check_sat adpt sym defaultLogData [p1] $ \case
Unsat _ -> return ()
Unknown -> fail "Solver returned UNKNOWN"
Sat _ -> fail "Should be UNSAT!"
-- asking to find `-2 <= x^2 + y <= -1` with `abs(x) <= 10`. Should find something.
solver_adapter_check_sat adpt sym defaultLogData [p2,p3,p4] $ \case
Unsat _ -> fail "Shoule be UNSAT!"
Unknown -> fail "Solver returned UNKNOWN"
Sat (eval,_bounds) ->
do x' <- groundEval eval x
abs x' <= 10 @? "correct abs(x) bound"
x2_y' <- groundEval eval x2_y
((-2) <= x2_y' && x2_y' <= (-1)) @? "correct bounds"
mkQuickstartTest :: SolverAdapter EmptyExprBuilderState -> TestTree
mkQuickstartTest adpt =
let wrap = if solver_adapter_name adpt == "stp"
then ignoreTestBecause "STP cannot generate the model"
else id
in wrap $
testCase (solver_adapter_name adpt) $
withSym adpt $ \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
(p',q',r') <-
solver_adapter_check_sat adpt sym defaultLogData [f] $ \case
Unsat _ -> fail "Unsatisfiable"
Unknown -> fail "Solver returned UNKNOWN"
Sat (eval, _) ->
do p' <- groundEval eval p
q' <- groundEval eval q
r' <- groundEval eval r
return (p',q',r')
-- This is the unique satisfiable model
p' == False @? "p value"
q' == False @? "q value"
r' == True @? "r value"
-- Compute a blocking predicate for the computed model
bs <- forM [(p,p'),(q,q'),(r,r')] $ \(x,v) -> eqPred sym x (backendPred sym v)
block <- notPred sym =<< andAllOf sym folded bs
-- Ask if there is some other model
solver_adapter_check_sat adpt sym defaultLogData [f,block] $ \case
Unsat _ -> return ()
Unknown -> fail "Solver returned UNKNOWN"
Sat _ -> fail "Should be a unique model!"
verilogTest :: TestTree
verilogTest = testCase "verilogTest" $ withIONonceGenerator $ \gen ->
do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
let w = knownNat @8
x <- freshConstant sym (safeSymbol "x") (BaseBVRepr w)
one <- bvLit sym w (mkBV w 1)
add <- bvAdd sym x one
r <- notPred sym =<< bvEq sym x add
edoc <- runExceptT (exprsVerilog sym [] [Some r] "f")
case edoc of
Left err -> fail $ "Failed to translate to Verilog: " ++ err
Right doc ->
unless (show doc ++ "\n" == refDoc) $
fail $ unlines [
"Unexpected output from Verilog translation:"
, show doc
, "instead of"
, refDoc
]
where
refDoc = unlines [ "module f(x, out);"
, " input [7:0] x;"
, " wire [7:0] wr = 8'h1;"
, " wire [7:0] wr_2 = wr * x;"
, " wire [7:0] wr_3 = wr + wr_2;"
, " wire wr_4 = wr_3 == x;"
, " wire wr_5 = ! wr_4;"
, " output out = wr_5;"
, "endmodule"
]
main :: IO ()
main = do
testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"
let solverNames = SolverName . solver_adapter_name <$> allAdapters
solvers <- reportSolverVersions testLevel (SolverName . solver_adapter_name)
=<< (zip allAdapters <$> mapM getSolverVersion solverNames)
let adapters = fst <$> solvers
defaultMain $
localOption (mkTimeout (10 * 1000 * 1000)) $
testGroup "AdapterTests"
[ testGroup "SmokeTest" $ map mkSmokeTest adapters
, testGroup "Config Tests" $ mkConfigTests adapters
, testGroup "QuickStart" $ map mkQuickstartTest adapters
, testGroup "nonlinear reals" $ map nonlinearRealTest adapters
, testGroup "Verilog" [verilogTest]
]