Count number of solver calls in propt and prop_convt

Useful for logging statistics

Author: peterschrammel

src/solvers/prop/prop.cpp

@@ -28,5 +28,11 @@ bvt propt::new_variables(std::size_t width)
 
 propt::resultt propt::prop_solve()
 {
+  ++number_of_solver_calls;
   return do_prop_solve();
 }
+
+std::size_t propt::get_number_of_solver_calls() const
+{
+  return number_of_solver_calls;
+}

src/solvers/prop/prop.h

@@ -119,13 +119,16 @@ class propt
     log.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
   }
 
+  std::size_t get_number_of_solver_calls() const;
+
 protected:
   virtual resultt do_prop_solve() = 0;
 
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;
 
   messaget log;
+  std::size_t number_of_solver_calls = 0;
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_H

src/solvers/prop/prop_conv.cpp

@@ -512,3 +512,8 @@ void prop_conv_solvert::print_assignment(std::ostream &out) const
   for(const auto &symbol : symbols)
     out << symbol.first << " = " << prop.l_get(symbol.second) << '\n';
 }
+
+std::size_t prop_conv_solvert::get_number_of_solver_calls() const
+{
+  return prop.get_number_of_solver_calls();
+}

src/solvers/prop/prop_conv.h

@@ -55,6 +55,9 @@ class prop_convt:public decision_proceduret
 
   // Resource limits:
   virtual void set_time_limit_seconds(uint32_t) {}
+
+  /// Returns the number of incremental solver calls
+  virtual std::size_t get_number_of_solver_calls() const = 0;
 };
 
 //
@@ -122,6 +125,8 @@ class prop_conv_solvert:public prop_convt
     prop.set_time_limit_seconds(lim);
   }
 
+  std::size_t get_number_of_solver_calls() const override;
+
 protected:
   virtual void post_process();
 

src/solvers/smt2/smt2_conv.cpp

@@ -4849,3 +4849,8 @@ exprt smt2_convt::substitute_let(
 
   return expr;
 }
+
+std::size_t smt2_convt::get_number_of_solver_calls() const
+{
+  return number_of_solver_calls;
+}

src/solvers/smt2/smt2_conv.h

@@ -135,6 +135,8 @@ class smt2_convt:public prop_convt
   void convert_type(const typet &);
   void convert_literal(const literalt);
 
+  std::size_t get_number_of_solver_calls() const override;
+
 protected:
   const namespacet &ns;
   std::ostream &out;
@@ -144,6 +146,8 @@ class smt2_convt:public prop_convt
   bvt assumptions;
   boolbv_widtht boolbv_width;
 
+  std::size_t number_of_solver_calls = 0;
+
   void write_header();
   void write_footer(std::ostream &);
 

src/solvers/smt2/smt2_dec.cpp

@@ -36,6 +36,8 @@ std::string smt2_dect::decision_procedure_text() const
 
 decision_proceduret::resultt smt2_dect::dec_solve()
 {
+  ++number_of_solver_calls;
+
   temporary_filet temp_file_problem("smt2_dec_problem_", ""),
     temp_file_stdout("smt2_dec_stdout_", ""),
     temp_file_stderr("smt2_dec_stderr_", "");