Merge pull request #258 from diffblue/unwind-progress

ebmc: Downgrade level of progress output during unwinding

Author: kroening

src/ebmc/ebmc_parse_options.cpp

@@ -404,6 +404,7 @@ void ebmc_parse_optionst::help()
     " {y--smv-netlist}               \t show netlist in SMV format\n"
     " {y--dot-netlist}               \t show netlist in DOT format\n"
     " {y--show-trans}                \t show transition system\n"
+    " {y--verbosity} {u#}            \t verbosity level, from 0 (silent) to 10 (everything)\n"
     // clang-format on
     "\n");
 }

src/trans-netlist/unwind_netlist.cpp

@@ -37,18 +37,18 @@ void unwind(
   if(add_initial_state && first)
   {
     // do initial state
-    message.status() << "Initial State" << messaget::eom;
-    
+    message.progress() << "Initial State" << messaget::eom;
+
     for(const auto & n : netlist.initial)
       solver.l_set_to(bmc_map.translate(0, n), true);
   }
 
   // do transitions
   if(last)
-    message.status() << "Transition " << t << messaget::eom;
+    message.progress() << "Transition " << t << messaget::eom;
   else
-    message.status() << "Transition " << t << "->" << t+1 << messaget::eom;
-  
+    message.progress() << "Transition " << t << "->" << t + 1 << messaget::eom;
+
   const bmc_mapt::timeframet &timeframe=bmc_map.timeframe_map[t];
 
   for(std::size_t n=0; n<timeframe.size(); n++)

src/trans-word-level/unwind.cpp

@@ -40,7 +40,7 @@ void unwind(
 
   // in-state constraints
 
-  message.status() << "In-state constraints" << messaget::eom;
+  message.progress() << "In-state constraints" << messaget::eom;
 
   if(!op_invar.is_true())
     for(std::size_t c = 0; c < no_timeframes; c++)
@@ -51,7 +51,7 @@ void unwind(
 
   if(initial_state)
   {
-    message.status() << "Initial state" << messaget::eom;
+    message.progress() << "Initial state" << messaget::eom;
 
     if(!op_init.is_true())
       decision_procedure.set_to_true(
@@ -60,7 +60,7 @@ void unwind(
 
   // transition relation
 
-  message.status() << "Transition relation" << messaget::eom;
+  message.progress() << "Transition relation" << messaget::eom;
 
   if(!op_trans.is_true())
     for(std::size_t t = 0; t < no_timeframes; t++)
@@ -69,10 +69,11 @@ void unwind(
       bool last=(t==no_timeframes-1);
 
       if(last)
-        message.status() << "Transition " << t << messaget::eom;
+        message.progress() << "Transition " << t << messaget::eom;
       else
-        message.status() << "Transition " << t << "->" << t+1 << messaget::eom;
-                  
+        message.progress() << "Transition " << t << "->" << t + 1
+                           << messaget::eom;
+
       decision_procedure.set_to_true(
         instantiate(op_trans, t, no_timeframes, ns));
     }