bill is a header-only reasoning library. The library serves as an integration layer for various reasoning engines (such as decision diagrams or satisfiability solvers) and provides unified interfaces for them.
The following code snippet uses a SAT solver to prove De Morgan's law for propositional logic.
#include <bill/sat/solver.hpp>
#include <bill/sat/tseytin.hpp>
solver<solvers::ghack> solver;
auto const a = lit_type(solver.add_variable(), lit_type::polarities::positive);
auto const b = lit_type(solver.add_variable(), lit_type::polarities::positive);
auto const t0 = add_tseytin_and(solver, a, b);
auto const t1 = ~add_tseytin_or(solver, ~a, ~b);
auto const t2 = add_tseytin_xor(solver, t0, t1);
solver.add_clause(t2);
CHECK(solver.solve() == result::states::unsatisfiable);
A modern compiler is required to build bill. We are continously testing with Clang 6.0.1, GCC 7.3.0, and GCC 8.2.0. More information can be found in the documentation.
bill is part of the EPFL logic synthesis libraries. The other libraries and several examples on how to use and integrate the libraries can be found in the logic synthesis tool showcase.