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

//! 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::Preprocessing> {
        if self.config.switch.preprocessing {
            match set_pure(self) {
                Ok(()) => {}
                Err(_) => {
                    log::error!(target: targets::PREPROCESSING, "Failed to set pure literals");
                    return Err(err::Preprocessing::Pure);
                }
            };
        }
        Ok(())
    }
}