12 #ifndef CPROVER_CBMC_CBMC_SOLVERS_H 13 #define CPROVER_CBMC_CBMC_SOLVERS_H 59 solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2):
65 solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2):
145 #endif // CPROVER_CBMC_CBMC_SOLVERS_H CNF Generation, via Tseitin.
Generate Equation using Symbolic Execution.
std::unique_ptr< propt > prop_ptr
const symbol_tablet & symbol_table
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
void set_ui(ui_message_handlert::uit _ui)
solvert(std::unique_ptr< prop_convt > p1, std::unique_ptr< std::ofstream > p2)
ui_message_handlert::uit ui
prop_convt & prop_conv() const
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
std::unique_ptr< std::ofstream > ofstream_ptr
void set_prop(std::unique_ptr< propt > p)
virtual std::unique_ptr< solvert > get_solver()
int solver(std::istream &in)
bool get_bool_option(const std::string &option) const
solvert(std::unique_ptr< prop_convt > p1, std::unique_ptr< propt > p2)
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()
void set_ofstream(std::unique_ptr< std::ofstream > p)
std::unique_ptr< prop_convt > prop_conv_ptr
void set_prop_conv(std::unique_ptr< prop_convt > p)
std::unique_ptr< solvert > get_default()
std::unique_ptr< solvert > get_dimacs()
std::unique_ptr< solvert > get_bv_refinement()
solvert(std::unique_ptr< prop_convt > p)
cbmc_solverst(const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler)