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

use crate::{context::Context, database::Database, error::CheckingError, rules::Deletion};
use colored::Colorize;

pub trait DeletionSequence {
    /// Get an [`Iterator`] of the constraint IDs that are deleted.
    fn get_deleted_ids(&self) -> impl Iterator<Item = &usize>;

    /// Write the deleted constraint IDs to a [`String`].
    #[inline]
    fn trace_deletions(&self) -> Option<String> {
        self.get_deleted_ids()
            .map(|id| id.to_string().bright_green().to_string())
            .reduce(|acc, value| acc + ", " + value.as_str())
    }

    /// Delete the constraint IDs from the [`Database`].
    #[inline]
    fn delete_constraints(
        &self,
        database: &mut Database,
        context: &mut Context,
    ) -> Result<(), CheckingError> {
        self.get_deleted_ids()
            .try_for_each(|&constraint_id| database.delete_constraint(context, constraint_id))
    }
}

impl DeletionSequence for Vec<usize> {
    #[inline]
    fn get_deleted_ids(&self) -> impl Iterator<Item = &usize> {
        self.iter()
    }
}

pub enum DeletionSequenceEnum<'a> {
    Deletion(&'a Deletion),
    Vec(Vec<usize>),
}

impl DeletionSequenceEnum<'_> {
    #[inline]
    pub fn trace_deletions(&self) -> Option<String> {
        match self {
            DeletionSequenceEnum::Deletion(del) => del.trace_deletions(),
            DeletionSequenceEnum::Vec(vec) => vec.trace_deletions(),
        }
    }

    #[inline]
    pub fn delete_constraints(
        &self,
        database: &mut Database,
        context: &mut Context,
    ) -> Result<(), CheckingError> {
        match self {
            DeletionSequenceEnum::Deletion(del) => del.delete_constraints(database, context),
            DeletionSequenceEnum::Vec(vec) => vec.delete_constraints(database, context),
        }
    }
}