logicaffeine-cli 0.10.0

largo — the LOGOS build tool: new/init/build/run/check/verify/publish for logicaffeine projects
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

//! `largo sat` — the certified SAT solver as a CLI verb.
//!
//! A thin wrapper over [`logicaffeine_proof::satcli`], the exact driver
//! behind the competition `logos-sat` binary — same output, same
//! competition exit codes (10 SAT, 20 UNSAT, 1 error).

use std::path::PathBuf;

/// Handle `largo sat <file.cnf> [--proof out.drat] [--stats]`.
///
/// Never returns on completion: the process exits with the competition
/// code so scripts can rely on `10`/`20` exactly as with `logos-sat`.
pub(crate) fn cmd_sat(
    file: PathBuf,
    proof: Option<PathBuf>,
    stats: bool,
) -> Result<(), Box<dyn std::error::Error>> {
    let code = logicaffeine_proof::satcli::run(
        &file,
        proof.as_deref(),
        stats || std::env::var("LOGOS_STATS").is_ok(),
        &mut std::io::stdout(),
        &mut std::io::stderr(),
    );
    std::process::exit(code as i32);
}