All Versions
89
Latest Version
Avg Release Cycle
51 days
Latest Release
1124 days ago

Changelog History
Page 6

  • v4.1 Changes

    March 06, 2015

    • Add support for the ABC solver from Berkeley. Thanks to Adam Foltzer for the required infrastructure! See: http://www.eecs.berkeley.edu/~alanmi/abc/ And Alan Mishchenko for adding infrastructure to ABC to work with SBV.

    • Upgrade the Boolector connection to use a SMT-Lib2 based interaction. NB. You need at least Boolector 2.0.6 installed!

    • Tracking changes in the SMT-Lib floating-point theory. If you are using symbolic floating-point types (i.e., SFloat and SDouble), then you should upgrade to this version and also get a very latest (unstable) Z3 release. See http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml for details.

    • Introduce a new class, 'RoundingFloat', which supports floating-point operations with arbitrary rounding-modes. Note that Haskell only allows RoundNearestTiesToAway, but with SBV, we get all 5 IEEE754 rounding-modes and all the basic operations ('fpAdd', 'fpMul', 'fpDiv', etc.) with these modes.

    • Allow Floating-Point RoundingMode to be symbolic as well

    • Improve the example Data/SBV/Examples/Misc/Floating.hs to include rounding-mode based addition example.

    • Changes required to make SBV compile with GHC 7.10; mostly around instance NFData declarations. Thanks to Iavor Diatchki for the patch.

    • Export a few extra symbols from the Internals module (mainly for Cryptol usage.)

  • v4.0 Changes

    January 22, 2015

    🚀 This release mainly contains contributions from Brian Huffman, allowing end-users to define new symbolic types, such as Word4, that SBV does not 👍 natively support. When GHC gets type-level literals, we shall most likely incorporate arbitrary bit-sized vectors and ints using this mechanism, 🚀 but in the interim, this release provides a means for the users to introduce individual instances.

    • Modifications to support arbitrary bit-sized vectors; These changes have been contributed by Brian Huffman of Galois. Thanks Brian.
    • A new example Data/SBV/Examples/Misc/Word4.hs showing how users can add new symbolic types.
    • Support for rotate-left/rotate-right with variable rotation amounts. (From Brian Huffman.)

  • v3.5 Changes

    January 15, 2015

    🚀 This release is mainly adding support for enumerated types in Haskell being translated to their symbolic counterparts; instead of going completely uninterpreted.

    • Keep track of data-type details for uninterpreted sorts.
    • Rework the U2Bridge example to use enumerated types.
    • The "Uninterpreted" name no longer makes sense with this change, so rework the relevant names to ensure proper internal naming.
    • Add Data/SBV/Examples/Misc/Enumerate.hs as an example for demonstrating how enumerations are translated.
    • Fix a long-standing bug in the implementation of select when translated as SMT-Lib tables. (Github issue #103.) Thanks to Brian Huffman for reporting.

  • v3.4 Changes

    December 21, 2014

    • This release is mainly addressing floating-point changes in SMT-Lib.

      • Track changes in the QF_FPA logic standard; new constants and alike. If you are using the floating-point logic, then you need a relatively new version of Z3 installed (4.3.3 or newer).
      • Add unary-negation as an explicit operator. Previously, we merely used the "0-x" semantics; but with floating point, this does not hold as 0-0 is 0, and is not -0! (Note that negative-zero is a valid floating point value, that is different than positive-zero; yet it compares equal to it. Sigh..)
      • Similarly, add abs as a native method; to make sure we map it to fp.abs for floating point values.
      • Test suite improvements

  • v3.3 Changes

    December 05, 2014

    • Implement 'safe' and 'safeWith', which statically determine all calls to 'sAssert' being safe to execute. This way, users can pepper their programs with liberal calls to 'sAssert' and check they are all safe in one go without further worry.

    • Robustify the interface to external solvers, by making sure we catch cases where the external solver might exist but not be runnable (library dependency missing, for example). It is impossible to be absolutely foolproof, but we now catch a few more cases and fail gracefully.

  • v3.2 Changes

    November 18, 2014

    • Implement 'sAssert'. This adds conditional symbolic simulation, by ensuring arbitrary boolean conditions hold during simulation; similar to ASSERT calls in other languages. Note that failures will be detected at symbolic-simulation time, i.e., each assert will generate a call to the external solver to ensure that the condition is never violated. If violation is possible the user will get an error, indicating the failure conditions.

    • Also implement 'sAssertCont' which allows for a programmatic way to extract/display results for consumers of 'sAssert'. While the latter simply calls 'error' in case of an assertion violation, the 'sAssertCont' variant takes a continuation which can be used to program how the results should be interpreted/displayed. (This is useful for libraries built on top of SBV.) Note that the type of the continuation is such that execution should still stop, i.e., once an assertion violation is detected, symbolic simulation will never continue.

    • Rework/simplify the 'Mergeable' class to make sure 'sBranch' is sufficiently lazy in case of structural merges. The original implementation was only lazy at the Word instance, but not at lists/tuples etc. Thanks to Brian Huffman for reporting this bug.

    • Add a few constant-folding optimizations for 'sDiv' and 'sRem'

    • Boolector: Modify output parser to conform to the new Boolector output format. This means that you need at least v2.0.0 of Boolector installed if you want to use that particular solver.

    • Fix long-standing translation bug regarding boolean Ord class comparisons. (i.e., 'False > True' etc.) While Haskell allows for this, SMT-Lib does not; and hence we have to be careful in translating. Thanks to Brian Huffman for reporting.

    • C code generation: Correctly translate square-root and fusedMA functions to C.

  • v3.1 Changes

    July 12, 2014

    NB: GHC 7.8.1 and 7.8.2 has a serious bug http://ghc.haskell.org/trac/ghc/ticket/9078 that causes SBV to crash under heavy/repeated calls. The bug is addressed in GHC 7.8.3; so upgrading to GHC 7.8.3 is essential for using SBV!

    New features/bug-fixes in v3.1:

    • Using multiple-SMT solvers in parallel:
      • Added functions that let the user run multiple solvers, using asynchronous threads. All results can be obtained (proveWithAll, proveWithAny, satWithAll), or SBV can return the fastest result (satWithAny, allSatWithAll, allSatWithAny). These functions are good for playing with multiple-solvers, especially on machines with multiple-cores.
      • Add function: sbvAvailableSolvers; which returns the list of solvers currently available, as installed on the machine we are running. (Not the list that SBV supports, but those that are actually available at run-time.) This function is useful with the multi-solve API.
    • Implement sBranch:
      • sBranch is a variant of 'ite' that consults the external SMT solver to see if a given branch condition is satisfiable before evaluating it. This can make certain otherwise recursive and thus not-symbolically-terminating inputs amenable to symbolic simulation, if termination can be established this way. Needless to say, this problem is always decidable as far as SBV programs are concerned, but it does not mean the decision procedure is cheap! Use with care.
      • sBranchTimeOut config parameter can be used to curtail long runs when sBranch is used. Of course, if time-out happens, SBV will assume the branch is feasible, in which case symbolic-termination may come back to bite you.)
    • New API:
      • Add predicate 'isSNaN' which allows testing 'SFloat'/'SDouble' values for nan-ness. This is similar to the Prelude function 'isNaN', except the Prelude version requires a RealFrac instance, which unfortunately is not currently implementable for cases. (Requires trigonometric functions etc.) Thus, we provide 'isSNaN' separately (along with the already existing 'isFPPoint') to simplify reasoning with floating-point.
    • Examples:
      • Add Data/SBV/Examples/Misc/SBranch.hs, to illustrate the use of sBranch.
    • Bug fixes:
      • Fix pipe-blocking issue, which exhibited itself in the presence of large numbers of variables (> 10K or so). See github issue #86. Thanks to Philipp Meyer for the fine report.
    • Misc:
      • Add missing SFloat/SDouble instances for SatModel class
      • Explicitly support KBool as a kind, separating it from KUnbounded False 1. Thanks to Brian Huffman for contributing the changes. This should have no user-visible impact, but comes in handy for internal reasons.

  • v3.0 Changes

    February 16, 2014
    • Support for floating-point numbers:
      • Preliminary support for IEEE-floating point arithmetic, introducing the types SFloat and SDouble. The support is still quite new, and Z3 is the only solver that currently features a solver for this logic. Likely to have bugs, both at the SBV level, and at the Z3 level; so any bug reports are welcome!
    • New backend solvers:
      • SBV now supports MathSAT from Fondazione Bruno Kessler and DISI-University of Trento. See: http://mathsat.fbk.eu/
    • Support all-sat calls in the presence of uninterpreted sorts:
      • Implement better support for allSat in the presence of uninterpreted sorts. Previously, SBV simply rejected running allSat queries in the presence of uninterpreted sorts, since it was not possible to generate a refuting model. The model returned by the SMT solver is simply not usable, since it names constants that is not visible in a subsequent run. Eric Seidel came up with the idea that we can actually compute equivalence classes based on a produced model, and assert the constraint that the new model should disallow the previously found equivalence classes instead. The idea seems to work well in practice, and there is also an example program demonstrating the functionality: Examples/Uninterpreted/UISortAllSat.hs
    • Programmable model extraction improvements:
      • Add functions getModelDictionary and getModelDictionaries, which provide low-level access to models returned from SMT solvers. Former for sat and prove calls, latter for allSat calls. Together with the exported utils from the Data.SBV.Internals module, this should allow for expert users to dissect the models returned and do fancier programming on top of SBV.
      • Add getModelValue, getModelValues, getModelUninterpretedValue, and getModelUninterpretedValues; which further aid in model value extraction.
    • Other:
      • Allow users to specify the SMT-Lib logic to use, if necessary. SBV will still pick the logic automatically, but users can now override that choice. Comes in handy when playing with custom logics.
    • Bug fixes:
      • Address allsat-laziness issue (#78 in github issue tracker). Essentially, simplify how all-sat is called so we can avoid calling the solver for solutions that are not needed. Thanks to Eric Seidel for reporting.
    • Examples:
      • Add Data/SBV/Examples/Misc/ModelExtract.hs as a simple example for programmable model extraction and usage.
      • Add Data/SBV/Examples/Misc/Floating.hs for some FP examples.
      • Use the AUFLIA logic in Examples.Existentials.Diophantine which helps z3 complete the proof quickly. (The BV logics take too long for this problem.)

  • v2.10 Changes

    March 22, 2013
    • Add support for the Boolector SMT solver
      • See: http://fmv.jku.at/boolector/
      • Use import Data.SBV.Bridge.Boolector to use Boolector from SBV
      • Boolector supports QF_BV (with an without arrays). In the last SMT-Lib competition it won both bit-vector categories. It is definitely worth trying it out for bitvector problems.
    • Changes to the library:
      • Generalize types of allDifferent and allEqual to take arbitrary EqSymbolic values. (Previously was just over SBV values.)
      • Add inRange predicate, which checks if a value is bounded within two others.
      • Add sElem predicate, which checks for symbolic membership
      • Add fullAdder: Returns the carry-over as a separate boolean bit.
      • Add fullMultiplier: Returns both the lower and higher bits resulting from multiplication.
      • Use the SMT-Lib Bool sort to represent SBool, instead of bit-vectors of length 1. While this is an under-the-hood mechanism that should be user-transparent, it turns out that one can no longer write axioms that return booleans in a direct way due to this translation. This change makes it easier to write axioms that utilize booleans as there is now a 1-to-1 match. (Suggested by Thomas DuBuisson.)
    • Solvers changes:
      • Z3: Update to the new parameter naming schema of Z3. This implies that you need to have a really recent version of Z3 installed, something in the Z3-4.3 series.
    • Examples:
      • Add Examples/Uninterpreted/Shannon.hs: Demonstrating Shannon expansion, boolean derivatives, etc.
    • Bug-fixes:
      • Gracefully handle the case if the backend-SMT solver does not put anything in stdout. (Reported by Thomas DuBuisson.)
      • Handle uninterpreted sort values, if they happen to be only created via function calls, as opposed to being inputs. (Reported by Thomas DuBuisson.)

  • v2.9 Changes

    January 02, 2013
    • Add support for the CVC4 SMT solver from Stanford: https://cvc4.github.io/ NB. Z3 remains the default solver for SBV. To use CVC4, use the *With variants of the interface (i.e., proveWith, satWith, ..) by passing cvc4 as the solver argument. (Similarly, use 'yices' as the argument for the *With functions for invoking yices.)
    • Latest release of Yices calls the SMT-Lib based solver executable yices-smt. Updated the default value of the executable to have this name for ease of use.
    • Add an extra boolean flag to compileToSMTLib and generateSMTBenchmarks functions to control if the translation should keep the query as is (for SAT cases), or negate it (for PROVE cases). Previously, this value was hard-coded to do the PROVE case only.

    • Add bridge modules, to simplify use of different solvers. You can now say:

        import Data.SBV.Bridge.CVC4
  import Data.SBV.Bridge.Yices
  import Data.SBV.Bridge.Z3

      to pick the appropriate default solver. if you simply 'import Data.SBV', then you will get the default SMT solver, which is currently Z3. The value 'defaultSMTSolver' refers to z3 (currently), and 'sbvCurrentSolver' refers to the chosen solver as determined by the imported module. (The latter is useful for modifying options to the SMT solver in an solver-agnostic way.)

    • Various improvements to Z3 model parsing routines.

    • New web page for SBV: http://leventerkok.github.com/sbv/ is now online.