mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
minor code simplification
This commit is contained in:
parent
01188462d5
commit
fcb03aa56c
|
@ -753,7 +753,7 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
if (j != i) {
|
||||
m_lemma[j] = m_lemma[i];
|
||||
m_lemma[j] = l;
|
||||
m_lemma_atoms.set(j, m_lemma_atoms.get(i));
|
||||
}
|
||||
j++;
|
||||
|
|
|
@ -41,7 +41,7 @@ static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes");
|
|||
template<typename T, typename T2U_Proc, typename R=unsigned long long>
|
||||
class approx_set_tpl : private T2U_Proc {
|
||||
protected:
|
||||
R m_set;
|
||||
R m_set = approx_set_traits<R>::zero;
|
||||
|
||||
unsigned e2u(T const & e) const { return T2U_Proc::operator()(e); }
|
||||
|
||||
|
@ -52,24 +52,17 @@ protected:
|
|||
static approx_set_tpl r2s(R const & s) { approx_set_tpl r; r.m_set = s; return r; }
|
||||
|
||||
public:
|
||||
approx_set_tpl():
|
||||
m_set(approx_set_traits<R>::zero) {
|
||||
}
|
||||
approx_set_tpl() = default;
|
||||
|
||||
explicit approx_set_tpl(T const & e):
|
||||
m_set(e2s(e)) {
|
||||
}
|
||||
|
||||
approx_set_tpl(unsigned sz, T const * es):
|
||||
m_set(approx_set_traits<R>::zero) {
|
||||
approx_set_tpl(unsigned sz, T const * es) {
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
insert(es[i]);
|
||||
}
|
||||
|
||||
approx_set_tpl(approx_set_tpl const & s):
|
||||
m_set(s.m_set) {
|
||||
}
|
||||
|
||||
void set(R s) { m_set = s; }
|
||||
|
||||
R get() const { return m_set; }
|
||||
|
|
Loading…
Reference in a new issue