Skip to content

Commit 7af156d

Browse files
romainbrenguierromainbrenguier
committed
Stop propt inheriting from messaget
No functional changes. A propt object should not be used as a messaget so the messaget should rather be a field.
1 parent 75bec44 commit 7af156d

File tree

10 files changed

+67
-71
lines changed

10 files changed

+67
-71
lines changed

‎src/cbmc/cbmc_solvers.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
7272
solver->set_prop(util_make_unique<satcheckt>());
7373
}
7474

75-
solver->prop().set_message_handler(message_handler);
75+
solver->prop().message.set_message_handler(message_handler);
7676

7777
auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
7878

@@ -92,7 +92,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
9292
no_incremental_check();
9393

9494
auto prop=util_make_unique<dimacs_cnft>();
95-
prop->set_message_handler(message_handler);
95+
prop->message.set_message_handler(message_handler);
9696

9797
std::string filename=options.get_option("outfile");
9898

@@ -113,7 +113,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
113113
return util_make_unique<satcheck_no_simplifiert>();
114114
}();
115115

116-
prop->set_message_handler(message_handler);
116+
prop->message.set_message_handler(message_handler);
117117

118118
bv_refinementt::infot info;
119119
info.ns=&ns;
@@ -141,7 +141,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
141141
string_refinementt::infot info;
142142
info.ns=&ns;
143143
auto prop=util_make_unique<satcheck_no_simplifiert>();
144-
prop->set_message_handler(message_handler);
144+
prop->message.set_message_handler(message_handler);
145145
info.prop=prop.get();
146146
info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
147147
info.output_xml = output_xml_in_refinement;

‎src/solvers/flattening/arrays.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ literalt arrayst::record_array_equality(
4848
// check types
4949
if(!base_type_eq(op0.type(), op1.type(), ns))
5050
{
51-
prop.error() << equality.pretty() << messaget::eom;
51+
prop.message.error() << equality.pretty() << messaget::eom;
5252
DATA_INVARIANT(
5353
false,
5454
"record_array_equality got equality without matching types");
@@ -117,7 +117,7 @@ void arrayst::collect_arrays(const exprt &a)
117117
// check types
118118
if(!base_type_eq(array_type, with_expr.old().type(), ns))
119119
{
120-
prop.error() << a.pretty() << messaget::eom;
120+
prop.message.error() << a.pretty() << messaget::eom;
121121
DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
122122
}
123123

@@ -135,7 +135,7 @@ void arrayst::collect_arrays(const exprt &a)
135135
// check types
136136
if(!base_type_eq(array_type, update_expr.old().type(), ns))
137137
{
138-
prop.error() << a.pretty() << messaget::eom;
138+
prop.message.error() << a.pretty() << messaget::eom;
139139
DATA_INVARIANT(
140140
false,
141141
"collect_arrays got 'update' without matching types");
@@ -157,14 +157,14 @@ void arrayst::collect_arrays(const exprt &a)
157157
// check types
158158
if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
159159
{
160-
prop.error() << a.pretty() << messaget::eom;
160+
prop.message.error() << a.pretty() << messaget::eom;
161161
DATA_INVARIANT(false, "collect_arrays got if without matching types");
162162
}
163163

164164
// check types
165165
if(!base_type_eq(array_type, if_expr.false_case().type(), ns))
166166
{
167-
prop.error() << a.pretty() << messaget::eom;
167+
prop.message.error() << a.pretty() << messaget::eom;
168168
DATA_INVARIANT(false, "collect_arrays got if without matching types");
169169
}
170170

@@ -518,7 +518,7 @@ void arrayst::add_array_constraints_with(
518518

519519
if(index_expr.type()!=value.type())
520520
{
521-
prop.error() << expr.pretty() << messaget::eom;
521+
prop.message.error() << expr.pretty() << messaget::eom;
522522
DATA_INVARIANT(
523523
false,
524524
"with-expression operand should match array element type");
@@ -588,7 +588,7 @@ void arrayst::add_array_constraints_update(
588588

589589
if(index_expr.type()!=value.type())
590590
{
591-
prop.error() << expr.pretty() << messaget::eom;
591+
prop.message.error() << expr.pretty() << messaget::eom;
592592
DATA_INVARIANT(
593593
false,
594594
"update operand should match array element type");

‎src/solvers/prop/prop.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,10 @@ Author: Daniel Kroening, [email protected]
2121

2222
/*! \brief TO_BE_DOCUMENTED
2323
*/
24-
class propt:public messaget
24+
class propt
2525
{
2626
public:
27+
messaget message;
2728
propt() { }
2829
virtual ~propt() { }
2930

@@ -113,7 +114,7 @@ class propt:public messaget
113114
// Resource limits:
114115
virtual void set_time_limit_seconds(uint32_t)
115116
{
116-
warning() << "CPU limit ignored (not implemented)" << eom;
117+
message.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
117118
}
118119

119120
protected:

‎src/solvers/qbf/qbf_quantor.cpp

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -34,10 +34,8 @@ const std::string qbf_quantort::solver_text()
3434
propt::resultt qbf_quantort::prop_solve()
3535
{
3636
{
37-
messaget::status() <<
38-
"Quantor: " <<
39-
no_variables() << " variables, " <<
40-
no_clauses() << " clauses" << eom;
37+
message.status() << "Quantor: " << no_variables() << " variables, "
38+
<< no_clauses() << " clauses" << messaget::eom;
4139
}
4240

4341
std::string qbf_tmp_file="quantor.qdimacs";
@@ -87,19 +85,19 @@ propt::resultt qbf_quantort::prop_solve()
8785

8886
if(!result_found)
8987
{
90-
messaget::error() << "Quantor failed: unknown result" << eom;
88+
message.error() << "Quantor failed: unknown result" << messaget::eom;
9189
return resultt::P_ERROR;
9290
}
9391
}
9492

9593
if(result)
9694
{
97-
messaget::status() << "Quantor: TRUE" << eom;
95+
message.status() << "Quantor: TRUE" << messaget::eom;
9896
return resultt::P_SATISFIABLE;
9997
}
10098
else
10199
{
102-
messaget::status() << "Quantor: FALSE" << eom;
100+
message.status() << "Quantor: FALSE" << messaget::eom;
103101
return resultt::P_UNSATISFIABLE;
104102
}
105103

‎src/solvers/qbf/qbf_qube.cpp

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -40,10 +40,8 @@ propt::resultt qbf_qubet::prop_solve()
4040
return resultt::P_SATISFIABLE;
4141

4242
{
43-
messaget::status() <<
44-
"QuBE: " <<
45-
no_variables() << " variables, " <<
46-
no_clauses() << " clauses" << eom;
43+
message.status() << "QuBE: " << no_variables() << " variables, "
44+
<< no_clauses() << " clauses" << messaget::eom;
4745
}
4846

4947
std::string qbf_tmp_file="qube.qdimacs";
@@ -95,19 +93,19 @@ propt::resultt qbf_qubet::prop_solve()
9593

9694
if(!result_found)
9795
{
98-
messaget::error() << "QuBE failed: unknown result" << eom;
96+
message.error() << "QuBE failed: unknown result" << messaget::eom;
9997
return resultt::P_ERROR;
10098
}
10199
}
102100

103101
if(result)
104102
{
105-
messaget::status() << "QuBE: TRUE" << eom;
103+
message.status() << "QuBE: TRUE" << messaget::eom;
106104
return resultt::P_SATISFIABLE;
107105
}
108106
else
109107
{
110-
messaget::status() << "QuBE: FALSE" << eom;
108+
message.status() << "QuBE: FALSE" << messaget::eom;
111109
return resultt::P_UNSATISFIABLE;
112110
}
113111

‎src/solvers/qbf/qbf_qube_core.cpp

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -37,9 +37,8 @@ propt::resultt qbf_qube_coret::prop_solve()
3737
return resultt::P_SATISFIABLE;
3838

3939
{
40-
messaget::status() << "QuBE: "
41-
<< no_variables() << " variables, "
42-
<< no_clauses() << " clauses" << eom;
40+
message.status() << "QuBE: " << no_variables() << " variables, "
41+
<< no_clauses() << " clauses" << messaget::eom;
4342
}
4443

4544
std::string result_tmp_file="qube.out";
@@ -99,33 +98,35 @@ propt::resultt qbf_qube_coret::prop_solve()
9998

10099
if(!result_found)
101100
{
102-
messaget::error() << "QuBE failed: unknown result" << eom;
101+
message.error() << "QuBE failed: unknown result" << messaget::eom;
103102
return resultt::P_ERROR;
104103
}
105104
}
106105

107106
int remove_result=remove(result_tmp_file.c_str());
108107
if(remove_result!=0)
109108
{
110-
messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
109+
message.error() << "Remove failed: " << std::strerror(errno)
110+
<< messaget::eom;
111111
return resultt::P_ERROR;
112112
}
113113

114114
remove_result=remove(qbf_tmp_file.c_str());
115115
if(remove_result!=0)
116116
{
117-
messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
117+
message.error() << "Remove failed: " << std::strerror(errno)
118+
<< messaget::eom;
118119
return resultt::P_ERROR;
119120
}
120121

121122
if(result)
122123
{
123-
messaget::status() << "QuBE: TRUE" << eom;
124+
message.status() << "QuBE: TRUE" << messaget::eom;
124125
return resultt::P_SATISFIABLE;
125126
}
126127
else
127128
{
128-
messaget::status() << "QuBE: FALSE" << eom;
129+
message.status() << "QuBE: FALSE" << messaget::eom;
129130
return resultt::P_UNSATISFIABLE;
130131
}
131132
}

‎src/solvers/qbf/qbf_skizzo.cpp

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -40,10 +40,8 @@ propt::resultt qbf_skizzot::prop_solve()
4040
return resultt::P_SATISFIABLE;
4141

4242
{
43-
messaget::status() <<
44-
"Skizzo: " <<
45-
no_variables() << " variables, " <<
46-
no_clauses() << " clauses" << eom;
43+
message.status() << "Skizzo: " << no_variables() << " variables, "
44+
<< no_clauses() << " clauses" << messaget::eom;
4745
}
4846

4947
std::string qbf_tmp_file="sKizzo.qdimacs";
@@ -95,19 +93,19 @@ propt::resultt qbf_skizzot::prop_solve()
9593

9694
if(!result_found)
9795
{
98-
messaget::error() << "Skizzo failed: unknown result" << eom;
96+
message.error() << "Skizzo failed: unknown result" << messaget::eom;
9997
return resultt::P_ERROR;
10098
}
10199
}
102100

103101
if(result)
104102
{
105-
messaget::status() << "Skizzo: TRUE" << eom;
103+
message.status() << "Skizzo: TRUE" << messaget::eom;
106104
return resultt::P_SATISFIABLE;
107105
}
108106
else
109107
{
110-
messaget::status() << "Skizzo: FALSE" << eom;
108+
message.status() << "Skizzo: FALSE" << messaget::eom;
111109
return resultt::P_UNSATISFIABLE;
112110
}
113111

‎src/solvers/sat/pbs_dimacs_cnf.cpp

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,7 @@ bool pbs_dimacs_cnft::pbs_solve()
128128

129129
if(file.fail())
130130
{
131-
error() << "Unable to read SAT results!" << eom;
131+
message.error() << "Unable to read SAT results!" << messaget::eom;
132132
return false;
133133
}
134134

@@ -194,7 +194,8 @@ bool pbs_dimacs_cnft::pbs_solve()
194194
#endif
195195
if(strstr(line.c_str(), "time out") != nullptr)
196196
{
197-
status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT." << eom;
197+
message.status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT."
198+
<< messaget::eom;
198199
return satisfied;
199200
}
200201
sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
@@ -218,21 +219,21 @@ propt::resultt pbs_dimacs_cnft::prop_solve()
218219
pbfile.close();
219220

220221
// We start counting at 1, thus there is one variable fewer.
221-
messaget::status() << (no_variables() - 1) << " variables, " << clauses.size()
222-
<< " clauses" << eom;
222+
message.status() << (no_variables() - 1) << " variables, " << clauses.size()
223+
<< " clauses" << messaget::eom;
223224

224225
const bool result = pbs_solve();
225226

226227
if(!result)
227228
{
228-
messaget::status() << "PBS checker: system is UNSATISFIABLE" << eom;
229+
message.status() << "PBS checker: system is UNSATISFIABLE" << messaget::eom;
229230
}
230231
else
231232
{
232-
messaget::status() << "PBS checker: system is SATISFIABLE";
233+
message.status() << "PBS checker: system is SATISFIABLE";
233234
if(optimize)
234-
messaget::status() << " (distance " << opt_sum << ")";
235-
messaget::status() << eom;
235+
message.status() << " (distance " << opt_sum << ")";
236+
message.status() << messaget::eom;
236237
}
237238

238239
if(result)

0 commit comments

Comments
 (0)