Skip to content

Commit 4aa485f

Browse files
tautschnigtautschnig
authored
Merge pull request #3249 from romainbrenguier/refactor/propt-messaget
Stop propt inheriting from messaget [blocks: #3800]
2 parents c74d257 + 756b003 commit 4aa485f

File tree

13 files changed

+93
-81
lines changed

13 files changed

+93
-81
lines changed

‎src/goto-checker/solver_factory.cpp

Lines changed: 7 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -149,15 +149,14 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
149149
!options.get_bool_option("sat-preprocessor")) // no simplifier
150150
{
151151
// simplifier won't work with beautification
152-
solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
152+
solver->set_prop(
153+
util_make_unique<satcheck_no_simplifiert>(message_handler));
153154
}
154155
else // with simplifier
155156
{
156-
solver->set_prop(util_make_unique<satcheckt>());
157+
solver->set_prop(util_make_unique<satcheckt>(message_handler));
157158
}
158159

159-
solver->prop().set_message_handler(message_handler);
160-
161160
auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
162161

163162
if(options.get_option("arrays-uf") == "never")
@@ -176,8 +175,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
176175
no_beautification();
177176
no_incremental_check();
178177

179-
auto prop = util_make_unique<dimacs_cnft>();
180-
prop->set_message_handler(message_handler);
178+
auto prop = util_make_unique<dimacs_cnft>(message_handler);
181179

182180
std::string filename = options.get_option("outfile");
183181

@@ -192,13 +190,11 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
192190
if(options.get_bool_option("sat-preprocessor"))
193191
{
194192
no_beautification();
195-
return util_make_unique<satcheckt>();
193+
return util_make_unique<satcheckt>(message_handler);
196194
}
197-
return util_make_unique<satcheck_no_simplifiert>();
195+
return util_make_unique<satcheck_no_simplifiert>(message_handler);
198196
}();
199197

200-
prop->set_message_handler(message_handler);
201-
202198
bv_refinementt::infot info;
203199
info.ns = &ns;
204200
info.prop = prop.get();
@@ -225,8 +221,7 @@ solver_factoryt::get_string_refinement()
225221
{
226222
string_refinementt::infot info;
227223
info.ns = &ns;
228-
auto prop = util_make_unique<satcheck_no_simplifiert>();
229-
prop->set_message_handler(message_handler);
224+
auto prop = util_make_unique<satcheck_no_simplifiert>(message_handler);
230225
info.prop = prop.get();
231226
info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
232227
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+
error() << equality.pretty() << messaget::eom;
5252
DATA_INVARIANT(
5353
false,
5454
"record_array_equality got equality without matching types");
@@ -116,7 +116,7 @@ void arrayst::collect_arrays(const exprt &a)
116116
// check types
117117
if(!base_type_eq(array_type, with_expr.old().type(), ns))
118118
{
119-
prop.error() << a.pretty() << messaget::eom;
119+
error() << a.pretty() << messaget::eom;
120120
DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
121121
}
122122

@@ -134,7 +134,7 @@ void arrayst::collect_arrays(const exprt &a)
134134
// check types
135135
if(!base_type_eq(array_type, update_expr.old().type(), ns))
136136
{
137-
prop.error() << a.pretty() << messaget::eom;
137+
error() << a.pretty() << messaget::eom;
138138
DATA_INVARIANT(
139139
false,
140140
"collect_arrays got 'update' without matching types");
@@ -156,14 +156,14 @@ void arrayst::collect_arrays(const exprt &a)
156156
// check types
157157
if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
158158
{
159-
prop.error() << a.pretty() << messaget::eom;
159+
error() << a.pretty() << messaget::eom;
160160
DATA_INVARIANT(false, "collect_arrays got if without matching types");
161161
}
162162

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

@@ -511,7 +511,7 @@ void arrayst::add_array_constraints_with(
511511

512512
if(index_expr.type()!=value.type())
513513
{
514-
prop.error() << expr.pretty() << messaget::eom;
514+
error() << expr.pretty() << messaget::eom;
515515
DATA_INVARIANT(
516516
false,
517517
"with-expression operand should match array element type");
@@ -580,7 +580,7 @@ void arrayst::add_array_constraints_update(
580580

581581
if(index_expr.type()!=value.type())
582582
{
583-
prop.error() << expr.pretty() << messaget::eom;
583+
prop.message.error() << expr.pretty() << messaget::eom;
584584
DATA_INVARIANT(
585585
false,
586586
"update operand should match array element type");

‎src/solvers/prop/prop.h

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

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

3031
// boolean operators
@@ -113,12 +114,14 @@ 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+
log.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
117118
}
118119

119120
protected:
120121
// to avoid a temporary for lcnf(...)
121122
bvt lcnf_bv;
123+
124+
messaget log;
122125
};
123126

124127
#endif // CPROVER_SOLVERS_PROP_PROP_H

‎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+
log.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+
log.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+
log.status() << "Quantor: TRUE" << messaget::eom;
9896
return resultt::P_SATISFIABLE;
9997
}
10098
else
10199
{
102-
messaget::status() << "Quantor: FALSE" << eom;
100+
log.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+
log.status() << "QuBE: " << no_variables() << " variables, " << no_clauses()
44+
<< " 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+
log.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+
log.status() << "QuBE: TRUE" << messaget::eom;
106104
return resultt::P_SATISFIABLE;
107105
}
108106
else
109107
{
110-
messaget::status() << "QuBE: FALSE" << eom;
108+
log.status() << "QuBE: FALSE" << messaget::eom;
111109
return resultt::P_UNSATISFIABLE;
112110
}
113111

‎src/solvers/qbf/qbf_qube_core.cpp

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

3838
{
39-
messaget::status() << "QuBE: "
40-
<< no_variables() << " variables, "
41-
<< no_clauses() << " clauses" << eom;
39+
log.status() << "QuBE: " << no_variables() << " variables, " << no_clauses()
40+
<< " clauses" << messaget::eom;
4241
}
4342

4443
std::string result_tmp_file="qube.out";
@@ -98,33 +97,33 @@ propt::resultt qbf_qube_coret::prop_solve()
9897

9998
if(!result_found)
10099
{
101-
messaget::error() << "QuBE failed: unknown result" << eom;
100+
log.error() << "QuBE failed: unknown result" << messaget::eom;
102101
return resultt::P_ERROR;
103102
}
104103
}
105104

106105
int remove_result=remove(result_tmp_file.c_str());
107106
if(remove_result!=0)
108107
{
109-
messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
108+
log.error() << "Remove failed: " << std::strerror(errno) << messaget::eom;
110109
return resultt::P_ERROR;
111110
}
112111

113112
remove_result=remove(qbf_tmp_file.c_str());
114113
if(remove_result!=0)
115114
{
116-
messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
115+
log.error() << "Remove failed: " << std::strerror(errno) << messaget::eom;
117116
return resultt::P_ERROR;
118117
}
119118

120119
if(result)
121120
{
122-
messaget::status() << "QuBE: TRUE" << eom;
121+
log.status() << "QuBE: TRUE" << messaget::eom;
123122
return resultt::P_SATISFIABLE;
124123
}
125124
else
126125
{
127-
messaget::status() << "QuBE: FALSE" << eom;
126+
log.status() << "QuBE: FALSE" << messaget::eom;
128127
return resultt::P_UNSATISFIABLE;
129128
}
130129
}

‎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+
log.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+
log.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+
log.status() << "Skizzo: TRUE" << messaget::eom;
106104
return resultt::P_SATISFIABLE;
107105
}
108106
else
109107
{
110-
messaget::status() << "Skizzo: FALSE" << eom;
108+
log.status() << "Skizzo: FALSE" << messaget::eom;
111109
return resultt::P_UNSATISFIABLE;
112110
}
113111

‎src/solvers/sat/dimacs_cnf.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,11 @@ dimacs_cnft::dimacs_cnft():break_lines(false)
1919
{
2020
}
2121

22+
dimacs_cnft::dimacs_cnft(message_handlert &message_handler) : dimacs_cnft()
23+
{
24+
log.set_message_handler(message_handler);
25+
}
26+
2227
void dimacs_cnft::set_assignment(literalt, bool)
2328
{
2429
UNIMPLEMENTED;

‎src/solvers/sat/dimacs_cnf.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ class dimacs_cnft:public cnf_clause_listt
1818
{
1919
public:
2020
dimacs_cnft();
21+
explicit dimacs_cnft(message_handlert &);
2122
virtual ~dimacs_cnft() { }
2223

2324
virtual void write_dimacs_cnf(std::ostream &out);

‎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+
log.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+
log.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::statistics() << (no_variables() - 1) << " variables, "
222-
<< clauses.size() << " clauses" << eom;
222+
log.statistics() << (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+
log.status() << "PBS checker: system is UNSATISFIABLE" << messaget::eom;
229230
}
230231
else
231232
{
232-
messaget::status() << "PBS checker: system is SATISFIABLE";
233+
log.status() << "PBS checker: system is SATISFIABLE";
233234
if(optimize)
234-
messaget::status() << " (distance " << opt_sum << ")";
235-
messaget::status() << eom;
235+
log.status() << " (distance " << opt_sum << ")";
236+
log.status() << messaget::eom;
236237
}
237238

238239
if(result)

0 commit comments

Comments
 (0)