Skip to content

Commit b055e6b

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 f7d2983 commit b055e6b

File tree

10 files changed

+65
-63
lines changed

10 files changed

+65
-63
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 & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -34,10 +34,10 @@ const std::string qbf_quantort::solver_text()
3434
propt::resultt qbf_quantort::prop_solve()
3535
{
3636
{
37-
messaget::status() <<
37+
message.status() <<
3838
"Quantor: " <<
3939
no_variables() << " variables, " <<
40-
no_clauses() << " clauses" << eom;
40+
no_clauses() << " clauses" << messaget::eom;
4141
}
4242

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

8888
if(!result_found)
8989
{
90-
messaget::error() << "Quantor failed: unknown result" << eom;
90+
message.error() << "Quantor failed: unknown result" << messaget::eom;
9191
return resultt::P_ERROR;
9292
}
9393
}
9494

9595
if(result)
9696
{
97-
messaget::status() << "Quantor: TRUE" << eom;
97+
message.status() << "Quantor: TRUE" << messaget::eom;
9898
return resultt::P_SATISFIABLE;
9999
}
100100
else
101101
{
102-
messaget::status() << "Quantor: FALSE" << eom;
102+
message.status() << "Quantor: FALSE" << messaget::eom;
103103
return resultt::P_UNSATISFIABLE;
104104
}
105105

‎src/solvers/qbf/qbf_qube.cpp

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

4242
{
43-
messaget::status() <<
43+
message.status() <<
4444
"QuBE: " <<
4545
no_variables() << " variables, " <<
46-
no_clauses() << " clauses" << eom;
46+
no_clauses() << " clauses" << messaget::eom;
4747
}
4848

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

9696
if(!result_found)
9797
{
98-
messaget::error() << "QuBE failed: unknown result" << eom;
98+
message.error() << "QuBE failed: unknown result" << messaget::eom;
9999
return resultt::P_ERROR;
100100
}
101101
}
102102

103103
if(result)
104104
{
105-
messaget::status() << "QuBE: TRUE" << eom;
105+
message.status() << "QuBE: TRUE" << messaget::eom;
106106
return resultt::P_SATISFIABLE;
107107
}
108108
else
109109
{
110-
messaget::status() << "QuBE: FALSE" << eom;
110+
message.status() << "QuBE: FALSE" << messaget::eom;
111111
return resultt::P_UNSATISFIABLE;
112112
}
113113

‎src/solvers/qbf/qbf_qube_core.cpp

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

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

4545
std::string result_tmp_file="qube.out";
@@ -99,33 +99,33 @@ propt::resultt qbf_qube_coret::prop_solve()
9999

100100
if(!result_found)
101101
{
102-
messaget::error() << "QuBE failed: unknown result" << eom;
102+
message.error() << "QuBE failed: unknown result" << messaget::eom;
103103
return resultt::P_ERROR;
104104
}
105105
}
106106

107107
int remove_result=remove(result_tmp_file.c_str());
108108
if(remove_result!=0)
109109
{
110-
messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
110+
message.error() << "Remove failed: " << std::strerror(errno) << 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) << messaget::eom;
118118
return resultt::P_ERROR;
119119
}
120120

121121
if(result)
122122
{
123-
messaget::status() << "QuBE: TRUE" << eom;
123+
message.status() << "QuBE: TRUE" << messaget::eom;
124124
return resultt::P_SATISFIABLE;
125125
}
126126
else
127127
{
128-
messaget::status() << "QuBE: FALSE" << eom;
128+
message.status() << "QuBE: FALSE" << messaget::eom;
129129
return resultt::P_UNSATISFIABLE;
130130
}
131131
}

‎src/solvers/qbf/qbf_skizzo.cpp

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

4242
{
43-
messaget::status() <<
43+
message.status() <<
4444
"Skizzo: " <<
4545
no_variables() << " variables, " <<
46-
no_clauses() << " clauses" << eom;
46+
no_clauses() << " clauses" << messaget::eom;
4747
}
4848

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

9696
if(!result_found)
9797
{
98-
messaget::error() << "Skizzo failed: unknown result" << eom;
98+
message.error() << "Skizzo failed: unknown result" << messaget::eom;
9999
return resultt::P_ERROR;
100100
}
101101
}
102102

103103
if(result)
104104
{
105-
messaget::status() << "Skizzo: TRUE" << eom;
105+
message.status() << "Skizzo: TRUE" << messaget::eom;
106106
return resultt::P_SATISFIABLE;
107107
}
108108
else
109109
{
110-
messaget::status() << "Skizzo: FALSE" << eom;
110+
message.status() << "Skizzo: FALSE" << messaget::eom;
111111
return resultt::P_UNSATISFIABLE;
112112
}
113113

‎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)