60 auto solver=util_make_unique<solvert>();
66 solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
70 solver->set_prop(util_make_unique<satcheckt>());
75 auto bv_cbmc=util_make_unique<bv_cbmct>(
ns,
solver->prop());
82 solver->set_prop_conv(std::move(bv_cbmc));
92 auto prop=util_make_unique<dimacs_cnft>();
97 auto cbmc_dimacs=util_make_unique<cbmc_dimacst>(
ns, *prop, filename);
98 return util_make_unique<solvert>(std::move(cbmc_dimacs), std::move(prop));
103 std::unique_ptr<propt> prop=[
this]() -> std::unique_ptr<propt>
109 return util_make_unique<satcheckt>();
111 return util_make_unique<satcheck_no_simplifiert>();
118 info.
prop=prop.get();
129 return util_make_unique<solvert>(
130 util_make_unique<bv_refinementt>(info),
141 auto prop=util_make_unique<satcheck_no_simplifiert>();
143 info.
prop=prop.get();
156 return util_make_unique<solvert>(
157 util_make_unique<string_refinementt>(info), std::move(prop));
171 error() <<
"please use --outfile" <<
eom;
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);
214 error() <<
"failed to open " << filename <<
eom;
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));
239 error() <<
"sorry, this solver does not support beautification" <<
eom;
250 error() <<
"sorry, this solver does not support incremental solving" <<
eom;
bool trace
Concretize strings after solver is finished.
std::size_t max_string_length
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
std::wstring widen(const char *s)
unsigned int get_unsigned_int_option(const std::string &option) const
#define DEFAULT_MAX_NB_REFINEMENT
string_refinementt constructor arguments
ui_message_handlert::uit ui
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
static mstreamt & eom(mstreamt &m)
bool refine_arrays
Enable array refinement.
int solver(std::istream &in)
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.
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
void no_incremental_check()
ui_message_handlert::uit ui
virtual void set_message_handler(message_handlert &_message_handler)
String support via creating string constraints and progressively instantiating the universal constrai...
message_handlert & get_message_handler()
const char * CBMC_VERSION
std::unique_ptr< solvert > get_default()
std::unique_ptr< solvert > get_dimacs()
std::unique_ptr< solvert > get_bv_refinement()
bool refine_arithmetic
Enable arithmetic refinement.
Bounded Model Checking for ANSI-C + HDL.
std::size_t refinement_bound
Abstraction Refinement Loop.
Counterexample Beautification.