Tags:#SMT(LA), Model Counting, Volume Computation and Volume Estimation
Abstract:
We present VolCE, a tool for computing and estimating the size of the solution space of SMT(LA) constraints. VolCE supports the SMT-LIB format. It integrates SMT solving with volume computation/estimation and integer solution counting for convex polytopes. Several effective techniques are adopted, which enable the tool to deal with high-dimensional problem instances efficiently.
VolCE: An Efficient Tool for Solving #SMT(LA) Problems