@@ -344,6 +344,14 @@ std::string BinaryDecisionDiagram::ToStringDnf(BddNodeIndex expr,
344344 return result;
345345}
346346
347+ namespace {
348+ #ifdef NDEBUG
349+ constexpr bool kDebug = false ;
350+ #else
351+ constexpr bool kDebug = true ;
352+ #endif
353+ } // namespace
354+
347355absl::StatusOr<std::vector<BddNodeIndex>> BinaryDecisionDiagram::GarbageCollect (
348356 absl::Span<BddNodeIndex const > roots, double gc_threshold) {
349357 if (nodes_size_ * gc_threshold < prev_nodes_size_) {
@@ -400,12 +408,12 @@ absl::StatusOr<std::vector<BddNodeIndex>> BinaryDecisionDiagram::GarbageCollect(
400408 }
401409 }
402410 // build a new free-list prefix.
403- for ( auto vs : iter::sliding_window (
404- iter::chain ( dead, std::vector<BddNodeIndex>{ BddNodeIndex (
405- free_node_head_. value ())}),
406- 2 )) {
407- BddNodeIndex first = vs[ 0 ];
408- BddNodeIndex second = vs[ 1 ] ;
411+ // Don't use iter::sliding_window because this is faster.
412+ for ( int i = 0 ; i < dead. size (); ++i) {
413+ BddNodeIndex first = dead[i];
414+ BddNodeIndex second = i + 1 < dead. size ()
415+ ? dead[i + 1 ]
416+ : BddNodeIndex (free_node_head_. value ()) ;
409417 nodes_[first.value ()] = FreeListNode (FreeListNode::Index (second.value ()));
410418 }
411419 free_node_head_ = FreeListNode::Index (dead.front ().value ());
@@ -439,24 +447,26 @@ absl::StatusOr<std::vector<BddNodeIndex>> BinaryDecisionDiagram::GarbageCollect(
439447 }
440448 nodes_size_ = cnt_live;
441449 prev_nodes_size_ = nodes_size_;
442- auto head = free_node_head_;
443- auto it = dead.begin ();
444- InlineBitmap debug_seen (nodes_.size ());
445- while (head.value () < nodes_.size () &&
446- head != FreeListNode::kNextIsConsecutive ) {
447- CHECK (!debug_seen.Get (head.value ()))
448- << " loop in free list at " << head.value ();
449- debug_seen.Set (head.value ());
450- if (it != dead.end ()) {
451- CHECK_EQ (head, FreeListNode::Index (it->value ()));
452- ++it;
453- }
454- CHECK (std::holds_alternative<FreeListNode>(nodes_[head.value ()]));
455- auto cur = std::get<FreeListNode>(nodes_[head.value ()]);
456- if (cur.raw_next () == FreeListNode::kNextIsConsecutive ) {
457- break ;
450+ if constexpr (kDebug ) {
451+ auto head = free_node_head_;
452+ auto it = dead.begin ();
453+ InlineBitmap debug_seen (nodes_.size ());
454+ while (head.value () < nodes_.size () &&
455+ head != FreeListNode::kNextIsConsecutive ) {
456+ CHECK (!debug_seen.Get (head.value ()))
457+ << " loop in free list at " << head.value ();
458+ debug_seen.Set (head.value ());
459+ if (it != dead.end ()) {
460+ CHECK_EQ (head, FreeListNode::Index (it->value ()));
461+ ++it;
462+ }
463+ CHECK (std::holds_alternative<FreeListNode>(nodes_[head.value ()]));
464+ auto cur = std::get<FreeListNode>(nodes_[head.value ()]);
465+ if (cur.raw_next () == FreeListNode::kNextIsConsecutive ) {
466+ break ;
467+ }
468+ head = cur.next_free (head);
458469 }
459- head = cur.next_free (head);
460470 }
461471 return std::move (dead);
462472}
0 commit comments