Struct ratsat::core::Solver
[−]
[src]
pub struct Solver { pub model: Vec<lbool>, // some fields omitted }
Fields
model: Vec<lbool>
If problem is satisfiable, this vector contains the model (if any).
Methods
impl Solver
[src]
pub fn new(opts: SolverOpts) -> Self
[src]
pub fn set_verbosity(&mut self, verbosity: i32)
[src]
pub fn num_clauses(&self) -> u32
[src]
pub fn num_learnts(&self) -> u32
[src]
pub fn verbosity(&self) -> i32
[src]
pub fn set_decision_var(&mut self, v: Var, b: bool)
[src]
pub fn num_vars(&self) -> u32
[src]
pub fn print_stats(&self)
[src]
Print some current statistics to standard output.
pub fn new_var(&mut self, upol: lbool, dvar: bool) -> Var
[src]
Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
pub fn new_var_default(&mut self) -> Var
[src]
pub fn add_clause_reuse(&mut self, clause: &mut Vec<Lit>) -> bool
[src]
pub fn simplify(&mut self) -> bool
[src]
Simplify the clause database according to the current top-level assigment. Currently, the only thing done here is the removal of satisfied clauses, but more things can be put here.
pub fn solve_limited(&mut self, assumps: &[Lit]) -> lbool
[src]
Search for a model that respects a given set of assumptions (With resource constraints).
Trait Implementations
impl Debug for Solver
[src]
fn fmt(&self, __arg_0: &mut Formatter) -> Result
[src]
Formats the value using the given formatter. Read more