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 <fstream>
15 #include <iostream>
16 #include <memory>
17 #include <string>
18 
19 #include <util/exception_utils.h>
20 #include <util/make_unique.h>
21 #include <util/unicode.h>
22 #include <util/version.h>
23 
27 #include <solvers/sat/dimacs_cnf.h>
28 #include <solvers/sat/satcheck.h>
29 #include <solvers/smt2/smt2_dec.h>
30 
34 {
35  // we shouldn't get here if this option isn't set
37 
39 
40  if(options.get_bool_option("boolector"))
42  else if(options.get_bool_option("cprover-smt2"))
44  else if(options.get_bool_option("mathsat"))
46  else if(options.get_bool_option("cvc3"))
48  else if(options.get_bool_option("cvc4"))
50  else if(options.get_bool_option("yices"))
52  else if(options.get_bool_option("z3"))
54  else if(options.get_bool_option("generic"))
56 
57  return s;
58 }
59 
60 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
61 {
62  auto solver = util_make_unique<solvert>();
63 
64  if(
65  options.get_bool_option("beautify") ||
66  !options.get_bool_option("sat-preprocessor")) // no simplifier
67  {
68  // simplifier won't work with beautification
69  solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
70  }
71  else // with simplifier
72  {
73  solver->set_prop(util_make_unique<satcheckt>());
74  }
75 
76  solver->prop().set_message_handler(message_handler);
77 
78  auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
79 
80  if(options.get_option("arrays-uf") == "never")
81  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
82  else if(options.get_option("arrays-uf") == "always")
83  bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
84 
85  solver->set_prop_conv(std::move(bv_pointers));
86 
87  return solver;
88 }
89 
90 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
91 {
94 
95  auto prop = util_make_unique<dimacs_cnft>();
96  prop->set_message_handler(message_handler);
97 
98  std::string filename = options.get_option("outfile");
99 
100  auto bv_dimacs = util_make_unique<bv_dimacst>(ns, *prop, filename);
101  return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
102 }
103 
104 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
105 {
106  std::unique_ptr<propt> prop = [this]() -> std::unique_ptr<propt> {
107  // We offer the option to disable the SAT preprocessor
108  if(options.get_bool_option("sat-preprocessor"))
109  {
111  return util_make_unique<satcheckt>();
112  }
113  return util_make_unique<satcheck_no_simplifiert>();
114  }();
115 
117 
119  info.ns = &ns;
120  info.prop = prop.get();
122 
123  // we allow setting some parameters
124  if(options.get_bool_option("max-node-refinement"))
125  info.max_node_refinement =
126  options.get_unsigned_int_option("max-node-refinement");
127 
128  info.refine_arrays = options.get_bool_option("refine-arrays");
129  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
130 
131  return util_make_unique<solvert>(
132  util_make_unique<bv_refinementt>(info), std::move(prop));
133 }
134 
138 std::unique_ptr<solver_factoryt::solvert>
140 {
142  info.ns = &ns;
143  auto prop = util_make_unique<satcheck_no_simplifiert>();
144  prop->set_message_handler(message_handler);
145  info.prop = prop.get();
148  if(options.get_bool_option("max-node-refinement"))
149  info.max_node_refinement =
150  options.get_unsigned_int_option("max-node-refinement");
151  info.refine_arrays = options.get_bool_option("refine-arrays");
152  info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
153 
154  return util_make_unique<solvert>(
155  util_make_unique<string_refinementt>(info), std::move(prop));
156 }
157 
158 std::unique_ptr<solver_factoryt::solvert>
160 {
162 
163  const std::string &filename = options.get_option("outfile");
164 
165  if(filename == "")
166  {
168  {
170  "required filename not provided",
171  "--outfile",
172  "provide a filename with --outfile");
173  }
174 
175  auto smt2_dec = util_make_unique<smt2_dect>(
176  ns,
177  "cbmc",
178  std::string("Generated by CBMC ") + CBMC_VERSION,
179  "QF_AUFBV",
180  solver);
181 
182  if(options.get_bool_option("fpa"))
183  smt2_dec->use_FPA_theory = true;
184 
185  return util_make_unique<solvert>(std::move(smt2_dec));
186  }
187  else if(filename == "-")
188  {
189  auto smt2_conv = util_make_unique<smt2_convt>(
190  ns,
191  "cbmc",
192  std::string("Generated by CBMC ") + CBMC_VERSION,
193  "QF_AUFBV",
194  solver,
195  std::cout);
196 
197  if(options.get_bool_option("fpa"))
198  smt2_conv->use_FPA_theory = true;
199 
200  smt2_conv->set_message_handler(message_handler);
201 
202  return util_make_unique<solvert>(std::move(smt2_conv));
203  }
204  else
205  {
206 #ifdef _MSC_VER
207  auto out = util_make_unique<std::ofstream>(widen(filename));
208 #else
209  auto out = util_make_unique<std::ofstream>(filename);
210 #endif
211 
212  if(!*out)
213  {
215  "failed to open file: " + filename, "--outfile");
216  }
217 
218  auto smt2_conv = util_make_unique<smt2_convt>(
219  ns,
220  "cbmc",
221  std::string("Generated by CBMC ") + CBMC_VERSION,
222  "QF_AUFBV",
223  solver,
224  *out);
225 
226  if(options.get_bool_option("fpa"))
227  smt2_conv->use_FPA_theory = true;
228 
229  smt2_conv->set_message_handler(message_handler);
230 
231  return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
232  }
233 }
234 
236 {
237  if(options.get_bool_option("beautify"))
238  {
240  "the chosen solver does not support beautification", "--beautify");
241  }
242 }
243 
245 {
246  const bool all_properties = options.get_bool_option("all-properties");
247  const bool cover = options.is_set("cover");
248  const bool incremental_check = options.is_set("incremental-check");
249 
250  if(all_properties)
251  {
253  "the chosen solver does not support incremental solving",
254  "--all_properties");
255  }
256  else if(cover)
257  {
259  "the chosen solver does not support incremental solving", "--cover");
260  }
261  else if(incremental_check)
262  {
264  "the chosen solver does not support incremental solving",
265  "--incremental-check");
266  }
267 }
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
smt2_convt::solvert::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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
smt2_convt::solvert::CPROVER_SMT2
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
bv_refinementt::infot
Definition: bv_refinement.h:33
solver_factoryt::get_dimacs
std::unique_ptr< solvert > get_dimacs()
Definition: solver_factory.cpp:90
bv_refinement.h
string_refinementt::configt::refinement_bound
std::size_t refinement_bound
Definition: string_refinement.h:67
smt2_convt::solvert::MATHSAT
bv_refinementt::configt::refine_arithmetic
bool refine_arithmetic
Enable arithmetic refinement.
Definition: bv_refinement.h:30
solver_factoryt::no_incremental_check
void no_incremental_check()
Definition: solver_factory.cpp:244
DEFAULT_MAX_NB_REFINEMENT
#define DEFAULT_MAX_NB_REFINEMENT
Definition: string_refinement.h:60
version.h
smt2_convt::solvert::CVC3
smt2_convt::solvert::BOOLECTOR
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:139
solver_factoryt::get_bv_refinement
std::unique_ptr< solvert > get_bv_refinement()
Definition: solver_factory.cpp:104
solver_factoryt::no_beautification
void no_beautification()
Definition: solver_factory.cpp:235
smt2_convt::solvert::YICES
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:60
bv_refinementt::infot::prop
propt * prop
Definition: bv_refinement.h:36
smt2_dec.h
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
solver_factoryt::message_handler
message_handlert & message_handler
Definition: solver_factory.h:123
string_refinement.h
solver_factory.h
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:52
solver_factoryt::get_default
std::unique_ptr< solvert > get_default()
Definition: solver_factory.cpp:60
optionst::get_unsigned_int_option
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:54
boolbvt::unbounded_arrayt::U_NONE
satcheck.h
dimacs_cnf.h
solver_factoryt::ns
namespacet ns
Definition: solver_factory.h:122
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:360
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
boolbvt::unbounded_arrayt::U_ALL
solver_factoryt::options
const optionst & options
Definition: solver_factory.h:120
unicode.h
smt2_convt::solvert::GENERIC
smt2_convt::solvert::Z3
string_refinementt::infot
string_refinementt constructor arguments
Definition: string_refinement.h:72
smt2_convt::solvert
solvert
Definition: smt2_conv.h:35
solver_factoryt::output_xml_in_refinement
const bool output_xml_in_refinement
Definition: solver_factory.h:124
bv_refinementt::infot::ns
const namespacet * ns
Definition: bv_refinement.h:35
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:37
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:33
bv_dimacs.h
solver_factoryt::get_smt2
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
Definition: solver_factory.cpp:159