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>
38 
40 
42  const optionst &_options,
43  const namespacet &_ns,
44  message_handlert &_message_handler,
45  bool _output_xml_in_refinement)
46  : options(_options),
47  ns(_ns),
48  message_handler(_message_handler),
49  output_xml_in_refinement(_output_xml_in_refinement)
50 {
51 }
52 
53 solver_factoryt::solvert::solvert(std::unique_ptr<decision_proceduret> p)
54  : decision_procedure_ptr(std::move(p))
55 {
56 }
57 
59  std::unique_ptr<decision_proceduret> p1,
60  std::unique_ptr<propt> p2)
61  : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
62 {
63 }
64 
66  std::unique_ptr<decision_proceduret> p1,
67  std::unique_ptr<std::ofstream> p2)
68  : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
69 {
70 }
71 
73 {
74  PRECONDITION(decision_procedure_ptr != nullptr);
75  return *decision_procedure_ptr;
76 }
77 
80 {
81  PRECONDITION(decision_procedure_ptr != nullptr);
83  dynamic_cast<stack_decision_proceduret *>(&*decision_procedure_ptr);
84  INVARIANT(solver != nullptr, "stack decision procedure required");
85  return *solver;
86 }
87 
89 {
90  PRECONDITION(prop_ptr != nullptr);
91  return *prop_ptr;
92 }
93 
95  decision_proceduret &decision_procedure)
96 {
97  const int timeout_seconds =
98  options.get_signed_int_option("solver-time-limit");
99 
100  if(timeout_seconds > 0)
101  {
103  dynamic_cast<solver_resource_limitst *>(&decision_procedure);
104  if(solver == nullptr)
105  {
107  log.warning() << "cannot set solver time limit on "
108  << decision_procedure.decision_procedure_text()
109  << messaget::eom;
110  return;
111  }
112 
113  solver->set_time_limit_seconds(timeout_seconds);
114  }
115 }
116 
118  std::unique_ptr<decision_proceduret> p)
119 {
120  decision_procedure_ptr = std::move(p);
121 }
122 
123 void solver_factoryt::solvert::set_prop(std::unique_ptr<propt> p)
124 {
125  prop_ptr = std::move(p);
126 }
127 
128 void solver_factoryt::solvert::set_ofstream(std::unique_ptr<std::ofstream> p)
129 {
130  ofstream_ptr = std::move(p);
131 }
132 
133 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
134 {
135  if(options.get_bool_option("dimacs"))
136  return get_dimacs();
137  if(options.is_set("external-sat-solver"))
138  return get_external_sat();
139  if(
140  options.get_bool_option("refine") &&
141  !options.get_bool_option("refine-strings"))
142  {
143  return get_bv_refinement();
144  }
145  else if(options.get_bool_option("refine-strings"))
146  return get_string_refinement();
147  const auto incremental_smt2_solver =
148  options.get_option("incremental-smt2-solver");
149  if(!incremental_smt2_solver.empty())
150  return get_incremental_smt2(incremental_smt2_solver);
151  if(options.get_bool_option("smt2"))
152  return get_smt2(get_smt2_solver_type());
153  return get_default();
154 }
155 
159 {
160  // we shouldn't get here if this option isn't set
162 
164 
165  if(options.get_bool_option("boolector"))
167  else if(options.get_bool_option("cprover-smt2"))
169  else if(options.get_bool_option("mathsat"))
171  else if(options.get_bool_option("cvc3"))
173  else if(options.get_bool_option("cvc4"))
175  else if(options.get_bool_option("yices"))
177  else if(options.get_bool_option("z3"))
179  else if(options.get_bool_option("generic"))
181 
182  return s;
183 }
184 
185 template <typename SatcheckT>
186 static std::unique_ptr<SatcheckT>
188 {
189  auto satcheck = util_make_unique<SatcheckT>(message_handler);
190  if(options.is_set("write-solver-stats-to"))
191  {
192  if(
193  auto hardness_collector = dynamic_cast<hardness_collectort *>(&*satcheck))
194  {
195  std::unique_ptr<solver_hardnesst> solver_hardness =
196  util_make_unique<solver_hardnesst>();
197  solver_hardness->set_outfile(options.get_option("write-solver-stats-to"));
198  hardness_collector->solver_hardness = std::move(solver_hardness);
199  }
200  else
201  {
203  log.warning()
204  << "Configured solver does not support --write-solver-stats-to. "
205  << "Solver stats will not be written." << messaget::eom;
206  }
207  }
208  return satcheck;
209 }
210 
211 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
212 {
213  auto solver = util_make_unique<solvert>();
214  if(
215  options.get_bool_option("beautify") ||
216  !options.get_bool_option("sat-preprocessor")) // no simplifier
217  {
218  // simplifier won't work with beautification
219  solver->set_prop(
220  make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options));
221  }
222  else // with simplifier
223  {
224  solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
225  }
226 
227  bool get_array_constraints =
228  options.get_bool_option("show-array-constraints");
229  auto bv_pointers = util_make_unique<bv_pointerst>(
230  ns, solver->prop(), message_handler, get_array_constraints);
231 
232  if(options.get_option("arrays-uf") == "never")
233  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
234  else if(options.get_option("arrays-uf") == "always")
235  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
236 
237  set_decision_procedure_time_limit(*bv_pointers);
238  solver->set_decision_procedure(std::move(bv_pointers));
239 
240  return solver;
241 }
242 
243 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
244 {
247 
248  auto prop = util_make_unique<dimacs_cnft>(message_handler);
249 
250  std::string filename = options.get_option("outfile");
251 
252  auto bv_dimacs =
253  util_make_unique<bv_dimacst>(ns, *prop, message_handler, filename);
254 
255  return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
256 }
257 
258 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
259 {
262 
263  std::string external_sat_solver = options.get_option("external-sat-solver");
264  auto prop =
265  util_make_unique<external_satt>(message_handler, external_sat_solver);
266 
267  auto bv_pointers = util_make_unique<bv_pointerst>(ns, *prop, message_handler);
268 
269  return util_make_unique<solvert>(std::move(bv_pointers), std::move(prop));
270 }
271 
272 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
273 {
274  std::unique_ptr<propt> prop = [this]() -> std::unique_ptr<propt> {
275  // We offer the option to disable the SAT preprocessor
276  if(options.get_bool_option("sat-preprocessor"))
277  {
279  return make_satcheck_prop<satcheckt>(message_handler, options);
280  }
281  return make_satcheck_prop<satcheck_no_simplifiert>(
283  }();
284 
286  info.ns = &ns;
287  info.prop = prop.get();
289 
290  // we allow setting some parameters
291  if(options.get_bool_option("max-node-refinement"))
292  info.max_node_refinement =
293  options.get_unsigned_int_option("max-node-refinement");
294 
295  info.refine_arrays = options.get_bool_option("refine-arrays");
296  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
298 
299  auto decision_procedure = util_make_unique<bv_refinementt>(info);
300  set_decision_procedure_time_limit(*decision_procedure);
301  return util_make_unique<solvert>(
302  std::move(decision_procedure), std::move(prop));
303 }
304 
308 std::unique_ptr<solver_factoryt::solvert>
310 {
312  info.ns = &ns;
313  auto prop =
314  make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options);
315  info.prop = prop.get();
318  if(options.get_bool_option("max-node-refinement"))
319  info.max_node_refinement =
320  options.get_unsigned_int_option("max-node-refinement");
321  info.refine_arrays = options.get_bool_option("refine-arrays");
322  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
324 
325  auto decision_procedure = util_make_unique<string_refinementt>(info);
326  set_decision_procedure_time_limit(*decision_procedure);
327  return util_make_unique<solvert>(
328  std::move(decision_procedure), std::move(prop));
329 }
330 
331 std::unique_ptr<solver_factoryt::solvert>
332 solver_factoryt::get_incremental_smt2(std::string solver_command)
333 {
335  auto solver_process = util_make_unique<smt_piped_solver_processt>(
336  std::move(solver_command), message_handler);
337 
338  return util_make_unique<solvert>(
339  util_make_unique<smt2_incremental_decision_proceduret>(
340  ns, std::move(solver_process), message_handler));
341 }
342 
343 std::unique_ptr<solver_factoryt::solvert>
345 {
347 
348  const std::string &filename = options.get_option("outfile");
349 
350  if(filename.empty())
351  {
353  {
355  "required filename not provided",
356  "--outfile",
357  "provide a filename with --outfile");
358  }
359 
360  auto smt2_dec = util_make_unique<smt2_dect>(
361  ns,
362  "cbmc",
363  std::string("Generated by CBMC ") + CBMC_VERSION,
364  "QF_AUFBV",
365  solver,
367 
368  if(options.get_bool_option("fpa"))
369  smt2_dec->use_FPA_theory = true;
370 
372  return util_make_unique<solvert>(std::move(smt2_dec));
373  }
374  else if(filename == "-")
375  {
376  auto smt2_conv = util_make_unique<smt2_convt>(
377  ns,
378  "cbmc",
379  std::string("Generated by CBMC ") + CBMC_VERSION,
380  "QF_AUFBV",
381  solver,
382  std::cout);
383 
384  if(options.get_bool_option("fpa"))
385  smt2_conv->use_FPA_theory = true;
386 
388  return util_make_unique<solvert>(std::move(smt2_conv));
389  }
390  else
391  {
392 #ifdef _MSC_VER
393  auto out = util_make_unique<std::ofstream>(widen(filename));
394 #else
395  auto out = util_make_unique<std::ofstream>(filename);
396 #endif
397 
398  if(!*out)
399  {
401  "failed to open file: " + filename, "--outfile");
402  }
403 
404  auto smt2_conv = util_make_unique<smt2_convt>(
405  ns,
406  "cbmc",
407  std::string("Generated by CBMC ") + CBMC_VERSION,
408  "QF_AUFBV",
409  solver,
410  *out);
411 
412  if(options.get_bool_option("fpa"))
413  smt2_conv->use_FPA_theory = true;
414 
416  return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
417  }
418 }
419 
421 {
422  if(options.get_bool_option("beautify"))
423  {
425  "the chosen solver does not support beautification", "--beautify");
426  }
427 }
428 
430 {
431  const bool all_properties = options.get_bool_option("all-properties");
432  const bool cover = options.is_set("cover");
433  const bool incremental_loop = options.is_set("incremental-loop");
434 
435  if(all_properties)
436  {
438  "the chosen solver does not support incremental solving",
439  "--all_properties");
440  }
441  else if(cover)
442  {
444  "the chosen solver does not support incremental solving", "--cover");
445  }
446  else if(incremental_loop)
447  {
449  "the chosen solver does not support incremental solving",
450  "--incremental-loop");
451  }
452 }
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
string_refinementt constructor arguments
std::wstring widen(const char *s)
Definition: unicode.cpp:48
const char * CBMC_VERSION