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
82
83
84
85
86
87

//! 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 the [abLiteral] structure, made of an atom (the 'a') and a boolean (the 'b').
//! <div class="warning">
//! Almost all interaction with literals in the library is through the canonical (abLiteral) representation in order to the compiler to decide whether or not to borrow or take ownership of a literal.
//! </div>
//!
//! An example:
//!
//! ```rust
//! # use otter_sat::structures::literal::abLiteral;
//! # use crate::otter_sat::structures::literal::Literal;
//! let atom = 79;
//! let polarity = true;
//! let literal = abLiteral::fresh(atom, polarity);
//!
//! assert!(literal.polarity());
//!
//! assert!(literal.atom().cmp(&79).is_eq());
//! assert!(literal.negate().polarity().cmp(&false).is_eq());
//!
//! assert!(literal.cmp(&abLiteral::fresh(79, !false)).is_eq());
//! ```
//!
//! 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.
//!     This is particularly useful when recording information from [dispatches](crate::dispatch).
//!
//! In other solvers an integer is often used, with the sign of the integer indicating the value of the literal.

#[allow(non_snake_case)]
#[doc(hidden)]
mod impl_abLiteral;

use crate::{
    db::{atom::AtomDB, ClauseKey},
    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 fresh(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) -> abLiteral;

    /// The external representation of the literal.
    /// Specifically, the external representation of the atom of the literal, prefexied with a minus sign if the literal has negative polarity.
    fn external_representation(&self, atom_db: &AtomDB) -> String;
}

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

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

/// how a literal was settled
#[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),
}