splr 0.17.2

A modern CDCL SAT solver in Rust
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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122

use std::{
    env,
    fs::{self, File},
    path::Path,
    process::{Command, Stdio},
};

/*
for f in ${UUF250}*.cnf; do
    target=`basename -s .cnf $f`
    rm -f ${target}.out
    splr -c -p ${target}.out ${f} > /dev/null
    if [ -z ${target}.out ]; then
        echo ' FAIL TO CERTIFICATE: ${f}'
        exit 1;
    egrep -v '^[cs]' < ${target}.out > ${target}.drat
    gratgen ${f} ${target}.drat -o ${target}.grat -j 4 > /dev/null
    gratchk unsat ${f} ${target}.grat
*/

fn main() {
    if let Some(uuf250) = env::args().nth(1) {
        let path = Path::new(&uuf250);
        for e in path
            .read_dir()
            .unwrap_or_else(|_| panic!("not exist {:?}", path))
        {
            if let Ok(cnf) = e.map(|e| e.path()) {
                if let Some(target) = cnf.file_name().map(Path::new) {
                    let out = target.with_extension("out");
                    let drat = target.with_extension("drat");
                    let grat = target.with_extension("grat");
                    // println!("########################################");
                    print!("# {}", cnf.file_name().unwrap().to_string_lossy());
                    // rm -f ${target}.out
                    if out.exists() {
                        fs::remove_file(&out).expect("fail to rm");
                    }
                    // splr -c -p ${target}.out ${f} > /dev/null
                    Command::new("splr")
                        .args(&["-c", "-p", &*out.to_string_lossy(), &*cnf.to_string_lossy()])
                        .stdout(Stdio::null())
                        .output()
                        .expect("failed to execute Splr");
                    // if [ -z ${target}.out ]; then
                    //     echo ' FAIL TO CERTIFICATE: ${f}'
                    //     exit 1;
                    // fi
                    if !out.exists() {
                        println!(
                            " FAIL TO CERTIFICATE: {} => {}",
                            cnf.file_name().unwrap().to_string_lossy(),
                            out.to_string_lossy(),
                        );
                        panic!("abort");
                    }
                    // egrep -v '^[cs]' < ${target}.out > ${target}.drat
                    Command::new("egrep")
                        .args(&["-v", "^[cs]"])
                        .stdin(File::open(out).expect(""))
                        .stdout(File::create(&drat).expect(""))
                        .output()
                        .expect("");
                    // gratgen ${f} ${target}.drat -o ${target}.grat -j 4 > /dev/null
                    Command::new("gratgen")
                        .args(&[
                            &*cnf.to_string_lossy(),
                            &*drat.to_string_lossy(),
                            "-o",
                            &*grat.to_string_lossy(),
                            "-j",
                            "4",
                        ])
                        .stdin(Stdio::piped())
                        .stdout(Stdio::null())
                        .stderr(Stdio::null())
                        .output()
                        .unwrap();
                    // .expect(&format!("FAIL TO GENERATE: {} => {}",
                    //                 cnf.file_name().unwrap().to_string_lossy(),
                    //                 grat.to_string_lossy(),
                    // ));
                    // gratchk unsat ${f} ${target}.grat
                    if grat.exists() {
                        print!(" => {}", grat.to_string_lossy());
                    } else {
                        println!(
                            " FAIL TO CONVERT: {} => {}",
                            cnf.file_name().unwrap().to_string_lossy(),
                            grat.to_string_lossy(),
                        );
                        panic!("abort");
                    }
                    let mut pass = false;
                    if let Ok(out) = Command::new("gratchk")
                        .args(&["unsat", &*cnf.to_string_lossy(), &*grat.to_string_lossy()])
                        .stdin(Stdio::piped())
                        .stderr(Stdio::null())
                        .output()
                    {
                        let str = String::from_utf8_lossy(&out.stdout);
                        for l in (*str).split('\n') {
                            if l.contains(&"s VERIFIED UNSAT") {
                                pass = true;
                                println!(" => VERIFIED UNSAT");
                                break;
                            }
                        }
                    }
                    if !pass {
                        println!(
                            " FAIL TO CERTIFICATE: {} => {}",
                            cnf.file_name().unwrap().to_string_lossy(),
                            grat.to_string_lossy(),
                        );
                        panic!("abort");
                    }
                }
            }
        }
    }
}