mcnf2opb/
mcnf2opb.rs

1//! # `mcnf2opb`
2//!
3//! A small tool for converting DIMACS MCNF files to OPB.
4
5use anyhow::Context;
6use clap::Parser;
7use rustsat::instances::{fio::opb::Options as OpbOptions, MultiOptInstance};
8use std::{io, path::PathBuf};
9
10#[derive(Parser)]
11#[command(author, version, about, long_about = None)]
12struct Args {
13    /// The DIMACS MCNF input file. Reads from `stdin` if not given.
14    in_path: Option<PathBuf>,
15    /// The OPB output path. Writes to `stdout` if not given.
16    out_path: Option<PathBuf>,
17    /// The index in the OPB file to treat as the lowest variable
18    #[arg(long, default_value_t = 1)]
19    first_var_idx: u32,
20    /// Avoid negated literals in the OPB file by transforming constraints
21    #[arg(long)]
22    avoid_negated_lits: bool,
23}
24
25fn main() -> anyhow::Result<()> {
26    let args = Args::parse();
27    let opb_opts = OpbOptions {
28        first_var_idx: args.first_var_idx,
29        no_negated_lits: args.avoid_negated_lits,
30    };
31
32    let inst: MultiOptInstance = if let Some(in_path) = args.in_path {
33        MultiOptInstance::from_dimacs_path(in_path).context("error parsing the input file")?
34    } else {
35        MultiOptInstance::from_dimacs(&mut io::BufReader::new(io::stdin()))
36            .context("error parsing input")?
37    };
38
39    let (mut constr, mut objs) = inst.decompose();
40    for obj in &mut objs {
41        let hardened = obj.convert_to_soft_lits(constr.var_manager_mut());
42        constr.extend(hardened.into());
43    }
44    let inst = MultiOptInstance::compose(constr, objs);
45
46    if let Some(out_path) = args.out_path {
47        inst.write_opb_path(out_path, opb_opts)
48            .context("error writing the output file")?;
49    } else {
50        inst.write_opb(&mut io::stdout(), opb_opts)
51            .context("error writing the output file")?;
52    }
53    Ok(())
54}
mcnf2opb/mcnf2opb.rs

mcnf2opb/
mcnf2opb.rs
