use dimacs::Clause;

/// Convert a literal to an integer; an inverse of `Lit::from_i64`
pub(crate) fn to_i64(lit: &dimacs::Lit) -> i64 {
    lit.var().to_u64() as i64
        * match lit.sign() {
            dimacs::Sign::Pos => 1,
            dimacs::Sign::Neg => -1,
        }
}

pub trait ToDimacs {
    fn to_dimacs(&self) -> String;
}

impl ToDimacs for Clause {
    fn to_dimacs(&self) -> String {
        if self.lits().is_empty() {
            "FALSE".to_string()
        } else {
            self.lits().iter().map(|lit| format!("{}", to_i64(lit))).collect::<Vec<_>>().join(" ")
        }
    }
}
