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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139

use std::{num::Saturating, rc::Rc};

use ahash::AHashMap;
use colored::Colorize;
use malachite_bigint::BigInt;
use num_traits::Zero;
use veripb_formula::prelude::*;
use veripb_propagator::propagation_engine::PropagationEngine;

use crate::{
    args::Args,
    order_context::{OrderContext, ReflexivityContext, SpecificationContext, TransitivityContext},
    prelude::*,
    rules::ObjectiveUpdateType,
};

// Index of propagation sets.
pub const CORE: usize = 0;
pub const DERIVED: usize = 1;
pub const AUTOPROVING: usize = 2;

// Constants for the checker.
pub const REQUIRED_RUP_STREAK: Saturating<u8> = Saturating(5);

#[derive(Debug)]
pub enum Subcontext {
    Subproof(SubproofContext),
    Order(OrderContext),
    Transitivity(TransitivityContext),
    Reflexivity(ReflexivityContext),
    Specification(SpecificationContext),
}

impl Subcontext {
    #[inline]
    pub fn is_subproof(&self) -> bool {
        matches!(self, Subcontext::Subproof(_))
    }
}

/// Context to store the state of the verifier.
#[derive(Debug, Default)]
pub struct Context {
    /// Command line arguments
    pub args: Args,
    /// Storage of variable names and used variables.
    pub var_names: VarNameManager,
    /// Original formula.
    pub original_constraints: Vec<Rc<DBConstraint>>,
    /// Current objective.
    pub objective: Option<PBObjective>,
    /// The currently best objective value logged while checked deletion was enabled.
    pub best_valid_objective_value: Option<BigInt>,
    /// The currently best objective value over all.
    pub best_objective_value: Option<BigInt>,
    /// Stack of currently used subproof contexts.
    pub subcontexts: Vec<Subcontext>,
    /// A flag to determine if we are inside a strengthening subproof, where some rules are not allowed.
    pub inside_strengthening_subproof: bool,
    /// Propagation engine for checks by propagation.
    pub propagation_engine: PropagationEngine,
    /// All orders known to checker.
    pub orders: AHashMap<String, Order>,
    /// The currently active order.
    pub active_order: Option<ActiveOrder>,
    /// Current streak autoproving red rules by the constraint being RUP.
    pub rup_streak: Saturating<u8>,
    /// Stored assignment for annotated RUP steps.
    pub annotated_rup_assignment: Assignment<BooleanVar>,
    /// Proof major version.
    pub major_version: Option<u8>,
    /// Proof minor version.
    pub minor_version: Option<u8>,
    /// Proof flags.
    pub has_output: bool,
    pub has_conclusion: bool,
    pub has_end_proof: bool,
    pub assumption_used: bool,
    /// Elaborator
    pub elaborator: Option<Elaborator>,
    /// The current level that is set
    pub current_level: Option<usize>,
    /// The storage of constraint IDs for each level
    pub level_ids: Vec<Vec<usize>>,
    /// Store if only core constraints can be used for proof.
    pub only_core: bool,
    /// Stores if the strengthening to core is more is enabled.
    pub is_strengthening_to_core: bool,
}

impl Context {
    pub fn new(args: Args, var_names: VarNameManager) -> Context {
        Context {
            args,
            var_names,
            propagation_engine: new_veripb_propagation_engine(),
            rup_streak: REQUIRED_RUP_STREAK,
            ..Default::default()
        }
    }

    pub fn update_objective(
        &mut self,
        mut objective_update: PBObjective,
        update_type: ObjectiveUpdateType,
    ) {
        match update_type {
            ObjectiveUpdateType::New => self.objective = Some(objective_update),
            ObjectiveUpdateType::Diff => {
                // Change the objective by the diff.
                let objective = self.objective.as_mut().unwrap();
                objective.constant += objective_update.constant;
                while let Some((var, term)) = objective_update.terms.pop_first() {
                    if let Some(existing_term) = objective.terms.get_mut(&var) {
                        objective.constant += existing_term.add_with(term);
                        if existing_term.coeff.is_zero() {
                            objective.terms.remove(&var);
                        }
                    } else {
                        objective.terms.insert(var, term);
                    }
                }
            }
        }

        // Trace objective change.
        if self.args.trace {
            println!(
                "  {} updated to: {}",
                "Objective".bright_green(),
                self.objective
                    .as_ref()
                    .unwrap()
                    .to_pretty_string(&self.var_names)
                    .green()
            );
        }
    }
}