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 
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
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_smt2(smt2_dect::solvert solver);
79 
81 
85  void
87 
88  // consistency checks during solver creation
89  void no_beautification();
90  void no_incremental_check();
91 };
92 
93 #endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
solver_factoryt::solvert::set_decision_procedure
void set_decision_procedure(std::unique_ptr< decision_proceduret > p)
Definition: solver_factory.cpp:115
optionst
Definition: options.h:23
decision_proceduret
Definition: decision_procedure.h:21
solver_factoryt::get_dimacs
std::unique_ptr< solvert > get_dimacs()
Definition: solver_factory.cpp:224
solver_factoryt::solvert
Definition: solver_factory.h:39
solver_factoryt::set_decision_procedure_time_limit
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...
Definition: solver_factory.cpp:92
solver_factoryt::no_incremental_check
void no_incremental_check()
Definition: solver_factory.cpp:400
solver_factoryt::solvert::prop
propt & prop() const
Definition: solver_factory.cpp:86
stack_decision_proceduret
Definition: stack_decision_procedure.h:58
solver_factoryt
Definition: solver_factory.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
solver_factoryt::get_string_refinement
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
Definition: solver_factory.cpp:290
solver_factoryt::get_bv_refinement
std::unique_ptr< solvert > get_bv_refinement()
Definition: solver_factory.cpp:253
solver_factoryt::no_beautification
void no_beautification()
Definition: solver_factory.cpp:391
solver_factoryt::solvert::solvert
solvert()=default
solver_factoryt::~solver_factoryt
virtual ~solver_factoryt()=default
solver_factoryt::solvert::set_ofstream
void set_ofstream(std::unique_ptr< std::ofstream > p)
Definition: solver_factory.cpp:126
smt2_dec.h
solver_factoryt::message_handler
message_handlert & message_handler
Definition: solver_factory.h:70
message_handlert
Definition: message.h:28
solver_factoryt::solver_factoryt
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.
Definition: solver_factory.cpp:39
solver_factoryt::get_default
std::unique_ptr< solvert > get_default()
Definition: solver_factory.cpp:194
solver_factoryt::get_solver
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
Definition: solver_factory.cpp:131
solver_factoryt::solvert::stack_decision_procedure
stack_decision_proceduret & stack_decision_procedure() const
Definition: solver_factory.cpp:77
solver_factoryt::get_external_sat
std::unique_ptr< solvert > get_external_sat()
Definition: solver_factory.cpp:239
solver_factoryt::solvert::decision_procedure_ptr
std::unique_ptr< decision_proceduret > decision_procedure_ptr
Definition: solver_factory.h:59
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
solver_factoryt::solvert::set_prop
void set_prop(std::unique_ptr< propt > p)
Definition: solver_factory.cpp:121
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:364
solver_factoryt::solvert::ofstream_ptr
std::unique_ptr< std::ofstream > ofstream_ptr
Definition: solver_factory.h:57
solver_factoryt::options
const optionst & options
Definition: solver_factory.h:68
smt2_convt::solvert
solvert
Definition: smt2_conv.h:38
solver_factoryt::output_xml_in_refinement
const bool output_xml_in_refinement
Definition: solver_factory.h:71
solver_factoryt::solvert::prop_ptr
std::unique_ptr< propt > prop_ptr
Definition: solver_factory.h:58
solver_factoryt::ns
const namespacet & ns
Definition: solver_factory.h:69
solver_factoryt::solvert::decision_procedure
decision_proceduret & decision_procedure() const
Definition: solver_factory.cpp:70
solver_factoryt::get_smt2_solver_type
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
Definition: solver_factory.cpp:152
solver_factoryt::get_smt2
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
Definition: solver_factory.cpp:313