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

use std::borrow::Borrow;

use crate::structures::literal::{self, abLiteral};

/// A decision level --- the decision and the *observed* consequences of that decision, given prior decisions and observed consequences.
///
/// Note: The consequences relation is reflexive, but no reflexive consequences are observed.
pub struct Level {
    decision: abLiteral,
    consequences: Vec<(literal::Source, abLiteral)>,
}

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

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

    /// The consequences of a level.
    pub fn consequences(&self) -> &[(literal::Source, abLiteral)] {
        &self.consequences
    }

    /// Records a literal consequence of the level from some source.
    ///
    /// No effort is made to check the literal is really a consequence.
    pub fn record_consequence(&mut self, literal: impl Borrow<abLiteral>, source: literal::Source) {
        self.consequences.push((source, *literal.borrow()))
    }
}