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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161

use crate::structures::{
    atom::{Atom, ATOM_MAX},
    clause::ABClause,
};

use super::{IntLiteral, Literal};

/// The representation of a literal as an atom paired with a boolean.
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, Debug)]
pub struct ABLiteral {
    /// The atom of a literal.
    atom: Atom,

    /// The polarity of a literal.
    polarity: bool,
}

impl Literal for ABLiteral {
    fn new(atom: Atom, polarity: bool) -> Self {
        Self { atom, polarity }
    }

    fn negate(&self) -> Self {
        Self {
            atom: self.atom,
            polarity: !self.polarity,
        }
    }

    fn atom(&self) -> Atom {
        self.atom
    }

    fn polarity(&self) -> bool {
        self.polarity
    }

    fn canonical(&self) -> super::CLiteral {
        #[cfg(feature = "boolean")]
        return *self;

        #[cfg(not(feature = "boolean"))]
        return self.into();
    }

    fn as_int(&self) -> isize {
        match self.polarity {
            true => self.atom as isize,
            false => -(self.atom as isize),
        }
    }
}

// Traits

impl PartialOrd for ABLiteral {
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        Some(self.cmp(other))
    }
}

impl Ord for ABLiteral {
    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
        if self.atom == other.atom {
            self.polarity.cmp(&other.polarity)
        } else {
            self.atom.cmp(&other.atom)
        }
    }
}

impl PartialOrd<IntLiteral> for ABLiteral {
    fn partial_cmp(&self, other: &IntLiteral) -> Option<std::cmp::Ordering> {
        Some(self.cmp(&ABLiteral::from(other)))
    }
}

impl PartialEq for ABLiteral {
    fn eq(&self, other: &Self) -> bool {
        self.atom == other.atom && self.polarity == other.polarity
    }
}

impl PartialEq<IntLiteral> for ABLiteral {
    fn eq(&self, other: &IntLiteral) -> bool {
        self.atom == other.atom() && self.polarity == other.polarity()
    }
}

impl Eq for ABLiteral {}

impl std::hash::Hash for ABLiteral {
    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
        self.atom.hash(state);
        self.polarity.hash(state);
    }
}

impl std::fmt::Display for ABLiteral {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self.polarity {
            true => write!(f, "{}", self.atom),
            false => write!(f, "-{}", self.atom),
        }
    }
}

// From

impl From<i16> for ABLiteral {
    fn from(value: i16) -> Self {
        ABLiteral::new(value.unsigned_abs() as Atom, value.is_positive())
    }
}

impl From<i32> for ABLiteral {
    fn from(value: i32) -> Self {
        ABLiteral::new(value.unsigned_abs(), value.is_positive())
    }
}

impl From<&i32> for ABLiteral {
    fn from(value: &i32) -> Self {
        ABLiteral::new(value.unsigned_abs(), value.is_positive())
    }
}

impl TryFrom<i64> for ABLiteral {
    type Error = ();

    fn try_from(value: i64) -> Result<Self, Self::Error> {
        let atom = value.unsigned_abs();
        if atom < ATOM_MAX.into() {
            Ok(ABLiteral::new(atom as Atom, value.is_positive()))
        } else {
            Err(())
        }
    }
}

impl TryFrom<isize> for ABLiteral {
    type Error = ();

    fn try_from(value: isize) -> Result<Self, Self::Error> {
        let atom = value.unsigned_abs();
        if ATOM_MAX.try_into().is_ok_and(|max| atom < max) {
            Ok(ABLiteral::new(atom as Atom, value.is_positive()))
        } else {
            Err(())
        }
    }
}

// Into

impl Into<ABClause> for ABLiteral {
    fn into(self) -> ABClause {
        vec![self]
    }
}