Skip to content

Commit b7aeac9

Browse files
romainbrenguierromainbrenguier
committed
fixup! Stop propt inheriting from messaget
1 parent 3485803 commit b7aeac9

File tree

8 files changed

+54
-57
lines changed

8 files changed

+54
-57
lines changed

‎src/solvers/prop/prop.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -114,14 +114,14 @@ class propt
114114
// Resource limits:
115115
virtual void set_time_limit_seconds(uint32_t)
116116
{
117-
message.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
117+
log.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
118118
}
119119

120120
protected:
121121
// to avoid a temporary for lcnf(...)
122122
bvt lcnf_bv;
123123

124-
messaget message;
124+
messaget log;
125125
};
126126

127127
#endif // CPROVER_SOLVERS_PROP_PROP_H

‎src/solvers/qbf/qbf_quantor.cpp

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

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

8686
if(!result_found)
8787
{
88-
message.error() << "Quantor failed: unknown result" << messaget::eom;
88+
log.error() << "Quantor failed: unknown result" << messaget::eom;
8989
return resultt::P_ERROR;
9090
}
9191
}
9292

9393
if(result)
9494
{
95-
message.status() << "Quantor: TRUE" << messaget::eom;
95+
log.status() << "Quantor: TRUE" << messaget::eom;
9696
return resultt::P_SATISFIABLE;
9797
}
9898
else
9999
{
100-
message.status() << "Quantor: FALSE" << messaget::eom;
100+
log.status() << "Quantor: FALSE" << messaget::eom;
101101
return resultt::P_UNSATISFIABLE;
102102
}
103103

‎src/solvers/qbf/qbf_qube.cpp

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

4242
{
43-
message.status() << "QuBE: " << no_variables() << " variables, "
44-
<< no_clauses() << " clauses" << messaget::eom;
43+
log.status() << "QuBE: " << no_variables() << " variables, " << no_clauses()
44+
<< " clauses" << messaget::eom;
4545
}
4646

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

9494
if(!result_found)
9595
{
96-
message.error() << "QuBE failed: unknown result" << messaget::eom;
96+
log.error() << "QuBE failed: unknown result" << messaget::eom;
9797
return resultt::P_ERROR;
9898
}
9999
}
100100

101101
if(result)
102102
{
103-
message.status() << "QuBE: TRUE" << messaget::eom;
103+
log.status() << "QuBE: TRUE" << messaget::eom;
104104
return resultt::P_SATISFIABLE;
105105
}
106106
else
107107
{
108-
message.status() << "QuBE: FALSE" << messaget::eom;
108+
log.status() << "QuBE: FALSE" << messaget::eom;
109109
return resultt::P_UNSATISFIABLE;
110110
}
111111

‎src/solvers/qbf/qbf_qube_core.cpp

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

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

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

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

106106
int remove_result=remove(result_tmp_file.c_str());
107107
if(remove_result!=0)
108108
{
109-
message.error() << "Remove failed: " << std::strerror(errno)
110-
<< messaget::eom;
109+
log.error() << "Remove failed: " << std::strerror(errno) << messaget::eom;
111110
return resultt::P_ERROR;
112111
}
113112

114113
remove_result=remove(qbf_tmp_file.c_str());
115114
if(remove_result!=0)
116115
{
117-
message.error() << "Remove failed: " << std::strerror(errno)
118-
<< messaget::eom;
116+
log.error() << "Remove failed: " << std::strerror(errno) << messaget::eom;
119117
return resultt::P_ERROR;
120118
}
121119

122120
if(result)
123121
{
124-
message.status() << "QuBE: TRUE" << messaget::eom;
122+
log.status() << "QuBE: TRUE" << messaget::eom;
125123
return resultt::P_SATISFIABLE;
126124
}
127125
else
128126
{
129-
message.status() << "QuBE: FALSE" << messaget::eom;
127+
log.status() << "QuBE: FALSE" << messaget::eom;
130128
return resultt::P_UNSATISFIABLE;
131129
}
132130
}

‎src/solvers/qbf/qbf_skizzo.cpp

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

4242
{
43-
message.status() << "Skizzo: " << no_variables() << " variables, "
44-
<< no_clauses() << " clauses" << messaget::eom;
43+
log.status() << "Skizzo: " << no_variables() << " variables, "
44+
<< no_clauses() << " clauses" << messaget::eom;
4545
}
4646

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

9494
if(!result_found)
9595
{
96-
message.error() << "Skizzo failed: unknown result" << messaget::eom;
96+
log.error() << "Skizzo failed: unknown result" << messaget::eom;
9797
return resultt::P_ERROR;
9898
}
9999
}
100100

101101
if(result)
102102
{
103-
message.status() << "Skizzo: TRUE" << messaget::eom;
103+
log.status() << "Skizzo: TRUE" << messaget::eom;
104104
return resultt::P_SATISFIABLE;
105105
}
106106
else
107107
{
108-
message.status() << "Skizzo: FALSE" << messaget::eom;
108+
log.status() << "Skizzo: FALSE" << messaget::eom;
109109
return resultt::P_UNSATISFIABLE;
110110
}
111111

‎src/solvers/sat/dimacs_cnf.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ dimacs_cnft::dimacs_cnft():break_lines(false)
2121

2222
dimacs_cnft::dimacs_cnft(message_handlert &message_handler) : dimacs_cnft()
2323
{
24-
message.set_message_handler(message_handler);
24+
log.set_message_handler(message_handler);
2525
}
2626

2727
void dimacs_cnft::set_assignment(literalt, bool)

‎src/solvers/sat/pbs_dimacs_cnf.cpp

Lines changed: 9 additions & 9 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-
message.error() << "Unable to read SAT results!" << messaget::eom;
131+
log.error() << "Unable to read SAT results!" << messaget::eom;
132132
return false;
133133
}
134134

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

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

225225
const bool result = pbs_solve();
226226

227227
if(!result)
228228
{
229-
message.status() << "PBS checker: system is UNSATISFIABLE" << messaget::eom;
229+
log.status() << "PBS checker: system is UNSATISFIABLE" << messaget::eom;
230230
}
231231
else
232232
{
233-
message.status() << "PBS checker: system is SATISFIABLE";
233+
log.status() << "PBS checker: system is SATISFIABLE";
234234
if(optimize)
235-
message.status() << " (distance " << opt_sum << ")";
236-
message.status() << messaget::eom;
235+
log.status() << " (distance " << opt_sum << ")";
236+
log.status() << messaget::eom;
237237
}
238238

239239
if(result)

‎src/solvers/sat/satcheck_minisat2.cpp

Lines changed: 20 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value)
7878
}
7979
catch(Minisat::OutOfMemoryException)
8080
{
81-
message.error() << "SAT checker ran out of memory" << messaget::eom;
81+
log.error() << "SAT checker ran out of memory" << messaget::eom;
8282
status = statust::ERROR;
8383
throw std::bad_alloc();
8484
}
@@ -144,7 +144,7 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
144144
}
145145
catch(const Minisat::OutOfMemoryException &)
146146
{
147-
message.error() << "SAT checker ran out of memory" << messaget::eom;
147+
log.error() << "SAT checker ran out of memory" << messaget::eom;
148148
status = statust::ERROR;
149149
throw std::bad_alloc();
150150
}
@@ -167,8 +167,8 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
167167
PRECONDITION(status != statust::ERROR);
168168

169169
{
170-
message.status() << (no_variables() - 1) << " variables, "
171-
<< solver->nClauses() << " clauses" << messaget::eom;
170+
log.status() << (no_variables() - 1) << " variables, " << solver->nClauses()
171+
<< " clauses" << messaget::eom;
172172
}
173173

174174
try
@@ -177,8 +177,8 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
177177

178178
if(!solver->okay())
179179
{
180-
message.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
181-
<< messaget::eom;
180+
log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
181+
<< messaget::eom;
182182
}
183183
else
184184
{
@@ -191,8 +191,8 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
191191

192192
if(has_false)
193193
{
194-
message.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
195-
<< messaget::eom;
194+
log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
195+
<< messaget::eom;
196196
}
197197
else
198198
{
@@ -210,8 +210,7 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
210210
solver_to_interrupt=solver;
211211
old_handler=signal(SIGALRM, interrupt_solver);
212212
if(old_handler==SIG_ERR)
213-
message.warning() << "Failed to set solver time limit"
214-
<< messaget::eom;
213+
log.warning() << "Failed to set solver time limit" << messaget::eom;
215214
else
216215
alarm(time_limit_seconds);
217216
}
@@ -240,21 +239,21 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
240239

241240
if(solver_result==l_True)
242241
{
243-
message.status() << "SAT checker: instance is SATISFIABLE"
244-
<< messaget::eom;
242+
log.status() << "SAT checker: instance is SATISFIABLE"
243+
<< messaget::eom;
245244
CHECK_RETURN(solver->model.size()>0);
246245
status=statust::SAT;
247246
return resultt::P_SATISFIABLE;
248247
}
249248
else if(solver_result==l_False)
250249
{
251-
message.status() << "SAT checker: instance is UNSATISFIABLE"
252-
<< messaget::eom;
250+
log.status() << "SAT checker: instance is UNSATISFIABLE"
251+
<< messaget::eom;
253252
}
254253
else
255254
{
256-
message.status() << "SAT checker: timed out or other error"
257-
<< messaget::eom;
255+
log.status() << "SAT checker: timed out or other error"
256+
<< messaget::eom;
258257
status=statust::ERROR;
259258
return resultt::P_ERROR;
260259
}
@@ -266,7 +265,7 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
266265
}
267266
catch(const Minisat::OutOfMemoryException &)
268267
{
269-
message.error() << "SAT checker ran out of memory" << messaget::eom;
268+
log.error() << "SAT checker ran out of memory" << messaget::eom;
270269
status=statust::ERROR;
271270
return resultt::P_ERROR;
272271
}
@@ -289,7 +288,7 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
289288
}
290289
catch(const Minisat::OutOfMemoryException &)
291290
{
292-
message.error() << "SAT checker ran out of memory" << messaget::eom;
291+
log.error() << "SAT checker ran out of memory" << messaget::eom;
293292
status = statust::ERROR;
294293
throw std::bad_alloc();
295294
}
@@ -347,7 +346,7 @@ satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(
347346
message_handlert &message_handler)
348347
: satcheck_minisat_no_simplifiert()
349348
{
350-
message.set_message_handler(message_handler);
349+
log.set_message_handler(message_handler);
351350
}
352351

353352
satcheck_minisat_simplifiert::satcheck_minisat_simplifiert():
@@ -359,7 +358,7 @@ satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
359358
message_handlert &message_handler)
360359
: satcheck_minisat_simplifiert()
361360
{
362-
message.set_message_handler(message_handler);
361+
log.set_message_handler(message_handler);
363362
}
364363

365364
void satcheck_minisat_simplifiert::set_frozen(literalt a)
@@ -374,7 +373,7 @@ void satcheck_minisat_simplifiert::set_frozen(literalt a)
374373
}
375374
catch(const Minisat::OutOfMemoryException &)
376375
{
377-
message.error() << "SAT checker ran out of memory" << messaget::eom;
376+
log.error() << "SAT checker ran out of memory" << messaget::eom;
378377
status = statust::ERROR;
379378
throw std::bad_alloc();
380379
}

0 commit comments

Comments
 (0)