From 74ee60155bf999cb10fd101dc4b1360e85d7fae0 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Wed, 28 Apr 2021 08:12:20 -0700 Subject: [PATCH] Add solver-specific strict_parsing configuration option and common handling. --- what4/src/What4/Config.hs | 16 +++++++ what4/src/What4/Protocol/SMTLib2.hs | 35 ++++++++------ what4/src/What4/Protocol/SMTLib2/Response.hs | 25 +++++----- what4/src/What4/Protocol/SMTWriter.hs | 29 ++++++++++-- what4/src/What4/Solver/Boolector.hs | 33 ++++++++----- what4/src/What4/Solver/CVC4.hs | 26 ++++++---- what4/src/What4/Solver/ExternalABC.hs | 9 ++++ what4/src/What4/Solver/STP.hs | 33 +++++++++---- what4/src/What4/Solver/Yices.hs | 31 +++++++----- what4/src/What4/Solver/Z3.hs | 19 ++++++-- what4/test/AdapterTest.hs | 50 +++++++++++++++++++- 11 files changed, 227 insertions(+), 79 deletions(-) diff --git a/what4/src/What4/Config.hs b/what4/src/What4/Config.hs index 820b33f0..f2ff105a 100644 --- a/what4/src/What4/Config.hs +++ b/what4/src/What4/Config.hs @@ -143,6 +143,7 @@ module What4.Config , optV , optU , optUV + , copyOpt , deprecatedOpt -- * Building and manipulating configurations @@ -661,6 +662,21 @@ optUV o vf h = mkOpt o (defaultOpt (configOptionType o) Nothing -> return optOK Just z -> return $ optErr $ pretty z +-- | The copyOpt creates a duplicate ConfigDesc under a different +-- name. This is typically used to taking a common operation and +-- modify the prefix to apply it to a more specialized role +-- (e.g. solver.strict_parsing --> solver.z3.strict_parsing). The +-- style and help text of the input ConfigDesc are preserved, but any +-- deprecation is discarded. +copyOpt :: (Text -> Text) -> ConfigDesc -> ConfigDesc +copyOpt modName (ConfigDesc o@(ConfigOption ty _) sty h _) = + let newName = case splitPath (modName (configOptionText o)) of + Just ps -> ps + Nothing -> error "new config option must not be empty" + in ConfigDesc (ConfigOption ty newName) sty h Nothing + + + ------------------------------------------------------------------------ -- ConfigState diff --git a/what4/src/What4/Protocol/SMTLib2.hs b/what4/src/What4/Protocol/SMTLib2.hs index ede817d8..6eb8bea1 100644 --- a/what4/src/What4/Protocol/SMTLib2.hs +++ b/what4/src/What4/Protocol/SMTLib2.hs @@ -129,7 +129,6 @@ import LibBF( bfToBits ) import Prelude hiding (writeFile) import What4.BaseTypes -import qualified What4.Concrete as BC import qualified What4.Config as CFG import qualified What4.Expr.Builder as B import What4.Expr.GroundEval @@ -931,15 +930,15 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures -> + -- | strictness override configuration + Maybe (CFG.ConfigOption I.BaseBoolType) -> B.ExprBuilder t st fs -> Streams.OutputStream Text -> Streams.InputStream Text -> IO (WriterConn t (Writer a)) - newDefaultWriter solver ack feats sym h in_h = do + newDefaultWriter solver ack feats strictOpt sym h in_h = do let cfg = I.getConfiguration sym - strictness <- maybe Strict - (\c -> if BC.fromConcreteBool c then Strict else Lenient) <$> - (CFG.getOption =<< CFG.getOptionSetting strictSMTParsing cfg) + strictness <- parserStrictness strictOpt strictSMTParsing cfg newWriter solver h in_h ack strictness (show solver) True feats True =<< B.getSymbolVarBimap sym @@ -948,6 +947,8 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures + -> Maybe (CFG.ConfigOption I.BaseBoolType) + -- ^ strictness override configuration -> B.ExprBuilder t st fs -> FilePath -- ^ Path to solver executable @@ -955,7 +956,7 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where -> (Session t a -> IO b) -- ^ Action to run -> IO b - withSolver solver ack feats sym path logData action = do + withSolver solver ack feats strictOpt sym path logData action = do args <- defaultSolverArgs solver sym withProcessHandles path args Nothing $ \hdls@(in_h, out_h, err_h, _ph) -> do @@ -964,7 +965,7 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where demuxProcessHandles in_h out_h err_h (fmap (\x -> ("; ", x)) $ logHandle logData) - writer <- newDefaultWriter solver ack feats sym in_stream out_stream + writer <- newDefaultWriter solver ack feats strictOpt sym in_stream out_stream let s = Session { sessionWriter = writer , sessionResponse = out_stream @@ -990,19 +991,21 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures + -> Maybe (CFG.ConfigOption I.BaseBoolType) + -- ^ strictness override configuration -> B.ExprBuilder t st fs -> LogData -> [B.BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b - runSolverInOverride solver ack feats sym logData predicates cont = do + runSolverInOverride solver ack feats strictOpt sym logData predicates cont = do I.logSolverEvent sym (I.SolverStartSATQuery $ I.SolverStartSATQueryRec { I.satQuerySolverName = show solver , I.satQueryReason = logReason logData }) path <- defaultSolverPath solver sym - withSolver solver ack feats sym path (logData{logVerbosity=2}) $ \session -> do + withSolver solver ack feats strictOpt sym path (logData{logVerbosity=2}) $ \session -> do -- Assume the predicates hold. forM_ predicates (SMTWriter.assume (sessionWriter session)) -- Run check SAT and get the model back. @@ -1022,18 +1025,18 @@ writeDefaultSMT2 :: SMTLib2Tweaks a -- ^ Name of solver for reporting. -> ProblemFeatures -- ^ Features supported by solver + -> Maybe (CFG.ConfigOption I.BaseBoolType) + -- ^ strictness override configuration -> B.ExprBuilder t st fs -> IO.Handle -> [B.BoolExpr t] -> IO () -writeDefaultSMT2 a nm feat sym h ps = do +writeDefaultSMT2 a nm feat strictOpt sym h ps = do bindings <- B.getSymbolVarBimap sym str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h null_in <- Streams.nullInput let cfg = I.getConfiguration sym - strictness <- maybe Strict - (\c -> if BC.fromConcreteBool c then Strict else Lenient) <$> - (CFG.getOption =<< CFG.getOptionSetting strictSMTParsing cfg) + strictness <- parserStrictness strictOpt strictSMTParsing cfg c <- newWriter a str null_in nullAcknowledgementAction strictness nm True feat True bindings setProduceModels c True forM_ ps (SMTWriter.assume c) @@ -1047,10 +1050,12 @@ startSolver -- ^ Action for acknowledging command responses -> (WriterConn t (Writer a) -> IO ()) -- ^ Action for setting start-up-time options and logic -> ProblemFeatures + -> Maybe (CFG.ConfigOption I.BaseBoolType) + -- ^ strictness override configuration -> Maybe IO.Handle -> B.ExprBuilder t st fs -> IO (SolverProcess t (Writer a)) -startSolver solver ack setup feats auxOutput sym = do +startSolver solver ack setup feats strictOpt auxOutput sym = do path <- defaultSolverPath solver sym args <- defaultSolverArgs solver sym hdls@(in_h, out_h, err_h, ph) <- startProcess path args Nothing @@ -1060,7 +1065,7 @@ startSolver solver ack setup feats auxOutput sym = do (fmap (\x -> ("; ", x)) auxOutput) -- Create writer - writer <- newDefaultWriter solver ack feats sym in_stream out_stream + writer <- newDefaultWriter solver ack feats strictOpt sym in_stream out_stream -- Set solver logic and solver-specific options setup writer diff --git a/what4/src/What4/Protocol/SMTLib2/Response.hs b/what4/src/What4/Protocol/SMTLib2/Response.hs index 864984ef..8f3021ec 100644 --- a/what4/src/What4/Protocol/SMTLib2/Response.hs +++ b/what4/src/What4/Protocol/SMTLib2/Response.hs @@ -23,6 +23,7 @@ module What4.Protocol.SMTLib2.Response , getLimitedSolverResponse , smtParseOptions , strictSMTParsing + , strictSMTParseOpt ) where @@ -38,7 +39,6 @@ import qualified System.IO.Streams as Streams import qualified System.IO.Streams.Attoparsec.Text as AStreams import qualified What4.BaseTypes as BT -import qualified What4.Concrete as BC import qualified What4.Config as CFG import What4.Protocol.SExp import qualified What4.Protocol.SMTLib2.Syntax as SMT2 @@ -49,18 +49,19 @@ import What4.Utils.Process ( filterAsync ) strictSMTParsing :: CFG.ConfigOption BT.BaseBoolType strictSMTParsing = CFG.configOption BT.BaseBoolRepr "solver.strict_parsing" +strictSMTParseOpt :: CFG.ConfigDesc +strictSMTParseOpt = + CFG.mkOpt strictSMTParsing CFG.boolOptSty + (Just $ PPU.reflow $ + Text.concat ["Strictly parse SMT responses and fail on" + , "unrecognized data (the default)." + , "This might need to be disabled when running" + , "the SMT solver in verbose mode." + ]) + Nothing + smtParseOptions :: [CFG.ConfigDesc] -smtParseOptions = - [ - CFG.mkOpt strictSMTParsing CFG.boolOptSty - (Just $ PPU.reflow $ - Text.concat ["Strictly parse SMT responses and fail on" - , "unrecognized data (the default)." - , "This might need to be disabled when running" - , "the SMT solver in verbose mode." - ]) - (Just (BC.ConcreteBool True)) - ] +smtParseOptions = [ strictSMTParseOpt ] data SMTResponse = AckSuccess diff --git a/what4/src/What4/Protocol/SMTWriter.hs b/what4/src/What4/Protocol/SMTWriter.hs index 5e7f3cc4..1b0fdd86 100644 --- a/what4/src/What4/Protocol/SMTWriter.hs +++ b/what4/src/What4/Protocol/SMTWriter.hs @@ -84,6 +84,7 @@ module What4.Protocol.SMTWriter , DefineStyle(..) , AcknowledgementAction(..) , ResponseStrictness(..) + , parserStrictness , nullAcknowledgementAction -- * SMTWriter operations , assume @@ -104,7 +105,7 @@ import Control.Monad.Fail( MonadFail ) #endif import Control.Exception -import Control.Lens hiding ((.>)) +import Control.Lens hiding ((.>), Strict) import Control.Monad.Extra import Control.Monad.IO.Class import Control.Monad.Reader @@ -140,15 +141,16 @@ import System.IO.Streams (OutputStream, InputStream) import qualified System.IO.Streams as Streams import What4.BaseTypes -import What4.Interface (RoundingMode(..), stringInfo) -import What4.ProblemFeatures +import qualified What4.Config as CFG import qualified What4.Expr.ArrayUpdateMap as AUM import qualified What4.Expr.BoolMap as BM import What4.Expr.Builder import What4.Expr.GroundEval import qualified What4.Expr.StringSeq as SSeq -import qualified What4.Expr.WeightedSum as WSum import qualified What4.Expr.UnaryBV as UnaryBV +import qualified What4.Expr.WeightedSum as WSum +import What4.Interface (RoundingMode(..), stringInfo) +import What4.ProblemFeatures import What4.ProgramLoc import What4.SatResult import qualified What4.SemiRing as SR @@ -739,7 +741,24 @@ newWriterConn h in_h ack solver_name beStrict features bindings cs = do data ResponseStrictness = Lenient -- ^ allows other output preceeding recognized solver responses | Strict -- ^ parse _only_ recognized solver responses; fail on anything else - deriving (Eq) + deriving (Eq, Show) + +-- | Given an optional override configuration option, return the SMT +-- response parsing strictness that should be applied based on the +-- override or thedefault strictSMTParsing configuration. +parserStrictness :: Maybe (CFG.ConfigOption BaseBoolType) + -> CFG.ConfigOption BaseBoolType + -> CFG.Config + -> IO ResponseStrictness +parserStrictness overrideOpt strictOpt cfg = do + ovr <- case overrideOpt of + Nothing -> return Nothing + Just o -> CFG.getMaybeOpt =<< CFG.getOptionSetting o cfg + optval <- case ovr of + Just v -> return $ Just v + Nothing -> CFG.getMaybeOpt =<< CFG.getOptionSetting strictOpt cfg + return $ maybe Strict (\c -> if c then Strict else Lenient) optval + -- | Status to indicate when term value will be uncached. data TermLifetime diff --git a/what4/src/What4/Solver/Boolector.hs b/what4/src/What4/Solver/Boolector.hs index 885f6bd5..c8c80b13 100644 --- a/what4/src/What4/Solver/Boolector.hs +++ b/what4/src/What4/Solver/Boolector.hs @@ -30,21 +30,20 @@ import Control.Monad import Data.Bits ( (.|.) ) import What4.BaseTypes -import What4.Config import What4.Concrete -import What4.Interface -import What4.ProblemFeatures -import What4.SatResult +import What4.Config import What4.Expr.Builder import What4.Expr.GroundEval -import What4.Solver.Adapter +import What4.Interface +import What4.ProblemFeatures import What4.Protocol.Online import qualified What4.Protocol.SMTLib2 as SMT2 +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) +import What4.SatResult +import What4.Solver.Adapter import What4.Utils.Process - - data Boolector = Boolector deriving Show -- | Path to boolector @@ -54,6 +53,11 @@ boolectorPath = configOption knownRepr "solver.boolector.path" boolectorPathOLD :: ConfigOption (BaseStringType Unicode) boolectorPathOLD = configOption knownRepr "boolector_path" +-- | Control strict parsing for Boolector solver responses (defaults +-- to solver.strict-parsing option setting). +boolectorStrictParsing :: ConfigOption BaseBoolType +boolectorStrictParsing = configOption knownRepr "solver.boolector.strict_parsing" + boolectorOptions :: [ConfigDesc] boolectorOptions = let bpOpt co = mkOpt @@ -63,7 +67,9 @@ boolectorOptions = (Just (ConcreteString "boolector")) bp = bpOpt boolectorPath bp2 = deprecatedOpt [bp] $ bpOpt boolectorPathOLD - in [ bp, bp2 ] <> SMT2.smtlib2Options + in [ bp, bp2 + , copyOpt (const $ configOptionText boolectorStrictParsing) strictSMTParseOpt + ] <> SMT2.smtlib2Options boolectorAdapter :: SolverAdapter st boolectorAdapter = @@ -73,6 +79,7 @@ boolectorAdapter = , solver_adapter_check_sat = runBoolectorInOverride , solver_adapter_write_smt2 = SMT2.writeDefaultSMT2 () "Boolector" defaultWriteSMTLIB2Features + (Just boolectorStrictParsing) } instance SMT2.SMTLib2Tweaks Boolector where @@ -85,7 +92,8 @@ runBoolectorInOverride :: (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a runBoolectorInOverride = - SMT2.runSolverInOverride Boolector SMT2.nullAcknowledgementAction boolectorFeatures + SMT2.runSolverInOverride Boolector SMT2.nullAcknowledgementAction + boolectorFeatures (Just boolectorStrictParsing) -- | Run Boolector in a session. Boolector will be configured to produce models, but -- otherwise left with the default configuration. @@ -97,7 +105,8 @@ withBoolector -> (SMT2.Session t Boolector -> IO a) -- ^ Action to run -> IO a -withBoolector = SMT2.withSolver Boolector SMT2.nullAcknowledgementAction boolectorFeatures +withBoolector = SMT2.withSolver Boolector SMT2.nullAcknowledgementAction + boolectorFeatures (Just boolectorStrictParsing) boolectorFeatures :: ProblemFeatures @@ -125,5 +134,7 @@ setInteractiveLogicAndOptions writer = do SMT2.setLogic writer SMT2.allSupported instance OnlineSolver (SMT2.Writer Boolector) where - startSolverProcess = SMT2.startSolver Boolector SMT2.smtAckResult setInteractiveLogicAndOptions + startSolverProcess feat = SMT2.startSolver Boolector SMT2.smtAckResult + setInteractiveLogicAndOptions feat + (Just boolectorStrictParsing) shutdownSolverProcess = SMT2.shutdownSolver Boolector diff --git a/what4/src/What4/Solver/CVC4.hs b/what4/src/What4/Solver/CVC4.hs index b9c53296..059215f9 100644 --- a/what4/src/What4/Solver/CVC4.hs +++ b/what4/src/What4/Solver/CVC4.hs @@ -35,19 +35,20 @@ import System.IO import qualified System.IO.Streams as Streams import What4.BaseTypes -import What4.Config -import What4.Solver.Adapter import What4.Concrete -import What4.Interface -import What4.ProblemFeatures -import What4.SatResult +import What4.Config import What4.Expr.Builder import What4.Expr.GroundEval +import What4.Interface +import What4.ProblemFeatures import What4.Protocol.Online import qualified What4.Protocol.SMTLib2 as SMT2 +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) import qualified What4.Protocol.SMTLib2.Response as RSP import qualified What4.Protocol.SMTLib2.Syntax as Syntax import What4.Protocol.SMTWriter +import What4.SatResult +import What4.Solver.Adapter import What4.Utils.Process @@ -77,6 +78,11 @@ cvc4Timeout = configOption knownRepr "solver.cvc4.timeout" cvc4TimeoutOLD :: ConfigOption BaseIntegerType cvc4TimeoutOLD = configOption knownRepr "cvc4_timeout" +-- | Control strict parsing for Boolector solver responses (defaults +-- to solver.strict-parsing option setting). +cvc4StrictParsing :: ConfigOption BaseBoolType +cvc4StrictParsing = configOption knownRepr "solver.cvc4.strict_parsing" + cvc4Options :: [ConfigDesc] cvc4Options = let pathOpt co = mkOpt co @@ -91,6 +97,7 @@ cvc4Options = (Just (ConcreteInteger 0)) t1 = tmOpt cvc4Timeout in [ p1, r1, t1 + , copyOpt (const $ configOptionText cvc4StrictParsing) strictSMTParseOpt , deprecatedOpt [p1] $ pathOpt cvc4PathOLD , deprecatedOpt [r1] $ intWithRangeOpt cvc4RandomSeedOLD (negate (2^(30::Int)-1)) (2^(30::Int)-1) @@ -195,7 +202,8 @@ runCVC4InOverride -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a -runCVC4InOverride = SMT2.runSolverInOverride CVC4 nullAcknowledgementAction (SMT2.defaultFeatures CVC4) +runCVC4InOverride = SMT2.runSolverInOverride CVC4 nullAcknowledgementAction + (SMT2.defaultFeatures CVC4) (Just cvc4StrictParsing) -- | Run CVC4 in a session. CVC4 will be configured to produce models, but -- otherwise left with the default configuration. @@ -207,7 +215,8 @@ withCVC4 -> (SMT2.Session t CVC4 -> IO a) -- ^ Action to run -> IO a -withCVC4 = SMT2.withSolver CVC4 nullAcknowledgementAction (SMT2.defaultFeatures CVC4) +withCVC4 = SMT2.withSolver CVC4 nullAcknowledgementAction + (SMT2.defaultFeatures CVC4) (Just cvc4StrictParsing) setInteractiveLogicAndOptions :: SMT2.SMTLib2Tweaks a => @@ -228,7 +237,8 @@ setInteractiveLogicAndOptions writer = do instance OnlineSolver (SMT2.Writer CVC4) where startSolverProcess feat mbIOh sym = do - sp <- SMT2.startSolver CVC4 SMT2.smtAckResult setInteractiveLogicAndOptions feat mbIOh sym + sp <- SMT2.startSolver CVC4 SMT2.smtAckResult setInteractiveLogicAndOptions + feat (Just cvc4StrictParsing) mbIOh sym timeout <- SolverGoalTimeout <$> (getOpt =<< getOptionSetting cvc4Timeout (getConfiguration sym)) return $ sp { solverGoalTimeout = timeout } diff --git a/what4/src/What4/Solver/ExternalABC.hs b/what4/src/What4/Solver/ExternalABC.hs index d4d84f26..5f389a78 100644 --- a/what4/src/What4/Solver/ExternalABC.hs +++ b/what4/src/What4/Solver/ExternalABC.hs @@ -35,6 +35,7 @@ import What4.Expr.GroundEval import What4.Interface import What4.ProblemFeatures import qualified What4.Protocol.SMTLib2 as SMT2 +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) import What4.Protocol.SMTWriter import What4.SatResult import What4.Solver.Adapter @@ -49,6 +50,11 @@ abcPath = configOption knownRepr "solver.abc.path" abcPathOLD :: ConfigOption (BaseStringType Unicode) abcPathOLD = configOption knownRepr "abc_path" +-- | Control strict parsing for ABC solver responses (defaults +-- to solver.strict-parsing option setting). +abcStrictParsing :: ConfigOption BaseBoolType +abcStrictParsing = configOption knownRepr "solver.abc.strict_parsing" + abcOptions :: [ConfigDesc] abcOptions = let optPath co = mkOpt co @@ -57,6 +63,7 @@ abcOptions = (Just (ConcreteString "abc")) p = optPath abcPath in [ p + , copyOpt (const $ configOptionText abcStrictParsing) strictSMTParseOpt , deprecatedOpt [p] $ optPath abcPathOLD ] <> SMT2.smtlib2Options @@ -100,6 +107,7 @@ writeABCSMT2File -> [BoolExpr t] -> IO () writeABCSMT2File = SMT2.writeDefaultSMT2 ExternalABC "ABC" abcFeatures + (Just abcStrictParsing) instance SMT2.SMTLib2GenericSolver ExternalABC where defaultSolverPath _ = findSolverPath abcPath . getConfiguration @@ -119,3 +127,4 @@ runExternalABCInOverride -> IO a runExternalABCInOverride = SMT2.runSolverInOverride ExternalABC nullAcknowledgementAction abcFeatures + (Just abcStrictParsing) diff --git a/what4/src/What4/Solver/STP.hs b/what4/src/What4/Solver/STP.hs index 4f00e1cb..2226c04a 100644 --- a/what4/src/What4/Solver/STP.hs +++ b/what4/src/What4/Solver/STP.hs @@ -25,16 +25,17 @@ module What4.Solver.STP import Data.Bits import What4.BaseTypes -import What4.Config import What4.Concrete -import What4.Interface -import What4.ProblemFeatures -import What4.SatResult +import What4.Config import What4.Expr.Builder import What4.Expr.GroundEval -import What4.Solver.Adapter +import What4.Interface +import What4.ProblemFeatures import What4.Protocol.Online import qualified What4.Protocol.SMTLib2 as SMT2 +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) +import What4.SatResult +import What4.Solver.Adapter import What4.Utils.Process data STP = STP deriving Show @@ -52,6 +53,11 @@ stpRandomSeed = configOption knownRepr "solver.stp.random-seed" stpRandomSeedOLD :: ConfigOption BaseIntegerType stpRandomSeedOLD = configOption knownRepr "stp.random-seed" +-- | Control strict parsing for Boolector solver responses (defaults +-- to solver.strict-parsing option setting). +stpStrictParsing :: ConfigOption BaseBoolType +stpStrictParsing = configOption knownRepr "solver.stp.strict_parsing" + intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc intWithRangeOpt nm lo hi = mkOpt nm sty Nothing Nothing where sty = integerWithRangeOptSty (Inclusive lo) (Inclusive hi) @@ -63,11 +69,13 @@ stpOptions = (Just "Path to STP executable.") (Just (ConcreteString "stp")) p1 = mkPath stpPath - r1 = intWithRangeOpt stpRandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1) + randbitval = 2^(30 :: Int)-1 + r1 = intWithRangeOpt stpRandomSeed (negate randbitval) randbitval in [ p1, r1 + , copyOpt (const $ configOptionText stpStrictParsing) strictSMTParseOpt , deprecatedOpt [p1] $ mkPath stpPathOLD , deprecatedOpt [r1] $ intWithRangeOpt stpRandomSeedOLD - (negate (2^(30::Int)-1)) (2^(30::Int)-1) + (negate randbitval) randbitval ] <> SMT2.smtlib2Options stpAdapter :: SolverAdapter st @@ -78,6 +86,7 @@ stpAdapter = , solver_adapter_check_sat = runSTPInOverride , solver_adapter_write_smt2 = SMT2.writeDefaultSMT2 STP "STP" defaultWriteSMTLIB2Features + (Just stpStrictParsing) } instance SMT2.SMTLib2Tweaks STP where @@ -104,7 +113,8 @@ runSTPInOverride -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a -runSTPInOverride = SMT2.runSolverInOverride STP SMT2.nullAcknowledgementAction (SMT2.defaultFeatures STP) +runSTPInOverride = SMT2.runSolverInOverride STP SMT2.nullAcknowledgementAction + (SMT2.defaultFeatures STP) (Just stpStrictParsing) -- | Run STP in a session. STP will be configured to produce models, buth -- otherwise left with the default configuration. @@ -116,7 +126,8 @@ withSTP -> (SMT2.Session t STP -> IO a) -- ^ Action to run -> IO a -withSTP = SMT2.withSolver STP SMT2.nullAcknowledgementAction (SMT2.defaultFeatures STP) +withSTP = SMT2.withSolver STP SMT2.nullAcknowledgementAction + (SMT2.defaultFeatures STP) (Just stpStrictParsing) setInteractiveLogicAndOptions :: SMT2.SMTLib2Tweaks a => @@ -133,5 +144,7 @@ setInteractiveLogicAndOptions writer = do -- SMT2.setOption writer "global-declarations" "true" instance OnlineSolver (SMT2.Writer STP) where - startSolverProcess = SMT2.startSolver STP SMT2.smtAckResult setInteractiveLogicAndOptions + startSolverProcess feat = SMT2.startSolver STP SMT2.smtAckResult + setInteractiveLogicAndOptions feat + (Just stpStrictParsing) shutdownSolverProcess = SMT2.shutdownSolver STP diff --git a/what4/src/What4/Solver/Yices.hs b/what4/src/What4/Solver/Yices.hs index d3cf2974..d0c101d6 100644 --- a/what4/src/What4/Solver/Yices.hs +++ b/what4/src/What4/Solver/Yices.hs @@ -64,7 +64,7 @@ module What4.Solver.Yices ) where #if !MIN_VERSION_base(4,13,0) -import Control.Monad.Fail( MonadFail ) +import Control.Monad.Fail ( MonadFail ) #endif import Control.Applicative @@ -102,25 +102,26 @@ import qualified System.IO.Streams.Attoparsec.Text as Streams import qualified Prettyprinter as PP import What4.BaseTypes -import What4.Config -import What4.Solver.Adapter import What4.Concrete -import What4.Interface -import What4.ProblemFeatures -import What4.SatResult +import What4.Config import qualified What4.Expr.Builder as B import What4.Expr.GroundEval import What4.Expr.VarIdentification -import What4.Protocol.SExp -import What4.Protocol.SMTLib2 (writeDefaultSMT2) -import What4.Protocol.SMTWriter as SMTWriter +import What4.Interface +import What4.ProblemFeatures import What4.Protocol.Online import qualified What4.Protocol.PolyRoot as Root +import What4.Protocol.SExp +import What4.Protocol.SMTLib2 (writeDefaultSMT2) +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) +import What4.Protocol.SMTWriter as SMTWriter +import What4.SatResult +import What4.Solver.Adapter import What4.Utils.HandleReader import What4.Utils.Process -import Prelude -import GHC.Stack +import Prelude +import GHC.Stack -- | This is a tag used to indicate that a 'WriterConn' is a connection -- to a specific Yices process. @@ -903,7 +904,7 @@ yicesAdapter = runYicesInOverride sym logData ps (cont . runIdentity . traverseSatResult (\x -> pure (x,Nothing)) pure) , solver_adapter_write_smt2 = - writeDefaultSMT2 () "YICES" yicesSMT2Features + writeDefaultSMT2 () "YICES" yicesSMT2Features (Just yicesStrictParsing) } -- | Path to yices @@ -934,6 +935,11 @@ yicesGoalTimeout = configOption knownRepr "solver.yices.goal-timeout" yicesGoalTimeoutOLD :: ConfigOption BaseIntegerType yicesGoalTimeoutOLD = configOption knownRepr "yices_goal-timeout" +-- | Control strict parsing for Yices solver responses (defaults +-- to solver.strict-parsing option setting). +yicesStrictParsing :: ConfigOption BaseBoolType +yicesStrictParsing = configOption knownRepr "solver.yices.strict_parsing" + yicesOptions :: [ConfigDesc] yicesOptions = let mkPath co = mkOpt co @@ -957,6 +963,7 @@ yicesOptions = i = mkIntr yicesEnableInteractive t = mkTmout yicesGoalTimeout in [ p, m, i, t + , copyOpt (const $ configOptionText yicesStrictParsing) strictSMTParseOpt , deprecatedOpt [p] $ mkPath yicesPathOLD , deprecatedOpt [m] $ mkMCSat yicesEnableMCSatOLD , deprecatedOpt [i] $ mkIntr yicesEnableInteractiveOLD diff --git a/what4/src/What4/Solver/Z3.hs b/what4/src/What4/Solver/Z3.hs index e9a406bb..a30722e8 100644 --- a/what4/src/What4/Solver/Z3.hs +++ b/what4/src/What4/Solver/Z3.hs @@ -41,6 +41,7 @@ import What4.Interface import What4.ProblemFeatures import What4.Protocol.Online import qualified What4.Protocol.SMTLib2 as SMT2 +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) import qualified What4.Protocol.SMTLib2.Syntax as SMT2Syntax import What4.Protocol.SMTWriter import What4.SatResult @@ -63,6 +64,12 @@ z3Timeout = configOption knownRepr "solver.z3.timeout" z3TimeoutOLD :: ConfigOption BaseIntegerType z3TimeoutOLD = configOption knownRepr "z3_timeout" +-- | Strict parsing specifically for Z3 interaction? If set, +-- overrides solver.strict_parsing, otherwise defaults to +-- solver.strict_parsing. +z3StrictParsing :: ConfigOption BaseBoolType +z3StrictParsing = configOption knownRepr "solver.z3.strict_parsing" + z3Options :: [ConfigDesc] z3Options = let mkPath co = mkOpt co @@ -76,6 +83,7 @@ z3Options = p = mkPath z3Path t = mkTmo z3Timeout in [ p, t + , copyOpt (const $ configOptionText z3StrictParsing) strictSMTParseOpt , deprecatedOpt [p] $ mkPath z3PathOLD , deprecatedOpt [t] $ mkTmo z3TimeoutOLD ] <> SMT2.smtlib2Options @@ -137,7 +145,7 @@ writeZ3SMT2File -> Handle -> [BoolExpr t] -> IO () -writeZ3SMT2File = SMT2.writeDefaultSMT2 Z3 "Z3" z3Features +writeZ3SMT2File = SMT2.writeDefaultSMT2 Z3 "Z3" z3Features (Just z3StrictParsing) instance SMT2.SMTLib2GenericSolver Z3 where defaultSolverPath _ = findSolverPath z3Path . getConfiguration @@ -171,7 +179,8 @@ runZ3InOverride -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a -runZ3InOverride = SMT2.runSolverInOverride Z3 nullAcknowledgementAction z3Features +runZ3InOverride = SMT2.runSolverInOverride Z3 nullAcknowledgementAction + z3Features (Just z3StrictParsing) -- | Run Z3 in a session. Z3 will be configured to produce models, but -- otherwise left with the default configuration. @@ -183,7 +192,8 @@ withZ3 -> (SMT2.Session t Z3 -> IO a) -- ^ Action to run -> IO a -withZ3 = SMT2.withSolver Z3 nullAcknowledgementAction z3Features +withZ3 = SMT2.withSolver Z3 nullAcknowledgementAction + z3Features (Just z3StrictParsing) setInteractiveLogicAndOptions :: @@ -205,7 +215,8 @@ setInteractiveLogicAndOptions writer = do instance OnlineSolver (SMT2.Writer Z3) where startSolverProcess feat mbIOh sym = do - sp <- SMT2.startSolver Z3 SMT2.smtAckResult setInteractiveLogicAndOptions feat mbIOh sym + sp <- SMT2.startSolver Z3 SMT2.smtAckResult setInteractiveLogicAndOptions feat + (Just z3StrictParsing) mbIOh sym timeout <- SolverGoalTimeout <$> (getOpt =<< getOptionSetting z3Timeout (getConfiguration sym)) return $ sp { solverGoalTimeout = timeout } diff --git a/what4/test/AdapterTest.hs b/what4/test/AdapterTest.hs index 896df7c5..c56f55f6 100644 --- a/what4/test/AdapterTest.hs +++ b/what4/test/AdapterTest.hs @@ -29,11 +29,14 @@ import Test.Tasty.HUnit import Data.Parameterized.Nonce import Data.Parameterized.Some +import qualified What4.BaseTypes as BT import What4.Config -import What4.Interface import What4.Expr -import What4.Solver +import What4.Interface +import What4.Protocol.SMTLib2.Response ( strictSMTParsing ) +import What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness(..) ) import What4.Protocol.VerilogWriter +import What4.Solver data State t = State @@ -78,6 +81,7 @@ mkConfigTests :: [SolverAdapter State] -> [TestTree] mkConfigTests adapters = [ testGroup "deprecated configs" (deprecatedConfigTests adapters) + , testGroup "strict parsing config" (strictParseConfigTests adapters) ] where wantOptSetFailure withText res = case res of @@ -173,6 +177,48 @@ mkConfigTests adapters = 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 = [