Skip to content

Manage lifetime of MiniSat and Glucose solver pointers using unique_ptr #6078

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 6 commits into from
May 5, 2021
Merged

Manage lifetime of MiniSat and Glucose solver pointers using unique_ptr #6078

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
2a43b15
Inherit constructor of `satcheck_minisat2_baset`
thomasspriggs May 5, 2021
e7b6d76
Declare destructor of `satcheck_minisat2_baset` using `override`
thomasspriggs May 5, 2021
2543943
Manage lifetime of MiniSat solver pointer using `unique_ptr`
thomasspriggs May 5, 2021
93c9544
Inherit constructor of `satcheck_glucose_baset`
thomasspriggs May 5, 2021
24b4fec
Declare destructor of `satcheck_glucose_baset` using `override`
thomasspriggs May 5, 2021
3547708
Manage lifetime of Glucose solver pointer using `unique_ptr`
thomasspriggs May 5, 2021
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
8 changes: 0 additions & 8 deletions scripts/expected_doxygen_warnings.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,6 @@
template
satcheck_glucose_baset< Glucose::SimpSolver >::~satcheck_glucose_baset()

/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:313: warning: no matching class member found for
template
satcheck_minisat2_baset< Minisat::Solver >::~satcheck_minisat2_baset()

/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:319: warning: no matching class member found for
template
satcheck_minisat2_baset< Minisat::SimpSolver >::~satcheck_minisat2_baset()

warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'goto_model.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
Expand Down
40 changes: 10 additions & 30 deletions src/solvers/sat/satcheck_minisat2.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
#include <stack>

#include <util/invariant.h>
#include <util/make_unique.h>
#include <util/threeval.h>

#include <minisat/core/Solver.h>
Expand Down Expand Up @@ -227,7 +228,7 @@ propt::resultt satcheck_minisat2_baset<T>::do_prop_solve()

if(time_limit_seconds != 0)
{
solver_to_interrupt = solver;
solver_to_interrupt = solver.get();
old_handler = signal(SIGALRM, interrupt_solver);
if(old_handler == SIG_ERR)
log.warning() << "Failed to set solver time limit" << messaget::eom;
Expand All @@ -241,7 +242,7 @@ propt::resultt satcheck_minisat2_baset<T>::do_prop_solve()
{
alarm(0);
signal(SIGALRM, old_handler);
solver_to_interrupt = solver;
solver_to_interrupt = solver.get();
}

#else // _WIN32
Expand Down Expand Up @@ -308,23 +309,15 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)

template <typename T>
satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
T *_solver,
message_handlert &message_handler)
: cnf_solvert(message_handler), solver(_solver), time_limit_seconds(0)
: cnf_solvert(message_handler),
solver(util_make_unique<T>()),
time_limit_seconds(0)
{
}

template<>
satcheck_minisat2_baset<Minisat::Solver>::~satcheck_minisat2_baset()
{
delete solver;
}

template<>
satcheck_minisat2_baset<Minisat::SimpSolver>::~satcheck_minisat2_baset()
{
delete solver;
}
template <typename T>
satcheck_minisat2_baset<T>::~satcheck_minisat2_baset() = default;

template<typename T>
bool satcheck_minisat2_baset<T>::is_in_conflict(literalt a) const
Expand Down Expand Up @@ -353,21 +346,8 @@ void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)
}
}

satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(
message_handlert &message_handler)
: satcheck_minisat2_baset<Minisat::Solver>(
new Minisat::Solver,
message_handler)
{
}

satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
message_handlert &message_handler)
: satcheck_minisat2_baset<Minisat::SimpSolver>(
new Minisat::SimpSolver,
message_handler)
{
}
template class satcheck_minisat2_baset<Minisat::Solver>;
template class satcheck_minisat2_baset<Minisat::SimpSolver>;

void satcheck_minisat_simplifiert::set_frozen(literalt a)
{
Expand Down
14 changes: 9 additions & 5 deletions src/solvers/sat/satcheck_minisat2.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]

#include <solvers/hardness_collector.h>

#include <memory>

// Select one: basic solver or with simplification.
// Note that the solver with simplifier isn't really robust
// when used incrementally, as variables may disappear
Expand All @@ -29,8 +31,10 @@ template <typename T>
class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
{
public:
satcheck_minisat2_baset(T *, message_handlert &message_handler);
virtual ~satcheck_minisat2_baset();
explicit satcheck_minisat2_baset(message_handlert &message_handler);
/// A default destructor defined in the `.cpp` is used to ensure the
/// unique_ptr to the solver is correctly destroyed.
~satcheck_minisat2_baset() override;

tvt l_get(literalt a) const override final;

Expand Down Expand Up @@ -81,7 +85,7 @@ class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
protected:
resultt do_prop_solve() override;

T *solver;
std::unique_ptr<T> solver;
uint32_t time_limit_seconds;

void add_variables();
Expand All @@ -94,15 +98,15 @@ class satcheck_minisat_no_simplifiert:
public satcheck_minisat2_baset<Minisat::Solver>
{
public:
explicit satcheck_minisat_no_simplifiert(message_handlert &message_handler);
using satcheck_minisat2_baset<Minisat::Solver>::satcheck_minisat2_baset;
const std::string solver_text() override;
};

class satcheck_minisat_simplifiert:
public satcheck_minisat2_baset<Minisat::SimpSolver>
{
public:
explicit satcheck_minisat_simplifiert(message_handlert &message_handler);
using satcheck_minisat2_baset<Minisat::SimpSolver>::satcheck_minisat2_baset;
const std::string solver_text() override final;
void set_frozen(literalt a) override final;
bool is_eliminated(literalt a) const;
Expand Down