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

use core::fmt::{self, Debug, Display};
pub use NoSuccessKind::*;
pub use SuccessKind::*;

pub struct Status<K>(pub K);

impl<K: Debug> Display for Status<K> {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        writeln!(f, "% SZS status {:?}", self.0)
    }
}

pub struct Output<O>(pub O);

impl<O: Display> Display for Output<O> {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        writeln!(f, "% SZS output start")?;
        writeln!(f, "{}", self.0)?;
        writeln!(f, "% SZS output end")
    }
}

#[derive(Debug)]
pub enum SuccessKind {
    Theorem,
    Satisfiable,
}

#[derive(Debug)]
pub enum NoSuccessKind {
    OSError,
    InputError,
    SyntaxError,
    SemanticError,
    Incomplete,
    Inappropriate,
}