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

use crate::{
    misc::log::targets::{self},
    structures::literal::{CLiteral, Literal},
    types::err::{self},
};

/// The index to a formula.
pub type FormulaIndex = u32;

/// The token of a formula index, used to distinguish re-use of the same [FormulaIndex].
pub type FormulaToken = u16;

/// A key to access a clause stored in the clause database.
///
/// Within the clause database clauses are stored in some indexed structure (e.g. a vector) an keys contain the index to the clause together with a token to distinguish reuse of the same index, where relevant.
///
/// The only exception to this is unit clauses.
/// Here, the index is to the atom database.
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub enum ClauseKey {
    /// The key to a unit clause contains the (unit) clause.
    OriginalUnit(CLiteral),

    /// The key to a unit clause contains the (unit) clause.
    AdditionUnit(CLiteral),

    /// The key to a binary clause.
    OriginalBinary(FormulaIndex),

    /// The key to a binary clause.
    AdditionBinary(FormulaIndex),

    /// The key to an original clause.
    Original(FormulaIndex),

    /// The key to an addition.
    Addition(FormulaIndex, FormulaToken),
}

impl ClauseKey {
    /// Extracts the index from a key.
    pub fn index(&self) -> usize {
        match self {
            Self::OriginalUnit(l) | Self::AdditionUnit(l) => l.atom() as usize,
            Self::OriginalBinary(i) | Self::AdditionBinary(i) => *i as usize,
            Self::Original(i) => *i as usize,
            Self::Addition(i, _) => *i as usize,
        }
    }

    /// Retokens an addition key to distnguish multiple uses of the same index.
    ///
    /// Returns an error if used on any other key, or if the token limit has been reached.
    pub fn retoken(&self) -> Result<Self, err::ClauseDBError> {
        match self {
            Self::OriginalUnit(_) | Self::AdditionUnit(_) => {
                log::error!(target: targets::CLAUSE_DB, "Unit keys have a unique token");
                Err(err::ClauseDBError::InvalidKeyToken)
            }

            Self::Original(_) => {
                log::error!(target: targets::CLAUSE_DB, "Formula keys have a unique token");
                Err(err::ClauseDBError::InvalidKeyToken)
            }

            Self::OriginalBinary(_) | Self::AdditionBinary(_) => {
                log::error!(target: targets::CLAUSE_DB, "Binary keys have a unique token");
                Err(err::ClauseDBError::InvalidKeyToken)
            }

            Self::Addition(index, token) => {
                if *token == FormulaToken::MAX {
                    return Err(err::ClauseDBError::StorageExhausted);
                }
                Ok(ClauseKey::Addition(*index, token + 1))
            }
        }
    }
}

impl std::fmt::Display for ClauseKey {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::OriginalUnit(key) => write!(f, "OriginalUnit({key})"),
            Self::AdditionUnit(key) => write!(f, "AdditionUnit({key})"),
            Self::OriginalBinary(key) => write!(f, "OriginalBinary({key})"),
            Self::AdditionBinary(key) => write!(f, "AdditionBinary({key})"),
            Self::Original(key) => write!(f, "Formula({key})"),
            Self::Addition(key, token) => write!(f, "Addition({key}, {token})"),
        }
    }
}