veripb 3.0.0

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

use std::rc::Rc;

use ahash::AHashSet;
use by_address::ByAddress;
use veripb_formula::prelude::*;

#[derive(Debug, Default)]
pub struct OccurrenceList {
    pub list: Vec<AHashSet<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, AHashSet::new());
                    }

                    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, AHashSet::new());
                    }

                    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, AHashSet::new());
                    }

                    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, AHashSet::new());
                    }

                    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, AHashSet::new());
                    }

                    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<&AHashSet<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
    }
}