Skip to content

Commit b8ffa5e

Browse files
tautschnigtautschnig
authored
Merge pull request diffblue#2135 from diffblue/solver-cleanout
remove support for SMT1
2 parents 0dc35fd + a2d9822 commit b8ffa5e

11 files changed

+11
-4339
lines changed

‎src/cbmc/cbmc_parse_options.cpp

+11-47
Original file line numberDiff line numberDiff line change
@@ -312,100 +312,64 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
312312
options.set_option("aig", true);
313313

314314
// SMT Options
315-
bool version_set=false;
316315

317316
if(cmdline.isset("smt1"))
318317
{
319-
options.set_option("smt1", true);
320-
options.set_option("smt2", false);
321-
version_set=true;
318+
error() << "--smt1 is no longer supported" << eom;
319+
exit(CPROVER_EXIT_USAGE_ERROR);
322320
}
323321

324322
if(cmdline.isset("smt2"))
325-
{
326-
// If both are given, smt2 takes precedence
327-
options.set_option("smt1", false);
328323
options.set_option("smt2", true);
329-
version_set=true;
330-
}
331324

332325
if(cmdline.isset("fpa"))
333326
options.set_option("fpa", true);
334327

335-
336328
bool solver_set=false;
337329

338330
if(cmdline.isset("boolector"))
339331
{
340332
options.set_option("boolector", true), solver_set=true;
341-
if(!version_set)
342-
options.set_option("smt2", true), version_set=true;
333+
options.set_option("smt2", true);
343334
}
344335

345336
if(cmdline.isset("mathsat"))
346337
{
347338
options.set_option("mathsat", true), solver_set=true;
348-
if(!version_set)
349-
options.set_option("smt2", true), version_set=true;
350-
}
351-
352-
if(cmdline.isset("cvc3"))
353-
{
354-
options.set_option("cvc3", true), solver_set=true;
355-
if(!version_set)
356-
options.set_option("smt1", true), version_set=true;
339+
options.set_option("smt2", true);
357340
}
358341

359342
if(cmdline.isset("cvc4"))
360343
{
361344
options.set_option("cvc4", true), solver_set=true;
362-
if(!version_set)
363-
options.set_option("smt2", true), version_set=true;
345+
options.set_option("smt2", true);
364346
}
365347

366348
if(cmdline.isset("yices"))
367349
{
368350
options.set_option("yices", true), solver_set=true;
369-
if(!version_set)
370-
options.set_option("smt2", true), version_set=true;
351+
options.set_option("smt2", true);
371352
}
372353

373354
if(cmdline.isset("z3"))
374355
{
375356
options.set_option("z3", true), solver_set=true;
376-
if(!version_set)
377-
options.set_option("smt2", true), version_set=true;
378-
}
379-
380-
if(cmdline.isset("opensmt"))
381-
{
382-
options.set_option("opensmt", true), solver_set=true;
383-
if(!version_set)
384-
options.set_option("smt1", true), version_set=true;
357+
options.set_option("smt2", true);
385358
}
386359

387-
if(version_set && !solver_set)
360+
if(cmdline.isset("smt2") && !solver_set)
388361
{
389362
if(cmdline.isset("outfile"))
390363
{
391364
// outfile and no solver should give standard compliant SMT-LIB
392-
options.set_option("generic", true), solver_set=true;
365+
options.set_option("generic", true);
393366
}
394367
else
395368
{
396-
if(options.get_bool_option("smt1"))
397-
{
398-
options.set_option("boolector", true), solver_set=true;
399-
}
400-
else
401-
{
402-
PRECONDITION(options.get_bool_option("smt2"));
403-
options.set_option("z3", true), solver_set=true;
404-
}
369+
// the default smt2 solver
370+
options.set_option("z3", true);
405371
}
406372
}
407-
// Either have solver and standard version set, or neither.
408-
PRECONDITION(version_set == solver_set);
409373

410374
if(cmdline.isset("beautify"))
411375
options.set_option("beautify", true);

‎src/cbmc/cbmc_solvers.cpp

-101
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ Author: Daniel Kroening, [email protected]
2121
#include <solvers/sat/satcheck.h>
2222
#include <solvers/refinement/bv_refinement.h>
2323
#include <solvers/refinement/string_refinement.h>
24-
#include <solvers/smt1/smt1_dec.h>
2524
#include <solvers/smt2/smt2_dec.h>
2625
#include <solvers/cvc/cvc_dec.h>
2726
#include <solvers/prop/aig_prop.h>
@@ -32,34 +31,6 @@ Author: Daniel Kroening, [email protected]
3231
#include "counterexample_beautification.h"
3332
#include "version.h"
3433

35-
/// Uses the options to pick an SMT 1.2 solver
36-
/// \return An smt1_dect::solvert giving the solver to use.
37-
smt1_dect::solvert cbmc_solverst::get_smt1_solver_type() const
38-
{
39-
assert(options.get_bool_option("smt1"));
40-
41-
smt1_dect::solvert s=smt1_dect::solvert::GENERIC;
42-
43-
if(options.get_bool_option("boolector"))
44-
s=smt1_dect::solvert::BOOLECTOR;
45-
else if(options.get_bool_option("mathsat"))
46-
s=smt1_dect::solvert::MATHSAT;
47-
else if(options.get_bool_option("cvc3"))
48-
s=smt1_dect::solvert::CVC3;
49-
else if(options.get_bool_option("cvc4"))
50-
s=smt1_dect::solvert::CVC4;
51-
else if(options.get_bool_option("opensmt"))
52-
s=smt1_dect::solvert::OPENSMT;
53-
else if(options.get_bool_option("yices"))
54-
s=smt1_dect::solvert::YICES;
55-
else if(options.get_bool_option("z3"))
56-
s=smt1_dect::solvert::Z3;
57-
else if(options.get_bool_option("generic"))
58-
s=smt1_dect::solvert::GENERIC;
59-
60-
return s;
61-
}
62-
6334
/// Uses the options to pick an SMT 2.0 solver
6435
/// \return An smt2_dect::solvert giving the solver to use.
6536
smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
@@ -76,8 +47,6 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
7647
s=smt2_dect::solvert::CVC3;
7748
else if(options.get_bool_option("cvc4"))
7849
s=smt2_dect::solvert::CVC4;
79-
else if(options.get_bool_option("opensmt"))
80-
s=smt2_dect::solvert::OPENSMT;
8150
else if(options.get_bool_option("yices"))
8251
s=smt2_dect::solvert::YICES;
8352
else if(options.get_bool_option("z3"))
@@ -189,76 +158,6 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
189158
util_make_unique<string_refinementt>(info), std::move(prop));
190159
}
191160

192-
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt1(
193-
smt1_dect::solvert solver)
194-
{
195-
no_beautification();
196-
no_incremental_check();
197-
198-
const std::string &filename=options.get_option("outfile");
199-
200-
if(filename=="")
201-
{
202-
if(solver==smt1_dect::solvert::GENERIC)
203-
{
204-
error() << "please use --outfile" << eom;
205-
throw 0;
206-
}
207-
208-
auto smt1_dec=
209-
util_make_unique<smt1_dect>(
210-
ns,
211-
"cbmc",
212-
"Generated by CBMC " CBMC_VERSION,
213-
"QF_AUFBV",
214-
solver);
215-
216-
return util_make_unique<solvert>(std::move(smt1_dec));
217-
}
218-
else if(filename=="-")
219-
{
220-
auto smt1_conv=
221-
util_make_unique<smt1_convt>(
222-
ns,
223-
"cbmc",
224-
"Generated by CBMC " CBMC_VERSION,
225-
"QF_AUFBV",
226-
solver,
227-
std::cout);
228-
229-
smt1_conv->set_message_handler(get_message_handler());
230-
231-
return util_make_unique<solvert>(std::move(smt1_conv));
232-
}
233-
else
234-
{
235-
#ifdef _MSC_VER
236-
auto out=util_make_unique<std::ofstream>(widen(filename));
237-
#else
238-
auto out=util_make_unique<std::ofstream>(filename);
239-
#endif
240-
241-
if(!out)
242-
{
243-
error() << "failed to open " << filename << eom;
244-
throw 0;
245-
}
246-
247-
auto smt1_conv=
248-
util_make_unique<smt1_convt>(
249-
ns,
250-
"cbmc",
251-
"Generated by CBMC " CBMC_VERSION,
252-
"QF_AUFBV",
253-
solver,
254-
*out);
255-
256-
smt1_conv->set_message_handler(get_message_handler());
257-
258-
return util_make_unique<solvert>(std::move(smt1_conv), std::move(out));
259-
}
260-
}
261-
262161
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
263162
smt2_dect::solvert solver)
264163
{

‎src/cbmc/cbmc_solvers.h

-5
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@ Author: Daniel Kroening, [email protected]
2424
#include <solvers/sat/cnf.h>
2525
#include <solvers/sat/satcheck.h>
2626
#include <solvers/prop/aig_prop.h>
27-
#include <solvers/smt1/smt1_dec.h>
2827
#include <solvers/smt2/smt2_dec.h>
2928
#include <goto-symex/symex_target_equation.h>
3029

@@ -112,8 +111,6 @@ class cbmc_solverst:public messaget
112111
return get_bv_refinement();
113112
else if(options.get_bool_option("refine-strings"))
114113
return get_string_refinement();
115-
if(options.get_bool_option("smt1"))
116-
return get_smt1(get_smt1_solver_type());
117114
if(options.get_bool_option("smt2"))
118115
return get_smt2(get_smt2_solver_type());
119116
return get_default();
@@ -137,10 +134,8 @@ class cbmc_solverst:public messaget
137134
std::unique_ptr<solvert> get_dimacs();
138135
std::unique_ptr<solvert> get_bv_refinement();
139136
std::unique_ptr<solvert> get_string_refinement();
140-
std::unique_ptr<solvert> get_smt1(smt1_dect::solvert solver);
141137
std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
142138

143-
smt1_dect::solvert get_smt1_solver_type() const;
144139
smt2_dect::solvert get_smt2_solver_type() const;
145140

146141
// consistency checks during solver creation

‎src/solvers/Makefile

-2
Original file line numberDiff line numberDiff line change
@@ -189,8 +189,6 @@ SRC = $(BOOLEFORCE_SRC) \
189189
sat/pbs_dimacs_cnf.cpp \
190190
sat/resolution_proof.cpp \
191191
sat/satcheck.cpp \
192-
smt1/smt1_conv.cpp \
193-
smt1/smt1_dec.cpp \
194192
smt2/smt2_conv.cpp \
195193
smt2/smt2_dec.cpp \
196194
smt2/smt2_parser.cpp \

0 commit comments

Comments
 (0)