rustsat 0.7.5

This library aims to provide implementations of elements commonly used in the development on software in the area of satisfiability solving. The focus of the library is to provide as much ease of use without giving up on performance.
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

//! # `shuffledimacs`
//!
//! A small tool for shuffling the order of constraints and the variable
//! indexing in a DIMACS file.
//!
//! Usage: `shuffledimacs [dimacs [m,w]cnf file] [output path]`

use std::path::{Path, PathBuf};

use anyhow::Context;
use rustsat::instances::{self, BasicVarManager, RandReindVarManager};

macro_rules! print_usage {
    () => {{
        eprintln!("Usage: shuffledimacs [dimacs [m,w]cnf file] [output path]");
        panic!()
    }};
}

enum FileType {
    Cnf,
    Wcnf,
    Mcnf,
}

fn main() -> anyhow::Result<()> {
    let in_path = PathBuf::from(&std::env::args().nth(1).unwrap_or_else(|| print_usage!()));
    let out_path = PathBuf::from(&std::env::args().nth(2).unwrap_or_else(|| print_usage!()));

    match determine_file_type(&in_path) {
        FileType::Cnf => {
            let inst = instances::SatInstance::<BasicVarManager>::from_dimacs_path(in_path)
                .context("Could not parse CNF")?;
            let n_vars = inst.n_vars();
            let rand_reindexer = RandReindVarManager::init(n_vars);
            inst.reindex(rand_reindexer)
                .shuffle()
                .write_dimacs_path(out_path)
                .context("Could not write CNF")?;
        }
        FileType::Wcnf => {
            let inst = instances::OptInstance::<BasicVarManager>::from_dimacs_path(in_path)
                .context("Could not parse WCNF")?;
            let n_vars = inst.constraints_ref().n_vars();
            let rand_reindexer = RandReindVarManager::init(n_vars);
            inst.reindex(rand_reindexer)
                .shuffle()
                .write_dimacs_path(out_path)
                .context("Could not write WCNF")?;
        }
        FileType::Mcnf => {
            let inst = instances::MultiOptInstance::<BasicVarManager>::from_dimacs_path(in_path)
                .context("Could not parse MCNF")?;
            let n_vars = inst.constraints_ref().n_vars();
            let rand_reindexer = RandReindVarManager::init(n_vars);
            inst.reindex(rand_reindexer)
                .shuffle()
                .write_dimacs_path(out_path)
                .context("Could not write MCNF")?;
        }
    }
    Ok(())
}

macro_rules! is_one_of {
    ($a:expr, $($b:expr),*) => {
        $( $a == $b || )* false
    }
}

fn determine_file_type(in_path: &Path) -> FileType {
    if let Some(ext) = in_path.extension() {
        let path_without_compr = in_path.with_extension("");
        let ext = if is_one_of!(ext, "gz", "bz2") {
            // Strip compression extension
            match path_without_compr.extension() {
                Some(ext) => ext,
                None => return FileType::Cnf, // Fallback default
            }
        } else {
            ext
        };
        if "wcnf" == ext {
            return FileType::Wcnf;
        };
        if "mcnf" == ext {
            return FileType::Mcnf;
        };
        return FileType::Cnf; // Fallback default
    };
    FileType::Cnf // Fallback default
}