Skip to content

Commit d30aa73

Browse files
committed
Use smt_logics.def to implement smt_logics classes
Because no customisation expected for these classes, using the `.def` to implement them saves duplicating code.
1 parent 7601ad5 commit d30aa73

File tree

2 files changed

+16
-9
lines changed

2 files changed

+16
-9
lines changed

src/solvers/smt2_incremental/smt_logics.cpp

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,10 @@ void smt_logict::accept(smt_logic_const_downcast_visitort &&visitor) const
4141
::accept(*this, id(), std::move(visitor));
4242
}
4343

44-
smt_logic_quantifier_free_bit_vectorst::smt_logic_quantifier_free_bit_vectorst()
45-
: smt_logict{ID_smt_logic_quantifier_free_bit_vectors}
46-
{
47-
}
44+
#define LOGIC_ID(the_id) \
45+
smt_logic_##the_id##t::smt_logic_##the_id##t() \
46+
: smt_logict{ID_smt_logic_##the_id} \
47+
{ \
48+
}
49+
#include "smt_logics.def"
50+
#undef LOGIC_ID

src/solvers/smt2_incremental/smt_logics.h

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -61,11 +61,15 @@ const smt_logict &smt_logict::storert<derivedt>::downcast(const irept &irep)
6161
return static_cast<const smt_logict &>(irep);
6262
}
6363

64-
class smt_logic_quantifier_free_bit_vectorst : public smt_logict
65-
{
66-
public:
67-
smt_logic_quantifier_free_bit_vectorst();
68-
};
64+
#define LOGIC_ID(the_id) \
65+
/* NOLINTNEXTLINE(readability/identifiers) cpplint does not match the ## */ \
66+
class smt_logic_##the_id##t : public smt_logict \
67+
{ \
68+
public: \
69+
smt_logic_##the_id##t(); \
70+
};
71+
#include "smt_logics.def"
72+
#undef LOGIC_ID
6973

7074
class smt_logic_const_downcast_visitort
7175
{

0 commit comments

Comments
 (0)