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

/*!
Configuration of the resolution buffer.
*/
use crate::config::{Config, StoppingCriteria};

/// Configuration for a resolution buffer.
pub struct BufferConfig {
    /// Whether check for and initiate subsumption.
    pub subsumption: bool,

    /// The stopping criteria to use during resolution.
    pub stopping: StoppingCriteria,
}

impl From<&Config> for BufferConfig {
    fn from(value: &Config) -> Self {
        Self {
            subsumption: value.subsumption.value,
            stopping: value.stopping_criteria.value,
        }
    }
}