veripb-formula 0.1.1

VeriPB library to handle pseudo-Boolean constraints, formulas, and more data structures.
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

//! Some general helper functions used inside this crate.

use std::{iter::Peekable, slice::Iter};

use malachite_bigint::BigInt;
use num_traits::One;

use crate::prelude::*;

#[derive(Debug, Clone, Copy)]
pub enum ConstraintPropagationResult {
    NoPropagation,
    Propagated,
    Conflict,
}

/// Merge [`Vec<Lit>`] literals and [`Vec<PBTerm`>] to literals.
///
/// This function immediately returns if merging the term in the [`Vec<Lit>`] is not possible due to the coefficient being larger than 1.
pub fn merge_in_situ_lits(
    clause_term: &mut Peekable<Iter<'_, Lit>>,
    summand_term: &mut Peekable<Iter<'_, impl PBTerm>>,
    resulting_lits: &mut Vec<Lit>,
    cancel: &mut i64,
) {
    loop {
        match (clause_term.peek(), summand_term.peek()) {
            (None, None) => break,
            (None, Some(term)) => {
                if !term.get_coeff().is_one() {
                    break;
                }
                resulting_lits.push(term.get_lit());
                summand_term.next();
            }
            (Some(&lit), None) => {
                resulting_lits.push(*lit);
                clause_term.next();
            }
            (Some(&lit), Some(term)) => match lit.get_var().cmp(&term.get_lit().get_var()) {
                std::cmp::Ordering::Less => {
                    resulting_lits.push(*lit);
                    clause_term.next();
                }
                std::cmp::Ordering::Greater => {
                    if !term.get_coeff().is_one() {
                        break;
                    }
                    resulting_lits.push(term.get_lit());
                    summand_term.next();
                }
                std::cmp::Ordering::Equal => {
                    match (lit.is_negated(), term.get_lit().is_negated()) {
                        (false, false) | (true, true) => break,
                        _ => {
                            if *term.get_coeff() == From::from(2) {
                                resulting_lits.push(term.get_lit());
                            } else if !term.get_coeff().is_one() {
                                break;
                            }
                            *cancel += 1;
                            clause_term.next();
                            summand_term.next();
                        }
                    }
                }
            },
        }
    }
}

/// Merge [`Vec<Lit>`] literals and [`Vec<PBTerm`>] to [`Vec<GeneralPBTerm<N>>`].
///
/// This function immediately returns if merging the term in the [`Vec<GeneralPBTerm<N>>`] is not possible due to the coefficient being larger than [`N::MAX`].
pub fn merge_from_lits<N: Int>(
    mut clause_term: Peekable<Iter<'_, Lit>>,
    mut summand_term: Peekable<Iter<'_, impl PBTerm>>,
    resulting_terms: &mut Vec<GeneralPBTerm<N>>,
    cancel: &mut N,
) {
    loop {
        match (clause_term.peek(), summand_term.peek()) {
            (None, None) => break,
            (None, Some(&term)) => {
                resulting_terms.push(GeneralPBTerm::new(
                    term.get_coeff().to_owned().into().try_into().ok().unwrap(),
                    term.get_lit(),
                ));
                summand_term.next();
            }
            (Some(&lit), None) => {
                resulting_terms.push(GeneralPBTerm::new(N::one(), *lit));
                clause_term.next();
            }
            (Some(&lit), Some(&term)) => match lit.get_var().cmp(&term.get_lit().get_var()) {
                std::cmp::Ordering::Less => {
                    resulting_terms.push(GeneralPBTerm::new(N::one(), *lit));
                    clause_term.next();
                }
                std::cmp::Ordering::Greater => {
                    resulting_terms.push(GeneralPBTerm::new(
                        term.get_coeff().to_owned().into().try_into().ok().unwrap(),
                        term.get_lit(),
                    ));
                    summand_term.next();
                }
                std::cmp::Ordering::Equal => {
                    let term = GeneralPBTerm::new(
                        Into::<BigInt>::into(term.get_coeff().to_owned())
                            .try_into()
                            .ok()
                            .unwrap(),
                        term.get_lit(),
                    );
                    resulting_terms.push(GeneralPBTerm::new(N::one(), *lit));
                    *cancel += resulting_terms.last_mut().unwrap().add_with(term);
                    if resulting_terms.last().unwrap().coeff.is_zero() {
                        resulting_terms.pop();
                    }

                    clause_term.next();
                    summand_term.next();
                }
            },
        }
    }
}