cprover
solver_factory.cpp
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 #include "solver_factory.h"
13 
14 #include <iostream>
15 
16 #include <util/exception_utils.h>
17 #include <util/make_unique.h>
18 #include <util/message.h>
19 #include <util/options.h>
20 #include <util/version.h>
21 
22 #ifdef _MSC_VER
23 #include <util/unicode.h>
24 #endif
25 
27 
29 #include <solvers/prop/prop.h>
32 #include <solvers/sat/dimacs_cnf.h>
34 #include <solvers/sat/satcheck.h>
37 
39  const optionst &_options,
40  const namespacet &_ns,
41  message_handlert &_message_handler,
42  bool _output_xml_in_refinement)
43  : options(_options),
44  ns(_ns),
45  message_handler(_message_handler),
46  output_xml_in_refinement(_output_xml_in_refinement)
47 {
48 }
49 
50 solver_factoryt::solvert::solvert(std::unique_ptr<decision_proceduret> p)
51  : decision_procedure_ptr(std::move(p))
52 {
53 }
54 
56  std::unique_ptr<decision_proceduret> p1,
57  std::unique_ptr<propt> p2)
58  : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
59 {
60 }
61 
63  std::unique_ptr<decision_proceduret> p1,
64  std::unique_ptr<std::ofstream> p2)
65  : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
66 {
67 }
68 
70 {
71  PRECONDITION(decision_procedure_ptr != nullptr);
72  return *decision_procedure_ptr;
73 }
74 
77 {
78  PRECONDITION(decision_procedure_ptr != nullptr);
80  dynamic_cast<stack_decision_proceduret *>(&*decision_procedure_ptr);
81  INVARIANT(solver != nullptr, "stack decision procedure required");
82  return *solver;
83 }
84 
86 {
87  PRECONDITION(prop_ptr != nullptr);
88  return *prop_ptr;
89 }
90 
92  decision_proceduret &decision_procedure)
93 {
94  const int timeout_seconds =
95  options.get_signed_int_option("solver-time-limit");
96 
97  if(timeout_seconds > 0)
98  {
100  dynamic_cast<solver_resource_limitst *>(&decision_procedure);
101  if(solver == nullptr)
102  {
104  log.warning() << "cannot set solver time limit on "
105  << decision_procedure.decision_procedure_text()
106  << messaget::eom;
107  return;
108  }
109 
110  solver->set_time_limit_seconds(timeout_seconds);
111  }
112 }
113 
115  std::unique_ptr<decision_proceduret> p)
116 {
117  decision_procedure_ptr = std::move(p);
118 }
119 
120 void solver_factoryt::solvert::set_prop(std::unique_ptr<propt> p)
121 {
122  prop_ptr = std::move(p);
123 }
124 
125 void solver_factoryt::solvert::set_ofstream(std::unique_ptr<std::ofstream> p)
126 {
127  ofstream_ptr = std::move(p);
128 }
129 
130 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
131 {
132  if(options.get_bool_option("dimacs"))
133  return get_dimacs();
134  if(options.is_set("external-sat-solver"))
135  return get_external_sat();
136  if(
137  options.get_bool_option("refine") &&
138  !options.get_bool_option("refine-strings"))
139  {
140  return get_bv_refinement();
141  }
142  else if(options.get_bool_option("refine-strings"))
143  return get_string_refinement();
144  const auto incremental_smt2_solver =
145  options.get_option("incremental-smt2-solver");
146  if(!incremental_smt2_solver.empty())
147  return get_incremental_smt2(incremental_smt2_solver);
148  if(options.get_bool_option("smt2"))
149  return get_smt2(get_smt2_solver_type());
150  return get_default();
151 }
152 
156 {
157  // we shouldn't get here if this option isn't set
159 
161 
162  if(options.get_bool_option("boolector"))
164  else if(options.get_bool_option("cprover-smt2"))
166  else if(options.get_bool_option("mathsat"))
168  else if(options.get_bool_option("cvc3"))
170  else if(options.get_bool_option("cvc4"))
172  else if(options.get_bool_option("yices"))
174  else if(options.get_bool_option("z3"))
176  else if(options.get_bool_option("generic"))
178 
179  return s;
180 }
181 
182 template <typename SatcheckT>
183 static std::unique_ptr<SatcheckT>
185 {
186  auto satcheck = util_make_unique<SatcheckT>(message_handler);
187  if(options.is_set("write-solver-stats-to"))
188  {
189  if(
190  auto hardness_collector = dynamic_cast<hardness_collectort *>(&*satcheck))
191  {
192  hardness_collector->enable_hardness_collection();
193  hardness_collector->with_solver_hardness(
194  [&options](solver_hardnesst &hardness) {
195  hardness.set_outfile(options.get_option("write-solver-stats-to"));
196  });
197  }
198  else
199  {
201  log.warning()
202  << "Configured solver does not support --write-solver-stats-to. "
203  << "Solver stats will not be written." << messaget::eom;
204  }
205  }
206  return satcheck;
207 }
208 
209 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
210 {
211  auto solver = util_make_unique<solvert>();
212  if(
213  options.get_bool_option("beautify") ||
214  !options.get_bool_option("sat-preprocessor")) // no simplifier
215  {
216  // simplifier won't work with beautification
217  solver->set_prop(
218  make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options));
219  }
220  else // with simplifier
221  {
222  solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
223  }
224 
225  bool get_array_constraints =
226  options.get_bool_option("show-array-constraints");
227  auto bv_pointers = util_make_unique<bv_pointerst>(
228  ns, solver->prop(), message_handler, get_array_constraints);
229 
230  if(options.get_option("arrays-uf") == "never")
231  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
232  else if(options.get_option("arrays-uf") == "always")
233  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
234 
235  set_decision_procedure_time_limit(*bv_pointers);
236  solver->set_decision_procedure(std::move(bv_pointers));
237 
238  return solver;
239 }
240 
241 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
242 {
245 
246  auto prop = util_make_unique<dimacs_cnft>(message_handler);
247 
248  std::string filename = options.get_option("outfile");
249 
250  auto bv_dimacs =
251  util_make_unique<bv_dimacst>(ns, *prop, message_handler, filename);
252 
253  return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
254 }
255 
256 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
257 {
260 
261  std::string external_sat_solver = options.get_option("external-sat-solver");
262  auto prop =
263  util_make_unique<external_satt>(message_handler, external_sat_solver);
264 
265  auto bv_pointers = util_make_unique<bv_pointerst>(ns, *prop, message_handler);
266 
267  return util_make_unique<solvert>(std::move(bv_pointers), std::move(prop));
268 }
269 
270 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
271 {
272  std::unique_ptr<propt> prop = [this]() -> std::unique_ptr<propt> {
273  // We offer the option to disable the SAT preprocessor
274  if(options.get_bool_option("sat-preprocessor"))
275  {
277  return make_satcheck_prop<satcheckt>(message_handler, options);
278  }
279  return make_satcheck_prop<satcheck_no_simplifiert>(
281  }();
282 
284  info.ns = &ns;
285  info.prop = prop.get();
287 
288  // we allow setting some parameters
289  if(options.get_bool_option("max-node-refinement"))
290  info.max_node_refinement =
291  options.get_unsigned_int_option("max-node-refinement");
292 
293  info.refine_arrays = options.get_bool_option("refine-arrays");
294  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
296 
297  auto decision_procedure = util_make_unique<bv_refinementt>(info);
298  set_decision_procedure_time_limit(*decision_procedure);
299  return util_make_unique<solvert>(
300  std::move(decision_procedure), std::move(prop));
301 }
302 
306 std::unique_ptr<solver_factoryt::solvert>
308 {
310  info.ns = &ns;
311  auto prop =
312  make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options);
313  info.prop = prop.get();
316  if(options.get_bool_option("max-node-refinement"))
317  info.max_node_refinement =
318  options.get_unsigned_int_option("max-node-refinement");
319  info.refine_arrays = options.get_bool_option("refine-arrays");
320  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
322 
323  auto decision_procedure = util_make_unique<string_refinementt>(info);
324  set_decision_procedure_time_limit(*decision_procedure);
325  return util_make_unique<solvert>(
326  std::move(decision_procedure), std::move(prop));
327 }
328 
329 std::unique_ptr<solver_factoryt::solvert>
330 solver_factoryt::get_incremental_smt2(std::string solver_command)
331 {
333 
334  return util_make_unique<solvert>(
335  util_make_unique<smt2_incremental_decision_proceduret>(
336  std::move(solver_command)));
337 }
338 
339 std::unique_ptr<solver_factoryt::solvert>
341 {
343 
344  const std::string &filename = options.get_option("outfile");
345 
346  if(filename.empty())
347  {
349  {
351  "required filename not provided",
352  "--outfile",
353  "provide a filename with --outfile");
354  }
355 
356  auto smt2_dec = util_make_unique<smt2_dect>(
357  ns,
358  "cbmc",
359  std::string("Generated by CBMC ") + CBMC_VERSION,
360  "QF_AUFBV",
361  solver,
363 
364  if(options.get_bool_option("fpa"))
365  smt2_dec->use_FPA_theory = true;
366 
368  return util_make_unique<solvert>(std::move(smt2_dec));
369  }
370  else if(filename == "-")
371  {
372  auto smt2_conv = util_make_unique<smt2_convt>(
373  ns,
374  "cbmc",
375  std::string("Generated by CBMC ") + CBMC_VERSION,
376  "QF_AUFBV",
377  solver,
378  std::cout);
379 
380  if(options.get_bool_option("fpa"))
381  smt2_conv->use_FPA_theory = true;
382 
384  return util_make_unique<solvert>(std::move(smt2_conv));
385  }
386  else
387  {
388 #ifdef _MSC_VER
389  auto out = util_make_unique<std::ofstream>(widen(filename));
390 #else
391  auto out = util_make_unique<std::ofstream>(filename);
392 #endif
393 
394  if(!*out)
395  {
397  "failed to open file: " + filename, "--outfile");
398  }
399 
400  auto smt2_conv = util_make_unique<smt2_convt>(
401  ns,
402  "cbmc",
403  std::string("Generated by CBMC ") + CBMC_VERSION,
404  "QF_AUFBV",
405  solver,
406  *out);
407 
408  if(options.get_bool_option("fpa"))
409  smt2_conv->use_FPA_theory = true;
410 
412  return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
413  }
414 }
415 
417 {
418  if(options.get_bool_option("beautify"))
419  {
421  "the chosen solver does not support beautification", "--beautify");
422  }
423 }
424 
426 {
427  const bool all_properties = options.get_bool_option("all-properties");
428  const bool cover = options.is_set("cover");
429  const bool incremental_loop = options.is_set("incremental-loop");
430 
431  if(all_properties)
432  {
434  "the chosen solver does not support incremental solving",
435  "--all_properties");
436  }
437  else if(cover)
438  {
440  "the chosen solver does not support incremental solving", "--cover");
441  }
442  else if(incremental_loop)
443  {
445  "the chosen solver does not support incremental solving",
446  "--incremental-loop");
447  }
448 }
Writing DIMACS Files.
Abstraction Refinement Loop.
virtual std::string decision_procedure_text() const =0
Return a textual description of the decision procedure.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:56
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition: options.cpp:62
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
signed int get_signed_int_option(const std::string &option) const
Definition: options.cpp:50
TO_BE_DOCUMENTED.
Definition: prop.h:23
void set_decision_procedure(std::unique_ptr< decision_proceduret > p)
decision_proceduret & decision_procedure() const
stack_decision_proceduret & stack_decision_procedure() const
void set_ofstream(std::unique_ptr< std::ofstream > p)
void set_prop(std::unique_ptr< propt > p)
message_handlert & message_handler
const optionst & options
const namespacet & ns
std::unique_ptr< solvert > get_external_sat()
std::unique_ptr< solvert > get_default()
solver_factoryt(const optionst &_options, const namespacet &_ns, message_handlert &_message_handler, bool _output_xml_in_refinement)
Note: The solver returned will hold a reference to the namespace ns.
std::unique_ptr< solvert > get_dimacs()
void set_decision_procedure_time_limit(decision_proceduret &decision_procedure)
Sets the timeout of decision_procedure if the solver-time-limit option has a positive value (in secon...
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
const bool output_xml_in_refinement
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
std::unique_ptr< solvert > get_incremental_smt2(std::string solver_command)
std::unique_ptr< solvert > get_bv_refinement()
Allows calling an external SAT solver to allow faster integration of newer SAT solvers.
Options.
Decision procedure with incremental SMT2 solving.
int solver(std::istream &in)
static std::unique_ptr< SatcheckT > make_satcheck_prop(message_handlert &message_handler, const optionst &options)
Solver Factory.
Solver capability to set resource limits.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Decision procedure with incremental solving with contexts and assumptions.
String support via creating string constraints and progressively instantiating the universal constrai...
#define DEFAULT_MAX_NB_REFINEMENT
unsigned max_node_refinement
Max number of times we refine a formula node.
Definition: bv_refinement.h:26
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:28
bool refine_arithmetic
Enable arithmetic refinement.
Definition: bv_refinement.h:30
const namespacet * ns
Definition: bv_refinement.h:35
message_handlert * message_handler
Definition: bv_refinement.h:37
A structure that facilitates collecting the complexity statistics from a decision procedure.
void set_outfile(const std::string &file_name)
string_refinementt constructor arguments
std::wstring widen(const char *s)
Definition: unicode.cpp:48
const char * CBMC_VERSION