42 s=smt1_dect::solvert::BOOLECTOR;
44 s=smt1_dect::solvert::MATHSAT;
46 s=smt1_dect::solvert::CVC3;
48 s=smt1_dect::solvert::CVC4;
50 s=smt1_dect::solvert::OPENSMT;
52 s=smt1_dect::solvert::YICES;
54 s=smt1_dect::solvert::Z3;
56 s=smt1_dect::solvert::GENERIC;
160 return new solvert(bv_refinement, prop);
172 if(solver==smt1_dect::solvert::GENERIC)
174 error() <<
"please use --outfile" <<
eom;
188 else if(filename==
"-")
206 std::ofstream *out=
new std::ofstream(
widen(filename));
208 std::ofstream *out=
new std::ofstream(filename);
213 error() <<
"failed to open " << filename <<
eom;
228 return new solvert(smt1_conv, out);
242 error() <<
"please use --outfile" <<
eom;
259 else if(filename==
"-")
280 std::ofstream *out=
new std::ofstream(
widen(filename));
282 std::ofstream *out=
new std::ofstream(filename);
287 error() <<
"failed to open " << filename <<
eom;
305 return new solvert(smt2_conv, out);
313 error() <<
"sorry, this solver does not support beautification" <<
eom;
324 error() <<
"sorry, this solver does not support incremental solving" <<
eom;
void set_prop_conv(prop_convt *p)
std::wstring widen(const char *s)
unsigned int get_unsigned_int_option(const std::string &option) const
solvert * get_bv_refinement()
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
solvert * get_smt2(smt2_dect::solvert solver)
static mstreamt & eom(mstreamt &m)
void set_ui(language_uit::uit _ui)
Decision procedure interface for various SMT 2.x solvers.
smt1_dect::solvert get_smt1_solver_type() const
Uses the options to pick an SMT 1.2 solver.
const std::string get_option(const std::string &option) const
bool get_bool_option(const std::string &option) const
bool do_arithmetic_refinement
void no_incremental_check()
virtual void set_message_handler(message_handlert &_message_handler)
Decision procedure interface for various SMT 1.x solvers.
unsigned max_node_refinement
message_handlert & get_message_handler()
unbounded_arrayt unbounded_array
satcheck_minisat_simplifiert satcheckt
solvert * get_default()
Get the default decision procedure.
Bounded Model Checking for ANSI-C + HDL.
satcheck_minisat_no_simplifiert satcheck_no_simplifiert
Abstraction Refinement Loop.
solvert * get_smt1(smt1_dect::solvert solver)
Counterexample Beautification.