veri_engine_lib/solver/encoded_ops/
popcnt.rs

1use crate::solver::SolverCtx;
2use easy_smt::SExpr;
3
4// Future work: possibly move these into the annotation language or an SMTLIB prelude
5
6// Encoding strategy borrowed from
7// https://github.com/fitzgen/synth-loop-free-prog/blob/6d04857693e4688eff4a36537840ba682353c2f3/src/component.rs#L219
8pub fn popcnt(s: &mut SolverCtx, ty: usize, x: SExpr, id: u32) -> SExpr {
9    let mut bits: Vec<_> = (0..ty)
10        .map(|i| s.zero_extend(7, s.smt.extract(i as i32, i as i32, x)))
11        .collect();
12    let initial = bits.pop().unwrap();
13    let r = bits.iter().fold(initial, |a, b| s.smt.bvadd(a, *b));
14
15    let id = format!("{ty}_{id}");
16    let result = s.declare(
17        format!("popcnt_{id}"),
18        s.smt.list(vec![
19            s.smt.atoms().und,
20            s.smt.atom("BitVec"),
21            s.smt.numeral(8),
22        ]),
23    );
24    s.assume(s.smt.eq(result, r));
25    result
26}