sbv v2.10 Release Notes

Release Date: 2013-03-22 // about 11 years ago
    • 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.)