Trait splr::SolveIF[−][src]

pub trait SolveIF {
    fn solve(&mut self) -> SolverResult;
}

API to solve SAT problems.

Required methods

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

search an assignment.

Errors

if solver becomes inconsistent by an internal error.

Loading content...

Implementors

impl SolveIF for Solver[src]

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

Examples

use splr::*;

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);
}
Loading content...