Skip to content

Commit 2a43b15

Browse files
committed
Inherit constructor of satcheck_minisat2_baset
This avoids having definitions of the constructors of `satcheck_minisat_simplifiert` and `satcheck_minisat_no_simplifiert` which were implemented the same way, by having a single template constructor instead. This will simplify subsequent changes to the constructor, because they will only need to be made in one place.
1 parent 3984250 commit 2a43b15

File tree

2 files changed

+6
-20
lines changed

2 files changed

+6
-20
lines changed

src/solvers/sat/satcheck_minisat2.cpp

Lines changed: 3 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -308,9 +308,8 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
308308

309309
template <typename T>
310310
satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
311-
T *_solver,
312311
message_handlert &message_handler)
313-
: cnf_solvert(message_handler), solver(_solver), time_limit_seconds(0)
312+
: cnf_solvert(message_handler), solver(new T), time_limit_seconds(0)
314313
{
315314
}
316315

@@ -353,21 +352,8 @@ void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)
353352
}
354353
}
355354

356-
satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(
357-
message_handlert &message_handler)
358-
: satcheck_minisat2_baset<Minisat::Solver>(
359-
new Minisat::Solver,
360-
message_handler)
361-
{
362-
}
363-
364-
satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
365-
message_handlert &message_handler)
366-
: satcheck_minisat2_baset<Minisat::SimpSolver>(
367-
new Minisat::SimpSolver,
368-
message_handler)
369-
{
370-
}
355+
template class satcheck_minisat2_baset<Minisat::Solver>;
356+
template class satcheck_minisat2_baset<Minisat::SimpSolver>;
371357

372358
void satcheck_minisat_simplifiert::set_frozen(literalt a)
373359
{

src/solvers/sat/satcheck_minisat2.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ template <typename T>
2929
class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
3030
{
3131
public:
32-
satcheck_minisat2_baset(T *, message_handlert &message_handler);
32+
explicit satcheck_minisat2_baset(message_handlert &message_handler);
3333
virtual ~satcheck_minisat2_baset();
3434

3535
tvt l_get(literalt a) const override final;
@@ -94,15 +94,15 @@ class satcheck_minisat_no_simplifiert:
9494
public satcheck_minisat2_baset<Minisat::Solver>
9595
{
9696
public:
97-
explicit satcheck_minisat_no_simplifiert(message_handlert &message_handler);
97+
using satcheck_minisat2_baset<Minisat::Solver>::satcheck_minisat2_baset;
9898
const std::string solver_text() override;
9999
};
100100

101101
class satcheck_minisat_simplifiert:
102102
public satcheck_minisat2_baset<Minisat::SimpSolver>
103103
{
104104
public:
105-
explicit satcheck_minisat_simplifiert(message_handlert &message_handler);
105+
using satcheck_minisat2_baset<Minisat::SimpSolver>::satcheck_minisat2_baset;
106106
const std::string solver_text() override final;
107107
void set_frozen(literalt a) override final;
108108
bool is_eliminated(literalt a) const;

0 commit comments

Comments
 (0)