cprover
Loading...
Searching...
No Matches
solver_factory.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Solver Factory
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "solver_factory.h"
13
14#include <iostream>
15
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>
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
53solver_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
123void solver_factoryt::solvert::set_prop(std::unique_ptr<propt> p)
124{
125 prop_ptr = std::move(p);
126}
127
128void solver_factoryt::solvert::set_ofstream(std::unique_ptr<std::ofstream> p)
129{
130 ofstream_ptr = std::move(p);
131}
132
133std::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"))
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
185template <typename SatcheckT>
186static 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
211std::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
238 solver->set_decision_procedure(std::move(bv_pointers));
239
240 return solver;
241}
242
243std::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
258std::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
272std::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"))
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
308std::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"))
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
331std::unique_ptr<solver_factoryt::solvert>
332solver_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
343std::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:24
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.
STL namespace.
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
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:49
const char * CBMC_VERSION