Struct varisat::solver::Solver

pub struct Solver<'a> {
    ctx: Box<Context<'a>>,
}

A boolean satisfiability solver.

Fields

ctx: Box<Context<'a>>

Methods

impl<'a> Solver<'a>

pub fn new() -> Solver<'a>

Create a new solver.

pub fn config(
    &mut self,
    config_update: &SolverConfigUpdate
) -> Result<(), Error>

Change the solver configuration.

pub fn add_formula(&mut self, formula: &CnfFormula)

Add a formula to the solver.

pub fn add_dimacs_cnf(&mut self, input: impl Read) -> Result<(), Error>

Reads and adds a formula in DIMACS CNF format.

Using this avoids creating a temporary CnfFormula.

pub fn witness_var(&mut self, var: Var)

Sets the "witness" sampling mode for a variable.

pub fn sample_var(&mut self, var: Var)

Sets the "sample" sampling mode for a variable.

pub fn hide_var(&mut self, var: Var)

Hide a variable.

Turns a free variable into an existentially quantified variable. If the passed Var is used again after this call, it refers to a new variable not the previously hidden variable.

pub fn observe_internal_vars(&mut self) -> Vec<Var>

Observe solver internal variables.

This turns solver internal variables into witness variables. There is no guarantee that the newly visible variables correspond to previously hidden variables.

Returns a list of newly visible variables.

pub fn solve(&mut self) -> Result<bool, SolverError>

Check the satisfiability of the current formula.

fn check_for_solver_error(&mut self) -> Result<(), SolverError>

Check for asynchronously generated errors.

To avoid threading errors out of deep call stacks, we have a solver_error field in the SolverState. This function takes and returns that error if present.

pub fn assume(&mut self, assumptions: &[Lit])

Assume given literals for future calls to solve.

This replaces the current set of assumed literals.

pub fn model(&self) -> Option<Vec<Lit>>

Set of literals that satisfy the formula.

pub fn failed_core(&self) -> Option<&[Lit]>

Subset of the assumptions that made the formula unsatisfiable.

This is not guaranteed to be minimal and may just return all assumptions every time.

pub fn write_proof(&mut self, target: impl Write + 'a, format: ProofFormat)

Generate a proof of unsatisfiability during solving.

This needs to be called before any clauses are added.

pub fn close_proof(&mut self) -> Result<(), SolverError>

Stop generating a proof of unsatisfiability.

This also flushes internal buffers and closes the target file.

pub fn enable_self_checking(&mut self)

Generate and check a proof on the fly.

This needs to be called before any clauses are added.

pub fn add_proof_processor(&mut self, processor: &'a mut dyn ProofProcessor)

Generate a proof and process it using a ProofProcessor.

This implicitly enables self checking.

This needs to be called before any clauses are added.

Trait Implementations

impl<'a> Drop for Solver<'a>

fn drop(&mut self)

Executes the destructor for this type.

impl<'a> Default for Solver<'a>

fn default() -> Solver<'a>

Returns the "default value" for a type.

impl<'a> ExtendFormula for Solver<'a>

fn add_clause(&mut self, clause: &[Lit])

Add a clause to the solver.

fn new_var(&mut self) -> Var

Add a new variable to the solver.

fn new_lit(&mut self) -> Lit

Add a new variable to the formula and return it as positive literal.

Important traits for NewVarIter<'a, F, V>

impl<'a, F, V> Iterator for NewVarIter<'a, F, V> where
    F: ExtendFormula,
    V: From<Var>,  type Item = V;

fn new_var_iter(&mut self, count: usize) -> NewVarIter<Self, Var>

Iterator over multiple new variables.

Important traits for NewVarIter<'a, F, V>

impl<'a, F, V> Iterator for NewVarIter<'a, F, V> where
    F: ExtendFormula,
    V: From<Var>,  type Item = V;

fn new_lit_iter(&mut self, count: usize) -> NewVarIter<Self, Lit>

Iterator over multiple new literals.

fn new_vars<Vars>(&mut self) -> Vars where
    Vars: UniformTuple<Var>, 

Add multiple new variables and return them.

fn new_lits<Lits>(&mut self) -> Lits where
    Lits: UniformTuple<Lit>, 

Add multiple new variables and return them as positive literals.