veripb 3.0.2

VeriPB is a proof checker for verifying pseudo-Boolean certificates of satisfiability, unsatisfiability, and optimality bounds.
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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139

use std::rc::Rc;

use ahash::{HashSet, RandomState};
use by_address::ByAddress;
use veripb_formula::prelude::*;

#[derive(Debug, Default)]
pub struct OccurrenceList {
    pub list: Vec<HashSet<ByAddress<Rc<DBConstraint>>>>,
}

impl OccurrenceList {
    #[inline]
    pub fn add(&mut self, constraint: &Rc<DBConstraint>) {
        match &constraint.constraint {
            PBConstraintEnum::Clause(clause) => {
                for lit in clause.get_lits() {
                    let index = lit.get_lit_data();
                    if index >= self.list.len() {
                        self.list.resize(
                            index + 1,
                            HashSet::with_hasher(RandomState::with_seeds(42, 42, 42, 42)),
                        );
                    }

                    self.list[index].insert(constraint.clone().into());
                }
            }
            PBConstraintEnum::Cardinality(cardinality) => {
                for lit in cardinality.get_lits() {
                    let index = lit.get_lit_data();
                    if index >= self.list.len() {
                        self.list.resize(
                            index + 1,
                            HashSet::with_hasher(RandomState::with_seeds(42, 42, 42, 42)),
                        );
                    }

                    self.list[index].insert(constraint.clone().into());
                }
            }
            PBConstraintEnum::GeneralPBI64(general_constraint) => {
                for lit in general_constraint.get_lits() {
                    let index = lit.get_lit_data();
                    if index >= self.list.len() {
                        self.list.resize(
                            index + 1,
                            HashSet::with_hasher(RandomState::with_seeds(42, 42, 42, 42)),
                        );
                    }

                    self.list[index].insert(constraint.clone().into());
                }
            }
            PBConstraintEnum::GeneralPBI128(general_constraint) => {
                for lit in general_constraint.get_lits() {
                    let index = lit.get_lit_data();
                    if index >= self.list.len() {
                        self.list.resize(
                            index + 1,
                            HashSet::with_hasher(RandomState::with_seeds(42, 42, 42, 42)),
                        );
                    }

                    self.list[index].insert(constraint.clone().into());
                }
            }
            PBConstraintEnum::GeneralPBBigInt(general_constraint) => {
                for lit in general_constraint.get_lits() {
                    let index = lit.get_lit_data();
                    if index >= self.list.len() {
                        self.list.resize(
                            index + 1,
                            HashSet::with_hasher(RandomState::with_seeds(42, 42, 42, 42)),
                        );
                    }

                    self.list[index].insert(constraint.clone().into());
                }
            }
        };

        constraint.header.borrow_mut().is_in_occurrences = true;
    }

    #[inline]
    pub fn remove(&mut self, constraint: &Rc<DBConstraint>) {
        let constraint = ByAddress(constraint.clone());
        match &constraint.constraint {
            PBConstraintEnum::Clause(clause) => {
                for lit in clause.get_lits() {
                    self.list[lit.get_lit_data()].remove(&constraint);
                }
            }
            PBConstraintEnum::Cardinality(cardinality) => {
                for lit in cardinality.get_lits() {
                    self.list[lit.get_lit_data()].remove(&constraint);
                }
            }
            PBConstraintEnum::GeneralPBI64(general_constraint) => {
                for lit in general_constraint.get_lits() {
                    self.list[lit.get_lit_data()].remove(&constraint);
                }
            }
            PBConstraintEnum::GeneralPBI128(general_constraint) => {
                for lit in general_constraint.get_lits() {
                    self.list[lit.get_lit_data()].remove(&constraint);
                }
            }
            PBConstraintEnum::GeneralPBBigInt(general_constraint) => {
                for lit in general_constraint.get_lits() {
                    self.list[lit.get_lit_data()].remove(&constraint);
                }
            }
        }
        constraint.header.borrow_mut().is_in_occurrences = false;
    }

    #[inline]
    pub fn get_constraints_for_lit(
        &self,
        lit: Lit,
    ) -> Option<&HashSet<ByAddress<Rc<DBConstraint>>>> {
        self.list.get(lit.get_lit_data())
    }

    #[inline]
    pub fn get_used_vars(&self) -> Vec<VarIdx> {
        let mut vars = Vec::new();
        for (lit_idx, list) in self.list.iter().enumerate() {
            if !list.is_empty() {
                vars.push(lit_idx / 2);
            }
        }

        vars.dedup();
        vars
    }
}