[−][src]Trait splr::traits::SatSolverIF

pub trait SatSolverIF {
    fn new(config: &Config, cnf: &CNFDescription) -> Solver;

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

    fn solve(&mut self) -> SolverResult;

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

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

Required methods

fn new(config: &Config, cnf: &CNFDescription) -> Solver

make a solver for debug. Probably you should use build instead of this.

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

make a solver and load a CNF into it.

Errors

IO error by failing to load a CNF file.

fn solve(&mut self) -> SolverResult

search an assignment.

Errors

if solver becomes inconsistent by an internal error.

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

add a vector of Lit as a clause to the solver.

Loading content...

Implementors

impl SatSolverIF for Solver[src]

fn solve(&mut self) -> SolverResult[src]

Examples

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

let config = Config::from("tests/sample.cnf");
if let Ok(mut s) = Solver::build(&config) {
    let res = s.solve();
    assert!(res.is_ok());
    assert_ne!(res.unwrap(), Certificate::UNSAT);
}

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

Examples

use splr::traits::SatSolverIF;
use splr::config::Config;
use splr::solver::Solver;

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