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  satcheck->enable_hardness_collection();
187  satcheck->with_solver_hardness([&options](solver_hardnesst &hardness) {
188  hardness.set_outfile(options.get_option("write-solver-stats-to"));
189  });
190  }
191  return satcheck;
192 }
193 
194 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
195 {
196  auto solver = util_make_unique<solvert>();
197  if(
198  options.get_bool_option("beautify") ||
199  !options.get_bool_option("sat-preprocessor")) // no simplifier
200  {
201  // simplifier won't work with beautification
202  solver->set_prop(
203  make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options));
204  }
205  else // with simplifier
206  {
207  solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
208  }
209 
210  auto bv_pointers =
211  util_make_unique<bv_pointerst>(ns, solver->prop(), message_handler);
212 
213  if(options.get_option("arrays-uf") == "never")
214  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
215  else if(options.get_option("arrays-uf") == "always")
216  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
217 
218  set_decision_procedure_time_limit(*bv_pointers);
219  solver->set_decision_procedure(std::move(bv_pointers));
220 
221  return solver;
222 }
223 
224 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
225 {
228 
229  auto prop = util_make_unique<dimacs_cnft>(message_handler);
230 
231  std::string filename = options.get_option("outfile");
232 
233  auto bv_dimacs =
234  util_make_unique<bv_dimacst>(ns, *prop, message_handler, filename);
235 
236  return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
237 }
238 
239 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
240 {
243 
244  std::string external_sat_solver = options.get_option("external-sat-solver");
245  auto prop =
246  util_make_unique<external_satt>(message_handler, external_sat_solver);
247 
248  auto bv_pointers = util_make_unique<bv_pointerst>(ns, *prop, message_handler);
249 
250  return util_make_unique<solvert>(std::move(bv_pointers), std::move(prop));
251 }
252 
253 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
254 {
255  std::unique_ptr<propt> prop = [this]() -> std::unique_ptr<propt> {
256  // We offer the option to disable the SAT preprocessor
257  if(options.get_bool_option("sat-preprocessor"))
258  {
260  return make_satcheck_prop<satcheckt>(message_handler, options);
261  }
262  return make_satcheck_prop<satcheck_no_simplifiert>(
264  }();
265 
267  info.ns = &ns;
268  info.prop = prop.get();
270 
271  // we allow setting some parameters
272  if(options.get_bool_option("max-node-refinement"))
273  info.max_node_refinement =
274  options.get_unsigned_int_option("max-node-refinement");
275 
276  info.refine_arrays = options.get_bool_option("refine-arrays");
277  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
279 
280  auto decision_procedure = util_make_unique<bv_refinementt>(info);
281  set_decision_procedure_time_limit(*decision_procedure);
282  return util_make_unique<solvert>(
283  std::move(decision_procedure), std::move(prop));
284 }
285 
289 std::unique_ptr<solver_factoryt::solvert>
291 {
293  info.ns = &ns;
294  auto prop =
295  make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options);
296  info.prop = prop.get();
299  if(options.get_bool_option("max-node-refinement"))
300  info.max_node_refinement =
301  options.get_unsigned_int_option("max-node-refinement");
302  info.refine_arrays = options.get_bool_option("refine-arrays");
303  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
305 
306  auto decision_procedure = util_make_unique<string_refinementt>(info);
307  set_decision_procedure_time_limit(*decision_procedure);
308  return util_make_unique<solvert>(
309  std::move(decision_procedure), std::move(prop));
310 }
311 
312 std::unique_ptr<solver_factoryt::solvert>
314 {
316 
317  const std::string &filename = options.get_option("outfile");
318 
319  if(filename.empty())
320  {
322  {
324  "required filename not provided",
325  "--outfile",
326  "provide a filename with --outfile");
327  }
328 
329  auto smt2_dec = util_make_unique<smt2_dect>(
330  ns,
331  "cbmc",
332  std::string("Generated by CBMC ") + CBMC_VERSION,
333  "QF_AUFBV",
334  solver);
335  smt2_dec->set_message_handler(message_handler);
336 
337  if(options.get_bool_option("fpa"))
338  smt2_dec->use_FPA_theory = true;
339 
340  smt2_dec->set_message_handler(message_handler);
341 
343  return util_make_unique<solvert>(std::move(smt2_dec));
344  }
345  else if(filename == "-")
346  {
347  auto smt2_conv = util_make_unique<smt2_convt>(
348  ns,
349  "cbmc",
350  std::string("Generated by CBMC ") + CBMC_VERSION,
351  "QF_AUFBV",
352  solver,
353  std::cout);
354 
355  if(options.get_bool_option("fpa"))
356  smt2_conv->use_FPA_theory = true;
357 
359  return util_make_unique<solvert>(std::move(smt2_conv));
360  }
361  else
362  {
363 #ifdef _MSC_VER
364  auto out = util_make_unique<std::ofstream>(widen(filename));
365 #else
366  auto out = util_make_unique<std::ofstream>(filename);
367 #endif
368 
369  if(!*out)
370  {
372  "failed to open file: " + filename, "--outfile");
373  }
374 
375  auto smt2_conv = util_make_unique<smt2_convt>(
376  ns,
377  "cbmc",
378  std::string("Generated by CBMC ") + CBMC_VERSION,
379  "QF_AUFBV",
380  solver,
381  *out);
382 
383  if(options.get_bool_option("fpa"))
384  smt2_conv->use_FPA_theory = true;
385 
387  return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
388  }
389 }
390 
392 {
393  if(options.get_bool_option("beautify"))
394  {
396  "the chosen solver does not support beautification", "--beautify");
397  }
398 }
399 
401 {
402  const bool all_properties = options.get_bool_option("all-properties");
403  const bool cover = options.is_set("cover");
404  const bool incremental_check = options.is_set("incremental-check");
405 
406  if(all_properties)
407  {
409  "the chosen solver does not support incremental solving",
410  "--all_properties");
411  }
412  else if(cover)
413  {
415  "the chosen solver does not support incremental solving", "--cover");
416  }
417  else if(incremental_check)
418  {
420  "the chosen solver does not support incremental solving",
421  "--incremental-check");
422  }
423 }
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:224
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:400
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:290
solver_factoryt::get_bv_refinement
std::unique_ptr< solvert > get_bv_refinement()
Definition: solver_factory.cpp:253
prop_conv.h
solver_factoryt::no_beautification
void no_beautification()
Definition: solver_factory.cpp:391
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:194
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:239
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:100
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:364
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
string_refinementt::infot
string_refinementt constructor arguments
Definition: string_refinement.h:80
smt2_convt::solvert
solvert
Definition: smt2_conv.h:38
solver_factoryt::output_xml_in_refinement
const bool output_xml_in_refinement
Definition: solver_factory.h:71
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.
validation_modet::INVARIANT
@ INVARIANT
solver_factoryt::get_smt2
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
Definition: solver_factory.cpp:313