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>
35 #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.get_bool_option("refine"))
135  return get_bv_refinement();
136  else if(options.get_bool_option("refine-strings"))
137  return get_string_refinement();
138  if(options.get_bool_option("smt2"))
139  return get_smt2(get_smt2_solver_type());
140  return get_default();
141 }
142 
146 {
147  // we shouldn't get here if this option isn't set
149 
151 
152  if(options.get_bool_option("boolector"))
154  else if(options.get_bool_option("cprover-smt2"))
156  else if(options.get_bool_option("mathsat"))
158  else if(options.get_bool_option("cvc3"))
160  else if(options.get_bool_option("cvc4"))
162  else if(options.get_bool_option("yices"))
164  else if(options.get_bool_option("z3"))
166  else if(options.get_bool_option("generic"))
168 
169  return s;
170 }
171 
172 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
173 {
174  auto solver = util_make_unique<solvert>();
175 
176  if(
177  options.get_bool_option("beautify") ||
178  !options.get_bool_option("sat-preprocessor")) // no simplifier
179  {
180  // simplifier won't work with beautification
181  solver->set_prop(
182  util_make_unique<satcheck_no_simplifiert>(message_handler));
183  }
184  else // with simplifier
185  {
186  solver->set_prop(util_make_unique<satcheckt>(message_handler));
187  }
188 
189  auto bv_pointers =
190  util_make_unique<bv_pointerst>(ns, solver->prop(), message_handler);
191 
192  if(options.get_option("arrays-uf") == "never")
193  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
194  else if(options.get_option("arrays-uf") == "always")
195  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
196 
197  set_decision_procedure_time_limit(*bv_pointers);
198  solver->set_decision_procedure(std::move(bv_pointers));
199 
200  return solver;
201 }
202 
203 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
204 {
207 
208  auto prop = util_make_unique<dimacs_cnft>(message_handler);
209 
210  std::string filename = options.get_option("outfile");
211 
212  auto bv_dimacs =
213  util_make_unique<bv_dimacst>(ns, *prop, message_handler, filename);
214  return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
215 }
216 
217 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
218 {
219  std::unique_ptr<propt> prop = [this]() -> std::unique_ptr<propt> {
220  // We offer the option to disable the SAT preprocessor
221  if(options.get_bool_option("sat-preprocessor"))
222  {
224  return util_make_unique<satcheckt>(message_handler);
225  }
226  return util_make_unique<satcheck_no_simplifiert>(message_handler);
227  }();
228 
230  info.ns = &ns;
231  info.prop = prop.get();
233 
234  // we allow setting some parameters
235  if(options.get_bool_option("max-node-refinement"))
236  info.max_node_refinement =
237  options.get_unsigned_int_option("max-node-refinement");
238 
239  info.refine_arrays = options.get_bool_option("refine-arrays");
240  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
242 
243  auto decision_procedure = util_make_unique<bv_refinementt>(info);
244  set_decision_procedure_time_limit(*decision_procedure);
245  return util_make_unique<solvert>(
246  std::move(decision_procedure), std::move(prop));
247 }
248 
252 std::unique_ptr<solver_factoryt::solvert>
254 {
256  info.ns = &ns;
257  auto prop = util_make_unique<satcheck_no_simplifiert>(message_handler);
258  info.prop = prop.get();
261  if(options.get_bool_option("max-node-refinement"))
262  info.max_node_refinement =
263  options.get_unsigned_int_option("max-node-refinement");
264  info.refine_arrays = options.get_bool_option("refine-arrays");
265  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
267 
268  auto decision_procedure = util_make_unique<string_refinementt>(info);
269  set_decision_procedure_time_limit(*decision_procedure);
270  return util_make_unique<solvert>(
271  std::move(decision_procedure), std::move(prop));
272 }
273 
274 std::unique_ptr<solver_factoryt::solvert>
276 {
278 
279  const std::string &filename = options.get_option("outfile");
280 
281  if(filename.empty())
282  {
284  {
286  "required filename not provided",
287  "--outfile",
288  "provide a filename with --outfile");
289  }
290 
291  auto smt2_dec = util_make_unique<smt2_dect>(
292  ns,
293  "cbmc",
294  std::string("Generated by CBMC ") + CBMC_VERSION,
295  "QF_AUFBV",
296  solver);
297  smt2_dec->set_message_handler(message_handler);
298 
299  if(options.get_bool_option("fpa"))
300  smt2_dec->use_FPA_theory = true;
301 
302  smt2_dec->set_message_handler(message_handler);
303 
305  return util_make_unique<solvert>(std::move(smt2_dec));
306  }
307  else if(filename == "-")
308  {
309  auto smt2_conv = util_make_unique<smt2_convt>(
310  ns,
311  "cbmc",
312  std::string("Generated by CBMC ") + CBMC_VERSION,
313  "QF_AUFBV",
314  solver,
315  std::cout);
316 
317  if(options.get_bool_option("fpa"))
318  smt2_conv->use_FPA_theory = true;
319 
321  return util_make_unique<solvert>(std::move(smt2_conv));
322  }
323  else
324  {
325 #ifdef _MSC_VER
326  auto out = util_make_unique<std::ofstream>(widen(filename));
327 #else
328  auto out = util_make_unique<std::ofstream>(filename);
329 #endif
330 
331  if(!*out)
332  {
334  "failed to open file: " + filename, "--outfile");
335  }
336 
337  auto smt2_conv = util_make_unique<smt2_convt>(
338  ns,
339  "cbmc",
340  std::string("Generated by CBMC ") + CBMC_VERSION,
341  "QF_AUFBV",
342  solver,
343  *out);
344 
345  if(options.get_bool_option("fpa"))
346  smt2_conv->use_FPA_theory = true;
347 
349  return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
350  }
351 }
352 
354 {
355  if(options.get_bool_option("beautify"))
356  {
358  "the chosen solver does not support beautification", "--beautify");
359  }
360 }
361 
363 {
364  const bool all_properties = options.get_bool_option("all-properties");
365  const bool cover = options.is_set("cover");
366  const bool incremental_check = options.is_set("incremental-check");
367 
368  if(all_properties)
369  {
371  "the chosen solver does not support incremental solving",
372  "--all_properties");
373  }
374  else if(cover)
375  {
377  "the chosen solver does not support incremental solving", "--cover");
378  }
379  else if(incremental_check)
380  {
382  "the chosen solver does not support incremental solving",
383  "--incremental-check");
384  }
385 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:152
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
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:114
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:203
bv_refinement.h
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:91
solver_factoryt::no_incremental_check
void no_incremental_check()
Definition: solver_factory.cpp:362
DEFAULT_MAX_NB_REFINEMENT
#define DEFAULT_MAX_NB_REFINEMENT
Definition: string_refinement.h:66
options.h
messaget::eom
static eomt eom
Definition: message.h:283
solver_factoryt::solvert::prop
propt & prop() const
Definition: solver_factory.cpp:85
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
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:253
solver_factoryt::get_bv_refinement
std::unique_ptr< solvert > get_bv_refinement()
Definition: solver_factory.cpp:217
prop_conv.h
solver_factoryt::no_beautification
void no_beautification()
Definition: solver_factory.cpp:353
smt2_convt::solvert::YICES
@ YICES
solver_factoryt::solvert::solvert
solvert()=default
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:125
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:27
string_refinement.h
solver_factory.h
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:57
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:38
solver_factoryt::get_default
std::unique_ptr< solvert > get_default()
Definition: solver_factory.cpp:172
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_factoryt::get_solver
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
Definition: solver_factory.cpp:130
solver_factoryt::solvert::stack_decision_procedure
stack_decision_proceduret & stack_decision_procedure() const
Definition: solver_factory.cpp:76
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_factoryt::solvert::set_prop
void set_prop(std::unique_ptr< propt > p)
Definition: solver_factory.cpp:120
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
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:390
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:69
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:145
bv_dimacs.h
validation_modet::INVARIANT
@ INVARIANT
solver_factoryt::get_smt2
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
Definition: solver_factory.cpp:275