@mpreiner mpreiner released this Jul 1, 2018 · 155 commits to master since this release

Assets 2

Changes:

  • new build system, requires cmake >= 2.8
    • setup-*.sh scripts for dependencies (btor2parser, SAT solvers) in contrib
  • support for quantified bit-vectors (BV)
  • new bounded model checker BtorMC
  • support for new format BTOR2
  • support for CaDiCaL as SAT back-end
  • name of the Python module changed to pyboolector
  • SMT2 support for:
    • echo
    • declare-const
    • check-sat-assuming
    • get-unsat-assumptions
    • set-option :produce-unsat-assumptions
    • set-option :produce-assertions
    • set-logic ALL
  • new API calls
    • boolector_constd
    • boolector_consth
    • boolector_copyright
    • boolector_exists
    • boolector_forall
    • boolector_get_failed_assumptions
    • boolector_repeat
    • boolector_pop
    • boolector_push
    • boolector_version
  • removed obsolete API calls
    • boolector_set_sat_solver_lingeling
    • boolector_set_sat_solver_minisat
    • boolector_set_sat_solver_picosat
  • changes in API calls
    • boolector_srl, boolector_sll and boolector_sra now supports operands with
      the same bit-width (SMT-LIB v2 compatible)
  • various improvements and extensions of btormbt