sbv 8.1 → 8.2
raw patch · 54 files changed
+613/−650 lines, 54 filesdep ~base
Dependency ranges changed: base
Files
- CHANGES.md +17/−1
- Data/SBV/Control/Query.hs +17/−15
- Data/SBV/Control/Utils.hs +4/−3
- Data/SBV/Core/Symbolic.hs +41/−31
- Data/SBV/Provers/ABC.hs +0/−2
- Data/SBV/Provers/Boolector.hs +0/−2
- Data/SBV/Provers/CVC4.hs +0/−2
- Data/SBV/Provers/MathSAT.hs +0/−2
- Data/SBV/Provers/Prover.hs +56/−36
- Data/SBV/Provers/Yices.hs +0/−2
- Data/SBV/Provers/Z3.hs +0/−2
- Data/SBV/SMT/SMTLib2.hs +12/−20
- Data/SBV/Utils/SExpr.hs +23/−1
- Documentation/SBV/Examples/BitPrecise/MultMask.hs +3/−0
- Documentation/SBV/Examples/Existentials/Diophantine.hs +2/−2
- SBVTestSuite/GoldFiles/optFloat1.gold +0/−108
- SBVTestSuite/GoldFiles/optFloat1a.gold +13/−0
- SBVTestSuite/GoldFiles/optFloat1b.gold +13/−0
- SBVTestSuite/GoldFiles/optFloat1c.gold +13/−0
- SBVTestSuite/GoldFiles/optFloat1d.gold +13/−0
- SBVTestSuite/GoldFiles/optFloat2.gold +0/−108
- SBVTestSuite/GoldFiles/optFloat2a.gold +13/−0
- SBVTestSuite/GoldFiles/optFloat2b.gold +13/−0
- SBVTestSuite/GoldFiles/optFloat2c.gold +13/−0
- SBVTestSuite/GoldFiles/optFloat2d.gold +13/−0
- SBVTestSuite/GoldFiles/quantified_prove_existsexists_contradiction_p.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_prove_existsforall_contradiction_p.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_prove_existsforall_satisfiable_p.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_prove_forallexists_contradiction_p.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_c.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_p.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_c.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_p.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_c.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_p.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_c.gold +1/−0
- SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_p.gold +1/−0
- SBVTestSuite/GoldFiles/query_uisatex2.gold +1/−1
- SBVTestSuite/GoldFiles/set_uninterp1.gold +11/−11
- SBVTestSuite/GoldFiles/sumBimapPlus.gold +2/−2
- SBVTestSuite/GoldFiles/sumLiftEither.gold +2/−2
- SBVTestSuite/GoldFiles/sumLiftMaybe.gold +1/−1
- SBVTestSuite/GoldFiles/sumMaybe.gold +1/−1
- SBVTestSuite/GoldFiles/uiSat_test1.gold +6/−6
- SBVTestSuite/GoldFiles/uiSat_test2.gold +34/−34
- SBVTestSuite/GoldFiles/uiSat_test3.gold +232/−232
- SBVTestSuite/GoldFiles/validate_0.gold +2/−2
- SBVTestSuite/GoldFiles/validate_1.gold +2/−2
- SBVTestSuite/GoldFiles/validate_2.gold +2/−2
- SBVTestSuite/GoldFiles/validate_5.gold +1/−1
- SBVTestSuite/GoldFiles/validate_6.gold +1/−1
- SBVTestSuite/GoldFiles/validate_7.gold +2/−1
- SBVTestSuite/TestSuite/Optimization/Floats.hs +21/−13
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,7 +1,23 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* 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
Data/SBV/Control/Query.hs view
@@ -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
Data/SBV/Control/Utils.hs view
@@ -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
Data/SBV/Core/Symbolic.hs view
@@ -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 <http://github.com/LeventErkok/sbv/issues/459> for why.)- , roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions- , solverSetOptions :: [SMTOption] -- ^ Options to set as we start the solver- , ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.- , redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied.+ 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 <http://github.com/LeventErkok/sbv/issues/459> for why.)+ , roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions+ , solverSetOptions :: [SMTOption] -- ^ Options to set as we start the solver+ , ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.+ , redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied. } +-- | 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
Data/SBV/Provers/ABC.hs view
@@ -39,8 +39,6 @@ , supportsCustomQueries = False , supportsGlobalDecls = False , supportsDataTypes = False- , supportsDTConstructorSigs = False- , supportsDTAccessorSigs = False , supportsFlattenedModels = Nothing } }
Data/SBV/Provers/Boolector.hs view
@@ -37,8 +37,6 @@ , supportsCustomQueries = True , supportsGlobalDecls = False , supportsDataTypes = False- , supportsDTConstructorSigs = False- , supportsDTAccessorSigs = False , supportsFlattenedModels = Nothing } }
Data/SBV/Provers/CVC4.hs view
@@ -41,8 +41,6 @@ , supportsCustomQueries = True , supportsGlobalDecls = True , supportsDataTypes = True- , supportsDTConstructorSigs = True- , supportsDTAccessorSigs = False , supportsFlattenedModels = Nothing } }
Data/SBV/Provers/MathSAT.hs view
@@ -41,8 +41,6 @@ , supportsCustomQueries = True , supportsGlobalDecls = False , supportsDataTypes = True- , supportsDTConstructorSigs = False- , supportsDTAccessorSigs = False , supportsFlattenedModels = Nothing } }
Data/SBV/Provers/Prover.hs view
@@ -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 " <empty>" else ""+ , "Assignment:" ++ if null env then " <none>" else "" ] ++ [ "" | not (null env)] ++ [ " " ++ l | l <- lines envShown]
Data/SBV/Provers/Yices.hs view
@@ -39,8 +39,6 @@ , supportsCustomQueries = True , supportsGlobalDecls = False , supportsDataTypes = False- , supportsDTConstructorSigs = False- , supportsDTAccessorSigs = False , supportsFlattenedModels = Nothing } }
Data/SBV/Provers/Z3.hs view
@@ -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)" ]
Data/SBV/SMT/SMTLib2.hs view
@@ -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: <http://github.com/Z3Prover/z3/issues/2135>+ -- and in particular <http://github.com/Z3Prover/z3/issues/2135#issuecomment-477636435>+ 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 ++ ")"
Data/SBV/Utils/SExpr.hs view
@@ -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)
Documentation/SBV/Examples/BitPrecise/MultMask.hs view
@@ -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 <http://github.com/Z3Prover/z3/issues/2075> -- for details.
Documentation/SBV/Examples/Existentials/Diophantine.hs view
@@ -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: <http://z3.codeplex.com/workitem/88>.)+-- issue.) basis :: Maybe Int -> [[SInteger]] -> IO [[Integer]] basis mbLim m = extractModels `fmap` allSatWith z3{allSatMaxModelCount = mbLim} cond where cond = do as <- mkExistVars n
− SBVTestSuite/GoldFiles/optFloat1.gold
@@ -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
+ SBVTestSuite/GoldFiles/optFloat1a.gold view
@@ -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
+ SBVTestSuite/GoldFiles/optFloat1b.gold view
@@ -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
+ SBVTestSuite/GoldFiles/optFloat1c.gold view
@@ -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
+ SBVTestSuite/GoldFiles/optFloat1d.gold view
@@ -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
− SBVTestSuite/GoldFiles/optFloat2.gold
@@ -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
+ SBVTestSuite/GoldFiles/optFloat2a.gold view
@@ -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
+ SBVTestSuite/GoldFiles/optFloat2b.gold view
@@ -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
+ SBVTestSuite/GoldFiles/optFloat2c.gold view
@@ -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
+ SBVTestSuite/GoldFiles/optFloat2d.gold view
@@ -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
SBVTestSuite/GoldFiles/quantified_prove_existsexists_contradiction_p.gold view
@@ -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
SBVTestSuite/GoldFiles/quantified_prove_existsforall_contradiction_p.gold view
@@ -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
SBVTestSuite/GoldFiles/quantified_prove_existsforall_satisfiable_p.gold view
@@ -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
SBVTestSuite/GoldFiles/quantified_prove_forallexists_contradiction_p.gold view
@@ -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
SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_c.gold view
@@ -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
SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_p.gold view
@@ -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
SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_c.gold view
@@ -25,5 +25,6 @@ s4)))) [SEND] (check-sat) [RECV] sat+*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_p.gold view
@@ -25,5 +25,6 @@ s4)))) [SEND] (check-sat) [RECV] sat+*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_c.gold view
@@ -25,5 +25,6 @@ s4))))) [SEND] (check-sat) [RECV] sat+*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_p.gold view
@@ -25,5 +25,6 @@ s4))))) [SEND] (check-sat) [RECV] sat+*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_c.gold view
@@ -25,5 +25,6 @@ s4))))) [SEND] (check-sat) [RECV] sat+*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_p.gold view
@@ -25,5 +25,6 @@ s4))))) [SEND] (check-sat) [RECV] sat+*** In a quantified context, obvservables will not be printed. *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/query_uisatex2.gold view
@@ -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
SBVTestSuite/GoldFiles/set_uninterp1.gold view
@@ -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!
SBVTestSuite/GoldFiles/sumBimapPlus.gold view
@@ -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))
SBVTestSuite/GoldFiles/sumLiftEither.gold view
@@ -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)
SBVTestSuite/GoldFiles/sumLiftMaybe.gold view
@@ -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)
SBVTestSuite/GoldFiles/sumMaybe.gold view
@@ -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))
SBVTestSuite/GoldFiles/uiSat_test1.gold view
@@ -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
SBVTestSuite/GoldFiles/uiSat_test2.gold view
@@ -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)
SBVTestSuite/GoldFiles/uiSat_test3.gold view
@@ -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
SBVTestSuite/GoldFiles/validate_0.gold view
@@ -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 ***
SBVTestSuite/GoldFiles/validate_1.gold view
@@ -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 ***
SBVTestSuite/GoldFiles/validate_2.gold view
@@ -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 ***
SBVTestSuite/GoldFiles/validate_5.gold view
@@ -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).
SBVTestSuite/GoldFiles/validate_6.gold view
@@ -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).
SBVTestSuite/GoldFiles/validate_7.gold view
@@ -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 = <universally quantified> :: Float
SBVTestSuite/TestSuite/Optimization/Floats.hs view
@@ -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"
sbv.cabal view
@@ -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