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

@@ -95,7 +95,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;
@@ -118,6 +118,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

@@ -36,11 +36,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();
@@ -79,6 +74,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

@@ -53,11 +53,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();
@@ -69,6 +64,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

@@ -47,8 +47,6 @@ class pbs_dimacs_cnft:public dimacs_cnft
 
   bool pbs_solve();
 
-  resultt prop_solve() override;
-
   tvt l_get(literalt a) const override;
 
   // dummy functions
@@ -59,6 +57,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
   explicit satcheck_glucose_baset(T *);
   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.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();

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
   explicit satcheck_minisat2_baset(T *);
   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.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.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.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;
 };
 

unit/solvers/bdd/miniBDD/miniBDD.cpp

@@ -147,7 +147,7 @@ class bdd_propt : public propt
     return "BDDs";
   }
 
-  resultt prop_solve() override
+  resultt do_prop_solve() override
   {
     UNREACHABLE;
     return {};