CBMC
Loading...
Searching...
No Matches
solver_factory.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Solver Factory
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "solver_factory.h"
13
14#include <util/cmdline.h>
16#include <util/exit_codes.h>
17#include <util/message.h>
18#include <util/options.h>
19#include <util/unicode.h>
20#include <util/version.h>
21
24#include <solvers/prop/prop.h>
33
34#include <iostream>
35
37 const optionst &_options,
38 const namespacet &_ns,
41 : options(_options),
42 ns(_ns),
43 message_handler(_message_handler),
44 output_xml_in_refinement(_output_xml_in_refinement)
45{
46}
47
48solver_factoryt::solvert::solvert(std::unique_ptr<stack_decision_proceduret> p)
49 : decision_procedure_ptr(std::move(p))
50{
51}
52
54 std::unique_ptr<stack_decision_proceduret> p1,
55 std::unique_ptr<propt> p2)
56 : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
57{
58}
59
61 std::unique_ptr<stack_decision_proceduret> p1,
62 std::unique_ptr<std::ofstream> p2)
63 : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
64{
65}
66
68 std::unique_ptr<boolbvt> p1,
69 std::unique_ptr<propt> p2)
70 : prop_ptr(std::move(p2)), decision_procedure_is_boolbvt_ptr(std::move(p1))
71{
72}
73
75{
77 (decision_procedure_ptr != nullptr) !=
78 (decision_procedure_is_boolbvt_ptr != nullptr));
79 if(decision_procedure_ptr)
80 return *decision_procedure_ptr;
81 else
82 return *decision_procedure_is_boolbvt_ptr;
83}
84
86{
87 PRECONDITION(decision_procedure_is_boolbvt_ptr != nullptr);
88 return *decision_procedure_is_boolbvt_ptr;
89}
90
92 solver_resource_limitst &decision_procedure)
93{
94 const int timeout_seconds =
95 options.get_signed_int_option("solver-time-limit");
96
97 if(timeout_seconds > 0)
98 decision_procedure.set_time_limit_seconds(timeout_seconds);
99}
100
101std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
102{
103 if(options.get_bool_option("dimacs"))
104 return get_dimacs();
105 if(options.is_set("external-sat-solver"))
106 return get_external_sat();
107 if(
108 options.get_bool_option("refine") &&
109 !options.get_bool_option("refine-strings"))
110 {
111 return get_bv_refinement();
112 }
113 else if(options.get_bool_option("refine-strings"))
114 return get_string_refinement();
115 const auto incremental_smt2_solver =
116 options.get_option("incremental-smt2-solver");
117 if(!incremental_smt2_solver.empty())
119 if(options.get_bool_option("smt2"))
121 return get_default();
122}
123
127{
128 // we shouldn't get here if this option isn't set
129 PRECONDITION(options.get_bool_option("smt2"));
130
132
133 if(options.get_bool_option("bitwuzla"))
135 else if(options.get_bool_option("boolector"))
137 else if(options.get_bool_option("cprover-smt2"))
139 else if(options.get_bool_option("mathsat"))
141 else if(options.get_bool_option("cvc3"))
143 else if(options.get_bool_option("cvc4"))
145 else if(options.get_bool_option("cvc5"))
147 else if(options.get_bool_option("yices"))
149 else if(options.get_bool_option("z3"))
151 else if(options.get_bool_option("generic"))
153
154 return s;
155}
156
160 const std::string &solver)
161{
163 log.warning() << "The specified solver, '" << solver
164 << "', is not available. "
165 << "The default solver will be used instead." << messaget::eom;
166}
167
168template <typename SatcheckT>
169static typename std::enable_if<
170 !std::is_base_of<hardness_collectort, SatcheckT>::value,
171 std::unique_ptr<SatcheckT>>::type
173{
174 auto satcheck = std::make_unique<SatcheckT>(message_handler);
175 if(options.is_set("write-solver-stats-to"))
176 {
178 log.warning()
179 << "Configured solver does not support --write-solver-stats-to. "
180 << "Solver stats will not be written." << messaget::eom;
181 }
182 return satcheck;
183}
184
185template <typename SatcheckT>
186static typename std::enable_if<
187 std::is_base_of<hardness_collectort, SatcheckT>::value,
188 std::unique_ptr<SatcheckT>>::type
190{
191 auto satcheck = std::make_unique<SatcheckT>(message_handler);
192 if(options.is_set("write-solver-stats-to"))
193 {
194 std::unique_ptr<solver_hardnesst> solver_hardness =
195 std::make_unique<solver_hardnesst>();
196 solver_hardness->set_outfile(options.get_option("write-solver-stats-to"));
197 satcheck->solver_hardness = std::move(solver_hardness);
198 }
199 return satcheck;
200}
201
202static std::unique_ptr<propt>
204{
205 const bool no_simplifier = options.get_bool_option("beautify") ||
206 !options.get_bool_option("sat-preprocessor") ||
207 options.get_bool_option("refine-strings");
208
209 if(options.is_set("sat-solver"))
210 {
211 const std::string &solver_option = options.get_option("sat-solver");
212 if(solver_option == "zchaff")
213 {
214#if defined SATCHECK_ZCHAFF
216#else
218#endif
219 }
220 else if(solver_option == "booleforce")
221 {
222#if defined SATCHECK_BOOLERFORCE
224#else
226#endif
227 }
228 else if(solver_option == "minisat1")
229 {
230#if defined SATCHECK_MINISAT1
232#else
234#endif
235 }
236 else if(solver_option == "minisat2")
237 {
238#if defined SATCHECK_MINISAT2
239 if(no_simplifier)
240 {
241 // simplifier won't work with beautification
244 }
245 else // with simplifier
246 {
249 }
250#else
252#endif
253 }
254 else if(solver_option == "ipasir")
255 {
256#if defined SATCHECK_IPASIR
258#else
260#endif
261 }
262 else if(solver_option == "picosat")
263 {
264#if defined SATCHECK_PICOSAT
266#else
268#endif
269 }
270 else if(solver_option == "lingeling")
271 {
272#if defined SATCHECK_LINGELING
274#else
276#endif
277 }
278 else if(solver_option == "glucose")
279 {
280#if defined SATCHECK_GLUCOSE
281 if(no_simplifier)
282 {
283 // simplifier won't work with beautification
286 }
287 else // with simplifier
288 {
291 }
292#else
294#endif
295 }
296 else if(solver_option == "cadical")
297 {
298#if defined SATCHECK_CADICAL
301#else
303#endif
304 }
305 else
306 {
308 log.error() << "unknown solver '" << solver_option << "'"
309 << messaget::eom;
311 }
312 }
313
314 // default solver
315 if(no_simplifier)
316 {
317 // simplifier won't work with beautification
320 }
321 else // with simplifier
322 {
324 }
325}
326
327std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
328{
330
331 bool get_array_constraints =
332 options.get_bool_option("show-array-constraints");
333 auto bv_pointers = std::make_unique<bv_pointerst>(
334 ns, *sat_solver, message_handler, get_array_constraints);
335
336 if(options.get_option("arrays-uf") == "never")
338 else if(options.get_option("arrays-uf") == "always")
340
342
343 std::unique_ptr<boolbvt> boolbv = std::move(bv_pointers);
344 return std::make_unique<solvert>(std::move(boolbv), std::move(sat_solver));
345}
346
347std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
348{
351
352 auto prop = std::make_unique<dimacs_cnft>(message_handler);
353
354 std::string filename = options.get_option("outfile");
355
356 std::unique_ptr<boolbvt> bv_dimacs =
357 std::make_unique<bv_dimacst>(ns, *prop, message_handler, filename);
358
359 return std::make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
360}
361
362std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
363{
366
367 std::string external_sat_solver = options.get_option("external-sat-solver");
368 auto prop =
369 std::make_unique<external_satt>(message_handler, external_sat_solver);
370
371 std::unique_ptr<boolbvt> bv_pointers =
372 std::make_unique<bv_pointerst>(ns, *prop, message_handler);
373
374 return std::make_unique<solvert>(std::move(bv_pointers), std::move(prop));
375}
376
377std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
378{
379 std::unique_ptr<propt> prop = get_sat_solver(message_handler, options);
380
382 info.ns = &ns;
383 info.prop = prop.get();
385
386 // we allow setting some parameters
387 if(options.get_bool_option("max-node-refinement"))
388 info.max_node_refinement =
389 options.get_unsigned_int_option("max-node-refinement");
390
391 info.refine_arrays = options.get_bool_option("refine-arrays");
392 info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
394
395 std::unique_ptr<boolbvt> decision_procedure =
396 std::make_unique<bv_refinementt>(info);
397 set_decision_procedure_time_limit(*decision_procedure);
398 return std::make_unique<solvert>(
399 std::move(decision_procedure), std::move(prop));
400}
401
405std::unique_ptr<solver_factoryt::solvert>
407{
409 info.ns = &ns;
411 info.prop = prop.get();
412 info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
414 if(options.get_bool_option("max-node-refinement"))
415 info.max_node_refinement =
416 options.get_unsigned_int_option("max-node-refinement");
417 info.refine_arrays = options.get_bool_option("refine-arrays");
418 info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
420
421 std::unique_ptr<boolbvt> decision_procedure =
422 std::make_unique<string_refinementt>(info);
423 set_decision_procedure_time_limit(*decision_procedure);
424 return std::make_unique<solvert>(
425 std::move(decision_procedure), std::move(prop));
426}
427
428std::unique_ptr<std::ofstream> open_outfile_and_check(
429 const std::string &filename,
431 const std::string &arg_name)
432{
433 if(filename.empty())
434 return nullptr;
435
436 auto out = std::make_unique<std::ofstream>(widen_if_needed(filename));
437
438 if(!*out)
439 {
441 "failed to open file: " + filename, arg_name);
442 }
443
445 log.status() << "Outputting SMTLib formula to file: " << filename
446 << messaget::eom;
447 return out;
448}
449
450std::unique_ptr<solver_factoryt::solvert>
452{
454
455 const std::string outfile_arg = options.get_option("outfile");
456 const std::string dump_smt_formula = options.get_option("dump-smt-formula");
457
458 if(!outfile_arg.empty() && !dump_smt_formula.empty())
459 {
461 "Argument --outfile is incompatible with --dump-smt-formula. ",
462 "--outfile");
463 }
464
465 std::unique_ptr<smt_base_solver_processt> solver_process = nullptr;
466
467 if(!outfile_arg.empty())
468 {
469 bool on_std_out = outfile_arg == "-";
470 std::unique_ptr<std::ostream> outfile =
472 ? nullptr
474 solver_process = std::make_unique<smt_incremental_dry_run_solvert>(
475 message_handler, on_std_out ? std::cout : *outfile, std::move(outfile));
476 }
477 else
478 {
479 const auto out_filename = options.get_option("dump-smt-formula");
480
481 // If no out_filename is provided `open_outfile_and_check` will return
482 // `nullptr`, and the solver will work normally without any logging.
483 solver_process = std::make_unique<smt_piped_solver_processt>(
484 std::move(solver_command),
487 out_filename, message_handler, "--dump-smt-formula"));
488 }
489
490 return std::make_unique<solvert>(
491 std::make_unique<smt2_incremental_decision_proceduret>(
492 ns, std::move(solver_process), message_handler));
493}
494
495std::unique_ptr<solver_factoryt::solvert>
497{
499
500 const std::string &filename = options.get_option("outfile");
501
502 if(filename.empty())
503 {
505 {
507 "required filename not provided",
508 "--outfile",
509 "provide a filename with --outfile");
510 }
511
512 auto smt2_dec = std::make_unique<smt2_dect>(
513 ns,
514 "cbmc",
515 std::string("Generated by CBMC ") + CBMC_VERSION,
516 "QF_AUFBV",
517 solver,
519
520 if(options.get_bool_option("fpa"))
521 smt2_dec->use_FPA_theory = true;
522
523 return std::make_unique<solvert>(std::move(smt2_dec));
524 }
525 else if(filename == "-")
526 {
527 auto smt2_conv = std::make_unique<smt2_convt>(
528 ns,
529 "cbmc",
530 std::string("Generated by CBMC ") + CBMC_VERSION,
531 "QF_AUFBV",
532 solver,
533 std::cout);
534
535 if(options.get_bool_option("fpa"))
536 smt2_conv->use_FPA_theory = true;
537
538 return std::make_unique<solvert>(std::move(smt2_conv));
539 }
540 else
541 {
542 auto out = open_outfile_and_check(filename, message_handler, "--outfile");
543
544 auto smt2_conv = std::make_unique<smt2_convt>(
545 ns,
546 "cbmc",
547 std::string("Generated by CBMC ") + CBMC_VERSION,
548 "QF_AUFBV",
549 solver,
550 *out);
551
552 if(options.get_bool_option("fpa"))
553 smt2_conv->use_FPA_theory = true;
554
555 return std::make_unique<solvert>(std::move(smt2_conv), std::move(out));
556 }
557}
558
560{
561 if(options.get_bool_option("beautify"))
562 {
564 "the chosen solver does not support beautification", "--beautify");
565 }
566}
567
569{
570 const bool all_properties = options.get_bool_option("all-properties");
571 const bool cover = options.is_set("cover");
572 const bool incremental_loop = options.is_set("incremental-loop");
573
575 {
577 "the chosen solver does not support incremental solving",
578 "--all_properties");
579 }
580 else if(cover)
581 {
583 "the chosen solver does not support incremental solving", "--cover");
584 }
585 else if(incremental_loop)
586 {
588 "the chosen solver does not support incremental solving",
589 "--incremental-loop");
590 }
591}
592
593static void parse_sat_options(const cmdlinet &cmdline, optionst &options)
594{
595 if(cmdline.isset("external-sat-solver"))
596 {
597 options.set_option(
598 "external-sat-solver", cmdline.get_value("external-sat-solver"));
599 }
600
601 options.set_option("sat-preprocessor", !cmdline.isset("no-sat-preprocessor"));
602
603 if(cmdline.isset("dimacs"))
604 options.set_option("dimacs", true);
605
606 if(cmdline.isset("sat-solver"))
607 options.set_option("sat-solver", cmdline.get_value("sat-solver"));
608}
609
610static void parse_smt2_options(const cmdlinet &cmdline, optionst &options)
611{
612 if(cmdline.isset("smt2"))
613 options.set_option("smt2", true);
614
615 if(cmdline.isset("fpa"))
616 options.set_option("fpa", true);
617
618 bool solver_set = false;
619
620 if(cmdline.isset("bitwuzla"))
621 {
622 options.set_option("bitwuzla", true), solver_set = true;
623 options.set_option("smt2", true);
624 }
625
626 if(cmdline.isset("boolector"))
627 {
628 options.set_option("boolector", true), solver_set = true;
629 options.set_option("smt2", true);
630 }
631
632 if(cmdline.isset("cprover-smt2"))
633 {
634 options.set_option("cprover-smt2", true), solver_set = true;
635 options.set_option("smt2", true);
636 }
637
638 if(cmdline.isset("mathsat"))
639 {
640 options.set_option("mathsat", true), solver_set = true;
641 options.set_option("smt2", true);
642 }
643
644 if(cmdline.isset("cvc4"))
645 {
646 options.set_option("cvc4", true), solver_set = true;
647 options.set_option("smt2", true);
648 }
649
650 if(cmdline.isset("cvc5"))
651 {
652 options.set_option("cvc5", true), solver_set = true;
653 options.set_option("smt2", true);
654 }
655
656 if(cmdline.isset("incremental-smt2-solver"))
657 {
658 options.set_option(
659 "incremental-smt2-solver", cmdline.get_value("incremental-smt2-solver")),
660 solver_set = true;
661 }
662
663 if(cmdline.isset("yices"))
664 {
665 options.set_option("yices", true), solver_set = true;
666 options.set_option("smt2", true);
667 }
668
669 if(cmdline.isset("z3"))
670 {
671 options.set_option("z3", true), solver_set = true;
672 options.set_option("smt2", true);
673 }
674
675 if(cmdline.isset("smt2") && !solver_set)
676 {
677 if(cmdline.isset("outfile"))
678 {
679 // outfile and no solver should give standard compliant SMT-LIB
680 options.set_option("generic", true);
681 }
682 else
683 {
684 // the default smt2 solver
685 options.set_option("z3", true);
686 }
687 }
688}
689
691{
692 parse_sat_options(cmdline, options);
693 parse_smt2_options(cmdline, options);
694
695 if(cmdline.isset("outfile"))
696 options.set_option("outfile", cmdline.get_value("outfile"));
697
698 if(cmdline.isset("dump-smt-formula"))
699 options.set_option(
700 "dump-smt-formula", cmdline.get_value("dump-smt-formula"));
701
702 if(cmdline.isset("write-solver-stats-to"))
703 {
704 options.set_option(
705 "write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
706 }
707
708 if(cmdline.isset("beautify"))
709 options.set_option("beautify", true);
710
711 if(cmdline.isset("refine-arrays"))
712 {
713 options.set_option("refine", true);
714 options.set_option("refine-arrays", true);
715 }
716
717 if(cmdline.isset("refine-arithmetic"))
718 {
719 options.set_option("refine", true);
720 options.set_option("refine-arithmetic", true);
721 }
722
723 if(cmdline.isset("refine"))
724 {
725 options.set_option("refine", true);
726 options.set_option("refine-arrays", true);
727 options.set_option("refine-arithmetic", true);
728 }
729
730 if(cmdline.isset("max-node-refinement"))
731 {
732 options.set_option(
733 "max-node-refinement", cmdline.get_value("max-node-refinement"));
734 }
735}
Writing DIMACS Files.
Abstraction Refinement Loop.
message_handlert & message_handler
Definition ai.h:521
virtual xmlt output_xml(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
Definition ai.cpp:136
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::string get_value(char option) const
Definition cmdline.cpp:48
virtual bool isset(char option) const
Definition cmdline.cpp:30
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
boolbvt & boolbv_decision_procedure() const
solvert(std::unique_ptr< stack_decision_proceduret > p)
stack_decision_proceduret & decision_procedure() const
message_handlert & message_handler
const optionst & options
const namespacet & ns
std::unique_ptr< solvert > get_external_sat()
std::unique_ptr< solvert > get_default()
solver_factoryt(const optionst &_options, const namespacet &_ns, message_handlert &_message_handler, bool _output_xml_in_refinement)
Note: The solver returned will hold a reference to the namespace ns.
void set_decision_procedure_time_limit(solver_resource_limitst &decision_procedure)
Sets the timeout of decision_procedure if the solver-time-limit option has a positive value (in secon...
std::unique_ptr< solvert > get_dimacs()
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
const bool output_xml_in_refinement
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
std::unique_ptr< solvert > get_incremental_smt2(std::string solver_command)
std::unique_ptr< solvert > get_bv_refinement()
virtual void set_time_limit_seconds(uint32_t)=0
Set the limit for the solver to time out in seconds.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition exit_codes.h:33
Allows calling an external SAT solver to allow faster integration of newer SAT solvers.
double log(double x)
Definition math.c:2449
STL namespace.
Options.
Decision procedure with incremental SMT2 solving.
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
Definition solver.cpp:44
static std::enable_if<!std::is_base_of< hardness_collectort, SatcheckT >::value, std::unique_ptr< SatcheckT > >::type make_satcheck_prop(message_handlert &message_handler, const optionst &options)
static void parse_sat_options(const cmdlinet &cmdline, optionst &options)
static void parse_smt2_options(const cmdlinet &cmdline, optionst &options)
std::unique_ptr< std::ofstream > open_outfile_and_check(const std::string &filename, message_handlert &message_handler, const std::string &arg_name)
static std::unique_ptr< propt > get_sat_solver(message_handlert &message_handler, const optionst &options)
static void emit_solver_warning(message_handlert &message_handler, const std::string &solver)
Emit a warning for non-existent solver solver via message_handler.
Solver Factory.
void parse_solver_options(const cmdlinet &cmdline, optionst &options)
Parse solver-related command-line parameters in cmdline and set corresponding values in options.
Solver capability to set resource limits.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
void exit(int status)
Definition stdlib.c:102
String support via creating string constraints and progressively instantiating the universal constrai...
#define DEFAULT_MAX_NB_REFINEMENT
string_refinementt constructor arguments
#define widen_if_needed(s)
Definition unicode.h:28
const char * CBMC_VERSION