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

use std::rc::Rc;

use veripb_formula::prelude::DBConstraint;

use crate::prelude::*;

#[derive(Debug)]
pub struct OrderProofRule;

impl Rule for OrderProofRule {
    fn compute(
        &mut self,
        context: &mut Context,
        database: &mut Database,
    ) -> Result<Vec<Rc<DBConstraint>>, CheckingError> {
        let mut subproof_context = SubproofContext::new(database.len());
        let (last_subcontext, subcontexts) = match context.subcontexts.split_last_mut() {
            Some((last, subcontexts)) => (last, subcontexts),
            None => return Err(CheckingError::ProofOnlyInReflexivityOrTransitivity),
        };
        let order_context = match subcontexts.last() {
            Some(Subcontext::Order(order)) => order,
            _ => return Err(CheckingError::ProofOnlyInReflexivityOrTransitivity),
        };
        let mut premises = Vec::new();

        match last_subcontext {
            Subcontext::Reflexivity(reflexivity) => {
                if reflexivity.is_proven {
                    return Err(CheckingError::ReflexivityAlreadyProven);
                }
                reflexivity.is_proven = true;
                let reflexivity_substitution = order_context.get_reflexivity_substitution();

                // Get the additional premises for reflexivity.
                for constraint in order_context.constructed_order.specification.iter() {
                    premises.push(Rc::new(constraint.substitute(&reflexivity_substitution)));
                }

                // Get the proofgoals for reflexivity.
                for constraint in order_context.constructed_order.definition.iter() {
                    let proofgoal = Rc::new(constraint.substitute(&reflexivity_substitution));
                    subproof_context.add_single_proofgoal(proofgoal, None);
                }
                if context.args.trace {
                    println!("  ** proofgoals for reflexivity **");
                    subproof_context.trace_all_internal_proofgoals(&context.var_names);
                }
            }
            Subcontext::Transitivity(transitivity) => {
                if transitivity.is_proven {
                    return Err(CheckingError::TransitivityAlreadyProven);
                }
                transitivity.is_proven = true;
                let (transitivity_substitution_y_z, transitivity_substitution_x_z) =
                    order_context.get_transitivity_substitution(transitivity);

                // Get additional premises from the specification.
                for constraint in order_context.constructed_order.specification.iter() {
                    premises.push(Rc::new(DBConstraint::from(constraint.constraint.clone())));
                }
                for constraint in order_context.constructed_order.specification.iter() {
                    premises.push(Rc::new(
                        constraint.substitute(&transitivity_substitution_y_z),
                    ));
                }
                for constraint in order_context.constructed_order.specification.iter() {
                    premises.push(Rc::new(
                        constraint.substitute(&transitivity_substitution_x_z),
                    ));
                }

                // Get additional premises and proofgoals from definition constraints.
                for constraint in order_context.constructed_order.definition.iter() {
                    premises.push(constraint.clone());
                    let proofgoal = Rc::new(constraint.substitute(&transitivity_substitution_x_z));
                    subproof_context.add_single_proofgoal(proofgoal, None);
                }
                for constraint in order_context.constructed_order.definition.iter() {
                    premises.push(Rc::new(
                        constraint.substitute(&transitivity_substitution_y_z),
                    ));
                }
                if context.args.trace {
                    println!("  ** proofgoals for transitivity **");
                    subproof_context.trace_all_internal_proofgoals(&context.var_names);
                }
            }
            _ => return Err(CheckingError::ProofOnlyInReflexivityOrTransitivity),
        }

        context
            .subcontexts
            .push(Subcontext::Subproof(subproof_context));

        // Add premise constraints
        Ok(premises)
    }

    #[inline]
    fn elaborate(
        &self,
        context: &mut Context,
        _database: &Database,
    ) -> Result<(), ElaborationError> {
        context.elaborator.as_mut().unwrap().writeln("\tproof");
        Ok(())
    }
}