Skip to content

remove support for SMT1 #2135

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Apr 30, 2018
Merged

remove support for SMT1 #2135

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
218dc31
remove support for SMT1
Apr 28, 2018
a2d9822
remove OpenSMT
Apr 28, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 11 additions & 47 deletions src/cbmc/cbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -312,100 +312,64 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
options.set_option("aig", true);

// SMT Options
bool version_set=false;

if(cmdline.isset("smt1"))
{
options.set_option("smt1", true);
options.set_option("smt2", false);
version_set=true;
error() << "--smt1 is no longer supported" << eom;
exit(CPROVER_EXIT_USAGE_ERROR);
}

if(cmdline.isset("smt2"))
{
// If both are given, smt2 takes precedence
options.set_option("smt1", false);
options.set_option("smt2", true);
version_set=true;
}

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


bool solver_set=false;

if(cmdline.isset("boolector"))
{
options.set_option("boolector", true), solver_set=true;
if(!version_set)
options.set_option("smt2", true), version_set=true;
options.set_option("smt2", true);
}

if(cmdline.isset("mathsat"))
{
options.set_option("mathsat", true), solver_set=true;
if(!version_set)
options.set_option("smt2", true), version_set=true;
}

if(cmdline.isset("cvc3"))
{
options.set_option("cvc3", true), solver_set=true;
if(!version_set)
options.set_option("smt1", true), version_set=true;
options.set_option("smt2", true);
}

if(cmdline.isset("cvc4"))
{
options.set_option("cvc4", true), solver_set=true;
if(!version_set)
options.set_option("smt2", true), version_set=true;
options.set_option("smt2", true);
}

if(cmdline.isset("yices"))
{
options.set_option("yices", true), solver_set=true;
if(!version_set)
options.set_option("smt2", true), version_set=true;
options.set_option("smt2", true);
}

if(cmdline.isset("z3"))
{
options.set_option("z3", true), solver_set=true;
if(!version_set)
options.set_option("smt2", true), version_set=true;
}

if(cmdline.isset("opensmt"))
{
options.set_option("opensmt", true), solver_set=true;
if(!version_set)
options.set_option("smt1", true), version_set=true;
options.set_option("smt2", true);
}

if(version_set && !solver_set)
if(cmdline.isset("smt2") && !solver_set)
{
if(cmdline.isset("outfile"))
{
// outfile and no solver should give standard compliant SMT-LIB
options.set_option("generic", true), solver_set=true;
options.set_option("generic", true);
}
else
{
if(options.get_bool_option("smt1"))
{
options.set_option("boolector", true), solver_set=true;
}
else
{
PRECONDITION(options.get_bool_option("smt2"));
options.set_option("z3", true), solver_set=true;
}
// the default smt2 solver
options.set_option("z3", true);
}
}
// Either have solver and standard version set, or neither.
PRECONDITION(version_set == solver_set);

if(cmdline.isset("beautify"))
options.set_option("beautify", true);
Expand Down
101 changes: 0 additions & 101 deletions src/cbmc/cbmc_solvers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ Author: Daniel Kroening, [email protected]
#include <solvers/sat/satcheck.h>
#include <solvers/refinement/bv_refinement.h>
#include <solvers/refinement/string_refinement.h>
#include <solvers/smt1/smt1_dec.h>
#include <solvers/smt2/smt2_dec.h>
#include <solvers/cvc/cvc_dec.h>
#include <solvers/prop/aig_prop.h>
Expand All @@ -32,34 +31,6 @@ Author: Daniel Kroening, [email protected]
#include "counterexample_beautification.h"
#include "version.h"

/// Uses the options to pick an SMT 1.2 solver
/// \return An smt1_dect::solvert giving the solver to use.
smt1_dect::solvert cbmc_solverst::get_smt1_solver_type() const
{
assert(options.get_bool_option("smt1"));

smt1_dect::solvert s=smt1_dect::solvert::GENERIC;

if(options.get_bool_option("boolector"))
s=smt1_dect::solvert::BOOLECTOR;
else if(options.get_bool_option("mathsat"))
s=smt1_dect::solvert::MATHSAT;
else if(options.get_bool_option("cvc3"))
s=smt1_dect::solvert::CVC3;
else if(options.get_bool_option("cvc4"))
s=smt1_dect::solvert::CVC4;
else if(options.get_bool_option("opensmt"))
s=smt1_dect::solvert::OPENSMT;
else if(options.get_bool_option("yices"))
s=smt1_dect::solvert::YICES;
else if(options.get_bool_option("z3"))
s=smt1_dect::solvert::Z3;
else if(options.get_bool_option("generic"))
s=smt1_dect::solvert::GENERIC;

return s;
}

/// Uses the options to pick an SMT 2.0 solver
/// \return An smt2_dect::solvert giving the solver to use.
smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
Expand All @@ -76,8 +47,6 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
s=smt2_dect::solvert::CVC3;
else if(options.get_bool_option("cvc4"))
s=smt2_dect::solvert::CVC4;
else if(options.get_bool_option("opensmt"))
s=smt2_dect::solvert::OPENSMT;
else if(options.get_bool_option("yices"))
s=smt2_dect::solvert::YICES;
else if(options.get_bool_option("z3"))
Expand Down Expand Up @@ -189,76 +158,6 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
util_make_unique<string_refinementt>(info), std::move(prop));
}

std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt1(
smt1_dect::solvert solver)
{
no_beautification();
no_incremental_check();

const std::string &filename=options.get_option("outfile");

if(filename=="")
{
if(solver==smt1_dect::solvert::GENERIC)
{
error() << "please use --outfile" << eom;
throw 0;
}

auto smt1_dec=
util_make_unique<smt1_dect>(
ns,
"cbmc",
"Generated by CBMC " CBMC_VERSION,
"QF_AUFBV",
solver);

return util_make_unique<solvert>(std::move(smt1_dec));
}
else if(filename=="-")
{
auto smt1_conv=
util_make_unique<smt1_convt>(
ns,
"cbmc",
"Generated by CBMC " CBMC_VERSION,
"QF_AUFBV",
solver,
std::cout);

smt1_conv->set_message_handler(get_message_handler());

return util_make_unique<solvert>(std::move(smt1_conv));
}
else
{
#ifdef _MSC_VER
auto out=util_make_unique<std::ofstream>(widen(filename));
#else
auto out=util_make_unique<std::ofstream>(filename);
#endif

if(!out)
{
error() << "failed to open " << filename << eom;
throw 0;
}

auto smt1_conv=
util_make_unique<smt1_convt>(
ns,
"cbmc",
"Generated by CBMC " CBMC_VERSION,
"QF_AUFBV",
solver,
*out);

smt1_conv->set_message_handler(get_message_handler());

return util_make_unique<solvert>(std::move(smt1_conv), std::move(out));
}
}

std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
smt2_dect::solvert solver)
{
Expand Down
5 changes: 0 additions & 5 deletions src/cbmc/cbmc_solvers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ Author: Daniel Kroening, [email protected]
#include <solvers/sat/cnf.h>
#include <solvers/sat/satcheck.h>
#include <solvers/prop/aig_prop.h>
#include <solvers/smt1/smt1_dec.h>
#include <solvers/smt2/smt2_dec.h>
#include <goto-symex/symex_target_equation.h>

Expand Down Expand Up @@ -112,8 +111,6 @@ class cbmc_solverst:public messaget
return get_bv_refinement();
else if(options.get_bool_option("refine-strings"))
return get_string_refinement();
if(options.get_bool_option("smt1"))
return get_smt1(get_smt1_solver_type());
if(options.get_bool_option("smt2"))
return get_smt2(get_smt2_solver_type());
return get_default();
Expand All @@ -137,10 +134,8 @@ class cbmc_solverst:public messaget
std::unique_ptr<solvert> get_dimacs();
std::unique_ptr<solvert> get_bv_refinement();
std::unique_ptr<solvert> get_string_refinement();
std::unique_ptr<solvert> get_smt1(smt1_dect::solvert solver);
std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);

smt1_dect::solvert get_smt1_solver_type() const;
smt2_dect::solvert get_smt2_solver_type() const;

// consistency checks during solver creation
Expand Down
2 changes: 0 additions & 2 deletions src/solvers/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,8 +189,6 @@ SRC = $(BOOLEFORCE_SRC) \
sat/pbs_dimacs_cnf.cpp \
sat/resolution_proof.cpp \
sat/satcheck.cpp \
smt1/smt1_conv.cpp \
smt1/smt1_dec.cpp \
smt2/smt2_conv.cpp \
smt2/smt2_dec.cpp \
smt2/smt2_parser.cpp \
Expand Down
Loading