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>
213 if(solver_option ==
"zchaff")
215#if defined SATCHECK_ZCHAFF
221 else if(solver_option ==
"booleforce")
223#if defined SATCHECK_BOOLERFORCE
229 else if(solver_option ==
"minisat1")
231#if defined SATCHECK_MINISAT1
237 else if(solver_option ==
"minisat2")
239#if defined SATCHECK_MINISAT2
255 else if(solver_option ==
"ipasir")
257#if defined SATCHECK_IPASIR
263 else if(solver_option ==
"picosat")
265#if defined SATCHECK_PICOSAT
271 else if(solver_option ==
"lingeling")
273#if defined SATCHECK_LINGELING
279 else if(solver_option ==
"glucose")
281#if defined SATCHECK_GLUCOSE
297 else if(solver_option ==
"cadical")
299#if defined SATCHECK_CADICAL
309 log.
error() <<
"unknown solver '" << solver_option <<
"'"
332 bool get_array_constraints =
333 options.get_bool_option(
"show-array-constraints");
334 auto bv_pointers = std::make_unique<bv_pointerst>(
337 if(
options.get_option(
"arrays-uf") ==
"never")
339 else if(
options.get_option(
"arrays-uf") ==
"always")
344 std::unique_ptr<boolbvt> boolbv = std::move(bv_pointers);
345 return std::make_unique<solvert>(std::move(boolbv), std::move(sat_solver));
355 std::string filename =
options.get_option(
"outfile");
357 std::unique_ptr<boolbvt> bv_dimacs =
360 return std::make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
368 std::string external_sat_solver =
options.get_option(
"external-sat-solver");
372 std::unique_ptr<boolbvt> bv_pointers =
375 return std::make_unique<solvert>(std::move(bv_pointers), std::move(prop));
384 info.
prop = prop.get();
388 if(
options.get_bool_option(
"max-node-refinement"))
390 options.get_unsigned_int_option(
"max-node-refinement");
396 std::unique_ptr<boolbvt> decision_procedure =
397 std::make_unique<bv_refinementt>(info);
399 return std::make_unique<solvert>(
400 std::move(decision_procedure), std::move(prop));
406std::unique_ptr<solver_factoryt::solvert>
412 info.
prop = prop.get();
415 if(
options.get_bool_option(
"max-node-refinement"))
417 options.get_unsigned_int_option(
"max-node-refinement");
422 std::unique_ptr<boolbvt> decision_procedure =
423 std::make_unique<string_refinementt>(info);
425 return std::make_unique<solvert>(
426 std::move(decision_procedure), std::move(prop));
430 const std::string &filename,
432 const std::string &arg_name)
442 "failed to open file: " + filename, arg_name);
446 log.
status() <<
"Outputting SMTLib formula to file: " << filename
451std::unique_ptr<solver_factoryt::solvert>
456 const std::string outfile_arg =
options.get_option(
"outfile");
457 const std::string dump_smt_formula =
options.get_option(
"dump-smt-formula");
459 if(!outfile_arg.empty() && !dump_smt_formula.empty())
462 "Argument --outfile is incompatible with --dump-smt-formula. ",
466 std::unique_ptr<smt_base_solver_processt> solver_process =
nullptr;
468 if(!outfile_arg.empty())
470 bool on_std_out = outfile_arg ==
"-";
471 std::unique_ptr<std::ostream> outfile =
475 solver_process = std::make_unique<smt_incremental_dry_run_solvert>(
476 message_handler, on_std_out ? std::cout : *outfile, std::move(outfile));
480 const auto out_filename =
options.get_option(
"dump-smt-formula");
484 solver_process = std::make_unique<smt_piped_solver_processt>(
485 std::move(solver_command),
491 return std::make_unique<solvert>(
492 std::make_unique<smt2_incremental_decision_proceduret>(
496std::unique_ptr<solver_factoryt::solvert>
501 const std::string &filename =
options.get_option(
"outfile");
508 "required filename not provided",
510 "provide a filename with --outfile");
513 auto smt2_dec = std::make_unique<smt2_dect>(
521 if(
options.get_bool_option(
"fpa"))
522 smt2_dec->use_FPA_theory =
true;
524 return std::make_unique<solvert>(std::move(smt2_dec));
526 else if(filename ==
"-")
528 auto smt2_conv = std::make_unique<smt2_convt>(
536 if(
options.get_bool_option(
"fpa"))
537 smt2_conv->use_FPA_theory =
true;
539 return std::make_unique<solvert>(std::move(smt2_conv));
545 auto smt2_conv = std::make_unique<smt2_convt>(
553 if(
options.get_bool_option(
"fpa"))
554 smt2_conv->use_FPA_theory =
true;
556 return std::make_unique<solvert>(std::move(smt2_conv), std::move(out));
562 if(
options.get_bool_option(
"beautify"))
565 "the chosen solver does not support beautification",
"--beautify");
571 const bool all_properties =
options.get_bool_option(
"all-properties");
572 const bool cover =
options.is_set(
"cover");
573 const bool incremental_loop =
options.is_set(
"incremental-loop");
578 "the chosen solver does not support incremental solving",
584 "the chosen solver does not support incremental solving",
"--cover");
586 else if(incremental_loop)
589 "the chosen solver does not support incremental solving",
590 "--incremental-loop");
596 if(cmdline.
isset(
"external-sat-solver"))
599 "external-sat-solver", cmdline.
get_value(
"external-sat-solver"));
604 if(cmdline.
isset(
"dimacs"))
607 if(cmdline.
isset(
"sat-solver"))
613 if(cmdline.
isset(
"smt2"))
616 if(cmdline.
isset(
"fpa"))
619 bool solver_set =
false;
621 if(cmdline.
isset(
"bitwuzla"))
627 if(cmdline.
isset(
"boolector"))
633 if(cmdline.
isset(
"cprover-smt2"))
639 if(cmdline.
isset(
"mathsat"))
645 if(cmdline.
isset(
"cvc4"))
651 if(cmdline.
isset(
"cvc5"))
657 if(cmdline.
isset(
"incremental-smt2-solver"))
660 "incremental-smt2-solver", cmdline.
get_value(
"incremental-smt2-solver")),
664 if(cmdline.
isset(
"yices"))
670 if(cmdline.
isset(
"z3"))
676 if(cmdline.
isset(
"smt2") && !solver_set)
678 if(cmdline.
isset(
"outfile"))
696 if(cmdline.
isset(
"outfile"))
699 if(cmdline.
isset(
"dump-smt-formula"))
701 "dump-smt-formula", cmdline.
get_value(
"dump-smt-formula"));
703 if(cmdline.
isset(
"write-solver-stats-to"))
706 "write-solver-stats-to", cmdline.
get_value(
"write-solver-stats-to"));
709 if(cmdline.
isset(
"beautify"))
712 if(cmdline.
isset(
"refine-arrays"))
718 if(cmdline.
isset(
"refine-arithmetic"))
724 if(cmdline.
isset(
"refine"))
731 if(cmdline.
isset(
"max-node-refinement"))
734 "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