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/namespace.h>
20 #include <util/options.h>
21 #include <util/version.h>
22 
23 #ifdef _MSC_VER
24 #include <util/unicode.h>
25 #endif
26 
28 
30 #include <solvers/prop/prop.h>
31 #include <solvers/prop/prop_conv.h>
34 #include <solvers/sat/dimacs_cnf.h>
36 #include <solvers/sat/satcheck.h>
38 
40  const optionst &_options,
41  const namespacet &_ns,
42  message_handlert &_message_handler,
43  bool _output_xml_in_refinement)
44  : options(_options),
45  ns(_ns),
46  message_handler(_message_handler),
47  output_xml_in_refinement(_output_xml_in_refinement)
48 {
49 }
50 
51 solver_factoryt::solvert::solvert(std::unique_ptr<decision_proceduret> p)
52  : decision_procedure_ptr(std::move(p))
53 {
54 }
55 
57  std::unique_ptr<decision_proceduret> p1,
58  std::unique_ptr<propt> p2)
59  : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
60 {
61 }
62 
64  std::unique_ptr<decision_proceduret> p1,
65  std::unique_ptr<std::ofstream> p2)
66  : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
67 {
68 }
69 
71 {
72  PRECONDITION(decision_procedure_ptr != nullptr);
73  return *decision_procedure_ptr;
74 }
75 
78 {
79  PRECONDITION(decision_procedure_ptr != nullptr);
81  dynamic_cast<stack_decision_proceduret *>(&*decision_procedure_ptr);
82  INVARIANT(solver != nullptr, "stack decision procedure required");
83  return *solver;
84 }
85 
87 {
88  PRECONDITION(prop_ptr != nullptr);
89  return *prop_ptr;
90 }
91 
93  decision_proceduret &decision_procedure)
94 {
95  const int timeout_seconds =
96  options.get_signed_int_option("solver-time-limit");
97 
98  if(timeout_seconds > 0)
99  {
101  dynamic_cast<solver_resource_limitst *>(&decision_procedure);
102  if(solver == nullptr)
103  {
105  log.warning() << "cannot set solver time limit on "
106  << decision_procedure.decision_procedure_text()
107  << messaget::eom;
108  return;
109  }
110 
111  solver->set_time_limit_seconds(timeout_seconds);
112  }
113 }
114 
116  std::unique_ptr<decision_proceduret> p)
117 {
118  decision_procedure_ptr = std::move(p);
119 }
120 
121 void solver_factoryt::solvert::set_prop(std::unique_ptr<propt> p)
122 {
123  prop_ptr = std::move(p);
124 }
125 
126 void solver_factoryt::solvert::set_ofstream(std::unique_ptr<std::ofstream> p)
127 {
128  ofstream_ptr = std::move(p);
129 }
130 
131 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
132 {
133  if(options.get_bool_option("dimacs"))
134  return get_dimacs();
135  if(options.is_set("external-sat-solver"))
136  return get_external_sat();
137  if(
138  options.get_bool_option("refine") &&
139  !options.get_bool_option("refine-strings"))
140  {
141  return get_bv_refinement();
142  }
143  else if(options.get_bool_option("refine-strings"))
144  return get_string_refinement();
145  if(options.get_bool_option("smt2"))
146  return get_smt2(get_smt2_solver_type());
147  return get_default();
148 }
149 
153 {
154  // we shouldn't get here if this option isn't set
156 
158 
159  if(options.get_bool_option("boolector"))
161  else if(options.get_bool_option("cprover-smt2"))
163  else if(options.get_bool_option("mathsat"))
165  else if(options.get_bool_option("cvc3"))
167  else if(options.get_bool_option("cvc4"))
169  else if(options.get_bool_option("yices"))
171  else if(options.get_bool_option("z3"))
173  else if(options.get_bool_option("generic"))
175 
176  return s;
177 }
178 
179 template <typename SatcheckT>
180 static std::unique_ptr<SatcheckT>
182 {
183  auto satcheck = util_make_unique<SatcheckT>(message_handler);
184  if(options.is_set("write-solver-stats-to"))
185  {
186  if(
187  auto hardness_collector = dynamic_cast<hardness_collectort *>(&*satcheck))
188  {
189  hardness_collector->enable_hardness_collection();
190  hardness_collector->with_solver_hardness(
191  [&options](solver_hardnesst &hardness) {
192  hardness.set_outfile(options.get_option("write-solver-stats-to"));
193  });
194  }
195  else
196  {
198  log.warning()
199  << "Configured solver does not support --write-solver-stats-to. "
200  << "Solver stats will not be written." << messaget::eom;
201  }
202  }
203  return satcheck;
204 }
205 
206 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
207 {
208  auto solver = util_make_unique<solvert>();
209  if(
210  options.get_bool_option("beautify") ||
211  !options.get_bool_option("sat-preprocessor")) // no simplifier
212  {
213  // simplifier won't work with beautification
214  solver->set_prop(
215  make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options));
216  }
217  else // with simplifier
218  {
219  solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
220  }
221 
222  bool get_array_constraints =
223  options.get_bool_option("show-array-constraints");
224  auto bv_pointers = util_make_unique<bv_pointerst>(
225  ns, solver->prop(), message_handler, get_array_constraints);
226 
227  if(options.get_option("arrays-uf") == "never")
228  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
229  else if(options.get_option("arrays-uf") == "always")
230  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
231 
232  set_decision_procedure_time_limit(*bv_pointers);
233  solver->set_decision_procedure(std::move(bv_pointers));
234 
235  return solver;
236 }
237 
238 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
239 {
242 
243  auto prop = util_make_unique<dimacs_cnft>(message_handler);
244 
245  std::string filename = options.get_option("outfile");
246 
247  auto bv_dimacs =
248  util_make_unique<bv_dimacst>(ns, *prop, message_handler, filename);
249 
250  return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
251 }
252 
253 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
254 {
257 
258  std::string external_sat_solver = options.get_option("external-sat-solver");
259  auto prop =
260  util_make_unique<external_satt>(message_handler, external_sat_solver);
261 
262  auto bv_pointers = util_make_unique<bv_pointerst>(ns, *prop, message_handler);
263 
264  return util_make_unique<solvert>(std::move(bv_pointers), std::move(prop));
265 }
266 
267 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
268 {
269  std::unique_ptr<propt> prop = [this]() -> std::unique_ptr<propt> {
270  // We offer the option to disable the SAT preprocessor
271  if(options.get_bool_option("sat-preprocessor"))
272  {
274  return make_satcheck_prop<satcheckt>(message_handler, options);
275  }
276  return make_satcheck_prop<satcheck_no_simplifiert>(
278  }();
279 
281  info.ns = &ns;
282  info.prop = prop.get();
284 
285  // we allow setting some parameters
286  if(options.get_bool_option("max-node-refinement"))
287  info.max_node_refinement =
288  options.get_unsigned_int_option("max-node-refinement");
289 
290  info.refine_arrays = options.get_bool_option("refine-arrays");
291  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
293 
294  auto decision_procedure = util_make_unique<bv_refinementt>(info);
295  set_decision_procedure_time_limit(*decision_procedure);
296  return util_make_unique<solvert>(
297  std::move(decision_procedure), std::move(prop));
298 }
299 
303 std::unique_ptr<solver_factoryt::solvert>
305 {
307  info.ns = &ns;
308  auto prop =
309  make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options);
310  info.prop = prop.get();
313  if(options.get_bool_option("max-node-refinement"))
314  info.max_node_refinement =
315  options.get_unsigned_int_option("max-node-refinement");
316  info.refine_arrays = options.get_bool_option("refine-arrays");
317  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
319 
320  auto decision_procedure = util_make_unique<string_refinementt>(info);
321  set_decision_procedure_time_limit(*decision_procedure);
322  return util_make_unique<solvert>(
323  std::move(decision_procedure), std::move(prop));
324 }
325 
326 std::unique_ptr<solver_factoryt::solvert>
328 {
330 
331  const std::string &filename = options.get_option("outfile");
332 
333  if(filename.empty())
334  {
336  {
338  "required filename not provided",
339  "--outfile",
340  "provide a filename with --outfile");
341  }
342 
343  auto smt2_dec = util_make_unique<smt2_dect>(
344  ns,
345  "cbmc",
346  std::string("Generated by CBMC ") + CBMC_VERSION,
347  "QF_AUFBV",
348  solver,
350 
351  if(options.get_bool_option("fpa"))
352  smt2_dec->use_FPA_theory = true;
353 
355  return util_make_unique<solvert>(std::move(smt2_dec));
356  }
357  else if(filename == "-")
358  {
359  auto smt2_conv = util_make_unique<smt2_convt>(
360  ns,
361  "cbmc",
362  std::string("Generated by CBMC ") + CBMC_VERSION,
363  "QF_AUFBV",
364  solver,
365  std::cout);
366 
367  if(options.get_bool_option("fpa"))
368  smt2_conv->use_FPA_theory = true;
369 
371  return util_make_unique<solvert>(std::move(smt2_conv));
372  }
373  else
374  {
375 #ifdef _MSC_VER
376  auto out = util_make_unique<std::ofstream>(widen(filename));
377 #else
378  auto out = util_make_unique<std::ofstream>(filename);
379 #endif
380 
381  if(!*out)
382  {
384  "failed to open file: " + filename, "--outfile");
385  }
386 
387  auto smt2_conv = util_make_unique<smt2_convt>(
388  ns,
389  "cbmc",
390  std::string("Generated by CBMC ") + CBMC_VERSION,
391  "QF_AUFBV",
392  solver,
393  *out);
394 
395  if(options.get_bool_option("fpa"))
396  smt2_conv->use_FPA_theory = true;
397 
399  return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
400  }
401 }
402 
404 {
405  if(options.get_bool_option("beautify"))
406  {
408  "the chosen solver does not support beautification", "--beautify");
409  }
410 }
411 
413 {
414  const bool all_properties = options.get_bool_option("all-properties");
415  const bool cover = options.is_set("cover");
416  const bool incremental_check = options.is_set("incremental-check");
417 
418  if(all_properties)
419  {
421  "the chosen solver does not support incremental solving",
422  "--all_properties");
423  }
424  else if(cover)
425  {
427  "the chosen solver does not support incremental solving", "--cover");
428  }
429  else if(incremental_check)
430  {
432  "the chosen solver does not support incremental solving",
433  "--incremental-check");
434  }
435 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
smt2_convt::solvert::CVC4
@ CVC4
exception_utils.h
bv_refinementt::configt::max_node_refinement
unsigned max_node_refinement
Max number of times we refine a formula node.
Definition: bv_refinement.h:26
bv_refinementt::configt::output_xml
bool output_xml
Definition: bv_refinement.h:24
smt2_convt::solvert::CPROVER_SMT2
@ CPROVER_SMT2
solver_factoryt::solvert::set_decision_procedure
void set_decision_procedure(std::unique_ptr< decision_proceduret > p)
Definition: solver_factory.cpp:115
optionst
Definition: options.h:23
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
decision_proceduret
Definition: decision_procedure.h:21
bv_refinementt::infot
Definition: bv_refinement.h:34
solver_factoryt::get_dimacs
std::unique_ptr< solvert > get_dimacs()
Definition: solver_factory.cpp:238
bv_refinement.h
Abstraction Refinement Loop.
string_refinementt::configt::refinement_bound
std::size_t refinement_bound
Definition: string_refinement.h:73
smt2_convt::solvert::MATHSAT
@ MATHSAT
bv_refinementt::configt::refine_arithmetic
bool refine_arithmetic
Enable arithmetic refinement.
Definition: bv_refinement.h:30
solver_factoryt::set_decision_procedure_time_limit
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...
Definition: solver_factory.cpp:92
solver_factoryt::no_incremental_check
void no_incremental_check()
Definition: solver_factory.cpp:412
DEFAULT_MAX_NB_REFINEMENT
#define DEFAULT_MAX_NB_REFINEMENT
Definition: string_refinement.h:66
options.h
Options.
messaget::eom
static eomt eom
Definition: message.h:297
solver_factoryt::solvert::prop
propt & prop() const
Definition: solver_factory.cpp:86
stack_decision_proceduret
Definition: stack_decision_procedure.h:58
version.h
namespace.h
smt2_convt::solvert::CVC3
@ CVC3
smt2_convt::solvert::BOOLECTOR
@ BOOLECTOR
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
stack_decision_procedure.h
Decision procedure with incremental solving with contexts and assumptions.
CBMC_VERSION
const char * CBMC_VERSION
make_unique.h
solver_factoryt::get_string_refinement
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
Definition: solver_factory.cpp:304
solver_factoryt::get_bv_refinement
std::unique_ptr< solvert > get_bv_refinement()
Definition: solver_factory.cpp:267
prop_conv.h
solver_factoryt::no_beautification
void no_beautification()
Definition: solver_factory.cpp:403
smt2_convt::solvert::YICES
@ YICES
solver_factoryt::solvert::solvert
solvert()=default
external_sat.h
Allows calling an external SAT solver to allow faster integration of newer SAT solvers.
optionst::is_set
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
bv_refinementt::infot::prop
propt * prop
Definition: bv_refinement.h:36
solver_factoryt::solvert::set_ofstream
void set_ofstream(std::unique_ptr< std::ofstream > p)
Definition: solver_factory.cpp:126
prop.h
bv_refinementt::infot::message_handler
message_handlert * message_handler
Definition: bv_refinement.h:37
solver_factoryt::message_handler
message_handlert & message_handler
Definition: solver_factory.h:70
optionst::get_signed_int_option
signed int get_signed_int_option(const std::string &option) const
Definition: options.cpp:50
message_handlert
Definition: message.h:28
string_refinement.h
String support via creating string constraints and progressively instantiating the universal constrai...
solver_factory.h
Solver Factory.
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:50
solver_factoryt::solver_factoryt
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.
Definition: solver_factory.cpp:39
solver_factoryt::get_default
std::unique_ptr< solvert > get_default()
Definition: solver_factory.cpp:206
optionst::get_unsigned_int_option
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:56
boolbvt::unbounded_arrayt::U_NONE
@ U_NONE
solver_resource_limits.h
Solver capability to set resource limits.
solver_factoryt::get_solver
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
Definition: solver_factory.cpp:131
solver_factoryt::solvert::stack_decision_procedure
stack_decision_proceduret & stack_decision_procedure() const
Definition: solver_factory.cpp:77
solver_factoryt::get_external_sat
std::unique_ptr< solvert > get_external_sat()
Definition: solver_factory.cpp:253
decision_proceduret::decision_procedure_text
virtual std::string decision_procedure_text() const =0
Return a textual description of the decision procedure.
satcheck.h
dimacs_cnf.h
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
solver_hardnesst::set_outfile
void set_outfile(const std::string &file_name)
Definition: solver_hardness.cpp:118
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition: solver_hardness.h:45
solver_factoryt::solvert::set_prop
void set_prop(std::unique_ptr< propt > p)
Definition: solver_factory.cpp:121
solver_resource_limitst
Definition: solver_resource_limits.h:16
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:368
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
boolbvt::unbounded_arrayt::U_ALL
@ U_ALL
solver_factoryt::options
const optionst & options
Definition: solver_factory.h:68
unicode.h
smt2_convt::solvert::GENERIC
@ GENERIC
make_satcheck_prop
static std::unique_ptr< SatcheckT > make_satcheck_prop(message_handlert &message_handler, const optionst &options)
Definition: solver_factory.cpp:181
smt2_convt::solvert::Z3
@ Z3
hardness_collectort
Definition: hardness_collector.h:23
string_refinementt::infot
string_refinementt constructor arguments
Definition: string_refinement.h:80
smt2_convt::solvert
solvert
Definition: smt2_conv.h:39
solver_factoryt::output_xml_in_refinement
const bool output_xml_in_refinement
Definition: solver_factory.h:71
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
bv_refinementt::infot::ns
const namespacet * ns
Definition: bv_refinement.h:35
message.h
messaget::warning
mstreamt & warning() const
Definition: message.h:404
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
solver_factoryt::ns
const namespacet & ns
Definition: solver_factory.h:69
solver_factoryt::solvert::decision_procedure
decision_proceduret & decision_procedure() const
Definition: solver_factory.cpp:70
bv_refinementt::configt::refine_arrays
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:28
solver_factoryt::get_smt2_solver_type
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
Definition: solver_factory.cpp:152
bv_dimacs.h
Writing DIMACS Files.
solver_factoryt::get_smt2
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
Definition: solver_factory.cpp:327