Struct Solver

pub struct Solver { /* private fields */ }

A solver called via an external executable

This solver will perform a call to the solver executable via Command and parse the solver output via fio::parse_sat_solver_output

Implementations

impl Solver

pub fn new( cmd: Command, input: InputVia, output: OutputVia, signature: &'static str, ) -> Self

Initializes a solver with a Command that is fully set up, except for the input instance

Notes

• If input is passed via a file with a path that ends in a compression extension, RustSAT will write a compressed file
• If the solver output is processed via a file, compression is not supported
• If Command::env_clear was called on the command and the input is passed via a file as the first argument, the fact that the environment has been cleared might be forgotten

Example

use std::process::Command;
use rustsat::solvers::{ExternalSolver, external};
let solver = ExternalSolver::new(
    Command::new("<path to solver binary>"),
    external::InputVia::tempfile_last(),
    external::OutputVia::pipe(),
    "solver-signature",
);

After this initialization, the solver instance can be used with the Solve trait.

pub fn new_default(cmd: Command, signature: &'static str) -> Self

Initializes a solver with default values for InputVia and OutputVia

The default values are passing the input via a temporary file and processing the output via a pipe.

Example

use std::process::Command;
use rustsat::solvers::{ExternalSolver, external};
let solver = ExternalSolver::new_default(
    Command::new("<path to solver binary>"),
    "solver-signature",
);

After this initialization, the solver instance can be used with the Solve trait.

Trait Implementations

impl Debug for Solver

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'a> Extend<&'a Clause> for Solver

fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl Extend<Clause> for Solver

fn extend<T: IntoIterator<Item = Clause>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl Solve for Solver

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

Gets a signature of the solver implementation

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

Solves the internal CNF formula without any assumptions.

fn lit_val(&self, lit: Lit) -> Result<TernaryVal>

Gets an assignment of a variable in the solver.

fn add_clause_ref<C>(&mut self, clause: &C) -> Result<()>

where C: AsRef<Cl> + ?Sized,

Adds a clause to the solver by reference. If the solver is in the satisfied or unsatisfied state before, it is in the input state afterwards.

fn solution(&self, high_var: Var) -> Result<Assignment>

Gets a solution found by the solver up to a specified highest variable.

fn add_clause(&mut self, clause: Clause) -> Result<()>

Adds a clause to the solver. If the solver is in the satisfied or unsatisfied state before, it is in the input state afterwards.

fn reserve(&mut self, _max_var: Var) -> Result<()>

Reserves memory in the solver until a maximum variables, if the solver supports it

fn var_val(&self, var: Var) -> Result<TernaryVal>

Same as Solve::lit_val, but for variables.

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

Like Solve::add_clause but for unit clauses (clauses with one literal).

fn add_binary(&mut self, lit1: Lit, lit2: Lit) -> Result<()>

Like Solve::add_clause but for clauses with two literals.

fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) -> Result<()>

Like Solve::add_clause but for clauses with three literals.

fn add_cnf(&mut self, cnf: Cnf) -> Result<()>

Adds all clauses from a Cnf instance.

fn add_cnf_ref(&mut self, cnf: &Cnf) -> Result<()>

Adds all clauses from a Cnf instance by reference.