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 
21 #include <solvers/prop/prop.h>
22 #include <solvers/prop/prop_conv.h>
23 #include <solvers/sat/cnf.h>
24 #include <solvers/sat/satcheck.h>
25 #include <solvers/prop/aig_prop.h>
26 #include <solvers/smt1/smt1_dec.h>
27 #include <solvers/smt2/smt2_dec.h>
28 #include <langapi/language_ui.h>
30 
31 #include "bv_cbmc.h"
32 
33 class cbmc_solverst:public messaget
34 {
35 public:
37  const optionst &_options,
38  const symbol_tablet &_symbol_table,
39  message_handlert &_message_handler):
40  messaget(_message_handler),
41  options(_options),
42  symbol_table(_symbol_table),
43  ns(_symbol_table)
44  {
45  }
46 
47  // The solver class,
48  // which owns a variety of allocated objects.
49  class solvert
50  {
51  public:
53  {
54  }
55 
57  {
58  }
59 
61  prop_ptr(p2),
62  prop_conv_ptr(p1)
63  {
64  }
65 
66  solvert(prop_convt *p1, std::ofstream *p2):
67  ofstream_ptr(p2),
68  prop_conv_ptr(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 
85  {
86  prop_conv_ptr=std::unique_ptr<prop_convt>(p);
87  }
88 
89  void set_prop(propt *p)
90  {
91  prop_ptr=std::unique_ptr<propt>(p);
92  }
93 
94  void set_ofstream(std::ofstream *p)
95  {
96  ofstream_ptr=std::unique_ptr<std::ofstream>(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  solvert *solver;
109 
110  if(options.get_bool_option("dimacs"))
111  solver = get_dimacs();
112  else if(options.get_bool_option("refine"))
113  solver = get_bv_refinement();
114  else if(options.get_bool_option("smt1"))
115  solver = get_smt1(get_smt1_solver_type());
116  else if(options.get_bool_option("smt2"))
117  solver = get_smt2(get_smt2_solver_type());
118  else
119  solver = get_default();
120 
121  return std::unique_ptr<solvert>(solver);
122  }
123 
124  virtual ~cbmc_solverst()
125  {
126  }
127 
128  void set_ui(language_uit::uit _ui) { ui=_ui; }
129 
130 protected:
134 
135  // use gui format
137 
138  solvert *get_default();
139  solvert *get_dimacs();
143 
146 
147  // consistency checks during solver creation
148  void no_beautification();
149  void no_incremental_check();
150 };
151 
152 #endif // CPROVER_CBMC_CBMC_SOLVERS_H
CNF Generation, via Tseitin.
void set_prop_conv(prop_convt *p)
Definition: cbmc_solvers.h:84
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:132
language_uit::uit ui
Definition: cbmc_solvers.h:136
solvert(prop_convt *p1, std::ofstream *p2)
Definition: cbmc_solvers.h:66
prop_convt & prop_conv() const
Definition: cbmc_solvers.h:72
solvert * get_bv_refinement()
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
solvert * get_smt2(smt2_dect::solvert solver)
solvert(prop_convt *p)
Definition: cbmc_solvers.h:56
std::unique_ptr< std::ofstream > ofstream_ptr
Definition: cbmc_solvers.h:100
void set_ofstream(std::ofstream *p)
Definition: cbmc_solvers.h:94
smt1_dect::solvert get_smt1_solver_type() const
Uses the options to pick an SMT 1.2 solver.
virtual std::unique_ptr< solvert > get_solver()
Definition: cbmc_solvers.h:106
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
The symbol table.
Definition: symbol_table.h:52
void set_prop(propt *p)
Definition: cbmc_solvers.h:89
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void no_incremental_check()
void set_ui(language_uit::uit _ui)
Definition: cbmc_solvers.h:128
TO_BE_DOCUMENTED.
Definition: prop.h:22
std::unique_ptr< prop_convt > prop_conv_ptr
Definition: cbmc_solvers.h:102
virtual ~cbmc_solverst()
Definition: cbmc_solvers.h:124
namespacet ns
Definition: cbmc_solvers.h:133
const optionst & options
Definition: cbmc_solvers.h:131
solvert * get_dimacs()
solvert * get_default()
Get the default decision procedure.
void no_beautification()
solvert(prop_convt *p1, propt *p2)
Definition: cbmc_solvers.h:60
Options.
solvert * get_smt1(smt1_dect::solvert solver)
cbmc_solverst(const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler)
Definition: cbmc_solvers.h:36