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");
std::wstring widen(const char *s)
message_handlert & message_handler
unsigned int get_unsigned_int_option(const std::string &option) const
#define DEFAULT_MAX_NB_REFINEMENT
std::unique_ptr< solvert > get_default()
string_refinementt constructor arguments
const bool output_xml_in_refinement
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
bool refine_arrays
Enable array refinement.
int solver(std::istream &in)
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
const std::string get_option(const std::string &option) const
bool get_bool_option(const std::string &option) const
unsigned max_node_refinement
Max number of times we refine a formula node.
#define PRECONDITION(CONDITION)
virtual void set_message_handler(message_handlert &_message_handler)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
std::unique_ptr< solvert > get_dimacs()
String support via creating string constraints and progressively instantiating the universal constrai...
void no_incremental_check()
const char * CBMC_VERSION
bool refine_arithmetic
Enable arithmetic refinement.
std::size_t refinement_bound
Abstraction Refinement Loop.
std::unique_ptr< solvert > get_bv_refinement()
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")