A hashing-based algorithm for discrete integration over finite domains.
A framework to provide white-box access to the execution of SAT solver.
An algorithm to generate uniform samples subject to given set of constraints.
An ANF and CNF simplifier and converter.
An algorithm to compute minimal independent support for a given CNF formula.
An approximate model counter for Bitvector theory.
A hashing-based approximate sampler for weighted CNF formulas.
A weighted model counter over Boolean domains.