cprover
solver_factory.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Solver Factory
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
13 #define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
14 
15 #include <memory>
16 
17 #include <solvers/smt2/smt2_dec.h>
18 
19 class message_handlert;
20 class namespacet;
21 class optionst;
22 class propt;
25 
26 class solver_factoryt final
27 {
28 public:
31  const optionst &_options,
32  const namespacet &_ns,
33  message_handlert &_message_handler,
34  bool _output_xml_in_refinement);
35 
36  // The solver class,
37  // which owns a variety of allocated objects.
38  class solvert final
39  {
40  public:
41  solvert() = default;
42  explicit solvert(std::unique_ptr<decision_proceduret> p);
43  solvert(std::unique_ptr<decision_proceduret> p1, std::unique_ptr<propt> p2);
44  solvert(
45  std::unique_ptr<decision_proceduret> p1,
46  std::unique_ptr<std::ofstream> p2);
47 
50  propt &prop() const;
51 
52  void set_decision_procedure(std::unique_ptr<decision_proceduret> p);
53  void set_prop(std::unique_ptr<propt> p);
54  void set_ofstream(std::unique_ptr<std::ofstream> p);
55 
56  // the objects are deleted in the opposite order they appear below
57  std::unique_ptr<std::ofstream> ofstream_ptr;
58  std::unique_ptr<propt> prop_ptr;
59  std::unique_ptr<decision_proceduret> decision_procedure_ptr;
60  };
61 
63  virtual std::unique_ptr<solvert> get_solver();
64 
65  virtual ~solver_factoryt() = default;
66 
67 protected:
68  const optionst &options;
69  const namespacet &ns;
72 
73  std::unique_ptr<solvert> get_default();
74  std::unique_ptr<solvert> get_dimacs();
75  std::unique_ptr<solvert> get_external_sat();
76  std::unique_ptr<solvert> get_bv_refinement();
77  std::unique_ptr<solvert> get_string_refinement();
78  std::unique_ptr<solvert> get_incremental_smt2(std::string solver_command);
79  std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
80 
82 
86  void
88 
89  // consistency checks during solver creation
90  void no_beautification();
91  void no_incremental_check();
92 };
93 
94 #endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
TO_BE_DOCUMENTED.
Definition: prop.h:23
std::unique_ptr< propt > prop_ptr
std::unique_ptr< decision_proceduret > decision_procedure_ptr
void set_decision_procedure(std::unique_ptr< decision_proceduret > p)
std::unique_ptr< std::ofstream > ofstream_ptr
decision_proceduret & decision_procedure() const
stack_decision_proceduret & stack_decision_procedure() const
void set_ofstream(std::unique_ptr< std::ofstream > p)
void set_prop(std::unique_ptr< propt > p)
message_handlert & message_handler
const optionst & options
const namespacet & ns
std::unique_ptr< solvert > get_external_sat()
std::unique_ptr< solvert > get_default()
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_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...
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_smt2(smt2_dect::solvert solver)
const bool output_xml_in_refinement
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
virtual ~solver_factoryt()=default
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
std::unique_ptr< solvert > get_incremental_smt2(std::string solver_command)
std::unique_ptr< solvert > get_bv_refinement()
int solver(std::istream &in)