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/prop/aig_prop.h>
27 #include <solvers/smt2/smt2_dec.h>
29 
30 #include "bv_cbmc.h"
31 
32 class cbmc_solverst:public messaget
33 {
34 public:
36  const optionst &_options,
37  const symbol_tablet &_symbol_table,
38  message_handlert &_message_handler):
39  messaget(_message_handler),
40  options(_options),
41  symbol_table(_symbol_table),
42  ns(_symbol_table),
43  ui(ui_message_handlert::uit::PLAIN)
44  {
45  }
46 
47  // The solver class,
48  // which owns a variety of allocated objects.
49  class solvert
50  {
51  public:
53  {
54  }
55 
56  explicit solvert(std::unique_ptr<prop_convt> p):prop_conv_ptr(std::move(p))
57  {
58  }
59 
60  solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2):
61  prop_ptr(std::move(p2)),
62  prop_conv_ptr(std::move(p1))
63  {
64  }
65 
66  solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2):
67  ofstream_ptr(std::move(p2)),
68  prop_conv_ptr(std::move(p1))
69  {
70  }
71 
73  {
74  assert(prop_conv_ptr!=nullptr);
75  return *prop_conv_ptr;
76  }
77 
78  propt &prop() const
79  {
80  assert(prop_ptr!=nullptr);
81  return *prop_ptr;
82  }
83 
84  void set_prop_conv(std::unique_ptr<prop_convt> p)
85  {
86  prop_conv_ptr=std::move(p);
87  }
88 
89  void set_prop(std::unique_ptr<propt> p)
90  {
91  prop_ptr=std::move(p);
92  }
93 
94  void set_ofstream(std::unique_ptr<std::ofstream> p)
95  {
96  ofstream_ptr=std::move(p);
97  }
98 
99  // the objects are deleted in the opposite order they appear below
100  std::unique_ptr<std::ofstream> ofstream_ptr;
101  std::unique_ptr<propt> prop_ptr;
102  std::unique_ptr<prop_convt> prop_conv_ptr;
103  };
104 
105  // returns a solvert object
106  virtual std::unique_ptr<solvert> get_solver()
107  {
108  if(options.get_bool_option("dimacs"))
109  return get_dimacs();
110  if(options.get_bool_option("refine"))
111  return get_bv_refinement();
112  else if(options.get_bool_option("refine-strings"))
113  return get_string_refinement();
114  if(options.get_bool_option("smt2"))
115  return get_smt2(get_smt2_solver_type());
116  return get_default();
117  }
118 
119  virtual ~cbmc_solverst()
120  {
121  }
122 
123  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
124 
125 protected:
129 
130  // use gui format
132 
133  std::unique_ptr<solvert> get_default();
134  std::unique_ptr<solvert> get_dimacs();
135  std::unique_ptr<solvert> get_bv_refinement();
136  std::unique_ptr<solvert> get_string_refinement();
137  std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
138 
140 
141  // consistency checks during solver creation
142  void no_beautification();
143  void no_incremental_check();
144 };
145 
146 #endif // CPROVER_CBMC_CBMC_SOLVERS_H
CNF Generation, via Tseitin.
Generate Equation using Symbolic Execution.
propt & prop() const
Definition: cbmc_solvers.h:78
std::unique_ptr< propt > prop_ptr
Definition: cbmc_solvers.h:101
const symbol_tablet & symbol_table
Definition: cbmc_solvers.h:127
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
void set_ui(ui_message_handlert::uit _ui)
Definition: cbmc_solvers.h:123
solvert(std::unique_ptr< prop_convt > p1, std::unique_ptr< std::ofstream > p2)
Definition: cbmc_solvers.h:66
ui_message_handlert::uit ui
Definition: cbmc_solvers.h:131
prop_convt & prop_conv() const
Definition: cbmc_solvers.h:72
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:100
void set_prop(std::unique_ptr< propt > p)
Definition: cbmc_solvers.h:89
virtual std::unique_ptr< solvert > get_solver()
Definition: cbmc_solvers.h:106
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:60
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:94
TO_BE_DOCUMENTED.
Definition: prop.h:24
std::unique_ptr< prop_convt > prop_conv_ptr
Definition: cbmc_solvers.h:102
virtual ~cbmc_solverst()
Definition: cbmc_solvers.h:119
namespacet ns
Definition: cbmc_solvers.h:128
const optionst & options
Definition: cbmc_solvers.h:126
void set_prop_conv(std::unique_ptr< prop_convt > p)
Definition: cbmc_solvers.h:84
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:56
Options.
cbmc_solverst(const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler)
Definition: cbmc_solvers.h:35