Struct batsat::core::Solver

pub struct Solver<Cb: Callbacks> { /* fields omitted */ }

The main solver structure.

Each instance is a full-fledged SAT solver, and it can be parametrized further with a theory::TheoryArg and with basic callbacks::Callbacks.

A Solver object contains the whole state of the SAT solver, including a clause allocator, literals, clauses, and statistics.

Implementations

impl<Cb: Callbacks> Solver<Cb>

pub fn new(opts: SolverOpts, cb: Cb) -> Self

Create a new solver with the given options and the callbacks cb.

impl<Cb: Callbacks> Solver<Cb>

pub fn new_with(opts: SolverOpts, cb: Cb) -> Self

Create a new solver with the given options and callbacks.

pub fn cb_mut(&mut self) -> &mut Cb

Temporary access to the callbacks

pub fn cb(&self) -> &Cb

Temporary access to the callbacks

pub fn dimacs_model(&self) -> SolverPrintDimacs<'_, Cb>

pub fn interrupt_async(&self)

Interrupt search asynchronously

Trait Implementations

impl<Cb: Callbacks + Default> Default for Solver<Cb>

pub fn default() -> Self

Returns the "default value" for a type.

impl<Cb: Callbacks> SolverInterface for Solver<Cb>

pub 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).

pub fn new_var_default(&mut self) -> Var

Create a new variable with the default polarity.

pub fn var_of_int(&mut self, v_idx: u32) -> Var

Get the i-th variable, possibly creating it if it doesn't already exist.

pub 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.

pub fn solve_limited_th<Th: Theory>(
    &mut self,
    th: &mut Th,
    assumps: &[Lit]
) -> lbool

Solve using the given theory.

pub fn simplify_th<Th: Theory>(&mut self, th: &mut Th) -> bool

Simplify using the given theory.

pub fn value_var(&self, v: Var) -> lbool

Query model for var.

pub fn value_lit(&self, v: Lit) -> lbool

Query model for lit.

pub fn get_model(&self) -> &[lbool]

Query whole model, as a mapping from Var to lbool.

pub fn is_ok(&self) -> bool

Is the solver in a state that can still be satisfiable?

pub fn num_vars(&self) -> u32

pub fn num_clauses(&self) -> u64

pub fn num_conflicts(&self) -> u64

pub fn num_propagations(&self) -> u64

pub fn num_decisions(&self) -> u64

pub fn num_restarts(&self) -> u64

pub fn value_lvl_0(&self, lit: Lit) -> lbool

Value of this literal if it's assigned at level 0, or UNDEF otherwise

pub fn print_stats(&self)

Print some current statistics to standard output.

pub fn unsat_core(&self) -> &[Lit]

Return unsat core (as a subset of assumptions).

pub fn unsat_core_contains_lit(&self, lit: Lit) -> bool

Does this literal occur in the unsat-core?

pub fn unsat_core_contains_var(&self, v: Var) -> bool

Does this variable occur in the unsat-core?

pub fn proved_at_lvl_0(&self) -> &[Lit]

Obtain the slice of literals that are proved at level 0.

pub 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.

pub fn solve_limited(&mut self, assumps: &[Lit]) -> lbool

Search for a model that respects a given set of assumptions (with resource constraints).