[−][src]Trait ipasir::IpasirSolver

pub trait IpasirSolver {
    fn signature(&self) -> &'static str;

    fn init() -> Self;

    fn add_clause<I, L>(&mut self, lits: I)
    where
        I: IntoIterator<Item = L>,
        L: Into<Lit>;

    fn assume(&mut self, lit: Lit);

    fn solve(&mut self) -> Result<SolveResponse>;

    fn val(&mut self, lit: Lit) -> Result<LitValue>;

    fn failed(&mut self, lit: Lit) -> Result<bool>;

    fn set_terminate<F>(&mut self, callback: F)
    where
        F: FnMut() -> SolveControl + 'static;

    fn set_learn<F>(&mut self, max_len: usize, callback: F)
    where
        F: FnMut(Clause) + 'static;
}

The IPASIR interface a SAT solver has to implement to be conforming.

Required methods

fn signature(&self) -> &'static str

Returns name and version of the incremental SAT solving implementation.

fn init() -> Self

Return a new incremental SAT solver.

States

  • Required: N/A
  • After: INPUT

fn add_clause<I, L>(&mut self, lits: I) where
    I: IntoIterator<Item = L>,
    L: Into<Lit>, 

Adds a clause to the solver.

The clause is defined to contain all yielded literals of the given iterator.

Note

  • Clauses added this way cannot be removed.
  • The addition of removable clauses can be simulated using activation literals and assumptions.

States

  • Required: any
  • After: INPUT

fn assume(&mut self, lit: Lit)

Adds the given literal as new assumption.

States

  • Required: any
  • After: INPUT

fn solve(&mut self) -> Result<SolveResponse>

Starts the solving process.

States

  • Required: any
  • After: any

fn val(&mut self, lit: Lit) -> Result<LitValue>

Queries the assignment of the given literal.

States

  • Required: SAT
  • After: SAT

fn failed(&mut self, lit: Lit) -> Result<bool>

Queries if the given literal was used to prove unsatisfiability.

States

  • Required: UNSAT
  • After: UNSAT

fn set_terminate<F>(&mut self, callback: F) where
    F: FnMut() -> SolveControl + 'static, 

Set a callback handler used to indicate a terminate requirement to the solver.

Note

The solver will periodically query this handler and check its return value during solving.

States

  • Required: any
  • After: same

fn set_learn<F>(&mut self, max_len: usize, callback: F) where
    F: FnMut(Clause) + 'static, 

Set a callback function used to extract learned clauses up to a given length from the solver.

Note

  • The solver will call this function for each learned clause that is not longer than the maximum length.
  • The solver calls the callback function with the parameter state that was passed into set_learn.

States

  • Required: any
  • After: same
Loading content...

Implementors

impl IpasirSolver for Solver[src]

Loading content...