45 bool _output_xml_in_refinement)
48 message_handler(_message_handler),
49 output_xml_in_refinement(_output_xml_in_refinement)
54 : decision_procedure_ptr(std::move(p))
59 std::unique_ptr<decision_proceduret> p1,
60 std::unique_ptr<propt> p2)
61 : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
66 std::unique_ptr<decision_proceduret> p1,
67 std::unique_ptr<std::ofstream> p2)
68 : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
75 return *decision_procedure_ptr;
97 const int timeout_seconds =
100 if(timeout_seconds > 0)
107 log.
warning() <<
"cannot set solver time limit on "
113 solver->set_time_limit_seconds(timeout_seconds);
118 std::unique_ptr<decision_proceduret> p)
120 decision_procedure_ptr = std::move(p);
125 prop_ptr = std::move(p);
130 ofstream_ptr = std::move(p);
147 const auto incremental_smt2_solver =
149 if(!incremental_smt2_solver.empty())
185 template <
typename SatcheckT>
186 static std::unique_ptr<SatcheckT>
195 std::unique_ptr<solver_hardnesst> solver_hardness =
196 util_make_unique<solver_hardnesst>();
198 hardness_collector->solver_hardness = std::move(solver_hardness);
204 <<
"Configured solver does not support --write-solver-stats-to. "
213 auto solver = util_make_unique<solvert>();
227 bool get_array_constraints =
229 auto bv_pointers = util_make_unique<bv_pointerst>(
238 solver->set_decision_procedure(std::move(bv_pointers));
255 return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
269 return util_make_unique<solvert>(std::move(bv_pointers), std::move(prop));
274 std::unique_ptr<propt> prop = [
this]() -> std::unique_ptr<propt> {
281 return make_satcheck_prop<satcheck_no_simplifiert>(
287 info.
prop = prop.get();
299 auto decision_procedure = util_make_unique<bv_refinementt>(info);
301 return util_make_unique<solvert>(
302 std::move(decision_procedure), std::move(prop));
308 std::unique_ptr<solver_factoryt::solvert>
315 info.
prop = prop.get();
325 auto decision_procedure = util_make_unique<string_refinementt>(info);
327 return util_make_unique<solvert>(
328 std::move(decision_procedure), std::move(prop));
331 std::unique_ptr<solver_factoryt::solvert>
335 auto solver_process = util_make_unique<smt_piped_solver_processt>(
338 return util_make_unique<solvert>(
339 util_make_unique<smt2_incremental_decision_proceduret>(
343 std::unique_ptr<solver_factoryt::solvert>
355 "required filename not provided",
357 "provide a filename with --outfile");
360 auto smt2_dec = util_make_unique<smt2_dect>(
369 smt2_dec->use_FPA_theory =
true;
372 return util_make_unique<solvert>(std::move(smt2_dec));
374 else if(filename ==
"-")
376 auto smt2_conv = util_make_unique<smt2_convt>(
385 smt2_conv->use_FPA_theory =
true;
388 return util_make_unique<solvert>(std::move(smt2_conv));
393 auto out = util_make_unique<std::ofstream>(
widen(filename));
395 auto out = util_make_unique<std::ofstream>(filename);
401 "failed to open file: " + filename,
"--outfile");
404 auto smt2_conv = util_make_unique<smt2_convt>(
413 smt2_conv->use_FPA_theory =
true;
416 return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
425 "the chosen solver does not support beautification",
"--beautify");
433 const bool incremental_loop =
options.
is_set(
"incremental-loop");
438 "the chosen solver does not support incremental solving",
444 "the chosen solver does not support incremental solving",
"--cover");
446 else if(incremental_loop)
449 "the chosen solver does not support incremental solving",
450 "--incremental-loop");
Abstraction Refinement Loop.
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
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
const std::string get_option(const std::string &option) const
signed int get_signed_int_option(const std::string &option) const
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()
Allows calling an external SAT solver to allow faster integration of newer SAT solvers.
Decision procedure with incremental SMT2 solving.
int solver(std::istream &in)
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
std::wstring widen(const char *s)
const char * CBMC_VERSION