Struct cryptominisat::Solver
[−]
[src]
pub struct Solver(_);
Methods
impl Solver[src]
fn new() -> Solver
Create new solver instance
fn nvars(&self) -> u32
Current number of variables. Call new_var() or new_vars() to increase this.
fn add_clause(&mut self, lits: &[Lit]) -> bool
Current number of variables
fn add_xor_clause(&mut self, vars: &[u32], rhs: bool) -> bool
Add a xor clause, which enforces that the xor of the unnegated variables equals rhs. It is generally more convienent to use add_xor_literal_clause() instead.
fn new_vars(&mut self, n: size_t)
Adds n new variabless.
fn solve(&mut self) -> Lbool
Solve and return Lbool::True if a solution was found.
fn solve_with_assumptions(&mut self, assumptions: &[Lit]) -> Lbool
Solve under the assumption that the passed literals are true and return Lbool::True if a solution was found.
fn get_model(&self) -> &[Lbool]
Returns true/false/unknown status for each variable.
fn get_conflict(&self) -> &[Lit]
Return conflicts for assumptions that led to unsatisfiability.
fn set_num_threads(&mut self, n: u32)
Set number of threads used for solving. Must not be called after other methods.
fn new_var(&mut self) -> Lit
Helper that adds a variable and returns the corresponding literal.
fn is_true(&self, lit: Lit) -> bool
Wrapper which calls get_model() and returns whether the given literal is true.
fn add_xor_literal_clause(&mut self, lits: &[Lit], rhs: bool) -> bool
Wrapper which converts literals to variables and then calls add_xor_clause()