Module reader 

Proofs can be read using a ProofReader. It reads the proof line-by-line, and can be thought of as an Iterator over Step.

The reader does not do any form of validation of the proof. It is up to the consumer of this crate to ensure that constraint IDs are valid, that inference labels make sense, etc.

use std::num::NonZero;
use std::rc::Rc;

use drcp_format::Conclusion;
use drcp_format::Deduction;
use drcp_format::Inference;
use drcp_format::IntAtomic;
use drcp_format::IntComparison::*;
use drcp_format::Step;
use drcp_format::reader::ProofReader;

let source = r#"
    a 1 [x1 >= 0]
    a 2 [x2 >= 0]
    i 2 1 0 2 c:1 l:inf_name
    n 3 1 -2 0 2
    c UNSAT
"#;

let a1 = IntAtomic {
    name: Rc::from("x1".to_owned()),
    comparison: GreaterEqual,
    value: 0,
};

let a2 = IntAtomic {
    name: Rc::from("x2".to_owned()),
    comparison: GreaterEqual,
    value: 0,
};

let mut reader = ProofReader::<_, i32>::new(source.as_bytes());

let inference = reader
    .next_step()
    .expect("no error reading")
    .expect("proof step exists");

assert_eq!(
    inference,
    Step::Inference(Inference {
        constraint_id: NonZero::new(2).unwrap(),
        premises: vec![a1.clone()],
        consequent: Some(a2.clone()),
        generated_by: Some(NonZero::new(1).unwrap()),
        label: Some("inf_name".into()),
    })
);

let deduction = reader
    .next_step()
    .expect("no error reading")
    .expect("proof step exists");

assert_eq!(
    deduction,
    Step::Deduction(Deduction {
        constraint_id: NonZero::new(3).unwrap(),
        premises: vec![a1.clone(), !a2],
        sequence: vec![NonZero::new(2).unwrap()],
    })
);

let conclusion = reader
    .next_step()
    .expect("no error reading")
    .expect("proof step exists");

assert_eq!(conclusion, Step::Conclusion(Conclusion::Unsat));

let eof = reader.next_step().expect("no error reading");
assert_eq!(eof, None);

Structs

ProofReader

A parser of DRCP proofs. See module documentation on crate::reader for examples on how to use it.

Enums

Error

The errors that can be encountered by the ProofReader.

Type Aliases

ReadAtomic

The IntAtomic type that is produced by the ProofReader.

ReadStep

The Step type that is produced by the ProofReader.