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);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.