<commit_before>use satyrs::cnf::{CNF, Assignment, PartialAssignment};
use std::io;

/**
 * DPLL Algorithm implementation
 * Start by cloning the cnf so we can modify the HashMap
 * Clone might be slow, consider a faster option
 * TODO: Consider using HashSet instead of Vec for the clauses
 */
#[allow(non_snake_case)]
pub fn DPLL(cnf: &CNF) -> Option<Assignment> {
    //let _cnf = cnf.clone();
    //println!("DPLL {:?}", _cnf);
    let mut p_assn = PartialAssignment::new(cnf.nvar as usize);
    match _dpll(cnf, &mut p_assn) {
        Some(assn) => Some(assn.assignment.iter().map(|a| { 
            println!("WE HERE ");
            match *a {
                Some(a) => a,
                None => true,
            }
        }).collect()),
        None => None,
    }
}

#[allow(unused_variables)]
fn _dpll(cnf: &CNF, p_assn: &mut PartialAssignment) -> Option<PartialAssignment> {
    // If consistent set of literals, return True
    println!("{}\n{}",cnf,p_assn);
    if cnf.clauses.is_empty() {
        let _p_assn = p_assn.clone();
        return Some(_p_assn);  // Display optional value
    }

    // If contains an empty clause return None
    // TODO: Consider optimizing
    for clause in cnf.clauses.values() {
        if clause.len() == 0 {
            return None;
        }
    }

    // For every unit-clause, unit-propogate
    let mut _cnf = cnf.clone();
    for unit in cnf.units.iter() {
        let clause = cnf.clauses.get(&unit).expect("Clause not found");
        let lit : i32 = zeroth!(clause);
        p_assn.assign_literal(lit);
        _cnf.unit_propagate(*unit); // Only propogate in the clone
    } // FIXME: Unit propogate might be the end of things
    println!("After Prop! {}",_cnf);
    // Clone for the right
    let mut r_cnf = _cnf.clone();

    // TODO: For every pure literal, pure literal assign
    // Choose literal L for split
    //let literal: i32 = zeroth!(_cnf.clauses.values().next().unwrap());
    let literal = match _cnf.clauses.values().next() {
        Some(thing) => Some(zeroth!(thing)),
        None => None,
    };
    
    if literal.is_none() {
        let _p_assn = p_assn.clone();
        return Some(_p_assn);
    }
    let lit = literal.unwrap();
    println!("Split on {} ({})",lit,lit/2);
    // Propagate literal
    _cnf.propagate(lit);

    // Return DPLL with L and -L
    p_assn.assign_literal(lit);

    //let mut buffer = String::new();<commit_msg>Naive literal choice<commit_after>use satyrs::cnf::{CNF, Assignment, PartialAssignment};
use std::io;

/**
 * DPLL Algorithm implementation
 * Start by cloning the cnf so we can modify the HashMap
 * Clone might be slow, consider a faster option
 * TODO: Consider using HashSet instead of Vec for the clauses
 */
#[allow(non_snake_case)]
pub fn DPLL(cnf: &CNF) -> Option<Assignment> {
    //let _cnf = cnf.clone();
    //println!("DPLL {:?}", _cnf);
    let mut p_assn = PartialAssignment::new(cnf.nvar as usize);
    match _dpll(cnf, &mut p_assn) {
        Some(assn) => Some(assn.assignment.iter().map(|a| { 
            println!("WE HERE ");
            match *a {
                Some(a) => a,
                None => true,
            }
        }).collect()),
        None => None,
    }
}

#[allow(unused_variables)]
fn _dpll(cnf: &CNF, p_assn: &mut PartialAssignment) -> Option<PartialAssignment> {
    // If consistent set of literals, return True
    println!("{}\n{}",cnf,p_assn);
    if cnf.clauses.is_empty() {
        let _p_assn = p_assn.clone();
        return Some(_p_assn);  // Display optional value
    }

    // If contains an empty clause return None
    // TODO: Consider optimizing
    for clause in cnf.clauses.values() {
        if clause.len() == 0 {
            return None;
        }
    }

    // For every unit-clause, unit-propogate
    let mut _cnf = cnf.clone();
    for unit in cnf.units.iter() {
        let clause = cnf.clauses.get(&unit).expect("Clause not found");
        let lit : i32 = zeroth!(clause);
        p_assn.assign_literal(lit);
        _cnf.unit_propagate(*unit); // Only propogate in the clone
    } // FIXME: Unit propogate might be the end of things
    println!("After Prop! {}",_cnf);
    // Clone for the right
    let mut r_cnf = _cnf.clone();

    // TODO: For every pure literal, pure literal assign
    // Choose literal L for split
    //let literal: i32 = zeroth!(_cnf.clauses.values().next().unwrap());
    let literal = match p_assn.unassigned.iter().next();
	/*		
	match _cnf.clauses.values().next() {
        Some(thing) => Some(zeroth!(thing)),
        None => None,
    };
    */
    if literal.is_none() {
        let _p_assn = p_assn.clone();
        return Some(_p_assn);
    }
    let lit = literal.unwrap();
    println!("Split on {} ({})",lit,lit/2);
    // Propagate literal
    _cnf.propagate(lit);

    // Return DPLL with L and -L
    p_assn.assign_literal(lit);

    //let mut buffer = String::new();
{'fraction_non_alphanumeric': 0.14509883839413085, 'fraction_numerical': 0.0024454860403505196, 'mean_word_length': 2.429769392033543, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 23, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1157713', 'n_tokens_mistral': 1656, 'n_tokens_neox': 1632, 'n_words': 437}