cprover
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/make_unique.h>
18#include <util/message.h>
19#include <util/options.h>
20#include <util/unicode.h>
21#include <util/version.h>
22
25#include <solvers/prop/prop.h>
35
36#include <iostream>
37
39 const optionst &_options,
40 const namespacet &_ns,
43 : options(_options),
44 ns(_ns),
45 message_handler(_message_handler),
46 output_xml_in_refinement(_output_xml_in_refinement)
47{
48}
49
50solver_factoryt::solvert::solvert(std::unique_ptr<decision_proceduret> p)
51 : decision_procedure_ptr(std::move(p))
52{
53}
54
56 std::unique_ptr<decision_proceduret> p1,
57 std::unique_ptr<propt> p2)
58 : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
59{
60}
61
63 std::unique_ptr<decision_proceduret> p1,
64 std::unique_ptr<std::ofstream> p2)
65 : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
66{
67}
68
70{
71 PRECONDITION(decision_procedure_ptr != nullptr);
72 return *decision_procedure_ptr;
73}
74
77{
78 PRECONDITION(decision_procedure_ptr != nullptr);
80 dynamic_cast<stack_decision_proceduret *>(&*decision_procedure_ptr);
81 INVARIANT(solver != nullptr, "stack decision procedure required");
82 return *solver;
83}
84
86 decision_proceduret &decision_procedure)
87{
88 const int timeout_seconds =
89 options.get_signed_int_option("solver-time-limit");
90
91 if(timeout_seconds > 0)
92 {
94 dynamic_cast<solver_resource_limitst *>(&decision_procedure);
95 if(solver == nullptr)
96 {
98 log.warning() << "cannot set solver time limit on "
99 << decision_procedure.decision_procedure_text()
100 << messaget::eom;
101 return;
102 }
103
104 solver->set_time_limit_seconds(timeout_seconds);
105 }
106}
107
109 std::unique_ptr<decision_proceduret> p)
110{
111 decision_procedure_ptr = std::move(p);
112}
113
114void solver_factoryt::solvert::set_prop(std::unique_ptr<propt> p)
115{
116 prop_ptr = std::move(p);
117}
118
119void solver_factoryt::solvert::set_ofstream(std::unique_ptr<std::ofstream> p)
120{
121 ofstream_ptr = std::move(p);
122}
123
124std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
125{
126 if(options.get_bool_option("dimacs"))
127 return get_dimacs();
128 if(options.is_set("external-sat-solver"))
129 return get_external_sat();
130 if(
131 options.get_bool_option("refine") &&
132 !options.get_bool_option("refine-strings"))
133 {
134 return get_bv_refinement();
135 }
136 else if(options.get_bool_option("refine-strings"))
137 return get_string_refinement();
138 const auto incremental_smt2_solver =
139 options.get_option("incremental-smt2-solver");
140 if(!incremental_smt2_solver.empty())
142 if(options.get_bool_option("smt2"))
144 return get_default();
145}
146
150{
151 // we shouldn't get here if this option isn't set
152 PRECONDITION(options.get_bool_option("smt2"));
153
155
156 if(options.get_bool_option("bitwuzla"))
158 else if(options.get_bool_option("boolector"))
160 else if(options.get_bool_option("cprover-smt2"))
162 else if(options.get_bool_option("mathsat"))
164 else if(options.get_bool_option("cvc3"))
166 else if(options.get_bool_option("cvc4"))
168 else if(options.get_bool_option("cvc5"))
170 else if(options.get_bool_option("yices"))
172 else if(options.get_bool_option("z3"))
174 else if(options.get_bool_option("generic"))
176
177 return s;
178}
179
183 const std::string &solver)
184{
186 log.warning() << "The specified solver, '" << solver
187 << "', is not available. "
188 << "The default solver will be used instead." << messaget::eom;
189}
190
191template <typename SatcheckT>
192static std::unique_ptr<SatcheckT>
194{
196 if(options.is_set("write-solver-stats-to"))
197 {
198 if(
199 auto hardness_collector = dynamic_cast<hardness_collectort *>(&*satcheck))
200 {
201 std::unique_ptr<solver_hardnesst> solver_hardness =
203 solver_hardness->set_outfile(options.get_option("write-solver-stats-to"));
204 hardness_collector->solver_hardness = std::move(solver_hardness);
205 }
206 else
207 {
209 log.warning()
210 << "Configured solver does not support --write-solver-stats-to. "
211 << "Solver stats will not be written." << messaget::eom;
212 }
213 }
214 return satcheck;
215}
216
217static std::unique_ptr<propt>
219{
220 const bool no_simplifier = options.get_bool_option("beautify") ||
221 !options.get_bool_option("sat-preprocessor") ||
222 options.get_bool_option("refine-arithmetic") ||
223 options.get_bool_option("refine-strings");
224
225 if(options.is_set("sat-solver"))
226 {
227 const std::string &solver_option = options.get_option("sat-solver");
228 if(solver_option == "zchaff")
229 {
230#if defined SATCHECK_ZCHAFF
232#else
234#endif
235 }
236 else if(solver_option == "booleforce")
237 {
238#if defined SATCHECK_BOOLERFORCE
240#else
242#endif
243 }
244 else if(solver_option == "minisat1")
245 {
246#if defined SATCHECK_MINISAT1
248#else
250#endif
251 }
252 else if(solver_option == "minisat2")
253 {
254#if defined SATCHECK_MINISAT2
255 if(no_simplifier)
256 {
257 // simplifier won't work with beautification
260 }
261 else // with simplifier
262 {
265 }
266#else
268#endif
269 }
270 else if(solver_option == "ipasir")
271 {
272#if defined SATCHECK_IPASIR
274#else
276#endif
277 }
278 else if(solver_option == "picosat")
279 {
280#if defined SATCHECK_PICOSAT
282#else
284#endif
285 }
286 else if(solver_option == "lingeling")
287 {
288#if defined SATCHECK_LINGELING
290#else
292#endif
293 }
294 else if(solver_option == "glucose")
295 {
296#if defined SATCHECK_GLUCOSE
297 if(no_simplifier)
298 {
299 // simplifier won't work with beautification
302 }
303 else // with simplifier
304 {
307 }
308#else
310#endif
311 }
312 else if(solver_option == "cadical")
313 {
314#if defined SATCHECK_CADICAL
316#else
318#endif
319 }
320 else
321 {
323 log.error() << "unknown solver '" << solver_option << "'"
324 << messaget::eom;
326 }
327 }
328
329 // default solver
330 if(no_simplifier)
331 {
332 // simplifier won't work with beautification
335 }
336 else // with simplifier
337 {
339 }
340}
341
342std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
343{
345
346 bool get_array_constraints =
347 options.get_bool_option("show-array-constraints");
349 ns, *sat_solver, message_handler, get_array_constraints);
350
351 if(options.get_option("arrays-uf") == "never")
353 else if(options.get_option("arrays-uf") == "always")
355
357
359 std::move(bv_pointers), std::move(sat_solver));
360}
361
362std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
363{
366
368
369 std::string filename = options.get_option("outfile");
370
371 auto bv_dimacs =
373
374 return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
375}
376
377std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
378{
381
382 std::string external_sat_solver = options.get_option("external-sat-solver");
383 auto prop =
385
387
388 return util_make_unique<solvert>(std::move(bv_pointers), std::move(prop));
389}
390
391std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
392{
393 std::unique_ptr<propt> prop = get_sat_solver(message_handler, options);
394
396 info.ns = &ns;
397 info.prop = prop.get();
399
400 // we allow setting some parameters
401 if(options.get_bool_option("max-node-refinement"))
402 info.max_node_refinement =
403 options.get_unsigned_int_option("max-node-refinement");
404
405 info.refine_arrays = options.get_bool_option("refine-arrays");
406 info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
408
409 auto decision_procedure = util_make_unique<bv_refinementt>(info);
410 set_decision_procedure_time_limit(*decision_procedure);
412 std::move(decision_procedure), std::move(prop));
413}
414
418std::unique_ptr<solver_factoryt::solvert>
420{
422 info.ns = &ns;
424 info.prop = prop.get();
425 info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
427 if(options.get_bool_option("max-node-refinement"))
428 info.max_node_refinement =
429 options.get_unsigned_int_option("max-node-refinement");
430 info.refine_arrays = options.get_bool_option("refine-arrays");
431 info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
433
434 auto decision_procedure = util_make_unique<string_refinementt>(info);
435 set_decision_procedure_time_limit(*decision_procedure);
437 std::move(decision_procedure), std::move(prop));
438}
439
440std::unique_ptr<std::ofstream> open_outfile_and_check(
441 const std::string &filename,
443 const std::string &arg_name)
444{
445 if(filename.empty())
446 return nullptr;
447
449
450 if(!*out)
451 {
453 "failed to open file: " + filename, arg_name);
454 }
455
457 log.status() << "Outputting SMTLib formula to file: " << filename
458 << messaget::eom;
459 return out;
460}
461
462std::unique_ptr<solver_factoryt::solvert>
464{
466
467 const std::string outfile_arg = options.get_option("outfile");
468 const std::string dump_smt_formula = options.get_option("dump-smt-formula");
469
470 if(!outfile_arg.empty() && !dump_smt_formula.empty())
471 {
473 "Argument --outfile is incompatible with --dump-smt-formula. ",
474 "--outfile");
475 }
476
477 std::unique_ptr<smt_base_solver_processt> solver_process = nullptr;
478
479 if(!outfile_arg.empty())
480 {
481 bool on_std_out = outfile_arg == "-";
482 std::unique_ptr<std::ostream> outfile =
484 ? nullptr
487 message_handler, on_std_out ? std::cout : *outfile, std::move(outfile));
488 }
489 else
490 {
491 const auto out_filename = options.get_option("dump-smt-formula");
492
493 // If no out_filename is provided `open_outfile_and_check` will return
494 // `nullptr`, and the solver will work normally without any logging.
496 std::move(solver_command),
499 out_filename, message_handler, "--dump-smt-formula"));
500 }
501
504 ns, std::move(solver_process), message_handler));
505}
506
507std::unique_ptr<solver_factoryt::solvert>
509{
511
512 const std::string &filename = options.get_option("outfile");
513
514 if(filename.empty())
515 {
517 {
519 "required filename not provided",
520 "--outfile",
521 "provide a filename with --outfile");
522 }
523
525 ns,
526 "cbmc",
527 std::string("Generated by CBMC ") + CBMC_VERSION,
528 "QF_AUFBV",
529 solver,
531
532 if(options.get_bool_option("fpa"))
533 smt2_dec->use_FPA_theory = true;
534
536 return util_make_unique<solvert>(std::move(smt2_dec));
537 }
538 else if(filename == "-")
539 {
540 auto smt2_conv = util_make_unique<smt2_convt>(
541 ns,
542 "cbmc",
543 std::string("Generated by CBMC ") + CBMC_VERSION,
544 "QF_AUFBV",
545 solver,
546 std::cout);
547
548 if(options.get_bool_option("fpa"))
549 smt2_conv->use_FPA_theory = true;
550
552 return util_make_unique<solvert>(std::move(smt2_conv));
553 }
554 else
555 {
556 auto out = open_outfile_and_check(filename, message_handler, "--outfile");
557
558 auto smt2_conv = util_make_unique<smt2_convt>(
559 ns,
560 "cbmc",
561 std::string("Generated by CBMC ") + CBMC_VERSION,
562 "QF_AUFBV",
563 solver,
564 *out);
565
566 if(options.get_bool_option("fpa"))
567 smt2_conv->use_FPA_theory = true;
568
570 return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
571 }
572}
573
575{
576 if(options.get_bool_option("beautify"))
577 {
579 "the chosen solver does not support beautification", "--beautify");
580 }
581}
582
584{
585 const bool all_properties = options.get_bool_option("all-properties");
586 const bool cover = options.is_set("cover");
587 const bool incremental_loop = options.is_set("incremental-loop");
588
590 {
592 "the chosen solver does not support incremental solving",
593 "--all_properties");
594 }
595 else if(cover)
596 {
598 "the chosen solver does not support incremental solving", "--cover");
599 }
600 else if(incremental_loop)
601 {
603 "the chosen solver does not support incremental solving",
604 "--incremental-loop");
605 }
606}
607
608static void parse_sat_options(const cmdlinet &cmdline, optionst &options)
609{
610 if(cmdline.isset("external-sat-solver"))
611 {
612 options.set_option(
613 "external-sat-solver", cmdline.get_value("external-sat-solver"));
614 }
615
616 options.set_option("sat-preprocessor", !cmdline.isset("no-sat-preprocessor"));
617
618 if(cmdline.isset("dimacs"))
619 options.set_option("dimacs", true);
620
621 if(cmdline.isset("sat-solver"))
622 options.set_option("sat-solver", cmdline.get_value("sat-solver"));
623}
624
625static void parse_smt2_options(const cmdlinet &cmdline, optionst &options)
626{
627 if(cmdline.isset("smt2"))
628 options.set_option("smt2", true);
629
630 if(cmdline.isset("fpa"))
631 options.set_option("fpa", true);
632
633 bool solver_set = false;
634
635 if(cmdline.isset("bitwuzla"))
636 {
637 options.set_option("bitwuzla", true), solver_set = true;
638 options.set_option("smt2", true);
639 }
640
641 if(cmdline.isset("boolector"))
642 {
643 options.set_option("boolector", true), solver_set = true;
644 options.set_option("smt2", true);
645 }
646
647 if(cmdline.isset("cprover-smt2"))
648 {
649 options.set_option("cprover-smt2", true), solver_set = true;
650 options.set_option("smt2", true);
651 }
652
653 if(cmdline.isset("mathsat"))
654 {
655 options.set_option("mathsat", true), solver_set = true;
656 options.set_option("smt2", true);
657 }
658
659 if(cmdline.isset("cvc4"))
660 {
661 options.set_option("cvc4", true), solver_set = true;
662 options.set_option("smt2", true);
663 }
664
665 if(cmdline.isset("cvc5"))
666 {
667 options.set_option("cvc5", true), solver_set = true;
668 options.set_option("smt2", true);
669 }
670
671 if(cmdline.isset("incremental-smt2-solver"))
672 {
673 options.set_option(
674 "incremental-smt2-solver", cmdline.get_value("incremental-smt2-solver")),
675 solver_set = true;
676 }
677
678 if(cmdline.isset("yices"))
679 {
680 options.set_option("yices", true), solver_set = true;
681 options.set_option("smt2", true);
682 }
683
684 if(cmdline.isset("z3"))
685 {
686 options.set_option("z3", true), solver_set = true;
687 options.set_option("smt2", true);
688 }
689
690 if(cmdline.isset("smt2") && !solver_set)
691 {
692 if(cmdline.isset("outfile"))
693 {
694 // outfile and no solver should give standard compliant SMT-LIB
695 options.set_option("generic", true);
696 }
697 else
698 {
699 // the default smt2 solver
700 options.set_option("z3", true);
701 }
702 }
703}
704
706{
707 parse_sat_options(cmdline, options);
708 parse_smt2_options(cmdline, options);
709
710 if(cmdline.isset("outfile"))
711 options.set_option("outfile", cmdline.get_value("outfile"));
712
713 if(cmdline.isset("dump-smt-formula"))
714 options.set_option(
715 "dump-smt-formula", cmdline.get_value("dump-smt-formula"));
716
717 if(cmdline.isset("write-solver-stats-to"))
718 {
719 options.set_option(
720 "write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
721 }
722
723 if(cmdline.isset("beautify"))
724 options.set_option("beautify", true);
725
726 if(cmdline.isset("refine-arrays"))
727 {
728 options.set_option("refine", true);
729 options.set_option("refine-arrays", true);
730 }
731
732 if(cmdline.isset("refine-arithmetic"))
733 {
734 options.set_option("refine", true);
735 options.set_option("refine-arithmetic", true);
736 }
737
738 if(cmdline.isset("refine"))
739 {
740 options.set_option("refine", true);
741 options.set_option("refine-arrays", true);
742 options.set_option("refine-arithmetic", true);
743 }
744
745 if(cmdline.isset("max-node-refinement"))
746 {
747 options.set_option(
748 "max-node-refinement", cmdline.get_value("max-node-refinement"));
749 }
750}
Writing DIMACS Files.
Abstraction Refinement Loop.
message_handlert & message_handler
Definition ai.h:522
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:563
std::string get_value(char option) const
Definition cmdline.cpp:48
virtual bool isset(char option) const
Definition cmdline.cpp:30
virtual std::string decision_procedure_text() const =0
Return a textual description of the decision procedure.
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:155
mstreamt & error() const
Definition message.h:399
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
solvert(std::unique_ptr< decision_proceduret > p)
void set_decision_procedure(std::unique_ptr< decision_proceduret > p)
decision_proceduret & decision_procedure() const
stack_decision_proceduret & stack_decision_procedure() const
void set_ofstream(std::unique_ptr< std::ofstream > p)
void set_prop(std::unique_ptr< propt > p)
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.
std::unique_ptr< solvert > get_dimacs()
void set_decision_procedure_time_limit(decision_proceduret &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_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()
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.
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 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.
static std::unique_ptr< SatcheckT > make_satcheck_prop(message_handlert &message_handler, const optionst &options)
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Decision procedure with incremental solving with contexts and assumptions.
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