logicng 0.1.0-alpha.3

A Library for Creating, Manipulating, and Solving Boolean Formulas
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

use crate::solver::minisat::sat::MsLit;

/// A MiniSAT clause
#[allow(clippy::struct_excessive_bools)]
#[derive(Clone, PartialEq, Debug)]
pub struct MsClause {
    pub data: Vec<MsLit>,
    pub learnt: bool,
    is_at_most: bool,
    pub activity: f64,
    sz_without_selectors: isize,
    seen: bool,
    lbd: i64,
    can_be_del: bool,
    one_watched: bool,
    at_most_watchers: isize,
}

impl MsClause {
    pub fn new(data: Vec<MsLit>, learnt: bool) -> Self {
        Self {
            data,
            learnt,
            is_at_most: false,
            activity: 0.0,
            sz_without_selectors: 0,
            seen: false,
            lbd: 0,
            can_be_del: true,
            one_watched: false,
            at_most_watchers: -1,
        }
    }

    pub fn len(&self) -> usize {
        self.data.len()
    }

    pub fn get(&self, i: usize) -> MsLit {
        self.data[i]
    }

    pub fn set(&mut self, i: usize, lit: MsLit) {
        self.data[i] = lit;
    }

    pub fn rescale_activity(&mut self) {
        self.activity *= 1e-20;
    }

    pub fn range_copy_from(&self, from: usize) -> Vec<MsLit> {
        self.data[from..].to_vec()
    }
}