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

#![allow(clippy::restriction)]

pub mod args;
pub mod context;
pub mod database;
pub mod deletion_sequence;
pub mod elaborator;
pub mod error;
pub mod misc_tokens;
pub mod occurrence_list;
pub mod order;
pub mod order_context;
pub mod parser;
pub mod prelude;
pub mod proofgoal;
pub mod rules;
pub mod subproof_context;
pub mod utils;
pub mod verifier;

use std::{ffi::OsStr, fs::File};

use ahash::AHashMap;
use args::Args;
use error::VeriPBError;
use memmap2::Mmap;
use parser::{error::ParseError, parser::Parser, utils::Position};
use prelude::*;
use veripb_formula::prelude::*;
use veripb_parser::{
    cnf_parser::parse_cnf_from_file, opb_parser::parse_opb_from_file,
    wcnf_parser::parse_wcnf_from_file,
};

pub fn run_checker(args: Args) -> anyhow::Result<()> {
    let pbp_file = File::open(&args.derivation).unwrap();
    let pbp_mmap = unsafe { Mmap::map(&pbp_file).unwrap() };
    let (formula, variables, formula_labels) = if args.cnf
        || (!args.opb && !args.wcnf && args.formula.extension() == Some(OsStr::new("cnf")))
    {
        let (formula, num_vars) = parse_cnf_from_file(&args.formula)?;
        let mut variables = VarNameManager::with_capacity(num_vars + 1);
        variables.add_by_name("");
        for i in 1..=num_vars {
            variables.add_by_name(&format!("x{i}"));
        }
        (formula, variables, AHashMap::new())
    } else if args.wcnf || (!args.opb && args.formula.extension() == Some(OsStr::new("wcnf"))) {
        let (formula, var_names) = parse_wcnf_from_file(&args.formula)?;
        (formula, var_names, AHashMap::new())
    } else {
        parse_opb_from_file(&args.formula)?
    };

    let context = Context::new(args, variables);
    let mut verifier = Verifier::new(context, formula)?;
    verifier.initialize()?;
    let mut parser = Parser::new(pbp_mmap, &mut verifier, formula_labels);
    match parser.parse() {
        Err(error) => {
            if let VeriPBError::Parse(ParseError {
                pos:
                    Position {
                        pos: 0,
                        col: 1,
                        line: 0,
                    },
                ..
            }) = error
            {
                if verifier.context.args.print_verification_result {
                    println!("Info: Switched to proof version 2.0 (it is recommended to migrate to proof version 3.0).");
                }
                verifier.verify_file_version_2()?
            } else {
                Err(error)?
            }
        }
        result => result?,
    }

    if verifier.context.assumption_used && verifier.context.args.show_warnings {
        println!("Warning: The proof used unchecked assumptions.");
    }
    Ok(())
}