{-# 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.Interface 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 , 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) ] 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 deprecatedConfigTests adaptrs = [ 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 $ head 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 $ head 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", "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] ]