size_t end_index = *end_index_opt; auto found_record_time = records_[end_index].time(); // 検索の条件より、みつかったレンジの左端は、検索範囲と一致するか左側にある。 // もしそうでないばあい、このレンジはその検索時刻を一切含まないためおかしい。 RHETORIC_ASSERT(found_record_time <= range.upper_bound()); if (found_record_time < range.upper_bound()) { // 検索範囲としては右端を含まないので、 // みつかったレンジの左端が検索範囲の右端よりも左にある場合は、 // そのレンジの一部が含まれるためそれがラストレンジ // end_index自体は含まないindexであるため、一個ずらす。 end_index += 1; } else { // みつかったレンジの左端がちょうど検索範囲の右端に一致する場合は、 // その一個左のレンジがラストレンジ // よってend_indexはこのままで良い。 RHETORIC_ASSERT(found_record_time == range.upper_bound()); } (edited)
