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

//! Implementation details of the [literal trait](Literal) for the [abLiteral] structure.

use crate::{
    db::atom::AtomDB,
    structures::atom::Atom,
    structures::literal::{abLiteral, Literal},
};

impl Literal for abLiteral {
    fn fresh(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::abLiteral {
        *self
    }

    fn external_representation(&self, atom_db: &AtomDB) -> String {
        let mut the_string = String::new();
        if !self.polarity {
            the_string.push('-');
        }
        the_string.push_str(atom_db.external_representation(self.atom).as_str());
        the_string
    }
}

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 PartialEq for abLiteral {
    fn eq(&self, other: &Self) -> bool {
        self.atom == other.atom && self.polarity == other.polarity
    }
}

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 Eq for abLiteral {}

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),
        }
    }
}