Say I have a mixed integer linear program in variables $x \in \mathbb{Z}^a, y \in \mathbb{Z}^b, z \in \mathbb{R}^c$ together with linear constraints on $(x,y,z)$. I want to count the number of values of $x \in \mathbb{Z}^a$ s.t. a solution $(x,y,z)$ exists.
Is there existing software to solve problems of this type? There are lots of MILP solvers (mixed integer linear programming), but I don't know of any that solve the counting version of the problem rather than the decision or search problems.
A brute force way to do this with a conventional MILP solver is to find an optimal integer solution, add a cut to separate that integer solution from the other feasible integer solutions, reoptimize, and repeat until you run out of integer solutions. For problems with a very small number of integer solutions and lots of continuous variables, this can work well, but it can also be very slow if there are many integer solutions.
Finding a separating cut is easy for problems with binary variables, but it becomes a problem specific challenge in general.
Found after some more searching:
LattE counts lattice points within rational polytopes via Barvinok's algorithm, which computes the rational multivariate generating function of the lattice points in a region (and then plugs in $x = 1$ to get the count). This works because the generating functions can be additively combined over different pieces of the polytope (at vertices and faces). A paper describing the software is
De Loera et al., Effective lattice point counting in rational convex polytopes
Sage appears to use LattE as a dependency, so that's an easy way to access it.
