cprover
cbmc_solvers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Solvers for VCs Generated by Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "cbmc_solvers.h"
13 
14 #include <memory>
15 #include <iostream>
16 #include <fstream>
17 
18 #include <util/unicode.h>
19 
20 #include <solvers/sat/satcheck.h>
22 #include <solvers/smt1/smt1_dec.h>
23 #include <solvers/smt2/smt2_dec.h>
24 #include <solvers/cvc/cvc_dec.h>
25 #include <solvers/prop/aig_prop.h>
26 #include <solvers/sat/dimacs_cnf.h>
27 
28 #include "bv_cbmc.h"
29 #include "cbmc_dimacs.h"
31 #include "version.h"
32 
36 {
37  assert(options.get_bool_option("smt1"));
38 
39  smt1_dect::solvert s=smt1_dect::solvert::GENERIC;
40 
41  if(options.get_bool_option("boolector"))
42  s=smt1_dect::solvert::BOOLECTOR;
43  else if(options.get_bool_option("mathsat"))
44  s=smt1_dect::solvert::MATHSAT;
45  else if(options.get_bool_option("cvc3"))
46  s=smt1_dect::solvert::CVC3;
47  else if(options.get_bool_option("cvc4"))
48  s=smt1_dect::solvert::CVC4;
49  else if(options.get_bool_option("opensmt"))
50  s=smt1_dect::solvert::OPENSMT;
51  else if(options.get_bool_option("yices"))
52  s=smt1_dect::solvert::YICES;
53  else if(options.get_bool_option("z3"))
54  s=smt1_dect::solvert::Z3;
55  else if(options.get_bool_option("generic"))
56  s=smt1_dect::solvert::GENERIC;
57 
58  return s;
59 }
60 
64 {
65  assert(options.get_bool_option("smt2"));
66 
68 
69  if(options.get_bool_option("boolector"))
71  else if(options.get_bool_option("mathsat"))
73  else if(options.get_bool_option("cvc3"))
75  else if(options.get_bool_option("cvc4"))
77  else if(options.get_bool_option("opensmt"))
79  else if(options.get_bool_option("yices"))
81  else if(options.get_bool_option("z3"))
83  else if(options.get_bool_option("generic"))
85 
86  return s;
87 }
88 
91 {
92  solvert *solver=new solvert;
93 
94  if(options.get_bool_option("beautify") ||
95  !options.get_bool_option("sat-preprocessor")) // no simplifier
96  {
97  // simplifier won't work with beautification
98  solver->set_prop(new satcheck_no_simplifiert());
99  }
100  else // with simplifier
101  {
102  solver->set_prop(new satcheckt());
103  }
104 
106 
107  bv_cbmct *bv_cbmc=new bv_cbmct(ns, solver->prop());
108 
109  if(options.get_option("arrays-uf")=="never")
111  else if(options.get_option("arrays-uf")=="always")
113 
114  solver->set_prop_conv(bv_cbmc);
115 
116  return solver;
117 }
118 
120 {
123 
124  dimacs_cnft *prop=new dimacs_cnft();
126 
127  std::string filename=options.get_option("outfile");
128 
129  return new solvert(new cbmc_dimacst(ns, *prop, filename), prop);
130 }
131 
133 {
134  propt *prop;
135 
136  // We offer the option to disable the SAT preprocessor
137  if(options.get_bool_option("sat-preprocessor"))
138  {
140  prop=new satcheckt();
141  }
142  else
143  prop=new satcheck_no_simplifiert();
144 
146 
147  bv_refinementt *bv_refinement=new bv_refinementt(ns, *prop);
148  bv_refinement->set_ui(ui);
149 
150  // we allow setting some parameters
151  if(options.get_option("max-node-refinement")!="")
152  bv_refinement->max_node_refinement =
153  options.get_unsigned_int_option("max-node-refinement");
154 
155  bv_refinement->do_array_refinement =
156  options.get_bool_option("refine-arrays");
157  bv_refinement->do_arithmetic_refinement =
158  options.get_bool_option("refine-arithmetic");
159 
160  return new solvert(bv_refinement, prop);
161 }
162 
164 {
167 
168  const std::string &filename=options.get_option("outfile");
169 
170  if(filename=="")
171  {
172  if(solver==smt1_dect::solvert::GENERIC)
173  {
174  error() << "please use --outfile" << eom;
175  throw 0;
176  }
177 
178  smt1_dect *smt1_dec=
179  new smt1_dect(
180  ns,
181  "cbmc",
182  "Generated by CBMC " CBMC_VERSION,
183  "QF_AUFBV",
184  solver);
185 
186  return new solvert(smt1_dec);
187  }
188  else if(filename=="-")
189  {
190  smt1_convt *smt1_conv=
191  new smt1_convt(
192  ns,
193  "cbmc",
194  "Generated by CBMC " CBMC_VERSION,
195  "QF_AUFBV",
196  solver,
197  std::cout);
198 
200 
201  return new solvert(smt1_conv);
202  }
203  else
204  {
205  #ifdef _MSC_VER
206  std::ofstream *out=new std::ofstream(widen(filename));
207  #else
208  std::ofstream *out=new std::ofstream(filename);
209  #endif
210 
211  if(!out)
212  {
213  error() << "failed to open " << filename << eom;
214  throw 0;
215  }
216 
217  smt1_convt *smt1_conv=
218  new smt1_convt(
219  ns,
220  "cbmc",
221  "Generated by CBMC " CBMC_VERSION,
222  "QF_AUFBV",
223  solver,
224  *out);
225 
227 
228  return new solvert(smt1_conv, out);
229  }
230 }
231 
233 {
235 
236  const std::string &filename=options.get_option("outfile");
237 
238  if(filename=="")
239  {
240  if(solver==smt2_dect::solvert::GENERIC)
241  {
242  error() << "please use --outfile" << eom;
243  throw 0;
244  }
245 
246  smt2_dect *smt2_dec=
247  new smt2_dect(
248  ns,
249  "cbmc",
250  "Generated by CBMC " CBMC_VERSION,
251  "QF_AUFBV",
252  solver);
253 
254  if(options.get_bool_option("fpa"))
255  smt2_dec->use_FPA_theory=true;
256 
257  return new solvert(smt2_dec);
258  }
259  else if(filename=="-")
260  {
261  smt2_convt *smt2_conv=
262  new smt2_convt(
263  ns,
264  "cbmc",
265  "Generated by CBMC " CBMC_VERSION,
266  "QF_AUFBV",
267  solver,
268  std::cout);
269 
270  if(options.get_bool_option("fpa"))
271  smt2_conv->use_FPA_theory=true;
272 
274 
275  return new solvert(smt2_conv);
276  }
277  else
278  {
279  #ifdef _MSC_VER
280  std::ofstream *out=new std::ofstream(widen(filename));
281  #else
282  std::ofstream *out=new std::ofstream(filename);
283  #endif
284 
285  if(!*out)
286  {
287  error() << "failed to open " << filename << eom;
288  throw 0;
289  }
290 
291  smt2_convt *smt2_conv=
292  new smt2_convt(
293  ns,
294  "cbmc",
295  "Generated by CBMC " CBMC_VERSION,
296  "QF_AUFBV",
297  solver,
298  *out);
299 
300  if(options.get_bool_option("fpa"))
301  smt2_conv->use_FPA_theory=true;
302 
304 
305  return new solvert(smt2_conv, out);
306  }
307 }
308 
310 {
311  if(options.get_bool_option("beautify"))
312  {
313  error() << "sorry, this solver does not support beautification" << eom;
314  throw 0;
315  }
316 }
317 
319 {
320  if(options.get_bool_option("all-properties") ||
321  options.get_option("cover")!="" ||
322  options.get_option("incremental-check")!="")
323  {
324  error() << "sorry, this solver does not support incremental solving" << eom;
325  throw 0;
326  }
327 }
void set_prop_conv(prop_convt *p)
Definition: cbmc_solvers.h:84
propt & prop() const
Definition: cbmc_solvers.h:78
std::wstring widen(const char *s)
Definition: unicode.cpp:56
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:54
Writing DIMACS Files.
language_uit::uit ui
Definition: cbmc_solvers.h:136
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)
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void set_ui(language_uit::uit _ui)
Definition: bv_refinement.h:45
Decision procedure interface for various SMT 2.x solvers.
Definition: smt2_dec.h:35
smt1_dect::solvert get_smt1_solver_type() const
Uses the options to pick an SMT 1.2 solver.
const std::string get_option(const std::string &option) const
Definition: options.cpp:60
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
bool do_arithmetic_refinement
Definition: bv_refinement.h:41
void set_prop(propt *p)
Definition: cbmc_solvers.h:89
void no_incremental_check()
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
TO_BE_DOCUMENTED.
Definition: prop.h:22
namespacet ns
Definition: cbmc_solvers.h:133
Decision procedure interface for various SMT 1.x solvers.
Definition: smt1_dec.h:30
unsigned max_node_refinement
Definition: bv_refinement.h:38
const optionst & options
Definition: cbmc_solvers.h:131
bool do_array_refinement
Definition: bv_refinement.h:40
message_handlert & get_message_handler()
Definition: message.h:127
unbounded_arrayt unbounded_array
Definition: boolbv.h:76
satcheck_minisat_simplifiert satcheckt
Definition: satcheck.h:49
solvert * get_dimacs()
solvert * get_default()
Get the default decision procedure.
void no_beautification()
Bounded Model Checking for ANSI-C + HDL.
mstreamt & error()
Definition: message.h:223
#define CBMC_VERSION
Definition: version.h:4
satcheck_minisat_no_simplifiert satcheck_no_simplifiert
Definition: satcheck.h:50
Abstraction Refinement Loop.
solvert * get_smt1(smt1_dect::solvert solver)
bool use_FPA_theory
Definition: smt2_conv.h:104
Counterexample Beautification.