A 16-thread bit-level parallel MC solver, compatible with BMC and PDR

To build Modelchecker, run the following command in the project directory:

./rebulid.sh
make clean
make -j

To use Modelchecker, run the following command in the project directory:

$ ./modelchecker [-pdr <pdr_thread>] [-bmc <bmc_thread>] <AIGER_file> 

Note that the maximum number of threads for PDR is 4, while the maximum number of threads for BMC is 12.

For unsafe circuits, Modelchecker will output a a witness to the standard output and display the program's runtime.

For safe circuits, Modelchecker will output "0" along with the runtime. Additionally, it will generate the circuit's certificate in both AIG and AAG formats in the current working directory, named certificate.aig and certificate.aag respectively.