Add solver-specific strict_parsing configuration option and common handling.

2024-11-29 13:55:51 +03:00 · 2021-04-28 08:12:20 -07:00 · 2021-04-28 08:12:20 -07:00 · 74ee60155b
commit 74ee60155b
parent 4b13d83f8b
11 changed files with 227 additions and 79 deletions
--- 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

--- 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
--- 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
--- 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
--- 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
--- 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 }
--- 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)
--- 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
--- 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
--- 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 }
--- 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 =
      [