Function decode_model_from 

pub fn decode_model_from(
    atom_of: &HashMap<String, Var>,
    model: &[bool],
    exprs: &[&ProofExpr],
) -> Vec<(String, bool)>

Decode a SAT model from a pre-extracted atom→variable map (the table Cnf already holds), so a solve need not clone the whole clause database just to read its model back. Equivalent to decode_model for the propositional atoms collect_atoms gathers.