splr 0.1.4

A pure rustic CDCL SAT solver based on Glucose
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
123
124
125
126
127
128
129
130
131

// DIMACS Model Checker in Rust
#![allow(unused_imports)]
use splr::config::Config;
use splr::solver::Solver;
use splr::traits::{SatSolverIF, ValidatorIF};
use std::env;
use std::fs::File;
use std::io::{stdin, BufRead, BufReader, Result};
use std::path::{Path, PathBuf};
use structopt::StructOpt;

#[derive(StructOpt)]
#[structopt(name = "dmcr", about = "DIMACS-format Model Checker in Rust")]
struct TargetOpts {
    #[structopt(parse(from_os_str))]
    #[structopt(short = "a", long = "assign")]
    assign: Option<std::path::PathBuf>,
    #[structopt(parse(from_os_str))]
    problem: std::path::PathBuf,
}

fn main() {
    let mut from_file = true;
    let mut found = false;
    let mut args = TargetOpts::from_args();
    let cnf = args.problem.to_str().unwrap();
    if !args.problem.exists() {
        println!("{} does not exist.", args.problem.to_str().unwrap(),);
        return;
    }
    let mut config = Config::default();
    config.cnf_filename = args.problem.clone();
    let mut s = Solver::build(&config).expect("failed to load");
    if args.assign == None {
        args.assign = Some(PathBuf::from(format!(
            ".ans_{}",
            Path::new(&args.problem)
                .file_name()
                .unwrap()
                .to_string_lossy()
        )));
    }
    if let Some(f) = &args.assign {
        if let Ok(d) = File::open(f.as_path()) {
            if let Some(vec) = read_assignment(&mut BufReader::new(d), cnf, &args.assign) {
                if s.inject_assigmnent(&vec).is_err() {
                    println!(
                        "{} seems an unsat problem but no proof.",
                        args.problem.to_str().unwrap()
                    );
                    return;
                }
            } else {
                return;
            }
            found = true;
        }
    }
    if !found {
        if let Some(vec) = read_assignment(&mut BufReader::new(stdin()), cnf, &args.assign) {
            if s.inject_assigmnent(&vec).is_err() {
                println!(
                    "{} seems an unsat problem but no proof.",
                    args.problem.to_str().unwrap(),
                );
                return;
            }
            found = true;
            from_file = false;
        } else {
            return;
        }
    }
    if !found {
        println!("There's no assign file.");
        return;
    }
    match s.validate() {
        Some(v) => println!(
            "Invalid assignment set for {} due to {:?}.",
            args.problem.to_str().unwrap(),
            v
        ),
        None if from_file => println!(
            "Valid assignment set for {} found in {}.",
            &args.problem.to_str().unwrap(),
            &args.assign.unwrap().to_str().unwrap(),
        ),
        None => println!(
            "Valid assignment set for {}.",
            &args.problem.to_str().unwrap()
        ),
    }
}

fn read_assignment(rs: &mut dyn BufRead, cnf: &str, assign: &Option<PathBuf>) -> Option<Vec<i32>> {
    let mut buf = String::new();
    loop {
        match rs.read_line(&mut buf) {
            Ok(0) => return Some(Vec::new()),
            Ok(_) => {
                if buf.starts_with('c') {
                    buf.clear();
                    continue;
                }
                if buf.starts_with('s') {
                    if buf.starts_with("s SATISFIABLE") {
                        buf.clear();
                        continue;
                    } else if buf.starts_with("s UNSATISFIABLE") {
                        println!("{} seems an unsatisfiable problem. I can't handle it.", cnf);
                        return None;
                    } else if let Some(asg) = assign {
                        println!("{} seems an illegal format file.", asg.to_str().unwrap(),);
                        return None;
                    }
                }
                let mut v: Vec<i32> = Vec::new();
                for s in buf.split_whitespace() {
                    match s.parse::<i32>() {
                        Ok(0) => break,
                        Ok(x) => v.push(x),
                        Err(e) => panic!("{} by {}", e, s),
                    }
                }
                return Some(v);
            }
            Err(e) => panic!("{}", e),
        }
    }
}