pact is a hashing-based projected approximate model counter for hybrid SMT formulas. pact takes input an SMT formula over any theory combination and returns the count projected over bitvector and Boolean variables. Please refer to our DAC'25 paper for details about pact.
./configure.sh --auto-download --cryptominisat
cd build
make
Count as pact, projected on bitvectors.
./cvc5 -S --hashsm xor <filename>
Count as pact, projected on Booleans
./cvc5 -S --projcount <filename>
Count with different hashing mode
./cvc5 -S --hashsm prime or ./cvc5 -S --hashsm shift
Count with varying epsilon and delta
./cvc5 -S --delta <value> --epsilon <value> <filename>
Count with varying starting slicesize
./cvc5 -S --slicesize <value> <filename>
Count by enumeration.
./cvc5 -e <filename>
Issue ./cvc5 -h and look for Model Counting Module for more options.
pact can be built on Linux and macOS. For Windows, pact can be cross-compiled using Mingw-w64.
For detailed build and installation instructions on these platforms, see file INSTALL.rst.
The counting part of pact is written by Arijit Shaw and Kuldeep S. Meel. pact depends on mammoth work done by cvc5. For a full list of cvc5's authors, please refer to the AUTHORS file. Please refer to cvc5's readme for more details about cvc5.