43 bool _output_xml_in_refinement)
46 message_handler(_message_handler),
47 output_xml_in_refinement(_output_xml_in_refinement)
52 : decision_procedure_ptr(std::move(p))
57 std::unique_ptr<decision_proceduret> p1,
58 std::unique_ptr<propt> p2)
59 : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
64 std::unique_ptr<decision_proceduret> p1,
65 std::unique_ptr<std::ofstream> p2)
66 : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
73 return *decision_procedure_ptr;
95 const int timeout_seconds =
98 if(timeout_seconds > 0)
105 log.
warning() <<
"cannot set solver time limit on "
111 solver->set_time_limit_seconds(timeout_seconds);
116 std::unique_ptr<decision_proceduret> p)
118 decision_procedure_ptr = std::move(p);
123 prop_ptr = std::move(p);
128 ofstream_ptr = std::move(p);
179 template <
typename SatcheckT>
180 static std::unique_ptr<SatcheckT>
186 satcheck->enable_hardness_collection();
196 auto solver = util_make_unique<solvert>();
219 solver->set_decision_procedure(std::move(bv_pointers));
236 return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
250 return util_make_unique<solvert>(std::move(bv_pointers), std::move(prop));
255 std::unique_ptr<propt> prop = [
this]() -> std::unique_ptr<propt> {
262 return make_satcheck_prop<satcheck_no_simplifiert>(
268 info.
prop = prop.get();
280 auto decision_procedure = util_make_unique<bv_refinementt>(info);
282 return util_make_unique<solvert>(
283 std::move(decision_procedure), std::move(prop));
289 std::unique_ptr<solver_factoryt::solvert>
296 info.
prop = prop.get();
306 auto decision_procedure = util_make_unique<string_refinementt>(info);
308 return util_make_unique<solvert>(
309 std::move(decision_procedure), std::move(prop));
312 std::unique_ptr<solver_factoryt::solvert>
324 "required filename not provided",
326 "provide a filename with --outfile");
329 auto smt2_dec = util_make_unique<smt2_dect>(
338 smt2_dec->use_FPA_theory =
true;
343 return util_make_unique<solvert>(std::move(smt2_dec));
345 else if(filename ==
"-")
347 auto smt2_conv = util_make_unique<smt2_convt>(
356 smt2_conv->use_FPA_theory =
true;
359 return util_make_unique<solvert>(std::move(smt2_conv));
364 auto out = util_make_unique<std::ofstream>(
widen(filename));
366 auto out = util_make_unique<std::ofstream>(filename);
372 "failed to open file: " + filename,
"--outfile");
375 auto smt2_conv = util_make_unique<smt2_convt>(
384 smt2_conv->use_FPA_theory =
true;
387 return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
396 "the chosen solver does not support beautification",
"--beautify");
404 const bool incremental_check =
options.
is_set(
"incremental-check");
409 "the chosen solver does not support incremental solving",
415 "the chosen solver does not support incremental solving",
"--cover");
417 else if(incremental_check)
420 "the chosen solver does not support incremental solving",
421 "--incremental-check");