1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92

use {
    super::{ClauseDB, ClauseId},
    crate::{assign::AssignIF, types::*},
};

/// API to calculate LBD.
pub trait LBDIF {
    /// return the LBD value for a set of literals.
    fn compute_lbd<A>(&mut self, asg: &A, vec: &[Lit]) -> usize
    where
        A: AssignIF;
    /// return the LBD value of clause `cid`.
    fn compute_lbd_of<A>(&mut self, asg: &A, cid: ClauseId) -> usize
    where
        A: AssignIF;
    /// re-calculate the LBD values of all (learnt) clauses.
    fn reset_lbd<A>(&mut self, asg: &A, all: bool)
    where
        A: AssignIF;
}

impl LBDIF for ClauseDB {
    fn compute_lbd<A>(&mut self, asg: &A, vec: &[Lit]) -> usize
    where
        A: AssignIF,
    {
        let level = asg.level_ref();
        unsafe {
            let key: usize = self.lbd_temp.get_unchecked(0) + 1;
            *self.lbd_temp.get_unchecked_mut(0) = key;
            let mut cnt = 0;
            for l in vec {
                let lv = level[l.vi()];
                let p = self.lbd_temp.get_unchecked_mut(lv as usize);
                if *p != key {
                    *p = key;
                    cnt += 1;
                }
            }
            cnt
        }
    }
    fn compute_lbd_of<A>(&mut self, asg: &A, cid: ClauseId) -> usize
    where
        A: AssignIF,
    {
        let level = asg.level_ref();
        unsafe {
            let key: usize = self.lbd_temp.get_unchecked(0) + 1;
            *self.lbd_temp.get_unchecked_mut(0) = key;
            let mut cnt = 0;
            for l in &self.clause[cid.ordinal as usize].lits {
                let lv = level[l.vi()];
                let p = self.lbd_temp.get_unchecked_mut(lv as usize);
                if *p != key {
                    *p = key;
                    cnt += 1;
                }
            }
            cnt
        }
    }
    fn reset_lbd<A>(&mut self, asg: &A, all: bool)
    where
        A: AssignIF,
    {
        let level = asg.level_ref();
        let mut key = self.lbd_temp[0];
        for c in &mut self.clause.iter_mut().skip(1) {
            if c.is(Flag::DEAD) || !c.is(Flag::LEARNT) || (!all && !c.is(Flag::JUST_USED)) {
                continue;
            }
            key += 1;
            let mut cnt = 0;
            for l in &c.lits {
                let lv = level[l.vi()];
                if lv != 0 {
                    let p = unsafe { self.lbd_temp.get_unchecked_mut(lv as usize) };
                    if *p != key {
                        *p = key;
                        cnt += 1;
                    }
                }
            }
            if cnt < c.rank {
                c.rank = cnt;
            }
        }
        self.lbd_temp[0] = key;
        self.num_lbd_update += 1;
    }
}