Many problems in verification, security, reliability, AI, and synthesis are solved in practice by reasoning over a set of constraints. The standard reasoning task is to ask whether there exists a solution satisfying those constraints. Satisfiability Modulo Theories (SMT) solvers are highly effective here. In many applications, however, we want richer information: how many inputs lead to a bug, how likely a stochastic system is to reach a failure state, how large a region satisfies a robustness or fairness property, or how many implementations satisfy a specification. Answering such quantitative questions raises both theoretical and algorithmic challenges because the notion of quantity changes with the underlying theory. For bitvectors, we count assignments; over real arithmetic, counting becomes volume computation; and for functions, we may count possible interpretations. In this talk, I will describe our work on the theory, algorithms, and implementation of these problems, and our broader goal of bringing these capabilities together into a general-purpose toolbox for quantitative automated reasoning.