use std::collections::VecDeque;
use std::usize;
// solve() uses a SolveResult generator as iterator.
use genawaiter::sync::Gen;
use log::{debug, trace};
#[derive(Copy, Clone, Debug, PartialEq, Hash, Eq, PartialOrd, Ord)]
pub struct Literal {
    id: usize,
    sign: bool,
}
impl Literal {
    pub(crate) fn new(id: usize, sign: bool) -> Literal {
        Literal { id, sign }
    }
    pub fn id(&self) -> usize {
        self.id
    }
    pub fn sign(&self) -> bool {
        self.sign
    }
    pub(crate) fn negate(&self) -> Literal {
        Literal {
            id: self.id,
            sign: !self.sign,
        }
    }
}
#[test]
fn test_id() {
    let lit = Literal { id: 2, sign: false };
    assert_eq!(lit.id(), 2);
}
// TODO: Nogoods from a program
#[derive(Copy, Clone, Debug)]
pub(crate) struct WatchList {
    pub(crate) first_watch: usize,
    pub(crate) second_watch: usize,
}
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
enum Watch {
    First,
    Second,
}
/// Solver internal representation of nogoods and assignments
type Nogood = Vec<Option<bool>>;
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum SolveResult {
    UnSat,
    Sat(Vec<Option<bool>>),
}
#[derive(Clone, Debug, PartialEq)]
enum PropagationResult {
    Ok,
    Conflict(Nogood),
}
/// Map implementation used by the library.
pub(crate) type Map<K, V> = rustc_hash::FxHashMap<K, V>;
#[derive(Clone, Debug)]
pub struct Solver {
    pub(crate) tight: bool,
    pub(crate) number_of_variables: usize,
    pub(crate) assignments: Vec<Option<bool>>,
    pub(crate) decisions: Vec<Literal>,
    pub(crate) watch_lists: Vec<WatchList>,
    pub(crate) nogoods: Vec<Nogood>,
    pub(crate) var_to_nogoods: Vec<Map<usize, bool>>,
    pub(crate) nogoods_to_var: Vec<Map<usize, bool>>,
    pub(crate) decision_level: usize,
    pub(crate) decision_number: usize,
    // Stores for each atom that has been decided the (sign, reason_index, decision_level, and decision number)
    pub(crate) assignments_log: Vec<(Option<bool>, Option<usize>, usize, usize)>,
    pub(crate) chronological_backtracking_level: usize,
}
impl Solver {
    pub fn solve(&mut self) -> impl Iterator<Item = SolveResult> + '_ {
        Gen::new(|co| async move {
            let mut sat = true;
            while sat {
                if let PropagationResult::Conflict(nogood) = self.propagate() {
                    trace!("conflict with nogood: {:?}",nogood);
                    if self.is_top_level_conflict(&nogood) {
                        sat = false;
                        co.yield_(SolveResult::UnSat).await;
                    } else if self.chronological_backtracking_level < self.decision_level {
                        let (uip, sigma, k) = self.conflict_resolution(&nogood);
                        debug!("uip: {:?}", &uip);
                        debug!("sigma: {:?}", sigma);
                        debug!("k: {:?}", k);
                        if self.chronological_backtracking_level > k {
                            self.decision_level = self.chronological_backtracking_level;
                        } else {
                            self.decision_level = k;
                        }
                        debug!("new_decision_level: {}", self.decision_level);
                        self.backjump();
                        // add complement of sigma
                        self.decision_number += 1;
                        self.assignments[sigma.id] = Some(!sigma.sign);
                        self.assignments_log[sigma.id] =
                            (Some(!sigma.sign), None, k, self.decision_number);
                        self.record_nogood(uip);
                    } else {
                        //get decision literal from this decision_level
                        let decision_literal = self.decisions[self.decision_level - 1];
                        self.decision_level -= 1;
                        self.chronological_backtracking_level = self.decision_level;
                        self.backjump();
                        // add complement of the decision literal
                        self.decision_number += 1;
                        self.assignments[decision_literal.id] = Some(!decision_literal.sign);
                        self.assignments_log[decision_literal.id] = (
                            Some(!decision_literal.sign),
                            None,
                            self.decision_level,
                            self.decision_number,
                        );
                    }
                } else if self.assignment_complete() {
                    co.yield_(SolveResult::Sat(self.assignments.clone())).await;
                    if self.decision_level == 0 {
                        return;
                    } else {
                        // get decision literal from this decision_level
                        let decision_literal = self.decisions[self.decision_level - 1];
                        // debug!("flip decision literal {:?}", decision_literal);
                        self.decision_level -= 1;
                        debug!("decision_level: {}", self.decision_level);
                        self.chronological_backtracking_level = self.decision_level;
                        debug!(
                            "chronological_backtracking_level: {}",
                            self.chronological_backtracking_level
                        );
                        self.backjump();
                        // add complement of the decision literal
                        self.decision_number += 1;
                        self.assignments[decision_literal.id] = Some(!decision_literal.sign);
                        self.assignments_log[decision_literal.id] = (
                            Some(!decision_literal.sign),
                            None,
                            self.decision_level,
                            self.decision_number,
                        );
                    }
                } else {
                    self.decide()
                }
            }
        })
        .into_iter()
    }
    fn record_nogood(&mut self, nogood: Nogood) {
        self.watch_lists.push(nogood_to_watch_list(&nogood));
        self.nogoods.push(nogood);
        let nogood_id = self.nogoods.len() - 1;
        for variable_id in 0..self.number_of_variables {
            if let Some(sign) = self.nogoods[nogood_id][variable_id] {
                self.var_to_nogoods[variable_id].insert(nogood_id, sign);
                self.nogoods_to_var.push(Map::default());
                self.nogoods_to_var[nogood_id].insert(variable_id, sign);
            }
        }
    }
    /// Analyze conflict and learn UIP nogood
    fn conflict_resolution(&self, nogood: &[Option<bool>]) -> (Nogood, Literal, usize) {
        let mut nogood = nogood.to_owned();
        let sigma = loop {
            debug!("delta: {:?}", nogood);
            let iter = nogood.iter().enumerate();
            // Determine sigma the last literal in delta that has been added to the assignment
            let mut sigma = Literal { id: 0, sign: true };
            let mut nogood_index = None;
            let mut decision_level_sigma = 0;
            let mut biggest_decision_number = 0;
            for (id, assignment) in iter {
                if let Some(sign) = *assignment {
                    let (_, ng_index, decision_level, decision_number) = self.assignments_log[id];
                    if decision_number >= biggest_decision_number {
                        biggest_decision_number = decision_number;
                        sigma = Literal { id, sign };
                        nogood_index = ng_index;
                        decision_level_sigma = decision_level;
                    }
                }
            }
            debug!("sigma: {:?}", sigma);
            // A nogood is a unique implication point if there is no other literal
            // from the same decision level as sigma
            let mut iter = nogood.iter().enumerate();
            let unique = loop {
                match iter.next() {
                    Some((id, &Some(sign))) => {
                        let literal = Literal { id, sign };
                        if sigma != literal {
                            // debug!("literal: {:?}", literal);
                            let (_, _, decision_level, _) = self.assignments_log[literal.id];
                            if decision_level == decision_level_sigma {
                                break false;
                            }
                        }
                    }
                    Some((_, &None)) => {}
                    None => break true,
                }
            };
            if unique {
                break sigma;
            }
            // debug!("not unique");
            if let Some(nogood_index) = nogood_index {
                let reason = &self.nogoods[nogood_index];
                debug!("reason: {:?}", reason);
                let res = resolve(&nogood, &sigma, reason);
                nogood = res;
            } else {
                // sigma is a decision_literals
                // the reason is empty
                let reason: Vec<Option<bool>> = vec![None; self.number_of_variables];
                // debug!("reason: {:?}", reason);
                let res = resolve(&nogood, &sigma, &reason);
                nogood = res;
            }
        };
        let mut k = 0;
        for (id, assignment) in nogood.iter().enumerate() {
            if let Some(sign) = *assignment {
                let literal = Literal { id, sign };
                if literal != sigma {
                    let (_, _, decision_level, _) = self.assignments_log[literal.id];
                    if decision_level > k {
                        k = decision_level
                    }
                }
            }
        }
        // debug!("k: {}", k);
        // debug!("sigma: {:?}", sigma);
        (nogood, sigma, k)
    }
    /// Increase decision level assign truth value to a previously unassigned variable
    fn decide(&mut self) {
        self.decision_level += 1;
        self.decision_number += 1;
        debug!("decision_level: {:?}", self.decision_level);
        let decision_literal = self.choose();
        debug!("decision_literal: {:?}", decision_literal);
        self.assignments[decision_literal.id()] = Some(decision_literal.sign);
        self.decisions.push(decision_literal);
        self.assignments_log[decision_literal.id] = (
            Some(decision_literal.sign),
            None,
            self.decision_level,
            self.decision_number,
        );
    }
    fn choose(&self) -> Literal {
        for id in 0..self.number_of_variables {
            if self.assignments[id] == Some(true) {
                continue;
            }
            if self.assignments[id] == Some(false) {
                continue;
            }
            return Literal { id, sign: true };
        }
        panic!("Logic error: calling choose on complete assignment-");
    }
    /// Return true if all variables have a truth value assignment
    fn assignment_complete(&self) -> bool {
        for id in 0..self.number_of_variables {
            if self.assignments[id] == Some(true) {
                continue;
            }
            if self.assignments[id] == Some(false) {
                continue;
            }
            return false;
        }
        true
    }
    /// Return true if there is a conflict on decision level 0
    fn is_top_level_conflict(&self, nogood: &[Option<bool>]) -> bool {
        for (id, assignment) in nogood.iter().enumerate() {
            if assignment.is_some() {
                let (_, _, decision_level, _) = self.assignments_log[id];
                if decision_level > 0 {
                    return false;
                }
            }
        }
        true
    }
    /// Backjump to decision level x and rewind assignment
    fn backjump(&mut self) {
        // debug!("backjump to decision_level {}", self.decision_level);
        for (id, assignment) in self.assignments.iter_mut().enumerate() {
            if let Some(sign) = *assignment {
                let lit = Literal { id, sign };
                let (_, _, decision_level, decision_number) = self.assignments_log[lit.id];
                if decision_level > self.decision_level {
                    self.assignments_log[lit.id] = (None, None, 0, 0);
                    *assignment = None;
                }
                if decision_number > self.decision_number {
                    self.decision_number = decision_number - 1;
                }
            }
        }
        // backtrack decisions
        while self.decisions.len() > self.decision_level {
            self.decisions.pop();
        }
    }
    /// Run unit propagation and unfounded set check
    fn propagate(&mut self) -> PropagationResult {
        trace!("propagate");
        trace!("assignment: {:?}", self.assignments);
        if let PropagationResult::Conflict(nogood) = self.unit_propagation() {
            return PropagationResult::Conflict(nogood);
        }
        if !self.tight {
            self.unfounded_loop_learning();
        }
        PropagationResult::Ok
    }
    /// Learn a nogood for an unfounded loop
    fn unfounded_loop_learning(&mut self) {
        todo!()
    }
    fn unit_propagation(&mut self) -> PropagationResult {
        let mut propagation_queue: VecDeque<Literal> = VecDeque::new();
        for (id, assignment) in self.assignments.iter().enumerate() {
            if let Some(sign) = *assignment {
                propagation_queue.push_back(Literal { id, sign });
            }
        }
        loop {
            if let Some(p) = propagation_queue.pop_front() {
                debug!("prp: {:?}", p);
                for (index, sign) in &self.var_to_nogoods[p.id] {
                    let watch_list = &mut self.watch_lists[*index];
                    // debug!(
                    //     "wl.0: {} wl.1: {} nogood: {:?}",
                    //     watch_list.first_watch, watch_list.second_watch, self.nogoods[*index]
                    // );
                    if watch_list.first_watch == p.id || watch_list.second_watch == p.id {
                        let dirty_watch = if watch_list.first_watch == p.id {
                            Watch::First
                        } else {
                            Watch::Second
                        };
                        if *sign == p.sign {
                            // propagated literal and nogood literal have the same sign
                            // try to update watch
                            if let Some(new_watch) = update_watches(
                                &self.nogoods_to_var[*index],
                                &self.assignments,
                                p,
                                watch_list.first_watch,
                                watch_list.second_watch,
                            ) {
                                if dirty_watch == Watch::First {
                                    watch_list.first_watch = new_watch;
                                } else {
                                    watch_list.second_watch = new_watch;
                                }
                                continue;
                            } else {
                                // debug!("one watch could not be updated. it's a conflict or an implication.");
                                let other_watch = if dirty_watch == Watch::First {
                                    &mut watch_list.second_watch
                                } else {
                                    &mut watch_list.first_watch
                                };
                                // debug!("check the other watch");
                                let sign = self.nogoods_to_var[*index][other_watch];
                                match self.assignments[*other_watch] {
                                    Some(x) => {
                                        if sign == x {
                                            // also the other watched literal is in the assignment. it's a conflict
                                            return PropagationResult::Conflict(
                                                self.nogoods[*index].clone(),
                                            );
                                        }
                                    }
                                    None => {
                                        // the other watch is unassigned. we can imply the complement
                                        let complement = !sign;
                                        self.assignments[*other_watch] = Some(complement);
                                        let lit = Literal {
                                            id: *other_watch,
                                            sign: complement,
                                        };
                                        debug!("infer: {:?}", lit);
                                        self.decision_number += 1;
                                        propagation_queue.push_back(lit);
                                        self.assignments_log[*other_watch] = (
                                            Some(complement),
                                            Some(*index),
                                            self.decision_level,
                                            self.decision_number,
                                        );
                                        debug!(
                                            "infer2: {:?} {:?}",
                                            *other_watch,
                                            (Some(complement), Some(*index), self.decision_level)
                                        );
                                    }
                                }
                            }
                        }
                    }
                }
            }
            if propagation_queue.is_empty() {
                return PropagationResult::Ok;
            }
        }
    }
}
fn update_watches(
    nogood_vars: &Map<usize, bool>,
    assignments: &[Option<bool>],
    p: Literal,
    first_watch: usize,
    second_watch: usize,
) -> Option<usize> {
    for (id, sign) in nogood_vars {
        if *id != p.id
            && *id != first_watch
            && *id != second_watch
            && assignments[*id] != Some(*sign)
        {
            return Some(*id);
        }
    }
    None
}
fn resolve(nogood: &[Option<bool>], sigma: &Literal, reason: &[Option<bool>]) -> Nogood {
    // assert sigma in nogood and reason
    let mut res = vec![];
    for (id, assignment) in nogood.iter().enumerate() {
        match *assignment {
            Some(sign) => {
                let literal = Literal { id, sign };
                if literal != *sigma {
                    res.push(Some(sign))
                } else {
                    res.push(None)
                }
            }
            None => res.push(None),
        }
    }
    let neg_sigma = sigma.negate();
    for (id, assignment) in reason.iter().enumerate() {
        if let Some(sign) = *assignment {
            let literal = Literal { id, sign };
            if literal != neg_sigma {
                res[id] = Some(sign);
            }
        }
    }
    res
}
fn nogood_to_watch_list(nogood: &[Option<bool>]) -> WatchList {
    //  TODO: special handling for nogoods of size 1
    let mut first_watch = 0;
    while nogood[first_watch].is_none() {
        first_watch += 1;
    }
    let mut second_watch = nogood.len() - 1;
    while nogood[second_watch].is_none() {
        second_watch -= 1;
    }
    WatchList {
        first_watch,
        second_watch,
    }
}
// only for tests
fn create_watch_lists(nogoods: &[Vec<Option<bool>>]) -> Vec<WatchList> {
    let mut watch_lists = vec![];
    for nogood in nogoods {
        //  TODO: special handling for nogoods of size 1
        watch_lists.push(nogood_to_watch_list(nogood))
    }
    watch_lists
}
/// only for testing
fn mock_decide(solver: &mut Solver) {
    solver.decision_level += 1;
    solver.decision_number += 1;
    solver.assignments[0] = Some(true);
    solver.assignments_log[0] = (
        Some(true),
        None,
        solver.decision_level,
        solver.decision_number,
    );
}
/// only for testing
fn mock_decide2(solver: &mut Solver) {
    solver.decision_level += 1;
    solver.decision_number += 1;
    solver.assignments[2] = Some(true);
    solver.assignments_log[2] = (
        Some(true),
        None,
        solver.decision_level,
        solver.decision_number,
    );
}
#[test]
fn test_unit_propagation() {
    let solver_nogoods = vec![vec![None, Some(true), Some(false)]];
    let number_of_variables = 3;
    let mut var_to_nogoods: Vec<Map<usize, bool>> = vec![Map::default(); number_of_variables];
    let mut nogoods_to_var: Vec<Map<usize, bool>> = vec![Map::default(); solver_nogoods.len()];
    for nogood_id in 0..solver_nogoods.len() {
        for variable_id in 0..number_of_variables {
            if let Some(sign) = solver_nogoods[nogood_id][variable_id] {
                var_to_nogoods[variable_id].insert(nogood_id, sign);
                nogoods_to_var[nogood_id].insert(variable_id, sign);
            }
        }
    }
    let mut solver = Solver {
        tight: true,
        number_of_variables,
        assignments: vec![None, Some(true), None],
        decisions: vec![Literal { id: 1, sign: true }],
        watch_lists: vec![],
        nogoods: solver_nogoods,
        var_to_nogoods,
        nogoods_to_var,
        decision_level: 0,
        decision_number: 0,
        assignments_log: vec![(None, None, 0, 0); number_of_variables],
        chronological_backtracking_level: 0,
    };
    solver.watch_lists = create_watch_lists(&solver.nogoods);
    solver.unit_propagation();
    let res = &solver.assignments;
    assert_eq!(*res, vec![None, Some(true), Some(true)]);
}
#[test]
fn test_unit_propagation_conflict() {
    use crate::convert::Builder;
    let builder = Builder {
        nogoods: vec![
            vec![
                Literal { id: 0, sign: true },
                Literal { id: 1, sign: false },
            ],
            vec![
                Literal { id: 1, sign: true },
                Literal { id: 2, sign: false },
            ],
            vec![Literal { id: 1, sign: true }, Literal { id: 2, sign: true }],
        ],
    };
    let mut solver = builder.build();
    mock_decide(&mut solver); // assign Literal(0)
    let prop_result = solver.unit_propagation();
    if let PropagationResult::Conflict(nogood) = prop_result {
        assert_eq!(nogood, vec![None, Some(true), Some(true)]);
        let top_level_conflict = solver.is_top_level_conflict(&nogood);
        assert_eq!(top_level_conflict, false);
        let (uip, sigma, k) = solver.conflict_resolution(&nogood);
        assert_eq!(uip, vec![None, Some(true), None]);
        assert_eq!(sigma, Literal { id: 1, sign: true });
        if solver.chronological_backtracking_level > k {
            solver.decision_level = solver.chronological_backtracking_level;
        } else {
            solver.decision_level = k;
        }
        println!("new_decision_level: {}", solver.decision_level);
        solver.backjump();
        // add complement of sigma
        solver.decision_number += 1;
        solver.assignments[sigma.id] = Some(!sigma.sign);
        solver.assignments_log[sigma.id] = (Some(!sigma.sign), None, k, solver.decision_number);
        solver.record_nogood(uip);
        let res = solver.unit_propagation();
        assert_eq!(res, PropagationResult::Ok);
        assert_eq!(solver.assignments, vec![Some(false), Some(false), None]);
        mock_decide2(&mut solver); // assign Literal(2)
        let res = solver.unit_propagation();
        assert_eq!(res, PropagationResult::Ok);
        assert_eq!(
            solver.assignments,
            vec![Some(false), Some(false), Some(true)]
        );
        assert_eq!(solver.assignment_complete(), true);
    }
}
#[test]
pub fn test_solve_1() {
    use crate::convert::Builder;
    let builder = Builder {
        nogoods: vec![
            vec![
                Literal { id: 0, sign: true },
                Literal { id: 1, sign: false },
            ],
            vec![
                Literal { id: 1, sign: true },
                Literal { id: 2, sign: false },
            ],
            vec![Literal { id: 1, sign: true }, Literal { id: 2, sign: true }],
        ],
    };
    let mut solver = builder.build();
    let mut solutions = solver.solve();
    let res = solutions.next();
    assert_eq!(
        res,
        Some(SolveResult::Sat(vec![Some(false), Some(false), Some(true)]))
    );
    let res = solutions.next();
    assert_eq!(
        res,
        Some(SolveResult::Sat(vec![
            Some(false),
            Some(false),
            Some(false)
        ]))
    );
    let res = solutions.next();
    assert_eq!(res, None);
}
#[test]
pub fn test_solve_unsat_1() {
    use crate::convert::Builder;
    let builder = Builder {
        nogoods: vec![
            vec![Literal { id: 0, sign: true }],
            vec![Literal { id: 0, sign: false }],
        ],
    };
    let mut solver = builder.build();
    let mut solutions = solver.solve();
    let res = solutions.next();
    assert_eq!(res, Some(SolveResult::UnSat));
    let res = solutions.next();
    assert_eq!(res, None);
}
#[test]
pub fn test_solve_unsat_2() {
    use crate::convert::Builder;
    let builder = Builder {
        nogoods: vec![
            vec![Literal { id: 1, sign: true }],
            vec![Literal { id: 1, sign: false }],
        ],
    };
    let mut solver = builder.build();
    let mut solutions = solver.solve();
    let res = solutions.next();
    assert_eq!(res, Some(SolveResult::UnSat));
    let res = solutions.next();
    assert_eq!(res, None);
}
pub fn create_test_solver() -> Solver {
    use crate::convert::Builder;
    let builder = Builder {
        nogoods: vec![
            vec![
                Literal { id: 3, sign: false },
                Literal { id: 2, sign: true },
            ],
            vec![
                Literal { id: 0, sign: false },
                Literal { id: 5, sign: true },
            ],
            vec![
                Literal { id: 7, sign: false },
                Literal { id: 4, sign: false },
                Literal { id: 6, sign: true },
            ],
            vec![
                Literal { id: 3, sign: false },
                Literal { id: 9, sign: true },
            ],
            vec![
                Literal { id: 0, sign: false },
                Literal { id: 7, sign: false },
                Literal { id: 10, sign: true },
            ],
            vec![
                Literal { id: 1, sign: false },
                Literal { id: 12, sign: true },
            ],
            vec![
                Literal { id: 0, sign: true },
                Literal { id: 5, sign: false },
                Literal {
                    id: 11,
                    sign: false,
                },
            ],
            vec![
                Literal { id: 7, sign: true },
                Literal { id: 8, sign: false },
                Literal { id: 8, sign: false },
            ],
            vec![
                Literal { id: 4, sign: true },
                Literal { id: 5, sign: false },
            ],
            vec![
                Literal { id: 1, sign: true },
                Literal {
                    id: 12,
                    sign: false,
                },
            ],
            vec![
                Literal { id: 3, sign: true },
                Literal { id: 2, sign: false },
                Literal { id: 9, sign: false },
            ],
            vec![Literal { id: 8, sign: true }, Literal { id: 7, sign: true }],
            vec![
                Literal { id: 8, sign: false },
                Literal { id: 7, sign: false },
            ],
            vec![
                Literal { id: 9, sign: true },
                Literal { id: 4, sign: false },
                Literal { id: 7, sign: true },
            ],
            vec![
                Literal { id: 9, sign: true },
                Literal { id: 4, sign: true },
                Literal { id: 7, sign: false },
            ],
            vec![
                Literal { id: 9, sign: false },
                Literal { id: 4, sign: true },
                Literal { id: 7, sign: true },
            ],
            vec![
                Literal { id: 11, sign: true },
                Literal { id: 0, sign: true },
            ],
            vec![
                Literal {
                    id: 11,
                    sign: false,
                },
                Literal { id: 0, sign: false },
            ],
            vec![
                Literal { id: 5, sign: true },
                Literal { id: 3, sign: false },
                Literal { id: 4, sign: false },
            ],
            vec![
                Literal { id: 5, sign: true },
                Literal { id: 3, sign: true },
                Literal { id: 4, sign: true },
            ],
            vec![
                Literal { id: 5, sign: false },
                Literal { id: 3, sign: true },
                Literal { id: 4, sign: false },
            ],
            vec![
                Literal { id: 10, sign: true },
                Literal { id: 1, sign: true },
            ],
            vec![
                Literal {
                    id: 10,
                    sign: false,
                },
                Literal { id: 1, sign: false },
            ],
            vec![
                Literal { id: 12, sign: true },
                Literal { id: 0, sign: true },
                Literal { id: 7, sign: false },
            ],
            vec![
                Literal { id: 12, sign: true },
                Literal { id: 0, sign: false },
                Literal { id: 7, sign: true },
            ],
            vec![
                Literal {
                    id: 12,
                    sign: false,
                },
                Literal { id: 0, sign: false },
                Literal { id: 7, sign: false },
            ],
            vec![
                Literal { id: 6, sign: true },
                Literal { id: 3, sign: false },
            ],
            vec![
                Literal { id: 6, sign: false },
                Literal { id: 3, sign: true },
            ],
            vec![
                Literal { id: 2, sign: true },
                Literal { id: 0, sign: false },
                Literal { id: 1, sign: false },
            ],
            vec![
                Literal { id: 2, sign: true },
                Literal { id: 0, sign: true },
                Literal { id: 1, sign: true },
            ],
            vec![
                Literal { id: 2, sign: false },
                Literal { id: 0, sign: true },
                Literal { id: 1, sign: false },
            ],
        ],
    };
    builder.build()
}

pub mod convert;
pub mod solver;
use thiserror::Error;
#[derive(Error, Debug)]
pub enum AspifError {
    #[error("More than one solve item")]
    MultipleSolveItems,
    #[error("No solve item")]
    NoSolveItem,
    #[error("ParseError: {msg}")]
    ParseError { msg: String },
}

use crate::solver::{Literal, Map, Solver, WatchList};
use aspif::AspifProgram;
use log::{debug, info};
use string_interner::symbol::SymbolU32;
use string_interner::StringInterner;
#[derive(Default)]
pub struct LiteralMapper {
    aspif_literals: Map<u64, usize>,
    pub bodies: Map<Vec<Literal>, usize>,
    literal_count: usize,
    supports: Map<usize, Vec<(Vec<Literal>, Vec<Literal>)>>,
}
impl LiteralMapper {
    fn u64_to_solver_literal(&mut self, a: &u64) -> Literal {
        if let Some((_key, value)) = self.aspif_literals.get_key_value(a) {
            Literal::new(*value, true)
        } else {
            self.aspif_literals.insert(*a, self.literal_count);
            let literal = Literal::new(self.literal_count, true);
            self.literal_count += 1;
            literal
        }
    }
    fn i64_to_solver_literal(&mut self, a: &i64) -> Literal {
        if *a >= 0 {
            let b = *a as u64;
            if let Some((_key, value)) = self.aspif_literals.get_key_value(&b) {
                Literal::new(*value, true)
            } else {
                self.aspif_literals.insert(b, self.literal_count);
                let literal = Literal::new(self.literal_count, true);
                self.literal_count += 1;
                literal
            }
        } else {
            let b = -a as u64;
            if let Some((_key, value)) = self.aspif_literals.get_key_value(&b) {
                Literal::new(*value, false)
            } else {
                self.aspif_literals.insert(b, self.literal_count);
                let literal = Literal::new(self.literal_count, false);
                self.literal_count += 1;
                literal
            }
        }
    }
    /// Returns corresponding solver literal if the body already exist in the LiteralMap
    /// else creates a new entry and returns the literal
    fn body2solver_literal(&mut self, body: &[Literal]) -> Literal {
        if let Some((_key, value)) = self.bodies.get_key_value(body) {
            Literal::new(*value, true)
        } else {
            self.bodies.insert(body.to_owned(), self.literal_count);
            let literal = Literal::new(self.literal_count, true);
            self.literal_count += 1;
            literal
        }
    }
    /// Returns corresponding solver literal if the body already exist in the LiteralMap
    fn get_body_literal(&self, body: &[Literal]) -> Option<Literal> {
        self.bodies
            .get(body)
            .map(|value| Literal::new(*value, true))
    }
    /// This function creates rule nogoods as in Definition 1 in *Advanced Conflict-Driven Disjunctive Answer Set Solving*
    /// It also collects support body clauses for atom wise shifted rules as in *Advanced Conflict-Driven Disjunctive Answer Set Solving*
    fn write_rule_nogood(&mut self, rule: &aspif::Rule, nogoods: &mut Vec<Vec<Literal>>) {
        let body_clause = match &rule.body {
            aspif::Body::NormalBody { elements } => {
                // Create clause that makes the body true
                let mut body_clause = vec![];
                for e in elements {
                    body_clause.push(self.i64_to_solver_literal(e));
                }
                // TODO: is sort and dedup here necessary ?
                body_clause.sort();
                body_clause.dedup();
                body_clause
            }
            aspif::Body::WeightBody {
                lowerbound: _,
                elements: _,
            } => {
                panic!("Unsupported Body")
            }
        };
        match &rule.head {
            aspif::Head::Disjunction { elements } => {
                let ori_body_lit = self.body2solver_literal(&body_clause);
                debug!("Body_lit:{:?} -> {:?}", ori_body_lit, body_clause);
                // Create rule nogood
                let mut rule_nogood = vec![];
                for e in elements {
                    let head_lit = self.u64_to_solver_literal(e);
                    let neg_head_lit = head_lit.negate();
                    rule_nogood.push(neg_head_lit)
                }
                rule_nogood.push(ori_body_lit);
                debug!("Rule nogood: {rule_nogood:?}");
                nogoods.push(rule_nogood);
                // Shift head atoms to the new body
                for (idx, e) in elements.iter().enumerate() {
                    let new_head_lit = self.u64_to_solver_literal(e);
                    let mut body_extension = vec![];
                    for (idx2, e) in elements.iter().enumerate() {
                        if idx2 != idx {
                            let lit2 = self.u64_to_solver_literal(e);
                            let neg_lit = lit2.negate();
                            body_extension.push(neg_lit);
                        }
                    }
                    // debug!("Support for {new_head_lit:?}: {:?}{:?}",body_clause,body_extension);
                    self.supports
                        .entry(new_head_lit.id())
                        .and_modify(|e| e.push((body_clause.clone(), body_extension.clone())))
                        .or_insert(vec![(body_clause.clone(), body_extension)]);
                }
            }
            aspif::Head::Choice { elements } => {
                panic!("Unsupported Head : Choice")
            }
        };
    }
    /// This function creates support nogoods as in Definition 2 in *Advanced Conflict-Driven Disjunctive Answer Set Solving*
    fn write_support_nogoods(&mut self, nogoods: &mut Vec<Vec<Literal>>) {
        for (k, support) in &self.supports {
            let mut support_nogood = vec![];
            // Create support nogoods
            support_nogood.push(Literal::new(*k, true));
            for (old_body, extension) in support {
                let mut new_body = old_body.clone();
                new_body.extend_from_slice(extension);
                if let Some(lit) = self.get_body_literal(&new_body) {
                    // new_body is known
                    let neg_lit = lit.negate();
                    support_nogood.push(neg_lit);
                } else if let Some(lit) = self.get_body_literal(old_body) {
                    let neg_lit = lit.negate();
                    support_nogood.push(neg_lit);
                    for lit in extension {
                        let neg_lit = lit.negate();
                        support_nogood.push(neg_lit);
                    }
                } else {
                    unreachable!()
                }
            }
            debug!("Support nogood: {:?}", support_nogood);
            nogoods.push(support_nogood);
        }
    }
    /// This function creates conjunction nogoods as in Definition 3 in *Advanced Conflict-Driven Disjunctive Answer Set Solving*
    fn write_conjuction_nogoods(&self, nogoods: &mut Vec<Vec<Literal>>) {
        for (body, lit_id) in &self.bodies {
            debug!("CNG  lit:{} body{:?}", lit_id, body);
            let mut conjunction_nogood1 = vec![];
            let lit = Literal::new(*lit_id, true);
            let neg_lit = Literal::new(*lit_id, false);
            conjunction_nogood1.push(neg_lit);
            for l in body.iter() {
                conjunction_nogood1.push(*l);
                let mut conjunction_nogoodn = vec![lit];
                conjunction_nogoodn.push(l.negate());
                debug!("Conjunction nogood: {:?}", conjunction_nogoodn);
                nogoods.push(conjunction_nogoodn);
            }
            debug!("Conjunction nogood: {:?}", conjunction_nogood1);
            nogoods.push(conjunction_nogood1);
        }
    }
}
#[test]
fn test_aspif_i64_to_solver_literal() {
    let mut lm = LiteralMapper::default();
    let l0 = Literal::new(0, true);
    let l1 = Literal::new(1, false);
    let l2 = Literal::new(0, false);
    let l3 = Literal::new(1, true);
    let sl0 = lm.i64_to_solver_literal(&12);
    let sl1 = lm.i64_to_solver_literal(&-2);
    let sl2 = lm.i64_to_solver_literal(&-12);
    let sl3 = lm.i64_to_solver_literal(&-2);
    let sl4 = lm.i64_to_solver_literal(&2);
    assert_eq!(l0, sl0);
    assert_eq!(l1, sl1);
    assert_eq!(l2, sl2);
    assert_eq!(l1, sl3);
    assert_eq!(l3, sl4);
}
#[test]
fn test_aspif_u64_to_solver_literal() {
    let mut lm = LiteralMapper::default();
    let l0 = Literal::new(0, true);
    let l1 = Literal::new(1, false);
    let l2 = Literal::new(0, false);
    let l3 = Literal::new(1, true);
    let sl0 = lm.u64_to_solver_literal(&12);
    let sl1 = lm.i64_to_solver_literal(&-2);
    let sl2 = lm.i64_to_solver_literal(&-12);
    let sl3 = lm.u64_to_solver_literal(&2);
    assert_eq!(l0, sl0);
    assert_eq!(l1, sl1);
    assert_eq!(l2, sl2);
    assert_eq!(l3, sl3);
}
#[test]
fn test_body_to_solver_literal() {
    // TODO
    // let mut lm = LiteralMapper::default();
    // let la = Literal::new(0, true);
    // let lb = Literal::new(1, false);
    // let lc = Literal::new(0, false);
    // let ld = Literal::new(1, true);
    // let sl0 = lm.body2solver_literal(&[la,lb]);
    // let sl1 = lm.body2solver_literal(&[lb,lc]);
    // let sl2 = lm.body2solver_literal(&[lc,ld]);
    // let sl3 = lm.body2solver_literal(&[lb,ld]);
    // let l0 = Literal::new(2, true);
    // let l1 = Literal::new(3, true);
    // let l2 = Literal::new(4, true);
    // let l3 = Literal::new(5, true);
    // assert_eq!(l0, sl0);
    // assert_eq!(l1, sl1);
    // assert_eq!(l2, sl2);
    // assert_eq!(l3, sl3);
}
pub type SymbolMapper = Map<Vec<Literal>, SymbolU32>;
fn insert_into_symbol_mapper(
    symbol_mapper: &mut SymbolMapper,
    literal_mapper: &mut LiteralMapper,
    symbol: SymbolU32,
    condition: &[i64],
) {
    let mut new_condition = vec![];
    for e in condition {
        new_condition.push(literal_mapper.i64_to_solver_literal(e));
    }
    // TODO: This is buggy if there could be multiple symbols with the same condition
    // q :- not p.
    // p :- not q.
    // #show t:p.
    symbol_mapper.insert(new_condition, symbol);
}
use petgraph::algo::tarjan_scc;
use petgraph::graph::{DiGraph, NodeIndex};
/// Create a (directed) positive atom dependency graph
/// The graph will be used to compute scc's which correspond to loops of the program
pub fn graph_from_aspif(aspif_program: &AspifProgram) {
    let mut literal_mapper = LiteralMapper::default();
    let mut positive_atom_dependency_graph: DiGraph<u32, ()> = DiGraph::default();
    for statement in &aspif_program.statements {
        debug!("stmt:{:?}", statement);
        match statement {
            aspif::Statement::Rule(rule) => {
                let body_clause = match &rule.body {
                    aspif::Body::NormalBody { elements } => {
                        let mut body_clause = vec![];
                        for e in elements {
                            body_clause.push(literal_mapper.i64_to_solver_literal(e));
                        }
                        body_clause.sort();
                        body_clause
                    }
                    aspif::Body::WeightBody {
                        lowerbound: _,
                        elements: _,
                    } => {
                        panic!("Unsupported Body")
                    }
                };
                match &rule.head {
                    aspif::Head::Disjunction { elements } => {
                        for body_lit in &body_clause {
                            if body_lit.sign() {
                                for head_atom_id in elements {
                                    while positive_atom_dependency_graph.node_count()
                                        <= *head_atom_id as usize
                                    {
                                        let _a = positive_atom_dependency_graph.add_node(0);
                                    }
                                    let a = NodeIndex::from(*head_atom_id as u32);
                                    while positive_atom_dependency_graph.node_count()
                                        <= body_lit.id()
                                    {
                                        let _a = positive_atom_dependency_graph.add_node(0);
                                    }
                                    let b = NodeIndex::from(body_lit.id() as u32);
                                    positive_atom_dependency_graph.add_edge(a, b, ());
                                }
                            }
                        }
                    }
                    aspif::Head::Choice { elements } => {
                        panic!("Unsupported Head : Choice")
                    }
                }
            }
            // aspif::Statement::Minimize(_) => todo!(),
            // aspif::Statement::Projection(_) => todo!(),
            aspif::Statement::Output(_) => {}
            // aspif::Statement::External { atom, init } => todo!(),
            // aspif::Statement::Assumption(_) => todo!(),
            // aspif::Statement::Heuristic {
            //     modifier,
            //     atom,
            //     k,
            //     priority,
            //     condition,
            // } => todo!(),
            // aspif::Statement::Edge { u, v, condition } => todo!(),
            // aspif::Statement::NumericTheoryTerm { id, w } => todo!(),
            // aspif::Statement::SymbolicTheoryTerm { id, string } => todo!(),
            // aspif::Statement::CompoundTheoryTerm { id, t, terms } => todo!(),
            // aspif::Statement::TheoryAtomElements {
            //     id,
            //     theory_terms,
            //     literals,
            // } => todo!(),
            // aspif::Statement::TheoryAtom {
            //     atom,
            //     symbolic_term,
            //     theory_atom_elements,
            //     theory_operation,
            // } => todo!(),
            // aspif::Statement::TheoryDirective {
            //     symbolic_term,
            //     theory_atom_elements,
            //     theory_operation,
            // } => todo!(),
            // aspif::Statement::Comment => todo!(),
            _ => {
                panic!("Unsupported Statement");
            }
        }
    }
    debug!("positive_atom_dependency_graph: {positive_atom_dependency_graph:?}");
    info!("Strongly connected components ...");
    let components = tarjan_scc(&positive_atom_dependency_graph);
    for scc in components {
        debug!("{scc:?}");
    }
}
pub struct Builder {
    pub(crate) nogoods: Vec<Vec<Literal>>,
}
impl Builder {
    pub fn from_aspif(aspif_program: &AspifProgram) -> (Self, SymbolMapper, StringInterner) {
        let mut interner = StringInterner::default();
        let mut literal_mapper = LiteralMapper::default();
        let mut symbol_mapper = SymbolMapper::default();
        let mut nogoods = vec![];
        for statement in &aspif_program.statements {
            match statement {
                aspif::Statement::Rule(rule) => {
                    literal_mapper.write_rule_nogood(rule, &mut nogoods);
                }
                // aspif::Statement::Minimize(_) => todo!(),
                // aspif::Statement::Projection(_) => todo!(),
                aspif::Statement::Output(output) => {
                    let sym = interner.get_or_intern(&output.string);
                    insert_into_symbol_mapper(
                        &mut symbol_mapper,
                        &mut literal_mapper,
                        sym,
                        &output.condition,
                    )
                }
                // aspif::Statement::External { atom, init } => todo!(),
                // aspif::Statement::Assumption(_) => todo!(),
                // aspif::Statement::Heuristic {
                //     modifier,
                //     atom,
                //     k,
                //     priority,
                //     condition,
                // } => todo!(),
                // aspif::Statement::Edge { u, v, condition } => todo!(),
                // aspif::Statement::NumericTheoryTerm { id, w } => todo!(),
                // aspif::Statement::SymbolicTheoryTerm { id, string } => todo!(),
                // aspif::Statement::CompoundTheoryTerm { id, t, terms } => todo!(),
                // aspif::Statement::TheoryAtomElements {
                //     id,
                //     theory_terms,
                //     literals,
                // } => todo!(),
                // aspif::Statement::TheoryAtom {
                //     atom,
                //     symbolic_term,
                //     theory_atom_elements,
                //     theory_operation,
                // } => todo!(),
                // aspif::Statement::TheoryDirective {
                //     symbolic_term,
                //     theory_atom_elements,
                //     theory_operation,
                // } => todo!(),
                // aspif::Statement::Comment => todo!(),
                _ => {
                    panic!("Unsupported Statement");
                }
            }
        }
        literal_mapper.write_support_nogoods(&mut nogoods);
        literal_mapper.write_conjuction_nogoods(&mut nogoods);
        (Builder { nogoods }, symbol_mapper, interner)
    }
    pub fn build(self) -> Solver {
        let mut number_of_variables = 0;
        for nogood in &self.nogoods {
            for lit in nogood {
                if lit.id() + 1 > number_of_variables {
                    number_of_variables = lit.id() + 1;
                }
            }
        }
        let mut solver_nogoods = vec![];
        for nogood in self.nogoods {
            let mut solver_nogood = vec![None; number_of_variables];
            for (id, item) in solver_nogood.iter_mut().enumerate() {
                if nogood.contains(&Literal::new(id, true)) {
                    *item = Some(true);
                } else if nogood.contains(&Literal::new(id, false)) {
                    *item = Some(false);
                }
            }
            debug!("Solver nogood: {:?}", solver_nogood);
            solver_nogoods.push(solver_nogood);
        }
        let mut watch_lists = vec![];
        for nogood in &solver_nogoods {
            //  TODO: special handling for nogoods of size 1
            let mut left_watch = 0;
            while nogood[left_watch].is_none() {
                left_watch += 1;
            }
            let mut right_watch = nogood.len() - 1;
            while nogood[right_watch].is_none() {
                right_watch -= 1;
            }
            watch_lists.push(WatchList {
                first_watch: left_watch,
                second_watch: right_watch,
            })
        }
        let mut var_to_nogoods: Vec<Map<usize, bool>> = vec![Map::default(); number_of_variables];
        let mut nogoods_to_var: Vec<Map<usize, bool>> = vec![Map::default(); solver_nogoods.len()];
        for nogood_id in 0..solver_nogoods.len() {
            for (variable_id, map) in var_to_nogoods
                .iter_mut()
                .enumerate()
                .take(number_of_variables)
            {
                if let Some(sign) = solver_nogoods[nogood_id][variable_id] {
                    map.insert(nogood_id, sign);
                    nogoods_to_var[nogood_id].insert(variable_id, sign);
                }
            }
        }
        Solver {
            tight: true,
            number_of_variables,
            assignments: vec![None; number_of_variables],
            decisions: vec![],
            watch_lists,
            nogoods: solver_nogoods,
            var_to_nogoods,
            nogoods_to_var,
            decision_level: 0,
            decision_number: 0,
            assignments_log: vec![(None, None, 0, 0); number_of_variables],
            chronological_backtracking_level: 0,
        }
    }
}
#[test]
fn test_write_rule_nogood() {
    let mut lm = LiteralMapper::default();
    let l0 = Literal::new(0, true);
    let l1 = Literal::new(1, false);
    let l2 = Literal::new(2, true);
    let l3 = Literal::new(3, false);
    let mut nogoods = vec![];
    // Rule with empty body and empty head `:-.` the corresponding rule nogood should contain only the literal corresponding to the empty body
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 0 0 0").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[0], vec![l0])
    }
    // Rule with one head and empty body `a.`
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 1 0 0").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[1], vec![l1, l0])
    }
    // :- not a.
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 0 0 1 -1").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[2], vec![l2])
    }
    // a :- not a.
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 1 0 1 -1").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[3], vec![l1, l2])
    }
    // b :- not a.
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 2 0 1 -1").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[4], vec![l3, l2])
    }
    // a;b :- not a.
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 2 1 2 0 1 -1").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[5], vec![l1, l3, l2])
    }
}
#[test]
fn test_write_nogoods() {
    let mut lm = LiteralMapper::default();
    let na = Literal::new(0, false);
    let ne = Literal::new(1, false);
    let b1 = Literal::new(2, true);
    let nb = Literal::new(3, false);
    let mut nogoods = vec![];
    // b :- a, not e.
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 4 0 2 1 -3").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[0], vec![nb, b1])
    }
    let nd = Literal::new(4, false);
    let b2 = Literal::new(5, true);
    // a :- b, not d.
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 1 0 2 4 -5").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[1], vec![na, b2])
    }
    let b3 = Literal::new(6, true);
    let nc = Literal::new(7, false);
    // c;d :- b.
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 2 2 5 0 1 4").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[2], vec![nc, nd, b3])
    }
    let b4 = Literal::new(8, true);
    // b :- d, c.
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 4 0 2 5 2").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[3], vec![nb, b4])
    }
    let b5 = Literal::new(9, true);
    // a;c :- not e.
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 2 1 2 0 1 -3").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[4], vec![na, nc, b5])
    }
    let b6 = Literal::new(10, true);
    // e :- not a, not c.
    if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 3 0 2 -1 -2").unwrap() {
        lm.write_rule_nogood(&rule, &mut nogoods);
        assert_eq!(nogoods[5], vec![ne, b6])
    }
}
#[test]
fn test_collect_atom_support() {
    //TODO
}
// pub struct GroundDisjunctiveRule {
//     head: Vec<u32>,
//     body: Body,
// }
// impl GroundDisjunctiveRule {
//     fn new(head: &[u32], pbody: &[u32], nbody: &[u32]) -> Self {
//         let mut head_atoms = Vec::from(head);
//         head_atoms.dedup();
//         let body = Body::new(pbody, nbody);
//         GroundDisjunctiveRule {
//             head: head_atoms,
//             body,
//         }
//     }
// }
// #[derive(PartialEq, Clone, Debug)]
// pub enum Body {
//     // Body contains a Contradiction and can never be satisfied
//     Contradiction,
//     Conditions {
//         positive_body: Vec<u32>,
//         negative_body: Vec<u32>,
//     },
// }
// impl Body {
//     fn new(pbody: &[u32], nbody: &[u32]) -> Self {
//         let mut positive_body = Vec::from(pbody);
//         positive_body.dedup();
//         let mut negative_body = Vec::from(nbody);
//         negative_body.dedup();
//         for a1 in &negative_body {
//             for a2 in &positive_body {
//                 if a1 == a2 {
//                     return Body::Contradiction;
//                 }
//             }
//         }
//         Body::Conditions {
//             positive_body,
//             negative_body,
//         }
//     }
// }
// type SolversAtoms = u32;
// fn atoms(program: &[GroundDisjunctiveRule]) -> Vec<SolversAtoms> {
//     Vec::default()
// }
// fn bodies(program: &[GroundDisjunctiveRule]) -> Vec<SolversAtoms> {
//     Vec::default()
// }

use anyhow::Result;
use clap::Parser;
use log::{debug, error, info, warn};
use solver::convert::Builder;
use solver::solver::create_test_solver;
use std::fs;
use std::io;
use std::path::PathBuf;
/// Solver
#[derive(Parser, Debug)]
#[clap(name = "solver")]
#[clap(version, author)]
struct Opt {
    /// Input file in aspif format
    #[clap(name = "FILE", parse(from_os_str))]
    file: Option<PathBuf>,
    /// Verbose mode (-v, -vv, -vvv, etc)
    #[clap(short = 'v', long = "verbose", parse(from_occurrences))]
    verbose: usize,
}
pub enum Reader<'a> {
    File(io::BufReader<fs::File>),
    Stdin(io::StdinLock<'a>),
}
impl<'a> io::Read for Reader<'a> {
    fn read(&mut self, buf: &mut [u8]) -> io::Result<usize> {
        match self {
            Self::File(reader) => reader.read(buf),
            Self::Stdin(guard) => guard.read(buf),
        }
    }
}
impl<'a> io::BufRead for Reader<'a> {
    fn fill_buf(&mut self) -> io::Result<&[u8]> {
        match self {
            Self::File(reader) => reader.fill_buf(),
            Self::Stdin(guard) => guard.fill_buf(),
        }
    }
    fn consume(&mut self, amt: usize) {
        match self {
            Self::File(reader) => reader.consume(amt),
            Self::Stdin(guard) => guard.consume(amt),
        }
    }
}
fn main() {
    let opt = Opt::parse();
    stderrlog::new()
        .module(module_path!())
        .verbosity(opt.verbose * 4)
        .module("solver")
        .module("solver::convert")
        .init()
        .unwrap();
    if let Err(err) = run(opt) {
        error!("{:?}", err);
        std::process::exit(1);
    }
}
fn run(opt: Opt) -> Result<()> {
    let stdin = io::stdin();
    let input = match opt.file {
        Some(path) => {
            let file = fs::File::open(path)?;
            Reader::File(io::BufReader::new(file))
        }
        None => {
            let guard = stdin.lock();
            Reader::Stdin(guard)
        }
    };
    // let mut out = std::io::stdout();
    info!("Reading input ...");
    let parse_result = match input {
        Reader::File(buf_reader) => aspif::read_aspif(buf_reader)?,
        Reader::Stdin(buf_reader) => aspif::read_aspif(buf_reader)?,
    };
    info!("Translate to nogoods (wip) ...");
    let (builder, symbol_mapper, interner) = match parse_result {
        aspif::ParseResult::Complete(aspif_program) => {
            info!("Create a (directed) positive atom dependecy graph (wip)...");
            let res = solver::convert::graph_from_aspif(&aspif_program);
            info!("Create a builder (wip) ...");
            Builder::from_aspif(&aspif_program)
        }
        aspif::ParseResult::Incomplete(_) => {
            warn!("Could not read complete aspif program.");
            panic!("Could not read complete aspif program.");
        }
    };
    info!("Build solver ...");
    let mut solver = builder.build();
    for (condition, symbol) in &symbol_mapper {
        println!("condition:{:?} symbol:{} ",condition, interner.resolve(*symbol).unwrap());
    }
    // let mut solver = create_test_solver();
    info!("Solve ...");
    use solver::solver::SolveResult;
    let mut solutions = solver.solve().enumerate();
    loop {
        if let Some((c, res)) = solutions.next() {
            match res {
                SolveResult::Sat(assignments) => {
                    print!("Solution {}: ", c + 1);
                    for (condition, symbol) in &symbol_mapper {
                        let mut satisfied = true;
                        for literal in condition {
                            match assignments[literal.id()] {
                                Some(sign) => satisfied = sign == literal.sign(),
                                None => panic!("Partial assignment!"),
                            }
                            if !satisfied {
                                break;
                            };
                        }
                        if satisfied {
                            print!("{} ", interner.resolve(*symbol).unwrap());
                        }
                        // debug!("condition: {:?} sym: {}",condition,interner.resolve(*symbol).unwrap());
                    }
                    let mut string = String::new();
                    for (id, e) in assignments.iter().enumerate() {
                        match e {
                            Some(true) => string = format!("{} {}", string, id),
                            Some(false) => string = format!("{} ~{}", string, id),
                            None => {}
                        }
                    }
                    debug!("solution: {string}");
                    println!();
                }
                SolveResult::UnSat => {
                    println!("UNSAT");
                }
            }
        } else {
            println!("EXHAUSTED");
            break;
        }
    }
    Ok(())
}

[package]
name = "solver"
version = "0.1.0"
authors = ["robauke"]
description = "A CDNL solver."
edition = "2021"
# documentation = "https://docs.rs/versuch"
[dependencies]
rustc-hash = "1.1.0"
genawaiter = { version = "0.99" }
string-interner = "0.14"
fnv = "1.0"                                                                    # deterministic HashMap
petgraph = "0.6"
aspif = { git = "https://github.com/sthiele/aspif-parser", branch = "st/wip" }
# aspif = {path = "../../aspif-parser"}
clap = { version = "3.0", features = ["derive"] }
anyhow = "1.0"
log = "0.4"
thiserror = "1.0"
stderrlog = "0.5"

# Versuch
Produce aspif output with clingo:
```sh
clingo test.lp --pre=aspif > test.aspif
```
Run versuch:
```sh
cargo run --example versuch test.aspif -v
```

[workspace]
members = [
	"solver",
]