Skip to content

Commit a3dc29d

Browse files
tautschnigtautschnig
authored
Merge pull request #7544 from tautschnig/features/refinement-sat-solver
Honour --sat-solver with refinement
2 parents 76593f8 + f1be42c commit a3dc29d

File tree

2 files changed

+64
-97
lines changed

2 files changed

+64
-97
lines changed

‎src/goto-checker/solver_factory.cpp‎

Lines changed: 64 additions & 92 deletions
Original file line numberDiff line numberDiff line change
@@ -87,12 +87,6 @@ solver_factoryt::solvert::stack_decision_procedure() const
8787
return *solver;
8888
}
8989

90-
propt &solver_factoryt::solvert::prop() const
91-
{
92-
PRECONDITION(prop_ptr != nullptr);
93-
return *prop_ptr;
94-
}
95-
9690
void solver_factoryt::set_decision_procedure_time_limit(
9791
decision_proceduret &decision_procedure)
9892
{
@@ -188,6 +182,17 @@ smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const
188182
return s;
189183
}
190184

185+
/// Emit a warning for non-existent solver \p solver via \p message_handler.
186+
static void emit_solver_warning(
187+
message_handlert &message_handler,
188+
const std::string &solver)
189+
{
190+
messaget log(message_handler);
191+
log.warning() << "The specified solver, '" << solver
192+
<< "', is not available. "
193+
<< "The default solver will be used instead." << messaget::eom;
194+
}
195+
191196
template <typename SatcheckT>
192197
static std::unique_ptr<SatcheckT>
193198
make_satcheck_prop(message_handlert &message_handler, const optionst &options)
@@ -214,123 +219,107 @@ make_satcheck_prop(message_handlert &message_handler, const optionst &options)
214219
return satcheck;
215220
}
216221

217-
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
222+
static std::unique_ptr<propt>
223+
get_sat_solver(message_handlert &message_handler, const optionst &options)
218224
{
219-
auto solver = util_make_unique<solvert>();
220-
bool solver_set = false;
225+
const bool no_simplifier = options.get_bool_option("beautify") ||
226+
!options.get_bool_option("sat-preprocessor") ||
227+
options.get_bool_option("refine") ||
228+
options.get_bool_option("refine-strings");
229+
221230
if(options.is_set("sat-solver"))
222231
{
223232
const std::string &solver_option = options.get_option("sat-solver");
224233
if(solver_option == "zchaff")
225234
{
226235
#if defined SATCHECK_ZCHAFF
227-
solver->set_prop(
228-
make_satcheck_prop<satcheck_zchafft>(message_handler, options));
229-
solver_set = true;
236+
return make_satcheck_prop<satcheck_zchafft>(message_handler, options);
230237
#else
231-
emit_solver_warning("zchaff");
238+
emit_solver_warning(message_handler, "zchaff");
232239
#endif
233240
}
234241
else if(solver_option == "booleforce")
235242
{
236243
#if defined SATCHECK_BOOLERFORCE
237-
solver->set_prop(
238-
make_satcheck_prop<satcheck_booleforcet>(message_handler, options));
239-
solver_set = true;
244+
return make_satcheck_prop<satcheck_booleforcet>(message_handler, options);
240245
#else
241-
emit_solver_warning("booleforce");
246+
emit_solver_warning(message_handler, "booleforce");
242247
#endif
243248
}
244249
else if(solver_option == "minisat1")
245250
{
246251
#if defined SATCHECK_MINISAT1
247-
solver->set_prop(
248-
make_satcheck_prop<satcheck_minisat1t>(message_handler, options));
249-
solver_set = true;
252+
return make_satcheck_prop<satcheck_minisat1t>(message_handler, options);
250253
#else
251-
emit_solver_warning("minisat1");
254+
emit_solver_warning(message_handler, "minisat1");
252255
#endif
253256
}
254257
else if(solver_option == "minisat2")
255258
{
256259
#if defined SATCHECK_MINISAT2
257-
if(
258-
options.get_bool_option("beautify") ||
259-
!options.get_bool_option("sat-preprocessor")) // no simplifier
260+
if(no_simplifier)
260261
{
261262
// simplifier won't work with beautification
262-
solver->set_prop(make_satcheck_prop<satcheck_minisat_no_simplifiert>(
263-
message_handler, options));
263+
return make_satcheck_prop<satcheck_minisat_no_simplifiert>(
264+
message_handler, options);
264265
}
265266
else // with simplifier
266267
{
267-
solver->set_prop(make_satcheck_prop<satcheck_minisat_simplifiert>(
268-
message_handler, options));
268+
return make_satcheck_prop<satcheck_minisat_simplifiert>(
269+
message_handler, options);
269270
}
270-
solver_set = true;
271271
#else
272-
emit_solver_warning("minisat2");
272+
emit_solver_warning(message_handler, "minisat2");
273273
#endif
274274
}
275275
else if(solver_option == "ipasir")
276276
{
277277
#if defined SATCHECK_IPASIR
278-
solver->set_prop(
279-
make_satcheck_prop<satcheck_ipasirt>(message_handler, options));
280-
solver_set = true;
278+
return make_satcheck_prop<satcheck_ipasirt>(message_handler, options);
281279
#else
282-
emit_solver_warning("ipasir");
280+
emit_solver_warning(message_handler, "ipasir");
283281
#endif
284282
}
285283
else if(solver_option == "picosat")
286284
{
287285
#if defined SATCHECK_PICOSAT
288-
solver->set_prop(
289-
make_satcheck_prop<satcheck_picosatt>(message_handler, options));
290-
solver_set = true;
286+
return make_satcheck_prop<satcheck_picosatt>(message_handler, options);
291287
#else
292-
emit_solver_warning("picosat");
288+
emit_solver_warning(message_handler, "picosat");
293289
#endif
294290
}
295291
else if(solver_option == "lingeling")
296292
{
297293
#if defined SATCHECK_LINGELING
298-
solver->set_prop(
299-
make_satcheck_prop<satcheck_lingelingt>(message_handler, options));
300-
solver_set = true;
294+
return make_satcheck_prop<satcheck_lingelingt>(message_handler, options);
301295
#else
302-
emit_solver_warning("lingeling");
296+
emit_solver_warning(message_handler, "lingeling");
303297
#endif
304298
}
305299
else if(solver_option == "glucose")
306300
{
307301
#if defined SATCHECK_GLUCOSE
308-
if(
309-
options.get_bool_option("beautify") ||
310-
!options.get_bool_option("sat-preprocessor")) // no simplifier
302+
if(no_simplifier)
311303
{
312304
// simplifier won't work with beautification
313-
solver->set_prop(make_satcheck_prop<satcheck_glucose_no_simplifiert>(
314-
message_handler, options));
305+
return make_satcheck_prop<satcheck_glucose_no_simplifiert>(
306+
message_handler, options);
315307
}
316308
else // with simplifier
317309
{
318-
solver->set_prop(make_satcheck_prop<satcheck_glucose_simplifiert>(
319-
message_handler, options));
310+
return make_satcheck_prop<satcheck_glucose_simplifiert>(
311+
message_handler, options);
320312
}
321-
solver_set = true;
322313
#else
323-
emit_solver_warning("glucose");
314+
emit_solver_warning(message_handler, "glucose");
324315
#endif
325316
}
326317
else if(solver_option == "cadical")
327318
{
328319
#if defined SATCHECK_CADICAL
329-
solver->set_prop(
330-
make_satcheck_prop<satcheck_cadicalt>(message_handler, options));
331-
solver_set = true;
320+
return make_satcheck_prop<satcheck_cadicalt>(message_handler, options);
332321
#else
333-
emit_solver_warning("cadical");
322+
emit_solver_warning(message_handler, "cadical");
334323
#endif
335324
}
336325
else
@@ -341,45 +330,38 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
341330
exit(CPROVER_EXIT_USAGE_ERROR);
342331
}
343332
}
344-
if(!solver_set)
333+
334+
// default solver
335+
if(no_simplifier)
345336
{
346-
// default solver
347-
if(
348-
options.get_bool_option("beautify") ||
349-
!options.get_bool_option("sat-preprocessor")) // no simplifier
350-
{
351-
// simplifier won't work with beautification
352-
solver->set_prop(
353-
make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options));
354-
}
355-
else // with simplifier
356-
{
357-
solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
358-
}
337+
// simplifier won't work with beautification
338+
return make_satcheck_prop<satcheck_no_simplifiert>(
339+
message_handler, options);
359340
}
341+
else // with simplifier
342+
{
343+
return make_satcheck_prop<satcheckt>(message_handler, options);
344+
}
345+
}
346+
347+
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
348+
{
349+
auto sat_solver = get_sat_solver(message_handler, options);
360350

361351
bool get_array_constraints =
362352
options.get_bool_option("show-array-constraints");
363353
auto bv_pointers = util_make_unique<bv_pointerst>(
364-
ns, solver->prop(), message_handler, get_array_constraints);
354+
ns, *sat_solver, message_handler, get_array_constraints);
365355

366356
if(options.get_option("arrays-uf") == "never")
367357
bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
368358
else if(options.get_option("arrays-uf") == "always")
369359
bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
370360

371361
set_decision_procedure_time_limit(*bv_pointers);
372-
solver->set_decision_procedure(std::move(bv_pointers));
373362

374-
return solver;
375-
}
376-
377-
void solver_factoryt::emit_solver_warning(const std::string &solver)
378-
{
379-
messaget log(message_handler);
380-
log.warning() << "The specified solver, '" << solver
381-
<< "', is not available. "
382-
<< "The default solver will be used instead." << messaget::eom;
363+
return util_make_unique<solvert>(
364+
std::move(bv_pointers), std::move(sat_solver));
383365
}
384366

385367
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
@@ -413,16 +395,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
413395

414396
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
415397
{
416-
std::unique_ptr<propt> prop = [this]() -> std::unique_ptr<propt> {
417-
// We offer the option to disable the SAT preprocessor
418-
if(options.get_bool_option("sat-preprocessor"))
419-
{
420-
no_beautification();
421-
return make_satcheck_prop<satcheckt>(message_handler, options);
422-
}
423-
return make_satcheck_prop<satcheck_no_simplifiert>(
424-
message_handler, options);
425-
}();
398+
std::unique_ptr<propt> prop = get_sat_solver(message_handler, options);
426399

427400
bv_refinementt::infot info;
428401
info.ns = &ns;
@@ -452,8 +425,7 @@ solver_factoryt::get_string_refinement()
452425
{
453426
string_refinementt::infot info;
454427
info.ns = &ns;
455-
auto prop =
456-
make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options);
428+
auto prop = get_sat_solver(message_handler, options);
457429
info.prop = prop.get();
458430
info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
459431
info.output_xml = output_xml_in_refinement;

‎src/goto-checker/solver_factory.h‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,6 @@ class solver_factoryt final
3838
class solvert final
3939
{
4040
public:
41-
solvert() = default;
4241
explicit solvert(std::unique_ptr<decision_proceduret> p);
4342
solvert(std::unique_ptr<decision_proceduret> p1, std::unique_ptr<propt> p2);
4443
solvert(
@@ -47,7 +46,6 @@ class solver_factoryt final
4746

4847
decision_proceduret &decision_procedure() const;
4948
stack_decision_proceduret &stack_decision_procedure() const;
50-
propt &prop() const;
5149

5250
void set_decision_procedure(std::unique_ptr<decision_proceduret> p);
5351
void set_prop(std::unique_ptr<propt> p);
@@ -89,9 +87,6 @@ class solver_factoryt final
8987
// consistency checks during solver creation
9088
void no_beautification();
9189
void no_incremental_check();
92-
93-
// emit a warning for non-existent solver
94-
void emit_solver_warning(const std::string &solver);
9590
};
9691

9792
/// Parse solver-related command-line parameters in \p cmdline and set

0 commit comments

Comments
 (0)