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