Skip to content


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
branch: master
Commits on Mar 31, 2015
  1. Merge pull request #146 from brianhuffman/master

    Redefine `svFromWord1` so that it works for both signed and unsigned input
  2. @brianhuffman

    Redefine `svFromWord1` so that it works for both signed and unsigned …

    brianhuffman authored
    Fixes #144: now `svTestBit` should work properly for signed words.
  3. Revert Makefile to older version..

    I was confused partly because of the -s flag; but that's legit
    as those are tested as part of "cabal test"..
  4. Another simplification

  5. Clean-up test suite

  6. Update float-add example.

    Fixes #142
Commits on Mar 30, 2015
  1. @brianhuffman

    Implement sbvTestBit using svTestBit, which is faster on large words

    brianhuffman authored
    Fixes #129.
    NOTE: This patch changes the SMTLib encoding for the testbit operation.
  2. @brianhuffman

    Add check to svTestBit: if index is larger than bit size, return svFalse

    brianhuffman authored
    This avoids a "high extract index is bigger than the size of the
    bit-vector" error message from the SMT solver in case the user runs
    svTestBit with a large index.
Commits on Mar 29, 2015
  1. Floating point: Fix expected outcomes

    New release of Z3 mandates changes here. I wish there was a better way
    to do this. Also note: The last example is no longer working! I think
    there’s a Z3 bug lurking here that I need to track and report.
  2. Robustify IEEE754 signum/test selector.

    This relates to issue #101
  3. Simplify test predicates

  4. Fix isNormalFP concrete-predicates.

    We can't just define isNormal to be not . isDenormal, since that
    does the wrong thing for NaN/Infinity/-Infinity values. So,
    explicitly disallow those.
  5. Improve response when backend solver has no model

    In case of “unknown” the backend solver may not have a model to
    present. Watch for that case and respond appropriately, instead of
    choking.. This is terribly z3 specific I’m afraid, but will have to do
    for now; until SMTLib folks come up with a way to query solvers to see
    if there’s model available.
  6. Floating-Point to Real conversions and back

    Implement sRealToSFloat, sRealToSDouble, and fpToSReal. Also add
    symbolic rounding modes as convenient shortcuts.
    Note that while the conversion seems to be working OK, Z3 is having
    hard time actually producing results for queries involving these
    conversions. Filed this issue: Z3Prover/z3#14
  7. Reimplement "toSReal"

    Remove the old hack (pre uninterpreted trick), and rename it to
  8. Mention classifiers

  9. Add fp-classifiers

    This partially addresses #132. Unfortunately a bunch of tests are
    failing for these tests due to issues in Z3. In particular, see:
    Z3Prover/z3#13 and
    Until those bugs are resolved on the z3 side these predicates should be
    used with care!
Commits on Mar 28, 2015
  1. Make haddock 100% happy!

  2. Make hlint happy

Commits on Mar 27, 2015
  1. @brianhuffman
  2. @brianhuffman

    Add more special-case shortcuts to svXOr

    brianhuffman authored
    Some test cases fail if these are not included.
  3. @brianhuffman

    Function normCW now normalizes values of kind KBool

    brianhuffman authored
    This fixes a bug that was triggered by the implementation of svNot:
    'svNot svFalse' would produce 'CW KBool (CWInteger -1)', which is
    not in normal form.
Commits on Mar 26, 2015
  1. @brianhuffman
Something went wrong with that request. Please try again.