Add protected do_prop_solve for overriding

This will allow us to count solver invocations
without repeating the code in each propt implementation.

Author: peterschrammel

src/solvers/prop/prop.cpp

@@ -25,3 +25,8 @@ bvt propt::new_variables(std::size_t width)
     result[i]=new_variable();
   return result;
 }
+
+propt::resultt propt::prop_solve()
+{
+  return do_prop_solve();
+}

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;
@@ -120,6 +120,8 @@ class propt
   }
 
 protected:
+  virtual resultt do_prop_solve() = 0;
+
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;
 

src/solvers/sat/cnf_clause_list.h

@@ -39,11 +39,6 @@ class cnf_clause_listt:public cnft
     return tvt::unknown();
   }
 
-  resultt prop_solve() override
-  {
-    return resultt::P_ERROR;
-  }
-
   size_t no_clauses() const override
   {
     return clauses.size();
@@ -82,6 +77,11 @@ class cnf_clause_listt:public cnft
   }
 
 protected:
+  resultt do_prop_solve() override
+  {
+    return resultt::P_ERROR;
+  }
+
   clausest clauses;
 };
 

src/solvers/sat/dimacs_cnf.h

@@ -52,11 +52,6 @@ class dimacs_cnf_dumpt:public cnft
 
   void lcnf(const bvt &bv) override;
 
-  resultt prop_solve() override
-  {
-    return resultt::P_ERROR;
-  }
-
   tvt l_get(literalt) const override
   {
     return tvt::unknown();
@@ -68,6 +63,11 @@ class dimacs_cnf_dumpt:public cnft
   }
 
 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,8 +48,6 @@ class pbs_dimacs_cnft:public dimacs_cnft
 
   bool pbs_solve();
 
-  resultt prop_solve() override;
-
   tvt l_get(literalt a) const override;
 
   // dummy functions
@@ -60,6 +58,8 @@ class pbs_dimacs_cnft:public dimacs_cnft
   }
 
 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

@@ -21,10 +21,12 @@ class satcheck_booleforce_baset:public cnf_solvert
   virtual ~satcheck_booleforce_baset();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   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

@@ -24,7 +24,6 @@ class satcheck_cadicalt:public cnf_solvert
   virtual ~satcheck_cadicalt();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
@@ -42,6 +41,8 @@ class satcheck_cadicalt:public cnf_solvert
   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,7 +30,6 @@ class satcheck_glucose_baset:public cnf_solvert
   satcheck_glucose_baset(T *, message_handlert &message_handler);
   virtual ~satcheck_glucose_baset();
 
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
@@ -53,6 +52,8 @@ class satcheck_glucose_baset:public cnf_solvert
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   T *solver;
 
   void add_variables();

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

@@ -24,8 +24,6 @@ class satcheck_ipasirt:public cnf_solvert
   /// This method returns the description produced by the linked SAT solver
   const std::string solver_text() override;
 
-  resultt prop_solve() override;
-
   /// This method returns the truth value for a literal of the current SAT model
   tvt l_get(literalt a) const override final;
 
@@ -47,6 +45,8 @@ class satcheck_ipasirt:public cnf_solvert
   }
 
 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);
 

src/solvers/sat/satcheck_lingeling.h

@@ -22,7 +22,6 @@ class satcheck_lingelingt:public cnf_solvert
   virtual ~satcheck_lingelingt();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
@@ -41,6 +40,8 @@ class satcheck_lingelingt:public cnf_solvert
   void set_frozen(literalt a) override;
 
 protected:
+  resultt do_prop_solve() override;
+
   // NOLINTNEXTLINE(readability/identifiers)
   struct LGL * solver;
   bvt assumptions;

src/solvers/sat/satcheck_minisat.cpp

@@ -150,7 +150,7 @@ void satcheck_minisat1_baset::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_minisat1_baset::prop_solve()
+propt::resultt satcheck_minisat1_baset::do_prop_solve()
 {
   PRECONDITION(status != ERROR);
 
@@ -262,11 +262,11 @@ const std::string satcheck_minisat1_prooft::solver_text()
   return "MiniSAT + Proof";
 }
 
-propt::resultt satcheck_minisat1_coret::prop_solve()
+propt::resultt satcheck_minisat1_coret::do_prop_solve()
 {
   propt::resultt r;
 
-  r=satcheck_minisat1_prooft::prop_solve();
+  r = satcheck_minisat1_prooft::do_prop_solve();
 
   if(status==UNSAT)
   {

src/solvers/sat/satcheck_minisat.h

@@ -25,7 +25,6 @@ class satcheck_minisat1_baset:public cnf_solvert
   virtual ~satcheck_minisat1_baset();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) final;
@@ -48,6 +47,8 @@ class satcheck_minisat1_baset:public cnf_solvert
   bool is_in_conflict(literalt l) const override;
 
 protected:
+  resultt do_prop_solve() override;
+
   // NOLINTNEXTLINE(readability/identifiers)
   class Solver *solver;
   void add_variables();
@@ -84,7 +85,6 @@ class satcheck_minisat1_coret:public satcheck_minisat1_prooft
   ~satcheck_minisat1_coret();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
 
   bool has_in_core() const
   {
@@ -99,5 +99,7 @@ class satcheck_minisat1_coret:public satcheck_minisat1_prooft
 
 protected:
   std::vector<bool> in_core;
+
+  resultt do_prop_solve() override;
 };
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_MINISAT_H

src/solvers/sat/satcheck_minisat2.cpp

@@ -162,8 +162,8 @@ static void interrupt_solver(int signum)
 
 #endif
 
-template<typename T>
-propt::resultt satcheck_minisat2_baset<T>::prop_solve()
+template <typename T>
+propt::resultt satcheck_minisat2_baset<T>::do_prop_solve()
 {
   PRECONDITION(status != statust::ERROR);
 

src/solvers/sat/satcheck_minisat2.h

@@ -30,7 +30,6 @@ class satcheck_minisat2_baset:public cnf_solvert
   satcheck_minisat2_baset(T *, message_handlert &message_handler);
   virtual ~satcheck_minisat2_baset();
 
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override final;
 
   void lcnf(const bvt &bv) override final;
@@ -64,6 +63,8 @@ class satcheck_minisat2_baset:public cnf_solvert
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   T *solver;
   uint32_t time_limit_seconds;
 

src/solvers/sat/satcheck_picosat.cpp

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

src/solvers/sat/satcheck_picosat.h

@@ -22,7 +22,6 @@ class satcheck_picosatt:public cnf_solvert
   ~satcheck_picosatt();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
@@ -40,6 +39,8 @@ class satcheck_picosatt:public cnf_solvert
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   bvt assumptions;
 
 private:

src/solvers/sat/satcheck_zchaff.cpp

@@ -70,7 +70,7 @@ void satcheck_zchaff_baset::copy_cnf()
       reinterpret_cast<int*>(&((*it)[0])), it->size());
 }
 
-propt::resultt satcheck_zchaff_baset::prop_solve()
+propt::resultt satcheck_zchaff_baset::do_prop_solve()
 {
   // this is *not* incremental
   PRECONDITION(status == INIT);

src/solvers/sat/satcheck_zchaff.h

@@ -25,7 +25,6 @@ class satcheck_zchaff_baset:public cnf_clause_listt
   virtual ~satcheck_zchaff_baset();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
   void set_assignment(literalt a, bool value) override;
   virtual void copy_cnf();
@@ -36,6 +35,8 @@ class satcheck_zchaff_baset:public cnf_clause_listt
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   CSolver *solver;
 
   enum statust { INIT, SAT, UNSAT, ERROR };

src/solvers/sat/satcheck_zcore.cpp

@@ -34,7 +34,7 @@ const std::string satcheck_zcoret::solver_text()
   return "ZCore";
 }
 
-propt::resultt satcheck_zcoret::prop_solve()
+propt::resultt satcheck_zcoret::do_prop_solve()
 {
   // We start counting at 1, thus there is one variable fewer.
   {

src/solvers/sat/satcheck_zcore.h

@@ -21,7 +21,6 @@ class satcheck_zcoret:public dimacs_cnft
   virtual ~satcheck_zcoret();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   bool is_in_core(literalt l) const
@@ -30,6 +29,8 @@ class satcheck_zcoret:public dimacs_cnft
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   std::set<unsigned> in_core;
 };