splr 0.19.0

//! Conflict Analysis

use {
    super::State,
    crate::{
        assign::{AssignIF, AssignStack, PropagateIF, VarManipulateIF},
        cdb::{ClauseDB, ClauseDBIF},
        types::*,
    },
};

/// returns:
/// - 0: if a new assignment is generated by conflict analysis.
/// - 1: if a binary link is generated.
/// - otherwise: it's the LBD of the learnt clause.
#[allow(clippy::cognitive_complexity)]
pub fn handle_conflict(
    asg: &mut AssignStack,
    cdb: &mut ClauseDB,
    state: &mut State,
    cc: &ConflictContext,
) -> Result<(ClauseId, DecisionLevel), SolverError> {
    // `conflicting_level` should be calculated from cc.1 instead of cc.0.
    // Because the conflicting_literal has two values assigned at different levels.
    // We need larger one.
    #[cfg(feature = "chrono_BT")]
    let conflicting_level; // for now
    #[cfg(not(feature = "chrono_BT"))]
    let conflicting_level = asg.decision_level();

    // we need a catch here for handling the possibility of level zero conflict
    // at higher level due to the incoherence between the current level and conflicting
    // level in chronoBT. This leads to UNSAT solution. No need to update misc stats.
    {
        if let AssignReason::Implication(cid) = cc.1
            && cdb[cid].iter().all(|l| asg.level(l.vi()) == 0)
        {
            return Err(SolverError::RootLevelConflict(*cc));
        }
    }

    #[cfg(feature = "chrono_BT")]
    match cc.1 {
        AssignReason::BinaryLink(l) => {
            conflicting_level = asg.var(l.vi()).level.max(asg.var(cc.0.vi()).level);
        }
        AssignReason::Implication(cid) => {
            let c = &cdb[cid];
            conflicting_level = c.iter().map(|l| asg.level(l.vi())).max().unwrap();
            if 1 == c
                .iter()
                .filter(|l| asg.level(l.vi()) == conflicting_level)
                .count()
                && let Some(second_level) = c
                    .iter()
                    .map(|l| asg.level(l.vi()))
                    .filter(|l| *l < conflicting_level)
                    .max()
            {
                debug_assert!(0 < second_level);
                let rank = c.rank;
                asg.cancel_until(cdb, second_level);
                return Ok(rank);
            }
        }
        _ => {
            panic!();
        }
    }
    asg.cancel_until(cdb, conflicting_level);
    asg.handle(SolverEvent::Conflict);

    let assign_level = conflict_analyze(asg, cdb, state, cc).max(asg.root_level());
    let new_learnt = &mut state.new_learnt;
    let learnt_len = new_learnt.len();
    if learnt_len == 0 {
        return Err(SolverError::EmptyClause);
    }
    let l0 = new_learnt[0];
    if learnt_len == 1 {
        //
        //## A NEW ASSERTION by UNIT LEARNT CLAUSE GENERATION
        //
        match asg.assigned(l0) {
            Some(true) if asg.root_level() < asg.level(l0.vi()) => {
                panic!("double assignment occurred");
                // asg.lift_to_asserted(l0.vi());
            }
            Some(false) if asg.level(l0.vi()) == asg.root_level() => {
                return Err(SolverError::RootLevelConflict((l0, asg.reason(l0.vi()))));
            }
            _ => {
                // dump to certified even if it's a literal.
                cdb.certificate_add_assertion(l0);
                if asg.assign_at_root_level(cdb, l0).is_err() {
                    unreachable!("handle_conflict::root_level_conflict_by_assertion");
                }
                cdb.handle(SolverEvent::Assert(l0.vi()));
                return Ok((ClauseId::default(), 0));
            }
        }
    }
    let l1 = new_learnt[1];
    // assert: root_level < cl, which was checked already by new_learnt.is_empty().

    // NCB places firstUIP on level bl, while CB does it on level cl.
    // ?? || Therefore the condition to use CB is: activity(firstUIP) < activity(v(bl)).
    // PREMISE: root_level < bl, because asg.decision_vi accepts only non-zero values.

    // At the present time, some reason clauses can contain first UIP or its negation.
    // So we have to filter vars instead of literals to avoid double counting.
    #[cfg(feature = "reason_side_rewarding")]
    let mut bumped = new_learnt.iter().map(|l| l.vi()).collect::<Vec<VarId>>();
    for lit in new_learnt.iter() {
        //
        //## Learnt Literal Rewarding
        //
        asg.reward_at_analysis(lit.vi());

        //
        //## Reason-Side Rewarding
        //
        #[cfg(feature = "reason_side_rewarding")]
        match asg.reason(lit.vi()) {
            AssignReason::BinaryLink(from) => {
                let vi = from.vi();
                if !bumped.contains(&vi) {
                    asg.reward_at_analysis(vi);
                    bumped.push(vi);
                }
            }
            AssignReason::Implication(r) => {
                let mut cs = Vec::new();
                for l in cdb[r].iter() {
                    let vi = l.vi();
                    if !bumped.contains(&vi) {
                        asg.reward_at_analysis(vi);
                        bumped.push(vi);
                    }
                    if let AssignReason::Implication(ci) = asg.reason(l.vi()) {
                        cs.push(ci);
                    }
                }
                for ci in cs.into_iter() {
                    cdb[ci].update_reference(asg);
                }
            }
            AssignReason::Decision(_) => (),
            AssignReason::None => unreachable!("handle_conflict"),
        }
    }

    // Certify the new learnt clause *before* backjumping: `cancel_until` may
    // instantly drop reason clauses that are no longer locked (see
    // `PropagateIF::cancel_until`), which are exactly the clauses that
    // `conflict_analyze` just resolved through to build `new_learnt`. If those
    // clauses were deleted (and their DRAT `d` line emitted) before this new
    // clause is added, the RUP/RAT justification for the new clause can lose
    // its natural witness and become unverifiable. Registering the clause
    // first (and thus writing its `a` line first) preserves the standard
    // "certify before you garbage-collect what justified it" invariant.
    // `new_clause` itself has no dependency on assignment/trail state, so
    // this reordering doesn't change its behavior.
    let ref_clause = cdb.new_clause(new_learnt, true);
    asg.cancel_until(cdb, assign_level);
    // debug_assert_eq!(asg.assigned(l0), None);
    // debug_assert_eq!(
    //     new_learnt.iter().skip(1).map(|l| asg.level(l.vi())).max(),
    //     Some(assign_level)
    // );
    let ret: (ClauseId, DecisionLevel);
    match ref_clause {
        RefClause::Clause(cid) if learnt_len == 2 => {
            debug_assert_eq!(l0, cdb[cid].lit0());
            debug_assert_eq!(l1, cdb[cid].lit1());
            debug_assert_eq!(asg.assigned(l0), None);

            asg.assign_by_implication(l0, AssignReason::BinaryLink(!l1), assign_level);
            ret = (cid, 1);
        }
        RefClause::Clause(cid) => {
            debug_assert_eq!(cdb[cid].lit0(), l0);
            asg.assign_by_implication(l0, AssignReason::Implication(cid), assign_level);
            cdb[cid].turn_on(FlagClause::ASSIGN_REASON);
            // lbd should be calculated at conflict level, where all literals are assigned.
            // But since vars hold the last level even after unassignment,
            // we can have postponed the calculation.
            let d = asg.literal_block_distance_current(&cdb[cid].lits);
            ret = (cid, d);
        }
        RefClause::RegisteredClause(cid) => {
            debug_assert_eq!(learnt_len, 2);
            debug_assert!(
                (l0 == cdb[cid].lit0() && l1 == cdb[cid].lit1())
                    || (l0 == cdb[cid].lit1() && l1 == cdb[cid].lit0())
            );
            debug_assert_eq!(asg.assigned(l0), None);
            // if bt_drift.is_none() && asg.assigned(l1) != Some(false) {
            //     dbg!(cc);
            //     dbg!(asg.decision_level());
            //     dbg!(cid);
            //     for l in cdb[cid].iter() {
            //         println!("{:?} @ {} => {:?}", l, asg.level(l.vi()), asg.assigned(*l));
            //     }
            //     panic!("here we are!");
            // }
            ret = (cid, asg.literal_block_distance_current(&cdb[cid].lits));
            asg.assign_by_implication(l0, AssignReason::BinaryLink(!l1), assign_level);
        }
        RefClause::Dead => unreachable!("handle_conflict::RefClause::Dead"),
        RefClause::EmptyClause => unreachable!("handle_conflict::RefClause::EmptyClause"),
        RefClause::UnitClause(_) => unreachable!("handle_conflict::RefClause::UnitClause"),
    }
    state.c_lvl.update(conflicting_level as f64);
    state.b_lvl.update(assign_level as f64);
    Ok(ret)
}

///
/// ## Conflict Analysis
///
fn conflict_analyze(
    asg: &mut AssignStack,
    cdb: &mut ClauseDB,
    state: &mut State,
    cc: &ConflictContext,
) -> DecisionLevel {
    let learnt = &mut state.new_learnt;
    learnt.clear();
    learnt.push(Lit::from(u32::MAX));
    let root_level = asg.root_level();
    // assert_eq!(asg.decision_level(), asg.var(cc.0.vi()).level);
    let dl = asg.decision_level();
    let mut path_cnt = 0;
    let &(mut p, mut reason) = cc;
    // assert_eq!(
    //     dl,
    //     asg.var(p.vi()).level,
    //     "conflict: {:?} occurred at a lower level than current dl",
    //     cc
    // );
    /// Trace and reward the var.
    macro_rules! conflict_level {
        ($vi: expr) => {
            path_cnt += 1;
            //## Conflict-Side Rewarding
            asg.reward_at_analysis($vi);
        };
    }
    macro_rules! trace {
        ($($arg: expr),*) => {
            #[cfg(feature = "trace_analysis")]
            println!($($arg),*);
        };
    }
    /// A logging facility.
    macro_rules! trace_lit {
        ($lit: expr, $message: expr) => {
            #[cfg(feature = "trace_analysis")]
            {
                let vi = $lit.vi();
                let lv = asg.level(vi);
                println!("{}: literal {} at level {}", $message, i32::from($lit), $lv);
            }
        };
    }
    /// vi must be assigned at the current or lower decision level.
    macro_rules! validate_vi {
        ($vi: expr) => {
            debug_assert!(!asg.var($vi).is(FlagVar::ELIMINATED));
            debug_assert!(
                asg.assign($vi).is_some(),
                "conflict_analyze(validate_vi) found unassigned: {:?}",
                $vi
            );
            debug_assert!(asg.level($vi) <= dl);
        };
    }
    macro_rules! set_seen {
        ($vi: expr) => {
            debug_assert!(!asg.var($vi).is(FlagVar::CA_SEEN));
            asg.var_mut($vi).turn_on(FlagVar::CA_SEEN);
        };
    }

    {
        trace_lit!("- handle conflicting literal", p);
        let vi = p.vi();
        validate_vi!(vi);
        set_seen!(vi);
        let lvl = asg.level(vi);
        if dl == lvl {
            conflict_level!(vi);
        } else {
            debug_assert_ne!(root_level, lvl);
            learnt.push(p);
        }
    }
    let mut trail_index = asg.stack_len() - 1;
    if let AssignReason::Implication(cid) = cc.1 {
        cdb.update_at_analysis(cid);
    }
    loop {
        match reason {
            AssignReason::BinaryLink(l) => {
                let vi = l.vi();
                if !asg.var(vi).is(FlagVar::CA_SEEN) {
                    validate_vi!(vi);
                    // debug_assert_eq!(
                    //     asg.level(vi),
                    //     dl,
                    //     "unblanced bi-clause {}-{} at conflict level {dl}, source: {}, cc: {:?}",
                    //     p,
                    //     l,
                    //     asg.var(p.vi()).level,
                    //     cc
                    // );
                    // if root_level == asg.level(vi) { continue; }
                    set_seen!(vi);
                    trace_lit!(l, " - binary linked");
                    let lvl = asg.level(vi);
                    if dl == lvl {
                        trace_lit!(l, " -- found another path");
                        conflict_level!(vi);
                    } else {
                        trace_lit!(l, " -- push to learnt");
                        // This path is created for chrono-BT.
                        // So we must consider if `l` should be pushed or `!l`.
                        // From debug log, it seems to be `!l`.
                        learnt.push(!l);
                    }
                }
            }
            AssignReason::Implication(cid) => {
                trace!(
                    "analyze clause {}(first literal: {}) for {}",
                    cid,
                    i32::from(cdb[cid].lit0()),
                    p
                );
                debug_assert!(!cdb[cid].is_dead() && 2 < cdb[cid].len());
                // if !cdb.update_at_analysis(asg, cid) {
                // if !cdb[cid].is(FlagClause::LEARNT) {
                //     cdb[cid].used = cdb[cid].used.saturating_add(1);
                // }
                for q in cdb[cid].iter().skip(1) {
                    let vi = q.vi();
                    debug_assert!(asg.var(vi).assign.is_some());
                    // if asg.var(vi).assign.is_none() {
                    //     println!(
                    //         "Implication clause contains non-assinged lit (cc: {:?}, at level: {:?})",
                    //         cc,
                    //         asg.var(cc.0.vi()).level
                    //     );
                    //     println!("p: {:?}, level: {:?}", p, asg.var(p.vi()).level);
                    //     println!("dl: {}", asg.decision_level());
                    //     println!(
                    //         "c{:?}: {:?}",
                    //         cid,
                    //         cdb[cid]
                    //             .iter()
                    //             // .filter(|l| asg.var(l.vi()).assign.is_none())
                    //             .map(|l| (l, asg.var(l.vi()).level))
                    //             .collect::<Vec<_>>()
                    //     );
                    //     panic!();
                    // }
                    validate_vi!(vi);
                    if !asg.var(vi).is(FlagVar::CA_SEEN) {
                        let lvl = asg.level(vi);
                        if root_level == lvl {
                            trace_lit!(q, " -- ignore");
                            continue;
                        }
                        set_seen!(vi);
                        if dl == lvl {
                            trace_lit!(q, " -- found another path");
                            conflict_level!(vi);
                        } else {
                            trace_lit!(q, " -- push to learnt");
                            learnt.push(*q);
                        }
                    } else {
                        trace!(q, " -- ignore flagged already");
                    }
                }
                cdb[cid].update_reference(asg);
            }
            AssignReason::Decision(_) | AssignReason::None => {}
        }
        //
        // set the index of the next literal to trail_index
        //
        #[allow(clippy::blocks_in_conditions)]
        while {
            let vi = asg.stack(trail_index).vi();

            let lvl = asg.level(vi);
            let v = asg.var(vi);
            !v.is(FlagVar::CA_SEEN) || lvl != dl
        } {
            trace_lit!(asg.stack(trail_index), "skip, not flagged");

            trail_index -= 1;
        }
        p = asg.stack(trail_index);
        trace!("move to flagged {}; num path: {}", p.vi(), path_cnt - 1);

        asg.var_mut(p.vi()).turn_off(FlagVar::CA_SEEN);
        // since the trail can contain a literal which level is under `dl` after
        // the `dl`-th decision var, we must skip it.
        path_cnt -= 1;
        if path_cnt == 0 {
            break;
        }
        debug_assert!(0 < trail_index);
        trail_index -= 1;
        reason = asg.reason(p.vi());
    }
    // debug_assert!(learnt.iter().all(|l| *l != !p));
    debug_assert_eq!(asg.level(p.vi()), dl);
    learnt[0] = !p;
    // asg.var_mut(p.vi()).turn_off(FlagVar::USED);
    trace!(
        "appending {}, the final (but not minimized) learnt is {:?}",
        learnt[0], learnt
    );
    minimize_learnt(&mut state.new_learnt, asg, cdb)
}

fn minimize_learnt(
    new_learnt: &mut Vec<Lit>,
    asg: &mut AssignStack,
    cdb: &mut ClauseDB,
) -> DecisionLevel {
    let mut to_clear: Vec<Lit> = new_learnt.clone();
    let mut levels = vec![false; asg.decision_level() as usize + 1];
    for l in &new_learnt[1..] {
        levels[asg.level(l.vi()) as usize] = true;
    }
    let l0 = new_learnt[0];
    let _len = new_learnt.len();
    let _lbd = levels.iter().filter(|b| **b).count();
    // if lbd < 5 || 20 < len {
    new_learnt.retain(|l| *l == l0 || !l.is_redundant(asg, cdb, &mut to_clear, &levels));
    // }
    if 2 < new_learnt.len() {
        cdb.minimize_with_bi_clauses(asg, new_learnt);
    }
    // find correct backtrack level from remaining literals
    let mut level_to_return = 0;
    if 1 < new_learnt.len() {
        let mut max_i = 1;
        level_to_return = asg.level(new_learnt[max_i].vi());
        for (i, l) in new_learnt.iter().enumerate().skip(2) {
            let lv = asg.level(l.vi());
            if level_to_return < lv {
                level_to_return = lv;
                max_i = i;
            }
        }
        new_learnt.swap(1, max_i);
    }
    for l in &to_clear {
        asg.var_mut(l.vi()).turn_off(FlagVar::CA_SEEN);
    }
    level_to_return
}

/// return `true` if the `lit` is redundant, which is defined by
/// any leaf of implication graph for it isn't an asserted var nor a decision var.
impl Lit {
    fn is_redundant(
        self,
        asg: &mut AssignStack,
        cdb: &ClauseDB,
        clear: &mut Vec<Lit>,
        levels: &[bool],
    ) -> bool {
        if matches!(asg.reason(self.vi()), AssignReason::Decision(_)) {
            return false;
        }
        let mut stack = vec![self];
        let top = clear.len();
        while let Some(sl) = stack.pop() {
            match asg.reason(sl.vi()) {
                AssignReason::BinaryLink(l) => {
                    let vi = l.vi();
                    let lv = asg.level(vi);
                    if 0 < lv && !asg.var(vi).is(FlagVar::CA_SEEN) {
                        // if asg.reason(vi) != AssignReason::Decision(_) && levels[lv as usize] {
                        if matches!(
                            asg.reason(vi),
                            AssignReason::Implication(_) | AssignReason::BinaryLink(_)
                        ) && levels[lv as usize]
                        {
                            asg.var_mut(vi).turn_on(FlagVar::CA_SEEN);
                            stack.push(l);
                            clear.push(l);
                        } else {
                            // one of the roots is a decision var at an unchecked level.
                            for l in &clear[top..] {
                                asg.var_mut(l.vi()).turn_off(FlagVar::CA_SEEN);
                            }
                            clear.truncate(top);
                            return false;
                        }
                    }
                }
                AssignReason::Implication(cid) => {
                    let c = &cdb[cid];
                    for q in &(*c)[1..] {
                        let vi = q.vi();
                        let lv = asg.level(vi);
                        if 0 < lv && !asg.var(vi).is(FlagVar::CA_SEEN) {
                            // if asg.reason(vi) != AssignReason::default() && levels[lv as usize] {
                            if matches!(
                                asg.reason(vi),
                                AssignReason::BinaryLink(_) | AssignReason::Implication(_,)
                            ) && levels[lv as usize]
                            {
                                asg.var_mut(vi).turn_on(FlagVar::CA_SEEN);
                                stack.push(*q);
                                clear.push(*q);
                            } else {
                                // one of the roots is a decision var at an unchecked level.
                                for l in &clear[top..] {
                                    asg.var_mut(l.vi()).turn_off(FlagVar::CA_SEEN);
                                }
                                clear.truncate(top);
                                return false;
                            }
                        }
                    }
                }
                AssignReason::Decision(_) | AssignReason::None => unreachable!("is_redundant"),
            }
        }
        true
    }
}

#[allow(dead_code)]
fn check_graph(asg: &AssignStack, cdb: &ClauseDB, lit: Lit, mes: &str) {
    let its_level = asg.level(lit.vi());
    let mut children = Vec::new();
    let precedents = lit_level(asg, cdb, lit, &mut children, mes);
    assert!(precedents <= its_level);
}

#[allow(dead_code)]
fn lit_level(
    asg: &AssignStack,
    cdb: &ClauseDB,
    lit: Lit,
    bag: &mut Vec<Lit>,
    _mes: &str,
) -> DecisionLevel {
    if bag.contains(&lit) {
        return 0;
    }
    bag.push(lit);
    match asg.reason(lit.vi()) {
        AssignReason::Decision(0) => asg.root_level(),
        AssignReason::Decision(lvl) => lvl,
        AssignReason::Implication(cid) => {
            assert_eq!(
                cdb[cid].lit0(),
                lit,
                "lit0 {} != lit{}, cid {}, {}",
                cdb[cid].lit0(),
                lit,
                cid,
                cdb[cid]
            );
            // assert!(
            //     !bag.contains(&lit),
            //     "{}; {} is contained in {:?}\n{:?}\n{}",
            //     mes,
            //     lit,
            //     bag,
            //     asg.reason(lit.vi()),
            //     dumper(asg, cdb, bag),
            // );
            // bag.push(lit);
            cdb[cid]
                .iter()
                .skip(1)
                .map(|l| lit_level(asg, cdb, !*l, bag, _mes))
                .max()
                .unwrap()
        }
        AssignReason::BinaryLink(b) => lit_level(asg, cdb, b, bag, _mes),
        AssignReason::None => panic!("One of root of {lit} isn't assigned."),
    }
}

#[allow(dead_code)]
fn dumper(asg: &AssignStack, cdb: &ClauseDB, bag: &[Lit]) -> String {
    use std::fmt::Write as _;
    let mut s = String::new();
    for l in bag {
        writeln!(
            s,
            "{:8>} :: level {:4>}, {:?} {:?}",
            *l,
            asg.level(l.vi()),
            asg.reason(l.vi()),
            match asg.reason(l.vi()) {
                AssignReason::Decision(_) => vec![],
                AssignReason::BinaryLink(lit) => vec![*l, !lit],
                AssignReason::Implication(cid) => cdb[cid].iter().copied().collect::<Vec<Lit>>(),
                AssignReason::None => vec![],
            },
        )
        .unwrap();
    }
    s
}