fabian/minisat
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix status print warnings

Browse source
This commit is contained in:
Fabian Posch 2024-08-09 18:42:20 +02:00
parent 54320c0d8e
commit 6497ee686c
1 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Main.C
View file

@ -19,6 +19,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "Solver.h"
#include <ctime>
#include <iomanip>
#include <iostream>
#include <ostream>
#include <unistd.h>
#include <signal.h>
#include <zlib.h>
@ -167,13 +170,16 @@ void printStats(SolverStats& stats)
{
double cpu_time = cpuTime();
int64 mem_used = memUsed();
reportf("restarts : %"I64_fmt"\n", stats.starts);
reportf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", stats.conflicts , stats.conflicts /cpu_time);
reportf("decisions : %-12"I64_fmt" (%.0f /sec)\n", stats.decisions , stats.decisions /cpu_time);
reportf("propagations : %-12"I64_fmt" (%.0f /sec)\n", stats.propagations, stats.propagations/cpu_time);
reportf("conflict literals : %-12"I64_fmt" (%4.2f %% deleted)\n", stats.tot_literals, (stats.max_literals - stats.tot_literals)*100 / (double)stats.max_literals);
if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0);
reportf("CPU time : %g s\n", cpu_time);
using namespace std;
cout << setprecision(0);
cout << "restarts : " << stats.starts << endl << flush;
cout << "conflicts : " << stats.conflicts << " (" << stats.conflicts / cpu_time << " /sec)" << endl << flush;
cout << "decisions : " << stats.decisions << " (" << stats.decisions / cpu_time << " /sec)" << endl << flush;
cout << "propagations : " << stats.propagations << " (" << stats.propagations / cpu_time << " /sec)" << endl << flush;
cout << std::setprecision(2);
cout << "conflict literals : " << stats.tot_literals << " (" << setw(4) << (stats.max_literals - stats.tot_literals)*100 / (double)stats.max_literals << " %% deleted)" << endl << flush;
if (mem_used != 0) std::cout << "Memory used : " << setprecision(2) << mem_used / 1048576.0 << " MB" << endl << flush;
cout << "CPU time : " << cpu_time << " s" << endl << flush;
}
Solver* solver;