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

src/solvers/sat/satcheck_cadical.cpp

@@ -65,7 +65,7 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_cadicalt::prop_solve()
+propt::resultt satcheck_cadicalt::do_prop_solve()
 {
   INVARIANT(status != statust::ERROR, "there cannot be an error");
 

src/solvers/sat/satcheck_cadical.h

@@ -23,19 +23,26 @@ class satcheck_cadicalt:public cnf_solvert
   satcheck_cadicalt();
   virtual ~satcheck_cadicalt();
 
-  virtual const std::string solver_text() override;
-  virtual resultt prop_solve() override;
-  virtual tvt l_get(literalt a) const override;
-
-  virtual void lcnf(const bvt &bv) override;
-  virtual void set_assignment(literalt a, bool value) override;
-
-  virtual void set_assumptions(const bvt &_assumptions) override;
-  virtual bool has_set_assumptions() const override { return false; }
-  virtual bool has_is_in_conflict() const override { return false; }
-  virtual bool is_in_conflict(literalt a) const override;
+  const std::string solver_text() override;
+  tvt l_get(literalt a) const override;
+
+  void lcnf(const bvt &bv) override;
+  void set_assignment(literalt a, bool value) override;
+
+  void set_assumptions(const bvt &_assumptions) override;
+  bool has_set_assumptions() const override
+  {
+    return false;
+  }
+  bool has_is_in_conflict() const override
+  {
+    return false;
+  }
+  bool is_in_conflict(literalt a) const override;
 
 protected:
+  resultt do_prop_solve() override;
+
   // NOLINTNEXTLINE(readability/identifiers)
   CaDiCaL::Solver * solver;
 };

src/solvers/sat/satcheck_glucose.cpp

@@ -131,8 +131,8 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
   }
 }
 
-template<typename T>
-propt::resultt satcheck_glucose_baset<T>::prop_solve()
+template <typename T>
+propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
 {
   PRECONDITION(status != statust::ERROR);
 

src/solvers/sat/satcheck_glucose.h

@@ -30,23 +30,30 @@ class satcheck_glucose_baset:public cnf_solvert
   satcheck_glucose_baset(T *, message_handlert &message_handler);
   virtual ~satcheck_glucose_baset();
 
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  tvt l_get(literalt a) const override;
 
-  virtual void lcnf(const bvt &bv);
-  virtual void set_assignment(literalt a, bool value);
+  void lcnf(const bvt &bv) override;
+  void set_assignment(literalt a, bool value) override;
 
   // extra MiniSat feature: solve with assumptions
-  virtual void set_assumptions(const bvt &_assumptions);
+  void set_assumptions(const bvt &_assumptions) override;
 
   // extra MiniSat feature: default branching decision
   void set_polarity(literalt a, bool value);
 
-  virtual bool is_in_conflict(literalt a) const;
-  virtual bool has_set_assumptions() const { return true; }
-  virtual bool has_is_in_conflict() const { return true; }
+  bool is_in_conflict(literalt a) const override;
+  bool has_set_assumptions() const override
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override
+  {
+    return true;
+  }
 
 protected:
+  resultt do_prop_solve() override;
+
   T *solver;
 
   void add_variables();
@@ -58,16 +65,16 @@ class satcheck_glucose_no_simplifiert:
 {
 public:
   explicit satcheck_glucose_no_simplifiert(message_handlert &message_handler);
-  virtual const std::string solver_text();
+  const std::string solver_text() override;
 };
 
 class satcheck_glucose_simplifiert:
   public satcheck_glucose_baset<Glucose::SimpSolver>
 {
 public:
   explicit satcheck_glucose_simplifiert(message_handlert &message_handler);
-  virtual const std::string solver_text();
-  virtual void set_frozen(literalt a);
+  const std::string solver_text() override;
+  void set_frozen(literalt a) override;
   bool is_eliminated(literalt a) const;
 };
 

src/solvers/sat/satcheck_ipasir.cpp

@@ -93,7 +93,7 @@ void satcheck_ipasirt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_ipasirt::prop_solve()
+propt::resultt satcheck_ipasirt::do_prop_solve()
 {
   INVARIANT(status!=statust::ERROR, "there cannot be an error");
 

src/solvers/sat/satcheck_ipasir.h

@@ -22,25 +22,31 @@ class satcheck_ipasirt:public cnf_solvert
   virtual ~satcheck_ipasirt() override;
 
   /// This method returns the description produced by the linked SAT solver
-  virtual const std::string solver_text() override;
-
-  virtual resultt prop_solve() override;
+  const std::string solver_text() override;
 
   /// This method returns the truth value for a literal of the current SAT model
-  virtual tvt l_get(literalt a) const override final;
+  tvt l_get(literalt a) const override final;
 
-  virtual void lcnf(const bvt &bv) override final;
+  void lcnf(const bvt &bv) override final;
 
   /* This method is not supported, and currently not called anywhere in CBMC */
-  virtual void set_assignment(literalt a, bool value) override;
+  void set_assignment(literalt a, bool value) override;
 
-  virtual void set_assumptions(const bvt &_assumptions) override;
+  void set_assumptions(const bvt &_assumptions) override;
 
-  virtual bool is_in_conflict(literalt a) const override;
-  virtual bool has_set_assumptions() const override final { return true; }
-  virtual bool has_is_in_conflict() const override final { return true; }
+  bool is_in_conflict(literalt a) const override;
+  bool has_set_assumptions() const override final
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override final
+  {
+    return true;
+  }
 
 protected:
+  resultt do_prop_solve() override;
+
   void *solver;
 
   bvt assumptions;

src/solvers/sat/satcheck_lingeling.cpp

@@ -63,7 +63,7 @@ void satcheck_lingelingt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_lingelingt::prop_solve()
+propt::resultt satcheck_lingelingt::do_prop_solve()
 {
   PRECONDITION(status != ERROR);