Merge pull request #3749 from diffblue/clauses-is-statistics

increase verbosity level of CNF statistics

Author: Daniel Kroening

src/solvers/sat/pbs_dimacs_cnf.cpp

@@ -218,8 +218,8 @@ propt::resultt pbs_dimacs_cnft::prop_solve()
   pbfile.close();
 
   // We start counting at 1, thus there is one variable fewer.
-  messaget::status() << (no_variables() - 1) << " variables, " << clauses.size()
-                     << " clauses" << eom;
+  messaget::statistics() << (no_variables() - 1) << " variables, "
+                         << clauses.size() << " clauses" << eom;
 
   const bool result = pbs_solve();
 

src/solvers/sat/satcheck_cadical.cpp

@@ -69,8 +69,8 @@ propt::resultt satcheck_cadicalt::prop_solve()
 {
   INVARIANT(status != statust::ERROR, "there cannot be an error");
 
-  messaget::status() << (no_variables() - 1) << " variables, " << clause_counter
-                     << " clauses" << eom;
+  messaget::statistics() << (no_variables() - 1) << " variables, "
+                         << clause_counter << " clauses" << eom;
 
   if(status == statust::UNSAT)
   {

src/solvers/sat/satcheck_glucose.cpp

@@ -137,11 +137,8 @@ propt::resultt satcheck_glucose_baset<T>::prop_solve()
   PRECONDITION(status != statust::ERROR);
 
   // We start counting at 1, thus there is one variable fewer.
-  {
-    messaget::status() <<
-      (no_variables()-1) << " variables, " <<
-      solver->nClauses() << " clauses" << eom;
-  }
+  messaget::statistics() << (no_variables() - 1) << " variables, "
+                         << solver->nClauses() << " clauses" << eom;
 
   try
   {

src/solvers/sat/satcheck_ipasir.cpp

@@ -97,11 +97,8 @@ propt::resultt satcheck_ipasirt::prop_solve()
 {
   INVARIANT(status!=statust::ERROR, "there cannot be an error");
 
-  {
-    messaget::status() <<
-      (no_variables()-1) << " variables, " <<
-      clause_counter << " clauses" << eom;
-  }
+  messaget::statistics() << (no_variables() - 1) << " variables, "
+                         << clause_counter << " clauses" << eom;
 
   // use the internal representation, as ipasir does not support reporting the
   // status

src/solvers/sat/satcheck_lingeling.cpp

@@ -72,7 +72,7 @@ propt::resultt satcheck_lingelingt::prop_solve()
     std::string msg=
       std::to_string(no_variables()-1)+" variables, "+
       std::to_string(clause_counter)+" clauses";
-    messaget::status() << msg << messaget::eom;
+    messaget::statistics() << msg << messaget::eom;
   }
 
   std::string msg;

src/solvers/sat/satcheck_minisat.cpp

@@ -154,11 +154,8 @@ propt::resultt satcheck_minisat1_baset::prop_solve()
 {
   PRECONDITION(status != ERROR);
 
-  {
-    messaget::status() <<
-      (_no_variables-1) << " variables, " <<
-      solver->nClauses() << " clauses" << messaget::eom;
-  }
+  messaget::statistics() << (_no_variables - 1) << " variables, "
+                         << solver->nClauses() << " clauses" << messaget::eom;
 
   add_variables();
 

src/solvers/sat/satcheck_minisat2.cpp

@@ -167,11 +167,8 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
 {
   PRECONDITION(status != statust::ERROR);
 
-  {
-    messaget::status() <<
-      (no_variables()-1) << " variables, " <<
-      solver->nClauses() << " clauses" << eom;
-  }
+  messaget::statistics() << (no_variables() - 1) << " variables, "
+                         << solver->nClauses() << " clauses" << eom;
 
   try
   {

src/solvers/sat/satcheck_picosat.cpp

@@ -73,7 +73,7 @@ propt::resultt satcheck_picosatt::prop_solve()
     std::string msg=
       std::to_string(_no_variables-1)+" variables, "+
       std::to_string(picosat_added_original_clauses(picosat))+" clauses";
-    messaget::status() << msg << messaget::eom;
+    messaget::statistics() << msg << messaget::eom;
   }
 
   std::string msg;

src/solvers/sat/satcheck_zchaff.cpp

@@ -81,7 +81,7 @@ propt::resultt satcheck_zchaff_baset::prop_solve()
     std::string msg=
       std::to_string(solver->num_variables())+" variables, "+
       std::to_string(solver->clauses().size())+" clauses";
-    messaget::status() << msg << messaget::eom;
+    messaget::statistics() << msg << messaget::eom;
   }
 
   SAT_StatusT result=(SAT_StatusT)solver->solve();

src/solvers/sat/satcheck_zcore.cpp

@@ -41,7 +41,7 @@ propt::resultt satcheck_zcoret::prop_solve()
     std::string msg=
       std::to_string(no_variables()-1)+" variables, "+
       std::to_string(no_clauses())+" clauses";
-    messaget::status() << msg << messaget::eom;
+    messaget::statistics() << msg << messaget::eom;
   }
 
   // get the core