diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,31 @@ * Hackage: * GitHub: -* Latest Hackage released version: 8.8, 2020-09-04 +* Latest Hackage released version: 8.9, 2020-10-28 + +### Version 8.9, 2020-10-28 + + * Rename 'sbvAvailableSolvers' to 'getAvailableSolvers'. + + * Use SMTLib's int2bv if supported by the backend solver. If not, we still + do a manual translation. (CVC4 and z3 support it natively, Yices and + MathSAT does not, for which we do the manual translation. ABC and dReal + doesn't support the coversion at all, since former doesn't support integers + and the latter doesn't support bit-vectors.) Thanks to Martin Lundfall + for the initial pull request. + + * Add `sym` as a synonym for `uninterpret`. This allows us to write expressions + of the form `sat $ sym "a" - sym "b" .== (0::SInteger)`, without resorting to lambda + expressions or having to explicitly be in the Symbolic monad. + + * Added missing instances for overflow-checking arithmetic of arbitrary + sized signed and unsigned bitvectors. + + * In a sat (or allSat) call, also return the values of the uninterpreted values, along with + all the explicitly named inputs. Strictly speaking, this is backwards-incompatible, + but it the new behavior is consistent with how we handle uninterpreted values in general. + + * Improve SMTLib logic-detection code to use generics. ### Version 8.8, 2020-09-04 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -19,7 +19,7 @@ -- -- >>> prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8) -- Falsifiable. Counter-example: --- s0 = 32 :: Word8 +-- s0 = 64 :: Word8 -- -- The function 'prove' has the following type: -- @@ -332,7 +332,7 @@ -- ** Solvers , boolector, cvc4, yices, dReal, z3, mathSAT, abc -- ** Configurations - , defaultSolverConfig, defaultSMTCfg, defaultDeltaSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers + , defaultSolverConfig, defaultSMTCfg, defaultDeltaSMTCfg, sbvCheckSolverInstallation, getAvailableSolvers , setLogic, Logic(..), setOption, setInfo, setTimeOut -- ** SBV exceptions , SBVException(..) @@ -458,7 +458,7 @@ are useful when you do not care if the solvers produce the same result, but rather want to get the solution as quickly as possible, taking advantage of modern many-core machines. -Note that the function 'sbvAvailableSolvers' will return all the installed solvers, which can be +Note that the function 'getAvailableSolvers' will return all the installed solvers, which can be used as the first argument to all these functions, if you simply want to try all available solvers on a machine. -} @@ -479,8 +479,8 @@ >>> safe (sub :: SInt8 -> SInt8 -> SInt8) [sub: x >= y must hold!: Violated. Model: - s0 = 30 :: Int8 - s1 = 32 :: Int8] + s0 = 0 :: Int8 + s1 = 1 :: Int8] What happens if we make sure to arrange for this invariant? Consider this version: diff --git a/Data/SBV/Client.hs b/Data/SBV/Client.hs --- a/Data/SBV/Client.hs +++ b/Data/SBV/Client.hs @@ -20,7 +20,7 @@ module Data.SBV.Client ( sbvCheckSolverInstallation , defaultSolverConfig - , sbvAvailableSolvers + , getAvailableSolvers , mkSymbolicEnumeration , mkUninterpretedSort ) where @@ -40,7 +40,7 @@ -- simple call to the solver to ensure all is well. sbvCheckSolverInstallation :: SMTConfig -> IO Bool sbvCheckSolverInstallation cfg = check `C.catch` (\(_ :: C.SomeException) -> return False) - where check = do ThmResult r <- proveWith cfg $ \x -> (x+x) .== ((x*2) :: SWord8) + where check = do ThmResult r <- proveWith cfg $ \x -> sNot (sNot x) .== (x :: SBool) case r of Unsatisfiable{} -> return True _ -> return False @@ -56,8 +56,8 @@ defaultSolverConfig ABC = abc -- | Return the known available solver configs, installed on your machine. -sbvAvailableSolvers :: IO [SMTConfig] -sbvAvailableSolvers = filterM sbvCheckSolverInstallation (map defaultSolverConfig [minBound .. maxBound]) +getAvailableSolvers :: IO [SMTConfig] +getAvailableSolvers = filterM sbvCheckSolverInstallation (map defaultSolverConfig [minBound .. maxBound]) -- | Turn a name into a symbolic type. If first argument is true, we'll also derive Eq and Ord instances. declareSymbolic :: Bool -> TH.Name -> TH.Q [TH.Dec] diff --git a/Data/SBV/Control/BaseIO.hs b/Data/SBV/Control/BaseIO.hs --- a/Data/SBV/Control/BaseIO.hs +++ b/Data/SBV/Control/BaseIO.hs @@ -448,6 +448,10 @@ getValueCV :: Maybe Int -> SV -> Query CV getValueCV = Trans.getValueCV +-- | Get the value of an uninterpreted value +getUICVal :: Maybe Int -> (String, SBVType) -> Query CV +getUICVal = Trans.getUICVal + -- | Get the value of an uninterpreted function as an association list -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.Control.getUIFunCVAssoc' 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 @@ -13,6 +13,7 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} @@ -335,8 +336,9 @@ let assocs = sortOn fst obsvs ++ sortByNodeId [p | p@(_, (nm, _)) <- inputAssocs, not (isNonModelVar cfg nm)] - -- collect UIs if requested - let uiFuns = [ui | ui@(_, SBVType as) <- uis, length as > 1, satTrackUFs cfg] -- functions have at least two things in their type! + -- collect UIs, and UI functions if requested + let uiFuns = [ui | ui@(nm, SBVType as) <- uis, length as > 1, satTrackUFs cfg, not (isNonModelVar cfg nm)] -- functions have at least two things in their type! + uiRegs = [ui | ui@(nm, SBVType as) <- uis, length as == 1, not (isNonModelVar cfg nm)] -- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out -- as cex's tend to get larger @@ -361,12 +363,14 @@ then Just <$> mapM (get . flipQ) qinps else return Nothing - uivs <- mapM (\ui@(nm, t) -> (\a -> (nm, (t, a))) <$> getUIFunCVAssoc mbi ui) uiFuns + uiFunVals <- mapM (\ui@(nm, t) -> (\a -> (nm, (t, a))) <$> getUIFunCVAssoc mbi ui) uiFuns + uiVals <- mapM (\ui@(nm, _) -> (nm,) <$> getUICVal mbi ui) uiRegs + return SMTModel { modelObjectives = [] , modelBindings = bindings - , modelAssocs = assocs - , modelUIFuns = uivs + , modelAssocs = uiVals ++ assocs + , modelUIFuns = uiFunVals } -- | Just after a check-sat is issued, collect objective values. Used 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 @@ -24,7 +24,7 @@ module Data.SBV.Control.Utils ( io , ask, send, getValue, getFunction, getUninterpretedValue - , getValueCV, getUIFunCVAssoc, getUnsatAssumptions + , getValueCV, getUICVal, getUIFunCVAssoc, getUnsatAssumptions , SMTFunction(..), registerUISMTFunction , getQueryState, modifyQueryState, getConfig, getObjectives, getUIs , getSBVAssertions, getSBVPgm, getQuantifiedInputs, getObservables @@ -698,25 +698,7 @@ | s == falseSV = return falseCV | True - = do let nm = show s - k = kindOf s - - modelIndex = case mbi of - Nothing -> "" - Just i -> " :model_index " ++ show i - - cmd = "(get-value (" ++ nm ++ ")" ++ modelIndex ++ ")" - - bad = unexpected "getModel" cmd ("a value binding for kind: " ++ show k) Nothing - - r <- ask cmd - - let recover val = case recoverKindedValue (kindOf s) val of - Just cv -> return cv - Nothing -> bad r Nothing - - parse r bad $ \case EApp [EApp [ECon v, val]] | v == nm -> recover val - _ -> bad r Nothing + = extractValue mbi (show s) (kindOf s) -- | "Make up" a CV for this type. Like zero, but smarter. defaultKindedValue :: Kind -> Maybe CV @@ -956,6 +938,32 @@ (CV KReal (CAlgReal a), CV KReal (CAlgReal b)) -> return $ CV KReal (CAlgReal (mergeAlgReals ("Cannot merge real-values for " ++ show s) a b)) _ -> bad +-- | Retrieve value from the solver +extractValue :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> String -> Kind -> m CV +extractValue mbi nm k = do + let modelIndex = case mbi of + Nothing -> "" + Just i -> " :model_index " ++ show i + + cmd = "(get-value (" ++ nm ++ ")" ++ modelIndex ++ ")" + + bad = unexpected "getModel" cmd ("a value binding for kind: " ++ show k) Nothing + + r <- ask cmd + + let recover val = case recoverKindedValue k val of + Just cv -> return cv + Nothing -> bad r Nothing + + parse r bad $ \case EApp [EApp [ECon v, val]] | v == nm -> recover val + _ -> bad r Nothing + +-- | Generalization of 'Data.SBV.Control.getUICVal' +getUICVal :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, SBVType) -> m CV +getUICVal mbi (nm, t) = case t of + SBVType [k] -> extractValue mbi nm k + _ -> error $ "SBV.getUICVal: Expected to be called on an uninterpeted value of a base type, received something else: " ++ show (nm, t) + -- | Generalization of 'Data.SBV.Control.getUIFunCVAssoc' getUIFunCVAssoc :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, SBVType) -> m ([([CV], CV)], CV) getUIFunCVAssoc mbi (nm, typ) = do @@ -1082,20 +1090,25 @@ , not (isNonModelVar cfg nm) -- make sure they aren't explicitly ignored ] + allUiRegs = [u | u@(nm, SBVType as) <- allUninterpreteds, length as == 1 -- non-function ones + , not (isNonModelVar cfg nm) -- make sure not ignored + ] + -- We can only "allSat" if all component types themselves are interpreted. (Otherwise -- there is no way to reflect back the values to the solver.) - collectAcceptable [] sofar = return sofar + collectAcceptable [] sofar = return sofar collectAcceptable ((nm, t@(SBVType ats)):rest) sofar | not (any hasUninterpretedSorts ats) = collectAcceptable rest (nm : sofar) | True = do queryDebug [ "*** SBV.allSat: Uninterpreted function: " ++ nm ++ " :: " ++ show t - , "*** Will *not* be used in allSat consideretions since its type" + , "*** Will *not* be used in allSat considerations since its type" , "*** has uninterpreted sorts present." ] collectAcceptable rest sofar uiFuns <- reverse <$> collectAcceptable allUiFuns [] + _ <- collectAcceptable allUiRegs [] -- only done to get the queryDebug output. Actual result not needed/used -- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out -- as cex's tend to get larger @@ -1129,19 +1142,19 @@ -- If we have any universals, then the solutions are unique upto prefix existentials. w = ALL `elem` map fst qinps - res <- loop grabObservables topState (allUiFuns, uiFuns) qinps vars cfg AllSatResult { allSatMaxModelCountReached = False - , allSatHasPrefixExistentials = w - , allSatSolverReturnedUnknown = False - , allSatSolverReturnedDSat = False - , allSatResults = [] - } + res <- loop grabObservables topState (allUiFuns, uiFuns) allUiRegs qinps vars cfg AllSatResult { allSatMaxModelCountReached = False + , allSatHasPrefixExistentials = w + , allSatSolverReturnedUnknown = False + , allSatSolverReturnedDSat = False + , allSatResults = [] + } -- results come out in reverse order, so reverse them: pure $ res { allSatResults = reverse (allSatResults res) } where isFree (KUserSort _ Nothing) = True isFree _ = False - loop grabObservables topState (allUiFuns, uiFunsToReject) qinps vars cfg = go (1::Int) + loop grabObservables topState (allUiFuns, uiFunsToReject) allUiRegs qinps vars cfg = go (1::Int) where go :: Int -> AllSatResult -> m AllSatResult go !cnt sofar | Just maxModels <- allSatMaxModelCount cfg, cnt > maxModels @@ -1185,6 +1198,8 @@ return (nm, (t, cvs)) uiFunVals <- mapM getUIFun allUiFuns + uiRegVals <- mapM (\ui@(nm, _) -> (nm,) <$> getUICVal Nothing ui) allUiRegs + -- Add on observables if we're asked to do so: obsvs <- if grabObservables then getObservables @@ -1202,18 +1217,25 @@ let model = SMTModel { modelObjectives = [] , modelBindings = bindings - , modelAssocs = sortOn fst obsvs ++ [(n, cv) | (_, (n, (_, cv))) <- assocs] + , modelAssocs = uiRegVals ++ sortOn fst obsvs ++ [(n, cv) | (_, (n, (_, cv))) <- assocs] , modelUIFuns = uiFunVals } m = Satisfiable cfg model (interpreteds, uninterpreteds) = partition (not . isFree . kindOf . fst) (map (snd . snd) assocs) + interpretedRegUis = filter (not . isFree . kindOf . snd) uiRegVals + + interpretedRegUiSVs = [(cvt n (kindOf cv), cv) | (n, cv) <- interpretedRegUis] + where cvt :: String -> Kind -> SVal + cvt nm k = SVal k $ Right $ cache r + where r st = newExpr st k (SBVApp (Uninterpreted nm) []) + -- For each interpreted variable, figure out the model equivalence -- NB. When the kind is floating, we *have* to be careful, since +/- zero, and NaN's -- and equality don't get along! interpretedEqs :: [SVal] - interpretedEqs = [mkNotEq (kindOf sv) sv (SVal (kindOf sv) (Left cv)) | (sv, cv) <- interpreteds] + interpretedEqs = [mkNotEq (kindOf sv) sv (SVal (kindOf sv) (Left cv)) | (sv, cv) <- interpretedRegUiSVs ++ interpreteds] where mkNotEq k a b | isDouble k || isFloat k = svNot (a `fpNotEq` b) | True = a `svNotEqual` b @@ -1238,7 +1260,7 @@ -- We do this rather brute-force, since we need to create a new function -- and do an existential assertion. uninterpretedReject :: Maybe [String] - uninterpretedFuns :: [String] + uninterpretedFuns :: [String] (uninterpretedReject, uninterpretedFuns) = (uiReject, concat defs) where uiReject = case rejects of [] -> Nothing diff --git a/Data/SBV/Core/Floating.hs b/Data/SBV/Core/Floating.hs --- a/Data/SBV/Core/Floating.hs +++ b/Data/SBV/Core/Floating.hs @@ -222,15 +222,15 @@ -- Q.E.D. -- >>> prove $ roundTrip @Int32 -- Falsifiable. Counter-example: - -- s0 = RoundNearestTiesToEven :: RoundingMode - -- s1 = -206897400 :: Int32 + -- s0 = RoundTowardNegative :: RoundingMode + -- s1 = -44297675 :: Int32 -- -- Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float: -- - -- >>> toRational (-206897400 :: Float) - -- (-206897408) % 1 + -- >>> toRational (-44297675 :: Float) + -- (-44297676) % 1 -- - -- Note how the numerator is different, it is off by 8. This is hardly surprising, since floats become sparser as + -- Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as -- the magnitude increases to be able to cover all the integer values representable. toSFloat :: SRoundingMode -> SBV a -> SFloat @@ -263,16 +263,16 @@ -- Q.E.D. -- >>> prove $ roundTrip @Int64 -- Falsifiable. Counter-example: - -- s0 = RoundTowardNegative :: RoundingMode - -- s1 = -18014398509481983 :: Int64 + -- s0 = RoundNearestTiesToAway :: RoundingMode + -- s1 = -3871901667041025751 :: Int64 -- -- Just like in the `SFloat` case, once we reach 64-bits, we no longer can exactly represent the -- integer value for all possible values: -- - -- >>> toRational (-18014398509481983 :: Double) - -- (-18014398509481984) % 1 + -- >>> toRational (-3871901667041025751 :: Double) + -- (-3871901667041025536) % 1 -- - -- In this case the numerator is off by 1. + -- In this case the numerator is off by 15. toSDouble :: SRoundingMode -> SBV a -> SDouble -- default definition if we have an integral like diff --git a/Data/SBV/Core/Kind.hs b/Data/SBV/Core/Kind.hs --- a/Data/SBV/Core/Kind.hs +++ b/Data/SBV/Core/Kind.hs @@ -10,6 +10,7 @@ ----------------------------------------------------------------------------- {-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -51,7 +52,7 @@ | KTuple [Kind] | KMaybe Kind | KEither Kind Kind - deriving (Eq, Ord) + deriving (Eq, Ord, G.Data) -- | The interesting about the show instance is that it can tell apart two kinds nicely; since it conveniently -- ignores the enumeration constructors. Also, when we construct a 'KUserSort', we make sure we don't use any of diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -2135,12 +2135,16 @@ -- | Most generalized form of uninterpretation, this function should not be needed -- by end-user-code, but is rather useful for the library development. sbvUninterpret :: Maybe ([String], a) -> String -> a + -- | A synonym for 'uninterpret'. Allows us to create variables without + -- having to call 'free' explicitly, i.e., without being in the symbolic monad. + sym :: String -> a {-# MINIMAL sbvUninterpret #-} -- defaults: uninterpret = sbvUninterpret Nothing cgUninterpret nm code v = sbvUninterpret (Just (code, v)) nm + sym = uninterpret -- Plain constants instance HasKind a => Uninterpreted (SBV a) where diff --git a/Data/SBV/Core/Sized.hs b/Data/SBV/Core/Sized.hs --- a/Data/SBV/Core/Sized.hs +++ b/Data/SBV/Core/Sized.hs @@ -73,7 +73,7 @@ -- | Type family to create the appropriate non-zero constraint type family IsNonZero (arg :: Nat) :: Constraint where IsNonZero 0 = TypeError ZeroWidth - IsNonZero n = () + IsNonZero _ = () -- | 'WordN' has a kind instance (KnownNat n, IsNonZero n) => HasKind (WordN n) where 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 @@ -104,10 +104,11 @@ #endif -- | A symbolic node id -newtype NodeId = NodeId Int deriving (Eq, Ord) +newtype NodeId = NodeId Int deriving (Eq, Ord, G.Data) -- | A symbolic word, tracking it's signedness and size. data SV = SV !Kind !NodeId + deriving G.Data -- | For equality, we merely use the node-id instance Eq SV where @@ -190,7 +191,7 @@ | MaybeConstructor Kind Bool -- Construct a maybe value; False: Nothing, True: Just | MaybeIs Kind Bool -- Maybe tester; False: nothing, True: just | MaybeAccess -- Maybe branch access; grab the contents of the just - deriving (Eq, Ord) + deriving (Eq, Ord, G.Data) -- | Floating point operations data FPOp = FP_Cast Kind Kind SV -- From-Kind, To-Kind, RoundingMode. This is "value" conversion @@ -215,7 +216,7 @@ | FP_IsNaN | FP_IsNegative | FP_IsPositive - deriving (Eq, Ord) + deriving (Eq, Ord, G.Data) -- Note that the show instance maps to the SMTLib names. We need to make sure -- this mapping stays correct through SMTLib changes. The only exception @@ -261,7 +262,7 @@ | NR_Exp | NR_Log | NR_Pow - deriving (Eq, Ord) + deriving (Eq, Ord, G.Data) -- | The show instance carefully arranges for these to be printed as it can be understood by dreal instance Show NROp where @@ -286,13 +287,13 @@ | PB_Le [Int] Int -- ^ At most k, with coefficients given. Generalizes PB_AtMost | PB_Ge [Int] Int -- ^ At least k, with coefficients given. Generalizes PB_AtLeast | PB_Eq [Int] Int -- ^ Exactly k, with coefficients given. Generalized PB_Exactly - deriving (Eq, Ord, Show) + deriving (Eq, Ord, Show, G.Data) -- | Overflow operations data OvOp = Overflow_SMul_OVFL -- ^ Signed multiplication overflow | Overflow_SMul_UDFL -- ^ Signed multiplication underflow | Overflow_UMul_OVFL -- ^ Unsigned multiplication overflow - deriving (Eq, Ord) + deriving (Eq, Ord, G.Data) -- | Show instance. It's important that these follow the internal z3 names instance Show OvOp where @@ -314,7 +315,7 @@ | StrStrToNat -- ^ Retrieve integer encoded by string @s@ (ground rewriting only) | StrNatToStr -- ^ Retrieve string encoded by integer @i@ (ground rewriting only) | StrInRe RegExp -- ^ Check if string is in the regular expression - deriving (Eq, Ord) + deriving (Eq, Ord, G.Data) -- | Regular expressions. Note that regular expressions themselves are -- concrete, but the 'Data.SBV.RegExp.match' function from the 'Data.SBV.RegExp.RegExpMatchable' class @@ -334,7 +335,7 @@ | Loop Int Int RegExp -- ^ From @n@ repetitions to @m@ repetitions | Union [RegExp] -- ^ Union of regular expressions | Inter RegExp RegExp -- ^ Intersection of regular expressions - deriving (Eq, Ord) + deriving (Eq, Ord, G.Data) -- | With overloaded strings, we can have direct literal regular expressions. instance IsString RegExp where @@ -413,7 +414,7 @@ | SeqPrefixOf -- ^ See StrPrefixOf | SeqSuffixOf -- ^ See StrSuffixOf | SeqReplace -- ^ See StrReplace - deriving (Eq, Ord) + deriving (Eq, Ord, G.Data) -- | Show instance for SeqOp. Again, mapping is important. instance Show SeqOp where @@ -439,7 +440,7 @@ | SetDifference | SetComplement | SetHasSize - deriving (Eq, Ord) + deriving (Eq, Ord, G.Data) -- The show instance for 'SetOp' is merely for debugging, we map them separately so -- the mapped strings are less important here. @@ -551,7 +552,7 @@ -- | A symbolic expression data SBVExpr = SBVApp !Op ![SV] - deriving (Eq, Ord) + deriving (Eq, Ord, G.Data) -- | To improve hash-consing, take advantage of commutative operators by -- reordering their arguments. @@ -1664,7 +1665,7 @@ uncache = uncacheGen rSVCache -- | An SMT array index is simply an int value -newtype ArrayIndex = ArrayIndex { unArrayIndex :: Int } deriving (Eq, Ord) +newtype ArrayIndex = ArrayIndex { unArrayIndex :: Int } deriving (Eq, Ord, G.Data) -- | We simply show indexes as the underlying integer instance Show ArrayIndex where @@ -1771,6 +1772,7 @@ , supportsBitVectors :: Bool -- ^ Supports bit-vectors? , supportsUninterpretedSorts :: Bool -- ^ Supports SMT-Lib2 style uninterpreted-sorts , supportsUnboundedInts :: Bool -- ^ Supports unbounded integers? + , supportsInt2bv :: Bool -- ^ Supports int2bv? , supportsReals :: Bool -- ^ Supports reals? , supportsApproxReals :: Bool -- ^ Supports printing of approximations of reals? , supportsDeltaSat :: Maybe String -- ^ Supports delta-satisfiability? (With given precision query) @@ -1843,6 +1845,10 @@ , ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess. , redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied. } + +-- | We show the name of the solver for the config. Arguably this is misleading, but better than nothing. +instance Show SMTConfig where + show = show . name . solver -- | Returns true if we have to perform validation validationRequested :: SMTConfig -> Bool diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs --- a/Data/SBV/Dynamic.hs +++ b/Data/SBV/Dynamic.hs @@ -95,7 +95,7 @@ -- ** Programmable model extraction , genParse, getModelAssignment, getModelDictionary -- * SMT Interface: Configurations and solvers - , SMTConfig(..), SMTLibVersion(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers + , SMTConfig(..), SMTLibVersion(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, getAvailableSolvers -- * Symbolic computations , outputSVal @@ -147,7 +147,7 @@ import Data.SBV.Provers.Prover (boolector, cvc4, yices, z3, mathSAT, abc, defaultSMTCfg) import Data.SBV.SMT.SMT (ThmResult(..), SatResult(..), SafeResult(..), OptimizeResult(..), AllSatResult(..), genParse) -import Data.SBV (sbvCheckSolverInstallation, defaultSolverConfig, sbvAvailableSolvers) +import Data.SBV (sbvCheckSolverInstallation, defaultSolverConfig, getAvailableSolvers) import qualified Data.SBV as SBV (SBool, proveWithAll, proveWithAny, satWithAll, satWithAny , proveConcurrentWithAll, proveConcurrentWithAny 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 @@ -35,6 +35,7 @@ , supportsBitVectors = True , supportsUninterpretedSorts = False , supportsUnboundedInts = False + , supportsInt2bv = False , supportsReals = False , supportsApproxReals = False , supportsDeltaSat = 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 @@ -33,6 +33,7 @@ , supportsBitVectors = True , supportsUninterpretedSorts = False , supportsUnboundedInts = False + , supportsInt2bv = False , supportsReals = False , supportsApproxReals = False , supportsDeltaSat = 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 @@ -37,6 +37,7 @@ , supportsBitVectors = True , supportsUninterpretedSorts = True , supportsUnboundedInts = True + , supportsInt2bv = True , supportsReals = True -- Not quite the same capability as Z3; but works more or less.. , supportsApproxReals = False , supportsDeltaSat = Nothing diff --git a/Data/SBV/Provers/DReal.hs b/Data/SBV/Provers/DReal.hs --- a/Data/SBV/Provers/DReal.hs +++ b/Data/SBV/Provers/DReal.hs @@ -37,6 +37,7 @@ , supportsBitVectors = False , supportsUninterpretedSorts = False , supportsUnboundedInts = True + , supportsInt2bv = False , supportsReals = True , supportsApproxReals = False , supportsDeltaSat = Just "(get-option :precision)" 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 @@ -37,6 +37,7 @@ , supportsBitVectors = True , supportsUninterpretedSorts = True , supportsUnboundedInts = True + , supportsInt2bv = False , supportsReals = True , supportsApproxReals = False , supportsDeltaSat = Nothing 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 @@ -35,6 +35,7 @@ , supportsBitVectors = True , supportsUninterpretedSorts = True , supportsUnboundedInts = True + , supportsInt2bv = False , supportsReals = True , supportsApproxReals = False , supportsDeltaSat = 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 @@ -35,6 +35,7 @@ , supportsBitVectors = True , supportsUninterpretedSorts = True , supportsUnboundedInts = True + , supportsInt2bv = True , supportsReals = True , supportsApproxReals = True , supportsDeltaSat = Nothing diff --git a/Data/SBV/RegExp.hs b/Data/SBV/RegExp.hs --- a/Data/SBV/RegExp.hs +++ b/Data/SBV/RegExp.hs @@ -87,7 +87,7 @@ -- >>> let phone = pre * "-" * post -- >>> sat $ \s -> (s :: SString) `match` phone -- Satisfiable. Model: --- s0 = "840-4224" :: String +-- s0 = "100-8000" :: String class RegExpMatchable a where -- | @`match` s r@ checks whether @s@ is in the language generated by @r@. match :: a -> RegExp -> SBool 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 @@ -9,7 +9,8 @@ -- Conversion of symbolic programs to SMTLib format, Using v2 of the standard ----------------------------------------------------------------------------- -{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -26,13 +27,15 @@ import qualified Data.Set as Set import Data.SBV.Core.Data -import Data.SBV.Core.Symbolic (QueryContext(..), SetOp(..)) +import Data.SBV.Core.Symbolic (QueryContext(..), SetOp(..), OvOp(..)) import Data.SBV.Core.Kind (smtType, needsFlattening) import Data.SBV.SMT.Utils import Data.SBV.Control.Types import Data.SBV.Utils.PrettyNum (smtRoundingMode, cvToSMTLib) +import qualified Data.Generics.Uniplate.Data as G + tbd :: String -> a tbd e = error $ "SBV.SMTLib2: Not-yet-supported: " ++ e @@ -52,6 +55,7 @@ tupleArities = findTupleArities kindInfo hasNonBVArrays = (not . null) [() | (_, (_, (k1, k2), _)) <- arrs, not (isBounded k1 && isBounded k2)] hasArrayInits = (not . null) [() | (_, (_, _, ArrayFree (Just _))) <- arrs] + hasOverflows = (not . null) [() | (_ :: OvOp) <- G.universeBi asgnsSeq] hasList = any isList kindInfo hasSets = any isSet kindInfo hasTuples = not . null $ tupleArities @@ -72,6 +76,8 @@ , "*** But the chosen solver (" ++ show (name (solver cfg)) ++ ") doesn't support this feature." ] + setAll reason = ["(set-logic ALL) ; " ++ reason ++ ", using catch-all."] + -- Determining the logic is surprisingly tricky! logic -- user told us what to do: so just take it: @@ -102,20 +108,19 @@ -- we never set QF_S (ALL seems to work better in all cases) - | hasInteger || hasReal || not (null trueUSorts) || hasNonBVArrays || hasTuples || hasEither || hasMaybe || hasSets || hasList || hasString || hasArrayInits - = let why | hasInteger = "has unbounded values" - | hasReal = "has algebraic reals" - | not (null trueUSorts) = "has user-defined sorts" - | hasNonBVArrays = "has non-bitvector arrays" - | hasTuples = "has tuples" - | hasEither = "has either type" - | hasMaybe = "has maybe type" - | hasSets = "has sets" - | hasList = "has lists" - | hasString = "has strings" - | hasArrayInits = "has array initializers" - | True = "cannot determine the SMTLib-logic to use" - in ["(set-logic ALL) ; " ++ why ++ ", using catch-all."] + -- Things that require ALL + | hasInteger = setAll "has unbounded values" + | hasReal = setAll "has algebraic reals" + | not (null trueUSorts) = setAll "has user-defined sorts" + | hasNonBVArrays = setAll "has non-bitvector arrays" + | hasTuples = setAll "has tuples" + | hasEither = setAll "has either type" + | hasMaybe = setAll "has maybe type" + | hasSets = setAll "has sets" + | hasList = setAll "has lists" + | hasString = setAll "has strings" + | hasArrayInits = setAll "has array initializers" + | hasOverflows = setAll "has overflow checks" | hasDouble || hasFloat || hasRounding = if not (null foralls) @@ -629,8 +634,8 @@ cvtExp caps rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr where ssv = cvtSV skolemMap - supportsPB = supportsPseudoBooleans caps - + hasPB = supportsPseudoBooleans caps + hasInt2bv = supportsInt2bv caps hasDistinct = supportsDistinct caps bvOp = all isBounded arguments @@ -797,7 +802,7 @@ le0 = "(" ++ less ++ " " ++ ssv i ++ " " ++ mkCnst 0 ++ ")" gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ ssv i ++ ")" - sh (SBVApp (KindCast f t) [a]) = handleKindCast f t (ssv a) + sh (SBVApp (KindCast f t) [a]) = handleKindCast hasInt2bv f t (ssv a) sh (SBVApp (ArrEq i j) []) = "(= array_" ++ show i ++ " array_" ++ show j ++")" sh (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ ssv a ++ ")" @@ -844,8 +849,8 @@ sh (SBVApp (NonLinear w) args) = "(" ++ show w ++ " " ++ unwords (map ssv args) ++ ")" sh (SBVApp (PseudoBoolean pb) args) - | supportsPB = handlePB pb args' - | True = reducePB pb args' + | hasPB = handlePB pb args' + | True = reducePB pb args' where args' = map ssv args -- NB: Z3 semantics have the predicates reversed: i.e., it returns true if overflow isn't possible. Hence the not. @@ -1079,8 +1084,8 @@ where o = if hasSign x then oS else oW -- Various casts -handleKindCast :: Kind -> Kind -> String -> String -handleKindCast kFrom kTo a +handleKindCast :: Bool -> Kind -> Kind -> String -> String +handleKindCast hasInt2bv kFrom kTo a | kFrom == kTo = a | True @@ -1129,15 +1134,17 @@ zeroExtend i = "((_ zero_extend " ++ show i ++ ") " ++ a ++ ")" extract i = "((_ extract " ++ show i ++ " 0) " ++ a ++ ")" - -- NB. The following works regardless n < 0 or not, because the first thing we + -- Some solvers support int2bv, but not all. So, we use a capability to determine. + -- + -- NB. The "manual" implementation works regardless n < 0 or not, because the first thing we -- do is to compute "reduced" to bring it down to the correct range. It also works -- regardless were mapping to signed or unsigned bit-vector; because the representation -- is the same. - -- - -- NB2. (TODO) There is an SMTLib equivalent of this function, called int2bv. However, it - -- used to be uninterpreted for a long time by Z3; though I think that got fixed. We - -- might want to simply use that if it's reliably available across the board in solvers. - i2b n = "(let (" ++ reduced ++ ") (let (" ++ defs ++ ") " ++ body ++ "))" + i2b n + | hasInt2bv + = "((_ int2bv " ++ show n ++ ") " ++ a ++ ")" + | True + = "(let (" ++ reduced ++ ") (let (" ++ defs ++ ") " ++ body ++ "))" where b i = show (bit i :: Integer) reduced = "(__a (mod " ++ a ++ " " ++ b n ++ "))" mkBit 0 = "(__a0 (ite (= (mod __a 2) 0) #b0 #b1))" diff --git a/Data/SBV/Tools/BoundedList.hs b/Data/SBV/Tools/BoundedList.hs --- a/Data/SBV/Tools/BoundedList.hs +++ b/Data/SBV/Tools/BoundedList.hs @@ -145,6 +145,3 @@ -- | Bounded insertion sort bsort :: (Ord a, SymVal a) => Int -> SList a -> SList a bsort cnt = bfoldr cnt (binsert cnt) [] - --- Hlint is thinking "OverloadedLists" is wrong, but GHC wants it. -{-# ANN module ("HLint: ignore Unused LANGUAGE pragma" :: String) #-} diff --git a/Data/SBV/Tools/Overflow.hs b/Data/SBV/Tools/Overflow.hs --- a/Data/SBV/Tools/Overflow.hs +++ b/Data/SBV/Tools/Overflow.hs @@ -10,12 +10,13 @@ -- Based on: ----------------------------------------------------------------------------- -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -33,7 +34,10 @@ import Data.SBV.Core.Symbolic import Data.SBV.Core.Model import Data.SBV.Core.Operations +import Data.SBV.Core.Sized +import GHC.TypeLits + import GHC.Stack import Data.Int @@ -95,6 +99,9 @@ instance ArithOverflow SInt32 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} instance ArithOverflow SInt64 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance (KnownNat n, IsNonZero n) => ArithOverflow (SWord n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance (KnownNat n, IsNonZero n) => ArithOverflow (SInt n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} + instance ArithOverflow SVal where bvAddO = signPick2 bvuaddo bvsaddo bvSubO = signPick2 bvusubo bvssubo @@ -171,6 +178,21 @@ (*!) = checkOp2 ?loc "multiplication" (*) bvMulO (/!) = checkOp2 ?loc "division" sDiv bvDivO negateChecked = checkOp1 ?loc "unary negation" negate bvNegO + +instance (KnownNat n, IsNonZero n) => CheckedArithmetic (WordN n) where + (+!) = checkOp2 ?loc "addition" (+) bvAddO + (-!) = checkOp2 ?loc "subtraction" (-) bvSubO + (*!) = checkOp2 ?loc "multiplication" (*) bvMulO + (/!) = checkOp2 ?loc "division" sDiv bvDivO + negateChecked = checkOp1 ?loc "unary negation" negate bvNegO + +instance (KnownNat n, IsNonZero n) => CheckedArithmetic (IntN n) where + (+!) = checkOp2 ?loc "addition" (+) bvAddO + (-!) = checkOp2 ?loc "subtraction" (-) bvSubO + (*!) = checkOp2 ?loc "multiplication" (*) bvMulO + (/!) = checkOp2 ?loc "division" sDiv bvDivO + negateChecked = checkOp1 ?loc "unary negation" negate bvNegO + -- | Zero-extend to given bits zx :: Int -> SVal -> SVal diff --git a/Data/SBV/Trans.hs b/Data/SBV/Trans.hs --- a/Data/SBV/Trans.hs +++ b/Data/SBV/Trans.hs @@ -139,7 +139,7 @@ -- ** Solvers , boolector, cvc4, yices, z3, mathSAT, abc -- ** Configurations - , defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers + , defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, getAvailableSolvers , setLogic, Logic(..), setOption, setInfo, setTimeOut -- ** SBV exceptions , SBVException(..) diff --git a/Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs b/Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs --- a/Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs +++ b/Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs @@ -22,13 +22,13 @@ -- -- >>> checkArithOverflow midPointBroken -- Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:35:28:+!: SInt32 addition overflows: Violated. Model: --- low = 2147475457 :: Int32 --- high = 2147483645 :: Int32 +-- low = 2147483647 :: Int32 +-- high = 2147483647 :: Int32 -- -- Indeed: -- --- >>> (2147475457 + 2147483645) `div` (2::Int32) --- -4097 +-- >>> (2147483647 + 2147483647) `div` (2::Int32) +-- -1 -- -- giving us a negative mid-point value! midPointBroken :: SInt32 -> SInt32 -> SInt32 diff --git a/Documentation/SBV/Examples/Misc/Enumerate.hs b/Documentation/SBV/Examples/Misc/Enumerate.hs --- a/Documentation/SBV/Examples/Misc/Enumerate.hs +++ b/Documentation/SBV/Examples/Misc/Enumerate.hs @@ -60,7 +60,7 @@ -- | Enumerations are automatically ordered, so we can ask for the maximum -- element. Note the use of quantification. We have: -- --- maxE +-- >>> maxE -- Satisfiable. Model: -- maxE = C :: E maxE :: IO SatResult diff --git a/Documentation/SBV/Examples/Misc/Floating.hs b/Documentation/SBV/Examples/Misc/Floating.hs --- a/Documentation/SBV/Examples/Misc/Floating.hs +++ b/Documentation/SBV/Examples/Misc/Floating.hs @@ -58,19 +58,19 @@ -- -- >>> assocPlusRegular -- Falsifiable. Counter-example: --- x = -4.73427e15 :: Float --- y = 3.718088e19 :: Float --- z = 4.500073e20 :: Float +-- x = 1.3067223e-25 :: Float +-- y = -1.7763568e-15 :: Float +-- z = 1.7762754e-15 :: Float -- -- Indeed, we have: -- --- >>> let x = -4.73427e15 :: Float --- >>> let y = 3.718088e19 :: Float --- >>> let z = 4.500073e20 :: Float +-- >>> let x = 1.3067223e-25 :: Float +-- >>> let y = -1.7763568e-15 :: Float +-- >>> let z = 1.7762754e-15 :: Float -- >>> x + (y + z) --- 4.8718343e20 +-- -8.142091e-20 -- >>> (x + y) + z --- 4.8718347e20 +-- -8.142104e-20 -- -- Note the difference in the results! assocPlusRegular :: IO ThmResult @@ -92,13 +92,13 @@ -- -- >>> nonZeroAddition -- Falsifiable. Counter-example: --- a = 1.3408534e37 :: Float --- b = 6.977023e21 :: Float +-- a = 7.486071e12 :: Float +-- b = 188.8646 :: Float -- -- Indeed, we have: -- --- >>> let a = 1.3408534e37 :: Float --- >>> let b = 6.977023e21 :: Float +-- >>> let a = 7.486071e12 :: Float +-- >>> let b = 188.8646 :: Float -- >>> a + b == a -- True -- >>> b == 0 @@ -121,11 +121,11 @@ -- -- >>> multInverse -- Falsifiable. Counter-example: --- a = 7.660899e-39 :: Float +-- a = 8.590978e-39 :: Float -- -- Indeed, we have: -- --- >>> let a = 7.660899e-39 :: Float +-- >>> let a = 8.590978e-39 :: Float -- >>> a * (1/a) -- 0.99999994 multInverse :: IO ThmResult diff --git a/Documentation/SBV/Examples/ProofTools/BMC.hs b/Documentation/SBV/Examples/ProofTools/BMC.hs --- a/Documentation/SBV/Examples/ProofTools/BMC.hs +++ b/Documentation/SBV/Examples/ProofTools/BMC.hs @@ -83,7 +83,7 @@ -- BMC: Iteration: 2 -- BMC: Iteration: 3 -- BMC: Solution found at iteration 3 --- Right (3,[(0,10),(2,10),(2,6),(2,2)]) +-- Right (3,[(0,10),(0,6),(2,6),(2,2)]) -- -- As expected, there's a solution in this case. Furthermore, since the BMC engine -- found a solution at depth @3@, we also know that there is no solution at diff --git a/Documentation/SBV/Examples/Queries/AllSat.hs b/Documentation/SBV/Examples/Queries/AllSat.hs --- a/Documentation/SBV/Examples/Queries/AllSat.hs +++ b/Documentation/SBV/Examples/Queries/AllSat.hs @@ -20,9 +20,9 @@ import Data.SBV import Data.SBV.Control --- | Find all solutions to @x + y .== 10@ for positive @x@ and @y@, but at each --- iteration we would like to ensure that the value of @x@ we get is one more than --- the previous one. This is rather silly, but demonstrates how we can dynamically +-- | Find all solutions to @x + y .== 10@ for positive @x@ and @y@. +-- This is rather silly to do in the query mode as `allSat` can do +-- this automatically, but it demonstrates how we can dynamically -- query the result and put in new constraints based on those. goodSum :: Symbolic [(Integer, Integer)] goodSum = do x <- sInteger "x" diff --git a/Documentation/SBV/Examples/Queries/GuessNumber.hs b/Documentation/SBV/Examples/Queries/GuessNumber.hs --- a/Documentation/SBV/Examples/Queries/GuessNumber.hs +++ b/Documentation/SBV/Examples/Queries/GuessNumber.hs @@ -74,7 +74,7 @@ -- Current bounds: (41,521) -- Current bounds: (42,521) -- Solved in: 9 guesses: --- 971 0 21 31 36 39 40 41 42 +-- 776 0 21 31 36 39 40 41 42 play :: IO () play = do gs <- runSMT (guess 42) putStrLn $ "Solved in: " ++ show (length gs) ++ " guesses:" diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ ## SBV: SMT Based Verification in Haskell -[![Hackage version](http://img.shields.io/hackage/v/sbv.svg?label=Hackage)](http://hackage.haskell.org/package/sbv) +On Hackage: http://hackage.haskell.org/package/sbv Please see: http://leventerkok.github.io/sbv/ diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -73,7 +73,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version) -[RECV] (:version "4.8.9") +[RECV] (:version "4.8.10") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4) @@ -104,7 +104,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version) -[RECV] (:version "4.8.9") +[RECV] (:version "4.8.10") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) @@ -146,8 +146,6 @@ [RECV] (bey hey) [SEND] (get-proof) [RECV] ((set-logic ALL) - (declare-fun bey () Bool) - (declare-fun hey () Bool) (proof (let (($x224 (<= s0 6))) (let (($x225 (not $x224))) 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 @@ -150,7 +150,7 @@ (seq.unit (_ +zero 8 24))) 210))) [SEND] (get-value (q6)) -[RECV] ((q6 (_ as-array q6))) +[RECV] ((q6 ((as const Array) false))) *** Solver : Z3 *** Exit code: ExitSuccess 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 @@ -27,7 +27,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (_ as-array q1))) +[RECV] ((q1 ((as const Array) false))) [GOOD] (define-fun q1_model1 ((x!0 Bool)) Bool false ) 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 @@ -27,7 +27,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q2)) -[RECV] ((q2 (_ as-array q2))) +[RECV] ((q2 ((as const Array) false))) [GOOD] (define-fun q2_model1 ((x!0 Bool) (x!1 Bool)) Bool false ) @@ -290,7 +290,7 @@ [RECV] sat [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))))) + (or (and (not x!1) x!2) (and (not x!1) (not x!2)))))) [SEND] (get-value ((q2 false false))) [RECV] (((q2 false false) true)) [SEND] (get-value ((q2 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 @@ -29,9 +29,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (_ as-array q1))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (_ as-array q2))) +[RECV] ((q2 ((as const Array) false))) [GOOD] (define-fun q1_model1 ((x!0 Bool)) Bool false ) @@ -57,7 +57,7 @@ [SEND] (get-value (q1)) [RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (_ as-array q2))) +[RECV] ((q2 ((as const Array) false))) [GOOD] (define-fun q1_model2 ((x!0 Bool)) Bool true ) @@ -446,19 +446,27 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) -[RECV] ((q2 ((as const Array) true))) +[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_model15 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + false ) [GOOD] (define-fun q1_model15_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model15 x!0)))) [GOOD] (define-fun q2_model15 ((x!0 Bool) (x!1 Bool)) Bool - true + (ite (and (= x!0 false) (= x!1 false)) true + false) ) [GOOD] (define-fun q2_model15_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -473,19 +481,29 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) -[RECV] ((q2 ((as const Array) true))) +[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) + (or (and (not x!1) (not x!2)) (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) 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_model16 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + false ) [GOOD] (define-fun q1_model16_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model16 x!0)))) [GOOD] (define-fun q2_model16 ((x!0 Bool) (x!1 Bool)) Bool - true + (ite (and (= x!0 false) (= x!1 false)) true + (ite (and (= x!0 true) (= x!1 false)) true + false)) ) [GOOD] (define-fun q2_model16_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -500,20 +518,30 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const Array) true) true false false))) +[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) + (or (and (not x!1) (not x!2)) (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) 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_model17 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model17_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model17 x!0)))) [GOOD] (define-fun q2_model17 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 false)) false - true) + (ite (and (= x!0 false) (= x!1 false)) true + (ite (and (= x!0 true) (= x!1 false)) true + false)) ) [GOOD] (define-fun q2_model17_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -528,19 +556,30 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) true))) +[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const Array) true) true false false))) +[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) + (or (and (not x!1) (not x!2)) (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) 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_model18 ((x!0 Bool)) Bool - true + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model18_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model18 x!0)))) [GOOD] (define-fun q2_model18 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 false)) false - true) + (ite (and (= x!0 false) (= x!1 false)) true + (ite (and (= x!0 true) (= x!1 false)) true + false)) ) [GOOD] (define-fun q2_model18_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -557,7 +596,16 @@ [SEND] (get-value (q1)) [RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) -[RECV] ((q2 ((as const Array) true))) +[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) + (or (and (not x!1) (not x!2)) (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) 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_model19 ((x!0 Bool)) Bool true ) @@ -566,7 +614,9 @@ (distinct (q1 x!0) (q1_model19 x!0)))) [GOOD] (define-fun q2_model19 ((x!0 Bool) (x!1 Bool)) Bool - true + (ite (and (= x!0 false) (= x!1 false)) true + (ite (and (= x!0 true) (= x!1 false)) true + false)) ) [GOOD] (define-fun q2_model19_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -581,19 +631,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) -[RECV] ((q2 ((as const Array) false))) +[RECV] ((q2 (store ((as const Array) true) true true false))) [GOOD] (define-fun q1_model20 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + false ) [GOOD] (define-fun q1_model20_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model20 x!0)))) [GOOD] (define-fun q2_model20 ((x!0 Bool) (x!1 Bool)) Bool - false + (ite (and (= x!0 true) (= x!1 true)) false + true) ) [GOOD] (define-fun q2_model20_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -608,28 +658,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[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)) +[RECV] ((q2 (store ((as const Array) true) true true false))) [GOOD] (define-fun q1_model21 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model21_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model21 x!0)))) [GOOD] (define-fun q2_model21 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 false)) true - false) + (ite (and (= x!0 true) (= x!1 true)) false + true) ) [GOOD] (define-fun q2_model21_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -644,17 +686,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[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)) +[RECV] ((q2 (store ((as const Array) true) true true false))) [GOOD] (define-fun q1_model22 ((x!0 Bool)) Bool (ite (and (= x!0 true)) false true) @@ -664,8 +698,8 @@ (distinct (q1 x!0) (q1_model22 x!0)))) [GOOD] (define-fun q2_model22 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) true - false) + (ite (and (= x!0 true) (= x!1 true)) false + true) ) [GOOD] (define-fun q2_model22_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -680,19 +714,18 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const Array) true) false false false))) +[RECV] ((q2 (store ((as const Array) true) true true false))) [GOOD] (define-fun q1_model23 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + true ) [GOOD] (define-fun q1_model23_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model23 x!0)))) [GOOD] (define-fun q2_model23 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) false + (ite (and (= x!0 true) (= x!1 true)) false true) ) [GOOD] (define-fun q2_model23_reject () Bool @@ -708,21 +741,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const Array) true) false false false) true true false))) +[RECV] ((q2 ((as const Array) true))) [GOOD] (define-fun q1_model24 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model24_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model24 x!0)))) [GOOD] (define-fun q2_model24 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) false - (ite (and (= x!0 false) (= x!1 false)) false - true)) + true ) [GOOD] (define-fun q2_model24_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -737,20 +768,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const Array) true) false false false) true false false))) +[RECV] ((q2 (store (store ((as const Array) true) true false false) true true false))) [GOOD] (define-fun q1_model25 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model25_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model25 x!0)))) [GOOD] (define-fun q2_model25 ((x!0 Bool) (x!1 Bool)) Bool + (ite (and (= x!0 true) (= x!1 true)) false (ite (and (= x!0 true) (= x!1 false)) false - (ite (and (= x!0 false) (= x!1 false)) false true)) ) [GOOD] (define-fun q2_model25_reject () Bool @@ -766,28 +797,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true 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)) +[RECV] ((q2 (store (store ((as const Array) true) true false false) true true false))) [GOOD] (define-fun q1_model26 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + false ) [GOOD] (define-fun q1_model26_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model26 x!0)))) [GOOD] (define-fun q2_model26 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) true - false) + (ite (and (= x!0 true) (= x!1 true)) false + (ite (and (= x!0 true) (= x!1 false)) false + true)) ) [GOOD] (define-fun q2_model26_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -802,27 +825,28 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) true))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2)))) +[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and (not x!1) x!2) (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)) +[RECV] (((q2 false true) true)) [SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) false)) +[RECV] (((q2 true false) true)) [SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model27 ((x!0 Bool)) Bool - true + false ) [GOOD] (define-fun q1_model27_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model27 x!0)))) [GOOD] (define-fun q2_model27 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) true - false) + (ite (and (= x!0 false) (= x!1 true)) true + (ite (and (= x!0 true) (= x!1 false)) true + false)) ) [GOOD] (define-fun q2_model27_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -837,7 +861,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) true))) +[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))) @@ -849,7 +873,7 @@ [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model28 ((x!0 Bool)) Bool - true + false ) [GOOD] (define-fun q1_model28_reject () Bool (exists ((x!0 Bool)) @@ -872,28 +896,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) true))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [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))) -[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) true)) +[RECV] ((q2 ((as const Array) false))) [GOOD] (define-fun q1_model29 ((x!0 Bool)) Bool - true + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model29_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model29 x!0)))) [GOOD] (define-fun q2_model29 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 false)) true - (ite (and (= x!0 true) (= x!1 true)) true - false)) + false ) [GOOD] (define-fun q2_model29_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -908,29 +923,28 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [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)))))) +[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) false)) +[RECV] (((q2 false true) true)) [SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) true)) +[RECV] (((q2 true false) false)) [SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model30 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model30_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model30 x!0)))) [GOOD] (define-fun q2_model30 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 false)) true - (ite (and (= x!0 true) (= x!1 true)) true - false)) + (ite (and (= x!0 false) (= x!1 true)) true + false) ) [GOOD] (define-fun q2_model30_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -945,11 +959,12 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) true))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) [RECV] ((q2 (store ((as const Array) true) false false false))) [GOOD] (define-fun q1_model31 ((x!0 Bool)) Bool - true + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model31_reject () Bool (exists ((x!0 Bool)) @@ -972,20 +987,28 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) true))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const Array) true) false false false) true true false))) +[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_model32 ((x!0 Bool)) Bool - true + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model32_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model32 x!0)))) [GOOD] (define-fun q2_model32 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) false - (ite (and (= x!0 false) (= x!1 false)) false - true)) + (ite (and (= x!0 true) (= x!1 true)) true + false) ) [GOOD] (define-fun q2_model32_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1036,20 +1059,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and (not x!1) x!2) (and x!1 (not x!2)))))) +[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) true)) +[RECV] (((q2 true false) false)) [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model34 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + false ) [GOOD] (define-fun q1_model34_reject () Bool (exists ((x!0 Bool)) @@ -1057,8 +1079,7 @@ (q1_model34 x!0)))) [GOOD] (define-fun q2_model34 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 false) (= x!1 true)) true - (ite (and (= x!0 true) (= x!1 false)) true - false)) + false) ) [GOOD] (define-fun q2_model34_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1073,12 +1094,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) [RECV] ((q2 (store (store ((as const Array) true) false false false) false true false))) [GOOD] (define-fun q1_model35 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + false ) [GOOD] (define-fun q1_model35_reject () Bool (exists ((x!0 Bool)) @@ -1104,7 +1124,7 @@ [SEND] (get-value (q1)) [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const Array) true) false false false))) +[RECV] ((q2 (store (store ((as const Array) true) false false false) true false false))) [GOOD] (define-fun q1_model36 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -1114,8 +1134,9 @@ (distinct (q1 x!0) (q1_model36 x!0)))) [GOOD] (define-fun q2_model36 ((x!0 Bool) (x!1 Bool)) Bool + (ite (and (= x!0 true) (= x!1 false)) false (ite (and (= x!0 false) (= x!1 false)) false - true) + true)) ) [GOOD] (define-fun q2_model36_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1130,20 +1151,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const Array) true) true true false))) +[RECV] ((q2 (store (store ((as const Array) true) false false false) true false false))) [GOOD] (define-fun q1_model37 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + false ) [GOOD] (define-fun q1_model37_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model37 x!0)))) [GOOD] (define-fun q2_model37 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) false - true) + (ite (and (= x!0 true) (= x!1 false)) false + (ite (and (= x!0 false) (= x!1 false)) false + true)) ) [GOOD] (define-fun q2_model37_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1160,7 +1181,15 @@ [SEND] (get-value (q1)) [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const Array) true) true true false) false true false))) +[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and (not x!1) x!2) (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) 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_model38 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -1170,9 +1199,9 @@ (distinct (q1 x!0) (q1_model38 x!0)))) [GOOD] (define-fun q2_model38 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) false - (ite (and (= x!0 true) (= x!1 true)) false - true)) + (ite (and (= x!0 false) (= x!1 true)) true + (ite (and (= x!0 true) (= x!1 false)) true + false)) ) [GOOD] (define-fun q2_model38_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1187,20 +1216,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) true))) +[RECV] ((q1 ((as const Array) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const Array) true) true true false) false true false))) +[RECV] ((q2 (store ((as const Array) true) false false false))) [GOOD] (define-fun q1_model39 ((x!0 Bool)) Bool - true + false ) [GOOD] (define-fun q1_model39_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model39 x!0)))) [GOOD] (define-fun q2_model39 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) false - (ite (and (= x!0 true) (= x!1 true)) false - true)) + (ite (and (= x!0 false) (= x!1 false)) false + true) ) [GOOD] (define-fun q2_model39_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1215,26 +1243,26 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) true))) +[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))))) +[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2)))) [SEND] (get-value ((q2 false false))) -[RECV] (((q2 false false) true)) +[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) false)) +[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model40 ((x!0 Bool)) Bool - true + false ) [GOOD] (define-fun q1_model40_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model40 x!0)))) [GOOD] (define-fun q2_model40 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) true + (ite (and (= x!0 true) (= x!1 true)) true false) ) [GOOD] (define-fun q2_model40_reject () Bool @@ -1252,15 +1280,7 @@ [SEND] (get-value (q1)) [RECV] ((q1 (store ((as const Array) true) true 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)) +[RECV] ((q2 ((as const Array) false))) [GOOD] (define-fun q1_model41 ((x!0 Bool)) Bool (ite (and (= x!0 true)) false true) @@ -1270,8 +1290,7 @@ (distinct (q1 x!0) (q1_model41 x!0)))) [GOOD] (define-fun q2_model41 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) true - false) + false ) [GOOD] (define-fun q2_model41_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1286,26 +1305,27 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[RECV] ((q1 (store ((as const Array) true) true false))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2)))) +[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) 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)) +[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model42 ((x!0 Bool)) Bool - false + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model42_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model42 x!0)))) [GOOD] (define-fun q2_model42 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) true + (ite (and (= x!0 true) (= x!1 true)) true false) ) [GOOD] (define-fun q2_model42_reject () Bool @@ -1321,7 +1341,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[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))) @@ -1333,7 +1353,7 @@ [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model43 ((x!0 Bool)) Bool - false + true ) [GOOD] (define-fun q1_model43_reject () Bool (exists ((x!0 Bool)) @@ -1358,13 +1378,13 @@ [SEND] (get-value (q1)) [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)))) +[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) true)) +[RECV] (((q2 false true) false)) [SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) false)) +[RECV] (((q2 true false) true)) [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model44 ((x!0 Bool)) Bool @@ -1375,7 +1395,7 @@ (distinct (q1 x!0) (q1_model44 x!0)))) [GOOD] (define-fun q2_model44 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) true + (ite (and (= x!0 true) (= x!1 false)) true false) ) [GOOD] (define-fun q2_model44_reject () Bool @@ -1391,9 +1411,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[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))))) +[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))) [RECV] (((q2 false false) false)) [SEND] (get-value ((q2 false true))) @@ -1401,9 +1421,9 @@ [SEND] (get-value ((q2 true false))) [RECV] (((q2 true false) true)) [SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) false)) +[RECV] (((q2 true true) true)) [GOOD] (define-fun q1_model45 ((x!0 Bool)) Bool - false + true ) [GOOD] (define-fun q1_model45_reject () Bool (exists ((x!0 Bool)) @@ -1411,7 +1431,8 @@ (q1_model45 x!0)))) [GOOD] (define-fun q2_model45 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 true) (= x!1 false)) true - false) + (ite (and (= x!0 true) (= x!1 true)) true + false)) ) [GOOD] (define-fun q2_model45_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1426,19 +1447,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) -[RECV] ((q2 ((as const Array) false))) +[RECV] ((q2 (store ((as const Array) true) false false false))) [GOOD] (define-fun q1_model46 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + true ) [GOOD] (define-fun q1_model46_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model46 x!0)))) [GOOD] (define-fun q2_model46 ((x!0 Bool) (x!1 Bool)) Bool - false + (ite (and (= x!0 false) (= x!1 false)) false + true) ) [GOOD] (define-fun q2_model46_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1453,28 +1474,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 (store ((as const Array) true) true 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)) +[RECV] ((q2 (store ((as const Array) true) false false false))) [GOOD] (define-fun q1_model47 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model47_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model47 x!0)))) [GOOD] (define-fun q2_model47 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) true - false) + (ite (and (= x!0 false) (= x!1 false)) false + true) ) [GOOD] (define-fun q2_model47_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1489,27 +1502,28 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[RECV] ((q1 (store ((as const Array) true) true false))) [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)))))) +[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and (not x!1) x!2) (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)) +[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)) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model48 ((x!0 Bool)) Bool - false + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model48_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model48 x!0)))) [GOOD] (define-fun q2_model48 ((x!0 Bool) (x!1 Bool)) Bool + (ite (and (= x!0 false) (= x!1 true)) true (ite (and (= x!0 true) (= x!1 false)) true - (ite (and (= x!0 true) (= x!1 true)) true false)) ) [GOOD] (define-fun q2_model48_reject () Bool @@ -1525,28 +1539,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and (not x!1) x!2) (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) true)) -[SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) false)) -[SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) +[RECV] ((q2 (store (store ((as const Array) true) false false false) true true false))) [GOOD] (define-fun q1_model49 ((x!0 Bool)) Bool - false + true ) [GOOD] (define-fun q1_model49_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model49 x!0)))) [GOOD] (define-fun q2_model49 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) true - (ite (and (= x!0 true) (= x!1 true)) true - false)) + (ite (and (= x!0 true) (= x!1 true)) false + (ite (and (= x!0 false) (= x!1 false)) false + true)) ) [GOOD] (define-fun q2_model49_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1561,28 +1567,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[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)) +[RECV] ((q2 (store (store ((as const Array) true) false false false) true false false))) [GOOD] (define-fun q1_model50 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + true ) [GOOD] (define-fun q1_model50_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model50 x!0)))) [GOOD] (define-fun q2_model50 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) true - false) + (ite (and (= x!0 true) (= x!1 false)) false + (ite (and (= x!0 false) (= x!1 false)) false + true)) ) [GOOD] (define-fun q2_model50_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1597,9 +1595,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[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))))) +[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))) @@ -1607,10 +1605,9 @@ [SEND] (get-value ((q2 true false))) [RECV] (((q2 true false) false)) [SEND] (get-value ((q2 true true))) -[RECV] (((q2 true true) true)) +[RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model51 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + true ) [GOOD] (define-fun q1_model51_reject () Bool (exists ((x!0 Bool)) @@ -1618,8 +1615,7 @@ (q1_model51 x!0)))) [GOOD] (define-fun q2_model51 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 false) (= x!1 true)) true - (ite (and (= x!0 true) (= x!1 true)) true - false)) + false) ) [GOOD] (define-fun q2_model51_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1634,19 +1630,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[RECV] ((q1 (store ((as const Array) true) true false))) [SEND] (get-value (q2)) -[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and (not x!1) x!2) (and x!1 (not x!2)))))) +[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) true)) +[RECV] (((q2 true false) false)) [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model52 ((x!0 Bool)) Bool - false + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model52_reject () Bool (exists ((x!0 Bool)) @@ -1654,8 +1651,7 @@ (q1_model52 x!0)))) [GOOD] (define-fun q2_model52 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 false) (= x!1 true)) true - (ite (and (= x!0 true) (= x!1 false)) true - false)) + false) ) [GOOD] (define-fun q2_model52_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1670,19 +1666,29 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[RECV] ((q1 (store ((as const Array) true) true false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const Array) true) false false false))) +[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))) +[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) true)) [GOOD] (define-fun q1_model53 ((x!0 Bool)) Bool - false + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model53_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model53 x!0)))) [GOOD] (define-fun q2_model53 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) false - true) + (ite (and (= x!0 false) (= x!1 true)) true + (ite (and (= x!0 true) (= x!1 true)) true + false)) ) [GOOD] (define-fun q2_model53_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1697,18 +1703,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) true))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const Array) true) false false false) true false false))) +[RECV] ((q2 (store (store ((as const Array) true) false false false) false true false))) [GOOD] (define-fun q1_model54 ((x!0 Bool)) Bool - true + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model54_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model54 x!0)))) [GOOD] (define-fun q2_model54 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 false)) false + (ite (and (= x!0 false) (= x!1 true)) false (ite (and (= x!0 false) (= x!1 false)) false true)) ) @@ -1725,30 +1732,28 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 (store ((as const Array) true) true 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))))) +[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) true)) +[RECV] (((q2 false false) false)) [SEND] (get-value ((q2 false true))) -[RECV] (((q2 false true) true)) +[RECV] (((q2 false true) false)) [SEND] (get-value ((q2 true false))) -[RECV] (((q2 true false) false)) +[RECV] (((q2 true false) true)) [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model55 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model55_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model55 x!0)))) [GOOD] (define-fun q2_model55 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) true - (ite (and (= x!0 false) (= x!1 true)) true - false)) + (ite (and (= x!0 true) (= x!1 false)) true + false) ) [GOOD] (define-fun q2_model55_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1763,19 +1768,29 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) true))) +[RECV] ((q1 (store ((as const Array) true) true false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const Array) true) true true false))) +[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))) +[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) true)) [GOOD] (define-fun q1_model56 ((x!0 Bool)) Bool - true + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model56_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model56 x!0)))) [GOOD] (define-fun q2_model56 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) false - true) + (ite (and (= x!0 true) (= x!1 false)) true + (ite (and (= x!0 true) (= x!1 true)) true + false)) ) [GOOD] (define-fun q2_model56_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1792,12 +1807,11 @@ [SEND] (get-value (q1)) [RECV] ((q1 ((as const Array) true))) [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))))) +[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) true)) +[RECV] (((q2 false true) false)) [SEND] (get-value ((q2 true false))) [RECV] (((q2 true false) false)) [SEND] (get-value ((q2 true true))) @@ -1811,8 +1825,7 @@ (q1_model57 x!0)))) [GOOD] (define-fun q2_model57 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 false) (= x!1 false)) true - (ite (and (= x!0 false) (= x!1 true)) true - false)) + false) ) [GOOD] (define-fun q2_model57_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1827,19 +1840,28 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[RECV] ((q1 (store ((as const Array) true) true false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const Array) true) true true false))) +[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_model58 ((x!0 Bool)) Bool - false + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model58_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model58 x!0)))) [GOOD] (define-fun q2_model58 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) false - true) + (ite (and (= x!0 false) (= x!1 false)) true + false) ) [GOOD] (define-fun q2_model58_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1854,9 +1876,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1)))) +[RECV] ((q1 (store ((as const Array) true) true false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const Array) true) true true false))) +[RECV] ((q2 (store ((as const Array) true) true false false))) [GOOD] (define-fun q1_model59 ((x!0 Bool)) Bool (ite (and (= x!0 true)) false true) @@ -1866,7 +1888,7 @@ (distinct (q1 x!0) (q1_model59 x!0)))) [GOOD] (define-fun q2_model59 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) false + (ite (and (= x!0 true) (= x!1 false)) false true) ) [GOOD] (define-fun q2_model59_reject () Bool @@ -1882,21 +1904,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const Array) true) true true false) false true false))) +[RECV] ((q2 (store ((as const Array) true) true false false))) [GOOD] (define-fun q1_model60 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + true ) [GOOD] (define-fun q1_model60_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model60 x!0)))) [GOOD] (define-fun q2_model60 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) false - (ite (and (= x!0 true) (= x!1 true)) false - true)) + (ite (and (= x!0 true) (= x!1 false)) false + true) ) [GOOD] (define-fun q2_model60_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1911,30 +1931,18 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const Array) true) true false))) +[RECV] ((q1 ((as const Array) true))) [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))))) -[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) false)) +[RECV] ((q2 ((as const Array) true))) [GOOD] (define-fun q1_model61 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + true ) [GOOD] (define-fun q1_model61_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model61 x!0)))) [GOOD] (define-fun q2_model61 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) true - (ite (and (= x!0 false) (= x!1 true)) true - false)) + true ) [GOOD] (define-fun q2_model61_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1949,27 +1957,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[RECV] ((q1 (store ((as const Array) true) true 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)) +[RECV] ((q2 ((as const Array) true))) [GOOD] (define-fun q1_model62 ((x!0 Bool)) Bool - false + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model62_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model62 x!0)))) [GOOD] (define-fun q2_model62 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) true - false) + true ) [GOOD] (define-fun q2_model62_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1984,20 +1984,29 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[RECV] ((q1 ((as const Array) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const Array) true) true true false) false true false))) +[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) + (or (and (not x!1) x!2) (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) 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_model63 ((x!0 Bool)) Bool - false + true ) [GOOD] (define-fun q1_model63_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model63 x!0)))) [GOOD] (define-fun q2_model63 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) false - (ite (and (= x!0 true) (= x!1 true)) false - true)) + (ite (and (= x!0 false) (= x!1 false)) true + (ite (and (= x!0 false) (= x!1 true)) true + false)) ) [GOOD] (define-fun q2_model63_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -2012,7 +2021,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const Array) false))) +[RECV] ((q1 (store ((as const Array) true) true 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))))) @@ -2025,7 +2034,8 @@ [SEND] (get-value ((q2 true true))) [RECV] (((q2 true true) false)) [GOOD] (define-fun q1_model64 ((x!0 Bool)) Bool - false + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model64_reject () Bool (exists ((x!0 Bool)) @@ -2158,142 +2168,145 @@ q2 _ _ = True Solution #15: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 _ _ = True + q2 False False = True + q2 _ _ = False Solution #16: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 _ _ = True + q2 False False = True + q2 True False = True + q2 _ _ = False Solution #17: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True False = False - q2 _ _ = True + q2 False False = True + q2 True False = True + q2 _ _ = False Solution #18: q1 :: Bool -> Bool - q1 _ = True + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 True False = False - q2 _ _ = True + q2 False False = True + q2 True False = True + q2 _ _ = False Solution #19: q1 :: Bool -> Bool q1 _ = True q2 :: Bool -> Bool -> Bool - q2 _ _ = True + q2 False False = True + q2 True False = True + q2 _ _ = False Solution #20: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 _ _ = False + q2 True True = False + q2 _ _ = True Solution #21: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True False = True - q2 _ _ = False + q2 True True = False + q2 _ _ = True Solution #22: q1 :: Bool -> Bool q1 True = False q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 _ _ = False + q2 True True = False + q2 _ _ = True Solution #23: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False False = False - q2 _ _ = True + q2 True True = False + q2 _ _ = True Solution #24: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True True = False - q2 False False = False - q2 _ _ = True + q2 _ _ = True Solution #25: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True False = False - q2 False False = False - q2 _ _ = True + q2 True True = False + q2 True False = False + q2 _ _ = True Solution #26: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True True = True - q2 _ _ = False + q2 True True = False + q2 True False = False + q2 _ _ = True Solution #27: q1 :: Bool -> Bool - q1 _ = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True True = True - q2 _ _ = False + q2 False True = True + q2 True False = True + q2 _ _ = False Solution #28: q1 :: Bool -> Bool - q1 _ = True + q1 _ = False q2 :: Bool -> Bool -> Bool q2 True False = True q2 _ _ = False Solution #29: q1 :: Bool -> Bool - q1 _ = True + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True False = True - q2 True True = True - q2 _ _ = False + q2 _ _ = False Solution #30: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True False = True - q2 True True = True - q2 _ _ = False + q2 False True = True + q2 _ _ = False Solution #31: q1 :: Bool -> Bool - q1 _ = True + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool q2 False False = False q2 _ _ = True Solution #32: q1 :: Bool -> Bool - q1 _ = True + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True True = False - q2 False False = False - q2 _ _ = True + q2 True True = True + q2 _ _ = False Solution #33: q1 :: Bool -> Bool q1 True = True @@ -2304,17 +2317,14 @@ q2 _ _ = False Solution #34: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 True False = True - q2 _ _ = False + q2 False True = True + q2 _ _ = False Solution #35: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 _ = False q2 :: Bool -> Bool -> Bool q2 False True = False @@ -2326,58 +2336,58 @@ q1 _ = False q2 :: Bool -> Bool -> Bool + q2 True False = False q2 False False = False q2 _ _ = True Solution #37: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True True = False - q2 _ _ = True + q2 True False = False + q2 False False = False + q2 _ _ = True Solution #38: q1 :: Bool -> Bool q1 True = True q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False True = False - q2 True True = False - q2 _ _ = True + q2 False True = True + q2 True False = True + q2 _ _ = False Solution #39: q1 :: Bool -> Bool - q1 _ = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False True = False - q2 True True = False - q2 _ _ = True + q2 False False = False + q2 _ _ = True Solution #40: q1 :: Bool -> Bool - q1 _ = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False False = True - q2 _ _ = False + q2 True True = True + q2 _ _ = False Solution #41: q1 :: Bool -> Bool q1 True = False q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False False = True - q2 _ _ = False + q2 _ _ = False Solution #42: q1 :: Bool -> Bool - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 _ _ = False + q2 True True = True + q2 _ _ = False Solution #43: q1 :: Bool -> Bool - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 True True = True @@ -2387,161 +2397,161 @@ q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 _ _ = False + q2 True False = True + q2 _ _ = False Solution #45: q1 :: Bool -> Bool - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 True False = True + q2 True True = True q2 _ _ = False Solution #46: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 _ _ = False + q2 False False = False + q2 _ _ = True Solution #47: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 True True = True - q2 _ _ = False + q2 False False = False + q2 _ _ = True Solution #48: q1 :: Bool -> Bool - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 True False = True - q2 True True = True - q2 _ _ = False + q2 False True = True + q2 True False = True + q2 _ _ = False Solution #49: q1 :: Bool -> Bool - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 True True = True - q2 _ _ = False + q2 True True = False + q2 False False = False + q2 _ _ = True Solution #50: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 _ _ = False + q2 True False = False + q2 False False = False + q2 _ _ = True Solution #51: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False True = True - q2 True True = True q2 _ _ = False Solution #52: q1 :: Bool -> Bool - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 True False = True - q2 _ _ = False + q2 False True = True + q2 _ _ = False Solution #53: q1 :: Bool -> Bool - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False False = False - q2 _ _ = True + q2 False True = True + q2 True True = True + q2 _ _ = False Solution #54: q1 :: Bool -> Bool - q1 _ = True + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True False = False + q2 False True = False q2 False False = False q2 _ _ = True Solution #55: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False False = True - q2 False True = True - q2 _ _ = False + q2 True False = True + q2 _ _ = False Solution #56: q1 :: Bool -> Bool - q1 _ = True + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 True True = False - q2 _ _ = True + q2 True False = True + q2 True True = True + q2 _ _ = False Solution #57: q1 :: Bool -> Bool q1 _ = True q2 :: Bool -> Bool -> Bool q2 False False = True - q2 False True = True q2 _ _ = False Solution #58: q1 :: Bool -> Bool - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 True True = False - q2 _ _ = True + q2 False False = True + q2 _ _ = False Solution #59: q1 :: Bool -> Bool q1 True = False q1 _ = True q2 :: Bool -> Bool -> Bool - q2 True True = False - q2 _ _ = True + q2 True False = False + q2 _ _ = True Solution #60: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = False - q2 True True = False - q2 _ _ = True + q2 True False = False + q2 _ _ = True Solution #61: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False False = True - q2 False True = True - q2 _ _ = False + q2 _ _ = True Solution #62: q1 :: Bool -> Bool - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False False = True - q2 _ _ = False + q2 _ _ = True Solution #63: q1 :: Bool -> Bool - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = False - q2 True True = False - q2 _ _ = True + q2 False False = True + q2 False True = True + q2 _ _ = False Solution #64: q1 :: Bool -> Bool - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False False = True diff --git a/SBVTestSuite/GoldFiles/uninterpreted-3.gold b/SBVTestSuite/GoldFiles/uninterpreted-3.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/uninterpreted-3.gold @@ -0,0 +1,38 @@ +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-logic QF_UFBV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- tuples --- +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] (declare-fun p () Bool) +[GOOD] (declare-fun q () Bool) +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s0 () Bool p) +[GOOD] (define-fun s1 () Bool q) +[GOOD] (define-fun s2 () Bool (or s0 s1)) +[GOOD] (assert s2) +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (p)) +[RECV] ((p true)) +[SEND] (get-value (q)) +[RECV] ((q false)) +*** Solver : Z3 +*** Exit code: ExitSuccess + + FINAL:Satisfiable. Model: + p = True :: Bool + q = False :: Bool +DONE! diff --git a/SBVTestSuite/GoldFiles/uninterpreted-3a.gold b/SBVTestSuite/GoldFiles/uninterpreted-3a.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/uninterpreted-3a.gold @@ -0,0 +1,72 @@ +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-logic QF_UFBV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- tuples --- +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] (declare-fun p () Bool) +[GOOD] (declare-fun q () Bool) +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s0 () Bool p) +[GOOD] (define-fun s1 () Bool q) +[GOOD] (define-fun s2 () Bool (or s0 s1)) +[GOOD] (assert s2) +*** Checking Satisfiability, all solutions.. +Looking for solution 1 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (p)) +[RECV] ((p true)) +[SEND] (get-value (q)) +[RECV] ((q false)) +[GOOD] (define-fun s3 () Bool (distinct true s0)) +[GOOD] (define-fun s4 () Bool (or s1 s3)) +[GOOD] (assert s4) +Looking for solution 2 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (p)) +[RECV] ((p false)) +[SEND] (get-value (q)) +[RECV] ((q true)) +[GOOD] (define-fun s5 () Bool (distinct true s1)) +[GOOD] (define-fun s6 () Bool (or s0 s5)) +[GOOD] (assert s6) +Looking for solution 3 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (p)) +[RECV] ((p true)) +[SEND] (get-value (q)) +[RECV] ((q true)) +[GOOD] (define-fun s7 () Bool (or s3 s5)) +[GOOD] (assert s7) +Looking for solution 4 +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess + + FINAL:Solution #1: + p = True :: Bool + q = False :: Bool +Solution #2: + p = False :: Bool + q = True :: Bool +Solution #3: + p = True :: Bool + q = True :: Bool +Found 3 different solutions. +DONE! diff --git a/SBVTestSuite/GoldFiles/uninterpreted-4.gold b/SBVTestSuite/GoldFiles/uninterpreted-4.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/uninterpreted-4.gold @@ -0,0 +1,39 @@ +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-logic ALL) ; has user-defined sorts, using catch-all. +[GOOD] ; --- uninterpreted sorts --- +[GOOD] (declare-sort Q 0) ; N.B. Uninterpreted sort. +[GOOD] ; --- tuples --- +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] (declare-fun c () Q) +[GOOD] (declare-fun d () Q) +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s0 () Q c) +[GOOD] (define-fun s1 () Q d) +[GOOD] (define-fun s2 () Bool (distinct s0 s1)) +[GOOD] (assert s2) +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (c)) +[RECV] ((c Q!val!0)) +[SEND] (get-value (d)) +[RECV] ((d Q!val!1)) +*** Solver : Z3 +*** Exit code: ExitSuccess + + FINAL:Satisfiable. Model: + c = Q!val!0 :: Q + d = Q!val!1 :: Q +DONE! diff --git a/SBVTestSuite/GoldFiles/uninterpreted-4a.gold b/SBVTestSuite/GoldFiles/uninterpreted-4a.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/uninterpreted-4a.gold @@ -0,0 +1,50 @@ +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-logic ALL) ; has user-defined sorts, using catch-all. +[GOOD] ; --- uninterpreted sorts --- +[GOOD] (declare-sort Q 0) ; N.B. Uninterpreted sort. +[GOOD] ; --- tuples --- +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] (declare-fun c () Q) +[GOOD] (declare-fun d () Q) +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s0 () Q c) +[GOOD] (define-fun s1 () Q d) +[GOOD] (define-fun s2 () Bool (distinct s0 s1)) +[GOOD] (assert s2) +*** Checking Satisfiability, all solutions.. +*** SBV.allSat: Uninterpreted function: c :: Q +*** Will *not* be used in allSat considerations since its type +*** has uninterpreted sorts present. +*** SBV.allSat: Uninterpreted function: d :: Q +*** Will *not* be used in allSat considerations since its type +*** has uninterpreted sorts present. +*** SBV.allSat: Uninterpreted sorts present: Q +*** SBV will use equivalence classes to generate all-satisfying instances. +Looking for solution 1 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (c)) +[RECV] ((c Q!val!0)) +[SEND] (get-value (d)) +[RECV] ((d Q!val!1)) +*** Solver : Z3 +*** Exit code: ExitSuccess + + FINAL:Solution #1: + c = Q!val!0 :: Q + d = Q!val!1 :: Q +This is the only solution. +DONE! 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 @@ -25,11 +25,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (fp #b1 #xfe #b11111111111111111111111))) +[RECV] ((s0 (_ +zero 8 24))) *** Solver : Z3 *** Exit code: ExitSuccess [VALIDATE] Validating the model. Assignment: -[VALIDATE] x = -3.4028235e38 :: Float +[VALIDATE] x = 0.0 :: Float [VALIDATE] There are no constraints to check. [VALIDATE] Validating outputs. @@ -38,7 +38,7 @@ *** *** Assignment: *** -*** x = -3.4028235e38 :: Float +*** x = 0.0 :: Float *** *** Not all floating point operations are supported concretely. *** @@ -48,4 +48,4 @@ *** Alleged model: *** *** Satisfiable. Model: -*** x = -3.4028235e38 :: Float +*** 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 @@ -25,11 +25,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (fp #b0 #x03 #b11010011011011001000000))) +[RECV] ((s0 (_ -zero 8 24))) *** Solver : Z3 *** Exit code: ExitSuccess [VALIDATE] Validating the model. Assignment: -[VALIDATE] x = 8.58522e-38 :: Float +[VALIDATE] x = -0.0 :: Float [VALIDATE] There are no constraints to check. [VALIDATE] Validating outputs. @@ -38,7 +38,7 @@ *** *** Assignment: *** -*** x = 8.58522e-38 :: Float +*** x = -0.0 :: Float *** *** Floating point FMA operation is not supported concretely. *** @@ -48,4 +48,4 @@ *** Alleged model: *** *** Satisfiable. Model: -*** x = 8.58522e-38 :: Float +*** x = -0.0 :: Float diff --git a/SBVTestSuite/SBVDocTest.hs b/SBVTestSuite/SBVDocTest.hs --- a/SBVTestSuite/SBVDocTest.hs +++ b/SBVTestSuite/SBVDocTest.hs @@ -51,6 +51,7 @@ , "QuickCheck" , "random" , "syb" + , "uniplate" ] pargs = concatMap (\p -> ["-package", p]) packages diff --git a/SBVTestSuite/TestSuite/Uninterpreted/Uninterpreted.hs b/SBVTestSuite/TestSuite/Uninterpreted/Uninterpreted.hs --- a/SBVTestSuite/TestSuite/Uninterpreted/Uninterpreted.hs +++ b/SBVTestSuite/TestSuite/Uninterpreted/Uninterpreted.hs @@ -8,20 +8,33 @@ -- ----------------------------------------------------------------------------- -{-# OPTIONS_GHC -Wall -Werror #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -Wall -Werror #-} module TestSuite.Uninterpreted.Uninterpreted(tests) where import Utils.SBVTestFramework +data Q +mkUninterpretedSort ''Q + -- Test suite tests :: TestTree tests = testGroup "Uninterpreted.Uninterpreted" - [ testCase "uninterpreted-0" (assertIsThm p0) - , testCase "uninterpreted-1" (assertIsThm p1) - , testCase "uninterpreted-2" (assertIsntThm p2) + [ testCase "uninterpreted-0" $ assertIsThm p0 + , testCase "uninterpreted-1" $ assertIsThm p1 + , testCase "uninterpreted-2" $ assertIsntThm p2 + , goldenCapturedIO "uninterpreted-3" $ t p3 satWith + , goldenCapturedIO "uninterpreted-3a" $ t p3 allSatWith + , goldenCapturedIO "uninterpreted-4" $ t p4 satWith + , goldenCapturedIO "uninterpreted-4a" $ t p4 allSatWith ] + where t tc chk goldFile = do r <- chk defaultSMTCfg{verbose = True, redirectVerbose = Just goldFile} tc + appendFile goldFile ("\n FINAL:" ++ show r ++ "\nDONE!\n") f :: SInt8 -> SWord32 f = uninterpret "f" @@ -37,3 +50,18 @@ p2 :: SInt8 -> SWord16 -> SWord16 -> SBool p2 x y z = y .== z .=> g x y .== f x -- Not true + + +a, b :: SBool +a = sym "p" +b = sym "q" + +p3 :: SBool +p3 = a .|| b + +c, d :: SQ +c = sym "c" +d = sym "d" + +p4 :: SBool +p4 = c ./= d diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 8.8 +Version : 8.9 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 @@ -83,7 +83,7 @@ build-depends : crackNum , QuickCheck, template-haskell , array, async, containers, deepseq, directory, filepath, time - , pretty, process, mtl, random, syb, transformers + , pretty, process, mtl, random, syb, transformers, uniplate Exposed-modules : Data.SBV , Data.SBV.Control , Data.SBV.Dynamic