Skip to content

Commit 93c9544

Browse files
committed
Inherit constructor of satcheck_glucose_baset
This avoids having definitions of the constructors of `satcheck_glucose_simplifiert` and `satcheck_glucose_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 2543943 commit 93c9544

File tree

2 files changed

+6
-20
lines changed

2 files changed

+6
-20
lines changed

src/solvers/sat/satcheck_glucose.cpp

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

244244
template <typename T>
245245
satcheck_glucose_baset<T>::satcheck_glucose_baset(
246-
T *_solver,
247246
message_handlert &message_handler)
248-
: cnf_solvert(message_handler), solver(_solver)
247+
: cnf_solvert(message_handler), solver(new T)
249248
{
250249
}
251250

@@ -285,21 +284,8 @@ void satcheck_glucose_baset<T>::set_assumptions(const bvt &bv)
285284
}
286285
}
287286

288-
satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert(
289-
message_handlert &message_handler)
290-
: satcheck_glucose_baset<Glucose::Solver>(
291-
new Glucose::Solver,
292-
message_handler)
293-
{
294-
}
295-
296-
satcheck_glucose_simplifiert::satcheck_glucose_simplifiert(
297-
message_handlert &message_handler)
298-
: satcheck_glucose_baset<Glucose::SimpSolver>(
299-
new Glucose::SimpSolver,
300-
message_handler)
301-
{
302-
}
287+
template class satcheck_glucose_baset<Glucose::Solver>;
288+
template class satcheck_glucose_baset<Glucose::SimpSolver>;
303289

304290
void satcheck_glucose_simplifiert::set_frozen(literalt a)
305291
{

src/solvers/sat/satcheck_glucose.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_glucose_baset : public cnf_solvert, public hardness_collectort
3030
{
3131
public:
32-
satcheck_glucose_baset(T *, message_handlert &message_handler);
32+
explicit satcheck_glucose_baset(message_handlert &message_handler);
3333
virtual ~satcheck_glucose_baset();
3434

3535
tvt l_get(literalt a) const override;
@@ -82,15 +82,15 @@ class satcheck_glucose_no_simplifiert:
8282
public satcheck_glucose_baset<Glucose::Solver>
8383
{
8484
public:
85-
explicit satcheck_glucose_no_simplifiert(message_handlert &message_handler);
85+
using satcheck_glucose_baset<Glucose::Solver>::satcheck_glucose_baset;
8686
const std::string solver_text() override;
8787
};
8888

8989
class satcheck_glucose_simplifiert:
9090
public satcheck_glucose_baset<Glucose::SimpSolver>
9191
{
9292
public:
93-
explicit satcheck_glucose_simplifiert(message_handlert &message_handler);
93+
using satcheck_glucose_baset<Glucose::SimpSolver>::satcheck_glucose_baset;
9494
const std::string solver_text() override;
9595
void set_frozen(literalt a) override;
9696
bool is_eliminated(literalt a) const;

0 commit comments

Comments
 (0)