cprover
cbmc_solvers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bounded Model Checking for ANSI-C + HDL
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CBMC_CBMC_SOLVERS_H
13 #define CPROVER_CBMC_CBMC_SOLVERS_H
14 
15 #include <list>
16 #include <map>
17 #include <memory>
18 
19 #include <util/options.h>
20 #include <util/ui_message.h>
21 
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>
28 
29 #include "bv_cbmc.h"
30 
31 class cbmc_solverst:public messaget
32 {
33 public:
35  const optionst &_options,
36  const symbol_tablet &_symbol_table,
37  message_handlert &_message_handler):
38  messaget(_message_handler),
39  options(_options),
40  symbol_table(_symbol_table),
41  ns(_symbol_table),
42  ui(ui_message_handlert::uit::PLAIN)
43  {
44  }
45 
46  // The solver class,
47  // which owns a variety of allocated objects.
48  class solvert
49  {
50  public:
52  {
53  }
54 
55  explicit solvert(std::unique_ptr<prop_convt> p):prop_conv_ptr(std::move(p))
56  {
57  }
58 
59  solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2):
60  prop_ptr(std::move(p2)),
61  prop_conv_ptr(std::move(p1))
62  {
63  }
64 
65  solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2):
66  ofstream_ptr(std::move(p2)),
67  prop_conv_ptr(std::move(p1))
68  {
69  }
70 
72  {
73  assert(prop_conv_ptr!=nullptr);
74  return *prop_conv_ptr;
75  }
76 
77  propt &prop() const
78  {
79  assert(prop_ptr!=nullptr);
80  return *prop_ptr;
81  }
82 
83  void set_prop_conv(std::unique_ptr<prop_convt> p)
84  {
85  prop_conv_ptr=std::move(p);
86  }
87 
88  void set_prop(std::unique_ptr<propt> p)
89  {
90  prop_ptr=std::move(p);
91  }
92 
93  void set_ofstream(std::unique_ptr<std::ofstream> p)
94  {
95  ofstream_ptr=std::move(p);
96  }
97 
98  // the objects are deleted in the opposite order they appear below
99  std::unique_ptr<std::ofstream> ofstream_ptr;
100  std::unique_ptr<propt> prop_ptr;
101  std::unique_ptr<prop_convt> prop_conv_ptr;
102  };
103 
104  // returns a solvert object
105  virtual std::unique_ptr<solvert> get_solver()
106  {
107  if(options.get_bool_option("dimacs"))
108  return get_dimacs();
109  if(options.get_bool_option("refine"))
110  return get_bv_refinement();
111  else if(options.get_bool_option("refine-strings"))
112  return get_string_refinement();
113  if(options.get_bool_option("smt2"))
114  return get_smt2(get_smt2_solver_type());
115  return get_default();
116  }
117 
118  virtual ~cbmc_solverst()
119  {
120  }
121 
122  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
123 
124 protected:
128 
129  // use gui format
131 
132  std::unique_ptr<solvert> get_default();
133  std::unique_ptr<solvert> get_dimacs();
134  std::unique_ptr<solvert> get_bv_refinement();
135  std::unique_ptr<solvert> get_string_refinement();
136  std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
137 
139 
140  // consistency checks during solver creation
141  void no_beautification();
142  void no_incremental_check();
143 };
144 
145 #endif // CPROVER_CBMC_CBMC_SOLVERS_H
CNF Generation, via Tseitin.
Generate Equation using Symbolic Execution.
propt & prop() const
Definition: cbmc_solvers.h:77
std::unique_ptr< propt > prop_ptr
Definition: cbmc_solvers.h:100
const symbol_tablet & symbol_table
Definition: cbmc_solvers.h:126
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
void set_ui(ui_message_handlert::uit _ui)
Definition: cbmc_solvers.h:122
solvert(std::unique_ptr< prop_convt > p1, std::unique_ptr< std::ofstream > p2)
Definition: cbmc_solvers.h:65
ui_message_handlert::uit ui
Definition: cbmc_solvers.h:130
prop_convt & prop_conv() const
Definition: cbmc_solvers.h:71
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
STL namespace.
std::unique_ptr< std::ofstream > ofstream_ptr
Definition: cbmc_solvers.h:99
void set_prop(std::unique_ptr< propt > p)
Definition: cbmc_solvers.h:88
virtual std::unique_ptr< solvert > get_solver()
Definition: cbmc_solvers.h:105
int solver(std::istream &in)
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
solvert(std::unique_ptr< prop_convt > p1, std::unique_ptr< propt > p2)
Definition: cbmc_solvers.h:59
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
void no_incremental_check()
void set_ofstream(std::unique_ptr< std::ofstream > p)
Definition: cbmc_solvers.h:93
TO_BE_DOCUMENTED.
Definition: prop.h:24
std::unique_ptr< prop_convt > prop_conv_ptr
Definition: cbmc_solvers.h:101
virtual ~cbmc_solverst()
Definition: cbmc_solvers.h:118
namespacet ns
Definition: cbmc_solvers.h:127
const optionst & options
Definition: cbmc_solvers.h:125
void set_prop_conv(std::unique_ptr< prop_convt > p)
Definition: cbmc_solvers.h:83
std::unique_ptr< solvert > get_default()
std::unique_ptr< solvert > get_dimacs()
std::unique_ptr< solvert > get_bv_refinement()
void no_beautification()
solvert(std::unique_ptr< prop_convt > p)
Definition: cbmc_solvers.h:55
Options.
cbmc_solverst(const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler)
Definition: cbmc_solvers.h:34