21958406699

Committed 12 Feb 2026 05:00PM UTC coverage: 61.964% (+1.1%) from 60.815%

Build # 21958406699

Build Type

push

github

Committed by

chrjabs

Commit Message

refactor: migrate `rustsat-tools` parsers to `winnow`

closes #564

Run Details

241 of 301 new or added lines in 6 files covered. (80.07%)

1102 existing lines in 16 files now uncovered.

14178 of 22881 relevant lines covered (61.96%)

140791.04 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

0.0

/tools/src/bin/check-solution.rs

//! # `check-solution`
//!
//! A small tool for checking solutions to SAT and optimization instances.

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

use clap::{Parser, ValueEnum};
use rustsat::{
    instances::{
        fio::{self, opb::Options as OpbOptions},
        MultiOptInstance, OptInstance, SatInstance,
    },
    types::Assignment,
};

#[derive(Copy, Clone, PartialEq, Eq, ValueEnum)]
pub enum FileFormat {
    /// Infer the file format from the file extension according to the following rules:
    /// - `.cnf`: DIMACS CNF file
    /// - `.wcnf`: Weighted DIMACS CNF (MaxSAT) file
    /// - `.mcnf`: Multi-objective MaxSAT file
    /// - `.opb`: OPB file (without an objective)
    /// - `.mopb` / `.pbmo`: Multi-objective OPB file
    ///
    /// All file extensions can also be appended with `.bz2`, `.xz`, or `.gz` if compression is used.
    Infer,
    /// A DIMACS CNF file
    Cnf,
    /// A DIMACS WCNF file
    Wcnf,
    /// A DIMACS MCNF file
    Mcnf,
    /// An OPB file with zero or more objectives
    Opb,
}

#[derive(Parser)]
#[command(author, version, about, long_about = None)]
struct Args {
    /// The instance to check the solution against
    instance: PathBuf,
    /// The solution specified as one or multiple v-lines. If not specified, will be read from
    /// `stdin`.
    solution: Option<PathBuf>,
    /// The file format of the instance. With infer, the file format is
    /// inferred from the file extension.
    #[arg(long, value_enum, default_value_t = FileFormat::Infer)]
    file_format: FileFormat,
    /// The index in the OPB file to treat as the lowest variable
    #[arg(long, default_value_t = 1)]
    opb_first_var_idx: u32,
}

fn main() -> anyhow::Result<()> {
    let args = Args::parse();
    let opb_opts = OpbOptions {
        first_var_idx: args.opb_first_var_idx,
        ..OpbOptions::default()
    };
    let (constrs, objs) = parse_instance(args.instance, args.file_format, opb_opts)?.decompose();

    let mut reader = if let Some(solution) = args.solution {
        fio::open_compressed_uncompressed_read(solution)?
    } else {
        Box::new(io::BufReader::new(io::stdin()))
    };

    let mut sol = Assignment::default();
    loop {
        let mut buf = String::new();
        let read = reader.read_line(&mut buf)?;
        if read == 0 {
            break;
        }
        if buf.starts_with('v') {
            sol.extend_from_vline(&buf)?;
        }
    }

    if let Some(constr) = constrs.unsat_constraint(&sol) {
        println!("unsatisfied constraint: {constr}");
        std::process::exit(1);
    }
    print!("objective values: ");
    for i in 0..objs.len() {
        if i < objs.len() - 1 {
            print!("{}, ", objs[i].evaluate(&sol))
        } else {
            print!("{}", objs[i].evaluate(&sol));
        }
    }
    println!();
    Ok(())
}

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

fn parse_instance(
    inst_path: PathBuf,
    file_format: FileFormat,
    opb_opts: fio::opb::Options,
) -> anyhow::Result<MultiOptInstance> {
    Ok(match file_format {
        FileFormat::Infer => {
            if let Some(ext) = inst_path.extension() {
                let path_without_compr = inst_path.with_extension("");
                let ext = if is_one_of!(ext, "gz", "bz2", "xz") {
                    // Strip compression extension
                    match path_without_compr.extension() {
                        Some(ext) => ext,
                        None => anyhow::bail!("no file extension after compression extension"),
                    }
                } else {
                    ext
                };
                if is_one_of!(ext, "cnf", "dimacs") {
                    let inst = SatInstance::from_dimacs_path(inst_path)?;
                    MultiOptInstance::compose(inst, vec![])
                } else if is_one_of!(ext, "wcnf") {
                    let (inst, obj) = OptInstance::from_dimacs_path(inst_path)?.decompose();
                    MultiOptInstance::compose(inst, vec![obj])
                } else if is_one_of!(ext, "mcnf") {
                    MultiOptInstance::from_dimacs_path(inst_path)?
                } else if is_one_of!(ext, "opb", "mopb", "pbmo") {
                    MultiOptInstance::from_opb_path(inst_path, opb_opts)?
                } else {
                    anyhow::bail!("unknown file extension")
                }
            } else {
                anyhow::bail!("no file extension")
            }
        }
        FileFormat::Cnf => {
            let inst = SatInstance::from_dimacs_path(inst_path)?;
            MultiOptInstance::compose(inst, vec![])
        }
        FileFormat::Wcnf => {
            let (inst, obj) = OptInstance::from_dimacs_path(inst_path)?.decompose();
            MultiOptInstance::compose(inst, vec![obj])
        }
        FileFormat::Mcnf => MultiOptInstance::from_dimacs_path(inst_path)?,
        FileFormat::Opb => MultiOptInstance::from_opb_path(inst_path, opb_opts)?,
    })
}

1	//! # `check-solution`
2	//!
3	//! A small tool for checking solutions to SAT and optimization instances.
4
5	use std::{io, path::PathBuf};
6
7	use clap::{Parser, ValueEnum};
8	use rustsat::{
9	instances::{
10	fio::{self, opb::Options as OpbOptions},
11	MultiOptInstance, OptInstance, SatInstance,
12	},
13	types::Assignment,
14	};
15
16	#[derive(Copy, Clone, PartialEq, Eq, ValueEnum)]
17	pub enum FileFormat {
18	/// Infer the file format from the file extension according to the following rules:
19	/// - `.cnf`: DIMACS CNF file
20	/// - `.wcnf`: Weighted DIMACS CNF (MaxSAT) file
21	/// - `.mcnf`: Multi-objective MaxSAT file
22	/// - `.opb`: OPB file (without an objective)
23	/// - `.mopb` / `.pbmo`: Multi-objective OPB file
24	///
25	/// All file extensions can also be appended with `.bz2`, `.xz`, or `.gz` if compression is used.
26	Infer,
27	/// A DIMACS CNF file
28	Cnf,
29	/// A DIMACS WCNF file
30	Wcnf,
31	/// A DIMACS MCNF file
32	Mcnf,
33	/// An OPB file with zero or more objectives
34	Opb,
35	}
36
37	#[derive(Parser)]
38	#[command(author, version, about, long_about = None)]
39	struct Args {
40	/// The instance to check the solution against
41	instance: PathBuf,
42	/// The solution specified as one or multiple v-lines. If not specified, will be read from
43	/// `stdin`.
44	solution: Option<PathBuf>,
45	/// The file format of the instance. With infer, the file format is
46	/// inferred from the file extension.
47	#[arg(long, value_enum, default_value_t = FileFormat::Infer)]
48	file_format: FileFormat,
49	/// The index in the OPB file to treat as the lowest variable
50	#[arg(long, default_value_t = 1)]
51	opb_first_var_idx: u32,
52	}
53
54	fn main() -> anyhow::Result<()> {	×
55	let args = Args::parse();	×
56	let opb_opts = OpbOptions {	×
57	first_var_idx: args.opb_first_var_idx,	×
58	..OpbOptions::default()	×
59	};	×
60	let (constrs, objs) = parse_instance(args.instance, args.file_format, opb_opts)?.decompose();	×
61
62	let mut reader = if let Some(solution) = args.solution {	×
63	fio::open_compressed_uncompressed_read(solution)?	×
64	} else {
65	Box::new(io::BufReader::new(io::stdin()))	×
66	};
67
68	let mut sol = Assignment::default();	×
69	loop {
70	let mut buf = String::new();	×
71	let read = reader.read_line(&mut buf)?;	×
72	if read == 0 {	×
73	break;	×
74	}	×
75	if buf.starts_with('v') {	×
76	sol.extend_from_vline(&buf)?;	×
77	}	×
78	}
79
80	if let Some(constr) = constrs.unsat_constraint(&sol) {	×
81	println!("unsatisfied constraint: {constr}");	×
82	std::process::exit(1);	×
83	}	×
84	print!("objective values: ");	×
85	for i in 0..objs.len() {	×
86	if i < objs.len() - 1 {	×
87	print!("{}, ", objs[i].evaluate(&sol))	×
88	} else {	×
89	print!("{}", objs[i].evaluate(&sol));	×
90	}	×
91	}
92	println!();	×
93	Ok(())	×
94	}	×
95
96	macro_rules! is_one_of {
97	($a:expr, $($b:expr),*) => {
98	$( $a == $b \|\| )* false
99	}
100	}
101
102	fn parse_instance(	×
103	inst_path: PathBuf,	×
104	file_format: FileFormat,	×
105	opb_opts: fio::opb::Options,	×
106	) -> anyhow::Result<MultiOptInstance> {	×
107	Ok(match file_format {	×
108	FileFormat::Infer => {
109	if let Some(ext) = inst_path.extension() {	×
110	let path_without_compr = inst_path.with_extension("");	×
111	let ext = if is_one_of!(ext, "gz", "bz2", "xz") {	×
112	// Strip compression extension
113	match path_without_compr.extension() {	×
114	Some(ext) => ext,	×
115	None => anyhow::bail!("no file extension after compression extension"),	×
116	}
117	} else {
118	ext	×
119	};
120	if is_one_of!(ext, "cnf", "dimacs") {	×
121	let inst = SatInstance::from_dimacs_path(inst_path)?;	×
122	MultiOptInstance::compose(inst, vec![])	×
123	} else if is_one_of!(ext, "wcnf") {	×
124	let (inst, obj) = OptInstance::from_dimacs_path(inst_path)?.decompose();	×
125	MultiOptInstance::compose(inst, vec![obj])	×
126	} else if is_one_of!(ext, "mcnf") {	×
127	MultiOptInstance::from_dimacs_path(inst_path)?	×
128	} else if is_one_of!(ext, "opb", "mopb", "pbmo") {	×
129	MultiOptInstance::from_opb_path(inst_path, opb_opts)?	×
130	} else {
131	anyhow::bail!("unknown file extension")	×
132	}
133	} else {
UNCOV 134	anyhow::bail!("no file extension")	×
135	}
136	}
137	FileFormat::Cnf => {
UNCOV 138	let inst = SatInstance::from_dimacs_path(inst_path)?;	×
139	MultiOptInstance::compose(inst, vec![])	×
140	}
141	FileFormat::Wcnf => {
UNCOV 142	let (inst, obj) = OptInstance::from_dimacs_path(inst_path)?.decompose();	×
143	MultiOptInstance::compose(inst, vec![obj])	×
144	}
UNCOV 145	FileFormat::Mcnf => MultiOptInstance::from_dimacs_path(inst_path)?,	×
146	FileFormat::Opb => MultiOptInstance::from_opb_path(inst_path, opb_opts)?,	×
147	})
UNCOV 148	}	×

chrjabs / rustsat / 21958406699

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous