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

use crate::structures::atom::Atom;

use super::{ABLiteral, Literal};

/// The representation of a literal as an atom paired with a boolean.
#[allow(non_camel_case_types)]
pub type IntLiteral = i32;

impl Literal for IntLiteral {
    fn new(atom: Atom, polarity: bool) -> Self {
        match polarity {
            true => atom as IntLiteral,
            false => -(atom as IntLiteral),
        }
    }

    fn negate(&self) -> Self {
        -self
    }

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

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

    fn canonical(&self) -> super::CLiteral {
        #[cfg(feature = "boolean")]
        return ABLiteral::new(self.atom(), self.polarity());

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

    fn as_int(&self) -> isize {
        *self as isize
    }
}

// From

impl From<ABLiteral> for IntLiteral {
    fn from(value: ABLiteral) -> Self {
        let atom = value.atom();
        match value.polarity() {
            true => atom as IntLiteral,
            false => -(atom as IntLiteral),
        }
    }
}

impl From<&ABLiteral> for IntLiteral {
    fn from(value: &ABLiteral) -> Self {
        let atom = value.atom();
        match value.polarity() {
            true => atom as IntLiteral,
            false => -(atom as IntLiteral),
        }
    }
}

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

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