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 <list>
16 #include <map>
17 #include <memory>
18 
19 #include <util/options.h>
20 
22 #include <solvers/prop/prop.h>
23 #include <solvers/prop/prop_conv.h>
24 #include <solvers/sat/cnf.h>
25 #include <solvers/sat/satcheck.h>
26 #include <solvers/smt2/smt2_dec.h>
27 
29 {
30 public:
32  const optionst &_options,
33  const symbol_tablet &_symbol_table,
34  message_handlert &_message_handler,
35  bool _output_xml_in_refinement)
36  : options(_options),
37  symbol_table(_symbol_table),
38  ns(_symbol_table),
39  message_handler(_message_handler),
40  output_xml_in_refinement(_output_xml_in_refinement)
41  {
42  }
43 
44  // The solver class,
45  // which owns a variety of allocated objects.
46  class solvert
47  {
48  public:
50  {
51  }
52 
53  explicit solvert(std::unique_ptr<prop_convt> p)
54  : prop_conv_ptr(std::move(p))
55  {
56  }
57 
58  solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2)
59  : prop_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
60  {
61  }
62 
63  solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2)
64  : ofstream_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
65  {
66  }
67 
69  {
70  PRECONDITION(prop_conv_ptr != nullptr);
71  return *prop_conv_ptr;
72  }
73 
74  propt &prop() const
75  {
76  PRECONDITION(prop_ptr != nullptr);
77  return *prop_ptr;
78  }
79 
80  void set_prop_conv(std::unique_ptr<prop_convt> p)
81  {
82  prop_conv_ptr = std::move(p);
83  }
84 
85  void set_prop(std::unique_ptr<propt> p)
86  {
87  prop_ptr = std::move(p);
88  }
89 
90  void set_ofstream(std::unique_ptr<std::ofstream> p)
91  {
92  ofstream_ptr = std::move(p);
93  }
94 
95  // the objects are deleted in the opposite order they appear below
96  std::unique_ptr<std::ofstream> ofstream_ptr;
97  std::unique_ptr<propt> prop_ptr;
98  std::unique_ptr<prop_convt> prop_conv_ptr;
99  };
100 
101  // returns a solvert object
102  virtual std::unique_ptr<solvert> get_solver()
103  {
104  if(options.get_bool_option("dimacs"))
105  return get_dimacs();
106  if(options.get_bool_option("refine"))
107  return get_bv_refinement();
108  else if(options.get_bool_option("refine-strings"))
109  return get_string_refinement();
110  if(options.get_bool_option("smt2"))
111  return get_smt2(get_smt2_solver_type());
112  return get_default();
113  }
114 
116  {
117  }
118 
119 protected:
125 
126  std::unique_ptr<solvert> get_default();
127  std::unique_ptr<solvert> get_dimacs();
128  std::unique_ptr<solvert> get_bv_refinement();
129  std::unique_ptr<solvert> get_string_refinement();
130  std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
131 
133 
134  // consistency checks during solver creation
135  void no_beautification();
136  void no_incremental_check();
137 };
138 
139 #endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
symex_target_equation.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
solver_factoryt::solvert::solvert
solvert(std::unique_ptr< prop_convt > p1, std::unique_ptr< propt > p2)
Definition: solver_factory.h:58
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
solver_factoryt::solvert::solvert
solvert()
Definition: solver_factory.h:49
optionst
Definition: options.h:22
prop_convt
Definition: prop_conv.h:27
solver_factoryt::solvert::solvert
solvert(std::unique_ptr< prop_convt > p)
Definition: solver_factory.h:53
solver_factoryt::get_dimacs
std::unique_ptr< solvert > get_dimacs()
Definition: solver_factory.cpp:90
solver_factoryt::solvert
Definition: solver_factory.h:46
solver_factoryt::no_incremental_check
void no_incremental_check()
Definition: solver_factory.cpp:244
options.h
solver_factoryt
Definition: solver_factory.h:28
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
solver_factoryt::get_solver
virtual std::unique_ptr< solvert > get_solver()
Definition: solver_factory.h:102
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:139
solver_factoryt::get_bv_refinement
std::unique_ptr< solvert > get_bv_refinement()
Definition: solver_factory.cpp:104
prop_conv.h
solver_factoryt::no_beautification
void no_beautification()
Definition: solver_factory.cpp:235
solver_factoryt::solvert::set_ofstream
void set_ofstream(std::unique_ptr< std::ofstream > p)
Definition: solver_factory.h:90
solver_factoryt::solvert::set_prop_conv
void set_prop_conv(std::unique_ptr< prop_convt > p)
Definition: solver_factory.h:80
prop.h
smt2_dec.h
solver_factoryt::message_handler
message_handlert & message_handler
Definition: solver_factory.h:123
message_handlert
Definition: message.h:24
solver_factoryt::~solver_factoryt
virtual ~solver_factoryt()
Definition: solver_factory.h:115
solver_factoryt::get_default
std::unique_ptr< solvert > get_default()
Definition: solver_factory.cpp:60
satcheck.h
solver_factoryt::ns
namespacet ns
Definition: solver_factory.h:122
propt
TO_BE_DOCUMENTED.
Definition: prop.h:24
solver_factoryt::solver_factoryt
solver_factoryt(const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler, bool _output_xml_in_refinement)
Definition: solver_factory.h:31
solver_factoryt::solvert::set_prop
void set_prop(std::unique_ptr< propt > p)
Definition: solver_factory.h:85
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:360
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
solver_factoryt::solvert::ofstream_ptr
std::unique_ptr< std::ofstream > ofstream_ptr
Definition: solver_factory.h:96
solver_factoryt::solvert::solvert
solvert(std::unique_ptr< prop_convt > p1, std::unique_ptr< std::ofstream > p2)
Definition: solver_factory.h:63
solver_factoryt::solvert::prop
propt & prop() const
Definition: solver_factory.h:74
solver_factoryt::options
const optionst & options
Definition: solver_factory.h:120
solver_factoryt::symbol_table
const symbol_tablet & symbol_table
Definition: solver_factory.h:121
solver_factoryt::solvert::prop_conv_ptr
std::unique_ptr< prop_convt > prop_conv_ptr
Definition: solver_factory.h:98
smt2_convt::solvert
solvert
Definition: smt2_conv.h:35
solver_factoryt::output_xml_in_refinement
const bool output_xml_in_refinement
Definition: solver_factory.h:124
solver_factoryt::solvert::prop_ptr
std::unique_ptr< propt > prop_ptr
Definition: solver_factory.h:97
cnf.h
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:33
solver_factoryt::solvert::prop_conv
prop_convt & prop_conv() const
Definition: solver_factory.h:68
solver_factoryt::get_smt2
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
Definition: solver_factory.cpp:159