62 auto solver = util_make_unique<solvert>();
69 solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
73 solver->set_prop(util_make_unique<satcheckt>());
78 auto bv_pointers = util_make_unique<bv_pointerst>(
ns,
solver->prop());
85 solver->set_prop_conv(std::move(bv_pointers));
95 auto prop = util_make_unique<dimacs_cnft>();
100 auto bv_dimacs = util_make_unique<bv_dimacst>(
ns, *prop, filename);
101 return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
106 std::unique_ptr<propt> prop = [
this]() -> std::unique_ptr<propt> {
111 return util_make_unique<satcheckt>();
113 return util_make_unique<satcheck_no_simplifiert>();
120 info.
prop = prop.get();
131 return util_make_unique<solvert>(
132 util_make_unique<bv_refinementt>(info), std::move(prop));
138 std::unique_ptr<solver_factoryt::solvert>
143 auto prop = util_make_unique<satcheck_no_simplifiert>();
145 info.
prop = prop.get();
154 return util_make_unique<solvert>(
155 util_make_unique<string_refinementt>(info), std::move(prop));
158 std::unique_ptr<solver_factoryt::solvert>
170 "required filename not provided",
172 "provide a filename with --outfile");
175 auto smt2_dec = util_make_unique<smt2_dect>(
183 smt2_dec->use_FPA_theory =
true;
185 return util_make_unique<solvert>(std::move(smt2_dec));
187 else if(filename ==
"-")
189 auto smt2_conv = util_make_unique<smt2_convt>(
198 smt2_conv->use_FPA_theory =
true;
202 return util_make_unique<solvert>(std::move(smt2_conv));
207 auto out = util_make_unique<std::ofstream>(
widen(filename));
209 auto out = util_make_unique<std::ofstream>(filename);
215 "failed to open file: " + filename,
"--outfile");
218 auto smt2_conv = util_make_unique<smt2_convt>(
227 smt2_conv->use_FPA_theory =
true;
231 return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
240 "the chosen solver does not support beautification",
"--beautify");
248 const bool incremental_check =
options.
is_set(
"incremental-check");
253 "the chosen solver does not support incremental solving",
259 "the chosen solver does not support incremental solving",
"--cover");
261 else if(incremental_check)
264 "the chosen solver does not support incremental solving",
265 "--incremental-check");