Skip to content

Commit c0d987c

Browse files
tautschnigtautschnig
authored
Merge pull request #7260 from tautschnig/cleanup/solver_text-const
Make propt::solver_text const
2 parents daefb6a + 400c03e commit c0d987c

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

44 files changed

+99
-100
lines changed

‎src/solvers/prop/prop.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ class propt
9393
virtual bvt new_variables(std::size_t width);
9494

9595
// solving
96-
virtual const std::string solver_text()=0;
96+
virtual std::string solver_text() const = 0;
9797
enum class resultt { P_SATISFIABLE, P_UNSATISFIABLE, P_ERROR };
9898
resultt prop_solve();
9999

‎src/solvers/qbf/qbf_bdd_core.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ tvt qbf_bdd_coret::l_get(literalt a) const
8383
UNREACHABLE;
8484
}
8585

86-
const std::string qbf_bdd_coret::solver_text()
86+
std::string qbf_bdd_coret::solver_text() const
8787
{
8888
return "QBF/BDD/CORE";
8989
}

‎src/solvers/qbf/qbf_bdd_core.h

+14-14
Original file line numberDiff line numberDiff line change
@@ -31,12 +31,12 @@ class qbf_bdd_certificatet:public qdimacs_coret
3131

3232
public:
3333
qbf_bdd_certificatet(void);
34-
virtual ~qbf_bdd_certificatet(void);
34+
~qbf_bdd_certificatet(void) override;
3535

36-
virtual literalt new_variable(void);
36+
literalt new_variable(void) override;
3737

38-
virtual tvt l_get(literalt a) const;
39-
virtual const exprt f_get(literalt l);
38+
tvt l_get(literalt a) const override;
39+
const exprt f_get(literalt l) override;
4040
};
4141

4242

@@ -50,20 +50,20 @@ class qbf_bdd_coret:public qbf_bdd_certificatet
5050

5151
public:
5252
qbf_bdd_coret();
53-
virtual ~qbf_bdd_coret();
53+
~qbf_bdd_coret() override;
5454

55-
virtual literalt new_variable();
55+
literalt new_variable() override;
5656

57-
virtual void lcnf(const bvt &bv);
58-
virtual literalt lor(literalt a, literalt b);
59-
virtual literalt lor(const bvt &bv);
57+
void lcnf(const bvt &bv) override;
58+
literalt lor(literalt a, literalt b) override;
59+
literalt lor(const bvt &bv) override;
6060

61-
virtual const std::string solver_text();
62-
virtual resultt prop_solve();
63-
virtual tvt l_get(literalt a) const;
61+
std::string solver_text() const override;
62+
resultt prop_solve() override;
63+
tvt l_get(literalt a) const override;
6464

65-
virtual bool is_in_core(literalt l) const;
66-
virtual modeltypet m_get(literalt a) const;
65+
bool is_in_core(literalt l) const override;
66+
modeltypet m_get(literalt a) const override;
6767

6868
protected:
6969
void compress_certificate(void);

‎src/solvers/qbf/qbf_quantor.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ tvt qbf_quantort::l_get(literalt) const
2727
UNREACHABLE;
2828
}
2929

30-
const std::string qbf_quantort::solver_text()
30+
std::string qbf_quantort::solver_text() const
3131
{
3232
return "Quantor";
3333
}

‎src/solvers/qbf/qbf_quantor.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,11 @@ class qbf_quantort:public qdimacs_cnft
1616
{
1717
public:
1818
explicit qbf_quantort(message_handlert &message_handler);
19-
virtual ~qbf_quantort();
19+
~qbf_quantort() override;
2020

21-
virtual const std::string solver_text();
21+
std::string solver_text() const override;
2222
virtual resultt prop_solve();
23-
virtual tvt l_get(literalt a) const;
23+
tvt l_get(literalt a) const override;
2424
};
2525

2626
#endif // CPROVER_SOLVERS_QBF_QBF_QUANTOR_H

‎src/solvers/qbf/qbf_qube.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ tvt qbf_qubet::l_get(literalt) const
2929
UNREACHABLE;
3030
}
3131

32-
const std::string qbf_qubet::solver_text()
32+
std::string qbf_qubet::solver_text() const
3333
{
3434
return "QuBE";
3535
}

‎src/solvers/qbf/qbf_qube.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,11 @@ class qbf_qubet:public qdimacs_cnft
1616
{
1717
public:
1818
explicit qbf_qubet(message_handlert &message_handler);
19-
virtual ~qbf_qubet();
19+
~qbf_qubet() override;
2020

21-
virtual const std::string solver_text();
21+
std::string solver_text() const override;
2222
virtual resultt prop_solve();
23-
virtual tvt l_get(literalt a) const;
23+
tvt l_get(literalt a) const override;
2424
};
2525

2626
#endif // CPROVER_SOLVERS_QBF_QBF_QUBE_H

‎src/solvers/qbf/qbf_qube_core.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ qbf_qube_coret::~qbf_qube_coret()
2626
{
2727
}
2828

29-
const std::string qbf_qube_coret::solver_text()
29+
std::string qbf_qube_coret::solver_text() const
3030
{
3131
return "QuBE w/ toplevel assignments";
3232
}

‎src/solvers/qbf/qbf_qube_core.h

+6-6
Original file line numberDiff line numberDiff line change
@@ -24,14 +24,14 @@ class qbf_qube_coret:public qdimacs_coret
2424

2525
public:
2626
explicit qbf_qube_coret(message_handlert &message_handler);
27-
virtual ~qbf_qube_coret();
27+
~qbf_qube_coret() override;
2828

29-
virtual const std::string solver_text();
29+
std::string solver_text() const override;
3030
virtual resultt prop_solve();
3131

32-
virtual bool is_in_core(literalt l) const;
32+
bool is_in_core(literalt l) const override;
3333

34-
virtual tvt l_get(literalt a) const
34+
tvt l_get(literalt a) const override
3535
{
3636
unsigned v=a.var_no();
3737

@@ -49,9 +49,9 @@ class qbf_qube_coret:public qdimacs_coret
4949
return tvt::unknown();
5050
}
5151

52-
virtual modeltypet m_get(literalt a) const;
52+
modeltypet m_get(literalt a) const override;
5353

54-
virtual const exprt f_get(literalt)
54+
const exprt f_get(literalt) override
5555
{
5656
INVARIANT(false, "qube does not support full certificates.");
5757
}

‎src/solvers/qbf/qbf_skizzo.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ tvt qbf_skizzot::l_get(literalt) const
2929
UNREACHABLE;
3030
}
3131

32-
const std::string qbf_skizzot::solver_text()
32+
std::string qbf_skizzot::solver_text() const
3333
{
3434
return "Skizzo";
3535
}

‎src/solvers/qbf/qbf_skizzo.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,11 @@ class qbf_skizzot:public qdimacs_cnft
1616
{
1717
public:
1818
explicit qbf_skizzot(message_handlert &message_handler);
19-
virtual ~qbf_skizzot();
19+
~qbf_skizzot() override;
2020

21-
virtual const std::string solver_text();
21+
std::string solver_text() const override;
2222
virtual resultt prop_solve();
23-
virtual tvt l_get(literalt a) const;
23+
tvt l_get(literalt a) const override;
2424
};
2525

2626
#endif // CPROVER_SOLVERS_QBF_QBF_SKIZZO_H

‎src/solvers/qbf/qbf_skizzo_core.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ qbf_skizzo_coret::~qbf_skizzo_coret()
3939
{
4040
}
4141

42-
const std::string qbf_skizzo_coret::solver_text()
42+
std::string qbf_skizzo_coret::solver_text() const
4343
{
4444
return "Skizzo/Core";
4545
}

‎src/solvers/qbf/qbf_skizzo_core.h

+5-5
Original file line numberDiff line numberDiff line change
@@ -17,13 +17,13 @@ class qbf_skizzo_coret:public qbf_bdd_certificatet
1717
{
1818
public:
1919
qbf_skizzo_coret();
20-
virtual ~qbf_skizzo_coret();
20+
~qbf_skizzo_coret() override;
2121

22-
virtual const std::string solver_text();
23-
virtual resultt prop_solve();
22+
std::string solver_text() const override;
23+
resultt prop_solve() override;
2424

25-
virtual bool is_in_core(literalt l) const;
26-
virtual modeltypet m_get(literalt a) const;
25+
bool is_in_core(literalt l) const override;
26+
modeltypet m_get(literalt a) const override;
2727

2828
protected:
2929
std::string qbf_tmp_file;

‎src/solvers/qbf/qbf_squolem.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ tvt qbf_squolemt::l_get(literalt a) const
2626
UNREACHABLE;
2727
}
2828

29-
const std::string qbf_squolemt::solver_text()
29+
std::string qbf_squolemt::solver_text() const
3030
{
3131
return "Squolem";
3232
}

‎src/solvers/qbf/qbf_squolem.h

+8-8
Original file line numberDiff line numberDiff line change
@@ -24,16 +24,16 @@ class qbf_squolemt:public qdimacs_cnft
2424

2525
public:
2626
qbf_squolemt();
27-
virtual ~qbf_squolemt();
27+
~qbf_squolemt() override;
2828

29-
virtual const std::string solver_text();
30-
virtual resultt prop_solve();
31-
virtual tvt l_get(literalt a) const;
29+
std::string solver_text() const override;
30+
resultt prop_solve() override;
31+
tvt l_get(literalt a) const override;
3232

33-
virtual void lcnf(const bvt &bv);
34-
virtual void add_quantifier(const quantifiert &quantifier);
35-
virtual void set_quantifier(const quantifiert::typet type, const literalt l);
36-
virtual void set_no_variables(size_t no);
33+
void lcnf(const bvt &bv) override;
34+
void add_quantifier(const quantifiert &quantifier) override;
35+
void set_quantifier(const quantifiert::typet type, const literalt l) override;
36+
void set_no_variables(size_t no) override;
3737
virtual size_t no_clauses() const { return squolem.clauses(); }
3838
};
3939

‎src/solvers/qbf/qbf_squolem_core.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ tvt qbf_squolem_coret::l_get(literalt a) const
7474
return tvt(tvt::tv_enumt::TV_UNKNOWN);
7575
}
7676

77-
const std::string qbf_squolem_coret::solver_text()
77+
std::string qbf_squolem_coret::solver_text() const
7878
{
7979
return "Squolem (Certifying)";
8080
}

‎src/solvers/qbf/qbf_squolem_core.h

+12-12
Original file line numberDiff line numberDiff line change
@@ -24,29 +24,29 @@ class qbf_squolem_coret:public qdimacs_coret
2424

2525
public:
2626
qbf_squolem_coret();
27-
virtual ~qbf_squolem_coret();
27+
~qbf_squolem_coret() override;
2828

29-
virtual const std::string solver_text();
30-
virtual resultt prop_solve();
29+
std::string solver_text() const override;
30+
resultt prop_solve() override;
3131

32-
virtual tvt l_get(literalt a) const;
33-
virtual bool is_in_core(literalt l) const;
32+
tvt l_get(literalt a) const override;
33+
bool is_in_core(literalt l) const override;
3434

3535
void set_debug_filename(const std::string &str);
3636

37-
virtual void lcnf(const bvt &bv);
38-
virtual void add_quantifier(const quantifiert &quantifier);
39-
virtual void set_quantifier(const quantifiert::typet type, const literalt l);
40-
virtual void set_no_variables(size_t no);
37+
void lcnf(const bvt &bv) override;
38+
void add_quantifier(const quantifiert &quantifier) override;
39+
void set_quantifier(const quantifiert::typet type, const literalt l) override;
40+
void set_no_variables(size_t no) override;
4141
virtual size_t no_clauses() const { return squolem->clauses(); }
4242

43-
virtual modeltypet m_get(literalt a) const;
43+
modeltypet m_get(literalt a) const override;
4444

45-
virtual void write_qdimacs_cnf(std::ostream &out);
45+
void write_qdimacs_cnf(std::ostream &out) override;
4646

4747
void reset(void);
4848

49-
virtual const exprt f_get(literalt l);
49+
const exprt f_get(literalt l) override;
5050

5151
private:
5252
typedef std::unordered_map<unsigned, exprt> function_cachet;

‎src/solvers/qbf/qdimacs_cnf.h

+1-2
Original file line numberDiff line numberDiff line change
@@ -21,13 +21,12 @@ class qdimacs_cnft:public dimacs_cnft
2121
: dimacs_cnft(message_handler)
2222
{
2323
}
24-
virtual ~qdimacs_cnft() { }
2524

2625
virtual void write_qdimacs_cnf(std::ostream &out);
2726

2827
// dummy functions
2928

30-
virtual const std::string solver_text()
29+
std::string solver_text() const override
3130
{
3231
return "QDIMACS CNF";
3332
}

‎src/solvers/sat/cnf_clause_list.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ class cnf_clause_listt:public cnft
3131

3232
void lcnf(const bvt &bv) override;
3333

34-
const std::string solver_text() override
34+
std::string solver_text() const override
3535
{ return "CNF clause list"; }
3636

3737
tvt l_get(literalt) const override

‎src/solvers/sat/dimacs_cnf.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ class dimacs_cnft:public cnf_clause_listt
2424

2525
// dummy functions
2626

27-
const std::string solver_text() override
27+
std::string solver_text() const override
2828
{
2929
return "DIMACS CNF";
3030
}
@@ -48,7 +48,7 @@ class dimacs_cnf_dumpt:public cnft
4848
dimacs_cnf_dumpt(std::ostream &_out, message_handlert &message_handler);
4949
virtual ~dimacs_cnf_dumpt() { }
5050

51-
const std::string solver_text() override
51+
std::string solver_text() const override
5252
{
5353
return "DIMACS CNF Dumper";
5454
}

‎src/solvers/sat/external_sat.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ external_satt::external_satt(message_handlert &message_handler, std::string cmd)
2121
{
2222
}
2323

24-
const std::string external_satt::solver_text()
24+
std::string external_satt::solver_text() const
2525
{
2626
return "External SAT solver";
2727
}

‎src/solvers/sat/external_sat.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ class external_satt : public cnf_clause_list_assignmentt
2222
return false;
2323
}
2424

25-
const std::string solver_text() override;
25+
std::string solver_text() const override;
2626

2727
bool is_in_conflict(literalt) const override;
2828
void set_assignment(literalt, bool) override;

‎src/solvers/sat/pbs_dimacs_cnf.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ class pbs_dimacs_cnft:public dimacs_cnft
5252

5353
// dummy functions
5454

55-
const std::string solver_text() override
55+
std::string solver_text() const override
5656
{
5757
return "PBS - Pseudo Boolean/CNF Solver and Optimizer";
5858
}

‎src/solvers/sat/satcheck_booleforce.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ tvt satcheck_booleforce_baset::l_get(literalt a) const
5858
return result;
5959
}
6060

61-
const std::string satcheck_booleforce_baset::solver_text()
61+
std::string satcheck_booleforce_baset::solver_text() const
6262
{
6363
return std::string("Booleforce version ")+booleforce_version();
6464
}

‎src/solvers/sat/satcheck_booleforce.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ class satcheck_booleforce_baset:public cnf_solvert
2020
public:
2121
virtual ~satcheck_booleforce_baset();
2222

23-
const std::string solver_text() override;
23+
std::string solver_text() const override;
2424
tvt l_get(literalt a) const override;
2525

2626
void lcnf(const bvt &bv) override;

‎src/solvers/sat/satcheck_cadical.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ tvt satcheck_cadicalt::l_get(literalt a) const
3838
return result;
3939
}
4040

41-
const std::string satcheck_cadicalt::solver_text()
41+
std::string satcheck_cadicalt::solver_text() const
4242
{
4343
return std::string("CaDiCaL ") + solver->version();
4444
}

‎src/solvers/sat/satcheck_cadical.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
2525
explicit satcheck_cadicalt(message_handlert &message_handler);
2626
virtual ~satcheck_cadicalt();
2727

28-
const std::string solver_text() override;
28+
std::string solver_text() const override;
2929
tvt l_get(literalt a) const override;
3030

3131
void lcnf(const bvt &bv) override;

0 commit comments

Comments
 (0)