Merge pull request #4218 from peterschrammel/count-solver-calls

Add counting number of solver calls

Author: tautschnig

src/solvers/prop/prop.cpp

@@ -25,3 +25,14 @@ bvt propt::new_variables(std::size_t width)
     result[i]=new_variable();
   return result;
 }
+
+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

@@ -97,7 +97,7 @@ class propt
   // solving
   virtual const std::string solver_text()=0;
   enum class resultt { P_SATISFIABLE, P_UNSATISFIABLE, P_ERROR };
-  virtual resultt prop_solve()=0;
+  resultt prop_solve();
 
   // satisfying assignment
   virtual tvt l_get(literalt a) const=0;
@@ -119,11 +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/sat/cnf_clause_list.h

@@ -29,19 +29,20 @@ class cnf_clause_listt:public cnft
   }
   virtual ~cnf_clause_listt() { }
 
-  virtual void lcnf(const bvt &bv);
+  void lcnf(const bvt &bv) override;
 
-  virtual const std::string solver_text()
+  const std::string solver_text() override
   { return "CNF clause list"; }
 
-  virtual tvt l_get(literalt) const
+  tvt l_get(literalt) const override
   {
     return tvt::unknown();
   }
 
-  virtual resultt prop_solve() { return resultt::P_ERROR; }
-
-  virtual size_t no_clauses() const { return clauses.size(); }
+  size_t no_clauses() const override
+  {
+    return clauses.size();
+  }
 
   typedef std::list<bvt> clausest;
 
@@ -76,6 +77,11 @@ class cnf_clause_listt:public cnft
   }
 
 protected:
+  resultt do_prop_solve() override
+  {
+    return resultt::P_ERROR;
+  }
+
   clausest clauses;
 };
 
@@ -97,7 +103,7 @@ class cnf_clause_list_assignmentt:public cnf_clause_listt
     return assignment;
   }
 
-  virtual tvt l_get(literalt literal) const
+  tvt l_get(literalt literal) const override
   {
     if(literal.is_true())
       return tvt(true);

src/solvers/sat/dimacs_cnf.h

@@ -45,29 +45,29 @@ class dimacs_cnf_dumpt:public cnft
   dimacs_cnf_dumpt(std::ostream &_out, message_handlert &message_handler);
   virtual ~dimacs_cnf_dumpt() { }
 
-  virtual const std::string solver_text()
+  const std::string solver_text() override
   {
     return "DIMACS CNF Dumper";
   }
 
-  virtual void lcnf(const bvt &bv);
-
-  virtual resultt prop_solve()
-  {
-    return resultt::P_ERROR;
-  }
+  void lcnf(const bvt &bv) override;
 
-  virtual tvt l_get(literalt) const
+  tvt l_get(literalt) const override
   {
     return tvt::unknown();
   }
 
-  virtual size_t no_clauses() const
+  size_t no_clauses() const override
   {
     return 0;
   }
 
 protected:
+  resultt do_prop_solve() override
+  {
+    return resultt::P_ERROR;
+  }
+
   std::ostream &out;
 };
 

src/solvers/sat/pbs_dimacs_cnf.cpp

@@ -205,7 +205,7 @@ bool pbs_dimacs_cnft::pbs_solve()
   return satisfied;
 }
 
-propt::resultt pbs_dimacs_cnft::prop_solve()
+propt::resultt pbs_dimacs_cnft::do_prop_solve()
 {
   std::ofstream file("temp.cnf");
 

src/solvers/sat/pbs_dimacs_cnf.h

@@ -48,18 +48,18 @@ class pbs_dimacs_cnft:public dimacs_cnft
 
   bool pbs_solve();
 
-  virtual resultt prop_solve();
-
-  virtual tvt l_get(literalt a) const;
+  tvt l_get(literalt a) const override;
 
   // dummy functions
 
-  virtual const std::string solver_text()
+  const std::string solver_text() override
   {
     return "PBS - Pseudo Boolean/CNF Solver and Optimizer";
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   std::set<int> assigned;
 };
 

src/solvers/sat/satcheck_booleforce.cpp

@@ -79,7 +79,7 @@ void satcheck_booleforce_baset::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_booleforce_baset::prop_solve()
+propt::resultt satcheck_booleforce_baset::do_prop_solve()
 {
   PRECONDITION(status == SAT || status == INIT);
 

src/solvers/sat/satcheck_booleforce.h

@@ -20,11 +20,13 @@ class satcheck_booleforce_baset:public cnf_solvert
 public:
   virtual ~satcheck_booleforce_baset();
 
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  const std::string solver_text() override;
+  tvt l_get(literalt a) const override;
 
-  virtual void lcnf(const bvt &bv);
+  void lcnf(const bvt &bv) override;
+
+protected:
+  resultt do_prop_solve() override;
 };
 
 class satcheck_booleforcet:public satcheck_booleforce_baset