12 #ifndef CPROVER_CBMC_CBMC_SOLVERS_H 13 #define CPROVER_CBMC_CBMC_SOLVERS_H 121 return std::unique_ptr<solvert>(solver);
152 #endif // CPROVER_CBMC_CBMC_SOLVERS_H CNF Generation, via Tseitin.
void set_prop_conv(prop_convt *p)
Generate Equation using Symbolic Execution.
std::unique_ptr< propt > prop_ptr
const symbol_tablet & symbol_table
solvert(prop_convt *p1, std::ofstream *p2)
prop_convt & prop_conv() 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)
std::unique_ptr< std::ofstream > ofstream_ptr
void set_ofstream(std::ofstream *p)
smt1_dect::solvert get_smt1_solver_type() const
Uses the options to pick an SMT 1.2 solver.
virtual std::unique_ptr< solvert > get_solver()
bool get_bool_option(const std::string &option) const
void no_incremental_check()
void set_ui(language_uit::uit _ui)
std::unique_ptr< prop_convt > prop_conv_ptr
solvert * get_default()
Get the default decision procedure.
solvert(prop_convt *p1, propt *p2)
solvert * get_smt1(smt1_dect::solvert solver)
cbmc_solverst(const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler)