blob: 51e72726d0c903f3d47893120ee8f405997d5c58 (
plain) (
tree)
|
|
Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of
fixed-size bit-vectors, arrays and uninterpreted functions. It supports the
SMT-LIB logics BV, QF_ABV, QF_AUFBV, QF_BV and QF_UFBV. Boolector provides a
rich C and Python API and supports incremental solving, both with the SMT-LIB
commands push and pop, and as solving under assumptions. The documentation of
its API can be found here.
WWW: https://boolector.github.io/
|
