Make propt::solver_text const

tautschnig · tautschnig · commit bbbd21fa7c53 · 2022-10-20T10:21:20.000Z
There is no point in marking the string returned by value `const`, it's
really about marking the method itself `const`.
diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
@@ -93,7 +93,7 @@ class propt
   virtual bvt new_variables(std::size_t width);
 
   // solving
-  virtual const std::string solver_text()=0;
+  virtual std::string solver_text() const = 0;
   enum class resultt { P_SATISFIABLE, P_UNSATISFIABLE, P_ERROR };
   resultt prop_solve();
 
diff --git a/src/solvers/qbf/qbf_bdd_core.cpp b/src/solvers/qbf/qbf_bdd_core.cpp
@@ -83,7 +83,7 @@ tvt qbf_bdd_coret::l_get(literalt a) const
   UNREACHABLE;
 }
 
-const std::string qbf_bdd_coret::solver_text()
+std::string qbf_bdd_coret::solver_text() const
 {
   return "QBF/BDD/CORE";
 }
diff --git a/src/solvers/qbf/qbf_bdd_core.h b/src/solvers/qbf/qbf_bdd_core.h
@@ -58,7 +58,7 @@ class qbf_bdd_coret:public qbf_bdd_certificatet
   virtual literalt lor(literalt a, literalt b);
   virtual literalt lor(const bvt &bv);
 
-  virtual const std::string solver_text();
+  virtual std::string solver_text() const;
   virtual resultt prop_solve();
   virtual tvt l_get(literalt a) const;
 
diff --git a/src/solvers/qbf/qbf_quantor.cpp b/src/solvers/qbf/qbf_quantor.cpp
@@ -27,7 +27,7 @@ tvt qbf_quantort::l_get(literalt) const
   UNREACHABLE;
 }
 
-const std::string qbf_quantort::solver_text()
+std::string qbf_quantort::solver_text() const
 {
   return "Quantor";
 }
diff --git a/src/solvers/qbf/qbf_quantor.h b/src/solvers/qbf/qbf_quantor.h
@@ -18,7 +18,7 @@ class qbf_quantort:public qdimacs_cnft
   explicit qbf_quantort(message_handlert &message_handler);
   virtual ~qbf_quantort();
 
-  virtual const std::string solver_text();
+  virtual std::string solver_text() const;
   virtual resultt prop_solve();
   virtual tvt l_get(literalt a) const;
 };
diff --git a/src/solvers/qbf/qbf_qube.cpp b/src/solvers/qbf/qbf_qube.cpp
@@ -29,7 +29,7 @@ tvt qbf_qubet::l_get(literalt) const
   UNREACHABLE;
 }
 
-const std::string qbf_qubet::solver_text()
+std::string qbf_qubet::solver_text() const
 {
   return "QuBE";
 }
diff --git a/src/solvers/qbf/qbf_qube.h b/src/solvers/qbf/qbf_qube.h
@@ -18,7 +18,7 @@ class qbf_qubet:public qdimacs_cnft
   explicit qbf_qubet(message_handlert &message_handler);
   virtual ~qbf_qubet();
 
-  virtual const std::string solver_text();
+  virtual std::string solver_text() const;
   virtual resultt prop_solve();
   virtual tvt l_get(literalt a) const;
 };
diff --git a/src/solvers/qbf/qbf_qube_core.cpp b/src/solvers/qbf/qbf_qube_core.cpp
@@ -26,7 +26,7 @@ qbf_qube_coret::~qbf_qube_coret()
 {
 }
 
-const std::string qbf_qube_coret::solver_text()
+std::string qbf_qube_coret::solver_text() const
 {
   return "QuBE w/ toplevel assignments";
 }
diff --git a/src/solvers/qbf/qbf_qube_core.h b/src/solvers/qbf/qbf_qube_core.h
@@ -26,7 +26,7 @@ class qbf_qube_coret:public qdimacs_coret
   explicit qbf_qube_coret(message_handlert &message_handler);
   virtual ~qbf_qube_coret();
 
-  virtual const std::string solver_text();
+  virtual std::string solver_text() const;
   virtual resultt prop_solve();
 
   virtual bool is_in_core(literalt l) const;
diff --git a/src/solvers/qbf/qbf_skizzo.cpp b/src/solvers/qbf/qbf_skizzo.cpp
@@ -29,7 +29,7 @@ tvt qbf_skizzot::l_get(literalt) const
   UNREACHABLE;
 }
 
-const std::string qbf_skizzot::solver_text()
+std::string qbf_skizzot::solver_text() const
 {
   return "Skizzo";
 }
diff --git a/src/solvers/qbf/qbf_skizzo.h b/src/solvers/qbf/qbf_skizzo.h
@@ -18,7 +18,7 @@ class qbf_skizzot:public qdimacs_cnft
   explicit qbf_skizzot(message_handlert &message_handler);
   virtual ~qbf_skizzot();
 
-  virtual const std::string solver_text();
+  virtual std::string solver_text() const;
   virtual resultt prop_solve();
   virtual tvt l_get(literalt a) const;
 };
diff --git a/src/solvers/qbf/qbf_skizzo_core.cpp b/src/solvers/qbf/qbf_skizzo_core.cpp
@@ -39,7 +39,7 @@ qbf_skizzo_coret::~qbf_skizzo_coret()
 {
 }
 
-const std::string qbf_skizzo_coret::solver_text()
+std::string qbf_skizzo_coret::solver_text() const
 {
   return "Skizzo/Core";
 }
diff --git a/src/solvers/qbf/qbf_skizzo_core.h b/src/solvers/qbf/qbf_skizzo_core.h
@@ -19,7 +19,7 @@ class qbf_skizzo_coret:public qbf_bdd_certificatet
   qbf_skizzo_coret();
   virtual ~qbf_skizzo_coret();
 
-  virtual const std::string solver_text();
+  virtual std::string solver_text() const;
   virtual resultt prop_solve();
 
   virtual bool is_in_core(literalt l) const;
diff --git a/src/solvers/qbf/qbf_squolem.cpp b/src/solvers/qbf/qbf_squolem.cpp
@@ -26,7 +26,7 @@ tvt qbf_squolemt::l_get(literalt a) const
   UNREACHABLE;
 }
 
-const std::string qbf_squolemt::solver_text()
+std::string qbf_squolemt::solver_text() const
 {
   return "Squolem";
 }
diff --git a/src/solvers/qbf/qbf_squolem.h b/src/solvers/qbf/qbf_squolem.h
@@ -26,7 +26,7 @@ class qbf_squolemt:public qdimacs_cnft
   qbf_squolemt();
   virtual ~qbf_squolemt();
 
-  virtual const std::string solver_text();
+  virtual std::string solver_text() const;
   virtual resultt prop_solve();
   virtual tvt l_get(literalt a) const;
 
diff --git a/src/solvers/qbf/qbf_squolem_core.cpp b/src/solvers/qbf/qbf_squolem_core.cpp
@@ -74,7 +74,7 @@ tvt qbf_squolem_coret::l_get(literalt a) const
     return tvt(tvt::tv_enumt::TV_UNKNOWN);
 }
 
-const std::string qbf_squolem_coret::solver_text()
+std::string qbf_squolem_coret::solver_text() const
 {
   return "Squolem (Certifying)";
 }
diff --git a/src/solvers/qbf/qbf_squolem_core.h b/src/solvers/qbf/qbf_squolem_core.h
@@ -26,7 +26,7 @@ class qbf_squolem_coret:public qdimacs_coret
   qbf_squolem_coret();
   virtual ~qbf_squolem_coret();
 
-  virtual const std::string solver_text();
+  virtual std::string solver_text() const;
   virtual resultt prop_solve();
 
   virtual tvt l_get(literalt a) const;
diff --git a/src/solvers/qbf/qdimacs_cnf.h b/src/solvers/qbf/qdimacs_cnf.h
@@ -27,7 +27,7 @@ class qdimacs_cnft:public dimacs_cnft
 
   // dummy functions
 
-  virtual const std::string solver_text()
+  virtual std::string solver_text() const
   {
     return "QDIMACS CNF";
   }
diff --git a/src/solvers/sat/cnf_clause_list.h b/src/solvers/sat/cnf_clause_list.h
@@ -31,7 +31,7 @@ class cnf_clause_listt:public cnft
 
   void lcnf(const bvt &bv) override;
 
-  const std::string solver_text() override
+  std::string solver_text() const override
   { return "CNF clause list"; }
 
   tvt l_get(literalt) const override
diff --git a/src/solvers/sat/dimacs_cnf.h b/src/solvers/sat/dimacs_cnf.h
@@ -24,7 +24,7 @@ class dimacs_cnft:public cnf_clause_listt
 
   // dummy functions
 
-  const std::string solver_text() override
+  std::string solver_text() const override
   {
     return "DIMACS CNF";
   }
@@ -48,7 +48,7 @@ class dimacs_cnf_dumpt:public cnft
   dimacs_cnf_dumpt(std::ostream &_out, message_handlert &message_handler);
   virtual ~dimacs_cnf_dumpt() { }
 
-  const std::string solver_text() override
+  std::string solver_text() const override
   {
     return "DIMACS CNF Dumper";
   }
diff --git a/src/solvers/sat/external_sat.cpp b/src/solvers/sat/external_sat.cpp
@@ -21,7 +21,7 @@ external_satt::external_satt(message_handlert &message_handler, std::string cmd)
 {
 }
 
-const std::string external_satt::solver_text()
+std::string external_satt::solver_text() const
 {
   return "External SAT solver";
 }
diff --git a/src/solvers/sat/external_sat.h b/src/solvers/sat/external_sat.h
@@ -22,7 +22,7 @@ class external_satt : public cnf_clause_list_assignmentt
     return false;
   }
 
-  const std::string solver_text() override;
+  std::string solver_text() const override;
 
   bool is_in_conflict(literalt) const override;
   void set_assignment(literalt, bool) override;
diff --git a/src/solvers/sat/pbs_dimacs_cnf.h b/src/solvers/sat/pbs_dimacs_cnf.h
@@ -52,7 +52,7 @@ class pbs_dimacs_cnft:public dimacs_cnft
 
   // dummy functions
 
-  const std::string solver_text() override
+  std::string solver_text() const override
   {
     return "PBS - Pseudo Boolean/CNF Solver and Optimizer";
   }
diff --git a/src/solvers/sat/satcheck_booleforce.cpp b/src/solvers/sat/satcheck_booleforce.cpp
@@ -58,7 +58,7 @@ tvt satcheck_booleforce_baset::l_get(literalt a) const
   return result;
 }
 
-const std::string satcheck_booleforce_baset::solver_text()
+std::string satcheck_booleforce_baset::solver_text() const
 {
   return std::string("Booleforce version ")+booleforce_version();
 }
diff --git a/src/solvers/sat/satcheck_booleforce.h b/src/solvers/sat/satcheck_booleforce.h
@@ -20,7 +20,7 @@ class satcheck_booleforce_baset:public cnf_solvert
 public:
   virtual ~satcheck_booleforce_baset();
 
-  const std::string solver_text() override;
+  std::string solver_text() const override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
diff --git a/src/solvers/sat/satcheck_cadical.cpp b/src/solvers/sat/satcheck_cadical.cpp
@@ -38,7 +38,7 @@ tvt satcheck_cadicalt::l_get(literalt a) const
   return result;
 }
 
-const std::string satcheck_cadicalt::solver_text()
+std::string satcheck_cadicalt::solver_text() const
 {
   return std::string("CaDiCaL ") + solver->version();
 }
diff --git a/src/solvers/sat/satcheck_cadical.h b/src/solvers/sat/satcheck_cadical.h
@@ -25,7 +25,7 @@ class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
   explicit satcheck_cadicalt(message_handlert &message_handler);
   virtual ~satcheck_cadicalt();
 
-  const std::string solver_text() override;
+  std::string solver_text() const override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp
@@ -78,12 +78,12 @@ void satcheck_glucose_baset<T>::set_polarity(literalt a, bool value)
   }
 }
 
-const std::string satcheck_glucose_no_simplifiert::solver_text()
+std::string satcheck_glucose_no_simplifiert::solver_text() const
 {
   return "Glucose Syrup without simplifier";
 }
 
-const std::string satcheck_glucose_simplifiert::solver_text()
+std::string satcheck_glucose_simplifiert::solver_text() const
 {
   return "Glucose Syrup with simplifier";
 }
diff --git a/src/solvers/sat/satcheck_glucose.h b/src/solvers/sat/satcheck_glucose.h
@@ -71,15 +71,15 @@ class satcheck_glucose_no_simplifiert:
 {
 public:
   using satcheck_glucose_baset<Glucose::Solver>::satcheck_glucose_baset;
-  const std::string solver_text() override;
+  std::string solver_text() const override;
 };
 
 class satcheck_glucose_simplifiert:
   public satcheck_glucose_baset<Glucose::SimpSolver>
 {
 public:
   using satcheck_glucose_baset<Glucose::SimpSolver>::satcheck_glucose_baset;
-  const std::string solver_text() override;
+  std::string solver_text() const override;
   void set_frozen(literalt a) override;
   bool is_eliminated(literalt a) const;
 };
diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp
@@ -59,7 +59,7 @@ tvt satcheck_ipasirt::l_get(literalt a) const
   return result;
 }
 
-const std::string satcheck_ipasirt::solver_text()
+std::string satcheck_ipasirt::solver_text() const
 {
   return std::string(ipasir_signature());
 }
diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h
@@ -24,7 +24,7 @@ class satcheck_ipasirt : public cnf_solvert, public hardness_collectort
   virtual ~satcheck_ipasirt() override;
 
   /// This method returns the description produced by the linked SAT solver
-  const std::string solver_text() override;
+  std::string solver_text() const override;
 
   /// This method returns the truth value for a literal of the current SAT model
   tvt l_get(literalt a) const override final;
diff --git a/src/solvers/sat/satcheck_lingeling.cpp b/src/solvers/sat/satcheck_lingeling.cpp
@@ -43,7 +43,7 @@ tvt satcheck_lingelingt::l_get(literalt a) const
   return result;
 }
 
-const std::string satcheck_lingelingt::solver_text()
+std::string satcheck_lingelingt::solver_text() const
 {
   return "Lingeling";
 }
diff --git a/src/solvers/sat/satcheck_lingeling.h b/src/solvers/sat/satcheck_lingeling.h
@@ -21,7 +21,7 @@ class satcheck_lingelingt:public cnf_solvert
   satcheck_lingelingt();
   virtual ~satcheck_lingelingt();
 
-  const std::string solver_text() override;
+  std::string solver_text() const override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
diff --git a/src/solvers/sat/satcheck_minisat.cpp b/src/solvers/sat/satcheck_minisat.cpp
@@ -108,7 +108,7 @@ tvt satcheck_minisat1_baset::l_get(literalt a) const
   return result;
 }
 
-const std::string satcheck_minisat1_baset::solver_text()
+std::string satcheck_minisat1_baset::solver_text() const
 {
   return "MiniSAT 1.14p";
 }
@@ -257,7 +257,7 @@ satcheck_minisat1_baset::~satcheck_minisat1_baset()
   delete solver;
 }
 
-const std::string satcheck_minisat1_prooft::solver_text()
+std::string satcheck_minisat1_prooft::solver_text() const
 {
   return "MiniSAT + Proof";
 }
@@ -277,7 +277,7 @@ propt::resultt satcheck_minisat1_coret::do_prop_solve()
   return r;
 }
 
-const std::string satcheck_minisat1_coret::solver_text()
+std::string satcheck_minisat1_coret::solver_text() const
 {
   return "MiniSAT + Core";
 }
diff --git a/src/solvers/sat/satcheck_minisat.h b/src/solvers/sat/satcheck_minisat.h
@@ -24,7 +24,7 @@ class satcheck_minisat1_baset:public cnf_solvert
 
   virtual ~satcheck_minisat1_baset();
 
-  const std::string solver_text() override;
+  std::string solver_text() const override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) final;
@@ -68,7 +68,7 @@ class satcheck_minisat1_prooft:public satcheck_minisat1t
   satcheck_minisat1_prooft();
   ~satcheck_minisat1_prooft();
 
-  const std::string solver_text() override;
+  std::string solver_text() const override;
   simple_prooft &get_resolution_proof();
   // void set_partition_id(unsigned p_id);
 
@@ -84,7 +84,7 @@ class satcheck_minisat1_coret:public satcheck_minisat1_prooft
   satcheck_minisat1_coret();
   ~satcheck_minisat1_coret();
 
-  const std::string solver_text() override;
+  std::string solver_text() const override;
 
   bool has_in_core() const
   {
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
@@ -99,12 +99,12 @@ void satcheck_minisat2_baset<T>::clear_interrupt()
   solver->clearInterrupt();
 }
 
-const std::string satcheck_minisat_no_simplifiert::solver_text()
+std::string satcheck_minisat_no_simplifiert::solver_text() const
 {
   return "MiniSAT 2.2.1 without simplifier";
 }
 
-const std::string satcheck_minisat_simplifiert::solver_text()
+std::string satcheck_minisat_simplifiert::solver_text() const
 {
   return "MiniSAT 2.2.1 with simplifier";
 }
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
diff --git a/src/solvers/sat/satcheck_picosat.cpp b/src/solvers/sat/satcheck_picosat.cpp
diff --git a/src/solvers/sat/satcheck_picosat.h b/src/solvers/sat/satcheck_picosat.h
diff --git a/src/solvers/sat/satcheck_zchaff.cpp b/src/solvers/sat/satcheck_zchaff.cpp
diff --git a/src/solvers/sat/satcheck_zchaff.h b/src/solvers/sat/satcheck_zchaff.h
diff --git a/src/solvers/sat/satcheck_zcore.cpp b/src/solvers/sat/satcheck_zcore.cpp
diff --git a/src/solvers/sat/satcheck_zcore.h b/src/solvers/sat/satcheck_zcore.h
diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp

Original file line number	Diff line number	Diff line change
`@@ -83,7 +83,7 @@ tvt qbf_bdd_coret::l_get(literalt a) const`
`83`	`83`	`UNREACHABLE;`
`84`	`84`	`}`
`85`	`85`
`86`		`-const std::string qbf_bdd_coret::solver_text()`
	`86`	`+std::string qbf_bdd_coret::solver_text() const`
`87`	`87`	`{`
`88`	`88`	`return "QBF/BDD/CORE";`
`89`	`89`	`}`
Original file line number	Diff line number	Diff line change
`@@ -27,7 +27,7 @@ tvt qbf_quantort::l_get(literalt) const`
`27`	`27`	`UNREACHABLE;`
`28`	`28`	`}`
`29`	`29`
`30`		`-const std::string qbf_quantort::solver_text()`
	`30`	`+std::string qbf_quantort::solver_text() const`
`31`	`31`	`{`
`32`	`32`	`return "Quantor";`
`33`	`33`	`}`
Original file line number	Diff line number	Diff line change
`@@ -29,7 +29,7 @@ tvt qbf_qubet::l_get(literalt) const`
`29`	`29`	`UNREACHABLE;`
`30`	`30`	`}`
`31`	`31`
`32`		`-const std::string qbf_qubet::solver_text()`
	`32`	`+std::string qbf_qubet::solver_text() const`
`33`	`33`	`{`
`34`	`34`	`return "QuBE";`
`35`	`35`	`}`
Original file line number	Diff line number	Diff line change
`@@ -26,7 +26,7 @@ qbf_qube_coret::~qbf_qube_coret()`
`26`	`26`	`{`
`27`	`27`	`}`
`28`	`28`
`29`		`-const std::string qbf_qube_coret::solver_text()`
	`29`	`+std::string qbf_qube_coret::solver_text() const`
`30`	`30`	`{`
`31`	`31`	`return "QuBE w/ toplevel assignments";`
`32`	`32`	`}`
Original file line number	Diff line number	Diff line change
`@@ -29,7 +29,7 @@ tvt qbf_skizzot::l_get(literalt) const`
`29`	`29`	`UNREACHABLE;`
`30`	`30`	`}`
`31`	`31`
`32`		`-const std::string qbf_skizzot::solver_text()`
	`32`	`+std::string qbf_skizzot::solver_text() const`
`33`	`33`	`{`
`34`	`34`	`return "Skizzo";`
`35`	`35`	`}`