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;
89 options.get_signed_int_option(
"solver-time-limit");
98 log.
warning() <<
"cannot set solver time limit on "
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);
126 if(
options.get_bool_option(
"dimacs"))
128 if(
options.is_set(
"external-sat-solver"))
131 options.get_bool_option(
"refine") &&
132 !
options.get_bool_option(
"refine-strings"))
136 else if(
options.get_bool_option(
"refine-strings"))
139 options.get_option(
"incremental-smt2-solver");
142 if(
options.get_bool_option(
"smt2"))
156 if(
options.get_bool_option(
"bitwuzla"))
158 else if(
options.get_bool_option(
"boolector"))
160 else if(
options.get_bool_option(
"cprover-smt2"))
162 else if(
options.get_bool_option(
"mathsat"))
164 else if(
options.get_bool_option(
"cvc3"))
166 else if(
options.get_bool_option(
"cvc4"))
168 else if(
options.get_bool_option(
"cvc5"))
170 else if(
options.get_bool_option(
"yices"))
172 else if(
options.get_bool_option(
"z3"))
174 else if(
options.get_bool_option(
"generic"))
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>
196 if(
options.is_set(
"write-solver-stats-to"))
201 std::unique_ptr<solver_hardnesst> solver_hardness =
203 solver_hardness->set_outfile(
options.get_option(
"write-solver-stats-to"));
210 <<
"Configured solver does not support --write-solver-stats-to. "
217static std::unique_ptr<propt>
221 !
options.get_bool_option(
"sat-preprocessor") ||
222 options.get_bool_option(
"refine-arithmetic") ||
223 options.get_bool_option(
"refine-strings");
225 if(
options.is_set(
"sat-solver"))
230#if defined SATCHECK_ZCHAFF
238#if defined SATCHECK_BOOLERFORCE
246#if defined SATCHECK_MINISAT1
254#if defined SATCHECK_MINISAT2
272#if defined SATCHECK_IPASIR
280#if defined SATCHECK_PICOSAT
288#if defined SATCHECK_LINGELING
296#if defined SATCHECK_GLUCOSE
314#if defined SATCHECK_CADICAL
346 bool get_array_constraints =
347 options.get_bool_option(
"show-array-constraints");
351 if(
options.get_option(
"arrays-uf") ==
"never")
353 else if(
options.get_option(
"arrays-uf") ==
"always")
369 std::string filename =
options.get_option(
"outfile");
397 info.prop = prop.get();
401 if(
options.get_bool_option(
"max-node-refinement"))
402 info.max_node_refinement =
403 options.get_unsigned_int_option(
"max-node-refinement");
405 info.refine_arrays =
options.get_bool_option(
"refine-arrays");
406 info.refine_arithmetic =
options.get_bool_option(
"refine-arithmetic");
412 std::move(decision_procedure), std::move(prop));
418std::unique_ptr<solver_factoryt::solvert>
424 info.prop = prop.get();
427 if(
options.get_bool_option(
"max-node-refinement"))
428 info.max_node_refinement =
429 options.get_unsigned_int_option(
"max-node-refinement");
430 info.refine_arrays =
options.get_bool_option(
"refine-arrays");
431 info.refine_arithmetic =
options.get_bool_option(
"refine-arithmetic");
437 std::move(decision_procedure), std::move(prop));
441 const std::string &filename,
453 "failed to open file: " + filename,
arg_name);
457 log.
status() <<
"Outputting SMTLib formula to file: " << filename
462std::unique_ptr<solver_factoryt::solvert>
473 "Argument --outfile is incompatible with --dump-smt-formula. ",
477 std::unique_ptr<smt_base_solver_processt> solver_process =
nullptr;
482 std::unique_ptr<std::ostream> outfile =
507std::unique_ptr<solver_factoryt::solvert>
512 const std::string &filename =
options.get_option(
"outfile");
519 "required filename not provided",
521 "provide a filename with --outfile");
532 if(
options.get_bool_option(
"fpa"))
538 else if(filename ==
"-")
548 if(
options.get_bool_option(
"fpa"))
549 smt2_conv->use_FPA_theory =
true;
566 if(
options.get_bool_option(
"fpa"))
567 smt2_conv->use_FPA_theory =
true;
576 if(
options.get_bool_option(
"beautify"))
579 "the chosen solver does not support beautification",
"--beautify");
592 "the chosen solver does not support incremental solving",
598 "the chosen solver does not support incremental solving",
"--cover");
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"));
616 options.set_option(
"sat-preprocessor", !cmdline.
isset(
"no-sat-preprocessor"));
618 if(cmdline.
isset(
"dimacs"))
619 options.set_option(
"dimacs",
true);
621 if(cmdline.
isset(
"sat-solver"))
627 if(cmdline.
isset(
"smt2"))
628 options.set_option(
"smt2",
true);
630 if(cmdline.
isset(
"fpa"))
631 options.set_option(
"fpa",
true);
635 if(cmdline.
isset(
"bitwuzla"))
638 options.set_option(
"smt2",
true);
641 if(cmdline.
isset(
"boolector"))
644 options.set_option(
"smt2",
true);
647 if(cmdline.
isset(
"cprover-smt2"))
650 options.set_option(
"smt2",
true);
653 if(cmdline.
isset(
"mathsat"))
656 options.set_option(
"smt2",
true);
659 if(cmdline.
isset(
"cvc4"))
662 options.set_option(
"smt2",
true);
665 if(cmdline.
isset(
"cvc5"))
668 options.set_option(
"smt2",
true);
671 if(cmdline.
isset(
"incremental-smt2-solver"))
674 "incremental-smt2-solver", cmdline.
get_value(
"incremental-smt2-solver")),
678 if(cmdline.
isset(
"yices"))
681 options.set_option(
"smt2",
true);
684 if(cmdline.
isset(
"z3"))
687 options.set_option(
"smt2",
true);
692 if(cmdline.
isset(
"outfile"))
695 options.set_option(
"generic",
true);
700 options.set_option(
"z3",
true);
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"))
724 options.set_option(
"beautify",
true);
726 if(cmdline.
isset(
"refine-arrays"))
728 options.set_option(
"refine",
true);
729 options.set_option(
"refine-arrays",
true);
732 if(cmdline.
isset(
"refine-arithmetic"))
734 options.set_option(
"refine",
true);
735 options.set_option(
"refine-arithmetic",
true);
738 if(cmdline.
isset(
"refine"))
740 options.set_option(
"refine",
true);
741 options.set_option(
"refine-arrays",
true);
742 options.set_option(
"refine-arithmetic",
true);
745 if(cmdline.
isset(
"max-node-refinement"))
748 "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
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...
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 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
string_refinementt constructor arguments
#define widen_if_needed(s)
const char * CBMC_VERSION