40 bool _output_xml_in_refinement)
54 std::unique_ptr<stack_decision_proceduret> p1,
55 std::unique_ptr<propt> p2)
61 std::unique_ptr<stack_decision_proceduret> p1,
62 std::unique_ptr<std::ofstream> p2)
68 std::unique_ptr<boolbvt> p1,
69 std::unique_ptr<propt> p2)
94 const int timeout_seconds =
95 options.get_signed_int_option(
"solver-time-limit");
97 if(timeout_seconds > 0)
103 if(
options.get_bool_option(
"dimacs"))
105 if(
options.is_set(
"external-sat-solver"))
108 options.get_bool_option(
"refine") &&
109 !
options.get_bool_option(
"refine-strings"))
113 else if(
options.get_bool_option(
"refine-strings"))
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"))
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"))
160 const std::string &
solver)
164 <<
"', is not available. "
165 <<
"The default solver will be used instead." <<
messaget::eom;
168template <
typename SatcheckT>
169static typename std::enable_if<
170 !std::is_base_of<hardness_collectort, SatcheckT>::value,
171 std::unique_ptr<SatcheckT>>::type
179 <<
"Configured solver does not support --write-solver-stats-to. "
185template <
typename SatcheckT>
186static typename std::enable_if<
187 std::is_base_of<hardness_collectort, SatcheckT>::value,
188 std::unique_ptr<SatcheckT>>::type
194 std::unique_ptr<solver_hardnesst> solver_hardness =
195 std::make_unique<solver_hardnesst>();
197 satcheck->solver_hardness = std::move(solver_hardness);
202static std::unique_ptr<propt>
212 if(solver_option ==
"zchaff")
214#if defined SATCHECK_ZCHAFF
220 else if(solver_option ==
"booleforce")
222#if defined SATCHECK_BOOLERFORCE
228 else if(solver_option ==
"minisat1")
230#if defined SATCHECK_MINISAT1
236 else if(solver_option ==
"minisat2")
238#if defined SATCHECK_MINISAT2
254 else if(solver_option ==
"ipasir")
256#if defined SATCHECK_IPASIR
262 else if(solver_option ==
"picosat")
264#if defined SATCHECK_PICOSAT
270 else if(solver_option ==
"lingeling")
272#if defined SATCHECK_LINGELING
278 else if(solver_option ==
"glucose")
280#if defined SATCHECK_GLUCOSE
296 else if(solver_option ==
"cadical")
298#if defined SATCHECK_CADICAL
308 log.
error() <<
"unknown solver '" << solver_option <<
"'"
331 bool get_array_constraints =
332 options.get_bool_option(
"show-array-constraints");
333 auto bv_pointers = std::make_unique<bv_pointerst>(
336 if(
options.get_option(
"arrays-uf") ==
"never")
338 else if(
options.get_option(
"arrays-uf") ==
"always")
343 std::unique_ptr<boolbvt> boolbv = std::move(bv_pointers);
344 return std::make_unique<solvert>(std::move(boolbv), std::move(sat_solver));
354 std::string filename =
options.get_option(
"outfile");
356 std::unique_ptr<boolbvt> bv_dimacs =
359 return std::make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
367 std::string external_sat_solver =
options.get_option(
"external-sat-solver");
371 std::unique_ptr<boolbvt> bv_pointers =
374 return std::make_unique<solvert>(std::move(bv_pointers), std::move(prop));
383 info.
prop = prop.get();
387 if(
options.get_bool_option(
"max-node-refinement"))
389 options.get_unsigned_int_option(
"max-node-refinement");
395 std::unique_ptr<boolbvt> decision_procedure =
396 std::make_unique<bv_refinementt>(info);
398 return std::make_unique<solvert>(
399 std::move(decision_procedure), std::move(prop));
405std::unique_ptr<solver_factoryt::solvert>
411 info.
prop = prop.get();
414 if(
options.get_bool_option(
"max-node-refinement"))
416 options.get_unsigned_int_option(
"max-node-refinement");
421 std::unique_ptr<boolbvt> decision_procedure =
422 std::make_unique<string_refinementt>(info);
424 return std::make_unique<solvert>(
425 std::move(decision_procedure), std::move(prop));
429 const std::string &filename,
431 const std::string &arg_name)
441 "failed to open file: " + filename, arg_name);
445 log.
status() <<
"Outputting SMTLib formula to file: " << filename
450std::unique_ptr<solver_factoryt::solvert>
455 const std::string outfile_arg =
options.get_option(
"outfile");
456 const std::string dump_smt_formula =
options.get_option(
"dump-smt-formula");
458 if(!outfile_arg.empty() && !dump_smt_formula.empty())
461 "Argument --outfile is incompatible with --dump-smt-formula. ",
465 std::unique_ptr<smt_base_solver_processt> solver_process =
nullptr;
467 if(!outfile_arg.empty())
469 bool on_std_out = outfile_arg ==
"-";
470 std::unique_ptr<std::ostream> outfile =
474 solver_process = std::make_unique<smt_incremental_dry_run_solvert>(
475 message_handler, on_std_out ? std::cout : *outfile, std::move(outfile));
479 const auto out_filename =
options.get_option(
"dump-smt-formula");
483 solver_process = std::make_unique<smt_piped_solver_processt>(
484 std::move(solver_command),
490 return std::make_unique<solvert>(
491 std::make_unique<smt2_incremental_decision_proceduret>(
495std::unique_ptr<solver_factoryt::solvert>
500 const std::string &filename =
options.get_option(
"outfile");
507 "required filename not provided",
509 "provide a filename with --outfile");
512 auto smt2_dec = std::make_unique<smt2_dect>(
520 if(
options.get_bool_option(
"fpa"))
521 smt2_dec->use_FPA_theory =
true;
523 return std::make_unique<solvert>(std::move(smt2_dec));
525 else if(filename ==
"-")
527 auto smt2_conv = std::make_unique<smt2_convt>(
535 if(
options.get_bool_option(
"fpa"))
536 smt2_conv->use_FPA_theory =
true;
538 return std::make_unique<solvert>(std::move(smt2_conv));
544 auto smt2_conv = std::make_unique<smt2_convt>(
552 if(
options.get_bool_option(
"fpa"))
553 smt2_conv->use_FPA_theory =
true;
555 return std::make_unique<solvert>(std::move(smt2_conv), std::move(out));
561 if(
options.get_bool_option(
"beautify"))
564 "the chosen solver does not support beautification",
"--beautify");
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");
577 "the chosen solver does not support incremental solving",
583 "the chosen solver does not support incremental solving",
"--cover");
585 else if(incremental_loop)
588 "the chosen solver does not support incremental solving",
589 "--incremental-loop");
595 if(cmdline.
isset(
"external-sat-solver"))
598 "external-sat-solver", cmdline.
get_value(
"external-sat-solver"));
603 if(cmdline.
isset(
"dimacs"))
606 if(cmdline.
isset(
"sat-solver"))
612 if(cmdline.
isset(
"smt2"))
615 if(cmdline.
isset(
"fpa"))
618 bool solver_set =
false;
620 if(cmdline.
isset(
"bitwuzla"))
626 if(cmdline.
isset(
"boolector"))
632 if(cmdline.
isset(
"cprover-smt2"))
638 if(cmdline.
isset(
"mathsat"))
644 if(cmdline.
isset(
"cvc4"))
650 if(cmdline.
isset(
"cvc5"))
656 if(cmdline.
isset(
"incremental-smt2-solver"))
659 "incremental-smt2-solver", cmdline.
get_value(
"incremental-smt2-solver")),
663 if(cmdline.
isset(
"yices"))
669 if(cmdline.
isset(
"z3"))
675 if(cmdline.
isset(
"smt2") && !solver_set)
677 if(cmdline.
isset(
"outfile"))
695 if(cmdline.
isset(
"outfile"))
698 if(cmdline.
isset(
"dump-smt-formula"))
700 "dump-smt-formula", cmdline.
get_value(
"dump-smt-formula"));
702 if(cmdline.
isset(
"write-solver-stats-to"))
705 "write-solver-stats-to", cmdline.
get_value(
"write-solver-stats-to"));
708 if(cmdline.
isset(
"beautify"))
711 if(cmdline.
isset(
"refine-arrays"))
717 if(cmdline.
isset(
"refine-arithmetic"))
723 if(cmdline.
isset(
"refine"))
730 if(cmdline.
isset(
"max-node-refinement"))
733 "max-node-refinement", cmdline.
get_value(
"max-node-refinement"));
Abstraction Refinement Loop.
std::string get_value(char option) const
virtual bool isset(char option) const
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'.
mstreamt & warning() const
mstreamt & status() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
bool get_bool_option(const std::string &option) const
void set_option(const std::string &option, const bool value)
const std::string get_option(const std::string &option) const
std::unique_ptr< stack_decision_proceduret > decision_procedure_ptr
std::unique_ptr< propt > prop_ptr
std::unique_ptr< std::ofstream > ofstream_ptr
boolbvt & boolbv_decision_procedure() const
solvert(std::unique_ptr< stack_decision_proceduret > p)
stack_decision_proceduret & decision_procedure() const
std::unique_ptr< boolbvt > decision_procedure_is_boolbvt_ptr
message_handlert & message_handler
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()
void no_incremental_check()
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.
Allows calling an external SAT solver to allow faster integration of newer SAT solvers.
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)
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.
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)
String support via creating string constraints and progressively instantiating the universal constrai...
#define DEFAULT_MAX_NB_REFINEMENT
unsigned max_node_refinement
Max number of times we refine a formula node.
bool refine_arrays
Enable array refinement.
bool refine_arithmetic
Enable arithmetic refinement.
message_handlert * message_handler
std::size_t refinement_bound
string_refinementt constructor arguments
#define widen_if_needed(s)
const char * CBMC_VERSION