Struct sat::solver::dimacs::Dimacs
[−]
[src]
pub struct Dimacs<CmdFactory> {
// some fields omitted
}A SAT solver which invokes an external program using the DIMACS / MiniSAT file format.
Methods
impl<CmdFactory> Dimacs<CmdFactory> where CmdFactory: Fn() -> Command
fn new(cmd_factory: CmdFactory) -> Dimacs<CmdFactory> where CmdFactory: Fn() -> Command
Create an instance of the DIMACS solver.
The argument is a closure which should prepare a std::process::Command
to invoke the solver program. The input and output filenames will be
appended as additional arguments.
let s = Dimacs::new(|| { let mut c = process::Command::new("minisat"); c.stdout(process::Stdio::null()); c });
fn write_instance<W>(&self, writer: &mut W, instance: &Instance) where W: Write
Write an instance in DIMACS format.
You don't need to call this directly as part of the solver workflow. It may be useful for debugging.
fn read_solution<R>(&self, reader: &mut R, num_vars: usize) -> Option<Assignment> where R: BufRead
Read a solution in MiniSAT format.
You don't need to call this directly as part of the solver workflow. It may be useful for debugging.