Function weighted_model_count 

pub fn weighted_model_count(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    weight: &[(i64, i64)],
) -> i128

Symmetry-accelerated weighted model counting — the partition function Z = Σ_{m ⊨ F} W(m) with literal weights W(m) = Π_v weight[v].{1 if m[v] else 0}. The formula’s variable symmetry partitions the models into orbits, so each solve() recovers one model, its whole orbit is enumerated and its members’ weights summed, then the entire orbit is blocked — one solve per orbit instead of per model. Exact for ARBITRARY weights (every model’s true weight is summed; the symmetry only groups the search), the symmetry-aware analogue of weighted #SAT / lifted inference. Returns Z.