logic-form 0.4.0

Rust library for representing Cube, Clause, CNF and DNF
Documentation 
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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109

use crate::{Lit, LitMap, LitOrdVec, Var};
use giputils::{allocator::Gallocator, grc::Grc, gvec::Gvec, heap::BinaryHeapCmp};

#[derive(Debug, Clone, Default)]
pub struct Occur {
    occur: Gvec<u32>,
    dirty: bool,
    size: usize,
}

impl Occur {
    #[inline]
    fn len(&self) -> usize {
        self.size
    }

    #[inline]
    #[allow(unused)]
    fn is_empty(&self) -> bool {
        self.len() == 0
    }

    #[inline]
    fn clean(&mut self, cdb: &Gallocator<LitOrdVec>) {
        if self.dirty {
            self.occur.retain(|&i| !cdb.is_removed(i));
            self.dirty = false;
        }
    }

    #[inline]
    #[allow(unused)]
    fn clear(&mut self) {
        self.occur.clear();
        self.dirty = false;
        self.size = 0;
    }

    #[inline]
    pub fn add(&mut self, c: u32) {
        self.occur.push(c);
        self.size += 1;
    }

    #[inline]
    pub fn lazy_remove(&mut self) {
        self.dirty = true;
        self.size -= 1;
    }
}

pub struct Occurs {
    occurs: LitMap<Occur>,
    cdb: Grc<Gallocator<LitOrdVec>>,
}

impl Occurs {
    #[inline]
    #[allow(unused)]
    pub fn new(cdb: Grc<Gallocator<LitOrdVec>>) -> Self {
        Self {
            occurs: LitMap::new(),
            cdb,
        }
    }

    #[inline]
    pub fn new_with(var: Var, cdb: Grc<Gallocator<LitOrdVec>>) -> Self {
        Self {
            occurs: LitMap::new_with(var),
            cdb,
        }
    }

    #[inline]
    #[allow(unused)]
    pub fn reserve(&mut self, var: Var) {
        self.occurs.reserve(var);
    }

    #[inline]
    pub fn num_occur(&self, l: Lit) -> usize {
        self.occurs[l].len()
    }

    #[inline]
    pub fn add(&mut self, lit: Lit, o: u32) {
        self.occurs[lit].add(o);
    }

    #[inline]
    pub fn del(&mut self, lit: Lit, _o: u32) {
        self.occurs[lit].lazy_remove();
    }

    #[inline]
    pub fn get(&mut self, lit: Lit) -> &[u32] {
        self.occurs[lit].clean(&self.cdb);
        &self.occurs[lit].occur
    }
}

impl BinaryHeapCmp<Var> for Occurs {
    #[inline]
    fn lge(&self, s: Var, o: Var) -> bool {
        self.num_occur(s.lit()) + self.num_occur(!s.lit())
            < self.num_occur(o.lit()) + self.num_occur(!o.lit())
    }
}