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

use super::Clause;

/// A rough distinction between clauses, based on number of literals.
pub enum ClauseKind {
    /// The clause is empty
    Empty,
    /// The clause is a single literal.
    Unit,
    /// The clause is exactly two literals.
    Binary,
    /// The clause is (inexactly) more than two literals.
    Long,
}

impl ClauseKind {
    /// Identifies what kind of a clause a clause is.
    pub fn identify(clause: &impl Clause) -> Self {
        match clause.size() {
            0 => Self::Empty,
            1 => Self::Unit,
            2 => Self::Binary,
            _ => Self::Long,
        }
    }
}