splr 0.19.0

//! main struct AssignStack
use {
    super::{
        heap::{VarHeapIF, VarIdHeap},
        AssignIF, RephaseTarget, Var,
    },
    crate::{assign::learning_rate::VarActivityScheme, cdb::ClauseDBIF, types::*},
    std::{
        fmt,
        ops::Range,
        slice::{Iter, IterMut},
    },
};

/// A record of assignment. It's called 'trail' in Glucose.
#[derive(Clone, Debug)]
pub struct AssignStack {
    /// record of assignment
    pub(super) trail: Vec<Lit>,
    pub(super) trail_lim: Vec<usize>,
    /// the-number-of-assigned-and-propagated-vars + 1
    pub(super) q_head: usize,
    pub root_level: DecisionLevel,
    pub(super) var_order: VarIdHeap, // Variable Order

    #[cfg(feature = "trail_saving")]
    pub(super) trail_saved: Vec<Lit>,

    pub(super) num_reconflict: usize,
    pub(super) num_repropagation: usize,

    //
    //## Hotspot handling
    //
    /// weighted confllict distance average
    pub(crate) conflict_interval_average: (Ema2, Ema2),

    //
    //## Phase handling
    //
    pub(crate) phase_mode: RephaseTarget,
    pub(super) best_phases: Vec<(Option<bool>, DecisionLevel)>,

    //## Elimanated vars
    //
    pub eliminated: Vec<Lit>,

    //
    //## Statistics
    //
    /// the number of vars.
    pub num_vars: usize,
    /// the number of asserted vars.
    pub num_asserted_vars: usize,
    /// the number of eliminated vars.
    pub num_eliminated_vars: usize,
    pub(super) num_decision: usize,
    pub(super) num_propagation: usize,
    pub num_conflict: usize,
    pub(super) num_restart: usize,

    /// Decisions Per Conflict
    pub(super) dpc_ema: EmaSU,
    /// Propagations Per Conflict
    pub(super) ppc_ema: EmaSU,
    /// Conflicts Per Restart
    pub(super) cpr_ema: EmaSU,

    //
    //## Var DB
    //
    /// an index for counting elapsed time
    pub(super) tick: usize,
    /// vars
    pub(super) var: Vec<Var>,

    //
    //## LBD calculation
    //
    /// a working buffer for LBD calculation (indexed by decision level)
    pub(super) lbd_temp: Vec<usize>,

    //
    //## Var Rewarding
    //
    /// active var activity scheme
    pub(crate) activity_scheme: VarActivityScheme,
    /// var activity decay
    pub(super) activity_stay_rate: f64,
    /// its diff
    pub(super) activity_learning_rate: f64,

    //## Misc
    pub(super) rng: SplitMix64,
}

impl Default for AssignStack {
    fn default() -> AssignStack {
        AssignStack {
            trail: Vec::new(),
            trail_lim: Vec::new(),
            q_head: 0,
            root_level: 0,
            var_order: VarIdHeap::default(),

            #[cfg(feature = "trail_saving")]
            trail_saved: Vec::new(),

            num_reconflict: 0,
            num_repropagation: 0,
            conflict_interval_average: (Ema2::default(), Ema2::default_extended()),

            phase_mode: RephaseTarget::default(),
            best_phases: Vec::new(),

            eliminated: Vec::new(),

            num_vars: 0,
            num_asserted_vars: 0,
            num_eliminated_vars: 0,
            num_decision: 0,
            num_propagation: 0,
            num_conflict: 0,
            num_restart: 0,

            dpc_ema: EmaSU::new(100),
            ppc_ema: EmaSU::new(100),
            cpr_ema: EmaSU::new(100),

            tick: 0,
            var: Vec::new(),

            lbd_temp: Vec::new(),

            activity_stay_rate: 0.94,

            activity_scheme: VarActivityScheme::default(),
            activity_learning_rate: 0.06,
            rng: SplitMix64::new(0),
        }
    }
}

impl<'a> IntoIterator for &'a mut AssignStack {
    type Item = &'a Lit;
    type IntoIter = Iter<'a, Lit>;
    fn into_iter(self) -> Self::IntoIter {
        self.trail.iter()
    }
}

impl From<&mut AssignStack> for Vec<i32> {
    fn from(asg: &mut AssignStack) -> Vec<i32> {
        asg.trail.iter().map(|l| i32::from(*l)).collect::<Vec<_>>()
    }
}

impl Instantiate for AssignStack {
    fn instantiate(_config: &Config, cnf: &CNFDescription) -> AssignStack {
        let nv = cnf.num_of_variables;
        AssignStack {
            trail: Vec::with_capacity(nv),
            var_order: VarIdHeap::new(nv),

            #[cfg(feature = "trail_saving")]
            trail_saved: Vec::with_capacity(nv),

            num_vars: cnf.num_of_variables,

            var: Var::new_vars(nv),
            best_phases: vec![(None, DecisionLevel::MAX); nv + 1],

            lbd_temp: vec![0; nv + 1],

            activity_stay_rate: 0.9,

            activity_learning_rate: 0.1,
            rng: SplitMix64::new((cnf.num_of_variables + cnf.num_of_clauses) as u64),

            ..AssignStack::default()
        }
    }
    #[inline]
    fn handle(&mut self, e: SolverEvent) {
        match e {
            // called only by assertion on chronoBT
            // So execute everything of `assign_by_unitclause` but cancel_until(root_level)
            SolverEvent::Conflict => (),
            SolverEvent::Eliminate(vi) => {
                self.make_var_eliminated(vi);
            }
            SolverEvent::NewVar => {
                self.expand_heap();
                self.num_vars += 1;
                self.var.push(Var::default());
                self.lbd_temp.push(0);
            }
            e => panic!("don't call asg with {e:?}"),
        }
    }
}

impl AssignIF for AssignStack {
    fn root_level(&self) -> DecisionLevel {
        self.root_level
    }
    fn current_conflict_index(&self) -> usize {
        self.num_conflict
    }
    fn stack(&self, i: usize) -> Lit {
        self.trail[i]
    }
    fn stack_range(&self, r: Range<usize>) -> &[Lit] {
        &self.trail[r]
    }
    fn stack_len(&self) -> usize {
        self.trail.len()
    }
    fn len_upto(&self, n: DecisionLevel) -> usize {
        self.trail_lim.get(n as usize).map_or(0, |n| *n)
    }
    fn stack_is_empty(&self) -> bool {
        self.trail.is_empty()
    }
    fn stack_iter(&self) -> Iter<'_, Lit> {
        self.trail.iter()
    }
    fn decision_level(&self) -> DecisionLevel {
        self.trail_lim.len() as DecisionLevel
    }
    fn decision_vi(&self, lv: DecisionLevel) -> VarId {
        debug_assert!(0 < lv);
        self.trail[self.trail_lim[lv as usize - 1]].vi()
    }
    fn remains(&self) -> bool {
        self.q_head < self.trail.len()
    }
    fn assign_ref(&self) -> Vec<Option<bool>> {
        self.var.iter().map(|v| v.assign).collect::<Vec<_>>()
    }
    #[allow(unused_variables)]
    fn extend_model(&mut self, cdb: &mut impl ClauseDBIF) -> Vec<Option<bool>> {
        let lits = &self.eliminated;

        #[cfg(feature = "trace_elimination")]
        println!(
            "# extend_model\n - as i32: {:?}\n - as raw: {:?}",
            i32s(lits),
            lits.iter()
                .map(|l| {
                    let i = i32::from(l);
                    if i < 0 {
                        -2 * i
                    } else {
                        2 * i + 1
                    }
                })
                .collect::<Vec<_>>(),
        );
        let mut extended_model: Vec<Option<bool>> = self.assign_ref();
        if lits.is_empty() {
            return extended_model;
        }
        let mut i = lits.len();
        while 0 < i {
            i -= 1;
            let width = usize::from(lits[i]);
            debug_assert!(0 < width);
            debug_assert!(width <= i);
            let target_index = i - width;
            let last_lit_index = i - 1;
            let reason_literals = target_index + 1..=last_lit_index;
            i = target_index;
            debug_assert!(
                lits[reason_literals.clone()]
                    .iter()
                    .all(|l| extended_model[l.vi()].is_some()),
                "impossible: pseudo clause has unassigned literal(s)."
            );
            if lits[reason_literals.clone()]
                .iter()
                .all(|l| extended_model[l.vi()] == Some(!bool::from(*l)))
            {
                let l = lits[target_index];
                extended_model[l.vi()] = Some(bool::from(l));
            } else if lits[reason_literals.clone()]
                .iter()
                .any(|l| extended_model[l.vi()] == Some(bool::from(*l)))
            {
                continue;
            }
        }
        extended_model
    }
    fn satisfies(&self, vec: &[Lit]) -> bool {
        for l in vec {
            if self.assigned(*l) == Some(true) {
                return true;
            }
        }
        false
    }
    fn literal_block_distance(&mut self, lits: &[Lit]) -> DecisionLevel {
        let key: usize = self.lbd_temp[0] + 1;
        self.lbd_temp[0] = key;
        let mut cnt: DecisionLevel = 0;
        for l in lits {
            let lv: DecisionLevel = self.best_level(l.vi());
            if lv == 0 {
                continue;
            }
            if lv == DecisionLevel::MAX {
                // Every unassign var has a unique level.
                cnt += 1;
            } else {
                let p = &mut self.lbd_temp[lv as usize];
                if *p != key {
                    *p = key;
                    cnt = cnt.saturating_add(1);
                }
            }
        }
        cnt
    }
    fn literal_block_distance_current(&mut self, lits: &[Lit]) -> DecisionLevel {
        let key: usize = self.lbd_temp[0] + 1;
        self.lbd_temp[0] = key;
        let mut cnt: DecisionLevel = 0;
        for l in lits {
            let lv: DecisionLevel = self.level(l.vi());
            if lv == 0 {
                continue;
            }
            if lv == DecisionLevel::MAX {
                // Every unassign var has a unique level.
                cnt += 1;
            } else {
                let p = &mut self.lbd_temp[lv as usize];
                if *p != key {
                    *p = key;
                    cnt = cnt.saturating_add(1);
                }
            }
        }
        cnt
    }
    fn literal_block_distance_(&self, lits: &[Lit]) -> usize {
        lits.iter()
            .map(|l| self.var[l.vi()].level)
            .collect::<std::collections::HashSet<_>>()
            .len()
    }
    fn activity_sum(&mut self, lits: &[Lit]) -> f64 {
        lits.iter().map(|l| self.activity(l.vi())).sum::<f64>()
    }
    fn activity_scheme(&self) -> &VarActivityScheme {
        &self.activity_scheme
    }
    fn phase_mode(&self) -> RephaseTarget {
        self.phase_mode
    }
}

impl fmt::Display for AssignStack {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        let v = self.trail.iter().map(|l| i32::from(*l)).collect::<Vec<_>>();
        let levels = self.decision_level();
        let c = |i| match i {
            0 => {
                let a = self.len_upto(i);
                (0, &v[0..a])
            }
            x if x == levels => {
                let a = self.len_upto(levels - 1);
                (levels, &v[a..])
            }
            x => {
                let a = self.len_upto(x - 1);
                (x, &v[a..self.len_upto(x)])
            }
        };
        if 0 < levels {
            write!(
                f,
                "ASG:: trail({}):{:?}\n      stats: level: {}, asserted: {}, eliminated: {}",
                self.trail.len(),
                (0..=levels).map(c).collect::<Vec<_>>(),
                levels,
                self.num_asserted_vars,
                self.num_eliminated_vars,
            )
        } else {
            write!(
                f,
                "ASG:: trail({}):[(0, {:?})]\n      level: {}, asserted: {}, eliminated: {}",
                self.trail.len(),
                v,
                levels,
                self.num_asserted_vars,
                self.num_eliminated_vars,
            )
        }
    }
}

/// Var manipulation
pub trait VarManipulateIF {
    /// return the assignment of var.
    fn assign(&self, vi: VarId) -> Option<bool>;
    /// return *the value* of a literal.
    fn assigned(&self, l: Lit) -> Option<bool>;
    /// return the assign level of var.
    fn level(&self, vi: VarId) -> DecisionLevel;
    /// return the assign level of var at the best assignment context
    fn best_level(&self, vi: VarId) -> DecisionLevel;
    /// return the reason of assignment.
    fn reason(&self, vi: VarId) -> AssignReason;
    /// return the var.
    fn var(&self, vi: VarId) -> &Var;
    /// return the var.
    fn var_mut(&mut self, vi: VarId) -> &mut Var;
    /// return an iterator over Vars.
    fn var_iter(&self) -> Iter<'_, Var>;
    /// return a mutable iterator over Vars.
    fn var_iter_mut(&mut self) -> IterMut<'_, Var>;
    /// set var status to asserted.
    fn make_var_asserted(&mut self, vi: VarId);
    /// set var status to eliminated.
    fn make_var_eliminated(&mut self, vi: VarId);
}

impl VarManipulateIF for AssignStack {
    fn assigned(&self, l: Lit) -> Option<bool> {
        match self.var[l.vi()].assign {
            Some(x) if !bool::from(l) => Some(!x),
            x => x,
        }
    }
    #[inline]
    fn assign(&self, vi: VarId) -> Option<bool> {
        #[cfg(feature = "unsafe_access")]
        unsafe {
            self.var.get_unchecked(vi).assign
        }
        #[cfg(not(feature = "unsafe_access"))]
        self.var[vi].assign
    }
    #[inline]
    fn level(&self, vi: VarId) -> DecisionLevel {
        #[cfg(feature = "unsafe_access")]
        unsafe {
            self.var.get_unchecked(vi).level
        }
        #[cfg(not(feature = "unsafe_access"))]
        self.var[vi].level
    }
    #[inline]
    fn best_level(&self, vi: VarId) -> DecisionLevel {
        #[cfg(feature = "unsafe_access")]
        unsafe {
            self.best_phases.get_unchecked(vi).1
        }
        #[cfg(not(feature = "unsafe_access"))]
        self.best_phases[vi].1
    }
    #[inline]
    fn reason(&self, vi: VarId) -> AssignReason {
        #[cfg(feature = "unsafe_access")]
        unsafe {
            self.var.get_unchecked(vi).reason
        }
        #[cfg(not(feature = "unsafe_access"))]
        self.var[vi].reason
    }
    #[inline]
    fn var(&self, vi: VarId) -> &Var {
        #[cfg(feature = "unsafe_access")]
        unsafe {
            self.var.get_unchecked(vi)
        }
        #[cfg(not(feature = "unsafe_access"))]
        &self.var[vi]
    }
    #[inline]
    fn var_mut(&mut self, vi: VarId) -> &mut Var {
        #[cfg(feature = "unsafe_access")]
        unsafe {
            self.var.get_unchecked_mut(vi)
        }
        #[cfg(not(feature = "unsafe_access"))]
        &mut self.var[vi]
    }
    fn var_iter(&self) -> Iter<'_, Var> {
        self.var.iter()
    }
    fn var_iter_mut(&mut self) -> IterMut<'_, Var> {
        self.var.iter_mut()
    }
    fn make_var_asserted(&mut self, vi: VarId) {
        self.var[vi].reason = AssignReason::Decision(0);
        self.set_activity(vi, 0.0);
        self.remove_from_heap(vi);
    }
    fn make_var_eliminated(&mut self, vi: VarId) {
        if !self.var[vi].is(FlagVar::ELIMINATED) {
            self.var[vi].turn_on(FlagVar::ELIMINATED);
            self.set_activity(vi, 0.0);
            self.remove_from_heap(vi);
            debug_assert_eq!(self.decision_level(), self.root_level);
            self.trail.retain(|l| l.vi() != vi);
            self.num_eliminated_vars += 1;

            #[cfg(feature = "trace_elimination")]
            {
                let lv = self.var[vi].level;
                if self.root_level == self.var[vi].level && self.var[vi].assign.is_some() {
                    panic!("v:{}, dl:{}", self.var[vi], self.decision_level());
                }
                if !(self.root_level < self.var[vi].level || self.var[vi].assign.is_none()) {
                    panic!(
                        "v:{}, lvl:{} => {}, dl:{}, assign:{:?} ",
                        self.var[vi],
                        lv,
                        self.var[vi].level,
                        self.decision_level(),
                        self.var[vi].assign,
                    );
                }
                debug_assert!(
                    self.root_level < self.var[vi].level || self.var[vi].assign.is_none()
                );
            }
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::{assign::PropagateIF, cdb::ClauseDB};

    fn lit(i: i32) -> Lit {
        Lit::from(i)
    }
    #[test]
    fn test_propagation() {
        let config = Config::default();
        let cnf = CNFDescription {
            num_of_variables: 4,
            ..CNFDescription::default()
        };
        let mut asg = AssignStack::instantiate(&config, &cnf);
        let mut cdb = ClauseDB::instantiate(&config, &cnf);
        // [] + 1 => [1]
        assert!(asg.assign_at_root_level(&mut cdb, lit(1)).is_ok());
        assert_eq!(asg.trail, vec![lit(1)]);

        // [1] + 1 => [1]
        assert!(asg.assign_at_root_level(&mut cdb, lit(1)).is_ok());
        assert_eq!(asg.trail, vec![lit(1)]);

        // [1] + 2 => [1, 2]
        assert!(asg.assign_at_root_level(&mut cdb, lit(2)).is_ok());
        assert_eq!(asg.trail, vec![lit(1), lit(2)]);

        // [1, 2] + -1 => ABORT & [1, 2]
        assert!(asg.assign_at_root_level(&mut cdb, lit(-1)).is_err());
        assert_eq!(asg.decision_level(), 0);
        assert_eq!(asg.stack_len(), 2);

        // [1, 2] + 3 => [1, 2, 3]
        asg.assign_by_decision(lit(3));
        assert_eq!(asg.trail, vec![lit(1), lit(2), lit(3)]);
        assert_eq!(asg.decision_level(), 1);
        assert_eq!(asg.stack_len(), 3);
        assert_eq!(asg.len_upto(0), 2);

        // [1, 2, 3] + 4 => [1, 2, 3, 4]
        asg.assign_by_decision(lit(4));
        assert_eq!(asg.trail, vec![lit(1), lit(2), lit(3), lit(4)]);
        assert_eq!(asg.decision_level(), 2);
        assert_eq!(asg.stack_len(), 4);
        assert_eq!(asg.len_upto(1), 3);

        // [1, 2, 3] => [1, 2]
        #[cfg(feature = "trace_propagation")]
        {
            for l in asg.trail.iter() {
                asg.var[l.vi()].turn_on(Flag::PROPAGATED);
            } // simulate propagation
        }
        asg.cancel_until(&mut cdb, 1);
        assert_eq!(asg.trail, vec![lit(1), lit(2), lit(3)]);
        assert_eq!(asg.decision_level(), 1);
        assert_eq!(asg.stack_len(), 3);
        assert_eq!(asg.trail_lim, vec![2]);
        assert_eq!(asg.assigned(lit(1)), Some(true));
        assert_eq!(asg.assigned(lit(-1)), Some(false));
        assert_eq!(asg.assigned(lit(4)), None);

        // [1, 2, 3] => [1, 2, 3, 4]
        asg.assign_by_decision(lit(4));
        assert_eq!(asg.trail, vec![lit(1), lit(2), lit(3), lit(4)]);
        assert_eq!(asg.var[lit(4).vi()].level, 2);
        assert_eq!(asg.trail_lim, vec![2, 3]);

        // [1, 2, 3, 4] => [1, 2, -4]
        asg.assign_at_root_level(&mut cdb, Lit::from(-4i32))
            .expect("impossible");
        assert_eq!(asg.trail, vec![lit(1), lit(2), lit(-4)]);
        assert_eq!(asg.decision_level(), 0);
        assert_eq!(asg.stack_len(), 3);

        assert_eq!(asg.assigned(lit(-4)), Some(true));
        assert_eq!(asg.assigned(lit(-3)), None);
    }
}