From: trevor_hansen Date: Sat, 10 Jul 2010 04:54:09 +0000 (+0000) Subject: Output quick statistics if enabled, and exiting after generating the CNF. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=531e38eb9fe32b551aafa6562de66618fe62bd12;p=francis%2Fstp.git Output quick statistics if enabled, and exiting after generating the CNF. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@944 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/to-sat/AIG/BBNodeAIG.h b/src/to-sat/AIG/BBNodeAIG.h index 425325e..f9fec0a 100644 --- a/src/to-sat/AIG/BBNodeAIG.h +++ b/src/to-sat/AIG/BBNodeAIG.h @@ -11,9 +11,12 @@ #define BBNODEAIG_H_ #include "../../extlib-abc/aig.h" +#include namespace BEEV { + using std::cerr; + using std::endl; // This class wraps around a pointer to an AIG (provided by the ABC tool). // uses the default copy constructor and assignment operator. diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index 386ba04..33a15dc 100644 --- a/src/to-sat/AIG/ToSATAIG.cpp +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -75,7 +75,11 @@ namespace BEEV Cnf_DataFree(cnfData); if (bm->UserFlags.exit_after_CNF) + { + if (bm->UserFlags.quick_statistics_flag) + bm->GetRunTimes()->print(); exit(0); + } // cryptominisat treats simplify() as protected. #ifndef CRYPTOMINISAT2