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

/*!
Consequences of the context in some state.

Each consequence is recorded as a [CLiteral] and [Source] pair, with the literal representing an atom-value bind which must hold and the source noting the direct ancestor of the consequence.

If any assumptions or decisions have been made, the consequence is established only relative to those assumptions or decisions.
However, it does not follow the consequence *requires* those assumptions or decisions.

*/
use std::borrow::Borrow;

use crate::{
    db::ClauseKey,
    structures::{
        atom::Atom,
        literal::{CLiteral, Literal},
    },
};

/// The source of a bind.
#[derive(Clone, Copy, PartialEq, Eq)]
#[allow(clippy::upper_case_acronyms)]
pub enum Source {
    /// A decision was made where the alternative the alternative would make no difference to satisfiability.
    PureLiteral,

    /// A consequence of boolean constraint propagation.
    BCP(ClauseKey),
}

#[derive(Clone)]
/// A consequence of the context in some state.
pub struct Consequence {
    /// The atom-value bind which must hold, represented as a literal.
    pub literal: CLiteral,

    /// The immediate reason why the atom-value pair must be.
    pub source: Source,
}

impl Consequence {
    /// Creates a consequence from a bind represented as a literal and a source.
    pub fn from(literal: impl Borrow<CLiteral>, source: Source) -> Self {
        Consequence {
            literal: literal.borrow().canonical(),
            source,
        }
    }

    /// Creates a consequence of the given atom bound to the given value due to the given source.
    pub fn from_bind(atom: Atom, value: bool, source: Source) -> Self {
        Consequence {
            literal: CLiteral::new(atom, value),
            source,
        }
    }

    /// The bound atom.
    pub fn atom(&self) -> Atom {
        self.literal.atom()
    }

    /// The value the atom is bound to.
    pub fn value(&self) -> bool {
        self.literal.polarity()
    }

    /// The atom-value bind, represented as a literal.
    pub fn literal(&self) -> &CLiteral {
        &self.literal
    }

    /// The (immediate) reason why the atom-value bind must hold.
    pub fn source(&self) -> &Source {
        &self.source
    }
}