Trait Solve

Source

pub trait Solve: Extend<Clause> + for<'a> Extend<&'a Clause> {
Show 14 methods    // Required methods
    fn signature(&self) -> &'static str;
    fn solve(&mut self) -> Result<SolverResult>;
    fn lit_val(&self, lit: Lit) -> Result<TernaryVal>;
    fn add_clause_ref<C>(&mut self, clause: &C) -> Result<()>
       where C: AsRef<Cl> + ?Sized;

    // Provided methods
    fn reserve(&mut self, _max_var: Var) -> Result<()> { ... }
    fn solution(&self, high_var: Var) -> Result<Assignment> { ... }
    fn full_solution(&self) -> Result<Assignment>
       where Self: SolveStats { ... }
    fn var_val(&self, var: Var) -> Result<TernaryVal> { ... }
    fn add_clause(&mut self, clause: Clause) -> Result<()> { ... }
    fn add_unit(&mut self, lit: Lit) -> Result<()> { ... }
    fn add_binary(&mut self, lit1: Lit, lit2: Lit) -> Result<()> { ... }
    fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) -> Result<()> { ... }
    fn add_cnf(&mut self, cnf: Cnf) -> Result<()> { ... }
    fn add_cnf_ref(&mut self, cnf: &Cnf) -> Result<()> { ... }
}

Expand description

Trait for all SAT solvers in this library. Solvers outside of this library can also implement this trait to be able to use them with this library.

Note: the Extend implementations call Solve::add_clause or Solve::add_clause_ref internally but convert errors to panics.

Required Methods§

Source

fn signature(&self) -> &'static str

Gets a signature of the solver implementation

Source

fn solve(&mut self) -> Result<SolverResult>

Solves the internal CNF formula without any assumptions.

§Example

// any other solver crate works the same way
let mut solver = rustsat_minisat::core::Minisat::default();
solver.add_unit(lit![0]).unwrap();
let res = solver.solve().unwrap();
debug_assert_eq!(res, SolverResult::Sat);

§Errors

A solver may return any error. One typical option might be crate::OutOfMemory.

Source

fn lit_val(&self, lit: Lit) -> Result<TernaryVal>

Gets an assignment of a variable in the solver.

§Example

// any other solver crate works the same way
let mut solver = rustsat_minisat::core::Minisat::default();
solver.add_unit(lit![0]).unwrap();
let res = solver.solve().unwrap();
debug_assert_eq!(solver.lit_val(lit![0]).unwrap(), TernaryVal::True);

§Errors

If the solver is not in the satisfied state return StateError
A specific implementation might return other errors

Source

fn add_clause_ref<C>(&mut self, clause: &C) -> Result<()>
where C: AsRef<Cl> + ?Sized,

Adds a clause to the solver by reference. If the solver is in the satisfied or unsatisfied state before, it is in the input state afterwards.

§Errors

If the solver is in an invalid state, returns StateError
A specific implementation might return other errors

Provided Methods§

Source

fn reserve(&mut self, _max_var: Var) -> Result<()>

Reserves memory in the solver until a maximum variables, if the solver supports it

§Errors

A solver may return any error. One typical option might be crate::OutOfMemory.

Source

fn solution(&self, high_var: Var) -> Result<Assignment>

Gets a solution found by the solver up to a specified highest variable.

§Errors

If the solver is not in the satisfied state, returns StateError
A specific implementation might return other errors

Source

fn full_solution(&self) -> Result<Assignment>
where Self: SolveStats,

Gets a solution found by the solver up to the highest variable known to the solver.

§Errors

If the solver is not in the satisfied state, returns StateError
A specific implementation might return other errors

Source

fn var_val(&self, var: Var) -> Result<TernaryVal>

Same as Solve::lit_val, but for variables.

§Errors

If the solver is not in the satisfied state, returns StateError
A specific implementation might return other errors

Source

fn add_clause(&mut self, clause: Clause) -> Result<()>

Adds a clause to the solver. If the solver is in the satisfied or unsatisfied state before, it is in the input state afterwards.

This method can be implemented by solvers that can truly take ownership of the clause. Otherwise, it will fall back to the mandatory Solve::add_clause_ref method.