Recently, symbolic program analysis techniques have been extended to
quantitative analyses using model counting constraint solvers. Given
a constraint and a bound, a model counting constraint solver computes
the number of solutions for the constraint within the bound. We present
a parameterized model counting constraint solver for string and numeric
constraints. We first construct a multi-track deterministic finite state
automaton that accepts all solutions to the given constraint. We limit
the numeric constraints to linear integer arithmetic, and for non-regular
string constraints we over-approximate the solution set. Counting the
number of accepting paths in the generated automaton solves the model
counting problem. Our approach is parameterized in the sense that, we do
not assume a finite domain size during automata construction, resulting in
a potentially infinite set of solutions, and our model counting approach
works for arbitrarily large bounds. We experimentally demonstrate
the effectiveness of our approach on a large set of string and numeric
constraints extracted from software applications. We experimentally compare
our tool to five existing model counting constraint solvers for string and
numeric constraints and demonstrate that our tool is as efficient and as
or more precise than other solvers. Moreover, our tool can handle mixed
constraints with string and integer variables that no other tool can.