Skip to content

Commit

Permalink
Add allowQuantifiedQueries config option
Browse files Browse the repository at this point in the history 
Addresses #459
  • Loading branch information
@LeventErkok
LeventErkok committed Mar 2, 2019
1 parent a90b1bd commit 453fc2b
Show file tree
Hide file tree
Showing 4 changed files with 53 additions and 33 deletions.
9 changes: 9 additions & 0 deletions CHANGES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,15 @@
It accepts bit-vectors as arguments and an unsigned rotation quantity to keep
things simple.

* Added new configuration option 'allowQueryQuantifers', default is set to False.
SBV normally doesn't allow quantifiers in a query context, because there are
issues surrounding 'getValue'. However, Joel Burget pointed out this check
is too strict for certain scenarios. So, as an escape hatch, you can define
'allowQueryQuantifers' to be 'True' and SBV will bypass this check. Of course,
if you do this, then you are on your own regarding calls to `getValue` with
quantified parameters! See http://github.com/LeventErkok/sbv/issues/459
for details.

* [BACKWARDS COMPATIBILITY] Renamed the class `IEEEFloatConvertable` to
`IEEEFloatConvertible`. (Typo in name!)

Expand Down
11 changes: 10 additions & 1 deletion Data/SBV/Control/Utils.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1585,8 +1585,17 @@ executeQuery queryContext (QueryT userQuery) = do
--
-- So, we check if this is an external-query, and if there are quantified variables. If so, we
-- cowardly refuse to continue. For details, see: <http://github.com/LeventErkok/sbv/issues/407>
--
-- However, as discussed in <https://github.com/LeventErkok/sbv/issues/459>, we'll allow for this
-- if the user explicitly asks as to do so. In that case, all bets are off!

let allowQQs = case rm of
SMTMode _ _ _ cfg -> allowQuantifiedQueries cfg
CodeGen -> False -- doesn't matter in these two
Concrete -> False -- cases, but we're being careful

() <- liftIO $ case queryContext of
() <- unless allowQQs $ liftIO $
case queryContext of
QueryInternal -> return () -- we're good, internal usages don't mess with scopes
QueryExternal -> do
(userInps, _) <- readIORef (rinps st)
Expand Down
33 changes: 17 additions & 16 deletions Data/SBV/Core/Symbolic.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1686,22 +1686,23 @@ instance HasKind RoundingMode
-- The 'printBase' field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will
-- be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.
data SMTConfig = SMTConfig {
verbose :: Bool -- ^ Debug mode
, timing :: Timing -- ^ Print timing information on how long different phases took (construction, solving, etc.)
, printBase :: Int -- ^ Print integral literals in this base (2, 10, and 16 are supported.)
, printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16)
, satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.
, allSatMaxModelCount :: Maybe Int -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all.
, allSatPrintAlong :: Bool -- ^ In a 'Data.SBV.allSat' call, print models as they are found.
, satTrackUFs :: Bool -- ^ In a 'Data.SBV.sat' call, should we try to extract values of uninterpreted functions?
, isNonModelVar :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)
, transcript :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)
, smtLibVersion :: SMTLibVersion -- ^ What version of SMT-lib we use for the tool
, solver :: SMTSolver -- ^ The actual SMT solver.
, roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions
, solverSetOptions :: [SMTOption] -- ^ Options to set as we start the solver
, ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.
, redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied.
verbose :: Bool -- ^ Debug mode
, timing :: Timing -- ^ Print timing information on how long different phases took (construction, solving, etc.)
, printBase :: Int -- ^ Print integral literals in this base (2, 10, and 16 are supported.)
, printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16)
, satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.
, allSatMaxModelCount :: Maybe Int -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all.
, allSatPrintAlong :: Bool -- ^ In a 'Data.SBV.allSat' call, print models as they are found.
, satTrackUFs :: Bool -- ^ In a 'Data.SBV.sat' call, should we try to extract values of uninterpreted functions?
, isNonModelVar :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)
, transcript :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)
, smtLibVersion :: SMTLibVersion -- ^ What version of SMT-lib we use for the tool
, solver :: SMTSolver -- ^ The actual SMT solver.
, allowQuantifiedQueries :: Bool -- ^ Should we permit use of quantifiers in the query mode? (Default: False. See <http://github.com/LeventErkok/sbv/issues/459> for why.)
, roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions
, solverSetOptions :: [SMTOption] -- ^ Options to set as we start the solver
, ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.
, redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied.
}

-- We're just seq'ing top-level here, it shouldn't really matter. (i.e., no need to go deeper.)
Expand Down
33 changes: 17 additions & 16 deletions Data/SBV/Provers/Prover.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,22 +71,23 @@ import qualified Data.SBV.Provers.MathSAT as MathSAT
import qualified Data.SBV.Provers.ABC as ABC

mkConfig :: SMTSolver -> SMTLibVersion -> [Control.SMTOption] -> SMTConfig
mkConfig s smtVersion startOpts = SMTConfig { verbose = False
, timing = NoTiming
, printBase = 10
, printRealPrec = 16
, transcript = Nothing
, solver = s
, smtLibVersion = smtVersion
, satCmd = "(check-sat)"
, satTrackUFs = True -- i.e., yes, do extract UI function values
, allSatMaxModelCount = Nothing -- i.e., return all satisfying models
, allSatPrintAlong = False -- i.e., do not print models as they are found
, isNonModelVar = const False -- i.e., everything is a model-variable by default
, roundingMode = RoundNearestTiesToEven
, solverSetOptions = startOpts
, ignoreExitCode = False
, redirectVerbose = Nothing
mkConfig s smtVersion startOpts = SMTConfig { verbose = False
, timing = NoTiming
, printBase = 10
, printRealPrec = 16
, transcript = Nothing
, solver = s
, smtLibVersion = smtVersion
, satCmd = "(check-sat)"
, satTrackUFs = True -- i.e., yes, do extract UI function values
, allSatMaxModelCount = Nothing -- i.e., return all satisfying models
, allSatPrintAlong = False -- i.e., do not print models as they are found
, isNonModelVar = const False -- i.e., everything is a model-variable by default
, allowQuantifiedQueries = False
, roundingMode = RoundNearestTiesToEven
, solverSetOptions = startOpts
, ignoreExitCode = False
, redirectVerbose = Nothing
}

-- | If supported, this makes all output go to stdout, which works better with SBV
Expand Down

0 comments on commit 453fc2b

Please sign in to comment.