[−][src]Trait splr::SatSolverIF

pub trait SatSolverIF {
    fn add_unchecked_clause(&mut self, lits: &mut Vec<Lit>) -> Option<ClauseId>;

    fn build(config: &Config) -> Result<Solver, SolverError>;
}

API for SAT solver like build, solve and so on.

Required methods

fn add_unchecked_clause(&mut self, lits: &mut Vec<Lit>) -> Option<ClauseId>

add a clause to Solver.

fn build(config: &Config) -> Result<Solver, SolverError>

make a solver and load a CNF into it.

Errors

IO error by failing to load a CNF file.

Loading content...

Implementors

impl SatSolverIF for Solver[src]

fn build(config: &Config) -> Result<Solver, SolverError>[src]

Examples

use splr::config::Config;
use splr::solver::{SatSolverIF, Solver};

let config = Config::from("tests/sample.cnf");
assert!(Solver::build(&config).is_ok());
Loading content...