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

/*!
Literals are atoms paired with a (boolean) polarity.

Or, rather, anything which has methods for returning an atom and a polarity (and a few other useful things).

The 'canonical' implementation of the literal trait is given by the [CLiteral] structure.
This is either:
- An [IntLiteral], which aliases a literal to an integer such that the absolute value of the integer is the atom of the literal, and the sign of the intger is the polarity of the literal.
- An [ABLiteral] which holds an atom (the 'A') and a boolean (the 'B') representing the polarity of the literal.

<div class="warning">
Almost all interaction with literals in the library is through the canonical representation in order to the compiler to decide whether or not to borrow or take ownership.
</div>

Implementation of the literal trait requires implementation of two additional traits:
- [Ord]
  + Literals should be ordered by atom and then polarity, with the (Rust default) ordering of 'false' being (strictly) less than 'true'.
- [Hash](std::hash::Hash)
  + Literals are hashable in order to allow for straightforward use of literals as indicies of maps, etc.

# Examples

```rust
# use otter_sat::structures::literal::{CLiteral, Literal};
let atom = 79;
let polarity = true;
let literal = CLiteral::new(atom, polarity);

assert!(literal.polarity());

assert!(literal.atom().cmp(&79).is_eq());
assert!(literal.negate().polarity().cmp(&false).is_eq());

assert!(literal.cmp(&CLiteral::new(79, !false)).is_eq());
```

Preference is given to abstracting from the specific implementation of literals by using the [CLiteral] type alias.
Still, if [ABLiteral]s or [IntLiteral]s are used, some traits have agnostic implementations.

```rust
# use otter_sat::structures::literal::{ABLiteral, CLiteral, IntLiteral, Literal};
let atom = 14;
let polarity = true;

let canonical_literal = CLiteral::new(atom, polarity);
let ab_literal = ABLiteral::new(atom, polarity);
let int_literal = IntLiteral::new(atom, polarity);

assert_eq!(ab_literal, int_literal);
assert_eq!(ab_literal, canonical_literal);
assert_eq!(canonical_literal, int_literal);
```
*/

#[allow(non_snake_case)]
#[doc(hidden)]
mod ab_literal;
pub use ab_literal::ABLiteral;

mod int_literal;
pub use int_literal::IntLiteral;

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

/// Something which has methods for returning an atom and a polarity, etc.
pub trait Literal: std::cmp::Ord + std::hash::Hash {
    /// A fresh literal, specified by pairing an atom with a boolean.
    fn new(atom: Atom, polarity: bool) -> Self;

    /// The negation of the literal.
    fn negate(&self) -> Self;

    /// The atom of the literal.
    fn atom(&self) -> Atom;

    /// The polarity of the literal.
    fn polarity(&self) -> bool;

    /// The literal in it's 'canonical' form of an atom paired with a boolean.
    fn canonical(&self) -> CLiteral;

    /// The literal in it's integer form, with sign indicating polarity.
    fn as_int(&self) -> isize;
}

#[cfg(not(feature = "boolean"))]
/// The canonical implementation of a literal.
pub type CLiteral = IntLiteral;

#[cfg(feature = "boolean")]
/// The canonical implementation of a literal.
pub type CLiteral = ABLiteral;