otter_sat 0.1.0

A library for determining the satisfiability of boolean formulas written in conjunctive normal form, developed to support investigation into solvers by researchers, developers, or anyone curious.
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

/*!
Reports for the context.
*/

use crate::context::ContextState;

pub mod frat;

/// High-level reports regarding a solve.
#[derive(PartialEq, Eq, Clone, Copy, Debug)]
pub enum Report {
    /// The formula of the context is satisfiable.
    Satisfiable,

    /// The formula of the context is unsatisfiable.
    Unsatisfiable,

    /// Satisfiability of the formula of the context is unknown, for some reason.
    Unknown,
}

impl From<ContextState> for Report {
    fn from(value: ContextState) -> Self {
        match value {
            ContextState::Configuration | ContextState::Input | ContextState::Solving => {
                Self::Unknown
            }
            ContextState::Satisfiable => Self::Satisfiable,
            ContextState::Unsatisfiable(_) => Self::Unsatisfiable,
        }
    }
}

impl std::fmt::Display for Report {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Satisfiable => write!(f, "Satisfiable"),
            Self::Unsatisfiable => write!(f, "Unsatisfiable"),
            Self::Unknown => write!(f, "Unknown"),
        }
    }
}