Skip to main content

Preprocessor

sat_solver::sat::preprocessing

Trait Preprocessor 

Source 
pub trait Preprocessor<L: Literal, S: LiteralStorage<L>> {
    // Required method
    fn preprocess(&self, cnf: &[Clause<L, S>]) -> Vec<Clause<L, S>>;
}
Expand description

Defines the interface for a CNF formula preprocessor.

A preprocessor takes a list of clauses (representing a CNF formula) and returns a new list of clauses, presumably simplified or transformed in a way that preserves satisfiability.

§Type Parameters

  • L: The Literal type used in clauses.
  • S: The LiteralStorage type for clauses.

Required Methods§

Source

fn preprocess(&self, cnf: &[Clause<L, S>]) -> Vec<Clause<L, S>>

Applies the preprocessing technique to the given CNF formula.

§Arguments
  • cnf: A slice of Clause<L, S> representing the input formula.
§Returns

A Vec<Clause<L, S>> representing the preprocessed formula. This new vector might contain fewer clauses, modified clauses, or new clauses.

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§