Merge pull request #7241 from diffblue/chc_proof_strategy

CHC solver: extract solver progress reporting

Author: kroening

src/cprover/Makefile

@@ -26,6 +26,7 @@ SRC = address_taken.cpp \
       state_encoding.cpp \
       state_encoding_targets.cpp \
       solver.cpp \
+      solver_progress.cpp \
       variable_encoding.cpp \
       wcwidth.c \
       # Empty last line

src/cprover/console.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #  include <unistd.h>
 #endif
 
+#include <util/invariant.h>
 #include <util/run.h>
 #include <util/string_utils.h>
 #include <util/unicode.h>
@@ -181,6 +182,18 @@ std::ostream &consolet::reset(std::ostream &str)
     return str;
 }
 
+std::ostream &consolet::cursorup(std::ostream &str)
+{
+  PRECONDITION(is_terminal());
+  return str << "\x1b[1A";
+}
+
+std::ostream &consolet::cleareol(std::ostream &str)
+{
+  PRECONDITION(is_terminal());
+  return str << "\x1b[0K";
+}
+
 std::size_t consolet::width()
 {
   if(_width_is_set)

src/cprover/console.h

@@ -20,6 +20,7 @@ class consolet
 public:
   static void init();
 
+  // colors
   static std::ostream &blue(std::ostream &);
   static std::ostream &cyan(std::ostream &);
   static std::ostream &green(std::ostream &);
@@ -33,6 +34,12 @@ class consolet
 
   static std::ostream &reset(std::ostream &);
 
+  // cursor movement
+  static std::ostream &cursorup(std::ostream &);
+
+  // deletion
+  static std::ostream &cleareol(std::ostream &); // erase to end of line
+
   static bool is_terminal()
   {
     init();

src/cprover/solver.cpp

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 #include "propagate.h"
 #include "report_properties.h"
 #include "report_traces.h"
+#include "solver_progress.h"
 #include "solver_types.h"
 #include "state.h"
 
@@ -393,29 +394,6 @@ void solver(
     property.status = propertyt::DROPPED;
 }
 
-void solver_progress(size_t i, size_t n, bool verbose)
-{
-  if(verbose)
-  {
-  }
-  else
-  {
-    if(i == n)
-    {
-      if(consolet::is_terminal())
-        std::cout << "\x1b[1A\x1b[0K"; // clear the line
-    }
-    else
-    {
-      if(i != 0 && consolet::is_terminal())
-        std::cout << "\x1b[1A";
-
-      std::cout << consolet::orange << "Doing property " << (i + 1) << '/' << n
-                << consolet::reset << '\n';
-    }
-  }
-}
-
 solver_resultt solver(
   const std::vector<exprt> &constraints,
   const solver_optionst &solver_options,
@@ -441,14 +419,16 @@ solver_resultt solver(
     return solver_resultt::ALL_PASS;
   }
 
+  solver_progresst solver_progress(properties.size(), solver_options.verbose);
+
   // solve each property separately, in order of occurence
   for(std::size_t i = 0; i < properties.size(); i++)
   {
-    solver_progress(i, properties.size(), solver_options.verbose);
+    solver_progress(i);
     solver(frames, address_taken, solver_options, ns, properties, i);
   }
 
-  solver_progress(properties.size(), properties.size(), solver_options.verbose);
+  solver_progress.finished();
 
   // reporting
   report_properties(properties);

src/cprover/solver_progress.cpp

@@ -0,0 +1,59 @@
+/*******************************************************************\
+
+Module: Solver Progress Reporting
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Solver Progress Reporting
+
+#include "solver_progress.h"
+
+#include "console.h"
+
+#include <iostream>
+
+void solver_progresst::operator()(size_t current)
+{
+  if(verbose)
+  {
+  }
+  else
+  {
+    if(first)
+    {
+      first = false;
+    }
+    else
+    {
+      if(consolet::is_terminal())
+      {
+        // up one row and clear the line
+        std::cout << consolet::cursorup << consolet::cleareol;
+      }
+    }
+
+    std::cout << consolet::orange << "Processing property " << (current + 1)
+              << '/' << total << consolet::reset << '\n';
+  }
+}
+
+void solver_progresst::finished()
+{
+  if(verbose)
+  {
+  }
+  else
+  {
+    if(consolet::is_terminal())
+    {
+      if(!first)
+      {
+        // up one row and clear the line
+        std::cout << consolet::cursorup << consolet::cleareol;
+      }
+    }
+  }
+}

src/cprover/solver_progress.h

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: Solver Progress Reporting
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Solver Progress Reporting
+
+#ifndef CPROVER_CPROVER_SOLVER_PROGRESS_H
+#define CPROVER_CPROVER_SOLVER_PROGRESS_H
+
+#include "solver_types.h"
+
+class solver_progresst
+{
+public:
+  solver_progresst(std::size_t __total, bool __verbose)
+    : total(__total), verbose(__verbose)
+  {
+  }
+
+  void operator()(std::size_t current);
+  void finished();
+
+private:
+  bool first = true;
+  std::size_t total = 0;
+  bool verbose;
+};
+
+#endif // CPROVER_CPROVER_SOLVER_PROGRESS_H