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;
94 const int timeout_seconds =
97 if(timeout_seconds > 0)
104 log.
warning() <<
"cannot set solver time limit on "
110 solver->set_time_limit_seconds(timeout_seconds);
115 std::unique_ptr<decision_proceduret> p)
117 decision_procedure_ptr = std::move(p);
122 prop_ptr = std::move(p);
127 ofstream_ptr = std::move(p);
174 auto solver = util_make_unique<solvert>();
198 solver->set_decision_procedure(std::move(bv_pointers));
214 return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
219 std::unique_ptr<propt> prop = [
this]() -> std::unique_ptr<propt> {
231 info.
prop = prop.get();
243 auto decision_procedure = util_make_unique<bv_refinementt>(info);
245 return util_make_unique<solvert>(
246 std::move(decision_procedure), std::move(prop));
252 std::unique_ptr<solver_factoryt::solvert>
257 auto prop = util_make_unique<satcheck_no_simplifiert>(
message_handler);
258 info.
prop = prop.get();
268 auto decision_procedure = util_make_unique<string_refinementt>(info);
270 return util_make_unique<solvert>(
271 std::move(decision_procedure), std::move(prop));
274 std::unique_ptr<solver_factoryt::solvert>
286 "required filename not provided",
288 "provide a filename with --outfile");
291 auto smt2_dec = util_make_unique<smt2_dect>(
300 smt2_dec->use_FPA_theory =
true;
305 return util_make_unique<solvert>(std::move(smt2_dec));
307 else if(filename ==
"-")
309 auto smt2_conv = util_make_unique<smt2_convt>(
318 smt2_conv->use_FPA_theory =
true;
321 return util_make_unique<solvert>(std::move(smt2_conv));
326 auto out = util_make_unique<std::ofstream>(
widen(filename));
328 auto out = util_make_unique<std::ofstream>(filename);
334 "failed to open file: " + filename,
"--outfile");
337 auto smt2_conv = util_make_unique<smt2_convt>(
346 smt2_conv->use_FPA_theory =
true;
349 return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
358 "the chosen solver does not support beautification",
"--beautify");
366 const bool incremental_check =
options.
is_set(
"incremental-check");
371 "the chosen solver does not support incremental solving",
377 "the chosen solver does not support incremental solving",
"--cover");
379 else if(incremental_check)
382 "the chosen solver does not support incremental solving",
383 "--incremental-check");