41 bool _output_xml_in_refinement)
44 message_handler(_message_handler),
45 output_xml_in_refinement(_output_xml_in_refinement)
50 : decision_procedure_ptr(std::move(p))
55 std::unique_ptr<decision_proceduret> p1,
56 std::unique_ptr<propt> p2)
57 : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
62 std::unique_ptr<decision_proceduret> p1,
63 std::unique_ptr<std::ofstream> p2)
64 : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
71 return *decision_procedure_ptr;
87 const int timeout_seconds =
90 if(timeout_seconds > 0)
97 log.warning() <<
"cannot set solver time limit on "
103 solver->set_time_limit_seconds(timeout_seconds);
108 std::unique_ptr<decision_proceduret> p)
110 decision_procedure_ptr = std::move(p);
115 prop_ptr = std::move(p);
120 ofstream_ptr = std::move(p);
137 const auto incremental_smt2_solver =
139 if(!incremental_smt2_solver.empty())
182 const std::string &
solver)
185 log.warning() <<
"The specified solver, '" <<
solver
186 <<
"', is not available. "
187 <<
"The default solver will be used instead." <<
messaget::eom;
190 template <
typename SatcheckT>
191 static std::unique_ptr<SatcheckT>
200 std::unique_ptr<solver_hardnesst> solver_hardness =
201 std::make_unique<solver_hardnesst>();
203 hardness_collector->solver_hardness = std::move(solver_hardness);
209 <<
"Configured solver does not support --write-solver-stats-to. "
216 static std::unique_ptr<propt>
227 if(solver_option ==
"zchaff")
229 #if defined SATCHECK_ZCHAFF
235 else if(solver_option ==
"booleforce")
237 #if defined SATCHECK_BOOLERFORCE
243 else if(solver_option ==
"minisat1")
245 #if defined SATCHECK_MINISAT1
251 else if(solver_option ==
"minisat2")
253 #if defined SATCHECK_MINISAT2
257 return make_satcheck_prop<satcheck_minisat_no_simplifiert>(
262 return make_satcheck_prop<satcheck_minisat_simplifiert>(
269 else if(solver_option ==
"ipasir")
271 #if defined SATCHECK_IPASIR
277 else if(solver_option ==
"picosat")
279 #if defined SATCHECK_PICOSAT
285 else if(solver_option ==
"lingeling")
287 #if defined SATCHECK_LINGELING
293 else if(solver_option ==
"glucose")
295 #if defined SATCHECK_GLUCOSE
299 return make_satcheck_prop<satcheck_glucose_no_simplifiert>(
304 return make_satcheck_prop<satcheck_glucose_simplifiert>(
311 else if(solver_option ==
"cadical")
313 #if defined SATCHECK_CADICAL
322 log.error() <<
"unknown solver '" << solver_option <<
"'"
332 return make_satcheck_prop<satcheck_no_simplifiert>(
345 bool get_array_constraints =
347 auto bv_pointers = std::make_unique<bv_pointerst>(
357 return std::make_unique<solvert>(
358 std::move(bv_pointers), std::move(sat_solver));
373 return std::make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
387 return std::make_unique<solvert>(std::move(bv_pointers), std::move(prop));
396 info.
prop = prop.get();
408 auto decision_procedure = std::make_unique<bv_refinementt>(info);
410 return std::make_unique<solvert>(
411 std::move(decision_procedure), std::move(prop));
417 std::unique_ptr<solver_factoryt::solvert>
423 info.
prop = prop.get();
433 auto decision_procedure = std::make_unique<string_refinementt>(info);
435 return std::make_unique<solvert>(
436 std::move(decision_procedure), std::move(prop));
440 const std::string &filename,
442 const std::string &arg_name)
452 "failed to open file: " + filename, arg_name);
456 log.status() <<
"Outputting SMTLib formula to file: " << filename
461 std::unique_ptr<solver_factoryt::solvert>
469 if(!outfile_arg.empty() && !dump_smt_formula.empty())
472 "Argument --outfile is incompatible with --dump-smt-formula. ",
476 std::unique_ptr<smt_base_solver_processt> solver_process =
nullptr;
478 if(!outfile_arg.empty())
480 bool on_std_out = outfile_arg ==
"-";
481 std::unique_ptr<std::ostream> outfile =
485 solver_process = std::make_unique<smt_incremental_dry_run_solvert>(
486 message_handler, on_std_out ? std::cout : *outfile, std::move(outfile));
494 solver_process = std::make_unique<smt_piped_solver_processt>(
495 std::move(solver_command),
501 return std::make_unique<solvert>(
502 std::make_unique<smt2_incremental_decision_proceduret>(
506 std::unique_ptr<solver_factoryt::solvert>
518 "required filename not provided",
520 "provide a filename with --outfile");
523 auto smt2_dec = std::make_unique<smt2_dect>(
532 smt2_dec->use_FPA_theory =
true;
535 return std::make_unique<solvert>(std::move(smt2_dec));
537 else if(filename ==
"-")
539 auto smt2_conv = std::make_unique<smt2_convt>(
548 smt2_conv->use_FPA_theory =
true;
551 return std::make_unique<solvert>(std::move(smt2_conv));
557 auto smt2_conv = std::make_unique<smt2_convt>(
566 smt2_conv->use_FPA_theory =
true;
569 return std::make_unique<solvert>(std::move(smt2_conv), std::move(out));
578 "the chosen solver does not support beautification",
"--beautify");
586 const bool incremental_loop =
options.
is_set(
"incremental-loop");
591 "the chosen solver does not support incremental solving",
597 "the chosen solver does not support incremental solving",
"--cover");
599 else if(incremental_loop)
602 "the chosen solver does not support incremental solving",
603 "--incremental-loop");
609 if(cmdline.
isset(
"external-sat-solver"))
612 "external-sat-solver", cmdline.
get_value(
"external-sat-solver"));
617 if(cmdline.
isset(
"dimacs"))
620 if(cmdline.
isset(
"sat-solver"))
626 if(cmdline.
isset(
"smt2"))
629 if(cmdline.
isset(
"fpa"))
632 bool solver_set =
false;
634 if(cmdline.
isset(
"bitwuzla"))
640 if(cmdline.
isset(
"boolector"))
646 if(cmdline.
isset(
"cprover-smt2"))
652 if(cmdline.
isset(
"mathsat"))
658 if(cmdline.
isset(
"cvc4"))
664 if(cmdline.
isset(
"cvc5"))
670 if(cmdline.
isset(
"incremental-smt2-solver"))
673 "incremental-smt2-solver", cmdline.
get_value(
"incremental-smt2-solver")),
677 if(cmdline.
isset(
"yices"))
683 if(cmdline.
isset(
"z3"))
689 if(cmdline.
isset(
"smt2") && !solver_set)
691 if(cmdline.
isset(
"outfile"))
709 if(cmdline.
isset(
"outfile"))
712 if(cmdline.
isset(
"dump-smt-formula"))
714 "dump-smt-formula", cmdline.
get_value(
"dump-smt-formula"));
716 if(cmdline.
isset(
"write-solver-stats-to"))
719 "write-solver-stats-to", cmdline.
get_value(
"write-solver-stats-to"));
722 if(cmdline.
isset(
"beautify"))
725 if(cmdline.
isset(
"refine-arrays"))
731 if(cmdline.
isset(
"refine-arithmetic"))
737 if(cmdline.
isset(
"refine"))
744 if(cmdline.
isset(
"max-node-refinement"))
747 "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
An interface for a decision procedure for satisfiability problems.
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'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
unsigned int get_unsigned_int_option(const std::string &option) const
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
signed int get_signed_int_option(const std::string &option) const
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
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 no_incremental_check()
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.
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 void parse_sat_options(const cmdlinet &cmdline, optionst &options)
static std::unique_ptr< propt > get_sat_solver(message_handlert &message_handler, const 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)
void parse_solver_options(const cmdlinet &cmdline, optionst &options)
Parse solver-related command-line parameters in cmdline and set corresponding values in 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 capability to set resource limits.
#define PRECONDITION(CONDITION)
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
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