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

use crate::structures::{consequence::Consequence, literal::CLiteral};

/// A level storing a literal and its *observed* consequences (given prior assumptions, decisions and observed consequences).
/// As the literal is intended to be a decision or (representative) assumption, the prefix 'AD' is used.
pub struct ADLevel {
    literal: CLiteral,
    consequences: Vec<Consequence>,
}

impl ADLevel {
    /// A new level from some literal, with no recorded consequences.
    pub fn new(literal: CLiteral) -> Self {
        Self {
            literal,
            consequences: vec![],
        }
    }

    /// The literal of a level.
    pub fn literal(&self) -> CLiteral {
        self.literal
    }

    /// The consequences of a level.
    pub fn consequences(&self) -> &[Consequence] {
        &self.consequences
    }

    /// Stores a consequence of the level from some source.
    pub(super) fn store_consequence(&mut self, consequence: Consequence) {
        self.consequences.push(consequence)
    }
}