Skip to content
Commits on Feb 14, 2013
Commits on Jan 2, 2013
  1. Release 2.9

    committed
  2. Release 2.9

    committed
Commits on Dec 29, 2012
  1. Copyright year updates etc.

    committed
Commits on Dec 24, 2012
  1. Add 'sbvCurrentSolver' variable

    committed
    Allows writing solver-agnostic code, by appropriately referring to the
    solver in scope.
Commits on Dec 21, 2012
  1. Allow smt-Lib compilation to take a sat/prove parameter

    committed
    The compileToSMTLib and generateSMTBenchmarks functions translated the
    properties as if they were passed as an argument to 'prove', i.e., by
    negating the goal and asking the SMT solver if this negation is
    unsatisfiable. This commit allows users to specify whether they want
    compilation to be done in the SAT style (i.e., direct), or PROVE style
    (i.e., negated), by providing an extra boolean flag.
    
    Addresses issue #56.
Commits on Dec 20, 2012
  1. Add support for CVC4

    committed
    Latest release of Yices for SMT-Lib is called "yices-smt".. Fix the
    default value accordingly.
Commits on Nov 29, 2012
  1. Release 2.8

    committed
Commits on Nov 28, 2012
  1. Add shift functions that can take symbolic quantities

    committed
    In particular, added:
    
      sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight
    
    These take unsigned symbolic quantities as shift amounts.
  2. Update release notes

    committed
Commits on Oct 21, 2012
  1. Release 2.7

    committed
Commits on Oct 20, 2012
  1. Release 2.6

    committed
Commits on Oct 19, 2012
  1. Release 2.5

    committed
    Remove dependency on strict-concurrency package, as it causes hackage
    compilations to break.
  2. Release 2.4

    committed
Commits on Oct 16, 2012
  1. make sure rational-checks are done on concrete AlgReals

    committed
    When we process an AlgReal on the Haskell side, it's not sufficient
    that this value is concrete. It should also be something that Haskell
    can process, i.e., not a true real number that cannot be processed as a
    rational. This commit makes sure proper checks are done to satisfy this
    constraint, otherwise treating a given concrete real value as symbolic
    as far as constant folding is concerned.
Commits on Sep 9, 2012
  1. updated

    committed
Commits on Sep 8, 2012
  1. avoid Haskell's overflow in the test-suite

    committed
    minBound `divMod` (-1) overflows in Haskell for signed bounded types..
    So, avoid those cases.
Commits on Aug 29, 2012
  1. Add sDivMod

    committed
  2. BVDivisible -> SDivisible

    committed
Commits on Jul 20, 2012
  1. Release 2.3

    committed
    Dial down cabal dependencies, in particular we cannot depend on *newer* versions of packages then those that come with the latest ghc.. See the discussion in:
    
         http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html
Commits on Jul 17, 2012
Commits on May 30, 2012
  1. mark up new version (2.2)

    committed
Commits on May 24, 2012
  1. ready for release 2.1

    committed
Commits on May 23, 2012
Commits on May 21, 2012
  1. updated

    committed
Commits on May 17, 2012
  1. mention slet

    committed
Commits on May 16, 2012
  1. mention toSReal

    committed
Commits on May 15, 2012
Commits on May 11, 2012
  1. mark current working version

    committed
Commits on May 10, 2012
  1. Release 2.0

    committed
  2. ready for release 1.4

    committed
Commits on May 7, 2012
Commits on May 2, 2012
  1. update notes

    committed
Something went wrong with that request. Please try again.