-
Notifications
You must be signed in to change notification settings - Fork 7
/
opb2wcnf.rs
54 lines (46 loc) · 1.63 KB
/
opb2wcnf.rs
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
//! # opb2wcnf
//!
//! A small tool for converting OPB files to DIMACS WCNF.
use anyhow::Context;
use clap::Parser;
use rustsat::instances::{fio::opb::Options as OpbOptions, OptInstance};
use std::{io, path::PathBuf};
#[derive(Parser)]
#[command(author, version, about, long_about = None)]
struct Args {
/// The OPB input file. Reads from `stdin` if not given.
in_path: Option<PathBuf>,
/// The DIMACS WCNF output path. Writes to `stdout` if not given.
out_path: Option<PathBuf>,
/// The index in the OPB file to treat as the lowest variable
#[arg(long, default_value_t = 1)]
first_var_idx: usize,
}
fn main() -> anyhow::Result<()> {
let args = Args::parse();
let opb_opts = OpbOptions {
first_var_idx: 0,
..Default::default()
};
let inst: OptInstance = if let Some(in_path) = args.in_path {
OptInstance::from_opb_path(in_path, opb_opts).context("error parsing the input file")?
} else {
OptInstance::from_opb(io::BufReader::new(io::stdin()), opb_opts)
.context("error parsing input")?
};
let (constrs, obj) = inst.decompose();
let mut constrs = constrs.sanitize();
println!("c {} clauses", constrs.n_clauses());
println!("c {} cards", constrs.n_cards());
println!("c {} pbs", constrs.n_pbs());
constrs.convert_to_cnf();
let inst = OptInstance::compose(constrs, obj);
if let Some(out_path) = args.out_path {
inst.write_dimacs_path(out_path)
.context("io error writing the output file")?;
} else {
inst.write_dimacs(&mut io::stdout())
.context("io error writing to stdout")?;
}
Ok(())
}