Skip to main content

decode_model

Function decode_model 

Source
pub fn decode_model(
    cnf: &Cnf,
    model: &[bool],
    exprs: &[&ProofExpr],
) -> Vec<(String, bool)>
Expand description

Decode a SAT model back to (atom, value) bindings for every source atom appearing in exprs (Tseitin auxiliaries carry no source meaning and are skipped), sorted by name.