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
34
35

use crate::{
    config::Config,
    db::{atom::AtomDB, clause::ClauseDB, consequence_q::ConsequenceQ, literal::LiteralDB},
    generic::minimal_pcg::MinimalPCG32,
    resolution_buffer::ResolutionBuffer,
};

use rand::SeedableRng;

use super::{ContextState, Counters, GenericContext};

/// A context which uses [MinimalPCG32] as a source of randomness.
pub type Context = GenericContext<MinimalPCG32>;

impl Context {
    /// Creates a context from some given configuration.
    pub fn from_config(config: Config) -> Self {
        Self {
            atom_db: AtomDB::new(&config),
            clause_db: ClauseDB::new(&config),
            literal_db: LiteralDB::new(&config),
            resolution_buffer: ResolutionBuffer::new(&config),

            config,

            consequence_q: ConsequenceQ::default(),
            counters: Counters::default(),

            rng: crate::generic::minimal_pcg::MinimalPCG32::from_seed(0_u64.to_le_bytes()),
            state: ContextState::Configuration,

            callback_terminate: None,
        }
    }
}