Trait batsat::interface::SolverInterface
source · pub trait SolverInterface {
Show 18 methods
fn num_vars(&self) -> u32;
fn num_clauses(&self) -> u32;
fn num_conflicts(&self) -> u32;
fn is_ok(&self) -> bool;
fn print_stats(&self);
fn new_var(&mut self, upol: lbool, dvar: bool) -> Var;
fn new_var_default(&mut self) -> Var;
fn add_clause_reuse(&mut self, clause: &mut Vec<Lit>) -> bool;
fn simplify(&mut self) -> bool;
fn solve_limited(&mut self, assumps: &[Lit]) -> lbool;
fn proved_at_lvl_0(&self) -> &[Lit];
fn get_model(&self) -> &[lbool];
fn value_var(&self, _: Var) -> lbool;
fn value_lit(&self, _: Lit) -> lbool;
fn value_lvl_0(&self, _: Lit) -> lbool;
fn unsat_core(&self) -> &[Lit];
fn unsat_core_contains_lit(&self, lit: Lit) -> bool;
fn unsat_core_contains_var(&self, v: Var) -> bool;
}Expand description
Main interface for a solver: it makes it possible to add clauses, allocate variables, and check for satisfiability
Required Methods
fn num_vars(&self) -> u32
fn num_clauses(&self) -> u32
fn num_conflicts(&self) -> u32
fn is_ok(&self) -> bool
sourcefn print_stats(&self)
fn print_stats(&self)
Print some current statistics to standard output.
sourcefn new_var(&mut self, upol: lbool, dvar: bool) -> Var
fn new_var(&mut self, upol: lbool, dvar: bool) -> Var
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).
sourcefn new_var_default(&mut self) -> Var
fn new_var_default(&mut self) -> Var
Create a new variable with the default polarity
sourcefn add_clause_reuse(&mut self, clause: &mut Vec<Lit>) -> bool
fn add_clause_reuse(&mut self, clause: &mut Vec<Lit>) -> bool
Add a clause to the solver. Returns false if the solver is in
an UNSAT state.
sourcefn simplify(&mut self) -> bool
fn simplify(&mut self) -> bool
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.
sourcefn solve_limited(&mut self, assumps: &[Lit]) -> lbool
fn solve_limited(&mut self, assumps: &[Lit]) -> lbool
Search for a model that respects a given set of assumptions (With resource constraints).
sourcefn proved_at_lvl_0(&self) -> &[Lit]
fn proved_at_lvl_0(&self) -> &[Lit]
Obtain the slice of literals that are proved at level 0.
These literals will keep this value from now on.
sourcefn get_model(&self) -> &[lbool]
fn get_model(&self) -> &[lbool]
Query whole model
Precondition: last result was Sat (ie lbool::TRUE)
sourcefn value_var(&self, _: Var) -> lbool
fn value_var(&self, _: Var) -> lbool
Query model for var
Precondition: last result was Sat (ie lbool::TRUE)
sourcefn value_lvl_0(&self, _: Lit) -> lbool
fn value_lvl_0(&self, _: Lit) -> lbool
Value of this literal if it’s assigned at level 0, or UNDEF otherwise
sourcefn unsat_core(&self) -> &[Lit]
fn unsat_core(&self) -> &[Lit]
Return unsat core (as a subset of assumptions).
Precondition: last result was Unsat
sourcefn unsat_core_contains_lit(&self, lit: Lit) -> bool
fn unsat_core_contains_lit(&self, lit: Lit) -> bool
Does this literal occur in the unsat-core?
Precondition: last result was Unsat
sourcefn unsat_core_contains_var(&self, v: Var) -> bool
fn unsat_core_contains_var(&self, v: Var) -> bool
Does this variable occur in the unsat-core?
Precondition: last result was Unsat