42 bool _output_xml_in_refinement)
45 message_handler(_message_handler),
46 output_xml_in_refinement(_output_xml_in_refinement)
51 : decision_procedure_ptr(
std::move(p))
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))
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))
72 return *decision_procedure_ptr;
88 const int timeout_seconds =
91 if(timeout_seconds > 0)
98 log.
warning() <<
"cannot set solver time limit on "
104 solver->set_time_limit_seconds(timeout_seconds);
109 std::unique_ptr<decision_proceduret> p)
111 decision_procedure_ptr = std::move(p);
116 prop_ptr = std::move(p);
121 ofstream_ptr = std::move(p);
138 const auto incremental_smt2_solver =
140 if(!incremental_smt2_solver.empty())
183 const std::string &
solver)
187 <<
"', is not available. "
188 <<
"The default solver will be used instead." <<
messaget::eom;
191template <
typename SatcheckT>
192static std::unique_ptr<SatcheckT>
201 std::unique_ptr<solver_hardnesst> solver_hardness =
204 hardness_collector->solver_hardness = std::move(solver_hardness);
210 <<
"Configured solver does not support --write-solver-stats-to. "
217static std::unique_ptr<propt>
228 if(solver_option ==
"zchaff")
230#if defined SATCHECK_ZCHAFF
236 else if(solver_option ==
"booleforce")
238#if defined SATCHECK_BOOLERFORCE
244 else if(solver_option ==
"minisat1")
246#if defined SATCHECK_MINISAT1
252 else if(solver_option ==
"minisat2")
254#if defined SATCHECK_MINISAT2
270 else if(solver_option ==
"ipasir")
272#if defined SATCHECK_IPASIR
278 else if(solver_option ==
"picosat")
280#if defined SATCHECK_PICOSAT
286 else if(solver_option ==
"lingeling")
288#if defined SATCHECK_LINGELING
294 else if(solver_option ==
"glucose")
296#if defined SATCHECK_GLUCOSE
312 else if(solver_option ==
"cadical")
314#if defined SATCHECK_CADICAL
323 log.
error() <<
"unknown solver '" << solver_option <<
"'"
346 bool get_array_constraints =
359 std::move(bv_pointers), std::move(sat_solver));
397 info.
prop = prop.get();
412 std::move(decision_procedure), std::move(prop));
418std::unique_ptr<solver_factoryt::solvert>
424 info.
prop = prop.get();
437 std::move(decision_procedure), std::move(prop));
441 const std::string &filename,
443 const std::string &arg_name)
453 "failed to open file: " + filename, arg_name);
457 log.
status() <<
"Outputting SMTLib formula to file: " << filename
462std::unique_ptr<solver_factoryt::solvert>
470 if(!outfile_arg.empty() && !dump_smt_formula.empty())
473 "Argument --outfile is incompatible with --dump-smt-formula. ",
477 std::unique_ptr<smt_base_solver_processt> solver_process =
nullptr;
479 if(!outfile_arg.empty())
481 bool on_std_out = outfile_arg ==
"-";
482 std::unique_ptr<std::ostream> outfile =
487 message_handler, on_std_out ? std::cout : *outfile, std::move(outfile));
496 std::move(solver_command),
507std::unique_ptr<solver_factoryt::solvert>
519 "required filename not provided",
521 "provide a filename with --outfile");
533 smt2_dec->use_FPA_theory =
true;
538 else if(filename ==
"-")
549 smt2_conv->use_FPA_theory =
true;
567 smt2_conv->use_FPA_theory =
true;
579 "the chosen solver does not support beautification",
"--beautify");
587 const bool incremental_loop =
options.
is_set(
"incremental-loop");
592 "the chosen solver does not support incremental solving",
598 "the chosen solver does not support incremental solving",
"--cover");
600 else if(incremental_loop)
603 "the chosen solver does not support incremental solving",
604 "--incremental-loop");
610 if(cmdline.
isset(
"external-sat-solver"))
613 "external-sat-solver", cmdline.
get_value(
"external-sat-solver"));
618 if(cmdline.
isset(
"dimacs"))
621 if(cmdline.
isset(
"sat-solver"))
627 if(cmdline.
isset(
"smt2"))
630 if(cmdline.
isset(
"fpa"))
633 bool solver_set =
false;
635 if(cmdline.
isset(
"bitwuzla"))
641 if(cmdline.
isset(
"boolector"))
647 if(cmdline.
isset(
"cprover-smt2"))
653 if(cmdline.
isset(
"mathsat"))
659 if(cmdline.
isset(
"cvc4"))
665 if(cmdline.
isset(
"cvc5"))
671 if(cmdline.
isset(
"incremental-smt2-solver"))
674 "incremental-smt2-solver", cmdline.
get_value(
"incremental-smt2-solver")),
678 if(cmdline.
isset(
"yices"))
684 if(cmdline.
isset(
"z3"))
690 if(cmdline.
isset(
"smt2") && !solver_set)
692 if(cmdline.
isset(
"outfile"))
710 if(cmdline.
isset(
"outfile"))
713 if(cmdline.
isset(
"dump-smt-formula"))
715 "dump-smt-formula", cmdline.
get_value(
"dump-smt-formula"));
717 if(cmdline.
isset(
"write-solver-stats-to"))
720 "write-solver-stats-to", cmdline.
get_value(
"write-solver-stats-to"));
723 if(cmdline.
isset(
"beautify"))
726 if(cmdline.
isset(
"refine-arrays"))
732 if(cmdline.
isset(
"refine-arithmetic"))
738 if(cmdline.
isset(
"refine"))
745 if(cmdline.
isset(
"max-node-refinement"))
748 "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
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'.
mstreamt & warning() const
mstreamt & status() const
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.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
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 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)
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)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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