Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
13 #define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
34 bool _output_xml_in_refinement);
42 explicit solvert(std::unique_ptr<decision_proceduret> p);
43 solvert(std::unique_ptr<decision_proceduret> p1, std::unique_ptr<propt> p2);
45 std::unique_ptr<decision_proceduret> p1,
46 std::unique_ptr<std::ofstream> p2);
53 void set_prop(std::unique_ptr<propt> p);
93 #endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
void set_decision_procedure(std::unique_ptr< decision_proceduret > p)
std::unique_ptr< solvert > get_dimacs()
void set_decision_procedure_time_limit(decision_proceduret &decision_procedure)
Sets the timeout of decision_procedure if the solver-time-limit option has a positive value (in secon...
void no_incremental_check()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
std::unique_ptr< solvert > get_bv_refinement()
virtual ~solver_factoryt()=default
void set_ofstream(std::unique_ptr< std::ofstream > p)
message_handlert & message_handler
solver_factoryt(const optionst &_options, const namespacet &_ns, message_handlert &_message_handler, bool _output_xml_in_refinement)
Note: The solver returned will hold a reference to the namespace ns.
std::unique_ptr< solvert > get_default()
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
stack_decision_proceduret & stack_decision_procedure() const
std::unique_ptr< solvert > get_external_sat()
std::unique_ptr< decision_proceduret > decision_procedure_ptr
void set_prop(std::unique_ptr< propt > p)
int solver(std::istream &in)
std::unique_ptr< std::ofstream > ofstream_ptr
const bool output_xml_in_refinement
std::unique_ptr< propt > prop_ptr
decision_proceduret & decision_procedure() const
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)