Replaces the manually managed `uint32_t* data` with
`std::unique_ptr<uint32_t[]>`. Eliminates the explicit destructor,
all `delete[] data` calls in copy assign, move ctor, move assign,
and `set_free()`. Move operations become `= default`.

Also simplifies the ceiling division in `set_comp` from the two-step
divide-then-conditionally-add-1 to the standard
`(total_bits + block - 1) / block` form.

Makes `_bits_per_block` `static constexpr` instead of a per-instance
`const` member — it's a compile-time constant.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

reserve_comp_space() allocates Comp objects with malloc() but the
matching free() calls were scattered as bare free() calls throughout
comp_management. Adding a named free_comp() makes the allocator
contract explicit and searchable.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Copy constructor now uses member initializer list instead of assignment
in the body. The separate copy assignment and move assignment are
replaced by a single unified assignment operator via copy-and-swap,
which is exception-safe and avoids repeating the same 5-line body.

Also replaces the manually-searched del_c() loop with std::find_if
so the intent (find and swap-erase) is clear and the assert fires
before the pop_back rather than at the end of a failing loop.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

in_mb() was a file-local function in statistics.cpp. Moving it to
common.hpp (with a double overload for vm_usage values) allows
comp_cache.hpp to use it instead of repeating /(double)(1024*1024).

Also removes the useless early return in incorporateIrredClauseData
(returning without doing anything when clause size == 1 — the size==2
check below would simply not fire anyway).

Also removes the redundant std::fill in rehash_table: vec::growTo
already zero-initializes elements via placement-new, so filling after
resize is a no-op.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

The ceiling-division pattern 'bytes/sizeof(uint32_t) +
(bool)(bytes % sizeof(uint32_t))' appeared three times. Replacing
with a named constexpr helper makes the unit conversion explicit.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- Constrains the template to std::ranges::range and uses
  std::ranges::transform instead of a hand-rolled loop.
- Adds reserve() via if constexpr for sized ranges (avoids
  reallocations when converting vectors).
- Adds reserve() to the initializer_list overload (needed because
  brace-init lists can't be deduced by the template).
- Replaces the manual all_of-style check_cl_unsat loop with
  std::all_of for clarity.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

vec::capacity() was computing cap += add using imax(), then immediately
overwriting cap with a power-of-two size. The first computation
(lines with imax and overflow check) was dead code left from a
previous growth strategy refactoring.

Remove the dead computation and the now-unused imax() branchless-max
helper. The actual growth strategy (power-of-two with 2/3 backoff) is
unchanged.

Also use std::copy in copyTo() instead of the index-based loop.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

The local ganak_to_cms_cl(vector<Lit>) was redundant since
counter.hpp already provides a template that handles it (and now with
reserve). Remove it and the trivially-true assertion (num_jobs == num_jobs).

Update cms_to_ganak_cl and ganak_to_cms_vars to use
std::ranges::transform instead of hand-rolled push_back loops.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- td_decompose_component: construct unordered_set<uint32_t> directly
  from pointer range instead of insert loop.
- compute_td_score: use std::minmax_element instead of manual
  min/max accumulation loop.
- UIPFixer::operator(): collapse redundant if/return false into a
  single return expression.
- Sort lambda in vivify: collapse the nested if-then-return-true /
  return-false into a single boolean expression.
- red_cl_can_be_deleted: return \!is_antec_of() directly.
- Various else-after-return/break cleanups: remove unnecessary else
  branches after return, break, or continue.
- Pre-allocate ban vector in the SAT all-solutions loop.
- Remove dead 'if (true) {' wrapper from SAT mode exit path.
- Simplify lit_val_str / val_to_str: remove else-if chains.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

comp_cache:
- get_num_entries_used: use std::count_if over the live entry_base
  range instead of an index loop.
- create_new_comp: return the new T directly instead of via a named
  local variable.

ganak.cpp:
- find_disconnected: use std::all_of to check that all literals in a
  red clause share the same bag (replaces bool+break loop).
- count(): replace index-based bag-assignment double loop with a
  range-based outer loop + manual index counter (cleaner intent).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Changing the parameter type from uint32_t to int avoids a signed vs
unsigned comparison since the recursive calls also produce int values.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- init(): use range-based for when calling set_free on all entries.
- delete_some_entries(): use std::any_of for the has_deletable check;
  use in_mb() for the verbose MB display; use range-based for when
  recomputing sum_extra_bytes; fix typo "entires" → "entries".
- num_siblings(): remove the else-after-return pattern.
- calc_cutoff(): use pre-increment (++it) in the iterator loop.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…plification

remove_duplicates: replaces the hand-rolled single-pass loop with
std::adjacent_find (to detect tautological clauses) + std::unique +
erase (to remove true duplicates). The key insight is that after
sorting, complementary literals (a and a.neg()) are always adjacent
because neg() flips exactly the LSB of the raw encoding.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…tinue

- clash_cubes: replace manual loop with std::any_of
- symm_cubes: eliminate double map lookup (count + find) by using find once
- do_appmc_count: replace manual index push_back loop with std::iota;
  remove trivially-true assert(i >= 0)
- disable_small_cubes: remove unnecessary else after continue

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- do_appmc_count: remove pre-allocated unit/bin vectors, pass initializer
  lists directly to ganak_to_cms_cl; cleaner and removes accidental mutation risk
- cube_strengthen_by_flp: collapse if/else into ternary in the assumption
  building loop

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- find_best_branch: replace insert+manual-todo with resize for vars_act_dec growth
- compute_cube: replace hand-rolled push_back loop with std::ranges::transform
- ganak.cpp: eliminate scoped block by moving index variable into the for loop

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- propagate: collapse two-branch lev_at_declev assignment into single ||
- is_implied: replace manual push_back loop with std::ranges::transform
- minimize_uip_cl: simplify A||(B&&C) where B==\!A to A||C
- vivify_cls: simplify (\!red||(red&&X)) to (\!red||X) (absorption)
- recursive_cc_min: separate i,j declaration; declare i in for-init
- check_count: remove dead last_dec_lev computation (was computed but never read)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- v_satisfied/v_cl_satisfied: use std::any_of
- v_unsat: use std::all_of (all literals are F_TRI)
- v_backtrack: use std::for_each over suffix of v_trail
- v_fix_watch: use std::find_if instead of index-based search loop

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- propagate: replace index-based non-false literal search with std::find_if
- v_propagate: same
- vivify_cl: use std::copy for v_tmp->cl transfer instead of index loop
- fill_cl: collapse if/else c[0] assignment into ternary

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- backw_subsume_cl/backw_subsume_cl_with_bin: replace manual min-index loop
  with std::min_element for finding rarest-occurrence literal
- check_watchlists: simplify find+set+else-increment to single operator[] increment
  (operator[] zero-initializes missing entries for integral types)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- mybdd_two_or: extract repeated lit->bdd conversion into local lambda to_bdd,
  eliminating tmp/tmp2/lvar/rvar locals
- v_restore: replace manual at++ index with iterator advance (*bk_it++)
- clause_falsified: use std::all_of

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…ions

- check_current_state_unsat: use std::ranges::transform over trail
- check_derivable lambda: use std::ranges::transform to negate cms lits
- check_opt_sampling_determined: use initializer lists instead of vector<Lit>{...}
  for single/double-literal clauses

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- check_cls_deriveable: replace vector<Lit>{...} with brace-init {l, ws.lit()}
- check_all_cl_in_watchlists: use std::adjacent_find instead of index loop
- find_offs_in_watch: use std::any_of instead of manual loop

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…undant fill

- add_cl: replace raw index loop with std::copy to fill clause literals
- print_cls_stats: replace manual count loop with std::count_if
- comp_cache init: remove redundant std::fill after vec::resize (resize already zero-initializes)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…try_extend

- td_decompose_component: replace bool sat + for loop with any_of for clause satisfaction
- cube_try_extend_by_lit: same pattern for occurrence clause satisfaction check

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- init_activity_scores: use count_if for binary irredundant clause counting
- find_lev_to_set: use max_element to find second-highest level literal,
  eliminating updated/switch_to tracking variables

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…tchlists

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…che.hpp

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

conflicting_cl: manual loop over F_TRI check -> std::all_of
propagating_cl: manual loop with count -> none_of + count_if
currently_propagating_cl: manual loop with count -> none_of + count_if

All three now use the same vocabulary (std algorithms) as clause_falsified
and check_cl_unsat, making the intent self-documenting.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Consistent with the same pattern applied to recursive_cc_min.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…nalyzer.cpp

Two sequential for loops that summed sizes of unif_occ_long and unif_occ_bin
into total_sz are replaced with std::accumulate, consistent with the same
pattern used elsewhere in the codebase.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…epair

The index-based loop scanning for the first T_TRI literal from position 2
in a clause is replaced with std::find_if, eliminating the integer index
variable. The resulting iterator is used directly to select the block literal.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- find_disconnected: replace manual bool-flag loop (found/break) with
  std::find_if when searching for first already-assigned bag variable
- find_disconnected: replace for-loop accumulation with std::accumulate
  for total_vars check
- Add #include <numeric> for std::accumulate

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

The Counter::subset template checked whether sorted range a is a subset of
sorted range b using a manual index-based two-pointer loop. std::includes
performs exactly this operation on sorted ranges and is more expressive.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

The loop checking whether all clauses in a small component are identical
used a manual bool flag with break. Replace with std::all_of for cleaner
expression of the intent.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…ny_of

The second loop checking if any FALSE literal is at the same level as
the TRUE literal was a plain any_of pattern. Replace with std::any_of.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

The loop over clause literals building a remapped clause was a clear
transform: each literal maps to a new literal with a renamed variable.
Use std::ranges::transform to express this directly.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

On Mac, size_t (unsigned long) and uint64_t (unsigned long long) are
distinct types, causing ambiguity when calling in_mb with size_t
arguments. Replace the multiple overloads with a single template.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>