Skip to content
This repository has been archived by the owner on Aug 23, 2024. It is now read-only.

Boolector 3.1.0

Compare
Choose a tag to compare
@mpreiner mpreiner released this 02 Dec 22:12
· 193 commits to master since this release

Changes:

  • build system:
    • requires now cmake >= 3.3
    • exports library interface for using find_package(Boolector) in cmake projects
  • support for custom abort callback function
    (called on abort instead of actually aborting)
  • Python API now throws Python exceptions on abort conditions
    (e.g., when underlying C API is misused)
  • command line options that previously expected integer values denoting enum
    values are now configured with strings denoting the particular modes that
    can be selected; -=help and --=help allow to print detailed help
    messages for these modes
  • fixed issue in SMT2 parser to correctly print echo commands
    (thanks to Dominik Klumpp)
  • fixed race condition in Cython dependencies
    (thanks to Marco Gario)
  • patches and documentation for building Boolector on Windows
    (thanks to Andrew V. Jones)
  • support/use termination function feature of CaDiCaL
    (thanks to Andrew V. Jones)
  • various fixes to contrib dependecy scripts
    (thanks to Serge Bazanski)
  • new API calls
    • boolector_copy_sort
    • boolector_min_signed
    • boolector_max_signed
    • boolector_is_bv_const_zero
    • boolector_is_bv_const_one
    • boolector_is_bv_const_ones
    • boolector_is_bv_const_min_signed
    • boolector_is_bv_const_max_signed
  • CaDiCaL is now default SAT engine
  • support for constant arrays
  • support for GMP as bit-vector implementation
  • support for CyproMiniSat
    • supports multi-threading via option --sat-engine-n-threads
  • switched to Google test as testing framework
  • CLI options changed (replaced ':' with a '-')
  • BtorMC improvements (HWMCC'19 version)
    • k-induction engine with simple path constraints
  • Poolector Python script used in SMT-COMP'19