49 : decision_procedure_ptr(
std::move(p))
54 std::unique_ptr<stack_decision_proceduret>
p1,
55 std::unique_ptr<propt>
p2)
56 : prop_ptr(
std::move(
p2)), decision_procedure_ptr(
std::move(
p1))
61 std::unique_ptr<stack_decision_proceduret>
p1,
62 std::unique_ptr<std::ofstream>
p2)
63 : ofstream_ptr(
std::move(
p2)), decision_procedure_ptr(
std::move(
p1))
68 std::unique_ptr<boolbvt>
p1,
69 std::unique_ptr<propt>
p2)
70 : prop_ptr(
std::move(
p2)), decision_procedure_is_boolbvt_ptr(
std::move(
p1))
77 (decision_procedure_ptr !=
nullptr) !=
78 (decision_procedure_is_boolbvt_ptr !=
nullptr));
79 if(decision_procedure_ptr)
80 return *decision_procedure_ptr;
82 return *decision_procedure_is_boolbvt_ptr;
87 PRECONDITION(decision_procedure_is_boolbvt_ptr !=
nullptr);
88 return *decision_procedure_is_boolbvt_ptr;
95 options.get_signed_int_option(
"solver-time-limit");
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"))
116 options.get_option(
"incremental-smt2-solver");
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)
163 log.warning() <<
"The specified solver, '" <<
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
175 if(
options.is_set(
"write-solver-stats-to"))
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
192 if(
options.is_set(
"write-solver-stats-to"))
194 std::unique_ptr<solver_hardnesst> solver_hardness =
195 std::make_unique<solver_hardnesst>();
196 solver_hardness->set_outfile(
options.get_option(
"write-solver-stats-to"));
197 satcheck->solver_hardness = std::move(solver_hardness);
202static std::unique_ptr<propt>
206 !
options.get_bool_option(
"sat-preprocessor") ||
207 options.get_bool_option(
"refine-strings");
209 if(
options.is_set(
"sat-solver"))
214#if defined SATCHECK_ZCHAFF
222#if defined SATCHECK_BOOLERFORCE
230#if defined SATCHECK_MINISAT1
238#if defined SATCHECK_MINISAT2
256#if defined SATCHECK_IPASIR
264#if defined SATCHECK_PICOSAT
272#if defined SATCHECK_LINGELING
280#if defined SATCHECK_GLUCOSE
298#if defined SATCHECK_CADICAL
331 bool get_array_constraints =
332 options.get_bool_option(
"show-array-constraints");
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");
359 return std::make_unique<solvert>(std::move(
bv_dimacs), std::move(prop));
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"))
388 info.max_node_refinement =
389 options.get_unsigned_int_option(
"max-node-refinement");
391 info.refine_arrays =
options.get_bool_option(
"refine-arrays");
392 info.refine_arithmetic =
options.get_bool_option(
"refine-arithmetic");
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"))
415 info.max_node_refinement =
416 options.get_unsigned_int_option(
"max-node-refinement");
417 info.refine_arrays =
options.get_bool_option(
"refine-arrays");
418 info.refine_arithmetic =
options.get_bool_option(
"refine-arithmetic");
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,
441 "failed to open file: " + filename,
arg_name);
445 log.status() <<
"Outputting SMTLib formula to file: " << filename
450std::unique_ptr<solver_factoryt::solvert>
461 "Argument --outfile is incompatible with --dump-smt-formula. ",
465 std::unique_ptr<smt_base_solver_processt> solver_process =
nullptr;
470 std::unique_ptr<std::ostream> outfile =
474 solver_process = std::make_unique<smt_incremental_dry_run_solvert>(
483 solver_process = std::make_unique<smt_piped_solver_processt>(
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"))
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");
577 "the chosen solver does not support incremental solving",
583 "the chosen solver does not support incremental solving",
"--cover");
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"));
601 options.set_option(
"sat-preprocessor", !cmdline.
isset(
"no-sat-preprocessor"));
603 if(cmdline.
isset(
"dimacs"))
604 options.set_option(
"dimacs",
true);
606 if(cmdline.
isset(
"sat-solver"))
612 if(cmdline.
isset(
"smt2"))
613 options.set_option(
"smt2",
true);
615 if(cmdline.
isset(
"fpa"))
616 options.set_option(
"fpa",
true);
620 if(cmdline.
isset(
"bitwuzla"))
623 options.set_option(
"smt2",
true);
626 if(cmdline.
isset(
"boolector"))
629 options.set_option(
"smt2",
true);
632 if(cmdline.
isset(
"cprover-smt2"))
635 options.set_option(
"smt2",
true);
638 if(cmdline.
isset(
"mathsat"))
641 options.set_option(
"smt2",
true);
644 if(cmdline.
isset(
"cvc4"))
647 options.set_option(
"smt2",
true);
650 if(cmdline.
isset(
"cvc5"))
653 options.set_option(
"smt2",
true);
656 if(cmdline.
isset(
"incremental-smt2-solver"))
659 "incremental-smt2-solver", cmdline.
get_value(
"incremental-smt2-solver")),
663 if(cmdline.
isset(
"yices"))
666 options.set_option(
"smt2",
true);
669 if(cmdline.
isset(
"z3"))
672 options.set_option(
"smt2",
true);
677 if(cmdline.
isset(
"outfile"))
680 options.set_option(
"generic",
true);
685 options.set_option(
"z3",
true);
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"))
709 options.set_option(
"beautify",
true);
711 if(cmdline.
isset(
"refine-arrays"))
713 options.set_option(
"refine",
true);
714 options.set_option(
"refine-arrays",
true);
717 if(cmdline.
isset(
"refine-arithmetic"))
719 options.set_option(
"refine",
true);
720 options.set_option(
"refine-arithmetic",
true);
723 if(cmdline.
isset(
"refine"))
725 options.set_option(
"refine",
true);
726 options.set_option(
"refine-arrays",
true);
727 options.set_option(
"refine-arithmetic",
true);
730 if(cmdline.
isset(
"max-node-refinement"))
733 "max-node-refinement", cmdline.
get_value(
"max-node-refinement"));
Abstraction Refinement Loop.
message_handlert & message_handler
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
boolbvt & boolbv_decision_procedure() const
solvert(std::unique_ptr< stack_decision_proceduret > p)
stack_decision_proceduret & decision_procedure() const
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
string_refinementt constructor arguments
#define widen_if_needed(s)
const char * CBMC_VERSION