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
CNF Generation, via Tseitin.
prop_convt & prop_conv() const
Generate Equation using Symbolic Execution.
message_handlert & message_handler
virtual ~solver_factoryt()
std::unique_ptr< propt > prop_ptr
std::unique_ptr< solvert > get_default()
solver_factoryt(const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler, bool _output_xml_in_refinement)
void set_prop(std::unique_ptr< propt > p)
STL namespace.
const optionst & options
void set_prop_conv(std::unique_ptr< prop_convt > p)
const symbol_tablet & symbol_table
const bool output_xml_in_refinement
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
int solver(std::istream &in)
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
solvert(std::unique_ptr< prop_convt > p1, std::unique_ptr< std::ofstream > p2)
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
The symbol table.
Definition: symbol_table.h:19
solvert(std::unique_ptr< prop_convt > p1, std::unique_ptr< propt > p2)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
TO_BE_DOCUMENTED.
Definition: prop.h:24
std::unique_ptr< solvert > get_dimacs()
std::unique_ptr< std::ofstream > ofstream_ptr
void set_ofstream(std::unique_ptr< std::ofstream > p)
std::unique_ptr< prop_convt > prop_conv_ptr
solvert(std::unique_ptr< prop_convt > p)
Options.
std::unique_ptr< solvert > get_bv_refinement()
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
virtual std::unique_ptr< solvert > get_solver()