otter_sat 0.0.9

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
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

//! Details on the result of some procedure.
use crate::{
    db::ClauseKey,
    structures::{clause::vClause, literal::abLiteral},
};

/// Reports from the context.
#[derive(Clone)]
pub enum Report {
    /// Information regarding a solve.
    Solve(self::Solve),

    /// Information regarding the clause database.
    ClauseDB(self::ClauseDB),

    /// Information regarding the literal database.
    LiteralDB(self::LiteralDB),

    /// Information regarding the parse when building the context.
    Parser(self::Parser),

    /// No further dispatches will be sent regarding the current solve.
    Finish,
}

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

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

    /// Satisfiability of the formula of the context could not be determined within the time allowed.
    TimeUp,

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

/// Information regarding the clause database.
// TODO: It would be nice to break down the dispatch of the clause in line with other dispatches.
#[derive(PartialEq, Eq, Clone)]
pub enum ClauseDB {
    /// An active non-unit clause.
    Active(ClauseKey, vClause),
    /// An active unit clause
    ActiveUnit(abLiteral),
}

/// Information regarding the parse when building the context.
#[derive(PartialEq, Eq, Clone, Debug)]
pub enum Parser {
    /// A DIMACS file has been loaded.
    Load(String),

    /// The expected clause/literal count based on the header of a DIMACS file.
    Expected(usize, usize),

    /// A count of clauses/literals from parsing a DIMACS file.
    Counts(usize, usize),

    /// The count of clauses added to the context from parsing a DIMACS file.
    ContextClauses(usize),
}

/// Information regarding the literal database.
#[derive(PartialEq, Eq, Clone)]
pub enum LiteralDB {}

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

impl std::fmt::Display for self::Parser {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Load(formula) => write!(f, "Parsing \"{formula}\""),
            Self::Expected(a, c) => write!(f, "Expected:     {a} atoms and {c} clauses"),
            Self::Counts(a, c) => write!(f, "Parse result: {a} atoms and {c} clauses"),
            Self::ContextClauses(c) => write!(f, "{c} clauses are in the context"),
        }
    }
}