diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,23 @@ * Hackage: * GitHub: -* Latest Hackage released version: 8.1, 2019-03-09 +* Latest Hackage released version: 8.2, 2019-04-07 + +### Version 8.2, 2019-04-07 + + * Fixed minor issue with getting observables in quantified contexts. + + * Simplify data-type constructor usage and accessor formats. See + http://github.com/Z3Prover/z3/issues/2135 for a discussion. + + * Add support for model validation in optimization problems. Use the + config parameter: `optimizeValidateConstraints`. Default: False. This + feature nicely complements the `validateModel` option, which works + for `sat` and `prove` calls. Note that when we validate the model + for an optimization problem, we only make sure that the given result + satisfies the constraints not that it is minimum (or maximum) such + model. (And hence the new configuration variable.) Validating optimality + is beyond the scope of SBV. ### Version 8.1, 2019-03-09 diff --git a/Data/SBV/Control/Query.hs b/Data/SBV/Control/Query.hs --- a/Data/SBV/Control/Query.hs +++ b/Data/SBV/Control/Query.hs @@ -46,7 +46,9 @@ import Data.SBV.Core.Data -import Data.SBV.Core.Symbolic (MonadQuery(..), QueryState(..), SMTModel(..), SMTResult(..), State(..), incrementInternalCounter) +import Data.SBV.Core.Symbolic ( MonadQuery(..), QueryState(..), SMTModel(..), SMTResult(..), State(..) + , incrementInternalCounter, validationRequested + ) import Data.SBV.Utils.SExpr @@ -301,22 +303,22 @@ m@Concrete{} -> error $ "SBV.getModel: Model is not available in mode: " ++ show m SMTMode _ _ isSAT _ -> do cfg <- getConfig - inps <- getQuantifiedInputs - obsvs <- getObservables + qinps <- getQuantifiedInputs uis <- getUIs -- for "sat", display the prefix existentials. for "proof", display the prefix universals - let allModelInputs = if isSAT then takeWhile ((/= ALL) . fst) inps - else takeWhile ((== ALL) . fst) inps + let allModelInputs = if isSAT then takeWhile ((/= ALL) . fst) qinps + else takeWhile ((== ALL) . fst) qinps - -- are we inside a quantifier - insideQuantifier = length allModelInputs < length inps + -- Add on observables only if we're not in a quantified context + grabObservables = length allModelInputs == length qinps -- i.e., we didn't drop anything - -- observables are only meaningful if we're not in a quantified context - prefixObservables | insideQuantifier = [] - | True = obsvs + obsvs <- if grabObservables + then getObservables + else do queryDebug ["*** In a quantified context, obvservables will not be printed."] + return [] - sortByNodeId :: [(SV, (String, CV))] -> [(String, CV)] + let sortByNodeId :: [(SV, (String, CV))] -> [(String, CV)] sortByNodeId = map snd . sortBy (compare `on` (\(SV _ nid, _) -> nid)) grab (sv, nm) = wrap <$> getValueCV mbi sv @@ -324,7 +326,7 @@ inputAssocs <- mapM (grab . snd) allModelInputs - let assocs = sortOn fst prefixObservables + let assocs = sortOn fst obsvs ++ sortByNodeId [p | p@(_, (nm, _)) <- inputAssocs, not (isNonModelVar cfg nm)] -- collect UIs if requested @@ -349,8 +351,8 @@ (False, EX) -> (ALL, sv) (False, ALL) -> (EX, sv) - in if validateModel cfg - then Just <$> mapM (get . flipQ) inps + in if validationRequested cfg + then Just <$> mapM (get . flipQ) qinps else return Nothing uivs <- mapM (\ui@(nm, t) -> (\a -> (nm, (t, a))) <$> getUIFunCVAssoc mbi ui) uiFuns @@ -736,7 +738,7 @@ -- | Generalization of 'Data.SBV.Control.mkSMTResult' -- NB. This function does not allow users to create interpretations for UI-Funs. But that's --- probably not a good idea anyhow. Also, if you use the 'validateModel' feature, SBV will +-- probably not a good idea anyhow. Also, if you use the 'validateModel' or 'optimizeValidateConstraints' features, SBV will -- fail on models returned via this function. mkSMTResult :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult mkSMTResult asgns = do diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -79,7 +79,7 @@ import Data.SBV.Core.Symbolic ( IncState(..), withNewIncState, State(..), svToSV, symbolicEnv, SymbolicT , MonadQuery(..), QueryContext(..), Queriable(..), Fresh(..) - , registerLabel, svMkSymVar + , registerLabel, svMkSymVar, validationRequested , isSafetyCheckingIStage, isSetupIStage, isRunIStage, IStage(..), QueryT(..) , extractSymbolicSimulationState, MonadSymbolic(..), newUninterpreted ) @@ -1310,14 +1310,15 @@ -- Add on observables if we're asked to do so: obsvs <- if grabObservables then getObservables - else return [] + else do queryDebug ["*** In a quantified context, obvservables will not be printed."] + return [] bindings <- let grab i@(ALL, _) = return (i, Nothing) grab i@(EX, (sv, _)) = case sv `lookup` assocs of Just (_, (_, cv)) -> return (i, Just cv) Nothing -> do cv <- getValueCV Nothing sv return (i, Just cv) - in if validateModel cfg + in if validationRequested cfg then Just <$> mapM grab qinps else return Nothing diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -54,7 +54,7 @@ , OptimizeStyle(..), Objective(..), Penalty(..), objectiveName, addSValOptGoal , MonadQuery(..), QueryT(..), Query, Queriable(..), Fresh(..), QueryState(..), QueryContext(..) , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), SMTEngine - , outputSVal + , validationRequested, outputSVal ) where import Control.Arrow (first, second, (***)) @@ -1323,10 +1323,10 @@ , "***" , "*** To turn validation off, use `cfg{validateModel = False}`" , "***" - , "*** " ++ conc ++ "." + , "*** " ++ conc ] - cant = "Validation engine is not capable of handling this case. Failed to validate" + cant = "Validation engine is not capable of handling this case. Failed to validate." report = "Please report this as a bug in SBV!" in if isUninterpreted k @@ -1337,7 +1337,14 @@ nsv = (sv, nm) cv = case [(q, v) | ((q, nsv'), v) <- env, nsv == nsv'] of - [] -> bad ("Cannot locate variable: " ++ show nsv) report + [] -> if isTracker + then -- The sole purpose of a tracker variable is to send the optimization + -- directive to the solver, so we can name "expressions" that are minimized + -- or maximized. There will be no constraints on these when we are doing + -- the validation; in fact they will not even be used anywhere during a + -- validation run. So, simply push a zero value that inhabits all metrics. + mkConstCV k (0::Integer) + else bad ("Cannot locate variable: " ++ show (nsv, k)) report [(ALL, _)] -> bad ("Cannot validate models in the presence of universally quantified variable " ++ show (snd nsv)) cant [(EX, Nothing)] -> bad ("Cannot locate model value of variable: " ++ show (snd nsv)) report [(EX, Just c)] -> c @@ -1515,7 +1522,7 @@ -- we only add it if it's interesting; i.e., not directly -- true or has some attributes. let isValidating = case rm of - SMTMode _ _ _ cfg -> validateModel cfg + SMTMode _ _ _ cfg -> validationRequested cfg CodeGen -> False Concrete Nothing -> False Concrete (Just _) -> True -- The case when we *are* running the validation @@ -1697,8 +1704,6 @@ , supportsCustomQueries :: Bool -- ^ Supports interactive queries per SMT-Lib? , supportsGlobalDecls :: Bool -- ^ Supports global declarations? (Needed for push-pop.) , supportsDataTypes :: Bool -- ^ Supports datatypes? - , supportsDTConstructorSigs :: Bool -- ^ Supports full ascription on data-type constructors? (CVC4 and z3 differ!) - , supportsDTAccessorSigs :: Bool -- ^ Supports full ascription on data-type accessor? (CVC4 and z3 differ!) , supportsFlattenedModels :: Maybe [String] -- ^ Supports flattened model output? (With given config lines.) } @@ -1738,38 +1743,43 @@ -- 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) - , validateModel :: Bool -- ^ If set, SBV will attempt to validate the model it gets back from the solver. - , 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 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. + 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) + , validateModel :: Bool -- ^ If set, SBV will attempt to validate the model it gets back from the solver. + , optimizeValidateConstraints :: Bool -- ^ Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints. + , 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 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. } +-- | Returns true if we have to perform validation +validationRequested :: SMTConfig -> Bool +validationRequested SMTConfig{validateModel, optimizeValidateConstraints} = validateModel || optimizeValidateConstraints + -- We're just seq'ing top-level here, it shouldn't really matter. (i.e., no need to go deeper.) instance NFData SMTConfig where rnf SMTConfig{} = () -- | A model, as returned by a solver data SMTModel = SMTModel { - modelObjectives :: [(String, GeneralizedCV)] -- ^ Mapping of symbolic values to objective values. - , modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)] -- ^ Mapping of input variables as reported by the solver. Only collected if model validation is requested. - , modelAssocs :: [(String, CV)] -- ^ Mapping of symbolic values to constants. - , modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))] -- ^ Mapping of uninterpreted functions to association lists in the model. - -- Note that an uninterpreted constant (function of arity 0) will be stored - -- in the 'modelAssocs' field. + modelObjectives :: [(String, GeneralizedCV)] -- ^ Mapping of symbolic values to objective values. + , modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)] -- ^ Mapping of input variables as reported by the solver. Only collected if model validation is requested. + , modelAssocs :: [(String, CV)] -- ^ Mapping of symbolic values to constants. + , modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))] -- ^ Mapping of uninterpreted functions to association lists in the model. + -- Note that an uninterpreted constant (function of arity 0) will be stored + -- in the 'modelAssocs' field. } deriving Show diff --git a/Data/SBV/Provers/ABC.hs b/Data/SBV/Provers/ABC.hs --- a/Data/SBV/Provers/ABC.hs +++ b/Data/SBV/Provers/ABC.hs @@ -39,8 +39,6 @@ , supportsCustomQueries = False , supportsGlobalDecls = False , supportsDataTypes = False - , supportsDTConstructorSigs = False - , supportsDTAccessorSigs = False , supportsFlattenedModels = Nothing } } diff --git a/Data/SBV/Provers/Boolector.hs b/Data/SBV/Provers/Boolector.hs --- a/Data/SBV/Provers/Boolector.hs +++ b/Data/SBV/Provers/Boolector.hs @@ -37,8 +37,6 @@ , supportsCustomQueries = True , supportsGlobalDecls = False , supportsDataTypes = False - , supportsDTConstructorSigs = False - , supportsDTAccessorSigs = False , supportsFlattenedModels = Nothing } } diff --git a/Data/SBV/Provers/CVC4.hs b/Data/SBV/Provers/CVC4.hs --- a/Data/SBV/Provers/CVC4.hs +++ b/Data/SBV/Provers/CVC4.hs @@ -41,8 +41,6 @@ , supportsCustomQueries = True , supportsGlobalDecls = True , supportsDataTypes = True - , supportsDTConstructorSigs = True - , supportsDTAccessorSigs = False , supportsFlattenedModels = Nothing } } diff --git a/Data/SBV/Provers/MathSAT.hs b/Data/SBV/Provers/MathSAT.hs --- a/Data/SBV/Provers/MathSAT.hs +++ b/Data/SBV/Provers/MathSAT.hs @@ -41,8 +41,6 @@ , supportsCustomQueries = True , supportsGlobalDecls = False , supportsDataTypes = True - , supportsDTConstructorSigs = False - , supportsDTAccessorSigs = False , supportsFlattenedModels = Nothing } } diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -16,6 +16,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} module Data.SBV.Provers.Prover ( SMTSolver(..), SMTConfig(..), Predicate @@ -71,24 +72,25 @@ 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 - , validateModel = False - , allowQuantifiedQueries = False - , 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 + , validateModel = False + , optimizeValidateConstraints = False + , allowQuantifiedQueries = False + , roundingMode = RoundNearestTiesToEven + , solverSetOptions = startOpts + , ignoreExitCode = False + , redirectVerbose = Nothing } -- | If supported, this makes all output go to stdout, which works better with SBV @@ -162,7 +164,7 @@ -- | Generalization of 'Data.SBV.proveWith' proveWith :: SMTConfig -> a -> m ThmResult proveWith cfg a = do r <- runWithQuery False (checkNoOptimizations >> Control.getSMTResult) cfg a - ThmResult <$> if validateModel cfg + ThmResult <$> if validationRequested cfg then validate False cfg a r else return r @@ -173,7 +175,7 @@ -- | Generalization of 'Data.SBV.satWith' satWith :: SMTConfig -> a -> m SatResult satWith cfg a = do r <- runWithQuery True (checkNoOptimizations >> Control.getSMTResult) cfg a - SatResult <$> if validateModel cfg + SatResult <$> if validationRequested cfg then validate True cfg a r else return r @@ -184,7 +186,7 @@ -- | Generalization of 'Data.SBV.allSatWith' allSatWith :: SMTConfig -> a -> m AllSatResult allSatWith cfg a = do f@(mm, pe, un, rs) <- runWithQuery True (checkNoOptimizations >> Control.getAllSatResult) cfg a - AllSatResult <$> if validateModel cfg + AllSatResult <$> if validationRequested cfg then do rs' <- mapM (validate True cfg a) rs return (mm, pe, un, rs') else return f @@ -195,17 +197,23 @@ -- | Generalization of 'Data.SBV.optimizeWith' optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult - optimizeWith config style = runWithQuery True opt config + optimizeWith config style optGoal = do + res <- runWithQuery True opt config optGoal + if not (optimizeValidateConstraints config) + then return res + else let v :: SMTResult -> m SMTResult + v = validate True config optGoal + in case res of + LexicographicResult m -> LexicographicResult <$> v m + IndependentResult xs -> let w [] sofar = return (reverse sofar) + w ((n, m):rest) sofar = v m >>= \m' -> w rest ((n, m') : sofar) + in IndependentResult <$> w xs [] + ParetoResult (b, rs) -> ParetoResult . (b, ) <$> mapM v rs + where opt = do objectives <- Control.getObjectives qinps <- Control.getQuantifiedInputs spgm <- Control.getSBVPgm - when (validateModel config) $ - error $ unlines [ "" - , "*** Data.SBV: Model validation is not supported in optimization calls." - , "*** To turn validation off, use `cfg{validateModel = False}`" - ] - when (null objectives) $ error $ unlines [ "" , "*** Data.SBV: Unsupported call to optimize when no objectives are present." @@ -218,6 +226,17 @@ , "*** Please use a solver that has support, such as z3" ] + when (validateModel config && not (optimizeValidateConstraints config)) $ + error $ unlines [ "" + , "*** Data.SBV: Model validation is not supported in optimization calls." + , "***" + , "*** Instead, use `cfg{optimizeValidateConstraints = True}`" + , "***" + , "*** which checks that the results satisfy the constraints but does" + , "*** NOT ensure that they are optimal." + ] + + let universals = [s | (ALL, s) <- qinps] firstUniversal @@ -285,9 +304,9 @@ mapM_ (Control.send True) optimizerDirectives case style of - Lexicographic -> LexicographicResult <$> Control.getLexicographicOptResults - Independent -> IndependentResult <$> Control.getIndependentOptResults (map objectiveName objectives) - Pareto mbN -> ParetoResult <$> Control.getParetoOptResults mbN + Lexicographic -> LexicographicResult <$> Control.getLexicographicOptResults + Independent -> IndependentResult <$> Control.getIndependentOptResults (map objectiveName objectives) + Pareto mbN -> ParetoResult <$> Control.getParetoOptResults mbN -- | Generalization of 'Data.SBV.isVacuous' isVacuous :: a -> m Bool @@ -335,11 +354,12 @@ validate isSAT cfg p res = case res of Unsatisfiable{} -> return res Satisfiable _ m -> case modelBindings m of - Nothing -> error "Data.SBV.validate: Impossible happaned; no bindings during model validation." + Nothing -> error "Data.SBV.validate: Impossible happaned; no bindings generated during model validation." Just env -> check env - SatExtField{} -> return $ ProofError cfg [ "Cannot validate models produced during optimization." + SatExtField{} -> return $ ProofError cfg [ "The model requires an extension field value." + , "Cannot validate models with infinities/epsilons produced during optimization." , "" - , "To turn validation off, use `cfg{validateModel = False}`" + , "To turn validation off, use `cfg{optimizeValidateConstraints = False}`" , "" , "Unable to validate the produced model." ] @@ -360,13 +380,13 @@ | not (verbose cfg) = return () | True = debug cfg ["[VALIDATE] " `alignPlain` s] - notify $ "Validating the model in the " ++ if null env then "empty environment." else "environment:" + notify $ "Validating the model. " ++ if null env then "There are no assignments." else "Assignment:" mapM_ notify [" " ++ l | l <- lines envShown] result <- snd <$> runSymbolic (Concrete (Just (isSAT, env))) ((if isSAT then forSome_ p else forAll_ p) >>= output) let explain = [ "" - , "Environment:" ++ if null env then " " else "" + , "Assignment:" ++ if null env then " " else "" ] ++ [ "" | not (null env)] ++ [ " " ++ l | l <- lines envShown] diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs --- a/Data/SBV/Provers/Yices.hs +++ b/Data/SBV/Provers/Yices.hs @@ -39,8 +39,6 @@ , supportsCustomQueries = True , supportsGlobalDecls = False , supportsDataTypes = False - , supportsDTConstructorSigs = False - , supportsDTAccessorSigs = False , supportsFlattenedModels = Nothing } } diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -39,8 +39,6 @@ , supportsCustomQueries = True , supportsGlobalDecls = True , supportsDataTypes = True - , supportsDTConstructorSigs = False - , supportsDTAccessorSigs = True , supportsFlattenedModels = Just [ "(set-option :pp.max_depth 4294967295)" , "(set-option :pp.min_alias_size 4294967295)" ] diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -710,28 +710,20 @@ lift1 o _ sbvs = error $ "SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: " ++ show (o, sbvs) -- We fully qualify the constructor with their types to work around type checking issues - -- if the solver requires it, as specified by the 'supportsDTConstructorSigs' capability. - dtConstructor fld args res = result - where body = parIfArgs (unwords (fld : map ssv args)) - parIfArgs r | null args = r - | True = "(" ++ r ++ ")" - - constructor = body - withSig = "(as " ++ constructor ++ " " ++ smtType res ++ ")" - - result | supportsDTConstructorSigs caps = withSig - | True = constructor + -- Note that this is rather bizarre, as we're tagging the constructor with its *result* type, + -- not its full function type as one would expect. But this is per the spec: Pg. 27 of SMTLib 2.6 spec + -- says: + -- + -- To simplify sort checking, a function symbol in a term can be annotated with one of its result sorts sigma. + -- + -- I wish it was the full type here not just the result, but we go with the spec. Also see: + -- and in particular + dtConstructor fld args res = "((as " ++ fld ++ " " ++ smtType res ++ ") " ++ unwords (map ssv args) ++ ")" - -- We fully qualify the accessors with their types to work around type checking issues - -- if the solver requires it, as specified by the 'supportsDTAccessorSigs' capability. + -- Similarly, we fully qualify the accessors with their types to work around type checking issues dtAccessor fld params res = result - where accessor = "(_ is " ++ fld ++ ")" - - ps = " (" ++ unwords (map smtType params) ++ ") " - withSig = "(_ is (" ++ fld ++ ps ++ smtType res ++ "))" - - result | supportsDTAccessorSigs caps = withSig - | True = accessor + where ps = " (" ++ unwords (map smtType params) ++ ") " + result = "(_ is (" ++ fld ++ ps ++ smtType res ++ "))" sh (SBVApp Ite [a, b, c]) = "(ite " ++ ssv a ++ " " ++ ssv b ++ " " ++ ssv c ++ ")" diff --git a/Data/SBV/Utils/SExpr.hs b/Data/SBV/Utils/SExpr.hs --- a/Data/SBV/Utils/SExpr.hs +++ b/Data/SBV/Utils/SExpr.hs @@ -273,6 +273,28 @@ Just sv -> go (Left sv : sofar) elseBranch _ -> Nothing + -- Catch cases like: x = a) + go sofar inner@(EApp [ECon "=", _, _]) + = go sofar (EApp [ECon "ite", inner, true, false]) + + -- Catch cases like: not x + go sofar (EApp [ECon "not", inner]) + = go sofar (EApp [ECon "ite", inner, false, true]) + + -- Catch (or x y z..) + go sofar (EApp (ECon "or" : elts)) + = let xform [] = false + xform [x] = x + xform (x:xs) = EApp [ECon "ite", x, true, xform xs] + in go sofar $ xform elts + + -- Catch (and x y z..) + go sofar (EApp (ECon "and" : elts)) + = let xform [] = true + xform [x] = x + xform (x:xs) = EApp [ECon "ite", x, xform xs, false] + in go sofar $ xform elts + -- z3 sometimes puts together a bunch of booleans as final expression, -- see if we can catch that. go sofar e @@ -281,7 +303,7 @@ -- Otherwise, just treat it as an "unknown" arbitrary expression -- as the default. It could be something arbitrary of course, but it's - -- too complicated to parse; and hopefully this is good enogh. + -- too complicated to parse; and hopefully this is good enough. go sofar e = Just $ Right e : sofar cond :: [SExpr] -> [Either ([SExpr], SExpr) SExpr] -> Maybe ([SExpr], SExpr) diff --git a/Documentation/SBV/Examples/BitPrecise/MultMask.hs b/Documentation/SBV/Examples/BitPrecise/MultMask.hs --- a/Documentation/SBV/Examples/BitPrecise/MultMask.hs +++ b/Documentation/SBV/Examples/BitPrecise/MultMask.hs @@ -43,6 +43,9 @@ -- value above will have its bits at positions @[7,15,23,31,39,47,55,63]@ moved -- to positions @[56,57,58,59,60,61,62,63]@ respectively. -- +-- NB. Depending on your z3 version, you might also get the following +-- multiplier as the result: 0x8202040810204081. That value works just fine as well! +-- -- Note that we have to send z3 custom configuration for this problem as -- otherwise it takes too long. See -- for details. diff --git a/Documentation/SBV/Examples/Existentials/Diophantine.hs b/Documentation/SBV/Examples/Existentials/Diophantine.hs --- a/Documentation/SBV/Examples/Existentials/Diophantine.hs +++ b/Documentation/SBV/Examples/Existentials/Diophantine.hs @@ -45,10 +45,10 @@ -- | Find the basis solution. By definition, the basis has all non-trivial (i.e., non-0) solutions -- that cannot be written as the sum of two other solutions. We use the mathematically equivalent --- statement that a solution is in the basis if it's least according to the lexicographic +-- statement that a solution is in the basis if it's least according to the natural partial -- order using the ordinary less-than relation. (NB. We explicitly tell z3 to use the logic -- AUFLIA for this problem, as the BV solver that is chosen automatically has a performance --- issue. See: .) +-- issue.) basis :: Maybe Int -> [[SInteger]] -> IO [[Integer]] basis mbLim m = extractModels `fmap` allSatWith z3{allSatMaxModelCount = mbLim} cond where cond = do as <- mkExistVars n diff --git a/SBVTestSuite/GoldFiles/optFloat1.gold b/SBVTestSuite/GoldFiles/optFloat1.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/optFloat1.gold +++ /dev/null @@ -1,108 +0,0 @@ -Objective "min-x": Optimal model: - x = -3.4028235e38 :: Float - 3 2 1 0 - 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 1 11111110 11111111111111111111111 - Hex: FF7F FFFF - Precision: SP - Sign: Negative - Exponent: 127 (Stored: 254, Bias: 127) - Hex-float: -0x1.fffffep127 - Value: -3.4028235e38 (NORMAL) - y = 9.351032988705757e-251 :: Double - 6 5 4 3 2 1 0 - 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 0 00011000000 0101011011001001110011000000001001101000111010000000 - Hex: 0C05 6C9C C026 8E80 - Precision: DP - Sign: Positive - Exponent: -831 (Stored: 192, Bias: 1023) - Hex-float: +0x1.56c9cc0268e8p-831 - Value: +9.351032988705757e-251 (NORMAL) - min-x = 0x00800000 :: Word32 - max-x = 0x00800000 :: Word32 - min-y = 0x8c056c9cc0268e80 :: Word64 - max-y = 0x8c056c9cc0268e80 :: Word64 -Objective "max-x": Optimal model: - x = 3.4028235e38 :: Float - 3 2 1 0 - 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 11111110 11111111111111111111111 - Hex: 7F7F FFFF - Precision: SP - Sign: Positive - Exponent: 127 (Stored: 254, Bias: 127) - Hex-float: +0x1.fffffep127 - Value: +3.4028235e38 (NORMAL) - y = 9.351032988705757e-251 :: Double - 6 5 4 3 2 1 0 - 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 0 00011000000 0101011011001001110011000000001001101000111010000000 - Hex: 0C05 6C9C C026 8E80 - Precision: DP - Sign: Positive - Exponent: -831 (Stored: 192, Bias: 1023) - Hex-float: +0x1.56c9cc0268e8p-831 - Value: +9.351032988705757e-251 (NORMAL) - min-x = 0xff7fffff :: Word32 - max-x = 0xff7fffff :: Word32 - min-y = 0x8c056c9cc0268e80 :: Word64 - max-y = 0x8c056c9cc0268e80 :: Word64 -Objective "min-y": Optimal model: - x = 3.4028235e38 :: Float - 3 2 1 0 - 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 11111110 11111111111111111111111 - Hex: 7F7F FFFF - Precision: SP - Sign: Positive - Exponent: 127 (Stored: 254, Bias: 127) - Hex-float: +0x1.fffffep127 - Value: +3.4028235e38 (NORMAL) - y = -1.7976931348623157e308 :: Double - 6 5 4 3 2 1 0 - 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 1 11111111110 1111111111111111111111111111111111111111111111111111 - Hex: FFEF FFFF FFFF FFFF - Precision: DP - Sign: Negative - Exponent: 1023 (Stored: 2046, Bias: 1023) - Hex-float: -0x1.fffffffffffffp1023 - Value: -1.7976931348623157e308 (NORMAL) - min-x = 0xff7fffff :: Word32 - max-x = 0xff7fffff :: Word32 - min-y = 0x0010000000000000 :: Word64 - max-y = 0x0010000000000000 :: Word64 -Objective "max-y": Optimal model: - x = -1.8892078e22 :: Float - 3 2 1 0 - 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 1 11001001 00000000000010010001000 - Hex: E480 0488 - Precision: SP - Sign: Negative - Exponent: 74 (Stored: 201, Bias: 127) - Hex-float: -0x1.00091p74 - Value: -1.8892078e22 (NORMAL) - y = 1.7976931348623157e308 :: Double - 6 5 4 3 2 1 0 - 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 0 11111111110 1111111111111111111111111111111111111111111111111111 - Hex: 7FEF FFFF FFFF FFFF - Precision: DP - Sign: Positive - Exponent: 1023 (Stored: 2046, Bias: 1023) - Hex-float: +0x1.fffffffffffffp1023 - Value: +1.7976931348623157e308 (NORMAL) - min-x = 0x1b7ffb77 :: Word32 - max-x = 0x1b7ffb77 :: Word32 - min-y = 0xffefffffffffffff :: Word64 - max-y = 0xffefffffffffffff :: Word64 diff --git a/SBVTestSuite/GoldFiles/optFloat1a.gold b/SBVTestSuite/GoldFiles/optFloat1a.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optFloat1a.gold @@ -0,0 +1,13 @@ +Optimal model: + x = -3.4028235e38 :: Float + 3 2 1 0 + 1 09876543 21098765432109876543210 + S ---E8--- ----------F23---------- + Binary: 1 11111110 11111111111111111111111 + Hex: FF7F FFFF + Precision: SP + Sign: Negative + Exponent: 127 (Stored: 254, Bias: 127) + Hex-float: -0x1.fffffep127 + Value: -3.4028235e38 (NORMAL) + min-x = 0x00800000 :: Word32 diff --git a/SBVTestSuite/GoldFiles/optFloat1b.gold b/SBVTestSuite/GoldFiles/optFloat1b.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optFloat1b.gold @@ -0,0 +1,13 @@ +Optimal model: + x = -Infinity :: Float + 3 2 1 0 + 1 09876543 21098765432109876543210 + S ---E8--- ----------F23---------- + Binary: 1 11111111 00000000000000000000000 + Hex: FF80 0000 + Precision: SP + Sign: Negative + Exponent: 128 (Stored: 255, Bias: 127) + Hex-float: -Infinity + Value: -Infinity + min-x = 0x007fffff :: Word32 diff --git a/SBVTestSuite/GoldFiles/optFloat1c.gold b/SBVTestSuite/GoldFiles/optFloat1c.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optFloat1c.gold @@ -0,0 +1,13 @@ +Optimal model: + x = 3.4028235e38 :: Float + 3 2 1 0 + 1 09876543 21098765432109876543210 + S ---E8--- ----------F23---------- + Binary: 0 11111110 11111111111111111111111 + Hex: 7F7F FFFF + Precision: SP + Sign: Positive + Exponent: 127 (Stored: 254, Bias: 127) + Hex-float: +0x1.fffffep127 + Value: +3.4028235e38 (NORMAL) + max-x = 0xff7fffff :: Word32 diff --git a/SBVTestSuite/GoldFiles/optFloat1d.gold b/SBVTestSuite/GoldFiles/optFloat1d.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optFloat1d.gold @@ -0,0 +1,13 @@ +Optimal model: + x = Infinity :: Float + 3 2 1 0 + 1 09876543 21098765432109876543210 + S ---E8--- ----------F23---------- + Binary: 0 11111111 00000000000000000000000 + Hex: 7F80 0000 + Precision: SP + Sign: Positive + Exponent: 128 (Stored: 255, Bias: 127) + Hex-float: +Infinity + Value: +Infinity + max-y = 0xff800000 :: Word32 diff --git a/SBVTestSuite/GoldFiles/optFloat2.gold b/SBVTestSuite/GoldFiles/optFloat2.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/optFloat2.gold +++ /dev/null @@ -1,108 +0,0 @@ -Objective "min-x": Optimal model: - x = -Infinity :: Float - 3 2 1 0 - 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 1 11111111 00000000000000000000000 - Hex: FF80 0000 - Precision: SP - Sign: Negative - Exponent: 128 (Stored: 255, Bias: 127) - Hex-float: -Infinity - Value: -Infinity - y = 5.854952310409896e-270 :: Double - 6 5 4 3 2 1 0 - 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 0 00010000000 1000101111101011111111001111010011101011010010001101 - Hex: 0808 BEBF CF4E B48D - Precision: DP - Sign: Positive - Exponent: -895 (Stored: 128, Bias: 1023) - Hex-float: +0x1.8bebfcf4eb48dp-895 - Value: +5.854952310409896e-270 (NORMAL) - min-x = 0x007fffff :: Word32 - max-x = 0x007fffff :: Word32 - min-y = 0x8808bebfcf4eb48d :: Word64 - max-y = 0x8808bebfcf4eb48d :: Word64 -Objective "max-x": Optimal model: - x = Infinity :: Float - 3 2 1 0 - 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 11111111 00000000000000000000000 - Hex: 7F80 0000 - Precision: SP - Sign: Positive - Exponent: 128 (Stored: 255, Bias: 127) - Hex-float: +Infinity - Value: +Infinity - y = 5.854923399093713e-270 :: Double - 6 5 4 3 2 1 0 - 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 0 00010000000 1000101111101011011111001101010011101011010010000101 - Hex: 0808 BEB7 CD4E B485 - Precision: DP - Sign: Positive - Exponent: -895 (Stored: 128, Bias: 1023) - Hex-float: +0x1.8beb7cd4eb485p-895 - Value: +5.854923399093713e-270 (NORMAL) - min-x = 0xff800000 :: Word32 - max-x = 0xff800000 :: Word32 - min-y = 0x8808beb7cd4eb485 :: Word64 - max-y = 0x8808beb7cd4eb485 :: Word64 -Objective "min-y": Optimal model: - x = 1.7237e-41 :: Float - 3 2 1 0 - 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 00000000 00000000011000000001101 - Hex: 0000 300D - Precision: SP - Sign: Positive - Exponent: -126 (Stored: 0, Bias: 126) - Hex-float: +0x1.8068p-136 - Value: +1.7237e-41 (DENORMAL) - y = -Infinity :: Double - 6 5 4 3 2 1 0 - 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 1 11111111111 0000000000000000000000000000000000000000000000000000 - Hex: FFF0 0000 0000 0000 - Precision: DP - Sign: Negative - Exponent: 1024 (Stored: 2047, Bias: 1023) - Hex-float: -Infinity - Value: -Infinity - min-x = 0x8000300d :: Word32 - max-x = 0x8000300d :: Word32 - min-y = 0x000fffffffffffff :: Word64 - max-y = 0x000fffffffffffff :: Word64 -Objective "max-y": Optimal model: - x = 1.7237e-41 :: Float - 3 2 1 0 - 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 00000000 00000000011000000001101 - Hex: 0000 300D - Precision: SP - Sign: Positive - Exponent: -126 (Stored: 0, Bias: 126) - Hex-float: +0x1.8068p-136 - Value: +1.7237e-41 (DENORMAL) - y = Infinity :: Double - 6 5 4 3 2 1 0 - 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 0 11111111111 0000000000000000000000000000000000000000000000000000 - Hex: 7FF0 0000 0000 0000 - Precision: DP - Sign: Positive - Exponent: 1024 (Stored: 2047, Bias: 1023) - Hex-float: +Infinity - Value: +Infinity - min-x = 0x8000300d :: Word32 - max-x = 0x8000300d :: Word32 - min-y = 0xfff0000000000000 :: Word64 - max-y = 0xfff0000000000000 :: Word64 diff --git a/SBVTestSuite/GoldFiles/optFloat2a.gold b/SBVTestSuite/GoldFiles/optFloat2a.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optFloat2a.gold @@ -0,0 +1,13 @@ +Optimal model: + x = -1.7976931348623157e308 :: Double + 6 5 4 3 2 1 0 + 3 21098765432 1098765432109876543210987654321098765432109876543210 + S ----E11---- ------------------------F52------------------------- + Binary: 1 11111111110 1111111111111111111111111111111111111111111111111111 + Hex: FFEF FFFF FFFF FFFF + Precision: DP + Sign: Negative + Exponent: 1023 (Stored: 2046, Bias: 1023) + Hex-float: -0x1.fffffffffffffp1023 + Value: -1.7976931348623157e308 (NORMAL) + min-x = 0x0010000000000000 :: Word64 diff --git a/SBVTestSuite/GoldFiles/optFloat2b.gold b/SBVTestSuite/GoldFiles/optFloat2b.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optFloat2b.gold @@ -0,0 +1,13 @@ +Optimal model: + x = -Infinity :: Double + 6 5 4 3 2 1 0 + 3 21098765432 1098765432109876543210987654321098765432109876543210 + S ----E11---- ------------------------F52------------------------- + Binary: 1 11111111111 0000000000000000000000000000000000000000000000000000 + Hex: FFF0 0000 0000 0000 + Precision: DP + Sign: Negative + Exponent: 1024 (Stored: 2047, Bias: 1023) + Hex-float: -Infinity + Value: -Infinity + min-x = 0x000fffffffffffff :: Word64 diff --git a/SBVTestSuite/GoldFiles/optFloat2c.gold b/SBVTestSuite/GoldFiles/optFloat2c.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optFloat2c.gold @@ -0,0 +1,13 @@ +Optimal model: + x = 1.7976931348623157e308 :: Double + 6 5 4 3 2 1 0 + 3 21098765432 1098765432109876543210987654321098765432109876543210 + S ----E11---- ------------------------F52------------------------- + Binary: 0 11111111110 1111111111111111111111111111111111111111111111111111 + Hex: 7FEF FFFF FFFF FFFF + Precision: DP + Sign: Positive + Exponent: 1023 (Stored: 2046, Bias: 1023) + Hex-float: +0x1.fffffffffffffp1023 + Value: +1.7976931348623157e308 (NORMAL) + max-x = 0xffefffffffffffff :: Word64 diff --git a/SBVTestSuite/GoldFiles/optFloat2d.gold b/SBVTestSuite/GoldFiles/optFloat2d.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optFloat2d.gold @@ -0,0 +1,13 @@ +Optimal model: + x = Infinity :: Double + 6 5 4 3 2 1 0 + 3 21098765432 1098765432109876543210987654321098765432109876543210 + S ----E11---- ------------------------F52------------------------- + Binary: 0 11111111111 0000000000000000000000000000000000000000000000000000 + Hex: 7FF0 0000 0000 0000 + Precision: DP + Sign: Positive + Exponent: 1024 (Stored: 2047, Bias: 1023) + Hex-float: +Infinity + Value: +Infinity + max-y = 0xfff0000000000000 :: Word64 diff --git a/SBVTestSuite/GoldFiles/quantified_prove_existsexists_contradiction_p.gold b/SBVTestSuite/GoldFiles/quantified_prove_existsexists_contradiction_p.gold --- a/SBVTestSuite/GoldFiles/quantified_prove_existsexists_contradiction_p.gold +++ b/SBVTestSuite/GoldFiles/quantified_prove_existsexists_contradiction_p.gold @@ -25,5 +25,6 @@ (not s4)))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/quantified_prove_existsforall_contradiction_p.gold b/SBVTestSuite/GoldFiles/quantified_prove_existsforall_contradiction_p.gold --- a/SBVTestSuite/GoldFiles/quantified_prove_existsforall_contradiction_p.gold +++ b/SBVTestSuite/GoldFiles/quantified_prove_existsforall_contradiction_p.gold @@ -25,5 +25,6 @@ (not s4)))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/quantified_prove_existsforall_satisfiable_p.gold b/SBVTestSuite/GoldFiles/quantified_prove_existsforall_satisfiable_p.gold --- a/SBVTestSuite/GoldFiles/quantified_prove_existsforall_satisfiable_p.gold +++ b/SBVTestSuite/GoldFiles/quantified_prove_existsforall_satisfiable_p.gold @@ -25,5 +25,6 @@ (not s4))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/quantified_prove_forallexists_contradiction_p.gold b/SBVTestSuite/GoldFiles/quantified_prove_forallexists_contradiction_p.gold --- a/SBVTestSuite/GoldFiles/quantified_prove_forallexists_contradiction_p.gold +++ b/SBVTestSuite/GoldFiles/quantified_prove_forallexists_contradiction_p.gold @@ -25,6 +25,7 @@ (not s4)))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. [SEND] (get-value (s0)) [RECV] ((s0 #x00)) *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_c.gold b/SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_c.gold --- a/SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_c.gold +++ b/SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_c.gold @@ -25,6 +25,7 @@ s4))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. [SEND] (get-value (s0)) [RECV] ((s0 #x00)) *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_p.gold b/SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_p.gold --- a/SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_p.gold +++ b/SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_p.gold @@ -25,6 +25,7 @@ s4))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. [SEND] (get-value (s0)) [RECV] ((s0 #x00)) *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_c.gold b/SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_c.gold --- a/SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_c.gold +++ b/SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_c.gold @@ -25,5 +25,6 @@ s4)))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_p.gold b/SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_p.gold --- a/SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_p.gold +++ b/SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_p.gold @@ -25,5 +25,6 @@ s4)))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_c.gold b/SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_c.gold --- a/SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_c.gold +++ b/SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_c.gold @@ -25,5 +25,6 @@ s4))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_p.gold b/SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_p.gold --- a/SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_p.gold +++ b/SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_p.gold @@ -25,5 +25,6 @@ s4))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_c.gold b/SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_c.gold --- a/SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_c.gold +++ b/SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_c.gold @@ -25,5 +25,6 @@ s4))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_p.gold b/SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_p.gold --- a/SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_p.gold +++ b/SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_p.gold @@ -25,5 +25,6 @@ s4))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/query_uisatex2.gold b/SBVTestSuite/GoldFiles/query_uisatex2.gold --- a/SBVTestSuite/GoldFiles/query_uisatex2.gold +++ b/SBVTestSuite/GoldFiles/query_uisatex2.gold @@ -152,7 +152,7 @@ 21 7))))) [SEND] (get-value (q6)) -[RECV] ((q6 (lambda ((x!1 Int)) false))) +[RECV] ((q6 ((as const Array) false))) *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/set_uninterp1.gold b/SBVTestSuite/GoldFiles/set_uninterp1.gold --- a/SBVTestSuite/GoldFiles/set_uninterp1.gold +++ b/SBVTestSuite/GoldFiles/set_uninterp1.gold @@ -38,7 +38,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store ((as const (Array E Bool)) false) B true))) +[RECV] ((s0 (lambda ((x!1 E)) (= x!1 B)))) [GOOD] (define-fun s4 () (Array E Bool) (store ((as const (Array E Bool)) false) B true)) [GOOD] (define-fun s5 () Bool (= s0 s4)) [GOOD] (define-fun s6 () Bool (not s5)) @@ -47,7 +47,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) A true))) +[RECV] ((s0 (lambda ((x!1 E)) (or (= x!1 B) (= x!1 A))))) [GOOD] (define-fun s7 () (Array E Bool) (store (store ((as const (Array E Bool)) false) B true) A true)) [GOOD] (define-fun s8 () Bool (= s0 s7)) [GOOD] (define-fun s9 () Bool (not s8)) @@ -56,7 +56,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store (store (store ((as const (Array E Bool)) false) B true) C true) A true))) +[RECV] ((s0 (lambda ((x!1 E)) (or (= x!1 B) (= x!1 C) (= x!1 A))))) [GOOD] (define-fun s10 () (Array E Bool) (store (store (store ((as const (Array E Bool)) false) C true) B true) A true)) [GOOD] (define-fun s11 () Bool (= s0 s10)) [GOOD] (define-fun s12 () Bool (not s11)) @@ -65,7 +65,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) C true))) +[RECV] ((s0 (lambda ((x!1 E)) (or (= x!1 B) (= x!1 C))))) [GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) B true)) [GOOD] (define-fun s14 () Bool (= s0 s13)) [GOOD] (define-fun s15 () Bool (not s14)) @@ -74,7 +74,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store ((as const (Array E Bool)) false) A true))) +[RECV] ((s0 (lambda ((x!1 E)) (= x!1 A)))) [GOOD] (define-fun s16 () (Array E Bool) (store ((as const (Array E Bool)) false) A true)) [GOOD] (define-fun s17 () Bool (= s0 s16)) [GOOD] (define-fun s18 () Bool (not s17)) @@ -83,8 +83,8 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) A true))) -[GOOD] (define-fun s19 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) A true)) +[RECV] ((s0 (lambda ((x!1 E)) (= x!1 C)))) +[GOOD] (define-fun s19 () (Array E Bool) (store ((as const (Array E Bool)) false) C true)) [GOOD] (define-fun s20 () Bool (= s0 s19)) [GOOD] (define-fun s21 () Bool (not s20)) [GOOD] (assert s21) @@ -92,8 +92,8 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store ((as const (Array E Bool)) false) C true))) -[GOOD] (define-fun s22 () (Array E Bool) (store ((as const (Array E Bool)) false) C true)) +[RECV] ((s0 (lambda ((x!1 E)) (or (= x!1 A) (= x!1 C))))) +[GOOD] (define-fun s22 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) A true)) [GOOD] (define-fun s23 () Bool (= s0 s22)) [GOOD] (define-fun s24 () Bool (not s23)) [GOOD] (assert s24) @@ -117,8 +117,8 @@ Solution #6: s0 = {A} :: {E} Solution #7: - s0 = {A,C} :: {E} -Solution #8: s0 = {C} :: {E} +Solution #8: + s0 = {A,C} :: {E} Found 8 different solutions. DONE! diff --git a/SBVTestSuite/GoldFiles/sumBimapPlus.gold b/SBVTestSuite/GoldFiles/sumBimapPlus.gold --- a/SBVTestSuite/GoldFiles/sumBimapPlus.gold +++ b/SBVTestSuite/GoldFiles/sumBimapPlus.gold @@ -26,10 +26,10 @@ [GOOD] ; --- formula --- [GOOD] (define-fun s1 () Int (get_left_SBVEither s0)) [GOOD] (define-fun s3 () Int (+ s1 s2)) -[GOOD] (define-fun s4 () (SBVEither Int Int) (left_SBVEither s3)) +[GOOD] (define-fun s4 () (SBVEither Int Int) ((as left_SBVEither (SBVEither Int Int)) s3)) [GOOD] (define-fun s5 () Int (get_right_SBVEither s0)) [GOOD] (define-fun s6 () Int (+ s2 s5)) -[GOOD] (define-fun s7 () (SBVEither Int Int) (right_SBVEither s6)) +[GOOD] (define-fun s7 () (SBVEither Int Int) ((as right_SBVEither (SBVEither Int Int)) s6)) [GOOD] (define-fun s8 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int Int))) s0)) [GOOD] (define-fun s9 () (SBVEither Int Int) (ite s8 s4 s7)) [GOOD] (define-fun s10 () Int (get_left_SBVEither s9)) diff --git a/SBVTestSuite/GoldFiles/sumLiftEither.gold b/SBVTestSuite/GoldFiles/sumLiftEither.gold --- a/SBVTestSuite/GoldFiles/sumLiftEither.gold +++ b/SBVTestSuite/GoldFiles/sumLiftEither.gold @@ -24,10 +24,10 @@ [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula --- -[GOOD] (define-fun s2 () (SBVEither Int (_ BitVec 8)) (left_SBVEither s0)) +[GOOD] (define-fun s2 () (SBVEither Int (_ BitVec 8)) ((as left_SBVEither (SBVEither Int (_ BitVec 8))) s0)) [GOOD] (define-fun s3 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s2)) [GOOD] (define-fun s4 () Bool (ite s3 true false)) -[GOOD] (define-fun s5 () (SBVEither Int (_ BitVec 8)) (right_SBVEither s1)) +[GOOD] (define-fun s5 () (SBVEither Int (_ BitVec 8)) ((as right_SBVEither (SBVEither Int (_ BitVec 8))) s1)) [GOOD] (define-fun s6 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s5)) [GOOD] (define-fun s7 () Bool (ite s6 false true)) [GOOD] (assert s4) diff --git a/SBVTestSuite/GoldFiles/sumLiftMaybe.gold b/SBVTestSuite/GoldFiles/sumLiftMaybe.gold --- a/SBVTestSuite/GoldFiles/sumLiftMaybe.gold +++ b/SBVTestSuite/GoldFiles/sumLiftMaybe.gold @@ -24,7 +24,7 @@ [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula --- -[GOOD] (define-fun s1 () (SBVMaybe Int) (just_SBVMaybe s0)) +[GOOD] (define-fun s1 () (SBVMaybe Int) ((as just_SBVMaybe (SBVMaybe Int)) s0)) [GOOD] (define-fun s3 () Bool (distinct s1 s2)) [GOOD] (assert s3) [SEND] (check-sat) diff --git a/SBVTestSuite/GoldFiles/sumMaybe.gold b/SBVTestSuite/GoldFiles/sumMaybe.gold --- a/SBVTestSuite/GoldFiles/sumMaybe.gold +++ b/SBVTestSuite/GoldFiles/sumMaybe.gold @@ -30,7 +30,7 @@ [GOOD] (define-fun s2 () Bool (ite s1 true false)) [GOOD] (define-fun s4 () Int (get_just_SBVMaybe s0)) [GOOD] (define-fun s6 () Int (+ s4 s5)) -[GOOD] (define-fun s7 () (SBVMaybe Int) (just_SBVMaybe s6)) +[GOOD] (define-fun s7 () (SBVMaybe Int) ((as just_SBVMaybe (SBVMaybe Int)) s6)) [GOOD] (define-fun s8 () (SBVMaybe Int) (ite s1 s3 s7)) [GOOD] (define-fun s9 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe Int))) s8)) [GOOD] (define-fun s10 () Bool (ite s9 true false)) diff --git a/SBVTestSuite/GoldFiles/uiSat_test1.gold b/SBVTestSuite/GoldFiles/uiSat_test1.gold --- a/SBVTestSuite/GoldFiles/uiSat_test1.gold +++ b/SBVTestSuite/GoldFiles/uiSat_test1.gold @@ -26,7 +26,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [GOOD] (define-fun q1_model1 ((x!0 Bool)) Bool false ) @@ -40,7 +40,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [GOOD] (define-fun q1_model2 ((x!0 Bool)) Bool true ) @@ -56,8 +56,8 @@ [SEND] (get-value (q1)) [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [GOOD] (define-fun q1_model3 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model3_reject () Bool (exists ((x!0 Bool)) @@ -94,8 +94,8 @@ q1 _ = True Solution #3: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True Solution #4: q1 :: Bool -> Bool q1 True = True diff --git a/SBVTestSuite/GoldFiles/uiSat_test2.gold b/SBVTestSuite/GoldFiles/uiSat_test2.gold --- a/SBVTestSuite/GoldFiles/uiSat_test2.gold +++ b/SBVTestSuite/GoldFiles/uiSat_test2.gold @@ -26,7 +26,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) false))) +[RECV] ((q2 ((as const Array) false))) [GOOD] (define-fun q2_model1 ((x!0 Bool) (x!1 Bool)) Bool false ) @@ -40,7 +40,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) true))) +[RECV] ((q2 ((as const Array) true))) [GOOD] (define-fun q2_model2 ((x!0 Bool) (x!1 Bool)) Bool true ) @@ -55,14 +55,6 @@ [RECV] sat [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) (not x!2)))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) false)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q2_model3 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 false) (= x!1 false)) false true) @@ -78,6 +70,14 @@ [RECV] sat [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2)))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) true)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q2_model4 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 false) (= x!1 true)) true false) @@ -93,6 +93,14 @@ [RECV] sat [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2)))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) true)) [GOOD] (define-fun q2_model5 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 true) (= x!1 true)) true false) @@ -132,6 +140,14 @@ [RECV] sat [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 (not x!2))))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) true)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q2_model7 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 true) (= x!1 false)) true false) @@ -195,6 +211,14 @@ [RECV] sat [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2))))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) true)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q2_model10 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 false) (= x!1 false)) true false) @@ -210,14 +234,6 @@ [RECV] sat [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) x!2))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) false)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q2_model11 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 false) (= x!1 true)) false true) @@ -308,14 +324,6 @@ [RECV] sat [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 (not x!2)))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) false)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q2_model15 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 true) (= x!1 false)) false true) @@ -331,14 +339,6 @@ [RECV] sat [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 x!2))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) false)) [GOOD] (define-fun q2_model16 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 true) (= x!1 true)) false true) diff --git a/SBVTestSuite/GoldFiles/uiSat_test3.gold b/SBVTestSuite/GoldFiles/uiSat_test3.gold --- a/SBVTestSuite/GoldFiles/uiSat_test3.gold +++ b/SBVTestSuite/GoldFiles/uiSat_test3.gold @@ -28,9 +28,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) false))) +[RECV] ((q2 ((as const Array) false))) [GOOD] (define-fun q1_model1 ((x!0 Bool)) Bool false ) @@ -54,9 +54,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) false))) +[RECV] ((q2 ((as const Array) false))) [GOOD] (define-fun q1_model2 ((x!0 Bool)) Bool true ) @@ -80,9 +80,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) true))) +[RECV] ((q2 ((as const Array) true))) [GOOD] (define-fun q1_model3 ((x!0 Bool)) Bool false ) @@ -106,17 +106,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 (not x!2)))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) false)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model4 ((x!0 Bool)) Bool false ) @@ -144,14 +136,6 @@ [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 (not x!2)))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) false)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model5 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -180,6 +164,14 @@ [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2))))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) true)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model6 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -245,14 +237,6 @@ [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) x!2))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) false)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model8 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -278,17 +262,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) x!2))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) false)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model9 ((x!0 Bool)) Bool false ) @@ -351,7 +327,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not (and x!1 x!2)) (not (and (not x!1) x!2)))))) @@ -401,8 +377,8 @@ [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model12 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model12_reject () Bool (exists ((x!0 Bool)) @@ -426,7 +402,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not (and x!1 x!2)) (not (and (not x!1) x!2)))))) @@ -463,17 +439,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) x!2))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) false)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model14 ((x!0 Bool)) Bool true ) @@ -501,17 +469,9 @@ [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) x!2))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) false)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model15 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model15_reject () Bool (exists ((x!0 Bool)) @@ -537,17 +497,9 @@ [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 x!2))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model16 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model16_reject () Bool (exists ((x!0 Bool)) @@ -573,14 +525,6 @@ [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 x!2))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model17 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -608,7 +552,7 @@ [SEND] (get-value (q1)) [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) true))) +[RECV] ((q2 ((as const Array) true))) [GOOD] (define-fun q1_model18 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -635,10 +579,10 @@ [SEND] (get-value (q1)) [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) true))) +[RECV] ((q2 ((as const Array) true))) [GOOD] (define-fun q1_model19 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model19_reject () Bool (exists ((x!0 Bool)) @@ -660,9 +604,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) true))) +[RECV] ((q2 ((as const Array) true))) [GOOD] (define-fun q1_model20 ((x!0 Bool)) Bool true ) @@ -686,17 +630,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 x!2))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model21 ((x!0 Bool)) Bool false ) @@ -721,17 +657,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 x!2))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model22 ((x!0 Bool)) Bool true ) @@ -756,17 +684,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) (not x!2)))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) false)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model23 ((x!0 Bool)) Bool false ) @@ -793,7 +713,7 @@ [SEND] (get-value (q1)) [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) false))) +[RECV] ((q2 ((as const Array) false))) [GOOD] (define-fun q1_model24 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -821,6 +741,14 @@ [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 (not x!2))))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) true)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model25 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -849,14 +777,6 @@ [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) (not x!2)))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) false)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model26 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -923,6 +843,14 @@ [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2)))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) true)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model28 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -951,6 +879,14 @@ [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2)))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model29 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -976,9 +912,17 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 (not x!2))))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) true)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model30 ((x!0 Bool)) Bool false ) @@ -1003,9 +947,17 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2)))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) true)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model31 ((x!0 Bool)) Bool false ) @@ -1030,7 +982,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and (not x!1) x!2))))) [SEND] (get-value ((q2 false false))) @@ -1103,9 +1055,17 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2)))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model34 ((x!0 Bool)) Bool false ) @@ -1130,7 +1090,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 (not x!2)) (and x!1 x!2))))) [SEND] (get-value ((q2 false false))) @@ -1206,9 +1166,17 @@ [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2)))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) true)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model37 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model37_reject () Bool (exists ((x!0 Bool)) @@ -1234,17 +1202,9 @@ [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) (not x!2)))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) false)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model38 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model38_reject () Bool (exists ((x!0 Bool)) @@ -1280,8 +1240,8 @@ [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model39 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model39_reject () Bool (exists ((x!0 Bool)) @@ -1305,7 +1265,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not (and x!1 x!2)) (not (and (not x!1) (not x!2))))))) @@ -1342,17 +1302,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) (not x!2)))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) false)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model41 ((x!0 Bool)) Bool true ) @@ -1377,9 +1329,17 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2)))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) true)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model42 ((x!0 Bool)) Bool true ) @@ -1404,7 +1364,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and (not x!1) x!2))))) [SEND] (get-value ((q2 false false))) @@ -1453,8 +1413,8 @@ [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model44 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model44_reject () Bool (exists ((x!0 Bool)) @@ -1481,17 +1441,9 @@ [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 (not x!2)))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) false)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model45 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model45_reject () Bool (exists ((x!0 Bool)) @@ -1514,17 +1466,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 (not x!2)))))) -[SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) -[SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) false)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model46 ((x!0 Bool)) Bool true ) @@ -1549,7 +1493,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not (and x!1 x!2)) (not (and x!1 (not x!2))))))) @@ -1586,9 +1530,17 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2))))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) true)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model48 ((x!0 Bool)) Bool true ) @@ -1613,7 +1565,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and (not x!1) (not x!2)))))) [SEND] (get-value ((q2 false false))) @@ -1661,8 +1613,8 @@ [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model50 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model50_reject () Bool (exists ((x!0 Bool)) @@ -1689,9 +1641,17 @@ [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2))))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) true)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model51 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model51_reject () Bool (exists ((x!0 Bool)) @@ -1727,8 +1687,8 @@ [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model52 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model52_reject () Bool (exists ((x!0 Bool)) @@ -1752,9 +1712,17 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2)))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model53 ((x!0 Bool)) Bool true ) @@ -1779,7 +1747,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not (and (not x!1) (not x!2))) (not (and x!1 x!2)))))) @@ -1819,9 +1787,17 @@ [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2)))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model55 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model55_reject () Bool (exists ((x!0 Bool)) @@ -1847,9 +1823,17 @@ [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 (not x!2))))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) true)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model56 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model56_reject () Bool (exists ((x!0 Bool)) @@ -1872,9 +1856,17 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 (not x!2))))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) false)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) true)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model57 ((x!0 Bool)) Bool true ) @@ -1899,7 +1891,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) true))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and x!1 (not x!2)))))) [SEND] (get-value ((q2 false false))) @@ -1947,8 +1939,8 @@ [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model59 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model59_reject () Bool (exists ((x!0 Bool)) @@ -1974,10 +1966,10 @@ [SEND] (get-value (q1)) [RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) false))) +[RECV] ((q2 ((as const Array) false))) [GOOD] (define-fun q1_model60 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model60_reject () Bool (exists ((x!0 Bool)) @@ -1999,9 +1991,17 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2))))) +[SEND] (get-value ((q2 false false))) +[RECV] (((q2 false false) true)) +[SEND] (get-value ((q2 false true))) +[RECV] (((q2 false true) false)) +[SEND] (get-value ((q2 true false))) +[RECV] (((q2 true false) false)) +[SEND] (get-value ((q2 true true))) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model61 ((x!0 Bool)) Bool false ) @@ -2064,7 +2064,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and (not x!1) (not x!2)) (and (not x!1) x!2))))) @@ -2101,7 +2101,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and (not x!1) (not x!2)))))) [SEND] (get-value ((q2 false false))) @@ -2223,8 +2223,8 @@ q2 _ _ = False Solution #12: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False False = True @@ -2247,16 +2247,16 @@ q2 _ _ = True Solution #15: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False True = False q2 _ _ = True Solution #16: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 True True = False @@ -2278,8 +2278,8 @@ q2 _ _ = True Solution #19: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 _ _ = True @@ -2415,24 +2415,24 @@ q2 _ _ = False Solution #37: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False True = True q2 _ _ = False Solution #38: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False False = False q2 _ _ = True Solution #39: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False True = True @@ -2470,8 +2470,8 @@ q2 _ _ = False Solution #44: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False True = True @@ -2479,8 +2479,8 @@ q2 _ _ = False Solution #45: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 True False = False @@ -2517,8 +2517,8 @@ q2 _ _ = False Solution #50: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False False = True @@ -2526,16 +2526,16 @@ q2 _ _ = False Solution #51: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False False = True q2 _ _ = False Solution #52: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False False = True @@ -2558,16 +2558,16 @@ q2 _ _ = False Solution #55: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 True True = True q2 _ _ = False Solution #56: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 True False = True @@ -2589,8 +2589,8 @@ q2 _ _ = False Solution #59: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 True False = True @@ -2598,8 +2598,8 @@ q2 _ _ = False Solution #60: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 _ _ = False diff --git a/SBVTestSuite/GoldFiles/validate_0.gold b/SBVTestSuite/GoldFiles/validate_0.gold --- a/SBVTestSuite/GoldFiles/validate_0.gold +++ b/SBVTestSuite/GoldFiles/validate_0.gold @@ -27,7 +27,7 @@ [RECV] ((s0 #xff)) *** Solver : ABC *** Exit code: ExitSuccess -[VALIDATE] Validating the model in the environment: +[VALIDATE] Validating the model. Assignment: [VALIDATE] x = 255 :: Word8 [VALIDATE] There are no constraints to check. [VALIDATE] Validating outputs. @@ -35,7 +35,7 @@ FINAL OUTPUT: *** Data.SBV: Model validation failure: Final output evaluated to False. *** -*** Environment: +*** Assignment: *** *** x = 255 :: Word8 *** diff --git a/SBVTestSuite/GoldFiles/validate_1.gold b/SBVTestSuite/GoldFiles/validate_1.gold --- a/SBVTestSuite/GoldFiles/validate_1.gold +++ b/SBVTestSuite/GoldFiles/validate_1.gold @@ -28,7 +28,7 @@ [RECV] ((s0 (_ +zero 8 24))) *** Solver : Z3 *** Exit code: ExitSuccess -[VALIDATE] Validating the model in the environment: +[VALIDATE] Validating the model. Assignment: [VALIDATE] x = 0.0 :: Float [VALIDATE] There are no constraints to check. [VALIDATE] Validating outputs. @@ -36,7 +36,7 @@ FINAL OUTPUT: *** Data.SBV: Cannot validate the model, since s4 is not concretely computable. *** -*** Environment: +*** Assignment: *** *** x = 0.0 :: Float *** diff --git a/SBVTestSuite/GoldFiles/validate_2.gold b/SBVTestSuite/GoldFiles/validate_2.gold --- a/SBVTestSuite/GoldFiles/validate_2.gold +++ b/SBVTestSuite/GoldFiles/validate_2.gold @@ -28,7 +28,7 @@ [RECV] ((s0 (fp #b0 #x40 #b00000001000000000010000))) *** Solver : Z3 *** Exit code: ExitSuccess -[VALIDATE] Validating the model in the environment: +[VALIDATE] Validating the model. Assignment: [VALIDATE] x = 1.0884394e-19 :: Float [VALIDATE] There are no constraints to check. [VALIDATE] Validating outputs. @@ -36,7 +36,7 @@ FINAL OUTPUT: *** Data.SBV: Cannot validate the model, since s4 is not concretely computable. *** -*** Environment: +*** Assignment: *** *** x = 1.0884394e-19 :: Float *** diff --git a/SBVTestSuite/GoldFiles/validate_5.gold b/SBVTestSuite/GoldFiles/validate_5.gold --- a/SBVTestSuite/GoldFiles/validate_5.gold +++ b/SBVTestSuite/GoldFiles/validate_5.gold @@ -36,7 +36,7 @@ [RECV] ((s1 10)) *** Solver : Z3 *** Exit code: ExitSuccess -[VALIDATE] Validating the model in the environment: +[VALIDATE] Validating the model. Assignment: [VALIDATE] x = 13 :: Integer [VALIDATE] y = 10 :: Integer [VALIDATE] Validating 2 constraint(s). diff --git a/SBVTestSuite/GoldFiles/validate_6.gold b/SBVTestSuite/GoldFiles/validate_6.gold --- a/SBVTestSuite/GoldFiles/validate_6.gold +++ b/SBVTestSuite/GoldFiles/validate_6.gold @@ -36,7 +36,7 @@ [RECV] ((s1 11)) *** Solver : Z3 *** Exit code: ExitSuccess -[VALIDATE] Validating the model in the environment: +[VALIDATE] Validating the model. Assignment: [VALIDATE] x = 13 :: Integer [VALIDATE] y = 11 :: Integer [VALIDATE] Validating 2 constraint(s). diff --git a/SBVTestSuite/GoldFiles/validate_7.gold b/SBVTestSuite/GoldFiles/validate_7.gold --- a/SBVTestSuite/GoldFiles/validate_7.gold +++ b/SBVTestSuite/GoldFiles/validate_7.gold @@ -29,11 +29,12 @@ s8))))))))) [SEND] (check-sat) [RECV] sat +*** In a quantified context, obvservables will not be printed. [SEND] (get-value (s0)) [RECV] ((s0 (_ -oo 8 24))) *** Solver : Z3 *** Exit code: ExitSuccess -[VALIDATE] Validating the model in the environment: +[VALIDATE] Validating the model. Assignment: [VALIDATE] x = -Infinity :: Float [VALIDATE] y = :: Float diff --git a/SBVTestSuite/TestSuite/Optimization/Floats.hs b/SBVTestSuite/TestSuite/Optimization/Floats.hs --- a/SBVTestSuite/TestSuite/Optimization/Floats.hs +++ b/SBVTestSuite/TestSuite/Optimization/Floats.hs @@ -19,23 +19,31 @@ tests :: TestTree tests = testGroup "Optimization.Floats" - [ goldenVsStringShow "optFloat1" $ optimizeWith z3{printBase=16} Independent (p True) - , goldenVsStringShow "optFloat2" $ optimizeWith z3{printBase=16} Independent (p False) - , goldenVsStringShow "optFloat3" $ optimizeWith z3{printBase=16} Lexicographic q - , goldenVsStringShow "optFloat4" $ optimizeWith z3{printBase=16} Lexicographic r + [ goldenVsStringShow "optFloat1a" $ optimizeWith z3{printBase=16} Lexicographic (floatMinMax (minimize "min-x") True) + , goldenVsStringShow "optFloat1b" $ optimizeWith z3{printBase=16} Lexicographic (floatMinMax (minimize "min-x") False) + , goldenVsStringShow "optFloat1c" $ optimizeWith z3{printBase=16} Lexicographic (floatMinMax (maximize "max-x") True) + , goldenVsStringShow "optFloat1d" $ optimizeWith z3{printBase=16} Lexicographic (floatMinMax (maximize "max-y") False) + , goldenVsStringShow "optFloat2a" $ optimizeWith z3{printBase=16} Lexicographic (doubleMinMax (minimize "min-x") True) + , goldenVsStringShow "optFloat2b" $ optimizeWith z3{printBase=16} Lexicographic (doubleMinMax (minimize "min-x") False) + , goldenVsStringShow "optFloat2c" $ optimizeWith z3{printBase=16} Lexicographic (doubleMinMax (maximize "max-x") True) + , goldenVsStringShow "optFloat2d" $ optimizeWith z3{printBase=16} Lexicographic (doubleMinMax (maximize "max-y") False) + , goldenVsStringShow "optFloat3" $ optimizeWith z3{printBase=16} Lexicographic q + , goldenVsStringShow "optFloat4" $ optimizeWith z3{printBase=16} Lexicographic r ] -p :: Bool -> Goal -p reqPoint = do x <- sFloat "x" - y <- sDouble "y" +floatMinMax :: (SFloat -> Symbolic ()) -> Bool -> Goal +floatMinMax opt reqPoint = do x <- sFloat "x" - when reqPoint $ do constrain $ fpIsPoint x - constrain $ fpIsPoint y + when reqPoint $ constrain $ fpIsPoint x - minimize "min-x" x - maximize "max-x" x - minimize "min-y" y - maximize "max-y" y + opt x + +doubleMinMax :: (SDouble -> Symbolic ()) -> Bool -> Goal +doubleMinMax opt reqPoint = do x <- sDouble "x" + + when reqPoint $ constrain $ fpIsPoint x + + opt x q :: Goal q = do x <- sFloat "x" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 8.1 +Version: 8.2 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description: Express properties about Haskell programs and automatically prove them using SMT