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
andallEqual
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.)
- Generalize types of
- 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.)
- Add support for the Boolector SMT solver