Satisfiability modulo theory (SMT) solvers have significantly advanced automated reasoning due to their effectiveness in solving problems across various fields. With the advancement in SMT solvers, there is growing interest in exploring capabilities beyond mere satisfiability, similar to the progression observed in Boolean satisfiability solvers that expanded into counting and sampling. In this study, we investigate the following question: Can we rely on modern CNF model counters and CNF samplers to extend modern SMT solvers to handle the problems of counting and sampling over bit-vectors? The main contribution of this work is the development of an efficient and user-friendly tool, \(\textsf{csb}\) , that solves a bunch of problems around model counting and sampling on the theory of bit-vectors, namely exact and approximate projected and non-projected model counting, along with the almost-uniform and uniform-like sampling. In the case of exact counting, projected counting, and uniform sampling, \(\textsf{csb}\) is the first tool to solve the problem—although all these problems have a lot of applications. Our tool \(\textsf{csb}\) converts the bit-vector formula into a CNF formula using bit-blasting techniques before applying CNF model counters or samplers to perform counting or sampling. It keeps track of the variable mapping between the bitvector and CNF formula and passes that information to the CNF counter. We built our tool on top of SMT solver \(\textsf{STP}\) by integrating approximate model counter \(\textsf{ApproxMC}\) , exact model counter \(\textsf{Ganak}\) , almost-uniform sampler \(\textsf{UniGen}\) , and uniform-like sampler \(\textsf{CMSGen}\) in it. Our experiments demonstrate significant performance improvements over existing methods.
