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

/*!
Procedures for preprocessing formulas.
*/
use pure::set_pure;

use crate::{
    context::GenericContext,
    misc::log::targets::{self},
    types::err::{self},
};

pub mod pure;

impl<R: rand::Rng + std::default::Default> GenericContext<R> {
    /// Applies preprocessing in accordance with the configuration of the context.
    pub fn preprocess(&mut self) -> Result<(), err::PreprocessingError> {
        if self.config.preprocessing.value {
            match set_pure(self) {
                Ok(()) => {}
                Err(_) => {
                    log::error!(target: targets::PREPROCESSING, "Failed to set pure literals");
                    return Err(err::PreprocessingError::Unsatisfiable);
                }
            };
        }
        Ok(())
    }
}