diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,10 +1,43 @@ * Hackage: * GitHub: -* Latest Hackage released version: 7.12, 2018-09-23 +* Latest Hackage released version: 7.13, 2018-12-16 +### Version 7.13, 2018-12-16 + + * Generalize the types of `bminimum` and `bmaximum` by removing the `Num` + constraint. + + * Change the type of `observe` from: `SymWord a => String -> SBV a -> Symbolic ()` + to `SymWord a => String -> SBV a -> SBV a`. This allows for more concise observables, + like this: + + prove $ \x -> observe "lhs" (x+x) .== observe "rhs" (2*x+1) + Falsifiable. Counter-example: + s0 = 0 :: Integer + lhs = 0 :: Integer + rhs = 1 :: Integer + + * Add `Data.SBV.Tools.Range` module which defines `ranges` and `rangesWith` functions: They + compute the satisfying contiguous ranges for predicates with a single variable. See + `Data.SBV.Tools.Range` for examples. + + * Add `Data.SBV.Tools.BoundedFix` module, which defines the operator `bfix` that can be used + as a bounded fixed-point operator for use in bounded-model-checking like algorithms. See + `Data.SBV.Tools.BoundedFix` for some example use cases. + + * Fix list-element extraction code, which asserted too strong a constraint. See issue #421 + for details. Thanks to Joel Burget for reporting. + + * New bounded list functions: `breverse`, `bsort`, `bfoldrM`, `bfoldlM`, and `bmapM`. + Contributed by Joel Burget. + + * Add two new puzzle examples: + * `Documentation.SBV.Examples.Puzzles.LadyAndTigers` + * `Documentation.SBV.Examples.Puzzles.Garden` + ### Version 7.12, 2018-09-23 - + * Modifications to make SBV compile with GHC 8.6.1. (SBV should now compile fine with all versions of GHC since 8.0.1; and possibly earlier. Please report if you are using a version @@ -36,6 +69,9 @@ supported. ### Version 7.10, 2018-07-20 + * [BACKWARDS COMPATIBILITY] '==' and '/=' now always throw an error instead of + only throwing an error for non-concrete values. + https://github.com/LeventErkok/sbv/issues/301 * [BACKWARDS COMPATIBILITY] Array declarations are reworked to take an initial value. The call 'newArray' now accepts an optional default @@ -119,7 +155,7 @@ synchronous errors.) Thanks to Oliver Charles for pointing out this corner case. ### Version 7.9, 2018-06-15 - + * Add support for bit-vector arithmetic underflow/overflow detection. The new 'ArithmeticOverflow' class captures conditions under which addition, subtraction, multiplication, division, and negation can underflow/overflow for @@ -145,7 +181,7 @@ your old code will need some modifications. See the example in Documentation.SBV.Examples.Queries.Interpolants for the new usage. - * Add 'constrainWithAttribute' call, which can be used to attach + * Add 'constrainWithAttribute' call, which can be used to attach arbitrary attribute to a constraint. Main use case is in interpolant generation with MathSAT. @@ -154,11 +190,11 @@ * Code reorg: Simplify constant mapping table, by properly accounting for negative-zero floats. - + * Export 'sexprToVal' for the class SMTValue, which allows for custom definitions of value extractions. Thanks to Brian Schroeder for the patch. - + * Export 'Logic' directly from Data.SBV. (Previously was from Control.) * Fix a long standing issue (ever since we introduced queries) where @@ -205,7 +241,7 @@ * Add support for Symbolic characters ('SChar') and strings ('SString'.) Thanks to Joel Burget for the initial implementation. - + The 'SChar' type currently corresponds to the Latin-1 character set, and is thus a subset of the Haskell 'Char' type. This is due to the current limitations in SMT-solvers. However, there @@ -374,7 +410,7 @@ Optimization routines now properly handle quantified formulas, so long as the quantified metric does not involve any universal quantification itself. Thanks to Matthew Danish for reporting the issue. - + * Development/Infrastructure: Lots of work around the continuous integration for SBV. We now build/test on Linux/Mac/Windows on every commit. Thanks to Travis/Appveyor for providing free remote infrastructure. There are still @@ -382,7 +418,7 @@ would like to be involved and improve the test suite, please get in touch! ### Version 7.1, 2017-07-29 - + * Add support for 'getInterpolant' in Query mode. * Support for SMT-results that can contain multi-line strings, which @@ -516,7 +552,7 @@ * Add support for unsat-core extraction. To use this feature, use the `namedConstraint` function: - + namedConstraint :: String -> SBool -> Symbolic () to associate a label to a constrain or a boolean term that @@ -538,7 +574,7 @@ as speculated in the SMT-Lib document itself. Currently, Z3, MathSAT, and CVC4 backends support unsat-cores. - + (Thanks to Rohit Ramesh for the suggestion leading to this feature.) * Added function `distinct`, which returns true if all the elements of the @@ -574,7 +610,7 @@ but the fix should be as simple as `import Data.SBV.Tools.CodeGen`. * Move the following two functions to `Data.SBV.Internals`: - + compileToSMTLib generateSMTBenchmarks @@ -614,8 +650,8 @@ - `minimize`: Minimize a given arithmetic goal - `maximize`: Minimize a given arithmetic goal - For instance, a call of the form - + For instance, a call of the form + minimize "name-of-goal" $ x + 2*y Minimizes the arithmetic goal x+2*y, where x and y can be bit-vectors, reals, @@ -633,7 +669,7 @@ a user-given numeric penalty to satisfy the remaining constraints. The solver then tries to minimize the penalty, i.e., satisfy as many of the soft-asserts as possible such that the total penalty for those that are not satisfied is minimized. - + Note that `assertSoft` works well with optimization goals (minimize/maximize etc.), and are most useful when we are optimizing a metric and thus some of the constraints can be relaxed with a penalty to obtain a good solution. @@ -667,7 +703,7 @@ - `Data.SBV.Tools.GenTest` (test case generation) - `Data.SBV.Tools.Polynomial` (polynomial arithmetic, CRCs etc.) - `Data.SBV.Tools.STree` (full symbolic binary trees) - + To use the functionality of these modules, users must now explicitly import the corresponding module. Not other changes should be needed other than the explicit import. @@ -697,14 +733,14 @@ - Data.SBV.Examples.Optimization.LinearOpt: Simple linear-optimization example. - Data.SBV.Examples.Optimization.Production: Scheduling machines in a shop - Data.SBV.Examples.Optimization.VM: Scheduling virtual-machines in a data-center - + ### Version 5.15, 2017-01-30 * Bump up dependency on CrackNum >= 1.9, to get access to hexadecimal floats. * Improve time/tracking-print code. Thanks to Iavor Diatchki for the patch. ### Version 5.14, 2017-01-12 - + * Bump up QuickCheck dependency to >= 2.9.2 to avoid the following quick-check bug , which transitively impacted the quick-check as implemented by SBV. @@ -798,7 +834,7 @@ generalizations are also done for the dynamic variants. ### Version 5.6, 2015-12-06 - + * Minor changes to how we print models: * Align by the type * Always print the type (previously we were skipping for Bool) @@ -827,7 +863,7 @@ it simply returns its final argument. Use in coordination with 'safe' and 'safeWith', see below. * Implement 'safe' and 'safeWith', which statically determine all calls to 'sAssert' - being safe to execute. Any violations will be flagged. + being safe to execute. Any violations will be flagged. * SBV->C: Translate 'sAssert' calls to dynamic checks in the generated C code. If this is not desired, use the 'cgIgnoreSAssert' function to turn it off. @@ -860,7 +896,7 @@ output. SBV similarly changed to allow for non-determinism here. * Change the types of the following Floating-point operations: - + * sFloatAsSWord32, sFloatAsSWord32, blastSFloat, blastSDouble These were previously coded as relations, since NaN values were not representable @@ -948,12 +984,12 @@ * Boolector: Upgraded to work with new Boolector release 2.0.7. Note that earlier versions of Boolector are *not* supported. - + * MathSAT: Upgraded to work with latest release 5.3.7. Note that earlier versions of MathSAT are *not* supported (due to a buffering issue in MathSAT itself.) - + * MathSAT: Enabled floating-point support in MathSAT. - + * New examples: * Add Data.SBV.Examples.Puzzles.Birthday, which solves the Cheryl-Birthday problem that @@ -974,7 +1010,7 @@ * Rework floating-point arithmetic, and add missing floating-point operations: * fpRem : remainder - * fpRoundToIntegral: truncating round + * fpRoundToIntegral: truncating round * fpMin : min * fpMax : max * fpIsEqualObject : FP equality as object (i.e., NaN equals NaN, +0 does not equal -0, etc.) @@ -993,7 +1029,7 @@ equivalent to 'map sTestBit'. * Rename a set of symbolic functions for consistency. Here are the old/new names: - + * sbvTestBit --> sTestBit * sbvPopCount --> sPopCount * sbvShiftLeft --> sShiftLeft @@ -1004,16 +1040,16 @@ * Rename all FP recognizers to be in sync with FP operations. Here are the old/new names: - * isNormalFP --> fpIsNormal - * isSubnormalFP --> fpIsSubnormal - * isZeroFP --> fpIsZero - * isInfiniteFP --> fpIsInfinite - * isNaNFP --> fpIsNaN - * isNegativeFP --> fpIsNegative - * isPositiveFP --> fpIsPositive - * isNegativeZeroFP --> fpIsNegativeZero - * isPositiveZeroFP --> fpIsPositiveZero - * isPointFP --> fpIsPoint + * isNormalFP --> fpIsNormal + * isSubnormalFP --> fpIsSubnormal + * isZeroFP --> fpIsZero + * isInfiniteFP --> fpIsInfinite + * isNaNFP --> fpIsNaN + * isNegativeFP --> fpIsNegative + * isPositiveFP --> fpIsPositive + * isNegativeZeroFP --> fpIsNegativeZero + * isPositiveZeroFP --> fpIsPositiveZero + * isPointFP --> fpIsPoint * Lots of other work around floating-point, test cases, reorg, etc. @@ -1025,7 +1061,7 @@ * Hook-up crackNum package; so counter-examples involving floats and doubles can be printed in detail when the printBase is chosen to be - 2 or 16. (With base 10, we still get the simple output.) + 2 or 16. (With base 10, we still get the simple output.) ``` Prelude Data.SBV> satWith z3{printBase=2} $ \x -> x .== (2::SFloat) @@ -1070,7 +1106,7 @@ unliteral. Contributed by Brian Huffman. * Introduce FP conversion functions: - + * Between SReal and SFloat/SDouble * fpToSReal * sRealToSFloat @@ -1115,7 +1151,7 @@ * Silence some hlint/ghci warnings. Thanks to Trevor Elliott for the patch! * Haddock documentation fixes, improvements, etc. - + * Change ABC default option string to %blast; "&sweep -C 5000; &syn4; &cec -s -m -C 2000" which seems to give good results. Use SBV_ABC_OPTIONS environment variable (or via abc.rc file and a combination of SBV_ABC_OPTIONS) to experiment. @@ -1140,12 +1176,12 @@ RoundNearestTiesToAway, but with SBV, we get all 5 IEEE754 rounding-modes and all the basic operations ('fpAdd', 'fpMul', 'fpDiv', etc.) with these modes. - + * Allow Floating-Point RoundingMode to be symbolic as well * Improve the example "Data/SBV/Examples/Misc/Floating.hs" to include rounding-mode based addition example. - + * Changes required to make SBV compile with GHC 7.10; mostly around instance NFData declarations. Thanks to Iavor Diatchki for the patch. @@ -1161,7 +1197,7 @@ but in the interim, this release provides a means for the users to introduce individual instances. - * Modifications to support arbitrary bit-sized vectors; + * Modifications to support arbitrary bit-sized vectors; These changes have been contributed by Brian Huffman of Galois.. Thanks Brian. * A new example "Data/SBV/Examples/Misc/Word4.hs" showing @@ -1240,14 +1276,14 @@ means that you need at least v2.0.0 of Boolector installed if you want to use that particular solver. - * Fix long-standing translation bug regarding boolean Ord class comparisons. (i.e., + * Fix long-standing translation bug regarding boolean Ord class comparisons. (i.e., 'False > True' etc.) While Haskell allows for this, SMT-Lib does not; and hence we have to be careful in translating. Thanks to Brian Huffman for reporting. * C code generation: Correctly translate square-root and fusedMA functions to C. ### Version 3.1, 2014-07-12 - + NB: GHC 7.8.1 and 7.8.2 has a serious bug that causes SBV to crash under heavy/repeated calls. The bug is addressed in GHC 7.8.3; so upgrading to GHC 7.8.3 is essential for using SBV! @@ -1272,7 +1308,7 @@ simulation, if termination can be established this way. Needless to say, this problem is always decidable as far as SBV programs are concerned, but it does not mean the decision procedure is cheap! - Use with care. + Use with care. * sBranchTimeOut config parameter can be used to curtail long runs when sBranch is used. Of course, if time-out happens, SBV will assume the branch is feasible, in which case symbolic-termination @@ -1297,7 +1333,7 @@ user-visible impact, but comes in handy for internal reasons. ### Version 3.0, 2014-02-16 - + * Support for floating-point numbers: * Preliminary support for IEEE-floating point arithmetic, introducing the types `SFloat` and `SDouble`. The support is still quite new, @@ -1345,7 +1381,7 @@ z3 complete the proof quickly. (The BV logics take too long for this problem.) ### Version 2.10, 2013-03-22 - + * Add support for the Boolector SMT solver * See: http://fmv.jku.at/boolector/ * Use `import Data.SBV.Bridge.Boolector` to use Boolector from SBV @@ -1398,7 +1434,7 @@ import Data.SBV.Bridge.CVC4 import Data.SBV.Bridge.Yices import Data.SBV.Bridge.Z3 - + to pick the appropriate default solver. if you simply 'import Data.SBV', then you will get the default SMT solver, which is currently Z3. The value 'defaultSMTSolver' refers to z3 (currently), and 'sbvCurrentSolver' refers @@ -1444,7 +1480,7 @@ is also an instance of this class, and SDivisible is a more appropriate name to start with. Also add sQuot and sRem methods; along with sDivMod, sDiv, and sMod, with usual - semantics. + semantics. * Improve test suite, adding many constant-folding tests and start using cabal based tests (--enable-tests option.) @@ -1501,7 +1537,7 @@ for illustrating uninterpreted sorts and axioms. ### Version 2.0, 2012-05-10 - + This is a major release of SBV, adding support for symbolic algebraic reals: SReal. See http://en.wikipedia.org/wiki/Algebraic_number for details. In brief, algebraic reals are solutions to univariate polynomials with rational coefficients. The arithmetic @@ -1510,7 +1546,7 @@ representable in this way. (For instance, "sqrt 2" is algebraic, but pi, e are not.) However, algebraic reals is a superset of rationals, so SBV now also supports symbolic rationals as well. - + You *should* use Z3 v4.0 when working with real numbers. While the interface will work with older versions of Z3 (or other SMT solvers in general), it uses Z3 root-obj construct to retrieve and query algebraic reals. @@ -1680,7 +1716,7 @@ was not worth the complexity. ### Version 0.9.23, 2011-12-05 - + Library: * Add support for SInteger, the type of signed unbounded integer @@ -1709,7 +1745,7 @@ multiplication of two variables.) ### Version 0.9.22, 2011-11-13 - + The major change in this release is the support for quantifiers. The SBV library *no* longer assumes all variables are universals in a proof, (and correspondingly existential in a sat) call. Instead, the user @@ -1721,7 +1757,7 @@ This release also adds support for the Z3 solver, which is the main SMT-solver used for solving formulas involving quantifiers. More formally, - we use the new AUFBV/ABV/UFBV logics when quantifiers are involved. Also, + we use the new AUFBV/ABV/UFBV logics when quantifiers are involved. Also, the communication with Z3 is now done via SMT-Lib2 format. Eventually the SMTLib1 connection will be severed. @@ -1759,7 +1795,7 @@ * Add USB CRC code generation example, both via polynomials and using the internal CRC functionality ### Version 0.9.21, 2011-08-05 - + Code generation: * Allow for inclusion of user makefiles @@ -1767,7 +1803,7 @@ * Other minor clean-up ### Version 0.9.20, 2011-06-05 - + Regression on 0.9.19; add missing file to cabal ### Version 0.9.19, 2011-06-05 @@ -1804,7 +1840,7 @@ AES encryption ### Version 0.9.17, 2011-03-29 - + Code: * Simplify and reorganize the test suite @@ -1813,7 +1849,7 @@ * Improve AES decryption example, by using table-lookups in InvMixColumns. - + ### Version 0.9.16, 2011-03-28 Code: @@ -1827,7 +1863,7 @@ for use with the code-generator ### Version 0.9.15, 2011-03-24 - + Bug fixes: * Fix rotateL/rotateR instances on concrete @@ -1845,14 +1881,14 @@ of them, ~30K, but they run quickly.) ### Version 0.9.14, 2011-03-19 - + * Re-implement sharing using Stable names, inspired by the Data.Reify techniques. This avoids tricks with unsafe memory stashing, and hence is safe. Thus, issues with respect to CAFs are now resolved. ### Version 0.9.13, 2011-03-16 - + Bug fixes: * Make sure SBool short-cut evaluations are done @@ -1867,7 +1903,7 @@ * Add a GCD code-generation/verification example ### Version 0.9.12, 2011-03-10 - + New features: * Add support for compilation to C @@ -1879,7 +1915,7 @@ * Specification bug in Legatos multiplier example ### Version 0.9.11, 2011-02-16 - + * Make ghc-7.0 happy, minor re-org on the cabal file/Setup.hs ### Version 0.9.10, 2011-02-15 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: -- @@ -240,7 +240,7 @@ , OptimizeStyle(..) -- ** Objectives , Objective(..), Metric(..) - -- ** Soft assumptions + -- ** Soft assertions -- $softAssertions , assertWithPenalty , Penalty(..) -- ** Field extensions @@ -501,8 +501,8 @@ >>> safe (sub :: SInt8 -> SInt8 -> SInt8) [sub: x >= y must hold!: Violated. Model: - s0 = 30 :: Int8 - s1 = 32 :: Int8] + s0 = 6 :: Int8 + s1 = 8 :: Int8] What happens if we make sure to arrange for this invariant? Consider this version: @@ -995,9 +995,7 @@ res = ite (a1 .== 12 &&& a2 .== 22) -- insert a malicious bug! 1 (a1 + a2) - observe "Expected" spec - observe "Result" res - return $ spec .== res + return $ observe "Expected" spec .== observe "Result" res :} Falsifiable. Counter-example: i1 = 12 :: Word8 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 @@ -336,18 +336,38 @@ getObjValue :: (forall a. Maybe [String] -> Query a) -> [NamedSymVar] -> SExpr -> Query (Maybe (String, GeneralizedCW)) getObjValue bailOut inputs expr = case expr of - EApp [_] -> return Nothing -- Happens when a soft-assertion has no associated group. - EApp [ECon nm, v] -> locate nm v -- Regular case - EApp [EApp [ECon "bvadd", ECon nm, ENum _], v] -> locate nm v -- Happens when we "adjust" a signed-bounded objective - _ -> dontUnderstand (show expr) + EApp [_] -> return Nothing -- Happens when a soft-assertion has no associated group. + EApp [ECon nm, v] -> locate nm v Nothing -- Regular case + EApp [EApp [ECon "bvadd", ECon nm, ENum (a, _)], v] -> locate nm v (Just a) -- Happens when we "adjust" a signed-bounded objective + _ -> dontUnderstand (show expr) - where locate nm v = case listToMaybe [p | p@(sw, _) <- inputs, show sw == nm] of - Nothing -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names - Just (sw, actualName) -> grab sw v >>= \val -> return $ Just (actualName, val) + where locate nm v mbAdjust = case listToMaybe [p | p@(sw, _) <- inputs, show sw == nm] of + Nothing -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names + Just (sw, actualName) -> grab sw v >>= \val -> return $ Just (actualName, signAdjust mbAdjust val) dontUnderstand s = bailOut $ Just [ "Unable to understand solver output." , "While trying to process: " ++ s ] + + signAdjust :: Maybe Integer -> GeneralizedCW -> GeneralizedCW + signAdjust Nothing v = v + signAdjust (Just adj) e = goG e + where goG :: GeneralizedCW -> GeneralizedCW + goG (ExtendedCW ecw) = ExtendedCW $ goE ecw + goG (RegularCW cw) = RegularCW $ go cw + + goE :: ExtCW -> ExtCW + goE (Infinite k) = Infinite k + goE (Epsilon k) = Epsilon k + goE (Interval lo hi) = Interval (goE lo) (goE hi) + goE (BoundedCW cw) = BoundedCW (go cw) + goE (AddExtCW a b) = AddExtCW (goE a) (goE b) + goE (MulExtCW a b) = MulExtCW (goE a) (goE b) + + go :: CW -> CW + go cw = case (kindOf cw, cwVal cw) of + (k@(KBounded True _), CWInteger v) -> normCW $ CW k (CWInteger (v - adj)) + _ -> error $ "SBV.getObjValue: Unexpected cw received! " ++ show cw grab :: SW -> SExpr -> Query GeneralizedCW grab s topExpr diff --git a/Data/SBV/Core/Data.hs b/Data/SBV/Core/Data.hs --- a/Data/SBV/Core/Data.hs +++ b/Data/SBV/Core/Data.hs @@ -243,14 +243,14 @@ sRTZ = sRoundTowardZero -- | A 'Show' instance is not particularly "desirable," when the value is symbolic, --- but we do need this instance as otherwise we cannot simply evaluate Haskell functions +-- but we do need this instance as otherwise we cannot simply evaluate Haskell functions -- that return symbolic values and have their constant values printed easily! instance Show (SBV a) where show (SBV sv) = show sv --- | Equality constraint on SBV values. Not desirable since we can't really compare two --- symbolic values, but will do. Note that we do need this instance since we want --- Bits as a class for SBV that we implement, which necessiates the Eq class. +-- | This instance is only defined so that we can define an instance for +-- 'Data.Bits.Bits'. '==' and '/=' simply throw an error. Use +-- 'Data.SBV.EqSymbolic' instead. instance Eq (SBV a) where SBV a == SBV b = a == b SBV a /= SBV b = a /= b 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 @@ -18,7 +18,7 @@ , blastSFloat, blastSDouble ) where -import qualified Data.ReinterpretCast as RC (wordToFloat, wordToDouble, floatToWord, doubleToWord) +import qualified Data.Numbers.CrackNum as CN (wordToFloat, wordToDouble, floatToWord, doubleToWord) import Data.Int (Int8, Int16, Int32, Int64) import Data.Word (Word8, Word16, Word32, Word64) @@ -379,7 +379,7 @@ sFloatAsSWord32 :: SFloat -> SWord32 sFloatAsSWord32 fVal | Just f <- unliteral fVal, not (isNaN f) - = literal (RC.floatToWord f) + = literal (CN.floatToWord f) | True = SBV (SVal w32 (Right (cache y))) where w32 = KBounded False 32 @@ -400,7 +400,7 @@ sDoubleAsSWord64 :: SDouble -> SWord64 sDoubleAsSWord64 fVal | Just f <- unliteral fVal, not (isNaN f) - = literal (RC.doubleToWord f) + = literal (CN.doubleToWord f) | True = SBV (SVal w64 (Right (cache y))) where w64 = KBounded False 64 @@ -428,7 +428,7 @@ -- | Reinterpret the bits in a 32-bit word as a single-precision floating point number sWord32AsSFloat :: SWord32 -> SFloat sWord32AsSFloat fVal - | Just f <- unliteral fVal = literal $ RC.wordToFloat f + | Just f <- unliteral fVal = literal $ CN.wordToFloat f | True = SBV (SVal KFloat (Right (cache y))) where y st = do xsw <- sbvToSW st fVal newExpr st KFloat (SBVApp (IEEEFP (FP_Reinterpret (kindOf fVal) KFloat)) [xsw]) @@ -436,7 +436,7 @@ -- | Reinterpret the bits in a 32-bit word as a single-precision floating point number sWord64AsSDouble :: SWord64 -> SDouble sWord64AsSDouble dVal - | Just d <- unliteral dVal = literal $ RC.wordToDouble d + | Just d <- unliteral dVal = literal $ CN.wordToDouble d | True = SBV (SVal KDouble (Right (cache y))) where y st = do xsw <- sbvToSW st dVal newExpr st KDouble (SBVApp (IEEEFP (FP_Reinterpret (kindOf dVal) KDouble)) [xsw]) 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 @@ -41,8 +41,6 @@ import Control.Applicative (ZipList(ZipList)) import Control.Monad (when, unless, mplus) -import Control.Monad.Trans (liftIO) -import Control.Monad.Reader (ask) import GHC.Generics (U1(..), M1(..), (:*:)(..), K1(..)) import qualified GHC.Generics as G @@ -362,7 +360,8 @@ newExpr st KUnbounded (SBVApp (KindCast KReal KUnbounded) [xsw]) -- | label: Label the result of an expression. This is essentially a no-op, but useful as it generates a comment in the generated C/SMT-Lib code. --- Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy. +-- Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy. Compare this to 'observe' +-- which is good for printing counter-examples. label :: SymWord a => String -> SBV a -> SBV a label m x | Just _ <- unliteral x = x @@ -373,8 +372,9 @@ -- | Observe the value of an expression. Such values are useful in model construction, as they are printed part of a satisfying model, or a -- counter-example. The same works for quick-check as well. Useful when we want to see intermediate values, or expected/obtained --- pairs in a particular run. -observe :: SymWord a => String -> SBV a -> Symbolic () +-- pairs in a particular run. Note that an observed expression is always symbolic, i.e., it won't be constant folded. Compare this to 'label' +-- which is used for putting a label in the generated SMTLib-C code. +observe :: SymWord a => String -> SBV a -> SBV a observe m x | null m = error "SBV.observe: Bad empty name!" @@ -383,9 +383,11 @@ | "s" `isPrefixOf` m && all isDigit (drop 1 m) = error $ "SBV.observe: Names of the form sXXX are internal to SBV, please use a different name: " ++ show m | True - = do st <- ask - liftIO $ do xsw <- sbvToSW st x - recordObservable st m xsw + = SBV $ SVal k $ Right $ cache r + where k = kindOf x + r st = do xsw <- sbvToSW st x + recordObservable st m xsw + return xsw -- | Symbolic Equality. Note that we can't use Haskell's 'Eq' class since Haskell insists on returning Bool -- Comparing symbolic values will necessarily return a symbolic value. @@ -944,6 +946,8 @@ -- NB. In the optimizations below, use of -1 is valid as -- -1 has all bits set to True for both signed and unsigned values +-- | Using 'popCount' or 'testBit' on non-concrete values will result in an +-- error. Use 'sPopCount' or 'sTestBit' instead. instance (Num a, Bits a, SymWord a) => Bits (SBV a) where SBV x .&. SBV y = SBV (svAnd x y) SBV x .|. SBV y = SBV (svOr x y) 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 @@ -799,6 +799,8 @@ -- We really don't want an 'Eq' instance for 'SBV' or 'SVal'. As it really makes no sense. -- But since we do want the 'Bits' instance, we're forced to define equality. See -- . We simply error out. +-- | This instance is only defined so that we can define an instance for +-- 'Data.Bits.Bits'. '==' and '/=' simply throw an error. instance Eq SVal where a == b = error $ "Comparing symbolic bit-vectors; Use (.==) instead. Received: " ++ show (a, b) a /= b = error $ "Comparing symbolic bit-vectors; Use (./=) instead. Received: " ++ show (a, b) diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -33,6 +33,7 @@ import Data.SBV.Core.Data hiding (StrOp(..)) import Data.SBV.Core.Model +import Data.SBV.Utils.Boolean ((==>)) import Data.List (genericLength, genericIndex, genericDrop, genericTake) import qualified Data.List as L (tails, isSuffixOf, isPrefixOf, isInfixOf) @@ -41,7 +42,7 @@ -- -- $setup -- >>> import Data.SBV.Provers.Prover (prove, sat) --- >>> import Data.SBV.Utils.Boolean ((==>), (&&&), bnot, (<=>)) +-- >>> import Data.SBV.Utils.Boolean ((&&&), bnot, (<=>)) -- >>> import Data.Int -- >>> import Data.Word -- >>> :set -XOverloadedLists @@ -125,7 +126,7 @@ -- Q.E.D. -- >>> sat $ \(l :: SList Word16) -> length l .>= 2 &&& listToListAt l 0 ./= listToListAt l (length l - 1) -- Satisfiable. Model: --- s0 = [0,0,4096] :: [SWord16] +-- s0 = [0,0,32] :: [SWord16] listToListAt :: SymWord a => SList a -> SInteger -> SList a listToListAt s offset = subList s offset 1 @@ -151,7 +152,7 @@ y si st = do e <- internalVariable st kElem es <- newExpr st kSeq (SBVApp (SeqOp SeqUnit) [e]) let esSBV = SBV (SVal kSeq (Right (cache (\_ -> return es)))) - internalConstraint st False [] $ unSBV $ esSBV .== si + internalConstraint st False [] $ unSBV $ length l .> i ==> esSBV .== si return e -- | Short cut for 'elemAt' @@ -306,8 +307,8 @@ -- Q.E.D. -- >>> prove $ \(l :: SList Word16) i -> i .> 0 &&& i .< length l ==> indexOf l (subList l i 1) .== i -- Falsifiable. Counter-example: --- s0 = [0,0,0,0,0] :: [SWord16] --- s1 = 4 :: Integer +-- s0 = [32,0,0] :: [SWord16] +-- s1 = 2 :: Integer -- >>> prove $ \(l1 :: SList Word16) l2 -> length l2 .> length l1 ==> indexOf l1 l2 .== -1 -- Q.E.D. indexOf :: SymWord a => SList a -> SList a -> SInteger diff --git a/Data/SBV/List/Bounded.hs b/Data/SBV/List/Bounded.hs --- a/Data/SBV/List/Bounded.hs +++ b/Data/SBV/List/Bounded.hs @@ -14,20 +14,24 @@ -- bounded prefix of this list, at which point these functions come in handy. ----------------------------------------------------------------------------- -- -{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} module Data.SBV.List.Bounded ( -- * General folds - bfoldr, bfoldl + bfoldr, bfoldrM, bfoldl, bfoldlM -- * Map, filter, zipWith, elem - , bmap, bfilter, bzipWith, belem + , bmap, bmapM, bfilter, bzipWith, belem -- * Aggregates , bsum, bprod, band, bor, bany, ball, bmaximum, bminimum + -- * Miscellaneous: Reverse and sort + , breverse, bsort ) where import Data.SBV -import Data.SBV.List ((.:)) +import Data.SBV.List ((.:), (.++)) import qualified Data.SBV.List as L -- | Case analysis on a symbolic list. (Not exported.) @@ -40,12 +44,28 @@ where go 0 _ = b go i s = lcase s b (\h t -> h `f` go (i-1) t) +-- | Bounded monadic fold from the right. +bfoldrM :: forall a b m. (SymWord a, SymWord b, Monad m, Mergeable (m (SBV b))) + => Int -> (SBV a -> SBV b -> m (SBV b)) -> SBV b -> SList a -> m (SBV b) +bfoldrM cnt f b = go (cnt `max` 0) + where go :: Int -> SList a -> m (SBV b) + go 0 _ = return b + go i s = lcase s (return b) (\h t -> f h =<< go (i-1) t) + -- | Bounded fold from the left. bfoldl :: (SymWord a, SymWord b) => Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b bfoldl cnt f = go (cnt `max` 0) where go 0 b _ = b go i b s = lcase s b (\h t -> go (i-1) (b `f` h) t) +-- | Bounded monadic fold from the left. +bfoldlM :: forall a b m. (SymWord a, SymWord b, Monad m, Mergeable (m (SBV b))) + => Int -> (SBV b -> SBV a -> m (SBV b)) -> SBV b -> SList a -> m (SBV b) +bfoldlM cnt f = go (cnt `max` 0) + where go :: Int -> SBV b -> SList a -> m (SBV b) + go 0 b _ = return b + go i b s = lcase s (return b) (\h t -> do { fbh <- f b h; go (i-1) fbh t }) + -- | Bounded sum. bsum :: (SymWord a, Num a) => Int -> SList a -> SBV a bsum i = bfoldl i (+) 0 @@ -58,6 +78,11 @@ bmap :: (SymWord a, SymWord b) => Int -> (SBV a -> SBV b) -> SList a -> SList b bmap i f = bfoldr i (\x -> (f x .:)) [] +-- | Bounded monadic map. +bmapM :: (SymWord a, SymWord b, Monad m, Mergeable (m (SBV [b]))) + => Int -> (SBV a -> m (SBV b)) -> SList a -> m (SList b) +bmapM i f = bfoldrM i (\a bs -> (.:) <$> f a <*> pure bs) [] + -- | Bounded filter. bfilter :: SymWord a => Int -> (SBV a -> SBool) -> SList a -> SList a bfilter i f = bfoldr i (\x y -> ite (f x) (x .: y) y) [] @@ -79,11 +104,11 @@ ball i f = band i . bmap i f -- | Bounded maximum. Undefined if list is empty. -bmaximum :: (SymWord a, Num a) => Int -> SList a -> SBV a +bmaximum :: SymWord a => Int -> SList a -> SBV a bmaximum i l = bfoldl (i-1) smax (L.head l) (L.tail l) -- | Bounded minimum. Undefined if list is empty. -bminimum :: (SymWord a, Num a) => Int -> SList a -> SBV a +bminimum :: SymWord a => Int -> SList a -> SBV a bminimum i l = bfoldl (i-1) smin (L.head l) (L.tail l) -- | Bounded zipWith @@ -97,3 +122,24 @@ -- | Bounded element check belem :: SymWord a => Int -> SBV a -> SList a -> SBool belem i e = bany i (e .==) + +-- | Bounded reverse +breverse :: SymWord a => Int -> SList a -> SList a +breverse cnt = bfoldr cnt (\a b -> b .++ L.singleton a) [] + +-- | Bounded paramorphism (not exported). +bpara :: (SymWord a, SymWord b) => Int -> (SBV a -> SBV [a] -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b +bpara cnt f b = go (cnt `max` 0) + where go 0 _ = b + go i s = lcase s b (\h t -> f h t (go (i-1) t)) + +-- | Insert an element into a sorted list (not exported). +binsert :: SymWord a => Int -> SBV a -> SList a -> SList a +binsert cnt a = bpara cnt f (L.singleton a) + where f sortedHd sortedTl sortedTl' = ite (a .< sortedHd) + (a .: sortedHd .: sortedTl) + (sortedHd .: sortedTl') + +-- | Bounded insertion sort +bsort :: SymWord a => Int -> SList a -> SList a +bsort cnt = bfoldr cnt (binsert cnt) [] diff --git a/Data/SBV/RegExp.hs b/Data/SBV/RegExp.hs --- a/Data/SBV/RegExp.hs +++ b/Data/SBV/RegExp.hs @@ -81,7 +81,7 @@ -- >>> let phone = pre * "-" * post -- >>> sat $ \s -> (s :: SString) `match` phone -- Satisfiable. Model: --- s0 = "222-2248" :: String +-- s0 = "224-4222" :: 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 @@ -14,7 +14,7 @@ module Data.SBV.SMT.SMTLib2(cvt, cvtInc) where import Data.Bits (bit) -import Data.List (intercalate, partition, unzip3) +import Data.List (intercalate, partition, unzip3, nub) import Data.Maybe (listToMaybe, fromMaybe) import qualified Data.Foldable as F (toList) @@ -678,7 +678,16 @@ | Just f <- lookup op uninterpretedTable = f (map ssw args) | True - = error $ "SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " ++ show inp + = if not (null args) && isUninterpreted (head args) + then error $ unlines [ "" + , "*** Cannot translate operator : " ++ show op + , "*** When applied to arguments of kind: " ++ intercalate ", " (nub (map (show . kindOf) args)) + , "*** Found as part of the expression : " ++ show inp + , "***" + , "*** Note that uninterpreted kinds only support equality." + , "*** If you believe this is in error, please report!" + ] + else error $ "SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " ++ show inp where smtOpBVTable = [ (Plus, lift2 "bvadd") , (Minus, lift2 "bvsub") , (Times, lift2 "bvmul") diff --git a/Data/SBV/String.hs b/Data/SBV/String.hs --- a/Data/SBV/String.hs +++ b/Data/SBV/String.hs @@ -36,6 +36,7 @@ import Data.SBV.Core.Data hiding (SeqOp(..)) import Data.SBV.Core.Model +import Data.SBV.Utils.Boolean ((==>)) import qualified Data.Char as C import Data.List (genericLength, genericIndex, genericDrop, genericTake) @@ -45,7 +46,7 @@ -- -- $setup -- >>> import Data.SBV.Provers.Prover (prove, sat) --- >>> import Data.SBV.Utils.Boolean ((==>), (&&&), bnot, (<=>)) +-- >>> import Data.SBV.Utils.Boolean ((&&&), bnot, (<=>)) -- >>> :set -XOverloadedStrings -- | Length of a string. @@ -124,7 +125,7 @@ -- Q.E.D. -- >>> sat $ \s -> length s .>= 2 &&& strToStrAt s 0 ./= strToStrAt s (length s - 1) -- Satisfiable. Model: --- s0 = "\NUL\NUL\EOT" :: String +-- s0 = "\NUL\NUL\128" :: String strToStrAt :: SString -> SInteger -> SString strToStrAt s offset = subStr s offset 1 @@ -149,7 +150,7 @@ y si st = do c <- internalVariable st w8 cs <- newExpr st KString (SBVApp (StrOp StrUnit) [c]) let csSBV = SBV (SVal KString (Right (cache (\_ -> return cs)))) - internalConstraint st False [] $ unSBV $ csSBV .== si + internalConstraint st False [] $ unSBV $ length s .> i ==> csSBV .== si return c -- | Short cut for 'strToCharAt' @@ -304,8 +305,8 @@ -- Q.E.D. -- >>> prove $ \s i -> i .> 0 &&& i .< length s ==> indexOf s (subStr s i 1) .== i -- Falsifiable. Counter-example: --- s0 = "\NUL\NUL\NUL\NUL\NUL" :: String --- s1 = 3 :: Integer +-- s0 = " \NUL\NUL\NUL\NUL\NUL" :: String +-- s1 = 3 :: Integer -- >>> prove $ \s1 s2 -> length s2 .> length s1 ==> indexOf s1 s2 .== -1 -- Q.E.D. indexOf :: SString -> SString -> SInteger diff --git a/Data/SBV/Tools/BoundedFix.hs b/Data/SBV/Tools/BoundedFix.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Tools/BoundedFix.hs @@ -0,0 +1,74 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Tools.BoundedFix +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Bounded fixed-point unrolling. +----------------------------------------------------------------------------- + +{-# LANGUAGE FlexibleContexts #-} + +module Data.SBV.Tools.BoundedFix ( + bfix + ) where + +import Data.SBV + +-- Doctest only: +-- $setup +-- >>> bfac = bfix 10 "fac" fact where fact f n = ite (n .== 0) 1 ((n :: SInteger) * f (n-1)) + +-- | Bounded fixed-point operation. The call @bfix bnd nm f@ unrolls the recursion in @f@ at most +-- @bnd@ times, and uninterprets the function (with the name @nm@) after the bound is reached. +-- +-- This combinator is handy for dealing with recursive definitions that are not symbolically terminating +-- and when the property we are interested in does not require an infinite unrolling, or when we are happy +-- with a bounded proof. In particular, this operator can be used as a basis of software-bounded model +-- checking algorithms built on top of SBV. The bound can be successively refined in a CEGAR like loop +-- as necessary, by analyzing the counter-examples and rejecting them if they are false-negatives. +-- +-- For instance, we can define the factorial function using the bounded fixed-point operator like this: +-- +-- @ +-- bfac :: SInteger -> SInteger +-- bfac = bfix 10 "fac" fact +-- where fact f n = ite (n .== 0) 1 (n * f (n-1)) +-- @ +-- +-- This definition unrolls the recursion in factorial at most 10 times before uninterpreting the result. +-- We can now prove: +-- +-- >>> prove $ \n -> n .>= 1 &&& n .<= 9 ==> bfac n .== n * bfac (n-1) +-- Q.E.D. +-- +-- And we would get a bogus counter-example if the proof of our property needs a larger bound: +-- +-- >>> prove $ \n -> n .== 10 ==> bfac n .== 3628800 +-- Falsifiable. Counter-example: +-- s0 = 10 :: Integer +-- +-- By design, if a function defined via `bfix` is given a concrete argument, it will unroll +-- the recursion as much as necessary to complete the call (which can of course diverge). The bound +-- only applies if the given argument is symbolic. This fact can be used to observe concrete +-- values to see where the bounded-model-checking approach fails: +-- +-- >>> prove $ \n -> n .== 10 ==> observe "bfac_n" (bfac n) .== observe "bfac_10" (bfac 10) +-- Falsifiable. Counter-example: +-- s0 = 10 :: Integer +-- bfac_n = 7257600 :: Integer +-- bfac_10 = 3628800 :: Integer +-- +-- Here, we see that the SMT solver must have decided to assign the value @2@ in the final call just +-- as it was reaching the base case, and thus got the final result incorrect. (Note +-- that @7257600 = 2 * 3628800@.) A wrapper algorithm can then assert the actual value of +-- @bfac 10@ here as an extra constraint and can search for "deeper bugs." +bfix :: (SymWord a, Uninterpreted (SBV a -> r)) => Int -> String -> ((SBV a -> r) -> (SBV a -> r)) -> SBV a -> r +bfix bound nm f x + | isConcrete x = g x + | True = unroll bound x + where g = f g + unroll 0 = uninterpret nm + unroll i = f (unroll (i-1)) diff --git a/Data/SBV/Tools/Range.hs b/Data/SBV/Tools/Range.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Tools/Range.hs @@ -0,0 +1,173 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Tools.Range +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Single variable valid range detection. +----------------------------------------------------------------------------- + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Data.SBV.Tools.Range ( + + -- * Boundaries and ranges + Boundary(..), Range(..) + + -- * Computing valid ranges + , ranges, rangesWith + + ) where + +import Data.SBV +import Data.SBV.Control + +import Data.SBV.Internals hiding (Range) + +-- Doctest only +-- $setup +-- >>> :set -XScopedTypeVariables + +-- | A boundary value +data Boundary a = Unbounded -- ^ Unbounded + | Open a -- ^ Exclusive of the point + | Closed a -- ^ Inclusive of the point + +-- | Is this a closed value? +isClosed :: Boundary a -> Bool +isClosed Unbounded = False +isClosed (Open _) = False +isClosed (Closed _) = True + +-- | A range is a pair of boundaries: Lower and upper bounds +data Range a = Range (Boundary a) (Boundary a) + +-- | Show instance for 'Range' +instance Show a => Show (Range a) where + show (Range l u) = sh True l ++ "," ++ sh False u + where sh onLeft b = case b of + Unbounded | onLeft -> "(-oo" + | True -> "oo)" + Open v | onLeft -> "(" ++ show v + | True -> show v ++ ")" + Closed v | onLeft -> "[" ++ show v + | True -> show v ++ "]" + +-- | Given a single predicate over a single variable, find the contiguous ranges over which the predicate +-- is satisfied. SBV will make one call to the optimizer, and then as many calls to the solver as there are +-- disjoint ranges that the predicate is satisfied over. (Linear in the number of ranges.) Note that the +-- number of ranges is large, this can take a long time! Some examples: +-- +-- >>> ranges (\(_ :: SInteger) -> false) +-- [] +-- >>> ranges (\(_ :: SInteger) -> true) +-- [(-oo,oo)] +-- >>> ranges (\(x :: SInteger) -> bAnd [x .<= 120, x .>= -12, x ./= 3]) +-- [[-12,3),(3,120]] +-- >>> ranges (\(x :: SInteger) -> bAnd [x .<= 75, x .>= 5, x ./= 6, x ./= 67]) +-- [[5,6),(6,67),(67,75]] +-- >>> ranges (\(x :: SInteger) -> bAnd [x .<= 75, x ./= 3, x ./= 67]) +-- [(-oo,3),(3,67),(67,75]] +-- >>> ranges (\(x :: SReal) -> bAnd [x .> 3.2, x .< 12.7]) +-- [(3.2,12.7)] +-- >>> ranges (\(x :: SReal) -> bAnd [x .> 3.2, x .<= 12.7]) +-- [(3.2,12.7]] +-- >>> ranges (\(x :: SReal) -> bAnd [x .<= 12.7, x ./= 8]) +-- [(-oo,8.0),(8.0,12.7]] +-- >>> ranges (\(x :: SReal) -> bAnd [x .>= 12.7, x ./= 15]) +-- [[12.7,15.0),(15.0,oo)] +-- >>> ranges (\(x :: SInt8) -> bAnd [x .<= 7, x ./= 6]) +-- [[-128,6),(6,7]] +-- >>> ranges $ \x -> x .> (0::SReal) +-- [(0.0,oo)] +-- >>> ranges $ \x -> x .< (0::SReal) +-- [(-oo,0.0)] +ranges :: forall a. (Num a, SymWord a, SMTValue a, SatModel a, Metric (SBV a)) => (SBV a -> SBool) -> IO [Range a] +ranges = rangesWith defaultSMTCfg + +-- | Compute ranges, using the given solver configuration. +rangesWith :: forall a. (Num a, SymWord a, SMTValue a, SatModel a, Metric (SBV a)) => SMTConfig -> (SBV a -> SBool) -> IO [Range a] +rangesWith cfg prop = do mbBounds <- getInitialBounds + case mbBounds of + Nothing -> return [] + Just r -> search [r] [] + + where getInitialBounds :: IO (Maybe (Range a)) + getInitialBounds = do + let getGenVal :: GeneralizedCW -> Boundary a + getGenVal (RegularCW cw) = Closed $ getRegVal cw + getGenVal (ExtendedCW ecw) = getExtVal ecw + + getExtVal :: ExtCW -> Boundary a + getExtVal (Infinite _) = Unbounded + getExtVal (Epsilon k) = Open $ getRegVal (mkConstCW k (0::Integer)) + getExtVal i@Interval{} = error $ unlines [ "*** Data.SBV.ranges.getExtVal: Unexpected interval bounds!" + , "***" + , "*** Found bound: " ++ show i + , "*** Please report this as a bug!" + ] + getExtVal (BoundedCW cw) = Closed $ getRegVal cw + getExtVal (AddExtCW a b) = getExtVal a `addBound` getExtVal b + getExtVal (MulExtCW a b) = getExtVal a `mulBound` getExtVal b + + opBound :: (a -> a -> a) -> Boundary a -> Boundary a -> Boundary a + opBound f x y = case (fromBound x, fromBound y, isClosed x && isClosed y) of + (Just a, Just b, True) -> Closed $ a `f` b + (Just a, Just b, False) -> Open $ a `f` b + _ -> Unbounded + where fromBound Unbounded = Nothing + fromBound (Open a) = Just a + fromBound (Closed a) = Just a + + addBound, mulBound :: Boundary a -> Boundary a -> Boundary a + addBound = opBound (+) + mulBound = opBound (*) + + getRegVal :: CW -> a + getRegVal cw = case parseCWs [cw] of + Just (v, []) -> v + _ -> error $ "Data.SBV.interval.getRegVal: Cannot parse " ++ show cw + + IndependentResult m <- optimizeWith cfg Independent $ do x <- free_ + constrain $ prop x + minimize "min" x + maximize "max" x + case head (map snd m) of + Unsatisfiable{} -> return Nothing + Unknown{} -> error "Solver said Unknown!" + ProofError{} -> error (show (IndependentResult m)) + _ -> let Just (Just mi) = getModelObjectiveValue "min" `fmap` ("min" `lookup` m) + Just (Just ma) = getModelObjectiveValue "max" `fmap` ("max" `lookup` m) + in return $ Just $ Range (getGenVal mi) (getGenVal ma) + + + bisect :: Range a -> IO (Maybe [Range a]) + bisect (Range lo hi) = runSMTWith cfg $ do + x <- free_ + + let restrict v open closed = case v of + Unbounded -> true + Open a -> x `open` literal a + Closed a -> x `closed` literal a + + lower = restrict lo (.>) (.>=) + upper = restrict hi (.<) (.<=) + + constrain $ lower &&& upper &&& bnot (prop x) + + query $ do cs <- checkSat + case cs of + Unsat -> return Nothing + Unk -> error "Data.SBV.interval.bisect: Solver said unknown!" + Sat -> do midV <- Open <$> getValue x + return $ Just [Range lo midV, Range midV hi] + + search :: [Range a] -> [Range a] -> IO [Range a] + search [] sofar = return $ reverse sofar + search (c:cs) sofar = do mbCS <- bisect c + case mbCS of + Nothing -> search cs (c:sofar) + Just xss -> search (xss ++ cs) sofar diff --git a/Data/SBV/Utils/Lib.hs b/Data/SBV/Utils/Lib.hs --- a/Data/SBV/Utils/Lib.hs +++ b/Data/SBV/Utils/Lib.hs @@ -25,7 +25,7 @@ import Numeric (readHex, readOct, showHex) --- We have a nasty issue with the usual String/List confusion in Haskell. However, we can +-- | We have a nasty issue with the usual String/List confusion in Haskell. However, we can -- do a simple dynamic trick to determine where we are. The ice is thin here, but it seems to work. isKString :: forall a. Typeable a => a -> Bool isKString _ = isJust (fromDynamic (toDyn (undefined :: a)) :: Maybe String) diff --git a/Data/SBV/Utils/SExpr.hs b/Data/SBV/Utils/SExpr.hs --- a/Data/SBV/Utils/SExpr.hs +++ b/Data/SBV/Utils/SExpr.hs @@ -13,16 +13,17 @@ module Data.SBV.Utils.SExpr (SExpr(..), parenDeficit, parseSExpr) where -import Data.Bits (setBit, testBit) -import Data.Word (Word32, Word64) -import Data.Char (isDigit, ord, isSpace) -import Data.List (isPrefixOf) -import Data.Maybe (fromMaybe, listToMaybe) -import Numeric (readInt, readDec, readHex, fromRat) -import Data.ReinterpretCast (wordToFloat, wordToDouble) +import Data.Bits (setBit, testBit) +import Data.Word (Word32, Word64) +import Data.Char (isDigit, ord, isSpace) +import Data.List (isPrefixOf) +import Data.Maybe (fromMaybe, listToMaybe) +import Numeric (readInt, readDec, readHex, fromRat) import Data.SBV.Core.AlgReals import Data.SBV.Core.Data (nan, infinity, RoundingMode(..)) + +import Data.Numbers.CrackNum (wordToFloat, wordToDouble) -- | ADT S-Expression format, suitable for representing get-model output of SMT-Lib data SExpr = ECon String 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 @@ -20,13 +20,13 @@ -- -- >>> checkArithOverflow midPointBroken -- Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:33:28:+!: SInt32 addition overflows: Violated. Model: --- low = 2147483583 :: Int32 +-- low = 2147483647 :: Int32 -- high = 2147483647 :: Int32 -- -- Indeed: -- --- >>> (2147483583 + 2147483647) `div` (2::Int32) --- -33 +-- >>> (2147483647 + 2147483647) `div` (2::Int32) +-- -1 -- -- giving us a negative mid-point value! midPointBroken :: SInt32 -> SInt32 -> SInt32 diff --git a/Documentation/SBV/Examples/Lists/BoundedMutex.hs b/Documentation/SBV/Examples/Lists/BoundedMutex.hs --- a/Documentation/SBV/Examples/Lists/BoundedMutex.hs +++ b/Documentation/SBV/Examples/Lists/BoundedMutex.hs @@ -131,14 +131,14 @@ -- trying to show a bounded trace of length 10, such that the second process is ready but -- never transitions to critical. We have: -- --- >>> notFair 10 --- Fairness is violated at bound: 10 --- P1: [Idle,Idle,Ready,Critical,Idle,Idle,Ready,Critical,Idle,Idle] --- P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready] --- Ts: [1,2,1,1,1,1,1,1,1,1] +-- > ghci> notFair 10 +-- > Fairness is violated at bound: 10 +-- > P1: [Idle,Idle,Ready,Critical,Idle,Idle,Ready,Critical,Idle,Idle] +-- > P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready] +-- > Ts: [1,2,1,1,1,1,1,1,1,1] -- -- As expected, P2 gets ready but never goes critical since the arbiter keeps picking --- P1 unfairly. +-- P1 unfairly. (You might get a different trace depending on what z3 happens to produce!) -- -- Exercise for the reader: Change the 'validTurns' function so that it alternates the turns -- from the previous value if neither process is in critical. Show that this makes the 'notFair' 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 @@ -56,19 +56,19 @@ -- -- >>> assocPlusRegular -- Falsifiable. Counter-example: --- x = -1.844675e19 :: Float --- y = 8.7960925e12 :: Float --- z = -2.4178333e24 :: Float +-- x = 3.7634227e-37 :: Float +-- y = -3.7612938e-37 :: Float +-- z = -1.1036833e-38 :: Float -- -- Indeed, we have: -- --- >>> let x = -1.844675e19 :: Float --- >>> let y = 8.7960925e12 :: Float --- >>> let z = -2.4178333e24 :: Float +-- >>> let x = 3.7634227e-37 :: Float +-- >>> let y = -3.7612938e-37 :: Float +-- >>> let z = -1.1036833e-38 :: Float -- >>> x + (y + z) --- -2.417852e24 +-- -1.0823943e-38 -- >>> (x + y) + z --- -2.4178516e24 +-- -1.0823947e-38 -- -- Note the difference between two additions! assocPlusRegular :: IO ThmResult @@ -90,17 +90,17 @@ -- -- >>> nonZeroAddition -- Falsifiable. Counter-example: --- a = -2.524355e-29 :: Float --- b = 9.403955e-38 :: Float +-- a = -4.611686e18 :: Float +-- b = 1.3552526e-20 :: Float -- -- Indeed, we have: -- --- >>> (-2.524355e-29 + 9.403955e-38) == (-2.524355e-29 :: Float) +-- >>> (-4.611686e18 + 1.3552526e-20) == (-4.611686e18 :: Float) -- True -- -- But: -- --- >>> 9.403955e-38 == (0 :: Float) +-- >>> 1.3552526e-20 == (0 :: Float) -- False -- nonZeroAddition :: IO ThmResult @@ -121,13 +121,13 @@ -- -- >>> multInverse -- Falsifiable. Counter-example: --- a = -1.1299203187734916e-308 :: Double +-- a = 8.988465676670122e307 :: Double -- -- Indeed, we have: -- --- >>> let a = -1.1299203187734916e-308 :: Double +-- >>> let a = 8.988465676670122e307 :: Double -- >>> a * (1/a) --- 0.9999999999999999 +-- 1.0000000000000002 multInverse :: IO ThmResult multInverse = prove $ do a <- sDouble "a" constrain $ fpIsPoint a @@ -148,29 +148,29 @@ -- >>> roundingAdd -- Satisfiable. Model: -- rm = RoundTowardPositive :: RoundingMode --- x = 1.0 :: Float --- y = -6.1035094e-5 :: Float +-- x = 255.96877 :: Float +-- y = 255.875 :: Float -- -- (Note that depending on your version of Z3, you might get a different result.) -- Unfortunately we can't directly validate this result at the Haskell level, as Haskell only supports -- 'RoundNearestTiesToEven'. We have: -- --- >>> 1.0 + (-6.1035094e-5) :: Float --- 0.99993896 +-- >>> 255.96877 + 255.875 :: Float +-- 511.84375 -- -- While we cannot directly see the result when the mode is 'RoundTowardPositive' in Haskell, we can use -- SBV to provide us with that result thusly: -- --- >>> sat $ \z -> z .== fpAdd sRoundTowardPositive 1.0 (-6.1035094e-5 :: SFloat) +-- >>> sat $ \z -> z .== fpAdd sRoundTowardPositive 255.96877 (255.875 :: SFloat) -- Satisfiable. Model: --- s0 = 0.999939 :: Float +-- s0 = 511.84378 :: Float -- -- We can see why these two resuls are indeed different: The 'RoundTowardPositive' -- (which rounds towards positive-infinity) produces a larger result. Indeed, if we treat these numbers -- as 'Double' values, we get: -- --- >>> 1.0 + (-6.1035094e-5) :: Double --- 0.999938964906 +-- >>> 255.96877 + 255.875 :: Double +-- 511.84377 -- -- we see that the "more precise" result is larger than what the 'Float' value is, justifying the -- larger value with 'RoundTowardPositive'. A more detailed study is beyond our current scope, so we'll diff --git a/Documentation/SBV/Examples/Puzzles/Garden.hs b/Documentation/SBV/Examples/Puzzles/Garden.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/Puzzles/Garden.hs @@ -0,0 +1,110 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.Puzzles.Garden +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- The origin of this puzzle is Raymond Smullyan's "The Flower Garden" riddle: +-- +-- In a certain flower garden, each flower was either red, yellow, +-- or blue, and all three colors were represented. A statistician +-- once visited the garden and made the observation that whatever +-- three flowers you picked, at least one of them was bound to be red. +-- A second statistician visited the garden and made the observation +-- that whatever three flowers you picked, at least one was bound to +-- be yellow. +-- +-- Two logic students heard about this and got into an argument. +-- The first student said: “It therefore follows that whatever +-- three flowers you pick, at least one is bound to be blue, doesn’t +-- it?” The second student said: “Of course not!” +-- +-- Which student was right, and why? +-- +-- We slightly modify the puzzle. Assuming the first student is right, we use +-- SBV to show that the garden must contain exactly 3 flowers. In any other +-- case, the second student would be right. +------------------------------------------------------------------------------ + +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveAnyClass #-} + +module Documentation.SBV.Examples.Puzzles.Garden where + +import Data.SBV +import Data.List(isSuffixOf) + +-- | Colors of the flowers +data Color = Red | Yellow | Blue + +-- | Make 'Color' a symbolic value. +mkSymbolicEnumeration ''Color + +-- | Represent flowers by symbolic integers +type Flower = SInteger + +-- | The uninterpreted function 'col' assigns a color to each flower. +col :: Flower -> SBV Color +col = uninterpret "col" + +-- | Describe a valid pick of three flowers @i@, @j@, @k@, assuming +-- we have @n@ flowers to start with. Essentially the numbers should +-- be within bounds and distinct. +validPick :: SInteger -> Flower -> Flower -> Flower -> SBool +validPick n i j k = distinct [i, j, k] &&& bAll ok [i, j, k] + where ok x = inRange x (1, n) + +-- | Count the number of flowers that occur in a given set of flowers. +count :: Color -> [Flower] -> SInteger +count c fs = sum [ite (col f .== literal c) 1 0 | f <- fs] + +-- | Smullyan's puzzle. +puzzle :: Goal +puzzle = do n <- sInteger "N" + + let valid = validPick n + + -- Declare three existential flowers. We name these with + -- the suffix "_modelIgnore" as we don't consider variations + -- on them to be interesting for model construction purposes. + -- We'll use the 'isNonModelVar' parameter to ignore them + -- for that purpose. + ef1 <- exists "ef1_modelIgnore" + ef2 <- exists "ef2_modelIgnore" + ef3 <- exists "ef3_modelIgnore" + + -- Declare three universal flowers to aid in encoding the + -- statements made by students. + af1 <- forall "af1" + af2 <- forall "af2" + af3 <- forall "af3" + + -- Each color is represented: + constrain $ valid ef1 ef2 ef3 + constrain $ map col [ef1, ef2, ef3] .== map literal [Red, Yellow, Blue] + + -- Pick any three, at least one is Red + constrain $ valid af1 af2 af3 ==> count Red [af1, af2, af3] .>= 1 + + -- Pick any three, at least one is Yellow + constrain $ valid af1 af2 af3 ==> count Yellow [af1, af2, af3] .>= 1 + + -- Pick any three, at least one is Blue + constrain $ valid af1 af2 af3 ==> count Blue [af1, af2, af3] .>= 1 + +-- | Solve the puzzle. We have: +-- +-- >>> flowerCount +-- Solution #1: +-- N = 3 :: Integer +-- This is the only solution. (Unique up to prefix existentials.) +-- +-- So, a garden with 3 flowers is the only solution. (Note that we simply skip +-- over the prefix existentials for model purposes here, as they don't represent +-- a different solution.) +flowerCount :: IO () +flowerCount = print =<< allSatWith z3{isNonModelVar = ("_modelIgnore" `isSuffixOf`)} puzzle diff --git a/Documentation/SBV/Examples/Puzzles/LadyAndTigers.hs b/Documentation/SBV/Examples/Puzzles/LadyAndTigers.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/Puzzles/LadyAndTigers.hs @@ -0,0 +1,63 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.Puzzles.LadyAndTigers +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Puzzle: +-- +-- You are standing in front of three rooms and must choose one. In one room is a Lady +-- (whom you could and wish to marry), in the other two rooms are tigers (that if you +-- choose either of these rooms, the tiger invites you to breakfast – the problem is +-- that you are the main course). Your job is to choose the room with the Lady. +-- The signs on the doors are: +-- +-- * A Tiger is in this room +-- * A Lady is in this room +-- * A Tiger is in room two +-- +-- At most only 1 statement is true. Where’s the Lady? +----------------------------------------------------------------------------- + +module Documentation.SBV.Examples.Puzzles.LadyAndTigers where + +import Data.SBV + +-- | Prints the only solution: +-- +-- >>> ladyAndTigers +-- Solution #1: +-- sign1 = False :: Bool +-- sign2 = False :: Bool +-- sign3 = True :: Bool +-- tiger1 = False :: Bool +-- tiger2 = True :: Bool +-- tiger3 = True :: Bool +-- This is the only solution. +-- +-- That is, the lady is in room 1, and only the third room's sign is true. +ladyAndTigers :: IO AllSatResult +ladyAndTigers = allSat $ do + + -- One boolean for each of the correctness of the signs + [sign1, sign2, sign3] <- mapM sBool ["sign1", "sign2", "sign3"] + + -- One boolean for each of the presence of the tigers + [tiger1, tiger2, tiger3] <- mapM sBool ["tiger1", "tiger2", "tiger3"] + + -- Room 1 sign: A Tiger is in this room + constrain $ sign1 <=> tiger1 + + -- Room 2 sign: A Lady is in this room + constrain $ sign2 <=> bnot tiger2 + + -- Room 3 sign: A Tiger is in room 2 + constrain $ sign3 <=> tiger2 + + -- At most one sign is true + constrain $ [sign1, sign2, sign3] `pbAtMost` 1 + + -- There are precisely two tigers + constrain $ [tiger1, tiger2, tiger3] `pbExactly` 2 diff --git a/Documentation/SBV/Examples/Queries/CaseSplit.hs b/Documentation/SBV/Examples/Queries/CaseSplit.hs --- a/Documentation/SBV/Examples/Queries/CaseSplit.hs +++ b/Documentation/SBV/Examples/Queries/CaseSplit.hs @@ -19,6 +19,7 @@ -- of the number (such as NaN, negative-zero, etc. is most suitable.) -- -- We have: +-- -- >>> csDemo1 -- Case fpIsNegativeZero: Starting -- Case fpIsNegativeZero: Unsatisfiable @@ -56,6 +57,7 @@ -- | Demonstrates the "coverage" case. -- -- We have: +-- -- >>> csDemo2 -- Case negative: Starting -- Case negative: Unsatisfiable diff --git a/Documentation/SBV/Examples/Strings/SQLInjection.hs b/Documentation/SBV/Examples/Strings/SQLInjection.hs --- a/Documentation/SBV/Examples/Strings/SQLInjection.hs +++ b/Documentation/SBV/Examples/Strings/SQLInjection.hs @@ -103,24 +103,27 @@ -- Remember that our example program (in pseudo-code) is: -- -- @ --- query ("SELECT msg FROM msgs where topicid='" ++ my_topicid ++ "'") +-- query ("SELECT msg FROM msgs WHERE topicid='" ++ my_topicid ++ "'") -- @ -- --- We have: (NB. Turning this doctest off, since Z3 no longer can handle --- it, see: .) +-- We have: -- --- @ --- findInjection exampleProgram --- "h'; DROP TABLE 'users" --- @ +-- >>> findInjection exampleProgram +-- " f'; DROP TABLE 'users" -- -- Indeed, if we substitute the suggested string, we get the program: -- --- > query ("SELECT msg FROM msgs where topicid='h'; DROP TABLE 'users'") +-- > query ("SELECT msg FROM msgs WHERE topicid=' f'; DROP TABLE 'users'") -- --- which would query for topic @h@ and then delete the users table! +-- which would query for topic @' f'@ and then delete the users table! findInjection :: SQLExpr -> IO String findInjection expr = runSMT $ do + + -- This example generates different outputs on different platforms (Mac vs Linux). + -- So, we explicitly set the random-seed to get a consistent doctest output + -- Otherwise the following line isn't needed. + setOption $ OptionKeyword ":smt.random_seed" ["1"] + badTopic <- sString "badTopic" -- Create an initial environment that returns the symbolic diff --git a/SBVTestSuite/GoldFiles/allSat5.gold b/SBVTestSuite/GoldFiles/allSat5.gold --- a/SBVTestSuite/GoldFiles/allSat5.gold +++ b/SBVTestSuite/GoldFiles/allSat5.gold @@ -3,17 +3,17 @@ s1 = 1 :: Word8 Solution #2: s0 = 0 :: Word8 - s1 = 3 :: Word8 + s1 = 2 :: Word8 Solution #3: s0 = 0 :: Word8 - s1 = 2 :: Word8 + s1 = 3 :: Word8 Solution #4: s0 = 1 :: Word8 s1 = 2 :: Word8 Solution #5: - s0 = 2 :: Word8 + s0 = 1 :: Word8 s1 = 3 :: Word8 Solution #6: - s0 = 1 :: Word8 + s0 = 2 :: Word8 s1 = 3 :: Word8 Found 6 different solutions. diff --git a/SBVTestSuite/GoldFiles/concreteFoldl.gold b/SBVTestSuite/GoldFiles/concreteFoldl.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/concreteFoldl.gold @@ -0,0 +1,24 @@ +** 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_BV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (assert s_1) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/concreteFoldr.gold b/SBVTestSuite/GoldFiles/concreteFoldr.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/concreteFoldr.gold @@ -0,0 +1,24 @@ +** 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_BV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (assert s_1) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/concreteReverse.gold b/SBVTestSuite/GoldFiles/concreteReverse.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/concreteReverse.gold @@ -0,0 +1,24 @@ +** 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_BV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (assert s_1) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/concreteSort.gold b/SBVTestSuite/GoldFiles/concreteSort.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/concreteSort.gold @@ -0,0 +1,24 @@ +** 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_BV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (assert s_1) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldlABC1.gold b/SBVTestSuite/GoldFiles/foldlABC1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/foldlABC1.gold @@ -0,0 +1,57 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s3 () Int 0) +[GOOD] (define-fun s19 () Int 1) +[GOOD] (define-fun s12 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" +[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" +[GOOD] (declare-fun s14 () Int) ; tracks user variable "__internal_sbv_s14" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s4 () Bool (> s0 s3)) +[GOOD] (define-fun s5 () Bool (> s1 s3)) +[GOOD] (define-fun s6 () Bool (> s2 s3)) +[GOOD] (define-fun s7 () (Seq Int) (seq.unit s0)) +[GOOD] (define-fun s8 () (Seq Int) (seq.unit s1)) +[GOOD] (define-fun s9 () (Seq Int) (seq.unit s2)) +[GOOD] (define-fun s10 () (Seq Int) (seq.++ s8 s9)) +[GOOD] (define-fun s11 () (Seq Int) (seq.++ s7 s10)) +[GOOD] (define-fun s13 () Bool (= s11 s12)) +[GOOD] (define-fun s15 () (Seq Int) (seq.unit s14)) +[GOOD] (define-fun s16 () Int (seq.len s11)) +[GOOD] (define-fun s17 () Bool (> s16 s3)) +[GOOD] (define-fun s18 () Bool (not s17)) +[GOOD] (define-fun s20 () (Seq Int) (seq.extract s11 s3 s19)) +[GOOD] (define-fun s21 () Bool (= s15 s20)) +[GOOD] (define-fun s22 () Bool (or s18 s21)) +[GOOD] (define-fun s23 () Int (ite s13 s3 s14)) +[GOOD] (define-fun s24 () Int (+ s0 s1)) +[GOOD] (define-fun s25 () Int (+ s2 s24)) +[GOOD] (define-fun s26 () Bool (= s23 s25)) +[GOOD] (assert s4) +[GOOD] (assert s5) +[GOOD] (assert s6) +[GOOD] (assert s22) +[GOOD] (assert s26) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldlABC2.gold b/SBVTestSuite/GoldFiles/foldlABC2.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/foldlABC2.gold @@ -0,0 +1,71 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s3 () Int 0) +[GOOD] (define-fun s19 () Int 1) +[GOOD] (define-fun s12 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" +[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" +[GOOD] (declare-fun s14 () Int) ; tracks user variable "__internal_sbv_s14" +[GOOD] (declare-fun s26 () Int) ; tracks user variable "__internal_sbv_s26" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s4 () Bool (> s0 s3)) +[GOOD] (define-fun s5 () Bool (> s1 s3)) +[GOOD] (define-fun s6 () Bool (> s2 s3)) +[GOOD] (define-fun s7 () (Seq Int) (seq.unit s0)) +[GOOD] (define-fun s8 () (Seq Int) (seq.unit s1)) +[GOOD] (define-fun s9 () (Seq Int) (seq.unit s2)) +[GOOD] (define-fun s10 () (Seq Int) (seq.++ s8 s9)) +[GOOD] (define-fun s11 () (Seq Int) (seq.++ s7 s10)) +[GOOD] (define-fun s13 () Bool (= s11 s12)) +[GOOD] (define-fun s15 () (Seq Int) (seq.unit s14)) +[GOOD] (define-fun s16 () Int (seq.len s11)) +[GOOD] (define-fun s17 () Bool (> s16 s3)) +[GOOD] (define-fun s18 () Bool (not s17)) +[GOOD] (define-fun s20 () (Seq Int) (seq.extract s11 s3 s19)) +[GOOD] (define-fun s21 () Bool (= s15 s20)) +[GOOD] (define-fun s22 () Bool (or s18 s21)) +[GOOD] (define-fun s23 () Int (- s16 s19)) +[GOOD] (define-fun s24 () (Seq Int) (seq.extract s11 s19 s23)) +[GOOD] (define-fun s25 () Bool (= s12 s24)) +[GOOD] (define-fun s27 () (Seq Int) (seq.unit s26)) +[GOOD] (define-fun s28 () Int (seq.len s24)) +[GOOD] (define-fun s29 () Bool (> s28 s3)) +[GOOD] (define-fun s30 () Bool (not s29)) +[GOOD] (define-fun s31 () (Seq Int) (seq.extract s24 s3 s19)) +[GOOD] (define-fun s32 () Bool (= s27 s31)) +[GOOD] (define-fun s33 () Bool (or s30 s32)) +[GOOD] (define-fun s34 () Int (ite s25 s3 s26)) +[GOOD] (define-fun s35 () Int (+ s14 s34)) +[GOOD] (define-fun s36 () Int (ite s13 s3 s35)) +[GOOD] (define-fun s37 () Int (+ s0 s1)) +[GOOD] (define-fun s38 () Int (+ s2 s37)) +[GOOD] (define-fun s39 () Bool (= s36 s38)) +[GOOD] (assert s4) +[GOOD] (assert s5) +[GOOD] (assert s6) +[GOOD] (assert s22) +[GOOD] (assert s33) +[GOOD] (assert s39) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldlABC3.gold b/SBVTestSuite/GoldFiles/foldlABC3.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/foldlABC3.gold @@ -0,0 +1,85 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s3 () Int 0) +[GOOD] (define-fun s19 () Int 1) +[GOOD] (define-fun s12 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" +[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" +[GOOD] (declare-fun s14 () Int) ; tracks user variable "__internal_sbv_s14" +[GOOD] (declare-fun s26 () Int) ; tracks user variable "__internal_sbv_s26" +[GOOD] (declare-fun s37 () Int) ; tracks user variable "__internal_sbv_s37" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s4 () Bool (> s0 s3)) +[GOOD] (define-fun s5 () Bool (> s1 s3)) +[GOOD] (define-fun s6 () Bool (> s2 s3)) +[GOOD] (define-fun s7 () (Seq Int) (seq.unit s0)) +[GOOD] (define-fun s8 () (Seq Int) (seq.unit s1)) +[GOOD] (define-fun s9 () (Seq Int) (seq.unit s2)) +[GOOD] (define-fun s10 () (Seq Int) (seq.++ s8 s9)) +[GOOD] (define-fun s11 () (Seq Int) (seq.++ s7 s10)) +[GOOD] (define-fun s13 () Bool (= s11 s12)) +[GOOD] (define-fun s15 () (Seq Int) (seq.unit s14)) +[GOOD] (define-fun s16 () Int (seq.len s11)) +[GOOD] (define-fun s17 () Bool (> s16 s3)) +[GOOD] (define-fun s18 () Bool (not s17)) +[GOOD] (define-fun s20 () (Seq Int) (seq.extract s11 s3 s19)) +[GOOD] (define-fun s21 () Bool (= s15 s20)) +[GOOD] (define-fun s22 () Bool (or s18 s21)) +[GOOD] (define-fun s23 () Int (- s16 s19)) +[GOOD] (define-fun s24 () (Seq Int) (seq.extract s11 s19 s23)) +[GOOD] (define-fun s25 () Bool (= s12 s24)) +[GOOD] (define-fun s27 () (Seq Int) (seq.unit s26)) +[GOOD] (define-fun s28 () Int (seq.len s24)) +[GOOD] (define-fun s29 () Bool (> s28 s3)) +[GOOD] (define-fun s30 () Bool (not s29)) +[GOOD] (define-fun s31 () (Seq Int) (seq.extract s24 s3 s19)) +[GOOD] (define-fun s32 () Bool (= s27 s31)) +[GOOD] (define-fun s33 () Bool (or s30 s32)) +[GOOD] (define-fun s34 () Int (- s28 s19)) +[GOOD] (define-fun s35 () (Seq Int) (seq.extract s24 s19 s34)) +[GOOD] (define-fun s36 () Bool (= s12 s35)) +[GOOD] (define-fun s38 () (Seq Int) (seq.unit s37)) +[GOOD] (define-fun s39 () Int (seq.len s35)) +[GOOD] (define-fun s40 () Bool (> s39 s3)) +[GOOD] (define-fun s41 () Bool (not s40)) +[GOOD] (define-fun s42 () (Seq Int) (seq.extract s35 s3 s19)) +[GOOD] (define-fun s43 () Bool (= s38 s42)) +[GOOD] (define-fun s44 () Bool (or s41 s43)) +[GOOD] (define-fun s45 () Int (ite s36 s3 s37)) +[GOOD] (define-fun s46 () Int (+ s26 s45)) +[GOOD] (define-fun s47 () Int (ite s25 s3 s46)) +[GOOD] (define-fun s48 () Int (+ s14 s47)) +[GOOD] (define-fun s49 () Int (ite s13 s3 s48)) +[GOOD] (define-fun s50 () Int (+ s0 s1)) +[GOOD] (define-fun s51 () Int (+ s2 s50)) +[GOOD] (define-fun s52 () Bool (= s49 s51)) +[GOOD] (assert s4) +[GOOD] (assert s5) +[GOOD] (assert s6) +[GOOD] (assert s22) +[GOOD] (assert s33) +[GOOD] (assert s44) +[GOOD] (assert s52) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldrAB1.gold b/SBVTestSuite/GoldFiles/foldrAB1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/foldrAB1.gold @@ -0,0 +1,51 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s2 () Int 0) +[GOOD] (define-fun s15 () Int 1) +[GOOD] (define-fun s8 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" +[GOOD] (declare-fun s10 () Int) ; tracks user variable "__internal_sbv_s10" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s3 () Bool (> s0 s2)) +[GOOD] (define-fun s4 () Bool (> s1 s2)) +[GOOD] (define-fun s5 () (Seq Int) (seq.unit s0)) +[GOOD] (define-fun s6 () (Seq Int) (seq.unit s1)) +[GOOD] (define-fun s7 () (Seq Int) (seq.++ s5 s6)) +[GOOD] (define-fun s9 () Bool (= s7 s8)) +[GOOD] (define-fun s11 () (Seq Int) (seq.unit s10)) +[GOOD] (define-fun s12 () Int (seq.len s7)) +[GOOD] (define-fun s13 () Bool (> s12 s2)) +[GOOD] (define-fun s14 () Bool (not s13)) +[GOOD] (define-fun s16 () (Seq Int) (seq.extract s7 s2 s15)) +[GOOD] (define-fun s17 () Bool (= s11 s16)) +[GOOD] (define-fun s18 () Bool (or s14 s17)) +[GOOD] (define-fun s19 () Int (ite s9 s2 s10)) +[GOOD] (define-fun s20 () Int (+ s0 s1)) +[GOOD] (define-fun s21 () Bool (= s19 s20)) +[GOOD] (assert s3) +[GOOD] (assert s4) +[GOOD] (assert s18) +[GOOD] (assert s21) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldrAB2.gold b/SBVTestSuite/GoldFiles/foldrAB2.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/foldrAB2.gold @@ -0,0 +1,65 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s2 () Int 0) +[GOOD] (define-fun s15 () Int 1) +[GOOD] (define-fun s8 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" +[GOOD] (declare-fun s10 () Int) ; tracks user variable "__internal_sbv_s10" +[GOOD] (declare-fun s22 () Int) ; tracks user variable "__internal_sbv_s22" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s3 () Bool (> s0 s2)) +[GOOD] (define-fun s4 () Bool (> s1 s2)) +[GOOD] (define-fun s5 () (Seq Int) (seq.unit s0)) +[GOOD] (define-fun s6 () (Seq Int) (seq.unit s1)) +[GOOD] (define-fun s7 () (Seq Int) (seq.++ s5 s6)) +[GOOD] (define-fun s9 () Bool (= s7 s8)) +[GOOD] (define-fun s11 () (Seq Int) (seq.unit s10)) +[GOOD] (define-fun s12 () Int (seq.len s7)) +[GOOD] (define-fun s13 () Bool (> s12 s2)) +[GOOD] (define-fun s14 () Bool (not s13)) +[GOOD] (define-fun s16 () (Seq Int) (seq.extract s7 s2 s15)) +[GOOD] (define-fun s17 () Bool (= s11 s16)) +[GOOD] (define-fun s18 () Bool (or s14 s17)) +[GOOD] (define-fun s19 () Int (- s12 s15)) +[GOOD] (define-fun s20 () (Seq Int) (seq.extract s7 s15 s19)) +[GOOD] (define-fun s21 () Bool (= s8 s20)) +[GOOD] (define-fun s23 () (Seq Int) (seq.unit s22)) +[GOOD] (define-fun s24 () Int (seq.len s20)) +[GOOD] (define-fun s25 () Bool (> s24 s2)) +[GOOD] (define-fun s26 () Bool (not s25)) +[GOOD] (define-fun s27 () (Seq Int) (seq.extract s20 s2 s15)) +[GOOD] (define-fun s28 () Bool (= s23 s27)) +[GOOD] (define-fun s29 () Bool (or s26 s28)) +[GOOD] (define-fun s30 () Int (ite s21 s2 s22)) +[GOOD] (define-fun s31 () Int (+ s10 s30)) +[GOOD] (define-fun s32 () Int (ite s9 s2 s31)) +[GOOD] (define-fun s33 () Int (+ s0 s1)) +[GOOD] (define-fun s34 () Bool (= s32 s33)) +[GOOD] (assert s3) +[GOOD] (assert s4) +[GOOD] (assert s18) +[GOOD] (assert s29) +[GOOD] (assert s34) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldrAB3.gold b/SBVTestSuite/GoldFiles/foldrAB3.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/foldrAB3.gold @@ -0,0 +1,79 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s2 () Int 0) +[GOOD] (define-fun s15 () Int 1) +[GOOD] (define-fun s8 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" +[GOOD] (declare-fun s10 () Int) ; tracks user variable "__internal_sbv_s10" +[GOOD] (declare-fun s22 () Int) ; tracks user variable "__internal_sbv_s22" +[GOOD] (declare-fun s33 () Int) ; tracks user variable "__internal_sbv_s33" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s3 () Bool (> s0 s2)) +[GOOD] (define-fun s4 () Bool (> s1 s2)) +[GOOD] (define-fun s5 () (Seq Int) (seq.unit s0)) +[GOOD] (define-fun s6 () (Seq Int) (seq.unit s1)) +[GOOD] (define-fun s7 () (Seq Int) (seq.++ s5 s6)) +[GOOD] (define-fun s9 () Bool (= s7 s8)) +[GOOD] (define-fun s11 () (Seq Int) (seq.unit s10)) +[GOOD] (define-fun s12 () Int (seq.len s7)) +[GOOD] (define-fun s13 () Bool (> s12 s2)) +[GOOD] (define-fun s14 () Bool (not s13)) +[GOOD] (define-fun s16 () (Seq Int) (seq.extract s7 s2 s15)) +[GOOD] (define-fun s17 () Bool (= s11 s16)) +[GOOD] (define-fun s18 () Bool (or s14 s17)) +[GOOD] (define-fun s19 () Int (- s12 s15)) +[GOOD] (define-fun s20 () (Seq Int) (seq.extract s7 s15 s19)) +[GOOD] (define-fun s21 () Bool (= s8 s20)) +[GOOD] (define-fun s23 () (Seq Int) (seq.unit s22)) +[GOOD] (define-fun s24 () Int (seq.len s20)) +[GOOD] (define-fun s25 () Bool (> s24 s2)) +[GOOD] (define-fun s26 () Bool (not s25)) +[GOOD] (define-fun s27 () (Seq Int) (seq.extract s20 s2 s15)) +[GOOD] (define-fun s28 () Bool (= s23 s27)) +[GOOD] (define-fun s29 () Bool (or s26 s28)) +[GOOD] (define-fun s30 () Int (- s24 s15)) +[GOOD] (define-fun s31 () (Seq Int) (seq.extract s20 s15 s30)) +[GOOD] (define-fun s32 () Bool (= s8 s31)) +[GOOD] (define-fun s34 () (Seq Int) (seq.unit s33)) +[GOOD] (define-fun s35 () Int (seq.len s31)) +[GOOD] (define-fun s36 () Bool (> s35 s2)) +[GOOD] (define-fun s37 () Bool (not s36)) +[GOOD] (define-fun s38 () (Seq Int) (seq.extract s31 s2 s15)) +[GOOD] (define-fun s39 () Bool (= s34 s38)) +[GOOD] (define-fun s40 () Bool (or s37 s39)) +[GOOD] (define-fun s41 () Int (ite s32 s2 s33)) +[GOOD] (define-fun s42 () Int (+ s22 s41)) +[GOOD] (define-fun s43 () Int (ite s21 s2 s42)) +[GOOD] (define-fun s44 () Int (+ s10 s43)) +[GOOD] (define-fun s45 () Int (ite s9 s2 s44)) +[GOOD] (define-fun s46 () Int (+ s0 s1)) +[GOOD] (define-fun s47 () Bool (= s45 s46)) +[GOOD] (assert s3) +[GOOD] (assert s4) +[GOOD] (assert s18) +[GOOD] (assert s29) +[GOOD] (assert s40) +[GOOD] (assert s47) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/mapNoFailure.gold b/SBVTestSuite/GoldFiles/mapNoFailure.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/mapNoFailure.gold @@ -0,0 +1,216 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s5 () Int 6) +[GOOD] (define-fun s7 () Int 0) +[GOOD] (define-fun s20 () Int 1) +[GOOD] (define-fun s66 () Int 10) +[GOOD] (define-fun s18 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" +[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" +[GOOD] (declare-fun s57 () Int) ; tracks user variable "__internal_sbv_s57" +[GOOD] (declare-fun s70 () Int) ; tracks user variable "__internal_sbv_s70" +[GOOD] (declare-fun s82 () Int) ; tracks user variable "__internal_sbv_s82" +[GOOD] (declare-fun s94 () Int) ; tracks user variable "__internal_sbv_s94" +[GOOD] (declare-fun s106 () Int) ; tracks user variable "__internal_sbv_s106" +[GOOD] (declare-fun s118 () Int) ; tracks user variable "__internal_sbv_s118" +[GOOD] (declare-fun s130 () Int) ; tracks user variable "__internal_sbv_s130" +[GOOD] (declare-fun s142 () Int) ; tracks user variable "__internal_sbv_s142" +[GOOD] (declare-fun s154 () Int) ; tracks user variable "__internal_sbv_s154" +[GOOD] (declare-fun s166 () Int) ; tracks user variable "__internal_sbv_s166" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s3 () Int (+ s0 s1)) +[GOOD] (define-fun s4 () Int (+ s2 s3)) +[GOOD] (define-fun s6 () Bool (= s4 s5)) +[GOOD] (define-fun s8 () Bool (> s0 s7)) +[GOOD] (define-fun s9 () Bool (> s1 s7)) +[GOOD] (define-fun s10 () Bool (> s2 s7)) +[GOOD] (define-fun s11 () Bool (and s9 s10)) +[GOOD] (define-fun s12 () Bool (and s8 s11)) +[GOOD] (define-fun s13 () (Seq Int) (seq.unit s0)) +[GOOD] (define-fun s14 () (Seq Int) (seq.unit s1)) +[GOOD] (define-fun s15 () (Seq Int) (seq.unit s2)) +[GOOD] (define-fun s16 () (Seq Int) (seq.++ s14 s15)) +[GOOD] (define-fun s17 () (Seq Int) (seq.++ s13 s16)) +[GOOD] (define-fun s19 () Bool (= s17 s18)) +[GOOD] (define-fun s21 () Int (seq.len s17)) +[GOOD] (define-fun s22 () Int (- s21 s20)) +[GOOD] (define-fun s23 () (Seq Int) (seq.extract s17 s20 s22)) +[GOOD] (define-fun s24 () Bool (= s18 s23)) +[GOOD] (define-fun s25 () Int (seq.len s23)) +[GOOD] (define-fun s26 () Int (- s25 s20)) +[GOOD] (define-fun s27 () (Seq Int) (seq.extract s23 s20 s26)) +[GOOD] (define-fun s28 () Bool (= s18 s27)) +[GOOD] (define-fun s29 () Int (seq.len s27)) +[GOOD] (define-fun s30 () Int (- s29 s20)) +[GOOD] (define-fun s31 () (Seq Int) (seq.extract s27 s20 s30)) +[GOOD] (define-fun s32 () Bool (= s18 s31)) +[GOOD] (define-fun s33 () Int (seq.len s31)) +[GOOD] (define-fun s34 () Int (- s33 s20)) +[GOOD] (define-fun s35 () (Seq Int) (seq.extract s31 s20 s34)) +[GOOD] (define-fun s36 () Bool (= s18 s35)) +[GOOD] (define-fun s37 () Int (seq.len s35)) +[GOOD] (define-fun s38 () Int (- s37 s20)) +[GOOD] (define-fun s39 () (Seq Int) (seq.extract s35 s20 s38)) +[GOOD] (define-fun s40 () Bool (= s18 s39)) +[GOOD] (define-fun s41 () Int (seq.len s39)) +[GOOD] (define-fun s42 () Int (- s41 s20)) +[GOOD] (define-fun s43 () (Seq Int) (seq.extract s39 s20 s42)) +[GOOD] (define-fun s44 () Bool (= s18 s43)) +[GOOD] (define-fun s45 () Int (seq.len s43)) +[GOOD] (define-fun s46 () Int (- s45 s20)) +[GOOD] (define-fun s47 () (Seq Int) (seq.extract s43 s20 s46)) +[GOOD] (define-fun s48 () Bool (= s18 s47)) +[GOOD] (define-fun s49 () Int (seq.len s47)) +[GOOD] (define-fun s50 () Int (- s49 s20)) +[GOOD] (define-fun s51 () (Seq Int) (seq.extract s47 s20 s50)) +[GOOD] (define-fun s52 () Bool (= s18 s51)) +[GOOD] (define-fun s53 () Int (seq.len s51)) +[GOOD] (define-fun s54 () Int (- s53 s20)) +[GOOD] (define-fun s55 () (Seq Int) (seq.extract s51 s20 s54)) +[GOOD] (define-fun s56 () Bool (= s18 s55)) +[GOOD] (define-fun s58 () (Seq Int) (seq.unit s57)) +[GOOD] (define-fun s59 () Int (seq.len s55)) +[GOOD] (define-fun s60 () Bool (> s59 s7)) +[GOOD] (define-fun s61 () Bool (not s60)) +[GOOD] (define-fun s62 () (Seq Int) (seq.extract s55 s7 s20)) +[GOOD] (define-fun s63 () Bool (= s58 s62)) +[GOOD] (define-fun s64 () Bool (or s61 s63)) +[GOOD] (define-fun s65 () Bool (< s57 s7)) +[GOOD] (define-fun s67 () Bool (> s57 s66)) +[GOOD] (define-fun s68 () Bool (or s65 s67)) +[GOOD] (define-fun s69 () Bool (ite s56 s_2 s68)) +[GOOD] (define-fun s71 () (Seq Int) (seq.unit s70)) +[GOOD] (define-fun s72 () Bool (> s53 s7)) +[GOOD] (define-fun s73 () Bool (not s72)) +[GOOD] (define-fun s74 () (Seq Int) (seq.extract s51 s7 s20)) +[GOOD] (define-fun s75 () Bool (= s71 s74)) +[GOOD] (define-fun s76 () Bool (or s73 s75)) +[GOOD] (define-fun s77 () Bool (< s70 s7)) +[GOOD] (define-fun s78 () Bool (> s70 s66)) +[GOOD] (define-fun s79 () Bool (or s77 s78)) +[GOOD] (define-fun s80 () Bool (or s69 s79)) +[GOOD] (define-fun s81 () Bool (ite s52 s_2 s80)) +[GOOD] (define-fun s83 () (Seq Int) (seq.unit s82)) +[GOOD] (define-fun s84 () Bool (> s49 s7)) +[GOOD] (define-fun s85 () Bool (not s84)) +[GOOD] (define-fun s86 () (Seq Int) (seq.extract s47 s7 s20)) +[GOOD] (define-fun s87 () Bool (= s83 s86)) +[GOOD] (define-fun s88 () Bool (or s85 s87)) +[GOOD] (define-fun s89 () Bool (< s82 s7)) +[GOOD] (define-fun s90 () Bool (> s82 s66)) +[GOOD] (define-fun s91 () Bool (or s89 s90)) +[GOOD] (define-fun s92 () Bool (or s81 s91)) +[GOOD] (define-fun s93 () Bool (ite s48 s_2 s92)) +[GOOD] (define-fun s95 () (Seq Int) (seq.unit s94)) +[GOOD] (define-fun s96 () Bool (> s45 s7)) +[GOOD] (define-fun s97 () Bool (not s96)) +[GOOD] (define-fun s98 () (Seq Int) (seq.extract s43 s7 s20)) +[GOOD] (define-fun s99 () Bool (= s95 s98)) +[GOOD] (define-fun s100 () Bool (or s97 s99)) +[GOOD] (define-fun s101 () Bool (< s94 s7)) +[GOOD] (define-fun s102 () Bool (> s94 s66)) +[GOOD] (define-fun s103 () Bool (or s101 s102)) +[GOOD] (define-fun s104 () Bool (or s93 s103)) +[GOOD] (define-fun s105 () Bool (ite s44 s_2 s104)) +[GOOD] (define-fun s107 () (Seq Int) (seq.unit s106)) +[GOOD] (define-fun s108 () Bool (> s41 s7)) +[GOOD] (define-fun s109 () Bool (not s108)) +[GOOD] (define-fun s110 () (Seq Int) (seq.extract s39 s7 s20)) +[GOOD] (define-fun s111 () Bool (= s107 s110)) +[GOOD] (define-fun s112 () Bool (or s109 s111)) +[GOOD] (define-fun s113 () Bool (< s106 s7)) +[GOOD] (define-fun s114 () Bool (> s106 s66)) +[GOOD] (define-fun s115 () Bool (or s113 s114)) +[GOOD] (define-fun s116 () Bool (or s105 s115)) +[GOOD] (define-fun s117 () Bool (ite s40 s_2 s116)) +[GOOD] (define-fun s119 () (Seq Int) (seq.unit s118)) +[GOOD] (define-fun s120 () Bool (> s37 s7)) +[GOOD] (define-fun s121 () Bool (not s120)) +[GOOD] (define-fun s122 () (Seq Int) (seq.extract s35 s7 s20)) +[GOOD] (define-fun s123 () Bool (= s119 s122)) +[GOOD] (define-fun s124 () Bool (or s121 s123)) +[GOOD] (define-fun s125 () Bool (< s118 s7)) +[GOOD] (define-fun s126 () Bool (> s118 s66)) +[GOOD] (define-fun s127 () Bool (or s125 s126)) +[GOOD] (define-fun s128 () Bool (or s117 s127)) +[GOOD] (define-fun s129 () Bool (ite s36 s_2 s128)) +[GOOD] (define-fun s131 () (Seq Int) (seq.unit s130)) +[GOOD] (define-fun s132 () Bool (> s33 s7)) +[GOOD] (define-fun s133 () Bool (not s132)) +[GOOD] (define-fun s134 () (Seq Int) (seq.extract s31 s7 s20)) +[GOOD] (define-fun s135 () Bool (= s131 s134)) +[GOOD] (define-fun s136 () Bool (or s133 s135)) +[GOOD] (define-fun s137 () Bool (< s130 s7)) +[GOOD] (define-fun s138 () Bool (> s130 s66)) +[GOOD] (define-fun s139 () Bool (or s137 s138)) +[GOOD] (define-fun s140 () Bool (or s129 s139)) +[GOOD] (define-fun s141 () Bool (ite s32 s_2 s140)) +[GOOD] (define-fun s143 () (Seq Int) (seq.unit s142)) +[GOOD] (define-fun s144 () Bool (> s29 s7)) +[GOOD] (define-fun s145 () Bool (not s144)) +[GOOD] (define-fun s146 () (Seq Int) (seq.extract s27 s7 s20)) +[GOOD] (define-fun s147 () Bool (= s143 s146)) +[GOOD] (define-fun s148 () Bool (or s145 s147)) +[GOOD] (define-fun s149 () Bool (< s142 s7)) +[GOOD] (define-fun s150 () Bool (> s142 s66)) +[GOOD] (define-fun s151 () Bool (or s149 s150)) +[GOOD] (define-fun s152 () Bool (or s141 s151)) +[GOOD] (define-fun s153 () Bool (ite s28 s_2 s152)) +[GOOD] (define-fun s155 () (Seq Int) (seq.unit s154)) +[GOOD] (define-fun s156 () Bool (> s25 s7)) +[GOOD] (define-fun s157 () Bool (not s156)) +[GOOD] (define-fun s158 () (Seq Int) (seq.extract s23 s7 s20)) +[GOOD] (define-fun s159 () Bool (= s155 s158)) +[GOOD] (define-fun s160 () Bool (or s157 s159)) +[GOOD] (define-fun s161 () Bool (< s154 s7)) +[GOOD] (define-fun s162 () Bool (> s154 s66)) +[GOOD] (define-fun s163 () Bool (or s161 s162)) +[GOOD] (define-fun s164 () Bool (or s153 s163)) +[GOOD] (define-fun s165 () Bool (ite s24 s_2 s164)) +[GOOD] (define-fun s167 () (Seq Int) (seq.unit s166)) +[GOOD] (define-fun s168 () Bool (> s21 s7)) +[GOOD] (define-fun s169 () Bool (not s168)) +[GOOD] (define-fun s170 () (Seq Int) (seq.extract s17 s7 s20)) +[GOOD] (define-fun s171 () Bool (= s167 s170)) +[GOOD] (define-fun s172 () Bool (or s169 s171)) +[GOOD] (define-fun s173 () Bool (< s166 s7)) +[GOOD] (define-fun s174 () Bool (> s166 s66)) +[GOOD] (define-fun s175 () Bool (or s173 s174)) +[GOOD] (define-fun s176 () Bool (or s165 s175)) +[GOOD] (define-fun s177 () Bool (ite s19 s_2 s176)) +[GOOD] (assert s6) +[GOOD] (assert s12) +[GOOD] (assert s64) +[GOOD] (assert s76) +[GOOD] (assert s88) +[GOOD] (assert s100) +[GOOD] (assert s112) +[GOOD] (assert s124) +[GOOD] (assert s136) +[GOOD] (assert s148) +[GOOD] (assert s160) +[GOOD] (assert s172) +[GOOD] (assert s177) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/mapWithFailure.gold b/SBVTestSuite/GoldFiles/mapWithFailure.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/mapWithFailure.gold @@ -0,0 +1,251 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s8 () Int 0) +[GOOD] (define-fun s11 () Int 1) +[GOOD] (define-fun s154 () Int 2) +[GOOD] (define-fun s160 () Int 11) +[GOOD] (define-fun s164 () Int 10) +[GOOD] (define-fun s3 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "ints" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "__internal_sbv_s1" +[GOOD] (declare-fun s5 () Int) ; tracks user variable "__internal_sbv_s5" +[GOOD] (declare-fun s20 () Int) ; tracks user variable "__internal_sbv_s20" +[GOOD] (declare-fun s33 () Int) ; tracks user variable "__internal_sbv_s33" +[GOOD] (declare-fun s46 () Int) ; tracks user variable "__internal_sbv_s46" +[GOOD] (declare-fun s59 () Int) ; tracks user variable "__internal_sbv_s59" +[GOOD] (declare-fun s72 () Int) ; tracks user variable "__internal_sbv_s72" +[GOOD] (declare-fun s85 () Int) ; tracks user variable "__internal_sbv_s85" +[GOOD] (declare-fun s98 () Int) ; tracks user variable "__internal_sbv_s98" +[GOOD] (declare-fun s111 () Int) ; tracks user variable "__internal_sbv_s111" +[GOOD] (declare-fun s124 () Int) ; tracks user variable "__internal_sbv_s124" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s2 () (Seq Int) (seq.unit s1)) +[GOOD] (define-fun s4 () Bool (= s0 s3)) +[GOOD] (define-fun s6 () (Seq Int) (seq.unit s5)) +[GOOD] (define-fun s7 () Int (seq.len s0)) +[GOOD] (define-fun s9 () Bool (> s7 s8)) +[GOOD] (define-fun s10 () Bool (not s9)) +[GOOD] (define-fun s12 () (Seq Int) (seq.extract s0 s8 s11)) +[GOOD] (define-fun s13 () Bool (= s6 s12)) +[GOOD] (define-fun s14 () Bool (or s10 s13)) +[GOOD] (define-fun s15 () Int (+ s5 s11)) +[GOOD] (define-fun s16 () (Seq Int) (seq.unit s15)) +[GOOD] (define-fun s17 () Int (- s7 s11)) +[GOOD] (define-fun s18 () (Seq Int) (seq.extract s0 s11 s17)) +[GOOD] (define-fun s19 () Bool (= s3 s18)) +[GOOD] (define-fun s21 () (Seq Int) (seq.unit s20)) +[GOOD] (define-fun s22 () Int (seq.len s18)) +[GOOD] (define-fun s23 () Bool (> s22 s8)) +[GOOD] (define-fun s24 () Bool (not s23)) +[GOOD] (define-fun s25 () (Seq Int) (seq.extract s18 s8 s11)) +[GOOD] (define-fun s26 () Bool (= s21 s25)) +[GOOD] (define-fun s27 () Bool (or s24 s26)) +[GOOD] (define-fun s28 () Int (+ s11 s20)) +[GOOD] (define-fun s29 () (Seq Int) (seq.unit s28)) +[GOOD] (define-fun s30 () Int (- s22 s11)) +[GOOD] (define-fun s31 () (Seq Int) (seq.extract s18 s11 s30)) +[GOOD] (define-fun s32 () Bool (= s3 s31)) +[GOOD] (define-fun s34 () (Seq Int) (seq.unit s33)) +[GOOD] (define-fun s35 () Int (seq.len s31)) +[GOOD] (define-fun s36 () Bool (> s35 s8)) +[GOOD] (define-fun s37 () Bool (not s36)) +[GOOD] (define-fun s38 () (Seq Int) (seq.extract s31 s8 s11)) +[GOOD] (define-fun s39 () Bool (= s34 s38)) +[GOOD] (define-fun s40 () Bool (or s37 s39)) +[GOOD] (define-fun s41 () Int (+ s11 s33)) +[GOOD] (define-fun s42 () (Seq Int) (seq.unit s41)) +[GOOD] (define-fun s43 () Int (- s35 s11)) +[GOOD] (define-fun s44 () (Seq Int) (seq.extract s31 s11 s43)) +[GOOD] (define-fun s45 () Bool (= s3 s44)) +[GOOD] (define-fun s47 () (Seq Int) (seq.unit s46)) +[GOOD] (define-fun s48 () Int (seq.len s44)) +[GOOD] (define-fun s49 () Bool (> s48 s8)) +[GOOD] (define-fun s50 () Bool (not s49)) +[GOOD] (define-fun s51 () (Seq Int) (seq.extract s44 s8 s11)) +[GOOD] (define-fun s52 () Bool (= s47 s51)) +[GOOD] (define-fun s53 () Bool (or s50 s52)) +[GOOD] (define-fun s54 () Int (+ s11 s46)) +[GOOD] (define-fun s55 () (Seq Int) (seq.unit s54)) +[GOOD] (define-fun s56 () Int (- s48 s11)) +[GOOD] (define-fun s57 () (Seq Int) (seq.extract s44 s11 s56)) +[GOOD] (define-fun s58 () Bool (= s3 s57)) +[GOOD] (define-fun s60 () (Seq Int) (seq.unit s59)) +[GOOD] (define-fun s61 () Int (seq.len s57)) +[GOOD] (define-fun s62 () Bool (> s61 s8)) +[GOOD] (define-fun s63 () Bool (not s62)) +[GOOD] (define-fun s64 () (Seq Int) (seq.extract s57 s8 s11)) +[GOOD] (define-fun s65 () Bool (= s60 s64)) +[GOOD] (define-fun s66 () Bool (or s63 s65)) +[GOOD] (define-fun s67 () Int (+ s11 s59)) +[GOOD] (define-fun s68 () (Seq Int) (seq.unit s67)) +[GOOD] (define-fun s69 () Int (- s61 s11)) +[GOOD] (define-fun s70 () (Seq Int) (seq.extract s57 s11 s69)) +[GOOD] (define-fun s71 () Bool (= s3 s70)) +[GOOD] (define-fun s73 () (Seq Int) (seq.unit s72)) +[GOOD] (define-fun s74 () Int (seq.len s70)) +[GOOD] (define-fun s75 () Bool (> s74 s8)) +[GOOD] (define-fun s76 () Bool (not s75)) +[GOOD] (define-fun s77 () (Seq Int) (seq.extract s70 s8 s11)) +[GOOD] (define-fun s78 () Bool (= s73 s77)) +[GOOD] (define-fun s79 () Bool (or s76 s78)) +[GOOD] (define-fun s80 () Int (+ s11 s72)) +[GOOD] (define-fun s81 () (Seq Int) (seq.unit s80)) +[GOOD] (define-fun s82 () Int (- s74 s11)) +[GOOD] (define-fun s83 () (Seq Int) (seq.extract s70 s11 s82)) +[GOOD] (define-fun s84 () Bool (= s3 s83)) +[GOOD] (define-fun s86 () (Seq Int) (seq.unit s85)) +[GOOD] (define-fun s87 () Int (seq.len s83)) +[GOOD] (define-fun s88 () Bool (> s87 s8)) +[GOOD] (define-fun s89 () Bool (not s88)) +[GOOD] (define-fun s90 () (Seq Int) (seq.extract s83 s8 s11)) +[GOOD] (define-fun s91 () Bool (= s86 s90)) +[GOOD] (define-fun s92 () Bool (or s89 s91)) +[GOOD] (define-fun s93 () Int (+ s11 s85)) +[GOOD] (define-fun s94 () (Seq Int) (seq.unit s93)) +[GOOD] (define-fun s95 () Int (- s87 s11)) +[GOOD] (define-fun s96 () (Seq Int) (seq.extract s83 s11 s95)) +[GOOD] (define-fun s97 () Bool (= s3 s96)) +[GOOD] (define-fun s99 () (Seq Int) (seq.unit s98)) +[GOOD] (define-fun s100 () Int (seq.len s96)) +[GOOD] (define-fun s101 () Bool (> s100 s8)) +[GOOD] (define-fun s102 () Bool (not s101)) +[GOOD] (define-fun s103 () (Seq Int) (seq.extract s96 s8 s11)) +[GOOD] (define-fun s104 () Bool (= s99 s103)) +[GOOD] (define-fun s105 () Bool (or s102 s104)) +[GOOD] (define-fun s106 () Int (+ s11 s98)) +[GOOD] (define-fun s107 () (Seq Int) (seq.unit s106)) +[GOOD] (define-fun s108 () Int (- s100 s11)) +[GOOD] (define-fun s109 () (Seq Int) (seq.extract s96 s11 s108)) +[GOOD] (define-fun s110 () Bool (= s3 s109)) +[GOOD] (define-fun s112 () (Seq Int) (seq.unit s111)) +[GOOD] (define-fun s113 () Int (seq.len s109)) +[GOOD] (define-fun s114 () Bool (> s113 s8)) +[GOOD] (define-fun s115 () Bool (not s114)) +[GOOD] (define-fun s116 () (Seq Int) (seq.extract s109 s8 s11)) +[GOOD] (define-fun s117 () Bool (= s112 s116)) +[GOOD] (define-fun s118 () Bool (or s115 s117)) +[GOOD] (define-fun s119 () Int (+ s11 s111)) +[GOOD] (define-fun s120 () (Seq Int) (seq.unit s119)) +[GOOD] (define-fun s121 () Int (- s113 s11)) +[GOOD] (define-fun s122 () (Seq Int) (seq.extract s109 s11 s121)) +[GOOD] (define-fun s123 () Bool (= s3 s122)) +[GOOD] (define-fun s125 () (Seq Int) (seq.unit s124)) +[GOOD] (define-fun s126 () Int (seq.len s122)) +[GOOD] (define-fun s127 () Bool (> s126 s8)) +[GOOD] (define-fun s128 () Bool (not s127)) +[GOOD] (define-fun s129 () (Seq Int) (seq.extract s122 s8 s11)) +[GOOD] (define-fun s130 () Bool (= s125 s129)) +[GOOD] (define-fun s131 () Bool (or s128 s130)) +[GOOD] (define-fun s132 () Int (+ s11 s124)) +[GOOD] (define-fun s133 () (Seq Int) (seq.unit s132)) +[GOOD] (define-fun s134 () (Seq Int) (ite s123 s3 s133)) +[GOOD] (define-fun s135 () (Seq Int) (seq.++ s120 s134)) +[GOOD] (define-fun s136 () (Seq Int) (ite s110 s3 s135)) +[GOOD] (define-fun s137 () (Seq Int) (seq.++ s107 s136)) +[GOOD] (define-fun s138 () (Seq Int) (ite s97 s3 s137)) +[GOOD] (define-fun s139 () (Seq Int) (seq.++ s94 s138)) +[GOOD] (define-fun s140 () (Seq Int) (ite s84 s3 s139)) +[GOOD] (define-fun s141 () (Seq Int) (seq.++ s81 s140)) +[GOOD] (define-fun s142 () (Seq Int) (ite s71 s3 s141)) +[GOOD] (define-fun s143 () (Seq Int) (seq.++ s68 s142)) +[GOOD] (define-fun s144 () (Seq Int) (ite s58 s3 s143)) +[GOOD] (define-fun s145 () (Seq Int) (seq.++ s55 s144)) +[GOOD] (define-fun s146 () (Seq Int) (ite s45 s3 s145)) +[GOOD] (define-fun s147 () (Seq Int) (seq.++ s42 s146)) +[GOOD] (define-fun s148 () (Seq Int) (ite s32 s3 s147)) +[GOOD] (define-fun s149 () (Seq Int) (seq.++ s29 s148)) +[GOOD] (define-fun s150 () (Seq Int) (ite s19 s3 s149)) +[GOOD] (define-fun s151 () (Seq Int) (seq.++ s16 s150)) +[GOOD] (define-fun s152 () (Seq Int) (ite s4 s3 s151)) +[GOOD] (define-fun s153 () Int (seq.len s152)) +[GOOD] (define-fun s155 () Bool (> s153 s154)) +[GOOD] (define-fun s156 () Bool (not s155)) +[GOOD] (define-fun s157 () (Seq Int) (seq.extract s152 s154 s11)) +[GOOD] (define-fun s158 () Bool (= s2 s157)) +[GOOD] (define-fun s159 () Bool (or s156 s158)) +[GOOD] (define-fun s161 () Bool (> s1 s160)) +[GOOD] (define-fun s162 () Bool (not s161)) +[GOOD] (define-fun s163 () Bool (< s124 s8)) +[GOOD] (define-fun s165 () Bool (> s124 s164)) +[GOOD] (define-fun s166 () Bool (or s163 s165)) +[GOOD] (define-fun s167 () Bool (ite s123 s_2 s166)) +[GOOD] (define-fun s168 () Bool (< s111 s8)) +[GOOD] (define-fun s169 () Bool (> s111 s164)) +[GOOD] (define-fun s170 () Bool (or s168 s169)) +[GOOD] (define-fun s171 () Bool (or s167 s170)) +[GOOD] (define-fun s172 () Bool (ite s110 s_2 s171)) +[GOOD] (define-fun s173 () Bool (< s98 s8)) +[GOOD] (define-fun s174 () Bool (> s98 s164)) +[GOOD] (define-fun s175 () Bool (or s173 s174)) +[GOOD] (define-fun s176 () Bool (or s172 s175)) +[GOOD] (define-fun s177 () Bool (ite s97 s_2 s176)) +[GOOD] (define-fun s178 () Bool (< s85 s8)) +[GOOD] (define-fun s179 () Bool (> s85 s164)) +[GOOD] (define-fun s180 () Bool (or s178 s179)) +[GOOD] (define-fun s181 () Bool (or s177 s180)) +[GOOD] (define-fun s182 () Bool (ite s84 s_2 s181)) +[GOOD] (define-fun s183 () Bool (< s72 s8)) +[GOOD] (define-fun s184 () Bool (> s72 s164)) +[GOOD] (define-fun s185 () Bool (or s183 s184)) +[GOOD] (define-fun s186 () Bool (or s182 s185)) +[GOOD] (define-fun s187 () Bool (ite s71 s_2 s186)) +[GOOD] (define-fun s188 () Bool (< s59 s8)) +[GOOD] (define-fun s189 () Bool (> s59 s164)) +[GOOD] (define-fun s190 () Bool (or s188 s189)) +[GOOD] (define-fun s191 () Bool (or s187 s190)) +[GOOD] (define-fun s192 () Bool (ite s58 s_2 s191)) +[GOOD] (define-fun s193 () Bool (< s46 s8)) +[GOOD] (define-fun s194 () Bool (> s46 s164)) +[GOOD] (define-fun s195 () Bool (or s193 s194)) +[GOOD] (define-fun s196 () Bool (or s192 s195)) +[GOOD] (define-fun s197 () Bool (ite s45 s_2 s196)) +[GOOD] (define-fun s198 () Bool (< s33 s8)) +[GOOD] (define-fun s199 () Bool (> s33 s164)) +[GOOD] (define-fun s200 () Bool (or s198 s199)) +[GOOD] (define-fun s201 () Bool (or s197 s200)) +[GOOD] (define-fun s202 () Bool (ite s32 s_2 s201)) +[GOOD] (define-fun s203 () Bool (< s20 s8)) +[GOOD] (define-fun s204 () Bool (> s20 s164)) +[GOOD] (define-fun s205 () Bool (or s203 s204)) +[GOOD] (define-fun s206 () Bool (or s202 s205)) +[GOOD] (define-fun s207 () Bool (ite s19 s_2 s206)) +[GOOD] (define-fun s208 () Bool (< s5 s8)) +[GOOD] (define-fun s209 () Bool (> s5 s164)) +[GOOD] (define-fun s210 () Bool (or s208 s209)) +[GOOD] (define-fun s211 () Bool (or s207 s210)) +[GOOD] (define-fun s212 () Bool (ite s4 s_2 s211)) +[GOOD] (define-fun s213 () Bool (or s162 s212)) +[GOOD] (assert s14) +[GOOD] (assert s27) +[GOOD] (assert s40) +[GOOD] (assert s53) +[GOOD] (assert s66) +[GOOD] (assert s79) +[GOOD] (assert s92) +[GOOD] (assert s105) +[GOOD] (assert s118) +[GOOD] (assert s131) +[GOOD] (assert s159) +[GOOD] (assert s213) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/maxlWithFailure.gold b/SBVTestSuite/GoldFiles/maxlWithFailure.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/maxlWithFailure.gold @@ -0,0 +1,231 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s3 () Int 0) +[GOOD] (define-fun s4 () Int 1) +[GOOD] (define-fun s142 () Int 10) +[GOOD] (define-fun s1 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "ints" +[GOOD] (declare-fun s9 () Int) ; tracks user variable "__internal_sbv_s9" +[GOOD] (declare-fun s22 () Int) ; tracks user variable "__internal_sbv_s22" +[GOOD] (declare-fun s35 () Int) ; tracks user variable "__internal_sbv_s35" +[GOOD] (declare-fun s48 () Int) ; tracks user variable "__internal_sbv_s48" +[GOOD] (declare-fun s61 () Int) ; tracks user variable "__internal_sbv_s61" +[GOOD] (declare-fun s74 () Int) ; tracks user variable "__internal_sbv_s74" +[GOOD] (declare-fun s87 () Int) ; tracks user variable "__internal_sbv_s87" +[GOOD] (declare-fun s100 () Int) ; tracks user variable "__internal_sbv_s100" +[GOOD] (declare-fun s113 () Int) ; tracks user variable "__internal_sbv_s113" +[GOOD] (declare-fun s122 () Int) ; tracks user variable "__internal_sbv_s122" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s2 () Bool (= s0 s1)) +[GOOD] (define-fun s5 () Int (seq.len s0)) +[GOOD] (define-fun s6 () Int (- s5 s4)) +[GOOD] (define-fun s7 () (Seq Int) (seq.extract s0 s4 s6)) +[GOOD] (define-fun s8 () Bool (= s1 s7)) +[GOOD] (define-fun s10 () (Seq Int) (seq.unit s9)) +[GOOD] (define-fun s11 () Bool (> s5 s3)) +[GOOD] (define-fun s12 () Bool (not s11)) +[GOOD] (define-fun s13 () (Seq Int) (seq.extract s0 s3 s4)) +[GOOD] (define-fun s14 () Bool (= s10 s13)) +[GOOD] (define-fun s15 () Bool (or s12 s14)) +[GOOD] (define-fun s16 () Bool (<= s9 s3)) +[GOOD] (define-fun s17 () Int (ite s16 s3 s9)) +[GOOD] (define-fun s18 () Int (seq.len s7)) +[GOOD] (define-fun s19 () Int (- s18 s4)) +[GOOD] (define-fun s20 () (Seq Int) (seq.extract s7 s4 s19)) +[GOOD] (define-fun s21 () Bool (= s1 s20)) +[GOOD] (define-fun s23 () (Seq Int) (seq.unit s22)) +[GOOD] (define-fun s24 () Bool (> s18 s3)) +[GOOD] (define-fun s25 () Bool (not s24)) +[GOOD] (define-fun s26 () (Seq Int) (seq.extract s7 s3 s4)) +[GOOD] (define-fun s27 () Bool (= s23 s26)) +[GOOD] (define-fun s28 () Bool (or s25 s27)) +[GOOD] (define-fun s29 () Bool (<= s22 s17)) +[GOOD] (define-fun s30 () Int (ite s29 s17 s22)) +[GOOD] (define-fun s31 () Int (seq.len s20)) +[GOOD] (define-fun s32 () Int (- s31 s4)) +[GOOD] (define-fun s33 () (Seq Int) (seq.extract s20 s4 s32)) +[GOOD] (define-fun s34 () Bool (= s1 s33)) +[GOOD] (define-fun s36 () (Seq Int) (seq.unit s35)) +[GOOD] (define-fun s37 () Bool (> s31 s3)) +[GOOD] (define-fun s38 () Bool (not s37)) +[GOOD] (define-fun s39 () (Seq Int) (seq.extract s20 s3 s4)) +[GOOD] (define-fun s40 () Bool (= s36 s39)) +[GOOD] (define-fun s41 () Bool (or s38 s40)) +[GOOD] (define-fun s42 () Bool (<= s35 s30)) +[GOOD] (define-fun s43 () Int (ite s42 s30 s35)) +[GOOD] (define-fun s44 () Int (seq.len s33)) +[GOOD] (define-fun s45 () Int (- s44 s4)) +[GOOD] (define-fun s46 () (Seq Int) (seq.extract s33 s4 s45)) +[GOOD] (define-fun s47 () Bool (= s1 s46)) +[GOOD] (define-fun s49 () (Seq Int) (seq.unit s48)) +[GOOD] (define-fun s50 () Bool (> s44 s3)) +[GOOD] (define-fun s51 () Bool (not s50)) +[GOOD] (define-fun s52 () (Seq Int) (seq.extract s33 s3 s4)) +[GOOD] (define-fun s53 () Bool (= s49 s52)) +[GOOD] (define-fun s54 () Bool (or s51 s53)) +[GOOD] (define-fun s55 () Bool (<= s48 s43)) +[GOOD] (define-fun s56 () Int (ite s55 s43 s48)) +[GOOD] (define-fun s57 () Int (seq.len s46)) +[GOOD] (define-fun s58 () Int (- s57 s4)) +[GOOD] (define-fun s59 () (Seq Int) (seq.extract s46 s4 s58)) +[GOOD] (define-fun s60 () Bool (= s1 s59)) +[GOOD] (define-fun s62 () (Seq Int) (seq.unit s61)) +[GOOD] (define-fun s63 () Bool (> s57 s3)) +[GOOD] (define-fun s64 () Bool (not s63)) +[GOOD] (define-fun s65 () (Seq Int) (seq.extract s46 s3 s4)) +[GOOD] (define-fun s66 () Bool (= s62 s65)) +[GOOD] (define-fun s67 () Bool (or s64 s66)) +[GOOD] (define-fun s68 () Bool (<= s61 s56)) +[GOOD] (define-fun s69 () Int (ite s68 s56 s61)) +[GOOD] (define-fun s70 () Int (seq.len s59)) +[GOOD] (define-fun s71 () Int (- s70 s4)) +[GOOD] (define-fun s72 () (Seq Int) (seq.extract s59 s4 s71)) +[GOOD] (define-fun s73 () Bool (= s1 s72)) +[GOOD] (define-fun s75 () (Seq Int) (seq.unit s74)) +[GOOD] (define-fun s76 () Bool (> s70 s3)) +[GOOD] (define-fun s77 () Bool (not s76)) +[GOOD] (define-fun s78 () (Seq Int) (seq.extract s59 s3 s4)) +[GOOD] (define-fun s79 () Bool (= s75 s78)) +[GOOD] (define-fun s80 () Bool (or s77 s79)) +[GOOD] (define-fun s81 () Bool (<= s74 s69)) +[GOOD] (define-fun s82 () Int (ite s81 s69 s74)) +[GOOD] (define-fun s83 () Int (seq.len s72)) +[GOOD] (define-fun s84 () Int (- s83 s4)) +[GOOD] (define-fun s85 () (Seq Int) (seq.extract s72 s4 s84)) +[GOOD] (define-fun s86 () Bool (= s1 s85)) +[GOOD] (define-fun s88 () (Seq Int) (seq.unit s87)) +[GOOD] (define-fun s89 () Bool (> s83 s3)) +[GOOD] (define-fun s90 () Bool (not s89)) +[GOOD] (define-fun s91 () (Seq Int) (seq.extract s72 s3 s4)) +[GOOD] (define-fun s92 () Bool (= s88 s91)) +[GOOD] (define-fun s93 () Bool (or s90 s92)) +[GOOD] (define-fun s94 () Bool (<= s87 s82)) +[GOOD] (define-fun s95 () Int (ite s94 s82 s87)) +[GOOD] (define-fun s96 () Int (seq.len s85)) +[GOOD] (define-fun s97 () Int (- s96 s4)) +[GOOD] (define-fun s98 () (Seq Int) (seq.extract s85 s4 s97)) +[GOOD] (define-fun s99 () Bool (= s1 s98)) +[GOOD] (define-fun s101 () (Seq Int) (seq.unit s100)) +[GOOD] (define-fun s102 () Bool (> s96 s3)) +[GOOD] (define-fun s103 () Bool (not s102)) +[GOOD] (define-fun s104 () (Seq Int) (seq.extract s85 s3 s4)) +[GOOD] (define-fun s105 () Bool (= s101 s104)) +[GOOD] (define-fun s106 () Bool (or s103 s105)) +[GOOD] (define-fun s107 () Bool (<= s100 s95)) +[GOOD] (define-fun s108 () Int (ite s107 s95 s100)) +[GOOD] (define-fun s109 () Int (seq.len s98)) +[GOOD] (define-fun s110 () Int (- s109 s4)) +[GOOD] (define-fun s111 () (Seq Int) (seq.extract s98 s4 s110)) +[GOOD] (define-fun s112 () Bool (= s1 s111)) +[GOOD] (define-fun s114 () (Seq Int) (seq.unit s113)) +[GOOD] (define-fun s115 () Bool (> s109 s3)) +[GOOD] (define-fun s116 () Bool (not s115)) +[GOOD] (define-fun s117 () (Seq Int) (seq.extract s98 s3 s4)) +[GOOD] (define-fun s118 () Bool (= s114 s117)) +[GOOD] (define-fun s119 () Bool (or s116 s118)) +[GOOD] (define-fun s120 () Bool (<= s113 s108)) +[GOOD] (define-fun s121 () Int (ite s120 s108 s113)) +[GOOD] (define-fun s123 () (Seq Int) (seq.unit s122)) +[GOOD] (define-fun s124 () Int (seq.len s111)) +[GOOD] (define-fun s125 () Bool (> s124 s3)) +[GOOD] (define-fun s126 () Bool (not s125)) +[GOOD] (define-fun s127 () (Seq Int) (seq.extract s111 s3 s4)) +[GOOD] (define-fun s128 () Bool (= s123 s127)) +[GOOD] (define-fun s129 () Bool (or s126 s128)) +[GOOD] (define-fun s130 () Bool (<= s122 s121)) +[GOOD] (define-fun s131 () Int (ite s130 s121 s122)) +[GOOD] (define-fun s132 () Int (ite s112 s121 s131)) +[GOOD] (define-fun s133 () Int (ite s99 s108 s132)) +[GOOD] (define-fun s134 () Int (ite s86 s95 s133)) +[GOOD] (define-fun s135 () Int (ite s73 s82 s134)) +[GOOD] (define-fun s136 () Int (ite s60 s69 s135)) +[GOOD] (define-fun s137 () Int (ite s47 s56 s136)) +[GOOD] (define-fun s138 () Int (ite s34 s43 s137)) +[GOOD] (define-fun s139 () Int (ite s21 s30 s138)) +[GOOD] (define-fun s140 () Int (ite s8 s17 s139)) +[GOOD] (define-fun s141 () Int (ite s2 s3 s140)) +[GOOD] (define-fun s143 () Bool (> s141 s142)) +[GOOD] (define-fun s144 () Bool (not s143)) +[GOOD] (define-fun s145 () Bool (< s9 s3)) +[GOOD] (define-fun s146 () Bool (> s9 s142)) +[GOOD] (define-fun s147 () Bool (or s145 s146)) +[GOOD] (define-fun s148 () Bool (< s22 s3)) +[GOOD] (define-fun s149 () Bool (> s22 s142)) +[GOOD] (define-fun s150 () Bool (or s148 s149)) +[GOOD] (define-fun s151 () Bool (or s147 s150)) +[GOOD] (define-fun s152 () Bool (< s35 s3)) +[GOOD] (define-fun s153 () Bool (> s35 s142)) +[GOOD] (define-fun s154 () Bool (or s152 s153)) +[GOOD] (define-fun s155 () Bool (or s151 s154)) +[GOOD] (define-fun s156 () Bool (< s48 s3)) +[GOOD] (define-fun s157 () Bool (> s48 s142)) +[GOOD] (define-fun s158 () Bool (or s156 s157)) +[GOOD] (define-fun s159 () Bool (or s155 s158)) +[GOOD] (define-fun s160 () Bool (< s61 s3)) +[GOOD] (define-fun s161 () Bool (> s61 s142)) +[GOOD] (define-fun s162 () Bool (or s160 s161)) +[GOOD] (define-fun s163 () Bool (or s159 s162)) +[GOOD] (define-fun s164 () Bool (< s74 s3)) +[GOOD] (define-fun s165 () Bool (> s74 s142)) +[GOOD] (define-fun s166 () Bool (or s164 s165)) +[GOOD] (define-fun s167 () Bool (or s163 s166)) +[GOOD] (define-fun s168 () Bool (< s87 s3)) +[GOOD] (define-fun s169 () Bool (> s87 s142)) +[GOOD] (define-fun s170 () Bool (or s168 s169)) +[GOOD] (define-fun s171 () Bool (or s167 s170)) +[GOOD] (define-fun s172 () Bool (< s100 s3)) +[GOOD] (define-fun s173 () Bool (> s100 s142)) +[GOOD] (define-fun s174 () Bool (or s172 s173)) +[GOOD] (define-fun s175 () Bool (or s171 s174)) +[GOOD] (define-fun s176 () Bool (< s113 s3)) +[GOOD] (define-fun s177 () Bool (> s113 s142)) +[GOOD] (define-fun s178 () Bool (or s176 s177)) +[GOOD] (define-fun s179 () Bool (or s175 s178)) +[GOOD] (define-fun s180 () Bool (< s122 s3)) +[GOOD] (define-fun s181 () Bool (> s122 s142)) +[GOOD] (define-fun s182 () Bool (or s180 s181)) +[GOOD] (define-fun s183 () Bool (or s179 s182)) +[GOOD] (define-fun s184 () Bool (ite s112 s179 s183)) +[GOOD] (define-fun s185 () Bool (ite s99 s175 s184)) +[GOOD] (define-fun s186 () Bool (ite s86 s171 s185)) +[GOOD] (define-fun s187 () Bool (ite s73 s167 s186)) +[GOOD] (define-fun s188 () Bool (ite s60 s163 s187)) +[GOOD] (define-fun s189 () Bool (ite s47 s159 s188)) +[GOOD] (define-fun s190 () Bool (ite s34 s155 s189)) +[GOOD] (define-fun s191 () Bool (ite s21 s151 s190)) +[GOOD] (define-fun s192 () Bool (ite s8 s147 s191)) +[GOOD] (define-fun s193 () Bool (ite s2 s_2 s192)) +[GOOD] (define-fun s194 () Bool (or s144 s193)) +[GOOD] (assert s15) +[GOOD] (assert s28) +[GOOD] (assert s41) +[GOOD] (assert s54) +[GOOD] (assert s67) +[GOOD] (assert s80) +[GOOD] (assert s93) +[GOOD] (assert s106) +[GOOD] (assert s119) +[GOOD] (assert s129) +[GOOD] (assert s194) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/maxrWithFailure.gold b/SBVTestSuite/GoldFiles/maxrWithFailure.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/maxrWithFailure.gold @@ -0,0 +1,231 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s3 () Int 0) +[GOOD] (define-fun s9 () Int 1) +[GOOD] (define-fun s142 () Int 10) +[GOOD] (define-fun s1 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "ints" +[GOOD] (declare-fun s4 () Int) ; tracks user variable "__internal_sbv_s4" +[GOOD] (declare-fun s16 () Int) ; tracks user variable "__internal_sbv_s16" +[GOOD] (declare-fun s27 () Int) ; tracks user variable "__internal_sbv_s27" +[GOOD] (declare-fun s38 () Int) ; tracks user variable "__internal_sbv_s38" +[GOOD] (declare-fun s49 () Int) ; tracks user variable "__internal_sbv_s49" +[GOOD] (declare-fun s60 () Int) ; tracks user variable "__internal_sbv_s60" +[GOOD] (declare-fun s71 () Int) ; tracks user variable "__internal_sbv_s71" +[GOOD] (declare-fun s82 () Int) ; tracks user variable "__internal_sbv_s82" +[GOOD] (declare-fun s93 () Int) ; tracks user variable "__internal_sbv_s93" +[GOOD] (declare-fun s104 () Int) ; tracks user variable "__internal_sbv_s104" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s2 () Bool (= s0 s1)) +[GOOD] (define-fun s5 () (Seq Int) (seq.unit s4)) +[GOOD] (define-fun s6 () Int (seq.len s0)) +[GOOD] (define-fun s7 () Bool (> s6 s3)) +[GOOD] (define-fun s8 () Bool (not s7)) +[GOOD] (define-fun s10 () (Seq Int) (seq.extract s0 s3 s9)) +[GOOD] (define-fun s11 () Bool (= s5 s10)) +[GOOD] (define-fun s12 () Bool (or s8 s11)) +[GOOD] (define-fun s13 () Int (- s6 s9)) +[GOOD] (define-fun s14 () (Seq Int) (seq.extract s0 s9 s13)) +[GOOD] (define-fun s15 () Bool (= s1 s14)) +[GOOD] (define-fun s17 () (Seq Int) (seq.unit s16)) +[GOOD] (define-fun s18 () Int (seq.len s14)) +[GOOD] (define-fun s19 () Bool (> s18 s3)) +[GOOD] (define-fun s20 () Bool (not s19)) +[GOOD] (define-fun s21 () (Seq Int) (seq.extract s14 s3 s9)) +[GOOD] (define-fun s22 () Bool (= s17 s21)) +[GOOD] (define-fun s23 () Bool (or s20 s22)) +[GOOD] (define-fun s24 () Int (- s18 s9)) +[GOOD] (define-fun s25 () (Seq Int) (seq.extract s14 s9 s24)) +[GOOD] (define-fun s26 () Bool (= s1 s25)) +[GOOD] (define-fun s28 () (Seq Int) (seq.unit s27)) +[GOOD] (define-fun s29 () Int (seq.len s25)) +[GOOD] (define-fun s30 () Bool (> s29 s3)) +[GOOD] (define-fun s31 () Bool (not s30)) +[GOOD] (define-fun s32 () (Seq Int) (seq.extract s25 s3 s9)) +[GOOD] (define-fun s33 () Bool (= s28 s32)) +[GOOD] (define-fun s34 () Bool (or s31 s33)) +[GOOD] (define-fun s35 () Int (- s29 s9)) +[GOOD] (define-fun s36 () (Seq Int) (seq.extract s25 s9 s35)) +[GOOD] (define-fun s37 () Bool (= s1 s36)) +[GOOD] (define-fun s39 () (Seq Int) (seq.unit s38)) +[GOOD] (define-fun s40 () Int (seq.len s36)) +[GOOD] (define-fun s41 () Bool (> s40 s3)) +[GOOD] (define-fun s42 () Bool (not s41)) +[GOOD] (define-fun s43 () (Seq Int) (seq.extract s36 s3 s9)) +[GOOD] (define-fun s44 () Bool (= s39 s43)) +[GOOD] (define-fun s45 () Bool (or s42 s44)) +[GOOD] (define-fun s46 () Int (- s40 s9)) +[GOOD] (define-fun s47 () (Seq Int) (seq.extract s36 s9 s46)) +[GOOD] (define-fun s48 () Bool (= s1 s47)) +[GOOD] (define-fun s50 () (Seq Int) (seq.unit s49)) +[GOOD] (define-fun s51 () Int (seq.len s47)) +[GOOD] (define-fun s52 () Bool (> s51 s3)) +[GOOD] (define-fun s53 () Bool (not s52)) +[GOOD] (define-fun s54 () (Seq Int) (seq.extract s47 s3 s9)) +[GOOD] (define-fun s55 () Bool (= s50 s54)) +[GOOD] (define-fun s56 () Bool (or s53 s55)) +[GOOD] (define-fun s57 () Int (- s51 s9)) +[GOOD] (define-fun s58 () (Seq Int) (seq.extract s47 s9 s57)) +[GOOD] (define-fun s59 () Bool (= s1 s58)) +[GOOD] (define-fun s61 () (Seq Int) (seq.unit s60)) +[GOOD] (define-fun s62 () Int (seq.len s58)) +[GOOD] (define-fun s63 () Bool (> s62 s3)) +[GOOD] (define-fun s64 () Bool (not s63)) +[GOOD] (define-fun s65 () (Seq Int) (seq.extract s58 s3 s9)) +[GOOD] (define-fun s66 () Bool (= s61 s65)) +[GOOD] (define-fun s67 () Bool (or s64 s66)) +[GOOD] (define-fun s68 () Int (- s62 s9)) +[GOOD] (define-fun s69 () (Seq Int) (seq.extract s58 s9 s68)) +[GOOD] (define-fun s70 () Bool (= s1 s69)) +[GOOD] (define-fun s72 () (Seq Int) (seq.unit s71)) +[GOOD] (define-fun s73 () Int (seq.len s69)) +[GOOD] (define-fun s74 () Bool (> s73 s3)) +[GOOD] (define-fun s75 () Bool (not s74)) +[GOOD] (define-fun s76 () (Seq Int) (seq.extract s69 s3 s9)) +[GOOD] (define-fun s77 () Bool (= s72 s76)) +[GOOD] (define-fun s78 () Bool (or s75 s77)) +[GOOD] (define-fun s79 () Int (- s73 s9)) +[GOOD] (define-fun s80 () (Seq Int) (seq.extract s69 s9 s79)) +[GOOD] (define-fun s81 () Bool (= s1 s80)) +[GOOD] (define-fun s83 () (Seq Int) (seq.unit s82)) +[GOOD] (define-fun s84 () Int (seq.len s80)) +[GOOD] (define-fun s85 () Bool (> s84 s3)) +[GOOD] (define-fun s86 () Bool (not s85)) +[GOOD] (define-fun s87 () (Seq Int) (seq.extract s80 s3 s9)) +[GOOD] (define-fun s88 () Bool (= s83 s87)) +[GOOD] (define-fun s89 () Bool (or s86 s88)) +[GOOD] (define-fun s90 () Int (- s84 s9)) +[GOOD] (define-fun s91 () (Seq Int) (seq.extract s80 s9 s90)) +[GOOD] (define-fun s92 () Bool (= s1 s91)) +[GOOD] (define-fun s94 () (Seq Int) (seq.unit s93)) +[GOOD] (define-fun s95 () Int (seq.len s91)) +[GOOD] (define-fun s96 () Bool (> s95 s3)) +[GOOD] (define-fun s97 () Bool (not s96)) +[GOOD] (define-fun s98 () (Seq Int) (seq.extract s91 s3 s9)) +[GOOD] (define-fun s99 () Bool (= s94 s98)) +[GOOD] (define-fun s100 () Bool (or s97 s99)) +[GOOD] (define-fun s101 () Int (- s95 s9)) +[GOOD] (define-fun s102 () (Seq Int) (seq.extract s91 s9 s101)) +[GOOD] (define-fun s103 () Bool (= s1 s102)) +[GOOD] (define-fun s105 () (Seq Int) (seq.unit s104)) +[GOOD] (define-fun s106 () Int (seq.len s102)) +[GOOD] (define-fun s107 () Bool (> s106 s3)) +[GOOD] (define-fun s108 () Bool (not s107)) +[GOOD] (define-fun s109 () (Seq Int) (seq.extract s102 s3 s9)) +[GOOD] (define-fun s110 () Bool (= s105 s109)) +[GOOD] (define-fun s111 () Bool (or s108 s110)) +[GOOD] (define-fun s112 () Bool (<= s104 s3)) +[GOOD] (define-fun s113 () Int (ite s112 s3 s104)) +[GOOD] (define-fun s114 () Int (ite s103 s3 s113)) +[GOOD] (define-fun s115 () Bool (<= s93 s114)) +[GOOD] (define-fun s116 () Int (ite s115 s114 s93)) +[GOOD] (define-fun s117 () Int (ite s92 s3 s116)) +[GOOD] (define-fun s118 () Bool (<= s82 s117)) +[GOOD] (define-fun s119 () Int (ite s118 s117 s82)) +[GOOD] (define-fun s120 () Int (ite s81 s3 s119)) +[GOOD] (define-fun s121 () Bool (<= s71 s120)) +[GOOD] (define-fun s122 () Int (ite s121 s120 s71)) +[GOOD] (define-fun s123 () Int (ite s70 s3 s122)) +[GOOD] (define-fun s124 () Bool (<= s60 s123)) +[GOOD] (define-fun s125 () Int (ite s124 s123 s60)) +[GOOD] (define-fun s126 () Int (ite s59 s3 s125)) +[GOOD] (define-fun s127 () Bool (<= s49 s126)) +[GOOD] (define-fun s128 () Int (ite s127 s126 s49)) +[GOOD] (define-fun s129 () Int (ite s48 s3 s128)) +[GOOD] (define-fun s130 () Bool (<= s38 s129)) +[GOOD] (define-fun s131 () Int (ite s130 s129 s38)) +[GOOD] (define-fun s132 () Int (ite s37 s3 s131)) +[GOOD] (define-fun s133 () Bool (<= s27 s132)) +[GOOD] (define-fun s134 () Int (ite s133 s132 s27)) +[GOOD] (define-fun s135 () Int (ite s26 s3 s134)) +[GOOD] (define-fun s136 () Bool (<= s16 s135)) +[GOOD] (define-fun s137 () Int (ite s136 s135 s16)) +[GOOD] (define-fun s138 () Int (ite s15 s3 s137)) +[GOOD] (define-fun s139 () Bool (<= s4 s138)) +[GOOD] (define-fun s140 () Int (ite s139 s138 s4)) +[GOOD] (define-fun s141 () Int (ite s2 s3 s140)) +[GOOD] (define-fun s143 () Bool (> s141 s142)) +[GOOD] (define-fun s144 () Bool (not s143)) +[GOOD] (define-fun s145 () Bool (< s104 s3)) +[GOOD] (define-fun s146 () Bool (> s104 s142)) +[GOOD] (define-fun s147 () Bool (or s145 s146)) +[GOOD] (define-fun s148 () Bool (ite s103 s_2 s147)) +[GOOD] (define-fun s149 () Bool (< s93 s3)) +[GOOD] (define-fun s150 () Bool (> s93 s142)) +[GOOD] (define-fun s151 () Bool (or s149 s150)) +[GOOD] (define-fun s152 () Bool (or s148 s151)) +[GOOD] (define-fun s153 () Bool (ite s92 s_2 s152)) +[GOOD] (define-fun s154 () Bool (< s82 s3)) +[GOOD] (define-fun s155 () Bool (> s82 s142)) +[GOOD] (define-fun s156 () Bool (or s154 s155)) +[GOOD] (define-fun s157 () Bool (or s153 s156)) +[GOOD] (define-fun s158 () Bool (ite s81 s_2 s157)) +[GOOD] (define-fun s159 () Bool (< s71 s3)) +[GOOD] (define-fun s160 () Bool (> s71 s142)) +[GOOD] (define-fun s161 () Bool (or s159 s160)) +[GOOD] (define-fun s162 () Bool (or s158 s161)) +[GOOD] (define-fun s163 () Bool (ite s70 s_2 s162)) +[GOOD] (define-fun s164 () Bool (< s60 s3)) +[GOOD] (define-fun s165 () Bool (> s60 s142)) +[GOOD] (define-fun s166 () Bool (or s164 s165)) +[GOOD] (define-fun s167 () Bool (or s163 s166)) +[GOOD] (define-fun s168 () Bool (ite s59 s_2 s167)) +[GOOD] (define-fun s169 () Bool (< s49 s3)) +[GOOD] (define-fun s170 () Bool (> s49 s142)) +[GOOD] (define-fun s171 () Bool (or s169 s170)) +[GOOD] (define-fun s172 () Bool (or s168 s171)) +[GOOD] (define-fun s173 () Bool (ite s48 s_2 s172)) +[GOOD] (define-fun s174 () Bool (< s38 s3)) +[GOOD] (define-fun s175 () Bool (> s38 s142)) +[GOOD] (define-fun s176 () Bool (or s174 s175)) +[GOOD] (define-fun s177 () Bool (or s173 s176)) +[GOOD] (define-fun s178 () Bool (ite s37 s_2 s177)) +[GOOD] (define-fun s179 () Bool (< s27 s3)) +[GOOD] (define-fun s180 () Bool (> s27 s142)) +[GOOD] (define-fun s181 () Bool (or s179 s180)) +[GOOD] (define-fun s182 () Bool (or s178 s181)) +[GOOD] (define-fun s183 () Bool (ite s26 s_2 s182)) +[GOOD] (define-fun s184 () Bool (< s16 s3)) +[GOOD] (define-fun s185 () Bool (> s16 s142)) +[GOOD] (define-fun s186 () Bool (or s184 s185)) +[GOOD] (define-fun s187 () Bool (or s183 s186)) +[GOOD] (define-fun s188 () Bool (ite s15 s_2 s187)) +[GOOD] (define-fun s189 () Bool (< s4 s3)) +[GOOD] (define-fun s190 () Bool (> s4 s142)) +[GOOD] (define-fun s191 () Bool (or s189 s190)) +[GOOD] (define-fun s192 () Bool (or s188 s191)) +[GOOD] (define-fun s193 () Bool (ite s2 s_2 s192)) +[GOOD] (define-fun s194 () Bool (or s144 s193)) +[GOOD] (assert s12) +[GOOD] (assert s23) +[GOOD] (assert s34) +[GOOD] (assert s45) +[GOOD] (assert s56) +[GOOD] (assert s67) +[GOOD] (assert s78) +[GOOD] (assert s89) +[GOOD] (assert s100) +[GOOD] (assert s111) +[GOOD] (assert s194) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -76,7 +76,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.0") +[RECV] (:version "4.8.4") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4) @@ -107,7 +107,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version) -[RECV] (:version "4.8.0") +[RECV] (:version "4.8.4") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) diff --git a/SBVTestSuite/GoldFiles/reverse.gold b/SBVTestSuite/GoldFiles/reverse.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/reverse.gold @@ -0,0 +1,181 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s13 () Int 1) +[GOOD] (define-fun s53 () Int 0) +[GOOD] (define-fun s11 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" +[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" +[GOOD] (declare-fun s3 () Int) ; tracks user variable "d" +[GOOD] (declare-fun s50 () Int) ; tracks user variable "__internal_sbv_s50" +[GOOD] (declare-fun s60 () Int) ; tracks user variable "__internal_sbv_s60" +[GOOD] (declare-fun s69 () Int) ; tracks user variable "__internal_sbv_s69" +[GOOD] (declare-fun s78 () Int) ; tracks user variable "__internal_sbv_s78" +[GOOD] (declare-fun s87 () Int) ; tracks user variable "__internal_sbv_s87" +[GOOD] (declare-fun s96 () Int) ; tracks user variable "__internal_sbv_s96" +[GOOD] (declare-fun s105 () Int) ; tracks user variable "__internal_sbv_s105" +[GOOD] (declare-fun s114 () Int) ; tracks user variable "__internal_sbv_s114" +[GOOD] (declare-fun s123 () Int) ; tracks user variable "__internal_sbv_s123" +[GOOD] (declare-fun s132 () Int) ; tracks user variable "__internal_sbv_s132" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s4 () (Seq Int) (seq.unit s0)) +[GOOD] (define-fun s5 () (Seq Int) (seq.unit s1)) +[GOOD] (define-fun s6 () (Seq Int) (seq.unit s2)) +[GOOD] (define-fun s7 () (Seq Int) (seq.unit s3)) +[GOOD] (define-fun s8 () (Seq Int) (seq.++ s6 s7)) +[GOOD] (define-fun s9 () (Seq Int) (seq.++ s5 s8)) +[GOOD] (define-fun s10 () (Seq Int) (seq.++ s4 s9)) +[GOOD] (define-fun s12 () Bool (= s10 s11)) +[GOOD] (define-fun s14 () Int (seq.len s10)) +[GOOD] (define-fun s15 () Int (- s14 s13)) +[GOOD] (define-fun s16 () (Seq Int) (seq.extract s10 s13 s15)) +[GOOD] (define-fun s17 () Bool (= s11 s16)) +[GOOD] (define-fun s18 () Int (seq.len s16)) +[GOOD] (define-fun s19 () Int (- s18 s13)) +[GOOD] (define-fun s20 () (Seq Int) (seq.extract s16 s13 s19)) +[GOOD] (define-fun s21 () Bool (= s11 s20)) +[GOOD] (define-fun s22 () Int (seq.len s20)) +[GOOD] (define-fun s23 () Int (- s22 s13)) +[GOOD] (define-fun s24 () (Seq Int) (seq.extract s20 s13 s23)) +[GOOD] (define-fun s25 () Bool (= s11 s24)) +[GOOD] (define-fun s26 () Int (seq.len s24)) +[GOOD] (define-fun s27 () Int (- s26 s13)) +[GOOD] (define-fun s28 () (Seq Int) (seq.extract s24 s13 s27)) +[GOOD] (define-fun s29 () Bool (= s11 s28)) +[GOOD] (define-fun s30 () Int (seq.len s28)) +[GOOD] (define-fun s31 () Int (- s30 s13)) +[GOOD] (define-fun s32 () (Seq Int) (seq.extract s28 s13 s31)) +[GOOD] (define-fun s33 () Bool (= s11 s32)) +[GOOD] (define-fun s34 () Int (seq.len s32)) +[GOOD] (define-fun s35 () Int (- s34 s13)) +[GOOD] (define-fun s36 () (Seq Int) (seq.extract s32 s13 s35)) +[GOOD] (define-fun s37 () Bool (= s11 s36)) +[GOOD] (define-fun s38 () Int (seq.len s36)) +[GOOD] (define-fun s39 () Int (- s38 s13)) +[GOOD] (define-fun s40 () (Seq Int) (seq.extract s36 s13 s39)) +[GOOD] (define-fun s41 () Bool (= s11 s40)) +[GOOD] (define-fun s42 () Int (seq.len s40)) +[GOOD] (define-fun s43 () Int (- s42 s13)) +[GOOD] (define-fun s44 () (Seq Int) (seq.extract s40 s13 s43)) +[GOOD] (define-fun s45 () Bool (= s11 s44)) +[GOOD] (define-fun s46 () Int (seq.len s44)) +[GOOD] (define-fun s47 () Int (- s46 s13)) +[GOOD] (define-fun s48 () (Seq Int) (seq.extract s44 s13 s47)) +[GOOD] (define-fun s49 () Bool (= s11 s48)) +[GOOD] (define-fun s51 () (Seq Int) (seq.unit s50)) +[GOOD] (define-fun s52 () Int (seq.len s48)) +[GOOD] (define-fun s54 () Bool (> s52 s53)) +[GOOD] (define-fun s55 () Bool (not s54)) +[GOOD] (define-fun s56 () (Seq Int) (seq.extract s48 s53 s13)) +[GOOD] (define-fun s57 () Bool (= s51 s56)) +[GOOD] (define-fun s58 () Bool (or s55 s57)) +[GOOD] (define-fun s59 () (Seq Int) (ite s49 s11 s51)) +[GOOD] (define-fun s61 () (Seq Int) (seq.unit s60)) +[GOOD] (define-fun s62 () Bool (> s46 s53)) +[GOOD] (define-fun s63 () Bool (not s62)) +[GOOD] (define-fun s64 () (Seq Int) (seq.extract s44 s53 s13)) +[GOOD] (define-fun s65 () Bool (= s61 s64)) +[GOOD] (define-fun s66 () Bool (or s63 s65)) +[GOOD] (define-fun s67 () (Seq Int) (seq.++ s59 s61)) +[GOOD] (define-fun s68 () (Seq Int) (ite s45 s11 s67)) +[GOOD] (define-fun s70 () (Seq Int) (seq.unit s69)) +[GOOD] (define-fun s71 () Bool (> s42 s53)) +[GOOD] (define-fun s72 () Bool (not s71)) +[GOOD] (define-fun s73 () (Seq Int) (seq.extract s40 s53 s13)) +[GOOD] (define-fun s74 () Bool (= s70 s73)) +[GOOD] (define-fun s75 () Bool (or s72 s74)) +[GOOD] (define-fun s76 () (Seq Int) (seq.++ s68 s70)) +[GOOD] (define-fun s77 () (Seq Int) (ite s41 s11 s76)) +[GOOD] (define-fun s79 () (Seq Int) (seq.unit s78)) +[GOOD] (define-fun s80 () Bool (> s38 s53)) +[GOOD] (define-fun s81 () Bool (not s80)) +[GOOD] (define-fun s82 () (Seq Int) (seq.extract s36 s53 s13)) +[GOOD] (define-fun s83 () Bool (= s79 s82)) +[GOOD] (define-fun s84 () Bool (or s81 s83)) +[GOOD] (define-fun s85 () (Seq Int) (seq.++ s77 s79)) +[GOOD] (define-fun s86 () (Seq Int) (ite s37 s11 s85)) +[GOOD] (define-fun s88 () (Seq Int) (seq.unit s87)) +[GOOD] (define-fun s89 () Bool (> s34 s53)) +[GOOD] (define-fun s90 () Bool (not s89)) +[GOOD] (define-fun s91 () (Seq Int) (seq.extract s32 s53 s13)) +[GOOD] (define-fun s92 () Bool (= s88 s91)) +[GOOD] (define-fun s93 () Bool (or s90 s92)) +[GOOD] (define-fun s94 () (Seq Int) (seq.++ s86 s88)) +[GOOD] (define-fun s95 () (Seq Int) (ite s33 s11 s94)) +[GOOD] (define-fun s97 () (Seq Int) (seq.unit s96)) +[GOOD] (define-fun s98 () Bool (> s30 s53)) +[GOOD] (define-fun s99 () Bool (not s98)) +[GOOD] (define-fun s100 () (Seq Int) (seq.extract s28 s53 s13)) +[GOOD] (define-fun s101 () Bool (= s97 s100)) +[GOOD] (define-fun s102 () Bool (or s99 s101)) +[GOOD] (define-fun s103 () (Seq Int) (seq.++ s95 s97)) +[GOOD] (define-fun s104 () (Seq Int) (ite s29 s11 s103)) +[GOOD] (define-fun s106 () (Seq Int) (seq.unit s105)) +[GOOD] (define-fun s107 () Bool (> s26 s53)) +[GOOD] (define-fun s108 () Bool (not s107)) +[GOOD] (define-fun s109 () (Seq Int) (seq.extract s24 s53 s13)) +[GOOD] (define-fun s110 () Bool (= s106 s109)) +[GOOD] (define-fun s111 () Bool (or s108 s110)) +[GOOD] (define-fun s112 () (Seq Int) (seq.++ s104 s106)) +[GOOD] (define-fun s113 () (Seq Int) (ite s25 s11 s112)) +[GOOD] (define-fun s115 () (Seq Int) (seq.unit s114)) +[GOOD] (define-fun s116 () Bool (> s22 s53)) +[GOOD] (define-fun s117 () Bool (not s116)) +[GOOD] (define-fun s118 () (Seq Int) (seq.extract s20 s53 s13)) +[GOOD] (define-fun s119 () Bool (= s115 s118)) +[GOOD] (define-fun s120 () Bool (or s117 s119)) +[GOOD] (define-fun s121 () (Seq Int) (seq.++ s113 s115)) +[GOOD] (define-fun s122 () (Seq Int) (ite s21 s11 s121)) +[GOOD] (define-fun s124 () (Seq Int) (seq.unit s123)) +[GOOD] (define-fun s125 () Bool (> s18 s53)) +[GOOD] (define-fun s126 () Bool (not s125)) +[GOOD] (define-fun s127 () (Seq Int) (seq.extract s16 s53 s13)) +[GOOD] (define-fun s128 () Bool (= s124 s127)) +[GOOD] (define-fun s129 () Bool (or s126 s128)) +[GOOD] (define-fun s130 () (Seq Int) (seq.++ s122 s124)) +[GOOD] (define-fun s131 () (Seq Int) (ite s17 s11 s130)) +[GOOD] (define-fun s133 () (Seq Int) (seq.unit s132)) +[GOOD] (define-fun s134 () Bool (> s14 s53)) +[GOOD] (define-fun s135 () Bool (not s134)) +[GOOD] (define-fun s136 () (Seq Int) (seq.extract s10 s53 s13)) +[GOOD] (define-fun s137 () Bool (= s133 s136)) +[GOOD] (define-fun s138 () Bool (or s135 s137)) +[GOOD] (define-fun s139 () (Seq Int) (seq.++ s131 s133)) +[GOOD] (define-fun s140 () (Seq Int) (ite s12 s11 s139)) +[GOOD] (define-fun s141 () (Seq Int) (seq.++ s5 s4)) +[GOOD] (define-fun s142 () (Seq Int) (seq.++ s6 s141)) +[GOOD] (define-fun s143 () (Seq Int) (seq.++ s7 s142)) +[GOOD] (define-fun s144 () Bool (= s140 s143)) +[GOOD] (assert s58) +[GOOD] (assert s66) +[GOOD] (assert s75) +[GOOD] (assert s84) +[GOOD] (assert s93) +[GOOD] (assert s102) +[GOOD] (assert s111) +[GOOD] (assert s120) +[GOOD] (assert s129) +[GOOD] (assert s138) +[GOOD] (assert s144) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/reverseAlt10.gold b/SBVTestSuite/GoldFiles/reverseAlt10.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/reverseAlt10.gold @@ -0,0 +1,237 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s3 () Int 1) +[GOOD] (define-fun s43 () Int 0) +[GOOD] (define-fun s1 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "xs" +[GOOD] (declare-fun s40 () Int) ; tracks user variable "__internal_sbv_s40" +[GOOD] (declare-fun s50 () Int) ; tracks user variable "__internal_sbv_s50" +[GOOD] (declare-fun s59 () Int) ; tracks user variable "__internal_sbv_s59" +[GOOD] (declare-fun s68 () Int) ; tracks user variable "__internal_sbv_s68" +[GOOD] (declare-fun s77 () Int) ; tracks user variable "__internal_sbv_s77" +[GOOD] (declare-fun s86 () Int) ; tracks user variable "__internal_sbv_s86" +[GOOD] (declare-fun s95 () Int) ; tracks user variable "__internal_sbv_s95" +[GOOD] (declare-fun s104 () Int) ; tracks user variable "__internal_sbv_s104" +[GOOD] (declare-fun s113 () Int) ; tracks user variable "__internal_sbv_s113" +[GOOD] (declare-fun s122 () Int) ; tracks user variable "__internal_sbv_s122" +[GOOD] (declare-fun s131 () Int) ; tracks user variable "__internal_sbv_s131" +[GOOD] (declare-fun s135 () Int) ; tracks user variable "__internal_sbv_s135" +[GOOD] (declare-fun s140 () Int) ; tracks user variable "__internal_sbv_s140" +[GOOD] (declare-fun s145 () Int) ; tracks user variable "__internal_sbv_s145" +[GOOD] (declare-fun s150 () Int) ; tracks user variable "__internal_sbv_s150" +[GOOD] (declare-fun s155 () Int) ; tracks user variable "__internal_sbv_s155" +[GOOD] (declare-fun s160 () Int) ; tracks user variable "__internal_sbv_s160" +[GOOD] (declare-fun s165 () Int) ; tracks user variable "__internal_sbv_s165" +[GOOD] (declare-fun s170 () Int) ; tracks user variable "__internal_sbv_s170" +[GOOD] (declare-fun s175 () Int) ; tracks user variable "__internal_sbv_s175" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s2 () Bool (= s0 s1)) +[GOOD] (define-fun s4 () Int (seq.len s0)) +[GOOD] (define-fun s5 () Int (- s4 s3)) +[GOOD] (define-fun s6 () (Seq Int) (seq.extract s0 s3 s5)) +[GOOD] (define-fun s7 () Bool (= s1 s6)) +[GOOD] (define-fun s8 () Int (seq.len s6)) +[GOOD] (define-fun s9 () Int (- s8 s3)) +[GOOD] (define-fun s10 () (Seq Int) (seq.extract s6 s3 s9)) +[GOOD] (define-fun s11 () Bool (= s1 s10)) +[GOOD] (define-fun s12 () Int (seq.len s10)) +[GOOD] (define-fun s13 () Int (- s12 s3)) +[GOOD] (define-fun s14 () (Seq Int) (seq.extract s10 s3 s13)) +[GOOD] (define-fun s15 () Bool (= s1 s14)) +[GOOD] (define-fun s16 () Int (seq.len s14)) +[GOOD] (define-fun s17 () Int (- s16 s3)) +[GOOD] (define-fun s18 () (Seq Int) (seq.extract s14 s3 s17)) +[GOOD] (define-fun s19 () Bool (= s1 s18)) +[GOOD] (define-fun s20 () Int (seq.len s18)) +[GOOD] (define-fun s21 () Int (- s20 s3)) +[GOOD] (define-fun s22 () (Seq Int) (seq.extract s18 s3 s21)) +[GOOD] (define-fun s23 () Bool (= s1 s22)) +[GOOD] (define-fun s24 () Int (seq.len s22)) +[GOOD] (define-fun s25 () Int (- s24 s3)) +[GOOD] (define-fun s26 () (Seq Int) (seq.extract s22 s3 s25)) +[GOOD] (define-fun s27 () Bool (= s1 s26)) +[GOOD] (define-fun s28 () Int (seq.len s26)) +[GOOD] (define-fun s29 () Int (- s28 s3)) +[GOOD] (define-fun s30 () (Seq Int) (seq.extract s26 s3 s29)) +[GOOD] (define-fun s31 () Bool (= s1 s30)) +[GOOD] (define-fun s32 () Int (seq.len s30)) +[GOOD] (define-fun s33 () Int (- s32 s3)) +[GOOD] (define-fun s34 () (Seq Int) (seq.extract s30 s3 s33)) +[GOOD] (define-fun s35 () Bool (= s1 s34)) +[GOOD] (define-fun s36 () Int (seq.len s34)) +[GOOD] (define-fun s37 () Int (- s36 s3)) +[GOOD] (define-fun s38 () (Seq Int) (seq.extract s34 s3 s37)) +[GOOD] (define-fun s39 () Bool (= s1 s38)) +[GOOD] (define-fun s41 () (Seq Int) (seq.unit s40)) +[GOOD] (define-fun s42 () Int (seq.len s38)) +[GOOD] (define-fun s44 () Bool (> s42 s43)) +[GOOD] (define-fun s45 () Bool (not s44)) +[GOOD] (define-fun s46 () (Seq Int) (seq.extract s38 s43 s3)) +[GOOD] (define-fun s47 () Bool (= s41 s46)) +[GOOD] (define-fun s48 () Bool (or s45 s47)) +[GOOD] (define-fun s49 () (Seq Int) (ite s39 s1 s41)) +[GOOD] (define-fun s51 () (Seq Int) (seq.unit s50)) +[GOOD] (define-fun s52 () Bool (> s36 s43)) +[GOOD] (define-fun s53 () Bool (not s52)) +[GOOD] (define-fun s54 () (Seq Int) (seq.extract s34 s43 s3)) +[GOOD] (define-fun s55 () Bool (= s51 s54)) +[GOOD] (define-fun s56 () Bool (or s53 s55)) +[GOOD] (define-fun s57 () (Seq Int) (seq.++ s49 s51)) +[GOOD] (define-fun s58 () (Seq Int) (ite s35 s1 s57)) +[GOOD] (define-fun s60 () (Seq Int) (seq.unit s59)) +[GOOD] (define-fun s61 () Bool (> s32 s43)) +[GOOD] (define-fun s62 () Bool (not s61)) +[GOOD] (define-fun s63 () (Seq Int) (seq.extract s30 s43 s3)) +[GOOD] (define-fun s64 () Bool (= s60 s63)) +[GOOD] (define-fun s65 () Bool (or s62 s64)) +[GOOD] (define-fun s66 () (Seq Int) (seq.++ s58 s60)) +[GOOD] (define-fun s67 () (Seq Int) (ite s31 s1 s66)) +[GOOD] (define-fun s69 () (Seq Int) (seq.unit s68)) +[GOOD] (define-fun s70 () Bool (> s28 s43)) +[GOOD] (define-fun s71 () Bool (not s70)) +[GOOD] (define-fun s72 () (Seq Int) (seq.extract s26 s43 s3)) +[GOOD] (define-fun s73 () Bool (= s69 s72)) +[GOOD] (define-fun s74 () Bool (or s71 s73)) +[GOOD] (define-fun s75 () (Seq Int) (seq.++ s67 s69)) +[GOOD] (define-fun s76 () (Seq Int) (ite s27 s1 s75)) +[GOOD] (define-fun s78 () (Seq Int) (seq.unit s77)) +[GOOD] (define-fun s79 () Bool (> s24 s43)) +[GOOD] (define-fun s80 () Bool (not s79)) +[GOOD] (define-fun s81 () (Seq Int) (seq.extract s22 s43 s3)) +[GOOD] (define-fun s82 () Bool (= s78 s81)) +[GOOD] (define-fun s83 () Bool (or s80 s82)) +[GOOD] (define-fun s84 () (Seq Int) (seq.++ s76 s78)) +[GOOD] (define-fun s85 () (Seq Int) (ite s23 s1 s84)) +[GOOD] (define-fun s87 () (Seq Int) (seq.unit s86)) +[GOOD] (define-fun s88 () Bool (> s20 s43)) +[GOOD] (define-fun s89 () Bool (not s88)) +[GOOD] (define-fun s90 () (Seq Int) (seq.extract s18 s43 s3)) +[GOOD] (define-fun s91 () Bool (= s87 s90)) +[GOOD] (define-fun s92 () Bool (or s89 s91)) +[GOOD] (define-fun s93 () (Seq Int) (seq.++ s85 s87)) +[GOOD] (define-fun s94 () (Seq Int) (ite s19 s1 s93)) +[GOOD] (define-fun s96 () (Seq Int) (seq.unit s95)) +[GOOD] (define-fun s97 () Bool (> s16 s43)) +[GOOD] (define-fun s98 () Bool (not s97)) +[GOOD] (define-fun s99 () (Seq Int) (seq.extract s14 s43 s3)) +[GOOD] (define-fun s100 () Bool (= s96 s99)) +[GOOD] (define-fun s101 () Bool (or s98 s100)) +[GOOD] (define-fun s102 () (Seq Int) (seq.++ s94 s96)) +[GOOD] (define-fun s103 () (Seq Int) (ite s15 s1 s102)) +[GOOD] (define-fun s105 () (Seq Int) (seq.unit s104)) +[GOOD] (define-fun s106 () Bool (> s12 s43)) +[GOOD] (define-fun s107 () Bool (not s106)) +[GOOD] (define-fun s108 () (Seq Int) (seq.extract s10 s43 s3)) +[GOOD] (define-fun s109 () Bool (= s105 s108)) +[GOOD] (define-fun s110 () Bool (or s107 s109)) +[GOOD] (define-fun s111 () (Seq Int) (seq.++ s103 s105)) +[GOOD] (define-fun s112 () (Seq Int) (ite s11 s1 s111)) +[GOOD] (define-fun s114 () (Seq Int) (seq.unit s113)) +[GOOD] (define-fun s115 () Bool (> s8 s43)) +[GOOD] (define-fun s116 () Bool (not s115)) +[GOOD] (define-fun s117 () (Seq Int) (seq.extract s6 s43 s3)) +[GOOD] (define-fun s118 () Bool (= s114 s117)) +[GOOD] (define-fun s119 () Bool (or s116 s118)) +[GOOD] (define-fun s120 () (Seq Int) (seq.++ s112 s114)) +[GOOD] (define-fun s121 () (Seq Int) (ite s7 s1 s120)) +[GOOD] (define-fun s123 () (Seq Int) (seq.unit s122)) +[GOOD] (define-fun s124 () Bool (> s4 s43)) +[GOOD] (define-fun s125 () Bool (not s124)) +[GOOD] (define-fun s126 () (Seq Int) (seq.extract s0 s43 s3)) +[GOOD] (define-fun s127 () Bool (= s123 s126)) +[GOOD] (define-fun s128 () Bool (or s125 s127)) +[GOOD] (define-fun s129 () (Seq Int) (seq.++ s121 s123)) +[GOOD] (define-fun s130 () (Seq Int) (ite s2 s1 s129)) +[GOOD] (define-fun s132 () (Seq Int) (seq.unit s131)) +[GOOD] (define-fun s133 () Bool (= s126 s132)) +[GOOD] (define-fun s134 () Bool (or s125 s133)) +[GOOD] (define-fun s136 () (Seq Int) (seq.unit s135)) +[GOOD] (define-fun s137 () Bool (= s117 s136)) +[GOOD] (define-fun s138 () Bool (or s116 s137)) +[GOOD] (define-fun s139 () (Seq Int) (seq.++ s136 s132)) +[GOOD] (define-fun s141 () (Seq Int) (seq.unit s140)) +[GOOD] (define-fun s142 () Bool (= s108 s141)) +[GOOD] (define-fun s143 () Bool (or s107 s142)) +[GOOD] (define-fun s144 () (Seq Int) (seq.++ s141 s139)) +[GOOD] (define-fun s146 () (Seq Int) (seq.unit s145)) +[GOOD] (define-fun s147 () Bool (= s99 s146)) +[GOOD] (define-fun s148 () Bool (or s98 s147)) +[GOOD] (define-fun s149 () (Seq Int) (seq.++ s146 s144)) +[GOOD] (define-fun s151 () (Seq Int) (seq.unit s150)) +[GOOD] (define-fun s152 () Bool (= s90 s151)) +[GOOD] (define-fun s153 () Bool (or s89 s152)) +[GOOD] (define-fun s154 () (Seq Int) (seq.++ s151 s149)) +[GOOD] (define-fun s156 () (Seq Int) (seq.unit s155)) +[GOOD] (define-fun s157 () Bool (= s81 s156)) +[GOOD] (define-fun s158 () Bool (or s80 s157)) +[GOOD] (define-fun s159 () (Seq Int) (seq.++ s156 s154)) +[GOOD] (define-fun s161 () (Seq Int) (seq.unit s160)) +[GOOD] (define-fun s162 () Bool (= s72 s161)) +[GOOD] (define-fun s163 () Bool (or s71 s162)) +[GOOD] (define-fun s164 () (Seq Int) (seq.++ s161 s159)) +[GOOD] (define-fun s166 () (Seq Int) (seq.unit s165)) +[GOOD] (define-fun s167 () Bool (= s63 s166)) +[GOOD] (define-fun s168 () Bool (or s62 s167)) +[GOOD] (define-fun s169 () (Seq Int) (seq.++ s166 s164)) +[GOOD] (define-fun s171 () (Seq Int) (seq.unit s170)) +[GOOD] (define-fun s172 () Bool (= s54 s171)) +[GOOD] (define-fun s173 () Bool (or s53 s172)) +[GOOD] (define-fun s174 () (Seq Int) (seq.++ s171 s169)) +[GOOD] (define-fun s176 () (Seq Int) (seq.unit s175)) +[GOOD] (define-fun s177 () Bool (= s46 s176)) +[GOOD] (define-fun s178 () Bool (or s45 s177)) +[GOOD] (define-fun s179 () (Seq Int) (seq.++ s176 s174)) +[GOOD] (define-fun s180 () (Seq Int) (ite s39 s174 s179)) +[GOOD] (define-fun s181 () (Seq Int) (ite s35 s169 s180)) +[GOOD] (define-fun s182 () (Seq Int) (ite s31 s164 s181)) +[GOOD] (define-fun s183 () (Seq Int) (ite s27 s159 s182)) +[GOOD] (define-fun s184 () (Seq Int) (ite s23 s154 s183)) +[GOOD] (define-fun s185 () (Seq Int) (ite s19 s149 s184)) +[GOOD] (define-fun s186 () (Seq Int) (ite s15 s144 s185)) +[GOOD] (define-fun s187 () (Seq Int) (ite s11 s139 s186)) +[GOOD] (define-fun s188 () (Seq Int) (ite s7 s132 s187)) +[GOOD] (define-fun s189 () (Seq Int) (ite s2 s1 s188)) +[GOOD] (define-fun s190 () Bool (distinct s130 s189)) +[GOOD] (assert s48) +[GOOD] (assert s56) +[GOOD] (assert s65) +[GOOD] (assert s74) +[GOOD] (assert s83) +[GOOD] (assert s92) +[GOOD] (assert s101) +[GOOD] (assert s110) +[GOOD] (assert s119) +[GOOD] (assert s128) +[GOOD] (assert s134) +[GOOD] (assert s138) +[GOOD] (assert s143) +[GOOD] (assert s148) +[GOOD] (assert s153) +[GOOD] (assert s158) +[GOOD] (assert s163) +[GOOD] (assert s168) +[GOOD] (assert s173) +[GOOD] (assert s178) +[GOOD] (assert s190) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/sort.gold b/SBVTestSuite/GoldFiles/sort.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/sort.gold @@ -0,0 +1,227 @@ +** 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-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s14 () Int 1) +[GOOD] (define-fun s26 () Int 0) +[GOOD] (define-fun s12 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" +[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" +[GOOD] (declare-fun s23 () Int) ; tracks user variable "__internal_sbv_s23" +[GOOD] (declare-fun s34 () Int) ; tracks user variable "__internal_sbv_s34" +[GOOD] (declare-fun s41 () Int) ; tracks user variable "__internal_sbv_s41" +[GOOD] (declare-fun s55 () Int) ; tracks user variable "__internal_sbv_s55" +[GOOD] (declare-fun s69 () Int) ; tracks user variable "__internal_sbv_s69" +[GOOD] (declare-fun s93 () Int) ; tracks user variable "__internal_sbv_s93" +[GOOD] (declare-fun s100 () Int) ; tracks user variable "__internal_sbv_s100" +[GOOD] (declare-fun s114 () Int) ; tracks user variable "__internal_sbv_s114" +[GOOD] (declare-fun s128 () Int) ; tracks user variable "__internal_sbv_s128" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s3 () Bool (<= s0 s1)) +[GOOD] (define-fun s4 () Bool (<= s1 s2)) +[GOOD] (define-fun s5 () Bool (and s3 s4)) +[GOOD] (define-fun s6 () Bool (not s5)) +[GOOD] (define-fun s7 () (Seq Int) (seq.unit s0)) +[GOOD] (define-fun s8 () (Seq Int) (seq.unit s1)) +[GOOD] (define-fun s9 () (Seq Int) (seq.unit s2)) +[GOOD] (define-fun s10 () (Seq Int) (seq.++ s8 s9)) +[GOOD] (define-fun s11 () (Seq Int) (seq.++ s7 s10)) +[GOOD] (define-fun s13 () Bool (= s11 s12)) +[GOOD] (define-fun s15 () Int (seq.len s11)) +[GOOD] (define-fun s16 () Int (- s15 s14)) +[GOOD] (define-fun s17 () (Seq Int) (seq.extract s11 s14 s16)) +[GOOD] (define-fun s18 () Bool (= s12 s17)) +[GOOD] (define-fun s19 () Int (seq.len s17)) +[GOOD] (define-fun s20 () Int (- s19 s14)) +[GOOD] (define-fun s21 () (Seq Int) (seq.extract s17 s14 s20)) +[GOOD] (define-fun s22 () Bool (= s12 s21)) +[GOOD] (define-fun s24 () (Seq Int) (seq.unit s23)) +[GOOD] (define-fun s25 () Int (seq.len s21)) +[GOOD] (define-fun s27 () Bool (> s25 s26)) +[GOOD] (define-fun s28 () Bool (not s27)) +[GOOD] (define-fun s29 () (Seq Int) (seq.extract s21 s26 s14)) +[GOOD] (define-fun s30 () Bool (= s24 s29)) +[GOOD] (define-fun s31 () Bool (or s28 s30)) +[GOOD] (define-fun s32 () (Seq Int) (ite s22 s12 s24)) +[GOOD] (define-fun s33 () Bool (= s12 s32)) +[GOOD] (define-fun s35 () (Seq Int) (seq.unit s34)) +[GOOD] (define-fun s36 () Bool (> s19 s26)) +[GOOD] (define-fun s37 () Bool (not s36)) +[GOOD] (define-fun s38 () (Seq Int) (seq.extract s17 s26 s14)) +[GOOD] (define-fun s39 () Bool (= s35 s38)) +[GOOD] (define-fun s40 () Bool (or s37 s39)) +[GOOD] (define-fun s42 () (Seq Int) (seq.unit s41)) +[GOOD] (define-fun s43 () Int (seq.len s32)) +[GOOD] (define-fun s44 () Bool (> s43 s26)) +[GOOD] (define-fun s45 () Bool (not s44)) +[GOOD] (define-fun s46 () (Seq Int) (seq.extract s32 s26 s14)) +[GOOD] (define-fun s47 () Bool (= s42 s46)) +[GOOD] (define-fun s48 () Bool (or s45 s47)) +[GOOD] (define-fun s49 () Bool (< s34 s41)) +[GOOD] (define-fun s50 () Int (- s43 s14)) +[GOOD] (define-fun s51 () (Seq Int) (seq.extract s32 s14 s50)) +[GOOD] (define-fun s52 () (Seq Int) (seq.++ s42 s51)) +[GOOD] (define-fun s53 () (Seq Int) (seq.++ s35 s52)) +[GOOD] (define-fun s54 () Bool (= s12 s51)) +[GOOD] (define-fun s56 () (Seq Int) (seq.unit s55)) +[GOOD] (define-fun s57 () Int (seq.len s51)) +[GOOD] (define-fun s58 () Bool (> s57 s26)) +[GOOD] (define-fun s59 () Bool (not s58)) +[GOOD] (define-fun s60 () (Seq Int) (seq.extract s51 s26 s14)) +[GOOD] (define-fun s61 () Bool (= s56 s60)) +[GOOD] (define-fun s62 () Bool (or s59 s61)) +[GOOD] (define-fun s63 () Bool (< s34 s55)) +[GOOD] (define-fun s64 () Int (- s57 s14)) +[GOOD] (define-fun s65 () (Seq Int) (seq.extract s51 s14 s64)) +[GOOD] (define-fun s66 () (Seq Int) (seq.++ s56 s65)) +[GOOD] (define-fun s67 () (Seq Int) (seq.++ s35 s66)) +[GOOD] (define-fun s68 () Bool (= s12 s65)) +[GOOD] (define-fun s70 () (Seq Int) (seq.unit s69)) +[GOOD] (define-fun s71 () Int (seq.len s65)) +[GOOD] (define-fun s72 () Bool (> s71 s26)) +[GOOD] (define-fun s73 () Bool (not s72)) +[GOOD] (define-fun s74 () (Seq Int) (seq.extract s65 s26 s14)) +[GOOD] (define-fun s75 () Bool (= s70 s74)) +[GOOD] (define-fun s76 () Bool (or s73 s75)) +[GOOD] (define-fun s77 () Bool (< s34 s69)) +[GOOD] (define-fun s78 () Int (- s71 s14)) +[GOOD] (define-fun s79 () (Seq Int) (seq.extract s65 s14 s78)) +[GOOD] (define-fun s80 () (Seq Int) (seq.++ s70 s79)) +[GOOD] (define-fun s81 () (Seq Int) (seq.++ s35 s80)) +[GOOD] (define-fun s82 () (Seq Int) (seq.++ s70 s35)) +[GOOD] (define-fun s83 () (Seq Int) (ite s77 s81 s82)) +[GOOD] (define-fun s84 () (Seq Int) (ite s68 s35 s83)) +[GOOD] (define-fun s85 () (Seq Int) (seq.++ s56 s84)) +[GOOD] (define-fun s86 () (Seq Int) (ite s63 s67 s85)) +[GOOD] (define-fun s87 () (Seq Int) (ite s54 s35 s86)) +[GOOD] (define-fun s88 () (Seq Int) (seq.++ s42 s87)) +[GOOD] (define-fun s89 () (Seq Int) (ite s49 s53 s88)) +[GOOD] (define-fun s90 () (Seq Int) (ite s33 s35 s89)) +[GOOD] (define-fun s91 () (Seq Int) (ite s18 s12 s90)) +[GOOD] (define-fun s92 () Bool (= s12 s91)) +[GOOD] (define-fun s94 () (Seq Int) (seq.unit s93)) +[GOOD] (define-fun s95 () Bool (> s15 s26)) +[GOOD] (define-fun s96 () Bool (not s95)) +[GOOD] (define-fun s97 () (Seq Int) (seq.extract s11 s26 s14)) +[GOOD] (define-fun s98 () Bool (= s94 s97)) +[GOOD] (define-fun s99 () Bool (or s96 s98)) +[GOOD] (define-fun s101 () (Seq Int) (seq.unit s100)) +[GOOD] (define-fun s102 () Int (seq.len s91)) +[GOOD] (define-fun s103 () Bool (> s102 s26)) +[GOOD] (define-fun s104 () Bool (not s103)) +[GOOD] (define-fun s105 () (Seq Int) (seq.extract s91 s26 s14)) +[GOOD] (define-fun s106 () Bool (= s101 s105)) +[GOOD] (define-fun s107 () Bool (or s104 s106)) +[GOOD] (define-fun s108 () Bool (< s93 s100)) +[GOOD] (define-fun s109 () Int (- s102 s14)) +[GOOD] (define-fun s110 () (Seq Int) (seq.extract s91 s14 s109)) +[GOOD] (define-fun s111 () (Seq Int) (seq.++ s101 s110)) +[GOOD] (define-fun s112 () (Seq Int) (seq.++ s94 s111)) +[GOOD] (define-fun s113 () Bool (= s12 s110)) +[GOOD] (define-fun s115 () (Seq Int) (seq.unit s114)) +[GOOD] (define-fun s116 () Int (seq.len s110)) +[GOOD] (define-fun s117 () Bool (> s116 s26)) +[GOOD] (define-fun s118 () Bool (not s117)) +[GOOD] (define-fun s119 () (Seq Int) (seq.extract s110 s26 s14)) +[GOOD] (define-fun s120 () Bool (= s115 s119)) +[GOOD] (define-fun s121 () Bool (or s118 s120)) +[GOOD] (define-fun s122 () Bool (< s93 s114)) +[GOOD] (define-fun s123 () Int (- s116 s14)) +[GOOD] (define-fun s124 () (Seq Int) (seq.extract s110 s14 s123)) +[GOOD] (define-fun s125 () (Seq Int) (seq.++ s115 s124)) +[GOOD] (define-fun s126 () (Seq Int) (seq.++ s94 s125)) +[GOOD] (define-fun s127 () Bool (= s12 s124)) +[GOOD] (define-fun s129 () (Seq Int) (seq.unit s128)) +[GOOD] (define-fun s130 () Int (seq.len s124)) +[GOOD] (define-fun s131 () Bool (> s130 s26)) +[GOOD] (define-fun s132 () Bool (not s131)) +[GOOD] (define-fun s133 () (Seq Int) (seq.extract s124 s26 s14)) +[GOOD] (define-fun s134 () Bool (= s129 s133)) +[GOOD] (define-fun s135 () Bool (or s132 s134)) +[GOOD] (define-fun s136 () Bool (< s93 s128)) +[GOOD] (define-fun s137 () Int (- s130 s14)) +[GOOD] (define-fun s138 () (Seq Int) (seq.extract s124 s14 s137)) +[GOOD] (define-fun s139 () (Seq Int) (seq.++ s129 s138)) +[GOOD] (define-fun s140 () (Seq Int) (seq.++ s94 s139)) +[GOOD] (define-fun s141 () (Seq Int) (seq.++ s129 s94)) +[GOOD] (define-fun s142 () (Seq Int) (ite s136 s140 s141)) +[GOOD] (define-fun s143 () (Seq Int) (ite s127 s94 s142)) +[GOOD] (define-fun s144 () (Seq Int) (seq.++ s115 s143)) +[GOOD] (define-fun s145 () (Seq Int) (ite s122 s126 s144)) +[GOOD] (define-fun s146 () (Seq Int) (ite s113 s94 s145)) +[GOOD] (define-fun s147 () (Seq Int) (seq.++ s101 s146)) +[GOOD] (define-fun s148 () (Seq Int) (ite s108 s112 s147)) +[GOOD] (define-fun s149 () (Seq Int) (ite s92 s94 s148)) +[GOOD] (define-fun s150 () (Seq Int) (ite s13 s12 s149)) +[GOOD] (define-fun s151 () Bool (= s11 s150)) +[GOOD] (define-fun s152 () Bool (or s6 s151)) +[GOOD] (define-fun s153 () Bool (<= s0 s2)) +[GOOD] (define-fun s154 () Bool (<= s2 s1)) +[GOOD] (define-fun s155 () Bool (and s153 s154)) +[GOOD] (define-fun s156 () Bool (not s155)) +[GOOD] (define-fun s157 () (Seq Int) (seq.++ s9 s8)) +[GOOD] (define-fun s158 () (Seq Int) (seq.++ s7 s157)) +[GOOD] (define-fun s159 () Bool (= s150 s158)) +[GOOD] (define-fun s160 () Bool (or s156 s159)) +[GOOD] (define-fun s161 () Bool (<= s1 s0)) +[GOOD] (define-fun s162 () Bool (and s153 s161)) +[GOOD] (define-fun s163 () Bool (not s162)) +[GOOD] (define-fun s164 () (Seq Int) (seq.++ s7 s9)) +[GOOD] (define-fun s165 () (Seq Int) (seq.++ s8 s164)) +[GOOD] (define-fun s166 () Bool (= s150 s165)) +[GOOD] (define-fun s167 () Bool (or s163 s166)) +[GOOD] (define-fun s168 () Bool (<= s2 s0)) +[GOOD] (define-fun s169 () Bool (and s4 s168)) +[GOOD] (define-fun s170 () Bool (not s169)) +[GOOD] (define-fun s171 () (Seq Int) (seq.++ s9 s7)) +[GOOD] (define-fun s172 () (Seq Int) (seq.++ s8 s171)) +[GOOD] (define-fun s173 () Bool (= s150 s172)) +[GOOD] (define-fun s174 () Bool (or s170 s173)) +[GOOD] (define-fun s175 () Bool (and s3 s168)) +[GOOD] (define-fun s176 () Bool (not s175)) +[GOOD] (define-fun s177 () (Seq Int) (seq.++ s7 s8)) +[GOOD] (define-fun s178 () (Seq Int) (seq.++ s9 s177)) +[GOOD] (define-fun s179 () Bool (= s150 s178)) +[GOOD] (define-fun s180 () Bool (or s176 s179)) +[GOOD] (define-fun s181 () Bool (and s154 s161)) +[GOOD] (define-fun s182 () Bool (not s181)) +[GOOD] (define-fun s183 () (Seq Int) (seq.++ s8 s7)) +[GOOD] (define-fun s184 () (Seq Int) (seq.++ s9 s183)) +[GOOD] (define-fun s185 () Bool (= s150 s184)) +[GOOD] (define-fun s186 () Bool (or s182 s185)) +[GOOD] (assert s31) +[GOOD] (assert s40) +[GOOD] (assert s48) +[GOOD] (assert s62) +[GOOD] (assert s76) +[GOOD] (assert s99) +[GOOD] (assert s107) +[GOOD] (assert s121) +[GOOD] (assert s135) +[GOOD] (assert s152) +[GOOD] (assert s160) +[GOOD] (assert s167) +[GOOD] (assert s174) +[GOOD] (assert s180) +[GOOD] (assert s186) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs --- a/SBVTestSuite/SBVTest.hs +++ b/SBVTestSuite/SBVTest.hs @@ -27,6 +27,7 @@ import qualified TestSuite.Basics.ArithSolver import qualified TestSuite.Basics.Assert import qualified TestSuite.Basics.BasicTests +import qualified TestSuite.Basics.BoundedList import qualified TestSuite.Basics.Exceptions import qualified TestSuite.Basics.GenBenchmark import qualified TestSuite.Basics.Higher @@ -160,6 +161,7 @@ , TestSuite.Basics.ArithNoSolver.tests , TestSuite.Basics.Assert.tests , TestSuite.Basics.BasicTests.tests + , TestSuite.Basics.BoundedList.tests , TestSuite.Basics.Exceptions.testsRemote , TestSuite.Basics.GenBenchmark.tests , TestSuite.Basics.Higher.tests diff --git a/SBVTestSuite/TestSuite/Basics/AllSat.hs b/SBVTestSuite/TestSuite/Basics/AllSat.hs --- a/SBVTestSuite/TestSuite/Basics/AllSat.hs +++ b/SBVTestSuite/TestSuite/Basics/AllSat.hs @@ -17,16 +17,21 @@ import Data.Generics import Utils.SBVTestFramework +import Data.List (sortOn) + tests :: TestTree tests = testGroup "Basics.AllSat" [ goldenVsStringShow "allSat1" t1 , goldenVsStringShow "allSat2" t2 - , goldenVsStringShow "allSat3" $ allSat $ \x -> x .== (0::SFloat) - , goldenVsStringShow "allSat4" $ allSat $ \x -> x .< (0::SWord8) - , goldenVsStringShow "allSat5" $ allSat $ \x y -> x .< y &&& y .< (4::SWord8) - , goldenVsStringShow "allSat6" $ allSat $ exists "x" >>= \x -> exists "y" >>= \y -> forall "z" >>= \z -> return (x .< (y::SWord8) &&& y .< 3 &&& z .== (z::SWord8)) + , goldenVsStringShow "allSat3" $ allSat $ \x -> x .== (0::SFloat) + , goldenVsStringShow "allSat4" $ allSat $ \x -> x .< (0::SWord8) + , goldenVsStringShow "allSat5" $ fmap srt $ allSat $ \x y -> x .< y &&& y .< (4::SWord8) + , goldenVsStringShow "allSat6" $ allSat $ exists "x" >>= \x -> exists "y" >>= \y -> forall "z" >>= \z -> return (x .< (y::SWord8) &&& y .< 3 &&& z .== (z::SWord8)) ] + +srt :: AllSatResult -> AllSatResult +srt (AllSatResult (b1, b2, rs)) = AllSatResult (b1, b2, sortOn getModelDictionary rs) newtype Q = Q () deriving (Eq, Ord, Data, Read, Show, SymWord, HasKind) type SQ = SBV Q diff --git a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs @@ -16,7 +16,7 @@ module TestSuite.Basics.ArithNoSolver(tests) where -import qualified Data.ReinterpretCast as RC (wordToFloat, wordToDouble, floatToWord, doubleToWord) +import qualified Data.Numbers.CrackNum as CN (wordToFloat, wordToDouble, floatToWord, doubleToWord) import Data.SBV.Internals import Utils.SBVTestFramework @@ -419,11 +419,11 @@ ++ map cvtTestI [("fromFP_Double_ToInteger", show x, (fromSDouble sRNE :: SDouble -> SInteger) (literal x), ((fromIntegral :: Integer -> SInteger) . fpRound0) x) | x <- ds] ++ map cvtTestI [("fromFP_Double_ToReal", show x, (fromSDouble sRNE :: SDouble -> SReal) (literal x), (fromRational . fpRatio0) x) | x <- ds] - ++ map cvtTest [("reinterp_Word32_Float", show x, sWord32AsSFloat (literal x), literal (RC.wordToFloat x)) | x <- w32s] - ++ map cvtTest [("reinterp_Word64_Double", show x, sWord64AsSDouble (literal x), literal (RC.wordToDouble x)) | x <- w64s] + ++ map cvtTest [("reinterp_Word32_Float", show x, sWord32AsSFloat (literal x), literal (CN.wordToFloat x)) | x <- w32s] + ++ map cvtTest [("reinterp_Word64_Double", show x, sWord64AsSDouble (literal x), literal (CN.wordToDouble x)) | x <- w64s] - ++ map cvtTestI [("reinterp_Float_Word32", show x, sFloatAsSWord32 (literal x), literal (RC.floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN - ++ map cvtTestI [("reinterp_Double_Word64", show x, sDoubleAsSWord64 (literal x), literal (RC.doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN + ++ map cvtTestI [("reinterp_Float_Word32", show x, sFloatAsSWord32 (literal x), literal (CN.floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN + ++ map cvtTestI [("reinterp_Double_Word64", show x, sDoubleAsSWord64 (literal x), literal (CN.doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN floatRun1 nm f g cmb = map (nm,) [cmb (x, f x, extract (g (literal x))) | x <- fs] doubleRun1 nm f g cmb = map (nm,) [cmb (x, f x, extract (g (literal x))) | x <- ds] diff --git a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs @@ -17,7 +17,7 @@ module TestSuite.Basics.ArithSolver(tests) where -import qualified Data.ReinterpretCast as RC (wordToFloat, wordToDouble, floatToWord, doubleToWord) +import qualified Data.Numbers.CrackNum as RC (wordToFloat, wordToDouble, floatToWord, doubleToWord) import Data.SBV.Internals import Utils.SBVTestFramework diff --git a/SBVTestSuite/TestSuite/Basics/BoundedList.hs b/SBVTestSuite/TestSuite/Basics/BoundedList.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Basics/BoundedList.hs @@ -0,0 +1,196 @@ +----------------------------------------------------------------------------- +-- | +-- Module : TestSuite.Basics.BoundedList +-- Copyright : (c) Joel Burget +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Test the bounded sequence/list functions. +----------------------------------------------------------------------------- + +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module TestSuite.Basics.BoundedList(tests) where + +import Data.SBV.Control +import Utils.SBVTestFramework + +import Data.SBV.List ((.:), (.!!)) +import qualified Data.SBV.List as L +import qualified Data.SBV.List.Bounded as BL + +import Control.Monad (unless) +import Control.Monad.State + +-- | Flag to mark a failed computation +newtype Failure = Failure SBool + deriving (Boolean, Mergeable, EqSymbolic) + +-- | Evaluation monad with failure +newtype Eval a = Eval { unEval :: State Failure a } + deriving (Functor, Applicative, Monad, MonadState Failure) + +runEval :: Eval a -> (a, Failure) +runEval (Eval eval) = runState eval false + +instance Mergeable a => Mergeable (Eval a) where + symbolicMerge force test left right = Eval $ state $ \s0 -> + let (resL, sL) = runState (unEval left) s0 + (resR, sR) = runState (unEval right) s0 + in ( symbolicMerge force test resL resR + , symbolicMerge force test sL sR + ) + +markFailure :: SBool -> Eval () +markFailure failure = modify (||| Failure failure) + +-- Test suite +tests :: TestTree +tests = + testGroup "Basics.BoundedList" [ + goldenCapturedIO "concreteFoldr" $ \rf -> checkWith z3{redirectVerbose=Just rf} concreteFoldrSat Sat + , goldenCapturedIO "concreteFoldl" $ \rf -> checkWith z3{redirectVerbose=Just rf} concreteFoldlSat Sat + , goldenCapturedIO "foldrAB1" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldrAB 1) Unsat + , goldenCapturedIO "foldrAB2" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldrAB 2) Sat + , goldenCapturedIO "foldrAB3" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldrAB 3) Sat + , goldenCapturedIO "foldlABC1" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldlABC 1) Unsat + , goldenCapturedIO "foldlABC2" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldlABC 2) Unsat + , goldenCapturedIO "foldlABC3" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldlABC 3) Sat + , goldenCapturedIO "concreteReverse" $ \rf -> checkWith z3{redirectVerbose=Just rf} concreteReverseSat Sat + , goldenCapturedIO "reverse" $ \rf -> checkWith z3{redirectVerbose=Just rf} reverseSat Sat + , goldenCapturedIO "reverseAlt10" $ \rf -> checkWith z3{redirectVerbose=Just rf} (reverseAlt 10) Unsat + , goldenCapturedIO "concreteSort" $ \rf -> checkWith z3{redirectVerbose=Just rf} concreteSortSat Sat + , goldenCapturedIO "sort" $ \rf -> checkWith z3{redirectVerbose=Just rf} sortSat Sat + , goldenCapturedIO "mapWithFailure" $ \rf -> checkWith z3{redirectVerbose=Just rf} mapWithFailure Sat + , goldenCapturedIO "mapNoFailure" $ \rf -> checkWith z3{redirectVerbose=Just rf} mapNoFailure Unsat + , goldenCapturedIO "maxlWithFailure" $ \rf -> checkWith z3{redirectVerbose=Just rf} maxlWithFailure Sat + , goldenCapturedIO "maxrWithFailure" $ \rf -> checkWith z3{redirectVerbose=Just rf} maxrWithFailure Sat + ] + +checkWith :: SMTConfig -> Symbolic () -> CheckSatResult -> IO () +checkWith cfg props csExpected = runSMTWith cfg{verbose=True} $ do + _ <- props + query $ do cs <- checkSat + unless (cs == csExpected) $ + case cs of + Unsat -> error $ "Failed! Expected " ++ show csExpected ++ ", got Unsat" + Sat -> getModel >>= \r -> error $ "Failed! Expected " ++ show csExpected ++ ", got Sat:\n" ++ show (SatResult (Satisfiable cfg r)) + Unk -> getUnknownReason >>= \r -> error $ "Failed! Expected " ++ show csExpected ++ ", got Unk:\n" ++ show r + +concreteFoldrSat :: Symbolic () +concreteFoldrSat = constrain $ BL.bfoldr 3 (+) 0 [1..3] .== (6 :: SInteger) + +concreteFoldlSat :: Symbolic () +concreteFoldlSat = constrain $ BL.bfoldl 10 (+) 0 [1..3] .== (6 :: SInteger) + +-- unsatisfiable at bound = 1, satisfiable at bound = 2 or bound = 3 +foldrAB :: Int -> Symbolic () +foldrAB bound = do + [a, b] <- sIntegers ["a", "b"] + constrain $ a .> 0 + constrain $ b .> 0 + constrain $ BL.bfoldr bound (+) 0 (L.implode [a, b]) .== a + b + +-- unsatisfiable at bound = 1 or bound = 2, satisfiable at bound = 3 +foldlABC :: Int -> Symbolic () +foldlABC bound = do + [a, b, c] <- sIntegers ["a", "b", "c"] + constrain $ a .> 0 + constrain $ b .> 0 + constrain $ c .> 0 + constrain $ BL.bfoldr bound (+) 0 (L.implode [a, b, c]) .== a + b + c + +concreteReverseSat :: Symbolic () +concreteReverseSat = constrain $ BL.breverse 10 [1..10] .== ([10,9..1] :: SList Integer) + +reverseSat :: Symbolic () +reverseSat = do + abcd <- sIntegers ["a", "b", "c", "d"] + constrain $ BL.breverse 10 (L.implode abcd) .== L.implode (reverse abcd) + +reverseAlt :: Int -> Symbolic () +reverseAlt i = do + xs <- sList "xs" + + -- Assert the negation; so Unsat response means it's all good! + constrain $ BL.breverse i xs ./= rev i xs ([] :: SList Integer) + where -- classic reverse with accumulator + rev 0 _ sofar = sofar + rev c xs sofar = ite (L.null xs) + sofar + (rev (c-1) (L.tail xs) (L.head xs .: sofar)) + + +concreteSortSat :: Symbolic () +concreteSortSat = constrain $ BL.bsort 10 [5,6,3,8,9,2,1,7,10,4] .== ([1..10] :: SList Integer) + +sortSat :: Symbolic () +sortSat = do [a, b, c] <- sIntegers ["a", "b", "c"] + + let sorted = BL.bsort 3 $ L.implode [a, b, c] + + ordered :: (SInteger, SInteger, SInteger) -> SBool + ordered (x, y, z) = x .<= y &&& y .<= z + + constrain $ ordered (a, b, c) ==> sorted .== L.implode [a, b, c] + constrain $ ordered (a, c, b) ==> sorted .== L.implode [a, c, b] + constrain $ ordered (b, a, c) ==> sorted .== L.implode [b, a, c] + constrain $ ordered (b, c, a) ==> sorted .== L.implode [b, c, a] + constrain $ ordered (c, a, b) ==> sorted .== L.implode [c, a, b] + constrain $ ordered (c, b, a) ==> sorted .== L.implode [c, b, a] + +-- | Increment, failing if a value lies outside of [0, 10] +boundedIncr :: SList Integer -> Eval (SList Integer) +boundedIncr = BL.bmapM 10 $ \i -> do + markFailure $ i .< 0 ||| i .> 10 + pure $ i + 1 + +-- | Max (based on foldr), failing if a value lies outside of [0, 10] +boundedMaxr :: SList Integer -> Eval SInteger +boundedMaxr = BL.bfoldrM 10 + (\i maxi -> do + markFailure $ i .< 0 ||| i .> 10 + pure $ smax i maxi) + 0 + +-- | Max (based on foldl), failing if a value lies outside of [0, 10] +boundedMaxl :: SList Integer -> Eval SInteger +boundedMaxl = BL.bfoldlM 10 + (\maxi i -> do + markFailure $ i .< 0 ||| i .> 10 + pure $ smax i maxi) + 0 + +-- the mapping will have failed if one of the resulting values is greater than +-- 11 +mapWithFailure :: Symbolic () +mapWithFailure = do + lst <- sList "ints" + let (lst', failure) = runEval $ boundedIncr lst + constrain $ lst' .!! 2 .> 11 ==> failure .== true + +-- mapping over these values of a, b, and c cannot fail (this is unsat) +mapNoFailure :: Symbolic () +mapNoFailure = do + [a, b, c] <- sIntegers ["a", "b", "c"] + let (_lst', Failure failure) = runEval $ boundedIncr $ L.implode [a, b, c] + constrain $ a + b + c .== 6 + constrain $ a .> 0 &&& b .> 0 &&& c .> 0 + constrain failure + +-- boundedMaxl fails if one of the values is too big +maxlWithFailure :: Symbolic () +maxlWithFailure = do + lst <- sList "ints" + let (maxi, Failure failure) = runEval $ boundedMaxl lst + constrain $ maxi .> 10 ==> failure + +-- boundedMaxl fails if one of the values is too big +maxrWithFailure :: Symbolic () +maxrWithFailure = do + lst <- sList "ints" + let (maxi, Failure failure) = runEval $ boundedMaxr lst + constrain $ maxi .> 10 ==> failure diff --git a/SBVTestSuite/Utils/SBVTestFramework.hs b/SBVTestSuite/Utils/SBVTestFramework.hs --- a/SBVTestSuite/Utils/SBVTestFramework.hs +++ b/SBVTestSuite/Utils/SBVTestFramework.hs @@ -198,9 +198,6 @@ expected = literal $ opC v result = opS i - observe "Expected" expected - observe "Result" result - case (unliteral expected, unliteral result) of (Just _, Just _) -> return $ expected .== result _ -> return false @@ -255,9 +252,6 @@ expected = literal $ opC v1 v2 result = opS i1 i2 - observe "Expected" expected - observe "Result" result - case (unliteral expected, unliteral result) of (Just _, Just _) -> return $ expected .== result _ -> return false @@ -305,9 +299,6 @@ pickTests d origTests = fromMaybe noTestsSelected <$> walk origTests where noTestsSelected = TestGroup "pickTests.NoTestsSelected" [] - walk PlusTestOptions{} = error "pickTests: Unexpected PlusTestOptions" - walk WithResource{} = error "pickTests: Unexpected WithResource" - walk AskOptions{} = error "pickTests: Unexpected AskOptions" walk t@SingleTest{} = do c <- randomRIO (0, 99) if c < d then return $ Just t @@ -316,5 +307,6 @@ case cs of [] -> return Nothing _ -> return $ Just $ TestGroup tn cs + walk _ = error "pickTests: Unexpected test group!" {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-} diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 7.12 +Version: 7.13 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 @@ -48,10 +48,10 @@ TypeOperators TypeSynonymInstances Build-Depends : base >= 4.9 && < 5 - , crackNum >= 2.2 + , crackNum >= 2.3 , ghc, QuickCheck, template-haskell , array, async, containers, deepseq, directory, filepath, time - , pretty, process, mtl, random, syb, reinterpret-cast + , pretty, process, mtl, random, syb , generic-deriving Exposed-modules : Data.SBV , Data.SBV.Control @@ -66,6 +66,8 @@ , Data.SBV.Tools.GenTest , Data.SBV.Tools.Overflow , Data.SBV.Tools.Polynomial + , Data.SBV.Tools.Range + , Data.SBV.Tools.BoundedFix , Data.SBV.Tools.STree , Documentation.SBV.Examples.BitPrecise.BitTricks , Documentation.SBV.Examples.BitPrecise.BrokenSearch @@ -104,7 +106,9 @@ , Documentation.SBV.Examples.Puzzles.DogCatMouse , Documentation.SBV.Examples.Puzzles.Euler185 , Documentation.SBV.Examples.Puzzles.Fish + , Documentation.SBV.Examples.Puzzles.Garden , Documentation.SBV.Examples.Puzzles.HexPuzzle + , Documentation.SBV.Examples.Puzzles.LadyAndTigers , Documentation.SBV.Examples.Puzzles.MagicSquare , Documentation.SBV.Examples.Puzzles.NQueens , Documentation.SBV.Examples.Puzzles.SendMoreMoney @@ -166,7 +170,7 @@ , DeriveDataTypeable , Rank2Types , ScopedTypeVariables - Build-depends : base >= 4.9, reinterpret-cast, filepath, syb + Build-depends : base >= 4.9, filepath, syb, crackNum >= 2.3 , sbv, directory, random, mtl, containers , template-haskell, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, QuickCheck Hs-Source-Dirs : SBVTestSuite @@ -180,6 +184,7 @@ , TestSuite.Basics.ArithSolver , TestSuite.Basics.Assert , TestSuite.Basics.BasicTests + , TestSuite.Basics.BoundedList , TestSuite.Basics.Exceptions , TestSuite.Basics.GenBenchmark , TestSuite.Basics.Higher