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

use crate::{config::ConfigOption, context::ContextState};

/// Configuration of the literal database.
#[derive(Clone)]
pub struct LiteralDBConfig {
    /// Whether to stack assumptions on individual levels, or combine all assumptions on a single level.
    pub stacked_assumptions: ConfigOption<bool>,
}

impl Default for LiteralDBConfig {
    fn default() -> Self {
        Self {
            stacked_assumptions: ConfigOption {
                name: "stacked_assumptions",
                min: false,
                max: true,
                max_state: ContextState::Configuration,
                value: false,
            },
        }
    }
}