1* Hackage: <http://hackage.haskell.org/package/sbv> 2* GitHub: <http://leventerkok.github.com/sbv/> 3 4* Latest Hackage released version: 8.12, 2021-03-09 5 6### Version 8.12, 2021-03-09 7 8 * Fix a bug in crackNum for unsigned-integer values, which incorrectly 9 showed a negation sign for values with msb set to 1. 10 11### Version 8.11, 2021-03-09 12 13 * SBV now supports floating-point numbers with arbitrary exponent and 14 significand sizes. The type is `SFloatingPoint eb sb`, where `eb` 15 and `sb` are type-level naturals. In particular, SBV can now reason about 16 half-floats, which are used much more frequently in ML applications. Through 17 the LibBF binding, you can also use these concretely, so if you have a use 18 case for computing with floats, you can use SBV as a vehicle for doing so. 19 The exponent/significand sizes are limited to those supported by the LibBF 20 bindings, though the allowed range is rather large and should not be a limitation 21 in practice. (In particular, you'll most likely run out of memory before you 22 hit precision limits!) 23 24 * We now support a separate `crackNum` parameter in model display. If set to True 25 (default is False), SBV will display numeric values of bounded integers, words, 26 and all floats (SDouble, SFloat, and the new SFloatingPoint) in models in detail, 27 showing how they are laid out in memory. Numbers follow the usual 2's-complement 28 notation if they are signed, bit-vectors if they are not signed, and the floats 29 follow the usual IEEE754 binary layout rules. Similarly, there's now a function 30 crack :: SBV a -> String that does the same for non-model printing contexts. 31 32 * Changed the isNonModelVar config param to take a String (instead of Text). 33 Simplifies programming. 34 35 * Changes to make SBV compile with GHC9.0. Thanks to Ryan Scott for the patch. 36 37### Version 8.10, 2021-02-13 38 39 * Add "Documentation/SBV/Examples/Misc/NestedArray.hs" to demonstrate how 40 to model multi-dimensional arrays in SBV. 41 42 * Add "Documentation/SBV/Examples/Puzzles/Murder.hs" as another puzzle example. 43 44 * Performance updates: Thanks to Jeff Young, SBV now uses better underlying 45 data structures, performing better for heavy use-case scenarios. 46 47 * SBV now tracks constants more closely in query mode, providing more support 48 for constant arrays in a seamless way. (See #574 for details.) 49 50 * Pop-calls are now support for Yices and Boolector. (#577) 51 52 * Changes required to make SBV work with latest version of z3 regarding 53 String and Characters, which now allow for unicode characters. This required 54 renaming of certain recognizers in 'Data.SBV.Char' to restrict them to the 55 Latin1 subset. Otherwise, the changes should be transparent to the end user. 56 Please report any issues you might run into when you use SChar and SString types. 57 58### Version 8.9, 2020-10-28 59 60 * Rename 'sbvAvailableSolvers' to 'getAvailableSolvers'. 61 62 * Use SMTLib's int2bv if supported by the backend solver. If not, we still 63 do a manual translation. (CVC4 and z3 support it natively, Yices and 64 MathSAT does not, for which we do the manual translation. ABC and dReal 65 doesn't support the coversion at all, since former doesn't support integers 66 and the latter doesn't support bit-vectors.) Thanks to Martin Lundfall 67 for the initial pull request. 68 69 * Add `sym` as a synonym for `uninterpret`. This allows us to write expressions 70 of the form `sat $ sym "a" - sym "b" .== (0::SInteger)`, without resorting to lambda 71 expressions or having to explicitly be in the Symbolic monad. 72 73 * Added missing instances for overflow-checking arithmetic of arbitrary 74 sized signed and unsigned bitvectors. 75 76 * In a sat (or allSat) call, also return the values of the uninterpreted values, along with 77 all the explicitly named inputs. Strictly speaking, this is backwards-incompatible, 78 but it the new behavior is consistent with how we handle uninterpreted values in general. 79 80 * Improve SMTLib logic-detection code to use generics. 81 82### Version 8.8, 2020-09-04 83 84 * Reworked uninterpreted sorts. Added new function `mkUninterpretedSort` to make 85 declaration of completely uninterpreted sorts easier. In particular, we now 86 automatically introduce the symbolic variant of the type (by prefixing the 87 underlying type with `S`) so it becomes automatically available, both for uninterpreted 88 sorts and enumerations. In the latter case, we also automatically introduce the value `sX` 89 for each enumeration constant `X`, defined to be precisely `literal X`. 90 91 * Handle incremental mode table-declarations that depend on freshly declared variables. Thanks 92 to Gergő Érdi for reporting. 93 94 * Fix a soundness bug in SFunArray caching. Thanks to Gergő Érdi for reporting. See 95 https://github.com/LeventErkok/sbv/issues/541 for details. 96 97 * Add support for the dReal solver, and introduce the notion of delta-satisfiability, 98 where you can now check properties to be satisfiable against delta-perturbations. 99 See "Documentation.SBV.Examples.DeltaSat.DeltaSat" for a basic example. 100 101 * Add "extraArgs" parameter to SMTConfig to simplify passing extra command line 102 arguments to the solver. 103 104 * Add a method 105 106 sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> array a b 107 108 to the `SymArray` class, which allows for creation of arrays from lists of constant or 109 symbolic lists of pairs. The first argument is the value to use for uninitialized entries. 110 Note that the initializer must be a known constant, i.e., it cannot be symbolic. Latter 111 elements of the list will overwrite the earlier ones, if there are repeated keys. 112 113 * Thanks to Jan Hrcek, a whole bunch of typos were fixed in the documentation and 114 the source code. Much appreciated! 115 116### Version 8.7, 2020-06-30 117 118 * Add support for concurrent versions of solvers for query problems. Similar to 119 `satWithAny`, `proveWithAny` etc., except when we have queries. Thanks to Jeffrey Young 120 for the idea and the implementation. 121 122 * Add "Documentation.SBV.Examples.Misc.Newtypes", demonstrating how to use newtypes 123 over existing symbolic types as symbolic quantities themselves. Thanks to Curran McConnell 124 for the example. 125 126 * Added new predicate `sNotElem`, negating `sElem`. 127 128 * Added new predicate `distinctExcept`. This is same as `distinct` 129 except you can also provide an ignore list. The elements in 130 the first list will be checked to be distinct from each other, 131 or belong to the second list. This is good for writing constraints 132 that either require a default value or if picked be different 133 from each other for a set of variables. This sort of constraint 134 can be coded in user space, but SBV generates efficient code 135 instead of the obvious quadratic number of constraints. 136 137 * Add function 'algRealToRational' that can convert an algebraic-real 138 to a Haskell rational. We get an either value: If the algebraic real 139 is exact, then it returns a 'Left' value that represents the value 140 precisely. Otherwise, it returns a 'Right' value, which is only 141 an approximation. Note: Setting 'printRealPrec' in SMTConfig 142 to a higher value will increase the precision at the cost of more 143 computation by the SMT solver. 144 145 * Removed the 'SMTValue' class. It's functionality was not really 146 needed. If you ever used this class, removing it from your 147 type signatures should fix the issue. (You might have to 148 add SymVal constraint if you did not already have it.) Please 149 get in touch if you used this class in some cunning way and you 150 need its functionality back. 151 152 * Reworked SBVBenchSuite api, Phase 1 of BenchSuite completed. 153 154 * Add support for addAxiom command to work in the interactive mode. 155 Thanks to Martin Lundfall for the feedback. 156 157 * Fixed `proveWithAny` and `satWithAny` functions so they properly 158 kill the solvers that did not terminate first. Previously, they 159 became zombies if they didn't end up quickly. Thanks to 160 Robert Dockins for the investigation and the fix. 161 162 * Fixed a bug where resetAssertions call was forgetting to restore the 163 array and table contexts. Thanks to Martin Lundfall for reporting. 164 165### Version 8.6, 2020-02-08 166 167 * Fix typo in error message. Thanks to Oliver Charles 168 for the patch. 169 170 * Fix parsing of sequence counter-examples to accommodate 171 recent changes in z3. 172 173 * Add missing exports related to N-bit words. Thanks to 174 Markus Barenhoff for the patch. 175 176 * Generalized code-generation functions to accept a function 177 with an arbitrary return type, which was previously just unit. 178 This allows for complicated code-generation scenarios where 179 one code-gen run can produce input to the next. 180 181 * Scalability improvements for internal data structures. Thanks 182 to Brian Huffman for the patch. 183 184 * Add interpolation support for Z3, following changes to that 185 solver. Note that SBV now supports two different APIs for 186 interpolation extraction, one for Z3 and the other for 187 MathSAT. This is unfortunate, but necessary since interpolant 188 extraction isn't quite standardized amongst solvers and 189 MathSAT and Z3 use sufficiently different calling mechanisms 190 to warrant their own calls. See 'Documentation.SBV.Examples.Queries.Interpolants' 191 for examples that illustrate both cases. 192 193 * Add a new argument to `displayModels` function to allow rearranging 194 of the results in an 'allSat` call. Strictly speaking this is 195 a backwards breaking change, but substituting `id` for the 196 new argument gives you old functionality, so easy to work-around. 197 198 199### Version 8.5, 2019-10-16 200 201 * Changes to compile with GHC 8.8. Thanks to Oliver Charles 202 for the patch. 203 204 * Minor fix to how kinds are shown for non-standard sizes. 205 206 * Thanks to Jeffrey Young, SBV now has a performance benchmark 207 test-suite. The framework still new, but should help 208 in the long run to make sure SBV performance doesn't regress 209 on its test-suite, and by extension in general usage. 210 211### Version 8.4, 2019-08-31 212 213 * SBV now supports arbitrary-size bit-vectors, i.e., 214 SWord 17, SInt 9, SWord 128 etc. These work like any 215 other bit-vector, using the `DataKinds` feature of 216 GHC. Thanks to Ben Blaxill for the idea and the initial 217 implementation. Note that SBV still supports the traditional 218 fixed-size bit-vectors, SInt8, SWord16 etc. Support for 219 these will not be removed; so existing programs will 220 continue to work. 221 222 * To convert between arbitrary sized bit-vectors and 223 the old style equivalents, use `fromSized` and `toSized` 224 functions. The behavior is controlled with a closed 225 type-family so you will get a (hopefully not too 226 horrendous) type error message if you try to convert, 227 say, a SInt16 to SInt 22; or vice versa. 228 229 * Added arbitrary-sized bit vector operations: extraction, 230 extension, and joining; these use proxy arguments to 231 determine precise size info, and are much better suited 232 for type safety. Consequently, removed the Splittable 233 class which provided similar operations but only on 234 predefined types. There is a new class called ByteConverter 235 to convert to-and-from bytes for suitable bit-vector 236 sizes upto 512. 237 238 * Tuple construction functions are given new types to strengthen 239 type checking. Previously the tuple argument was ignored, 240 causing things to be marked as tuples when they actually 241 cannot be. (NB. The system was always type-safe, it just 242 didn't produce helpful type-error messages before.) 243 244 * Model validator: In the presence of universally quantified 245 variables, SBV used to refuse to validate given models. This 246 is the right thing to do since we would have to validate 247 the model for all possible values of all the universally 248 quantified variables. Obviously this is not useful. Instead, 249 SBV now simply assumes any universally quantified variable 250 is zero during model validation. This severely limits the 251 validation result, but it is better than nothing. (In the 252 verbose mode, a message to this effect will be printed.) 253 254 * Model validator: SBV can now validate models returned from 255 the backend solver for regular-expression match problems. 256 We also constant fold matches against constant strings without 257 calling the solver at all, less useful perhaps but more inline 258 with the general SBV methodology. 259 260 * Add implementation of SHA-2 family of functions as an example 261 algorithm. These are good for code-generation purposes as 262 opposed to actual verification tasks as it is hard to state 263 any properties of these algorithms. But the SBV generated 264 code can be quite useful in other development and verification 265 environments. See 'Documentation.SBV.Examples.Crypto.SHA' for 266 details. 267 268 * Add 'cgShowU8UsingHex function, which controls if we print unsigned-8 bit 269 values in code generation driver code in hex or not. Previously we were 270 using decimal, but in crypto code hex is always better. Default is 'False' 271 to keep backwards compatibility. 272 273 * Add `sObserve` from: `SymWord a => String -> SBV a -> Symbolic ()` which 274 comes in handy in symbolic contexts, especially with quick-check uses. 275 276 * Ramped up travis-appveyor build infrastructure. However, we no 277 longer test on the CI, since build-times are prohibitively long 278 and myriad issues cause instability. If you can help out regarding 279 testing on CI, please reach out! 280 281### Version 8.3, 2019-06-08 282 283 * Increment base dependency to 4.11. 284 285 * Add support for `Data.Set.hasSize`. 286 287 * Add `supportsFP` to CVC4 capabilities list. (#469) 288 289 * Fix a glitch in allSat computations that incorrectly 290 used values of internal variables in model construction. 291 292 * SBV now directly uses the new `seq.nth` function from z3 293 for sequence element access, instead of implementing it 294 internally. 295 296### Version 8.2, 2019-04-07 297 298 * Fixed minor issue with getting observables in quantified contexts. 299 300 * Simplify data-type constructor usage and accessor formats. See 301 http://github.com/Z3Prover/z3/issues/2135 for a discussion. 302 303 * Add support for model validation in optimization problems. Use the 304 config parameter: `optimizeValidateConstraints`. Default: False. This 305 feature nicely complements the `validateModel` option, which works 306 for `sat` and `prove` calls. Note that when we validate the model 307 for an optimization problem, we only make sure that the given result 308 satisfies the constraints not that it is minimum (or maximum) such 309 model. (And hence the new configuration variable.) Validating optimality 310 is beyond the scope of SBV. 311 312### Version 8.1, 2019-03-09 313 314 * Added support for `SEither` and `SMaybe` types: symbolic sums and symbolic 315 optional values. These can be accessed by importing `Data.SBV.Either` and 316 `Data.SBV.Maybe` respectively. They translate to SMTLib's data-type syntax, 317 and thus require a solver capable of handling datatypes. (Currently z3 and 318 cvc4 are the only solvers that do.) All the typical introduction and 319 elimination functions are provided, and these types integrate with all 320 other symbolic types. (So you can have a list of SMaybe of SEither 321 values, or at any nesting level.) Thanks to Joel Burget for the initial 322 implementation of this idea and his contributions. 323 324 * Added support for symbolic sets. The API closely follows that of `Data.Set` 325 of Haskell, with some major differences: Symbolic sets can be co-finite. 326 (That is, we can represent not only finite sets, but also sets whose complements 327 are finite.) The distinction shows up in the `complement` operation, which 328 is not supported in Haskell. All SBV sets can be complemented. On the flip 329 side, SBV sets do not support a size operation (as they can be infinite), 330 nor they can be converted to lists. See 'Data.SBV.Set' for the API documentation 331 and "Documentation/SBV/Examples/Misc/SetAlgebra.hs" for an example that proves 332 many familiar set properties. 333 334 * SBV models now contain values for uninterpreted functions. This was a long 335 requested feature, but there was no previous support since SMTLib does not 336 have a standard way of querying such values. We now support this for z3 and 337 cvc4: Note that SBV tries its best to interpret the output from these 338 solvers, but it may give up if the response is too complicated (or something 339 I haven't seen before!) due to non-standard format. Barring these details, 340 the calls to `sat` now include function models, and you can also get them 341 via `getFunction` in a query. 342 343 For an example use case demonstrating how to use UF-models to synthesize a 344 simple multiplier, see "Documentation/SBV/Examples/Uninterpreted/Multiply.hs". 345 346 * SBV now comes with a model validator. In a 'sat', 'prove', or 'allSat' call, 347 you can pass the configuration parameter 'z3{validateModel = True}' (or whichever 348 solver you're using), and z3 will attempt to validate the returned model 349 from the solver. Note that validation only works if there are no uninterpreted 350 kinds of functions, and also in quantifier-free problems only. Please report 351 your experiences, as there's room for improvement in validation, always! 352 353 * [BACKWARDS COMPATIBILITY] The `allSat` function is similarly modified to 354 return uninterpreted-function models. There are a few technical restrictions, 355 however: Only the values of uninterpreted functions without any uninterpreted 356 arguments will participate in `allSat` computation. (For instance, 357 `uninterpret "f" :: SInteger -> SInteger` is OK, but 358 `uninterpret "f" :: MyType -> SInteger` is not, where `MyType` itself 359 is uninterpreted.) The reason for this is again there is no SMTLib way of 360 reflecting uninterpreted model values back into the solver. This restriction 361 should not cause much trouble in practice, but do get in touch if it is a 362 use-case for you. 363 364 * Added configuration option `allSatPrintAlong`. If set to True, calls to 365 allSat will print their models as they are found. The default is False. 366 367 * Added configuration parameter `satTrackUFs` (defaulting to True) to control 368 if SBV should try to extract models for uninterpreted functions. In theory, 369 this should always be True, but for most practical problems we typically 370 don't care about the function values itself but that it exists. Set to 'False' 371 if this is the case for your problem. Note that this setting is also respected 372 in 'allSat' calls. 373 374 * Added function `registerUISMTFunction`, which can be used to directly register uninterpreted 375 functions. This is typically not necessary as uses of UI-functions do register them 376 automatically, but it can come in handy in certain scenarios where there are no 377 constraints on a UI-function other than its existence. 378 379 * Added `Data.SBV.Tools.WeakestPreconditions` module, which provides a toy imperative 380 language and an engine for checking partial and total correctness of imperative programs. 381 It uses Dijkstra's weakest preconditions methodology to establish correctness claims. 382 Loop invariants are required and must be supplied by the user. For total correctness, 383 user must also provide termination measure functions. However, if desired, these can 384 be skipped (by passing 'Nothing'), in which case partial correctness will be proven. 385 Checking input parameters for no-change is supported via stability checks. For example 386 use cases, see the `Documentation.SBV.Examples.WeakestPreconditions` directory. 387 388 * Added functions `elem`/`notElem` to `Data.SBV.List`. 389 390 * Added `snoc` (appending a single element at the end) to `Data.SBV.List` and `Data.SBV.String`. 391 392 * Rework the 'Queriable' class to allow projection/embedding pairs. Also 393 added a new 'Fresh' class, which is more usable in simpler scenarios 394 where the default projection/embedding definitions are suitable. 395 396 * Added strong-equality (.===) and inequality (./==) to the 'EqSymbolic' class. This 397 method is equivalent to the usual (.==) and (./=) for all types except 'SFloat' and 398 'SDouble'. For the floating types, it is object equality, that is 'NaN .=== Nan' 399 and '0 ./== -0'. Use the regular equality for float/double's as they follow the 400 IEEE754 rules, but occasionally we need to express object equality in a polymorphic 401 way. Essentially this method is the polymorphic equivalent of 'fpIsEqualObject' 402 except it works on all types. 403 404 * Removed the redundant 'SDivisible' constraint on rotate-left and rotate-right operations. 405 406 * Added unnamed equivalents of 'sBool', 'sWord8' etc; with a following underscore, i.e., 407 'sBool_', 'sWord8_'. The new functions are supported for all base types, chars, 408 strings, lists, and tuples. 409 410 * SBV now supports implicit constraints in the query mode, which were previously only 411 available before user queries started. 412 413 * Fixed a bug where hash-consing might reuse an expression even though the request might 414 have been made at a different type. This is a rare case in SBV to happen due to types, 415 but it was possible to exploit it in the Dynamic interface. Thanks to Brian Huffman 416 for reporting and diagnosing the issue. 417 418 * Fixed a bug where SBV was reporting incorrect "elapsed" time values, which are 419 printed when the 'timing' configuration parameter is specified. 420 421 * Documentation: Jan Path kindly fixed module headers of all the files to produce 422 much better looking Haddock documents. Thanks Jan! 423 424 * Added barrel-rotations (sBarrelRotateLeft-Right, svBarrelRotateLeft-Right) which 425 can produce better code for verification by bit-blasting the rotation amount. 426 It accepts bit-vectors as arguments and an unsigned rotation quantity to keep 427 things simple. 428 429 * Added new configuration option 'allowQuantifiedQueries', default is set to False. 430 SBV normally doesn't allow quantifiers in a query context, because there are 431 issues surrounding 'getValue'. However, Joel Burget pointed out this check 432 is too strict for certain scenarios. So, as an escape hatch, you can define 433 'allowQuantifiedQueries' to be 'True' and SBV will bypass this check. Of course, 434 if you do this, then you are on your own regarding calls to `getValue` with 435 quantified parameters! See http://github.com/LeventErkok/sbv/issues/459 436 for details. 437 438 * [BACKWARDS COMPATIBILITY] Renamed the class `IEEEFloatConvertable` to 439 `IEEEFloatConvertible`. (Typo in name!) Matt Peddie pointed out issues 440 regarding conversion of out-of-bounds float and double values to integral 441 types. Unfortunately SMTLib does not support these conversions, and we 442 had issues in getting Haskell, SMTLib, and C to agree. Summary: These conversions 443 are only guaranteed to work if they are done on numbers that lie within the 444 representable range of the target type. Thanks to Matt Peddie for pointing out 445 the out-of-bounds problem, his help in figuring out the issues. 446 447 * [BACKWARDS COMPATIBILITY] The 'AllSat' result now tracks if search has stopped 448 because the solver returned 'Unknown'. Previously this information was not 449 displayed. 450 451 * [BACKWARDS COMPATIBILITY, Internal] Several constraints on internal 452 classes (such as SymVal, EqSymbolic, OrdSymbolic) were reworked to 453 reflect the dependencies better. Strictly speaking this is a backwards 454 compatibility breaking change, but I doubt it'll impact any user 455 code; though you might have to add some extra constraints if you were 456 writing sufficiently polymorphic SBV code. Yell if you find otherwise! 457 458 * [BACKWARDS COMPATIBILITY] SBV now allows user-given names to be duplicated. 459 It will implicitly add a suffix to them to distinguish without complaining. (In 460 previous versions, we would error out.) The reason for this change is that 461 sometimes it's nice to be able to simply give a prefix for a class of names 462 and not worry about the actual name itself. (Note that this will cause issues 463 if you use model-extraction-via-maps method if we ever make a name unique 464 and store it under a different name, but that's hardly ever used feature and 465 arguably the right thing to do anyway.) Thanks to Joel Burget for suggesting 466 the idea. 467 468 * [BACKWARDS COMPATIBILITY, Internal] SBV is now more strict in how user-queries 469 are used, performing certain extra-checks that were not done before. (For instance, 470 previously it was possible to mix prove-sat with a query call, which should 471 not have been allowed.) If you have any code that breaks for this reason, you 472 probably should've written it in some other way to start with. Please get 473 in touch if that is the case. 474 475 * [BACKWARDS COMPATIBILITY] You need at least GHC 8.4.1 to compile SBV. 476 If you're stuck with an older version, let me know and we'll see if 477 we can create a custom version for you; though I'd much rather avoid this 478 if at all possible. 479 480 * SBV now supports optimization of goals of SDouble and SFloat types. This is 481 done using the lexicographic ordering on floats, and adds on the additional 482 constraint that the resulting float is not a NaN. If you use this feature, 483 then your float value will be minimized as the corresponding 32 (or 64 for 484 doubles) bit word. Note that this methods supports infinities properly, and 485 does not distinguish between -0 and +0. 486 487 * Optimization routines have been generalized to work over arbitrary metric-spaces, 488 with user-definable mappings. The simplest instance we have added is optimization 489 over booleans, by the obvious numeric mapping. Tuples are also supported with 490 the usual lexicographic ordering. In addition, SBV can now optimize over 491 user-defined enumerations. See "Documentation.SBV.Examples.Optimization.Enumerate" for 492 an example. 493 494 * Improved the internal representation of constraints to address performance 495 issues See http://github.com/LeventErkok/sbv/issues/460 for details. Thanks to 496 Thanks Jeffrey Young for reporting. 497 498### Version 8.0, 2019-01-14 499 500 * This is a major release of SBV, with several BACKWARDS COMPATIBILITY breaking 501 changes. Lots of reworking of the internals to modernize the SBV code base. 502 A few external API changes happened as well, mainly in terms of renamed 503 types/operators to reflect the current state of things. I expect most end user 504 programs to carry over unchanged, perhaps needing a bunch of renames. See below 505 for details. 506 507 * Transformer stack and `SymbolicT`: This major internal revamping was contributed 508 by Brian Schroeder. Brian reworked the internals of SBV to allow for custom monad 509 stacks. In particular, there is now a `SymbolicT` monad transformer, which 510 generalizes the `Symbolic` monad over an arbitrary base type, allowing users to 511 build SBV based symbolic execution engines on top of their own monad infrastructure. 512 513 Brian took the pains to ensure existing users (or those who do not have their 514 own monad stack), the transformer capabilities remain transparent. That is, 515 your existing code should recompile as is, or perhaps with minor aesthetic 516 changes. Please report if you find otherwise, or need help. 517 518 See `Documentation.SBV.Examples.Transformers.SymbolicEval` for an example of 519 how to use the transformer based code. 520 521 Thanks to Brian Schroeder for this massive effort to modernize the SBV code-base! 522 523 * Support for tuples: Thanks to Joel Burget, SBV now supports tuple types (up-to 524 8-tuples), and allows mixing and matching of lists and tuples arbitrarily 525 as symbolic values. For instance `SBV [(Integer, String)]` is a valid type as 526 is `SBV [(Integer, [(Char, (Float, String))])]`, with each component symbolically 527 represented. Along with `STuple` for regular 2-tuples, there are new types 528 for `STupleN` for `N` between 2 to 8, along with `untuple` destructor, and field 529 accessors similar to lens: For instance `p^._4` would project the 4th element of 530 a tuple that has at least 4 fields. The mixing and matching of field types and 531 nesting allows for very rich symbolic value representations. See 532 `Documentation.SBV.Examples.Misc.Tuple` for an example. 533 534 * [BACKWARDS COMPATIBILITY] The `Boolean` class is removed, which used to abstract 535 over logical connectives. Previously, this class handled 'SBool' and 'Bool', but 536 the generality was hardly ever used and caused typing ambiguities. The new 537 implementation simplifies boolean operators to simply operate on the `SBool` 538 type. Also changed the operator names to fit with all the others by starting 539 them with dots. A simple conversion guide: 540 541 * Literal True : true became sTrue 542 * Literal False: false became sFalse 543 * Negation : bNot became sNot 544 * Conjunction : &&& became .&& 545 * Disjunction : ||| became .|| 546 * XOr : <+> became .<+> 547 * Nand : ~& became .~& 548 * Nor : ~| became .~| 549 * Implication : ==> became .=> 550 * Iff : <=> became .<=> 551 * Aggregate and: bAnd became sAnd 552 * Aggregate or : bOr became sOr 553 * Existential : bAny became sAny 554 * Universal : bAll became sAll 555 556 * [BACKWARDS COMPATIBILITY, INTERNAL] Historically, SBV focused on bit-vectors and machine 557 words, which meant lots of internal types were named suggestive of this heritage. 558 With the addition of `SInteger`, `SReal`, `SFloat`, `SDouble` we have expanded 559 this, but still remained focused on atomic types. But, thanks largely to 560 Joel Burget, SBV now supports symbolic characters, strings, lists, and now 561 tuples, and nested tuples/lists, which makes this word-oriented naming confusing. 562 To reflect, we made the following internal renamings: 563 564 * SymWord became SymVal 565 * SW became SV 566 * CW became CV 567 * CWVal became CVal 568 569 Along with these, many of the internal constructor/variable names also changed in 570 a similar fashion. 571 572 For most casual users, these changes should not require any changes. But if you were 573 developing libraries on top of SBV, then you will have to adapt to the new schema. 574 Please report if there are any gotchas we have forgotten about. 575 576 * [BACKWARDS COMPATIBILITY] When user queries are present, SBV now picks the logic 577 "ALL" (as opposed to a suitable variant of bit-vectors as in the past versions). 578 This can be overridden by the 'setLogic' command as usual of course. While the new 579 choice breaks backwards compatibility, I expect the impact will be minimal, and 580 the new behavior matches better with user expectations on how external queries are 581 usually employed. 582 583 * [BACKWARDS COMPATIBILITY] Renamed the module `Data.SBV.List.Bounded` to 584 `Data.SBV.Tools.BoundedList`. 585 586 * Introduced a `Queriable` class, which simplifies symbolic programming with composite 587 user types. See `Documentation.SBV.Examples.ProofTools` directory for several 588 use cases and examples. 589 590 * Added function `observeIf`, companion to `observe`. Allows observing of values 591 if they satisfy a given predicate. 592 593 * Added function `ensureSat`, which makes sure the solver context is satisfiable 594 when called in the query mode. If not, an error will be thrown. Simplifies 595 programming when we expect a satisfiable result and want to bail out if otherwise. 596 597 * Added `nil` to `Data.SBV.List`. Added `nil` and `uncons` to `Data.SBV.String`. 598 These were inadvertently left out previously. 599 600 * Add `Data.SBV.Tools.BMC` module, which provides a BMC (bounded-model 601 checking engine) for traditional state transition systems. See 602 `Documentation.SBV.Examples.ProofTools.BMC` for example uses. 603 604 * Add `Data.SBV.Tools.Induction` module, which provides an induction engine 605 for traditional state transition systems. Also added several example use 606 cases in the directory `Documentation.SBV.Examples.ProofTools`. 607 608### Version 7.13, 2018-12-16 609 610 * Generalize the types of `bminimum` and `bmaximum` by removing the `Num` 611 constraint. 612 613 * Change the type of `observe` from: `SymWord a => String -> SBV a -> Symbolic ()` 614 to `SymWord a => String -> SBV a -> SBV a`. This allows for more concise observables, 615 like this: 616 617 prove $ \x -> observe "lhs" (x+x) .== observe "rhs" (2*x+1) 618 Falsifiable. Counter-example: 619 s0 = 0 :: Integer 620 lhs = 0 :: Integer 621 rhs = 1 :: Integer 622 623 * Add `Data.SBV.Tools.Range` module which defines `ranges` and `rangesWith` functions: They 624 compute the satisfying contiguous ranges for predicates with a single variable. See 625 `Data.SBV.Tools.Range` for examples. 626 627 * Add `Data.SBV.Tools.BoundedFix` module, which defines the operator `bfix` that can be used 628 as a bounded fixed-point operator for use in bounded-model-checking like algorithms. See 629 `Data.SBV.Tools.BoundedFix` for some example use cases. 630 631 * Fix list-element extraction code, which asserted too strong a constraint. See issue #421 632 for details. Thanks to Joel Burget for reporting. 633 634 * New bounded list functions: `breverse`, `bsort`, `bfoldrM`, `bfoldlM`, and `bmapM`. 635 Contributed by Joel Burget. 636 637 * Add two new puzzle examples: 638 * `Documentation.SBV.Examples.Puzzles.LadyAndTigers` 639 * `Documentation.SBV.Examples.Puzzles.Garden` 640 641### Version 7.12, 2018-09-23 642 643 * Modifications to make SBV compile with GHC 8.6.1. (SBV should 644 now compile fine with all versions of GHC since 8.0.1; and 645 possibly earlier. Please report if you are using a version 646 in this range and have issues.) 647 648 * Improve the BoundedMutex example to show a non-fair trace. 649 See `Documentation/SBV/Examples/Lists/BoundedMutex.hs`. 650 651 * Improve Haddock documentation links throughout. 652 653### Version 7.11, 2018-09-20 654 655 * Add support for symbolic lists. (That is, arbitrary but fixed length symbolic 656 lists of integers, floats, reals, etc. Nested lists are allowed as well.) 657 This is building on top of Joel Burget's initial work for supporting symbolic 658 strings and sequences, as supported by Z3. Note that the list theory solvers 659 are incomplete, so some queries might receive an unknown answer. See 660 `Documentation/SBV/Examples/Lists/Fibonacci.hs` for an example, and the 661 module `Data.SBV.List` for details. 662 663 * A new module `Data.SBV.List.Bounded` provides extra functions to manipulate 664 lists with given concrete bounds. Note that SMT solvers cannot deal with 665 recursive functions/inductive proofs in general, so the utilities in this 666 file can come in handy when expressing bounded-model-checking style 667 algorithms. See `Documentation/SBV/Examples/Lists/BoundedMutex.hs` for a 668 simple mutex algorithm proof. 669 670 * Remove dependency on data-binary-ieee754 package; which is no longer 671 supported. 672 673### Version 7.10, 2018-07-20 674 * [BACKWARDS COMPATIBILITY] '==' and '/=' now always throw an error instead of 675 only throwing an error for non-concrete values. 676 http://github.com/LeventErkok/sbv/issues/301 677 678 * [BACKWARDS COMPATIBILITY] Array declarations are reworked to take 679 an initial value. The call 'newArray' now accepts an optional default 680 value, which itself can be symbolic. If provided, the array will return 681 the given value for all reads from uninitialized locations. If not given, 682 then reads from unwritten locations produce uninterpreted constants. The 683 behavior of 'SFunArray' and 'SArray' is exactly the same in this regard. 684 Note that this is a backwards-compatibility breaking change, as you need 685 to pass a 'Nothing' argument to 'newArray' to get the old behavior. 686 (Solver note: If you use 'SFunArray', then defaults are fully supported 687 by SBV since these are internally handled, concrete or symbolic. If you 688 use 'SArray', which gets translated to SMTLib, then MathSAT and Z3 supports 689 default values with both concrete and symbolic cases, CVC4 only supports 690 if they are constants. Boolector and Yices don't support default values 691 at this point in time, and ABC doesn't support arrays at all.) 692 693 * [BACKWARDS COMPATIBILITY] SMTException type has been renamed to 694 SBVException. SBV now throws this exception in more cases to aid in 695 building tools on top of SBV that might want to deal with exceptions 696 in different ways. (Previously, we used to call 'error' instead.) 697 698 * [BACKWARDS COMPATIBILITY] Rename 'assertSoft' to 'assertWithPenalty', which 699 better reflects the nature of this function. Also add extra checks to warn 700 the user if optimization constraints are present in a regular sat/prove call. 701 702 * Implement `softConstrain`: Similar to 'constrain', except the solver is 703 free to leave it unsatisfied (i.e., leave it false) if necessary to 704 find a satisfying solution. Useful in modeling conditions that are 705 "nice-to-have" but not "required." Note that this is similar to 706 'assertWithPenalty', except it works in non-optimization contexts. 707 See `Documentation.SBV.Examples.Misc.SoftConstrain` for a simple example. 708 709 * Add 'CheckedArithmetic' class, which provides bit-vector arithmetic 710 operations that do automatic underflow/overflow checking. The operations 711 follow their regular counter-parts, with an exclamation mark added at 712 the end: +!, -!, *!, /!. There is also negateChecked, for the same 713 function on unary negation. If you program using these functions, 714 then you can call 'safe' on the resulting programs to make sure 715 these operations never cause underflow and overflow conditions. 716 717 * Similar to above, add 'sFromIntegralChecked', providing overflow/underflow 718 checks for cast operations. 719 720 * Add `Documentation.SBV.Examples.BitPrecise.BrokenSearch` module to show the 721 use of overflow checking utilities, using the classic broken binary search 722 example from http://ai.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html 723 724 * Fix an issue where SBV was not sending array declarations to the SMT-solver 725 if there were no explicit constraints. Thanks to Oliver Charles for reporting. 726 727 * Rework 'SFunArray' implementation, addressing performance issues. We now 728 carefully memoize elements as we do the look-ups. This addresses several 729 perfomance issues that came up; hopefully providing some relief. The 730 function 'mkSFunArray' is also removed, which used to lift Haskell 731 functions to such arrays, often used to implement initial values. Now, 732 if a read is done on an unwritten element of 'SFunArray' we get an 733 uninterpreted constant. This is inline with how 'SArray' works, and 734 is consistent. The old 'SFunArray' implementation based on functions 735 is no longer available, though it is easy to implement it in user-space 736 if needed. Please get in contact if this proves to be an issue. 737 738 * Add 'freshArray' to allow for creation of existential fresh arrays in the query mode. 739 This is similar to 'newArray' which works in the Symbolic mode, and is analogous to 740 'freshVar'. Most users shouldn't need this as 'newArray' calls should suffice. Only 741 use if you need a brand new array after switching to query mode. 742 743 * SBV now rejects queries if universally quantified inputs are present. Previously 744 these were allowed to go through, but in general skolemization makes the corresponding 745 variables unusable in the query context. See http://github.com/LeventErkok/sbv/issues/407 746 for details. If you have an actual use case for such a feature, please get in 747 touch. Thanks to Brian Schroeder for reporting this anomaly. 748 749 * Export 'addSValOptGoal' from 'Data.SBV.Internals', to help with 'Metric' class 750 instantiations. Requested by Dan Rosen. 751 752 * Export 'registerKind' from 'Data.SBV.Internals', to help with custom array declarations. 753 Thanks to Brian Schroeder for the patch. 754 755 * If an asynchronous exception is caught, SBV now throws it back without further processing. 756 (For instance, if the backend solver gets killed. Previously we were turning these into 757 synchronous errors.) Thanks to Oliver Charles for pointing out this corner case. 758 759### Version 7.9, 2018-06-15 760 761 * Add support for bit-vector arithmetic underflow/overflow detection. The new 762 'ArithmeticOverflow' class captures conditions under which addition, subtraction, 763 multiplication, division, and negation can underflow/overflow for 764 both signed and unsigned bit-vector values. The implementation is based on 765 http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf, 766 and can be used to detect overflow caused bugs in machine arithmetic. 767 See `Data.SBV.Tools.Overflow` for details. 768 769 * Add 'sFromIntegralO', which is the overflow/underflow detecting variant 770 of 'sFromIntegral'. This function returns (along with the converted 771 result), a pair of booleans showing whether the conversion underflowed 772 or overflowed. 773 774 * Change the function 'getUnknownReason' to return a proper data-type 775 ('SMTReasonUnknown') as opposed to a mere string. This is at the 776 query level. Similarly, change `Unknown` result to return the same 777 data-type at the sat/prove level. 778 779 * Interpolants: With Z3 4.8.0 release, Z3 folks have dropped support 780 for producing interpolants. If you need interpolants, you will have 781 to use the MathSAT backend now. Also, the MathSAT API is slightly 782 different from how Z3 supported interpolants as well, which means 783 your old code will need some modifications. See the example in 784 Documentation.SBV.Examples.Queries.Interpolants for the new usage. 785 786 * Add 'constrainWithAttribute' call, which can be used to attach 787 arbitrary attribute to a constraint. Main use case is in interpolant 788 generation with MathSAT. 789 790 * C code generation: SBV now spits out linker flag -lm if needed. 791 Thanks to Matt Peddie for reporting. 792 793 * Code reorg: Simplify constant mapping table, by properly accounting 794 for negative-zero floats. 795 796 * Export 'sexprToVal' for the class SMTValue, which allows for custom 797 definitions of value extractions. Thanks to Brian Schroeder for the 798 patch. 799 800 * Export 'Logic' directly from Data.SBV. (Previously was from Control.) 801 802 * Fix a long standing issue (ever since we introduced queries) where 803 'sAssert' calls were run in the context of the final output boolean, 804 which is simply the wrong thing to do. 805 806### Version 7.8, Released 2018-05-18 807 808 * Fix printing of min-bounds for signed 32/64 bit numbers in C 809 code generation: These are tricky since C does not allow 810 -min_value as a valid literal! Instead we use the macros provided in 811 stdint.h. Thanks to Matt Peddie for reporting this corner case. 812 813 * Fix translation of the `abs` function in C code generation, making 814 sure we use the correct variant. Thanks to Matt Peddie for reporting. 815 816 * Fix handling of tables and arrays in pushed-contexts. Previously, 817 we used initializers to get table/array values stored properly. 818 However, this trick does not work if we are in a pushed-context; 819 since a pop can forget the corresponding assignments. SBV now 820 handles this corner case properly, by using tracker assertions 821 to keep track of what array values must be restored at each pop. 822 Thanks to Martin Brain on the SMTLib mailing list for the 823 suggestion. (See http://github.com/LeventErkok/sbv/issues/374 824 for details.) 825 826 * Fix corner case in ite branch equality with float/double arguments, 827 where we were previously confusing +/-0 as equal to each other. 828 Thanks to Matt Peddie for reporting. 829 830 * Add a call 'cgOverwriteFiles', which suppresses code-generation 831 prompts for overwriting files and quiets the prompts during 832 code generation. Thanks to Matt Peddie for the suggestion. 833 834 * Add support for uninterpreted function introductions in the query 835 mode. Previously, this was only allowed before the query started, 836 now we fully support uninterpreted functions in all modes. 837 838 * New example: Documentation/SBV/Examples/Puzzles/HexPuzzle.hs, 839 showing how to code cover properties using SBV, using a form 840 of bounded model checking. 841 842### Version 7.7, Released 2018-04-29 843 844 * Add support for Symbolic characters ('SChar') and strings ('SString'.) 845 Thanks to Joel Burget for the initial implementation. 846 847 The 'SChar' type currently corresponds to the Latin-1 character 848 set, and is thus a subset of the Haskell 'Char' type. This is 849 due to the current limitations in SMT-solvers. However, there 850 is a pending SMTLib proposal to support unicode, and SBV will track 851 these changes to have full unicode support: For further details 852 see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml 853 854 The 'SString' type is the type of symbolic strings, consisting 855 of characters from the Latin-1 character set currently, just 856 like the planned 'SChar' improvements. Note that an 'SString' 857 is *not* simply a list of 'SChar' values: It is a symbolic 858 type of its own and is processed as a single item. Conversions 859 from list of characters is possible (via the 'implode' function). 860 In the other direction, one cannot generally 'explode' a string, 861 since it may be of arbitrary length and thus we would not know 862 what concrete list to map it to. This is a bit unlike Haskell, 863 but the differences dissipate quickly in general, and the power 864 of being able to deal with a string as a symbolic entity on its 865 own opens up many verification possibilities. 866 867 Note that currently only Z3 and CVC4 has support for this logic, 868 and they do differ in some details. Various character/string 869 operations are supported, including length, concatenation, 870 regular-expression matching, substrig operations, recognizers, etc. 871 If you use this logic, you are likely to find bugs in solvers themselves 872 as support is rather new: Please report. 873 874 * If unsat-core extraction is enabled, SBV now returns the unsat-core 875 directly with in a solver result. Thanks to Ara Adkins for the 876 suggestion. 877 878 * Add 'observe'. This function allows internal expressions to be 879 given values, which will be part of the satisfying model or 880 the counter-example upon model construction. Useful for tracking 881 expected/returned values. Also works with quickCheck. 882 883 * Revamp Haddock documentation, hopefully easier to follow now. 884 885 * Slightly modify the generated-C headers by removing whitespace. 886 This allows for certain "lint" rules to pass when SBV generated 887 code is used in conjunction with a larger code base. Thanks 888 to Greg Horn for the pull request. 889 890 * Improve implementation of 'svExp' to match that of '.^', making 891 it more defined when the exponent is constant. Thanks to Brian 892 Huffman for the patch. 893 894 * Export the underlying polynomial representation for algorithmic 895 reals from the Internals module for further user processing. 896 Thanks to Jan Path for the patch. 897 898### Version 7.6, Released 2018-03-18 899 900 * GHC 8.4.1 compatibility: Work around compilation issues. SBV 901 now compiles cleanly with GHC 8.4.1. 902 903 * Define and export sWordN, sWordN_, sIntN_, from the Dynamic 904 interface, which simplifies creation of variables of arbitrary 905 bit sizes. These are similar to sWord8, sInt8, etc.; except 906 they create dynamic counterparts that can be of arbitrary bit size. 907 908### Version 7.5, Released 2018-01-13 909 910 * Remove obsolete references to tactics in a few haddock comments. Thanks 911 to Matthew Pickering for reporting. 912 913 * Added logic Logic_NONE, to be used in cases where SBV should not 914 try to set the logic. This is useful when there is no viable value to 915 set, and the back-end solver doesn't understand the SMT-Lib convention 916 of using "ALL" as the logic name. (One example of this is the Yices 917 solver.) 918 919 * SBV now returns SMTException (instead of just calling error) in case 920 the backend solver responds with error message. The type SMTException 921 can be caught by the user programs, and it includes many fields as an 922 indication of what went wrong. (The command sent, what was expected, 923 what was seen, etc.) Note that if this exception is ever caught, the 924 backend solver is no longer alive: You should either just throw it, 925 or perform proper clean-up on your user code as required to set up 926 a new context. The provided show instance formats the exception nicely 927 for display purposes. See http://github.com/LeventErkok/sbv/issues/335 928 for details and thanks to Brian Huffman for reporting. 929 930 * SIntegral class now has Integral as a super-class, which ensures the 931 base-type it's used at is Integral. This was already true for all instances, 932 so we are just making it more explicit. 933 934 * Improve the implementation of .^ (exponentiation) to cover more cases, 935 in particular signed exponents are now OK so long as they are concrete 936 and positive, following Haskell convention. 937 938 * Removed the 'FromBits' class. Its functionality is now merged with the 939 new 'SFiniteBits' class, see below. 940 941 * Introduce 'SFiniteBits' class, which only incorporates finite-words in it, 942 i.e., SWord/SInt for 8-16-32-64. In particular it leaves out SInteger, 943 SFloat, SDouble, and SReal. Important in recognizing bit-vectors of 944 finite size, essentially. Here are the methods: 945 946 class (SymWord a, Num a, Bits a) => SFiniteBits a where 947 sFiniteBitSize :: SBV a -> Int -- ^ Bit size 948 lsb :: SBV a -> SBool -- ^ Least significant bit of a word, always stored at index 0. 949 msb :: SBV a -> SBool -- ^ Most significant bit of a word, always stored at the last position. 950 blastBE :: SBV a -> [SBool] -- ^ Big-endian blasting of a word into its bits. Also see the 'FromBits' class. 951 blastLE :: SBV a -> [SBool] -- ^ Little-endian blasting of a word into its bits. Also see the 'FromBits' class. 952 fromBitsBE :: [SBool] -> SBV a -- ^ Reconstruct from given bits, given in little-endian 953 fromBitsLE :: [SBool] -> SBV a -- ^ Reconstruct from given bits, given in little-endian 954 sTestBit :: SBV a -> Int -> SBool -- ^ Replacement for 'testBit', returning 'SBool' instead of 'Bool' 955 sExtractBits :: SBV a -> [Int] -> [SBool] -- ^ Variant of 'sTestBit', where we want to extract multiple bit positions. 956 sPopCount :: SBV a -> SWord8 -- ^ Variant of 'popCount', returning a symbolic value. 957 setBitTo :: SBV a -> Int -> SBool -> SBV a -- ^ A combo of 'setBit' and 'clearBit', when the bit to be set is symbolic. 958 fullAdder :: SBV a -> SBV a -> (SBool, SBV a) -- ^ Full adder, returns carry-out from the addition. Only for unsigned quantities. 959 fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a) -- ^ Full multiplier, returns both high and low-order bits. Only for unsigned quantities. 960 sCountLeadingZeros :: SBV a -> SWord8 -- ^ Count leading zeros in a word, big-endian interpretation 961 sCountTrailingZeros :: SBV a -> SWord8 -- ^ Count trailing zeros in a word, big-endian interpretation 962 963 Note that the functions 'sFiniteBitSize', 'sCountLeadingZeros', and 'sCountTrailingZeros' are 964 new. Others have existed in SBV before, we are just grouping them together now in this new class. 965 966 * Tightened certain signatures where SBV was too liberal, using the SFiniteBits class. New signatures are: 967 968 sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a -> SBV b -> SBV a 969 crc :: (SFiniteBits a, SFiniteBits b) => Int -> SBV a -> SBV b -> SBV b 970 readSTree :: (SFiniteBits i, SymWord e) => STree i e -> SBV i -> SBV e 971 writeSTree :: (SFiniteBits i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e 972 973 Thanks to Thomas DuBuisson for reporting. 974 975### Version 7.4, 2017-11-03 976 977 * Export queryDebug from the Control module, allowing custom queries to print 978 debugging messages with the verbose flag is set. 979 980 * Relax value-parsing to allow for non-standard output from solvers. For 981 instance, MathSAT/Yices prints reals as integers when they do not have a 982 fraction. We now support such cases, relaxing the standard slightly. Thanks 983 to Geoffrey Ramseyer for reporting. 984 985 * Fix optimization routines when applied to signed-bitvector goals. Thanks 986 to Anders Kaseorg for reporting. Since SMT-Lib does not distinguish between 987 signed and unsigned bit-vectors, we have to be careful when expressing goals 988 that are over signed values. See http://github.com/LeventErkok/sbv/issues/333 989 for details. 990 991### Version 7.3, 2017-09-06 992 993 * Query mode: Add support for arrays in query mode. Thanks to Brad Hardy for 994 providing the use-case and debugging help. 995 996 * Query mode: Add support for tables. (As used by 'select' calls.) 997 998### Version 7.2, 2017-08-29 999 1000 * Reworked implementation of shifts and rotates: When a signed quantity was 1001 being shifted right by more than its size, SBV used to return 0. Robert Dockins pointed 1002 out that the correct answer is actually -1 in such cases. The new implementation 1003 merges the dynamic and typed interfaces, and drops support for non-constant shifts 1004 of unbounded integers, which is not supported by SMTLib. Thanks to Robert for 1005 reporting the issue and identifying the root cause. 1006 1007 * Rework how quantifiers are handled: We now generate separate asserts for 1008 prefix-existentials. This allows for better (smaller) quantified code, while 1009 preserving semantics. 1010 1011 * Rework the interaction between quantifiers and optimization routines. 1012 Optimization routines now properly handle quantified formulas, so long as the 1013 quantified metric does not involve any universal quantification itself. Thanks 1014 to Matthew Danish for reporting the issue. 1015 1016 * Development/Infrastructure: Lots of work around the continuous integration 1017 for SBV. We now build/test on Linux/Mac/Windows on every commit. Thanks to 1018 Travis/Appveyor for providing free remote infrastructure. There are still 1019 gotchas and some reductions in tests due to host capacity issues. If you 1020 would like to be involved and improve the test suite, please get in touch! 1021 1022### Version 7.1, 2017-07-29 1023 1024 * Add support for 'getInterpolant' in Query mode. 1025 1026 * Support for SMT-results that can contain multi-line strings, which 1027 is rare but it does happen. Previously SBV incorrectly interpreted such 1028 responses to be erroneous. 1029 1030 * Many improvements to build infrastructure and code clean-up. 1031 1032 * Fix a bug in the implementation of `svSetBit`. Thanks to Robert Dockins 1033 for the report. 1034 1035### Version 7.0, 2017-07-19 1036 1037 * NB. SBV now requires GHC >= 8.0.1 to compile. If you are stuck with an older 1038 version of GHC, please get in contact. 1039 1040 * This is a major rewrite of the internals of SBV, and is a backwards compatibility 1041 breaking release. While we kept the top-level and most commonly used APIs the 1042 same (both types and semantics), much of the internals and advanced features 1043 have been rewritten to move SBV to a new model of execution: SBV no longer 1044 runs your program symbolically and calls the SMT solver afterwards. Instead, 1045 the interaction with the solver happens interleaved with the actual program execution. 1046 The motivation is to allow the end-users to send/receive arbitrary SMTLib 1047 commands to the solver, instead of the cooked-up recipes. SBV still provides 1048 all the recipes for its existing functionality, but users can now interact 1049 with the solver directly. See the module `Data.SBV.Control` for the main 1050 API, together with the new functions 'runSMT' and 'runSMTWith'. 1051 1052 * The 'Tactic' based solver control (introduced in v6.0) is completely removed, and 1053 is replaced by the above described mechanism which gives the user a lot of 1054 flexibility instead. Use queries for anything that required a tactic before. 1055 1056 * The call 'allSat' has been reworked so it performs only one call to the underlying 1057 solver and repeatedly issues check-sat to get new assignments. This differs from the 1058 previous implementation where we spun off a new call to the executable for each 1059 successive model. While this is more efficient and much more preferable, it also 1060 means that the results are no longer lazily computed: If there is an infinite number 1061 of solutions (or a very large number), you can no longer merely do a 'take' on the result. 1062 While this is inconvenient, it fits better with our new methodology of query based 1063 interaction. Note that the old behavior can be modeled, if required, by the user; by explicitly 1064 interleaving the calls to 'sat.' Furthermore, we now provide a new configuration 1065 parameter named 'allSatMaxModelCount' which can be used to limit the number models we 1066 seek. The default is to get all models, however long that might take. 1067 1068 * The Bridge modules (`Data.SBV.Bridge.Yices`, `Data.SBV.Bridge.Z3`) etc. are 1069 all removed. The bridge functionality was hardly used, where different solvers 1070 were much easier to access using the `with` functions. (Such as `proveWith`, 1071 `satWith` etc.) This should result in no loss of functionality, except for 1072 occasional explicit mention of solvers in your code, if you were using 1073 bridge modules to start with. 1074 1075 * Optimization routines have been changed to take a priority as an argument, (i.e., 1076 Lexicographic, Independent, etc.). The old method of supplying the priority 1077 via tactics is no longer supported. 1078 1079 * Pareto-front extraction has been reworked, reflecting the changes in Z3 for 1080 this functionality. Since pareto-fronts can be infinite in number, the user 1081 is now allowed to specify a "limit" to stop the solver from querying ad 1082 infinitum. If the limit is not specified, then sbv will query till it 1083 exhausts all the pareto-fronts, or till it runs out of memory in case there 1084 is an infinite number of them. 1085 1086 * Extraction of unsat-cores has changed. To use this feature, we now use 1087 custom queries. See `Data.SBV.Examples.Misc.UnsatCore` for an example. 1088 Old style of unsat-core extraction is no longer supported. 1089 1090 * The 'timing' option of SMTConfig has been reworked. Since we now start the 1091 solver immediately, it is no longer sensible to distinguish between "SBV" time, 1092 "translation" time etc. Instead, we print one simple "Elapsed" time if requested. 1093 If you need a detailed timing analysis, use the new 'transcript' option to 1094 SMTConfig: It will produce a file with precise timing intervals for each 1095 command issued to help you figure out how long each step took. 1096 1097 * The following functions have been reworked, so they now also return 1098 the time-elapsed for each solver: 1099 1100 satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)] 1101 satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult) 1102 proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)] 1103 proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult) 1104 1105 * Changed the way `satWithAny` and `proveWithAny` works. Previously, these 1106 two functions ran multiple solvers, and took the result of the first 1107 one to finish, killing all the others. In addition, they *waited* for 1108 the still-running solvers to finish cleaning-up, as sending a 'ThreadKilled' 1109 is usually not instantaneous. Furthermore, a solver might simply take 1110 its time! We now send the interrupt but do not wait for the process to 1111 actually terminate. In rare occasions this could create zombie processes 1112 if you use a solver that is not cooperating, but we have seen not insignificant 1113 speed-ups for regular usage due to ThreadKilled wait times being rather long. 1114 1115 * Configuration option `useLogic` is removed. If required, this should 1116 be done by a call to the new 'setLogic' function: 1117 1118 setLogic QF_NRA 1119 1120 * Configuration option `timeOut` is removed. This was rarely used, and the solver 1121 support was rather sketchy. We now have a better mechanism in the query mode 1122 for timeouts, where it really matters. Please get in touch if you relied on 1123 this old mechanism. Correspondingly, the functions `isTheorem`, `isSatisfiable`, 1124 `isTheoremWith` and `isSatisfiableWith` had their time-out arguments removed 1125 and return types simplified. 1126 1127 * The function 'isSatisfiableInCurrentPath' is removed. Proper queries should be used 1128 for what this function tentatively attempted to provide. Please get in touch 1129 if you relied on this function and want to restructure your code to use proper queries. 1130 1131 * Configuration option 'smtFile' is removed. Instead use 'transcript' now, which 1132 provides a much more detailed output that is directly loadable to a solver 1133 and has an accurate account of precisely what SBV sent. 1134 1135 * Enumerations are now much easier to use symbolically, with the addition 1136 of the template-haskell splice mkSymbolicEnumeration. See `Data/SBV/Examples/Misc/Enumerate.hs` 1137 for an example. 1138 1139 * Thanks to Kanishka Azimi, our external test suite is now run by 1140 Tasty! Kanishka modernized the test suite, and reworked the 1141 infrastructure that was showing its age. Thanks! 1142 1143 * The function pConstrain and the Data.SBV.Tools.ExpectedValue are 1144 removed. Probabilistic constraints were rarely used, and if 1145 necessary can be implemented outside of SBV. If you were using 1146 this feature, please get in contact. 1147 1148 * SArray and SFunArray has been reworked, and they no longer take 1149 and initial value. Similarly resetArray has been removed, as it 1150 did not really do what it advertised. If an initial value is needed, 1151 it is best to code this explicitly in your model. 1152 1153### Version 6.1, 2017-05-26 1154 1155 * Add support for unsat-core extraction. To use this feature, use 1156 the `namedConstraint` function: 1157 1158 namedConstraint :: String -> SBool -> Symbolic () 1159 1160 to associate a label to a constrain or a boolean term that 1161 can later be labeled by the backend solver as belonging to the 1162 unsat-core. 1163 1164 Unsat-cores are not enabled by default since they can be 1165 expensive; to use: 1166 1167 satWith z3{getUnsatCore=True} $ do ... 1168 1169 In the programmatic API, the function: 1170 1171 extractUnsatCore :: Modelable a => a -> Maybe [String] 1172 1173 can be used to programmatically extract the unsat-core. Note that 1174 backend solvers will only include the named expressions in the unsat-core, 1175 i.e., any unnamed yet part-of-the-core-unsat expressions will be missing; 1176 as speculated in the SMT-Lib document itself. 1177 1178 Currently, Z3, MathSAT, and CVC4 backends support unsat-cores. 1179 1180 (Thanks to Rohit Ramesh for the suggestion leading to this feature.) 1181 1182 * Added function `distinct`, which returns true if all the elements of the 1183 given list are different. This function replaces the old `allDifferent` 1184 function, which is now removed. The difference is that `distinct` will produce 1185 much better code for SMT-Lib. If you used `allDifferent` before, simply 1186 replacing it with `distinct` should work. 1187 1188 * Add support for pseudo-boolean operations: 1189 1190 pbAtMost :: [SBool] -> Int -> SBool 1191 pbAtLeast :: [SBool] -> Int -> SBool 1192 pbExactly :: [SBool] -> Int -> SBool 1193 pbLe :: [(Int, SBool)] -> Int -> SBool 1194 pbGe :: [(Int, SBool)] -> Int -> SBool 1195 pbEq :: [(Int, SBool)] -> Int -> SBool 1196 pbMutexed :: [SBool] -> SBool 1197 pbStronglyMutexed :: [SBool] -> SBool 1198 1199 These functions, while can be directly coded in SBV, produce better 1200 translations to SMTLib for more efficient solving of cardinality constraints. 1201 Currently, only Z3 supports pseudo-booleans directly. For all other solvers, 1202 SBV will translate these to equivalent terms that do not require special 1203 functions. 1204 1205 * The function getModel has been renamed to getAssignment. (The former name is 1206 now available as a query command.) 1207 1208 * Export `SolverCapabilities` from `Data.SBV.Internals`, in case users want access. 1209 1210 * Move code-generation facilities to `Data.SBV.Tools.CodeGen`, no longer exporting 1211 the relevant functions directly from `Data.SBV`. This could break existing code, 1212 but the fix should be as simple as `import Data.SBV.Tools.CodeGen`. 1213 1214 * Move the following two functions to `Data.SBV.Internals`: 1215 1216 compileToSMTLib 1217 generateSMTBenchmarks 1218 1219 If you use them, please `import Data.SBV.Internals`. 1220 1221 * Reorganized `EqSymbolic` and `EqOrd` classes to collect some of the 1222 similarly named function together. Users should see no impact due to this change. 1223 1224 1225### Version 6.0, 2017-05-07 1226 1227 * This is a backwards compatibility breaking release, hence the major version 1228 bump from 5.15 to 6.0: 1229 1230 - Most of existing code should work with no changes. 1231 - Old code relying on some features might require extra imports, 1232 since we no longer export some functionality directly from `Data.SBV`. 1233 This was done in order to reduce the number of exported items to 1234 avoid extra clutter. 1235 - Old optimization features are removed, as the new and much improved 1236 capabilities should be used instead. 1237 1238 * The next two bullets cover new features in SBV regarding optimization, based 1239 on the capabilities of the z3 SMT solver. With this release SBV gains the 1240 capability optimize objectives, and solve MaxSAT problems; by appropriately 1241 employing the corresponding capabilities in z3. A good review of these features 1242 as implemented by Z3, and thus what is available in SBV is given in this 1243 paper: http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf 1244 1245 * SBV now allows for real or integral valued metrics. Goals can be lexicographically 1246 (default), independently, or pareto-front optimized. Currently, only the z3 backend 1247 supports optimization routines. 1248 1249 Optimization can be done over bit-vector, real, and integer goals. The relevant 1250 functions are: 1251 1252 - `minimize`: Minimize a given arithmetic goal 1253 - `maximize`: Minimize a given arithmetic goal 1254 1255 For instance, a call of the form 1256 1257 minimize "name-of-goal" $ x + 2*y 1258 1259 Minimizes the arithmetic goal x+2*y, where x and y can be bit-vectors, reals, 1260 or integers. Such goals will be lexicographically optimized, i.e., in the order 1261 given. If there are multiple goals, then user can also ask for independent 1262 optimization results, or pareto-fronts. 1263 1264 Once the objectives are given, a top level call to `optimize` (similar to `prove` 1265 and `sat`) performs the optimization. 1266 1267 * SBV now implements soft-asserts. A soft assertion is a hint to the SMT solver that 1268 we would like a particular condition to hold if *possible*. That is, if there is 1269 a solution satisfying it, then we would like it to hold. However, if the set of 1270 constraints is unsatisfiable, then a soft-assertion can be violated by incurring 1271 a user-given numeric penalty to satisfy the remaining constraints. The solver then 1272 tries to minimize the penalty, i.e., satisfy as many of the soft-asserts as possible 1273 such that the total penalty for those that are not satisfied is minimized. 1274 1275 Note that `assertSoft` works well with optimization goals (minimize/maximize etc.), 1276 and are most useful when we are optimizing a metric and thus some of the constraints 1277 can be relaxed with a penalty to obtain a good solution. 1278 1279 * SBV no longer provides the old optimization routines, based on iterative and quantifier 1280 based methods. Those methods were rarely used, and are now superseded by the above 1281 mechanism. If the old code is needed, please contact for help: They can be resurrected 1282 in your own code if absolutely necessary. 1283 1284 * (NB. This feature is deprecated in 7.0, see above for its replacement.) 1285 SBV now implements tactics, which allow the user to navigate the proof process. 1286 This is an advanced feature that most users will have no need of, but can become 1287 handy when dealing with complicated problems. Users can, for instance, implement 1288 case-splitting in a proof to guide the underlying solver through. Here is the list 1289 of tactics implemented: 1290 1291 - `CaseSplit` : Case-split, with implicit coverage. Bool says whether we should be verbose. 1292 - `CheckCaseVacuity` : Should the case-splits be checked for vacuity? (Default: True.) 1293 - `ParallelCase` : Run case-splits in parallel. (Default: Sequential.) 1294 - `CheckConstrVacuity`: Should constraints be checked for vacuity? (Default: False.) 1295 - `StopAfter` : Time-out given to solver, in seconds. 1296 - `CheckUsing` : Invoke with check-sat-using command, instead of check-sat 1297 - `UseLogic` : Use this logic, a custom one can be specified too 1298 - `UseSolver` : Use this solver (z3, yices, etc.) 1299 - `OptimizePriority` : Specify priority for optimization: Lexicographic (default), Independent, or Pareto. 1300 1301 * Name-space clean-up. The following modules are no longer automatically exported 1302 from Data.SBV: 1303 1304 - `Data.SBV.Tools.ExpectedValue` (computing with expected values) 1305 - `Data.SBV.Tools.GenTest` (test case generation) 1306 - `Data.SBV.Tools.Polynomial` (polynomial arithmetic, CRCs etc.) 1307 - `Data.SBV.Tools.STree` (full symbolic binary trees) 1308 1309 To use the functionality of these modules, users must now explicitly import the corresponding 1310 module. Not other changes should be needed other than the explicit import. 1311 1312 * Changed the signatures of: 1313 1314 isSatisfiableInCurrentPath :: SBool -> Symbolic Bool 1315 svIsSatisfiableInCurrentPath :: SVal -> Symbolic Bool 1316 1317 to: 1318 1319 isSatisfiableInCurrentPath :: SBool -> Symbolic (Maybe SatResult) 1320 svIsSatisfiableInCurrentPath :: SVal -> Symbolic (Maybe SatResult) 1321 1322 which returns the result in case of SAT. This is more useful than before. This is 1323 backwards-compatibility breaking, but is more useful. (Requested by Jared Ziegler.) 1324 1325 * Add instance `Provable (Symbolic ())`, which simply stands for returning true 1326 for proof/sat purposes. This allows for simpler coding, as constrain/minimize/maximize 1327 calls (which return unit) can now be directly sat/prove processed, without needing 1328 a final call to return at the end. 1329 1330 * Add type synonym `Goal` (for `Symbolic ()`), in order to simplify type signatures 1331 1332 * SBV now properly adds check-sat commands and other directives in debugging output. 1333 1334 * New examples: 1335 - Data.SBV.Examples.Optimization.LinearOpt: Simple linear-optimization example. 1336 - Data.SBV.Examples.Optimization.Production: Scheduling machines in a shop 1337 - Data.SBV.Examples.Optimization.VM: Scheduling virtual-machines in a data-center 1338 1339### Version 5.15, 2017-01-30 1340 1341 * Bump up dependency on CrackNum >= 1.9, to get access to hexadecimal floats. 1342 * Improve time/tracking-print code. Thanks to Iavor Diatchki for the patch. 1343 1344### Version 5.14, 2017-01-12 1345 1346 * Bump up QuickCheck dependency to >= 2.9.2 to avoid the following quick-check 1347 bug <http://github.com/nick8325/quickcheck/issues/113>, which transitively impacted 1348 the quick-check as implemented by SBV. 1349 1350 * Generalize casts between integral-floats, using the rounding mode round-nearest-ties-to-even. 1351 Previously calls to sFromIntegral did not support conversion to floats since it needed 1352 a rounding mode. But it does make sense to support them with the default mode. If a different 1353 mode is needed, use the function 'toSFloat' as before, which takes an explicit rounding mode. 1354 1355### Version 5.13, 2016-10-29 1356 1357 * Fix broken links, thanks to Stephan Renatus for the patch. 1358 1359 * Code generation: Create directory path if it does not exist. Thanks to Robert Dockins 1360 for the patch. 1361 1362 * Generalize the type of sFromIntegral, dropping the Bits requirement. In turn, this 1363 allowed us to remove sIntegerToSReal, since sFromIntegral can be used instead. 1364 1365 * Add support for sRealToSInteger. (Essentially the floor function for SReal.) 1366 1367 * Several space-leaks fixed for better performance. Patch contributed by Robert Dockins. 1368 1369 * Improved Random instance for Rational. Thanks to Joe Leslie-Hurd for the idea. 1370 1371### Version 5.12, 2016-06-06 1372 1373 * Fix GHC8.0 compilation issues, and warning clean-up. Thanks to Adam Foltzer for the bulk 1374 of the work and Tom Sydney Kerckhove for the initial patch for 8.0 compatibility. 1375 1376 * Minor fix to printing models with floats when the base is 2/16, making sure the alignment 1377 is done properly accommodating for the crackNum output. 1378 1379 * Wait for external process to die on exception, to avoid spawning zombies. Thanks to 1380 Daniel Wagner for the patch. 1381 1382 * Fix hash-consed arrays: Previously we were caching based only on elements, which is not 1383 sufficient as you can have conflicts differing only on the address type, but same contents. 1384 Thanks to Brian Huffman for reporting and the corresponding patch. 1385 1386### Version 5.11, 2016-01-15 1387 1388 * Fix documentation issue; no functional changes 1389 1390### Version 5.10, 2016-01-14 1391 1392 * Documentation: Fix a bunch of dead http links. Thanks to Andres Sicard-Ramirez 1393 for reporting. 1394 1395 * Additions to the Dynamic API: 1396 1397 * svSetBit : set a given bit 1398 * svBlastLE, svBlastBE : Bit-blast to big/little endian 1399 * svWordFromLE, svWordFromBE: Unblast from big/little endian 1400 * svAddConstant : Add a constant to an SVal 1401 * svIncrement, svDecrement : Add/subtract 1 from an SVal 1402 1403### Version 5.9, 2016-01-05 1404 1405 * Default definition for 'symbolicMerge', which allows types that are 1406 instances of 'Generic' to have an automatically derivable merge (i.e., 1407 ite) instance. Thanks to Christian Conkle for the patch. 1408 1409 * Add support for "non-model-vars," where we can now tell SBV not 1410 to take into account certain variables from a model-building 1411 perspective. This comes handy in doing an `allSat` calls where 1412 there might be witness variables that we do not care the uniqueness 1413 for. See `Data/SBV/Examples/Misc/Auxiliary.hs` for an example, and 1414 the discussion in http://github.com/LeventErkok/sbv/issues/208 for 1415 motivation. 1416 1417 * Yices interface: If Reals are used, then pick the logic QF_UFLRA, instead 1418 of QF_AUFLIA. Unfortunately, logic selection remains tricky since the SMTLib 1419 story for logic selection is rather messy. Other solvers are not impacted 1420 by this change. 1421 1422### Version 5.8, 2016-01-01 1423 1424 * Fix some typos 1425 * Add 'svEnumFromThenTo' to the Dynamic interface, allowing dynamic construction 1426 of [x, y .. z] and [x .. y] when the involved values are concrete. 1427 * Add 'svExp' to the Dynamic interface, implementing exponentiation 1428 1429### Version 5.7, 2015-12-21 1430 1431 * Export `HasKind(..)` from the Dynamic interface. Thanks to Adam Foltzer for the patch. 1432 * More careful handling of SMT-Lib reserved names. 1433 * Update tested version of MathSAT to 5.3.9 1434 * Generalize `sShiftLeft`/`sShiftRight`/`sRotateLeft`/`sRotateRight` to work with signed 1435 shift/rotate amounts, where negative values revert the direction. Similar 1436 generalizations are also done for the dynamic variants. 1437 1438### Version 5.6, 2015-12-06 1439 1440 * Minor changes to how we print models: 1441 * Align by the type 1442 * Always print the type (previously we were skipping for Bool) 1443 1444 * Rework how SBV properties are quick-checked; much more usable and robust 1445 1446 * Provide a function `sbvQuickCheck`, which is essentially the same as 1447 quickCheck, except it also returns a boolean. Useful for the 1448 programmable API. (The dynamic version is called `svQuickCheck`.) 1449 1450 * Several changes/additions in support of the sbvPlugin development: 1451 * Data.SBV.Dynamic: Define/export `svFloat`/`svDouble`/`sReal`/`sNumerator`/`sDenominator` 1452 * Data.SBV.Internals: Export constructors of `Result`, `SMTModel`, 1453 and the function `showModel` 1454 * Simplify how Uninterpreted-types are internally represented. 1455 1456### Version 5.5, 2015-11-10 1457 1458 * This is essentially the same release as 5.4 below, except to allow SBV compile 1459 with GHC 7.8 series. Thanks to Adam Foltzer for the patch. 1460 1461### Version 5.4, 2015-11-09 1462 1463 * Add 'sAssert', which allows users to pepper their code with boolean conditions, much like 1464 the usual ASSERT calls. Note that the semantics of an 'sAssert' is that it is a NOOP, i.e., 1465 it simply returns its final argument. Use in coordination with 'safe' and 'safeWith', see below. 1466 1467 * Implement 'safe' and 'safeWith', which statically determine all calls to 'sAssert' 1468 being safe to execute. Any violations will be flagged. 1469 1470 * SBV->C: Translate 'sAssert' calls to dynamic checks in the generated C code. If this is 1471 not desired, use the 'cgIgnoreSAssert' function to turn it off. 1472 1473 * Add 'isSafe': Which converts a 'SafeResult' to a 'Bool', when we are only interested 1474 in a boolean result. 1475 1476 * Add Data/SBV/Examples/Misc/NoDiv0 to demonstrate the use of the 'safe' function. 1477 1478### Version 5.3, 2015-10-20 1479 1480 * Main point of this release to make SBV compile with GHC 7.8 again, to accommodate mainly 1481 for Cryptol. As Cryptol moves to GHC >= 7.10, we intend to remove the "compatibility" changes 1482 again. Thanks to Adam Foltzer for the patch. 1483 1484 * Minor mods to how bitvector equality/inequality are translated to SMTLib. No user visible 1485 impact. 1486 1487### Version 5.2, 2015-10-12 1488 1489 * Regression on 5.1: Fix a minor bug in base 2/16 printing where uninterpreted constants were 1490 not handled correctly. 1491 1492### Version 5.1, 2015-10-10 1493 1494 * fpMin, fpMax: If these functions receive +0/-0 as their two arguments, i.e., both 1495 zeros but alternating signs in any order, then SMTLib requires the output to be 1496 nondeterministically chosen. Previously, we fixed this result as +0 following the 1497 interpretation in Z3, but Z3 recently changed and now incorporates the nondeterministic 1498 output. SBV similarly changed to allow for non-determinism here. 1499 1500 * Change the types of the following Floating-point operations: 1501 1502 * sFloatAsSWord32, sFloatAsSWord32, blastSFloat, blastSDouble 1503 1504 These were previously coded as relations, since NaN values were not representable 1505 in the target domain uniquely. While it was OK, it was hard to use them. We now 1506 simply implement these as functions, and they are underspecified if the inputs 1507 are NaNs: In those cases, we simply get a symbolic output. The new types are: 1508 1509 * sFloatAsSWord32 :: SFloat -> SWord32 1510 * sDoubleAsSWord64 :: SDouble -> SWord64 1511 * blastSFloat :: SFloat -> (SBool, [SBool], [SBool]) 1512 * blastSDouble :: SDouble -> (SBool, [SBool], [SBool]) 1513 1514 * MathSAT backend: Use the SMTLib interpretation of fp.min/fp.max by passing the 1515 "-theory.fp.minmax_zero_mode=4" argument explicitly. 1516 1517 * Fix a bug in hash-consing of floating-point constants, where we were confusing +0 and 1518 -0 since we were using them as keys into the map though they compare equal. We now 1519 explicitly keep track of the negative-zero status to make sure this confusion does 1520 not arise. Note that this bug only exhibited itself in rare occurrences of both 1521 constants being present in a benchmark; a true corner case. Note that @NaN@ values 1522 are also interesting in this context: Since NaN /= NaN, we never hash-cons floating 1523 point constants that have the value NaN. But that is actually OK; it is a bit wasteful 1524 in case you have a lot of NaN constants around, but there is no soundness issue: We 1525 just waste a little bit of space. 1526 1527 * Remove the functions `allSatWithAny` and `allSatWithAll`. These two variants do *not* 1528 make sense when run with multiple solvers, as they internally sequentialize the solutions 1529 due to the nature of `allSat`. Not really needed anyhow; so removed. The variants 1530 `satWithAny/All` and `proveWithAny/All` are still available. 1531 1532 * Export SMTLibVersion from the library, forgotten export needed by Cryptol. Thanks to Adam 1533 Foltzer for the patch. 1534 1535 * Slightly modify model-outputs so the variables are aligned vertically. (Only matters 1536 if we have model-variable names that are of differing length.) 1537 1538 * Move to Travis-CI "docker" based infrastructure for builds 1539 1540 * Enable local builds to use the Herbie plugin. Currently SBV does not have any 1541 expressions that can benefit from Herbie, but it is nice to have this support in general. 1542 1543### Version 5.0, 2015-09-22 1544 1545 * Note: This is a backwards-compatibility breaking release, see below for details. 1546 1547 * SBV now requires GHC 7.10.1 or newer to be compiled, taking advantage of newer features/bug-fixes 1548 in GHC. If you really need SBV to compile with older GHCs, please get in touch. 1549 1550 * SBV no longer supports SMTLib1. We now exclusively use SMTLib2 for communicating with backend 1551 solvers. Strictly speaking, this means some loss in functionality: Uninterpreted-function models 1552 that we supported via Yices-1 are no longer available. In practice this facility was not really 1553 used, and required a very old version of Yices that was no longer supported by SRI and has 1554 lacked in other features. So, in reality this change should hardly matter for end-users. 1555 1556 * Added function `label`, which is useful in emitting comments around expressions. It is essentially 1557 a no-op, but does generate a comment with the given text in the SMT-Lib and C output, for diagnostic 1558 purposes. 1559 1560 * Added `sFromIntegral`: Conversions from all integral types (SInteger, SWord/SInts) between 1561 each other. Similar to the `fromIntegral` function of Haskell. These generate simple casts when 1562 used in code-generation to C, and thus are very efficient. 1563 1564 * SBV no longer supports the functions sBranch/sAssert, as we realized these functions can cause 1565 soundness issues under certain conditions. While the triggering scenarios are not common use-cases 1566 for these functions, we are opting for safety, and thus removing support. See 1567 http://github.com/LeventErkok/sbv/issues/180 for details; and see below for the new function 1568 'isSatisfiableInCurrentPath'. 1569 1570 * A new function 'isSatisfiableInCurrentPath' is added, which checks for satisfiability during a 1571 symbolic simulation run. This function can be used as the basis of sBranch/sAssert like functionality 1572 if needed. The difference is that this is a much lower level call, and also exposes the fact that 1573 the result is in the 'Symbolic' monad (which avoids the soundness issue). Of course, the new type 1574 makes it less useful as it will not be a drop-in replacement for if-then-else like structure. Intended 1575 to be used by tools built on top of SBV, as opposed to end-users. 1576 1577 * SBV no longer implements the 'SignCast' class, as its functionality is replaced by the 'sFromIntegral' 1578 function. Programs using the functions 'signCast' and 'unsignCast' should simply replace both 1579 with calls to 'sFromIntegral'. (Note that extra type-annotations might be necessary, similar to 1580 the uses of the 'fromIntegral' function in Haskell.) 1581 1582 * Backend solver related changes: 1583 1584 * Yices: Upgraded to work with Yices release 2.4.1. Note that earlier versions of Yices 1585 are *not* supported. 1586 1587 * Boolector: Upgraded to work with new Boolector release 2.0.7. Note that earlier versions 1588 of Boolector are *not* supported. 1589 1590 * MathSAT: Upgraded to work with latest release 5.3.7. Note that earlier versions of MathSAT 1591 are *not* supported (due to a buffering issue in MathSAT itself.) 1592 1593 * MathSAT: Enabled floating-point support in MathSAT. 1594 1595 * New examples: 1596 1597 * Add Data.SBV.Examples.Puzzles.Birthday, which solves the Cheryl-Birthday problem that 1598 went viral in April 2015. Turns out really easy to solve for SMT, but the formalization 1599 of the problem is still interesting as an exercise in formal reasoning. 1600 1601 * Add Data.SBV.Examples.Puzzles.SendMoreMoney, which solves the classic send + more = money 1602 problem. Really a trivial example, but included since it is pretty much the hello-world for 1603 basic constraint solving. 1604 1605 * Add Data.SBV.Examples.Puzzles.Fish, which solves a typical logic puzzle; finding the unique 1606 solution to a set of assertions made about a bunch of people, their pets, beverage choices, 1607 etc. Not particularly interesting, but could be fun to play around with for modeling purposes. 1608 1609 * Add Data.SBV.Examples.BitPrecise.MultMask, which demonstrates the use of the bitvector 1610 solver to an interesting bit-shuffling problem. 1611 1612 * Rework floating-point arithmetic, and add missing floating-point operations: 1613 1614 * fpRem : remainder 1615 * fpRoundToIntegral: truncating round 1616 * fpMin : min 1617 * fpMax : max 1618 * fpIsEqualObject : FP equality as object (i.e., NaN equals NaN, +0 does not equal -0, etc.) 1619 1620 This brings SBV up-to par with everything supported by the SMT-Lib FP theory. 1621 1622 * Add the IEEEFloatConvertable class, which provides conversions to/from Floats and other types. (i.e., 1623 value conversions from all other types to Floats and Doubles; and back.) 1624 1625 * Add SWord32/SWord64 to/from SFloat/SDouble conversions, as bit-pattern reinterpretation; using the 1626 IEEE754 interchange format. The functions are: sWord32AsSFloat, sWord64AsSDouble, sFloatAsSWord32, 1627 sDoubleAsSWord64. Note that the sWord32AsSFloat and sWord64ToSDouble are regular functions, but 1628 sFloatToSWord32 and sDoubleToSWord64 are "relations", since NaN values are not uniquely convertable. 1629 1630 * Add 'sExtractBits', which takes a list of indices to extract bits from, essentially 1631 equivalent to 'map sTestBit'. 1632 1633 * Rename a set of symbolic functions for consistency. Here are the old/new names: 1634 1635 * sbvTestBit --> sTestBit 1636 * sbvPopCount --> sPopCount 1637 * sbvShiftLeft --> sShiftLeft 1638 * sbvShiftRight --> sShiftRight 1639 * sbvRotateLeft --> sRotateLeft 1640 * sbvRotateRight --> sRotateRight 1641 * sbvSignedShiftArithRight --> sSignedShiftArithRight 1642 1643 * Rename all FP recognizers to be in sync with FP operations. Here are the old/new names: 1644 1645 * isNormalFP --> fpIsNormal 1646 * isSubnormalFP --> fpIsSubnormal 1647 * isZeroFP --> fpIsZero 1648 * isInfiniteFP --> fpIsInfinite 1649 * isNaNFP --> fpIsNaN 1650 * isNegativeFP --> fpIsNegative 1651 * isPositiveFP --> fpIsPositive 1652 * isNegativeZeroFP --> fpIsNegativeZero 1653 * isPositiveZeroFP --> fpIsPositiveZero 1654 * isPointFP --> fpIsPoint 1655 1656 * Lots of other work around floating-point, test cases, reorg, etc. 1657 1658 * Introduce shorter variants for rounding modes: sRNE, sRNA, sRTP, sRTN, sRTZ; 1659 aliases for sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, 1660 sRoundTowardNegative, and sRoundTowardZero; respectively. 1661 1662### Version 4.4, 2015-04-13 1663 1664 * Hook-up crackNum package; so counter-examples involving floats and 1665 doubles can be printed in detail when the printBase is chosen to be 1666 2 or 16. (With base 10, we still get the simple output.) 1667 1668 ``` 1669 Prelude Data.SBV> satWith z3{printBase=2} $ \x -> x .== (2::SFloat) 1670 Satisfiable. Model: 1671 s0 = 2.0 :: Float 1672 3 2 1 0 1673 1 09876543 21098765432109876543210 1674 S ---E8--- ----------F23---------- 1675 Binary: 0 10000000 00000000000000000000000 1676 Hex: 4000 0000 1677 Precision: SP 1678 Sign: Positive 1679 Exponent: 1 (Stored: 128, Bias: 127) 1680 Value: +2.0 (NORMAL) 1681 ``` 1682 1683 * Change how we print type info; for models instead of SType just print Type (i.e., 1684 for SWord8, instead print Word8) which makes more sense and is more consistent. 1685 This change should be mostly relevant as how we see the counter-example output. 1686 1687 * Fix long standing bug #75, where we now support arrays with Boolean source/targets. 1688 This is not a very commonly used case, but by letting the solver pick the logic, 1689 we now allow arrays to be uniformly supported. 1690 1691### Version 4.3, 2015-04-10 1692 1693 * Introduce Data.SBV.Dynamic, by Brian Huffman. This is mostly an internal 1694 reorg of the SBV codebase, and end-users should not be impacted by the 1695 changes. The introduction of the Dynamic SBV variant (i.e., one that does 1696 not mandate a phantom type as in `SBV Word8` etc. allows library writers 1697 more flexibility as they deal with arbitrary bit-vector sizes. The main 1698 customer of these changes are the Cryptol language and the associated 1699 toolset, but other developers building on top of SBV can find it useful 1700 as well. NB: The "strongly-typed" aspect of SBV is still the main way 1701 end-users should interact with SBV, and nothing changed in that respect! 1702 1703 * Add symbolic variants of floating-point rounding-modes for convenience 1704 1705 * Rename toSReal to sIntegerToSReal, which captures the intent more clearly 1706 1707 * Code clean-up: remove mbMinBound/mbMaxBound thus allowing less calls to 1708 unliteral. Contributed by Brian Huffman. 1709 1710 * Introduce FP conversion functions: 1711 1712 * Between SReal and SFloat/SDouble 1713 * fpToSReal 1714 * sRealToSFloat 1715 * sRealToSDouble 1716 * Between SWord32 and SFloat 1717 * sWord32ToSFloat 1718 * sFloatToSWord32 1719 * Between SWord64 and SDouble. (Relational, due to non-unique NaNs) 1720 * sWord64ToSDouble 1721 * sDoubleToSWord64 1722 * From float to sign/exponent/mantissa fields: (Relational, due to non-unique NaNs) 1723 * blastSFloat 1724 * blastSDouble 1725 1726 * Rework floating point classifiers. Remove isSNaN and isFPPoint (both renamed), 1727 and add the following new recognizers: 1728 1729 * isNormalFP 1730 * isSubnormalFP 1731 * isZeroFP 1732 * isInfiniteFP 1733 * isNaNFP 1734 * isNegativeFP 1735 * isPositiveFP 1736 * isNegativeZeroFP 1737 * isPositiveZeroFP 1738 * isPointFP (corresponds to a real number, i.e., neither NaN nor infinity) 1739 1740 * Re-implement sbvTestBit, by Brian Huffman. This version is much faster at large 1741 word sizes, as it avoids the costly mask generation. 1742 1743 * Code changes to suppress warnings with GHC7.10. General clean-up. 1744 1745### Version 4.2, 2015-03-17 1746 1747 * Add exponentiation (.^). Thanks to Daniel Wagner for contributing the code! 1748 1749 * Better handling of SBV_$SOLVER_OPTIONS, in particular keeping track of 1750 proper quoting in environment variables. Thanks to Adam Foltzer for 1751 the patch! 1752 1753 * Silence some hlint/ghci warnings. Thanks to Trevor Elliott for the patch! 1754 1755 * Haddock documentation fixes, improvements, etc. 1756 1757 * Change ABC default option string to %blast; "&sweep -C 5000; &syn4; &cec -s -m -C 2000" 1758 which seems to give good results. Use SBV_ABC_OPTIONS environment variable (or 1759 via abc.rc file and a combination of SBV_ABC_OPTIONS) to experiment. 1760 1761### Version 4.1, 2015-03-06 1762 1763 * Add support for the ABC solver from Berkeley. Thanks to Adam Foltzer 1764 for the required infrastructure! See: http://www.eecs.berkeley.edu/~alanmi/abc/ 1765 And Alan Mishchenko for adding infrastructure to ABC to work with SBV. 1766 1767 * Upgrade the Boolector connection to use a SMT-Lib2 based interaction. NB. You 1768 need at least Boolector 2.0.6 installed! 1769 1770 * Tracking changes in the SMT-Lib floating-point theory. If you are 1771 using symbolic floating-point types (i.e., SFloat and SDouble), then 1772 you should upgrade to this version and also get a very latest (unstable) 1773 Z3 release. See http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml 1774 for details. 1775 1776 * Introduce a new class, 'RoundingFloat', which supports floating-point 1777 operations with arbitrary rounding-modes. Note that Haskell only allows 1778 RoundNearestTiesToAway, but with SBV, we get all 5 IEEE754 rounding-modes 1779 and all the basic operations ('fpAdd', 'fpMul', 'fpDiv', etc.) with these 1780 modes. 1781 1782 * Allow Floating-Point RoundingMode to be symbolic as well 1783 1784 * Improve the example `Data/SBV/Examples/Misc/Floating.hs` to include 1785 rounding-mode based addition example. 1786 1787 * Changes required to make SBV compile with GHC 7.10; mostly around instance 1788 NFData declarations. Thanks to Iavor Diatchki for the patch. 1789 1790 * Export a few extra symbols from the Internals module (mainly for 1791 Cryptol usage.) 1792 1793### Version 4.0, 2015-01-22 1794 1795This release mainly contains contributions from Brian Huffman, allowing 1796end-users to define new symbolic types, such as Word4, that SBV does not 1797natively support. When GHC gets type-level literals, we shall most likely 1798incorporate arbitrary bit-sized vectors and ints using this mechanism, 1799but in the interim, this release provides a means for the users to introduce 1800individual instances. 1801 1802 * Modifications to support arbitrary bit-sized vectors; 1803 These changes have been contributed by Brian Huffman 1804 of Galois. Thanks Brian. 1805 * A new example `Data/SBV/Examples/Misc/Word4.hs` showing 1806 how users can add new symbolic types. 1807 * Support for rotate-left/rotate-right with variable 1808 rotation amounts. (From Brian Huffman.) 1809 1810### Version 3.5, 2015-01-15 1811 1812This release is mainly adding support for enumerated types in Haskell being 1813translated to their symbolic counterparts; instead of going completely 1814uninterpreted. 1815 1816 * Keep track of data-type details for uninterpreted sorts. 1817 * Rework the U2Bridge example to use enumerated types. 1818 * The "Uninterpreted" name no longer makes sense with this change, so 1819 rework the relevant names to ensure proper internal naming. 1820 * Add Data/SBV/Examples/Misc/Enumerate.hs as an example for demonstrating 1821 how enumerations are translated. 1822 * Fix a long-standing bug in the implementation of select when 1823 translated as SMT-Lib tables. (Github issue #103.) Thanks to 1824 Brian Huffman for reporting. 1825 1826### Version 3.4, 2014-12-21 1827 1828 * This release is mainly addressing floating-point changes in SMT-Lib. 1829 1830 * Track changes in the QF_FPA logic standard; new constants and alike. If you are 1831 using the floating-point logic, then you need a relatively new version of Z3 1832 installed (4.3.3 or newer). 1833 1834 * Add unary-negation as an explicit operator. Previously, we merely used the "0-x" 1835 semantics; but with floating point, this does not hold as 0-0 is 0, and is not -0! 1836 (Note that negative-zero is a valid floating point value, that is different than 1837 positive-zero; yet it compares equal to it. Sigh..) 1838 1839 * Similarly, add abs as a native method; to make sure we map it to fp.abs for 1840 floating point values. 1841 1842 * Test suite improvements 1843 1844### Version 3.3, 2014-12-05 1845 1846 * Implement 'safe' and 'safeWith', which statically determine all calls to 'sAssert' 1847 being safe to execute. This way, users can pepper their programs with liberal 1848 calls to 'sAssert' and check they are all safe in one go without further worry. 1849 1850 * Robustify the interface to external solvers, by making sure we catch cases where 1851 the external solver might exist but not be runnable (library dependency missing, 1852 for example). It is impossible to be absolutely foolproof, but we now catch a 1853 few more cases and fail gracefully. 1854 1855### Version 3.2, 2014-11-18 1856 1857 * Implement 'sAssert'. This adds conditional symbolic simulation, by ensuring arbitrary 1858 boolean conditions hold during simulation; similar to ASSERT calls in other languages. 1859 Note that failures will be detected at symbolic-simulation time, i.e., each assert will 1860 generate a call to the external solver to ensure that the condition is never violated. 1861 If violation is possible the user will get an error, indicating the failure conditions. 1862 1863 * Also implement 'sAssertCont' which allows for a programmatic way to extract/display results 1864 for consumers of 'sAssert'. While the latter simply calls 'error' in case of an assertion 1865 violation, the 'sAssertCont' variant takes a continuation which can be used to program 1866 how the results should be interpreted/displayed. (This is useful for libraries built on top of 1867 SBV.) Note that the type of the continuation is such that execution should still stop, i.e., 1868 once an assertion violation is detected, symbolic simulation will never continue. 1869 1870 * Rework/simplify the 'Mergeable' class to make sure 'sBranch' is sufficiently lazy 1871 in case of structural merges. The original implementation was only 1872 lazy at the Word instance, but not at lists/tuples etc. Thanks to Brian Huffman 1873 for reporting this bug. 1874 1875 * Add a few constant-folding optimizations for 'sDiv' and 'sRem' 1876 1877 * Boolector: Modify output parser to conform to the new Boolector output format. This 1878 means that you need at least v2.0.0 of Boolector installed if you want to use that 1879 particular solver. 1880 1881 * Fix long-standing translation bug regarding boolean Ord class comparisons. (i.e., 1882 'False > True' etc.) While Haskell allows for this, SMT-Lib does not; and hence 1883 we have to be careful in translating. Thanks to Brian Huffman for reporting. 1884 1885 * C code generation: Correctly translate square-root and fusedMA functions to C. 1886 1887### Version 3.1, 2014-07-12 1888 1889 NB: GHC 7.8.1 and 7.8.2 has a serious bug <http://ghc.haskell.org/trac/ghc/ticket/9078> 1890 that causes SBV to crash under heavy/repeated calls. The bug is addressed 1891 in GHC 7.8.3; so upgrading to GHC 7.8.3 is essential for using SBV! 1892 1893 New features/bug-fixes in v3.1: 1894 1895 * Using multiple-SMT solvers in parallel: 1896 * Added functions that let the user run multiple solvers, using asynchronous 1897 threads. All results can be obtained (proveWithAll, proveWithAny, satWithAll), 1898 or SBV can return the fastest result (satWithAny, allSatWithAll, allSatWithAny). 1899 These functions are good for playing with multiple-solvers, especially on 1900 machines with multiple-cores. 1901 * Add function: sbvAvailableSolvers; which returns the list of solvers currently 1902 available, as installed on the machine we are running. (Not the list that SBV 1903 supports, but those that are actually available at run-time.) This function 1904 is useful with the multi-solve API. 1905 * Implement sBranch: 1906 * sBranch is a variant of 'ite' that consults the external 1907 SMT solver to see if a given branch condition is satisfiable 1908 before evaluating it. This can make certain otherwise recursive 1909 and thus not-symbolically-terminating inputs amenable to symbolic 1910 simulation, if termination can be established this way. Needless 1911 to say, this problem is always decidable as far as SBV programs 1912 are concerned, but it does not mean the decision procedure is cheap! 1913 Use with care. 1914 * sBranchTimeOut config parameter can be used to curtail long runs when 1915 sBranch is used. Of course, if time-out happens, SBV will 1916 assume the branch is feasible, in which case symbolic-termination 1917 may come back to bite you.) 1918 * New API: 1919 * Add predicate 'isSNaN' which allows testing 'SFloat'/'SDouble' values 1920 for nan-ness. This is similar to the Prelude function 'isNaN', except 1921 the Prelude version requires a RealFrac instance, which unfortunately is 1922 not currently implementable for cases. (Requires trigonometric functions etc.) 1923 Thus, we provide 'isSNaN' separately (along with the already existing 1924 'isFPPoint') to simplify reasoning with floating-point. 1925 * Examples: 1926 * Add Data/SBV/Examples/Misc/SBranch.hs, to illustrate the use of sBranch. 1927 * Bug fixes: 1928 * Fix pipe-blocking issue, which exhibited itself in the presence of 1929 large numbers of variables (> 10K or so). See github issue #86. Thanks 1930 to Philipp Meyer for the fine report. 1931 * Misc: 1932 * Add missing SFloat/SDouble instances for SatModel class 1933 * Explicitly support KBool as a kind, separating it from `KUnbounded False 1`. 1934 Thanks to Brian Huffman for contributing the changes. This should have no 1935 user-visible impact, but comes in handy for internal reasons. 1936 1937### Version 3.0, 2014-02-16 1938 1939 * Support for floating-point numbers: 1940 * Preliminary support for IEEE-floating point arithmetic, introducing 1941 the types `SFloat` and `SDouble`. The support is still quite new, 1942 and Z3 is the only solver that currently features a solver for 1943 this logic. Likely to have bugs, both at the SBV level, and at the 1944 Z3 level; so any bug reports are welcome! 1945 * New backend solvers: 1946 * SBV now supports MathSAT from Fondazione Bruno Kessler and 1947 DISI-University of Trento. See: http://mathsat.fbk.eu/ 1948 * Support all-sat calls in the presence of uninterpreted sorts: 1949 * Implement better support for `allSat` in the presence of uninterpreted 1950 sorts. Previously, SBV simply rejected running `allSat` queries 1951 in the presence of uninterpreted sorts, since it was not possible 1952 to generate a refuting model. The model returned by the SMT solver 1953 is simply not usable, since it names constants that is not visible 1954 in a subsequent run. Eric Seidel came up with the idea that we can 1955 actually compute equivalence classes based on a produced model, and 1956 assert the constraint that the new model should disallow the previously 1957 found equivalence classes instead. The idea seems to work well 1958 in practice, and there is also an example program demonstrating 1959 the functionality: Examples/Uninterpreted/UISortAllSat.hs 1960 * Programmable model extraction improvements: 1961 * Add functions `getModelDictionary` and `getModelDictionaries`, which 1962 provide low-level access to models returned from SMT solvers. Former 1963 for `sat` and `prove` calls, latter for `allSat` calls. Together with 1964 the exported utils from the `Data.SBV.Internals` module, this should 1965 allow for expert users to dissect the models returned and do fancier 1966 programming on top of SBV. 1967 * Add `getModelValue`, `getModelValues`, `getModelUninterpretedValue`, and 1968 `getModelUninterpretedValues`; which further aid in model value 1969 extraction. 1970 * Other: 1971 * Allow users to specify the SMT-Lib logic to use, if necessary. SBV will 1972 still pick the logic automatically, but users can now override that choice. 1973 Comes in handy when playing with custom logics. 1974 * Bug fixes: 1975 * Address allsat-laziness issue (#78 in github issue tracker). Essentially, 1976 simplify how all-sat is called so we can avoid calling the solver for 1977 solutions that are not needed. Thanks to Eric Seidel for reporting. 1978 * Examples: 1979 * Add Data/SBV/Examples/Misc/ModelExtract.hs as a simple example for 1980 programmable model extraction and usage. 1981 * Add Data/SBV/Examples/Misc/Floating.hs for some FP examples. 1982 * Use the AUFLIA logic in Examples.Existentials.Diophantine which helps 1983 z3 complete the proof quickly. (The BV logics take too long for this problem.) 1984 1985### Version 2.10, 2013-03-22 1986 1987 * Add support for the Boolector SMT solver 1988 * See: http://fmv.jku.at/boolector/ 1989 * Use `import Data.SBV.Bridge.Boolector` to use Boolector from SBV 1990 * Boolector supports QF_BV (with an without arrays). In the last 1991 SMT-Lib competition it won both bit-vector categories. It is definitely 1992 worth trying it out for bitvector problems. 1993 * Changes to the library: 1994 * Generalize types of `allDifferent` and `allEqual` to take 1995 arbitrary EqSymbolic values. (Previously was just over SBV values.) 1996 * Add `inRange` predicate, which checks if a value is bounded within 1997 two others. 1998 * Add `sElem` predicate, which checks for symbolic membership 1999 * Add `fullAdder`: Returns the carry-over as a separate boolean bit. 2000 * Add `fullMultiplier`: Returns both the lower and higher bits resulting 2001 from multiplication. 2002 * Use the SMT-Lib Bool sort to represent SBool, instead of bit-vectors of length 1. 2003 While this is an under-the-hood mechanism that should be user-transparent, it 2004 turns out that one can no longer write axioms that return booleans in a direct 2005 way due to this translation. This change makes it easier to write axioms that 2006 utilize booleans as there is now a 1-to-1 match. (Suggested by Thomas DuBuisson.) 2007 * Solvers changes: 2008 * Z3: Update to the new parameter naming schema of Z3. This implies that 2009 you need to have a really recent version of Z3 installed, something 2010 in the Z3-4.3 series. 2011 * Examples: 2012 * Add Examples/Uninterpreted/Shannon.hs: Demonstrating Shannon expansion, 2013 boolean derivatives, etc. 2014 * Bug-fixes: 2015 * Gracefully handle the case if the backend-SMT solver does not put anything 2016 in stdout. (Reported by Thomas DuBuisson.) 2017 * Handle uninterpreted sort values, if they happen to be only created via 2018 function calls, as opposed to being inputs. (Reported by Thomas DuBuisson.) 2019 2020### Version 2.9, 2013-01-02 2021 2022 * Add support for the CVC4 SMT solver from Stanford: <https://cvc4.github.io/> 2023 NB. Z3 remains the default solver for SBV. To use CVC4, use the 2024 *With variants of the interface (i.e., proveWith, satWith, ..) 2025 by passing cvc4 as the solver argument. (Similarly, use 'yices' 2026 as the argument for the *With functions for invoking yices.) 2027 * Latest release of Yices calls the SMT-Lib based solver executable 2028 yices-smt. Updated the default value of the executable to have this 2029 name for ease of use. 2030 * Add an extra boolean flag to compileToSMTLib and generateSMTBenchmarks 2031 functions to control if the translation should keep the query as is 2032 (for SAT cases), or negate it (for PROVE cases). Previously, this value 2033 was hard-coded to do the PROVE case only. 2034 * Add bridge modules, to simplify use of different solvers. You can now say: 2035 2036 import Data.SBV.Bridge.CVC4 2037 import Data.SBV.Bridge.Yices 2038 import Data.SBV.Bridge.Z3 2039 2040 to pick the appropriate default solver. if you simply 'import Data.SBV', then 2041 you will get the default SMT solver, which is currently Z3. The value 2042 'defaultSMTSolver' refers to z3 (currently), and 'sbvCurrentSolver' refers 2043 to the chosen solver as determined by the imported module. (The latter is 2044 useful for modifying options to the SMT solver in an solver-agnostic way.) 2045 * Various improvements to Z3 model parsing routines. 2046 * New web page for SBV: http://leventerkok.github.com/sbv/ is now online. 2047 2048### Version 2.8, 2012-11-29 2049 2050 * Rename the SNum class to SIntegral, and make it index over regular 2051 types. This makes it much more useful, simplifying coding of 2052 polymorphic symbolic functions over integral types, which is 2053 the common case. 2054 * Add the functions: 2055 * sbvShiftLeft 2056 * sbvShiftRight 2057 which can accommodate unsigned symbolic shift amounts. Note that 2058 one cannot use the Haskell shiftL/shiftR functions from the Bits class since 2059 they are hard-wired to take 'Int' values as the shift amounts only. 2060 * Add a new function 'sbvArithShiftRight', which is the same as 2061 a shift-right, except it uses the MSB of the input as the bit to fill 2062 in (instead of always filling in with 0 bits). Note that this is 2063 the same as shiftRight for signed values, but differs from a shiftRight 2064 when the input is unsigned. (There is no Haskell analogue of this 2065 function, as Haskell shiftR is always arithmetic for signed 2066 types and logical for unsigned ones.) This variant is designed for 2067 use cases when one uses the underlying unsigned SMT-Lib representation 2068 to implement custom signed operations, for instance. 2069 * Several typo fixes. 2070 2071### Version 2.7, 2012-10-21 2072 2073 * Add missing QuickCheck instance for SReal 2074 * When dealing with concrete SReals, make sure to operate 2075 only on exact algebraic reals on the Haskell side, leaving 2076 true algebraic reals (i.e., those that are roots of polynomials 2077 that cannot be expressed as a rational) symbolic. This avoids 2078 issues with functions that we cannot implement directly on 2079 the Haskell side, like exact square-roots. 2080 * Documentation tweaks, typo fixes etc. 2081 * Rename BVDivisible class to SDivisible; since SInteger 2082 is also an instance of this class, and SDivisible is a 2083 more appropriate name to start with. Also add sQuot and sRem 2084 methods; along with sDivMod, sDiv, and sMod, with usual 2085 semantics. 2086 * Improve test suite, adding many constant-folding tests 2087 and start using cabal based tests (--enable-tests option.) 2088 2089### Versions 2.4, 2.5, and 2.6: Around mid October 2012 2090 2091 * Workaround issues related hackage compilation, in particular to the 2092 problem with the new containers package release, which does provide 2093 an NFData instance for sequences. 2094 * Add explicit Num requirements when necessary, as the Bits class 2095 no longer does this. 2096 * Remove dependency on the hackage package strict-concurrency, as 2097 hackage can no longer compile it due to some dependency mismatch. 2098 * Add forgotten Real class instance for the type 'AlgReal' 2099 * Stop putting bounds on hackage dependencies, as they cause 2100 more trouble then they actually help. (See the discussion 2101 here: <http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html>.) 2102 2103### Version 2.3, 2012-07-20 2104 2105 * Maintenance release, no new features. 2106 * Tweak cabal dependencies to avoid using packages that are newer 2107 than those that come with ghc-7.4.2. Apparently this is a no-no 2108 that breaks many things, see the discussion in this thread: 2109 http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html 2110 In particular, the use of containers >= 0.5 is *not* OK until we have 2111 a version of GHC that comes with that version. 2112 2113### Version 2.2, 2012-07-17 2114 2115 * Maintenance release, no new features. 2116 * Update cabal dependencies, in particular fix the 2117 regression with respect to latest version of the 2118 containers package. 2119 2120### Version 2.1, 2012-05-24 2121 2122 * Library: 2123 * Add support for uninterpreted sorts, together with user defined 2124 domain axioms. See Data.SBV.Examples.Uninterpreted.Sort 2125 and Data.SBV.Examples.Uninterpreted.Deduce for basic examples of 2126 this feature. 2127 * Add support for C code-generation with SReals. The user picks 2128 one of 3 possible C types for the SReal type: CgFloat, CgDouble 2129 or CgLongDouble, using the function cgSRealType. Naturally, the 2130 resulting C program will suffer a loss of precision, as it will 2131 be subject to IEE-754 rounding as implied by the underlying type. 2132 * Add toSReal :: SInteger -> SReal, which can be used to promote 2133 symbolic integers to reals. Comes handy in mixed integer/real 2134 computations. 2135 * Examples: 2136 * Recast the dog-cat-mouse example to use the solver over reals. 2137 * Add Data.SBV.Examples.Uninterpreted.Sort, and 2138 Data.SBV.Examples.Uninterpreted.Deduce 2139 for illustrating uninterpreted sorts and axioms. 2140 2141### Version 2.0, 2012-05-10 2142 2143 This is a major release of SBV, adding support for symbolic algebraic reals: SReal. 2144 See http://en.wikipedia.org/wiki/Algebraic_number for details. In brief, algebraic 2145 reals are solutions to univariate polynomials with rational coefficients. The arithmetic 2146 on algebraic reals is precise, with no approximation errors. Note that algebraic reals 2147 are a proper subset of all reals, in particular transcendental numbers are not 2148 representable in this way. (For instance, "sqrt 2" is algebraic, but pi, e are not.) 2149 However, algebraic reals is a superset of rationals, so SBV now also supports symbolic 2150 rationals as well. 2151 2152 You *should* use Z3 v4.0 when working with real numbers. While the interface will 2153 work with older versions of Z3 (or other SMT solvers in general), it uses Z3 2154 root-obj construct to retrieve and query algebraic reals. 2155 2156 While SReal values have infinite precision, printing such values is not trivial since 2157 we might need an infinite number of digits if the result happens to be irrational. The 2158 user controls printing precision, by specifying how many digits after the decimal point 2159 should be printed. The default number of decimal digits to print is 10. (See the 2160 'printRealPrec' field of SMT-solver configuration.) 2161 2162 The acronym SBV used to stand for Symbolic Bit Vectors. However, SBV has grown beyond 2163 bit-vectors, especially with the addition of support for SInteger and SReal types and 2164 other code-generation utilities. Therefore, "SMT Based Verification" is now a better fit 2165 for the expansion of the acronym SBV. 2166 2167 Other notable changes in the library: 2168 2169 * Add functions s[TYPE] and s[TYPE]s for each symbolic type we support (i.e., 2170 sBool, sBools, sWord8, sWord8s, etc.), to create symbolic variables of the 2171 right kind. Strictly speaking these are just synonyms for 'free' 2172 and 'mapM free' (plural versions), so they are not adding any additional 2173 power. Except, they are specialized at their respective types, and might be 2174 easier to remember. 2175 * Add function solve, which is merely a synonym for (return . bAnd), but 2176 it simplifies expressing problems. 2177 * Add class SNum, which simplifies writing polymorphic code over symbolic values 2178 * Increase haddock coverage metrics 2179 * Major code refactoring around symbolic kinds 2180 * SMTLib2: Emit ":produce-models" call before setting the logic, as required 2181 by the SMT-Lib2 standard. [Patch provided by arrowdodger on github, thanks!] 2182 2183 Bugs fixed: 2184 2185 * [Performance] Use a much simpler default definition for "select": While the 2186 older version (based on binary search on the bits of the indexer) was correct, 2187 it created unnecessarily big expressions. Since SBV does not have a notion 2188 of concrete subwords, the binary-search trick was not bringing any advantage 2189 in any case. Instead, we now simply use a linear walk over the elements. 2190 2191 Examples: 2192 2193 * Change dog-cat-mouse example to use SInteger for the counts 2194 * Add merge-sort example: Data.SBV.Examples.BitPrecise.MergeSort 2195 * Add diophantine solver example: Data.SBV.Examples.Existentials.Diophantine 2196 2197### Version 1.4, 2012-05-10 2198 2199 * Interim release for test purposes 2200 2201### Version 1.3, 2012-02-25 2202 2203 * Workaround cabal/hackage issue, functionally the same as release 2204 1.2 below 2205 2206### Version 1.2, 2012-02-25 2207 2208 Library: 2209 2210 * Add a hook so users can add custom script segments for SMT solvers. The new 2211 "solverTweaks" field in the SMTConfig data-type can be used for this purpose. 2212 The need for this came about due to the need to workaround a Z3 v3.2 issue 2213 detailed below: 2214 http://stackoverflow.com/questions/9426420/soundness-issue-with-integer-bv-mixed-benchmarks 2215 As a consequence, mixed Integer/BV problems can cause soundness issues in Z3 2216 and does in SBV. Unfortunately, it is too severe for SBV to add the workaround 2217 option, as it slows down the solver as a side effect as well. Thus, we are 2218 making this optionally available if/when needed. (Note that the work-around 2219 should not be necessary with Z3 v3.3; which is not released yet.) 2220 * Other minor clean-up 2221 2222### Version 1.1, 2012-02-14 2223 2224 Library: 2225 2226 * Rename bitValue to sbvTestBit 2227 * Add sbvPopCount 2228 * Add a custom implementation of 'popCount' for the Bits class 2229 instance of SBV (GHC >= 7.4.1 only) 2230 * Add 'sbvCheckSolverInstallation', which can be used to check 2231 that the given solver is installed and good to go. 2232 * Add 'generateSMTBenchmarks', simplifying the generation of 2233 SMTLib benchmarks for offline sharing. 2234 2235### Version 1.0, 2012-02-13 2236 2237 Library: 2238 2239 * Z3 is now the "default" SMT solver. Yices is still available, but 2240 has to be specifically selected. (Use satWith, allSatWith, proveWith, etc.) 2241 * Better handling of the pConstrain probability threshold for test 2242 case generation and quickCheck purposes. 2243 * Add 'renderTest', which accompanies 'genTest' to render test 2244 vectors as Haskell/C/Forte program segments. 2245 * Add 'expectedValue' which can compute the expected value of 2246 a symbolic value under the given constraints. Useful for statistical 2247 analysis and probability computations. 2248 * When saturating provable values, use forAll_ for proofs and forSome_ 2249 for sat/allSat. (Previously we were allways using forAll_, which is 2250 not incorrect but less intuitive.) 2251 * add function: 2252 extractModels :: SatModel a => AllSatResult -> [a] 2253 which simplifies accessing allSat results greatly. 2254 2255 Code-generation: 2256 2257 * add "cgGenerateMakefile" which allows the user to choose if SBV 2258 should generate a Makefile. (default: True) 2259 2260 Other 2261 2262 * Changes to make it compile with GHC 7.4.1. 2263 2264### Version 0.9.24, 2011-12-28 2265 2266 Library: 2267 2268 * Add "forSome," analogous to "forAll." (The name "exists" would've 2269 been better, but it's already taken.) This is not as useful as 2270 one might think as forAll and forSome do not nest, as an inner 2271 application of one pushes its argument to a Predicate, making 2272 the outer one useless, but it is nonetheless useful by itself. 2273 * Add a "Modelable" class, which simplifies model extraction. 2274 * Add support for quick-check at the "Symbolic SBool" level. Previously 2275 SBV only allowed functions returning SBool to be quick-checked, which 2276 forced a certain style of coding. In particular with the addition 2277 of quantifiers, the new coding style mostly puts the top-level 2278 expressions in the Symbolic monad, which were not quick-checkable 2279 before. With new support, the quickCheck, prove, sat, and allSat 2280 commands are all interchangeable with obvious meanings. 2281 * Add support for concrete test case generation, see the genTest function. 2282 * Improve optimize routines and add support for iterative optimization. 2283 * Add "constrain", simplifying conjunctive constraints, especially 2284 useful for adding constraints at variable generation time via 2285 forall/exists. Note that the interpretation of such constraints 2286 is different for genTest and quickCheck functions, where constraints 2287 will be used for appropriately filtering acceptable test values 2288 in those two cases. 2289 * Add "pConstrain", which probabilistically adds constraints. This 2290 is useful for quickCheck and genTest functions for filtering acceptable 2291 test values. (Calls to pConstrain will be rejected for sat/prove calls.) 2292 * Add "isVacuous" which can be used to check that the constraints added 2293 via constrain are satisfiable. This is useful to prevent vacuous passes, 2294 i.e., when a proof is not just passing because the constraints imposed 2295 are inconsistent. (Also added accompanying isVacuousWith.) 2296 * Add "free" and "free_", analogous to "forall/forall_" and "exists/exists_" 2297 The difference is that free behaves universally in a proof context, while 2298 it behaves existentially in a sat context. This allows us to express 2299 properties more succinctly, since the intended semantics is usually this 2300 way depending on the context. (i.e., in a proof, we want our variables 2301 universal, in a sat call existential.) Of course, exists/forall are still 2302 available when mixed quantifiers are needed, or when the user wants to 2303 be explicit about the quantifiers. 2304 2305 Examples 2306 2307 * Add Data/SBV/Examples/Puzzles/Coins.hs. (Shows the usage of "constrain".) 2308 2309 Dependencies 2310 2311 * Bump up random package dependency to 1.0.1.1 (from 1.0.0.2) 2312 2313 Internal 2314 2315 * Major reorganization of files to and build infrastructure to 2316 decrease build times and better layout 2317 * Get rid of custom Setup.hs, just use simple build. The extra work 2318 was not worth the complexity. 2319 2320### Version 0.9.23, 2011-12-05 2321 2322 Library: 2323 2324 * Add support for SInteger, the type of signed unbounded integer 2325 values. SBV can now prove theorems about unbounded numbers, 2326 following the semantics of Haskell Integer type. (Requires z3 to 2327 be used as the backend solver.) 2328 * Add functions 'optimize', 'maximize', and 'minimize' that can 2329 be used to find optimal solutions to given constraints with 2330 respect to a given cost function. 2331 * Add 'cgUninterpret', which simplifies code generation when we want 2332 to use an alternate definition in the target language (i.e., C). This 2333 is important for efficient code generation, when we want to 2334 take advantage of native libraries available in the target platform. 2335 2336 Other: 2337 2338 * Change getModel to return a tuple in the success case, where 2339 the first component is a boolean indicating whether the model 2340 is "potential." This is used to indicate that the solver 2341 actually returned "unknown" for the problem and the model 2342 might therefore be bogus. Note that we did not need this before 2343 since we only supported bounded bit-vectors, which has a decidable 2344 theory. With the addition of unbounded Integers and quantifiers, the 2345 solvers can now return unknown. This should still be rare in practice, 2346 but can happen with the use of non-linear constructs. (i.e., 2347 multiplication of two variables.) 2348 2349### Version 0.9.22, 2011-11-13 2350 2351 The major change in this release is the support for quantifiers. The 2352 SBV library *no* longer assumes all variables are universals in a proof, 2353 (and correspondingly existential in a sat) call. Instead, the user 2354 marks free-variables appropriately using forall/exists functions, and the 2355 solver translates them accordingly. Note that this is a non-backwards 2356 compatible change in sat calls, as the semantics of formulas is essentially 2357 changing. While this is unfortunate, it is more uniform and simpler to understand 2358 in general. 2359 2360 This release also adds support for the Z3 solver, which is the main 2361 SMT-solver used for solving formulas involving quantifiers. More formally, 2362 we use the new AUFBV/ABV/UFBV logics when quantifiers are involved. Also, 2363 the communication with Z3 is now done via SMT-Lib2 format. Eventually 2364 the SMTLib1 connection will be severed. 2365 2366 The other main change is the support for C code generation with 2367 uninterpreted functions enabling users to interface with external 2368 C functions defined elsewhere. See below for details. 2369 2370 Other changes: 2371 2372 Code: 2373 2374 * Change getModel, so it returns an Either value to indicate 2375 something went wrong; instead of throwing an error 2376 * Add support for computing CRCs directly (without needing 2377 polynomial division). 2378 2379 Code generation: 2380 2381 * Add "cgGenerateDriver" function, which can be used to turn 2382 on/off driver program generation. Default is to generate 2383 a driver. (Issue "cgGenerateDriver False" to skip the driver.) 2384 For a library, a driver will be generated if any of the 2385 constituent parts has a driver. Otherwise it will be skipped. 2386 * Fix a bug in C code generation where "Not" over booleans were 2387 incorrectly getting translated due to need for masking. 2388 * Add support for compilation with uninterpreted functions. Users 2389 can now specify the corresponding C code and SBV will simply 2390 call the "native" functions instead of generating it. This 2391 enables interfacing with other C programs. See the functions: 2392 cgAddPrototype, cgAddDecl, cgAddLDFlags 2393 2394 Examples: 2395 2396 * Add CRC polynomial generation example via existentials 2397 * Add USB CRC code generation example, both via polynomials and using the internal CRC functionality 2398 2399### Version 0.9.21, 2011-08-05 2400 2401 Code generation: 2402 2403 * Allow for inclusion of user makefiles 2404 * Allow for CCFLAGS to be set by the user 2405 * Other minor clean-up 2406 2407### Version 0.9.20, 2011-06-05 2408 2409 Regression on 0.9.19; add missing file to cabal 2410 2411### Version 0.9.19, 2011-06-05 2412 2413 2414 * Add SignCast class for conversion between signed/unsigned 2415 quantities for same-sized bit-vectors 2416 * Add full-binary trees that can be indexed symbolically (STree). The 2417 advantage of this type is that the reads and writes take 2418 logarithmic time. Suitable for implementing faster symbolic look-up. 2419 * Expose HasSignAndSize class through Data.SBV.Internals 2420 * Many minor improvements, file re-orgs 2421 2422Examples: 2423 2424 * Add sentence-counting example 2425 * Add an implementation of RC4 2426 2427### Version 0.9.18, 2011-04-07 2428 2429Code: 2430 2431 * Re-engineer code-generation, and compilation to C. 2432 In particular, allow arrays of inputs to be specified, 2433 both as function arguments and output reference values. 2434 * Add support for generation of generation of C-libraries, 2435 allowing code generation for a set of functions that 2436 work together. 2437 2438Examples: 2439 2440 * Update code-generation examples to use the new API. 2441 * Include a library-generation example for doing 128-bit 2442 AES encryption 2443 2444### Version 0.9.17, 2011-03-29 2445 2446Code: 2447 2448 * Simplify and reorganize the test suite 2449 2450Examples: 2451 2452 * Improve AES decryption example, by using 2453 table-lookups in InvMixColumns. 2454 2455### Version 0.9.16, 2011-03-28 2456 2457Code: 2458 2459 * Further optimizations on Bits instance of SBV 2460 2461Examples: 2462 2463 * Add AES algorithm as an example, showing how 2464 encryption algorithms are particularly suitable 2465 for use with the code-generator 2466 2467### Version 0.9.15, 2011-03-24 2468 2469Bug fixes: 2470 2471 * Fix rotateL/rotateR instances on concrete 2472 words. Previous versions was bogus since 2473 it relied on the Integer instance, which 2474 does the wrong thing after normalization. 2475 * Fix conversion of signed numbers from bits, 2476 previous version did not handle twos 2477 complement layout correctly 2478 2479Testing: 2480 2481 * Add a sleuth of concrete test cases on 2482 arithmetic to catch bugs. (There are many 2483 of them, ~30K, but they run quickly.) 2484 2485### Version 0.9.14, 2011-03-19 2486 2487 * Re-implement sharing using Stable names, inspired 2488 by the Data.Reify techniques. This avoids tricks 2489 with unsafe memory stashing, and hence is safe. 2490 Thus, issues with respect to CAFs are now resolved. 2491 2492### Version 0.9.13, 2011-03-16 2493 2494Bug fixes: 2495 2496 * Make sure SBool short-cut evaluations are done 2497 as early as possible, as these help with coding 2498 recursion-depth based algorithms, when dealing 2499 with symbolic termination issues. 2500 2501Examples: 2502 2503 * Add fibonacci code-generation example, original 2504 code by Lee Pike. 2505 * Add a GCD code-generation/verification example 2506 2507### Version 0.9.12, 2011-03-10 2508 2509New features: 2510 2511 * Add support for compilation to C 2512 * Add a mechanism for offline saving of SMT-Lib files 2513 2514Bug fixes: 2515 2516 * Output naming bug, reported by Josef Svenningsson 2517 * Specification bug in Legatos multiplier example 2518 2519### Version 0.9.11, 2011-02-16 2520 2521 * Make ghc-7.0 happy, minor re-org on the cabal file/Setup.hs 2522 2523### Version 0.9.10, 2011-02-15 2524 2525 * Integrate commits from Iavor: Generalize SBVs to keep 2526 track the integer directly without resorting to different 2527 leaf types 2528 * Remove the unnecessary CLC instruction from the Legato example 2529 * More tests 2530 2531### Version 0.9.9, 2011-01-23 2532 2533 * Support for user-defined SMT-Lib axioms to be 2534 specified for uninterpreted constants/functions 2535 * Move to using doctest style inline tests 2536 2537### Version 0.9.8, 2011-01-22 2538 2539 * Better support for uninterpreted-functions 2540 * Support counter-examples with SArrays 2541 * Ladner-Fischer scheme example 2542 * Documentation updates 2543 2544### Version 0.9.7, 2011-01-18 2545 2546 * First stable public hackage release 2547 2548### Versions 0.0.0 - 0.9.6, Mid 2010 through early 2011 2549 2550 * Basic infrastructure, design exploration 2551