veripb_parser/wcnf_parser.rs
1//! Parsing functions for WCNF MaxSAT files.
2//!
3//! The format has been specified in the [MaxSAT Evaluation 2022](https://maxsat-evaluations.github.io/2022/rules.html#input).
4
5use logos::Logos;
6use malachite_bigint::BigInt;
7use num_traits::Zero;
8use std::path::Path;
9use veripb_formula::prelude::*;
10
11use crate::{error::ParserError, parser::get_lines, wcnf_token::WCNFToken};
12
13enum Weight {
14 Hard,
15 Soft(BigInt),
16}
17
18/// Parse a formula from a WCNF file. The WCNF format is described in the [MaxSAT Evaluation 2022](https://maxsat-evaluations.github.io/2022/rules.html#input).
19///
20/// This function creates a [`VarNameManager`] and calls the function [`parse_wcnf_from_file_given_var_manager()`]. See [`parse_wcnf_from_file_given_var_manager()`] for more details.
21#[inline]
22pub fn parse_wcnf_from_file<P>(filename: P) -> Result<(Formula, VarNameManager), ParserError>
23where
24 P: AsRef<Path>,
25{
26 let mut var_name_manager = VarNameManager::default();
27 let formula = parse_wcnf_from_file_given_var_manager(filename, &mut var_name_manager)?;
28 Ok((formula, var_name_manager))
29}
30
31/// Parse a formula from a WCNF file. The WCNF format is described in the [MaxSAT Evaluation 2022](https://maxsat-evaluations.github.io/2022/rules.html#input).
32///
33/// For converting MaxSAT problem into a pseudo-Boolean minimization problem, we use the following conventions:
34/// - Hard clauses are constraints.
35/// - For empty soft clauses, increase the objective constant.
36/// - Unit soft clauses are added immediately to the objective with the weight as coefficient and the negated clause literal as the objective literal.
37/// - For any other soft clauses `C`, introduce a relaxation variable `_b<i>`, where `<i>` means that this clause is the ith clause. Then `~_b<i>` is added with the weight as coefficient to the objective and the clause `C or ~_b<i>` is added as a constraint.
38pub fn parse_wcnf_from_file_given_var_manager<P>(
39 filename: P,
40 var_name_manager: &mut VarNameManager,
41) -> Result<Formula, ParserError>
42where
43 P: AsRef<Path>,
44{
45 let mut database = Formula::default();
46 let lines = get_lines(&filename)?;
47 let mut current_lits = Vec::new();
48 let mut weight = None;
49 let mut objective_terms = Vec::new();
50 let mut objective_constant = BigInt::zero();
51 let mut clause_counter: u64 = 0;
52
53 for (line_number, line) in lines.map_while(Result::ok).enumerate() {
54 let mut lex = WCNFToken::lexer(&line);
55
56 while let Some(token) = lex.next() {
57 match token {
58 Ok(WCNFToken::Integer) => {
59 if weight.is_none() {
60 weight = Some(Weight::Soft(lex.slice().parse().unwrap()));
61 } else {
62 let integer: i64 = lex.slice().parse::<i64>().map_err(|_| {
63 ParserError::token_error_with_file(
64 lex.span(),
65 "literal",
66 filename.as_ref().to_string_lossy().to_string(),
67 line_number,
68 )
69 })?;
70 match integer {
71 0 => {
72 clause_counter += 1;
73 match std::mem::take(&mut weight) {
74 None => {
75 return Err(ParserError::token_error_with_file(
76 lex.span(),
77 "weight",
78 filename.as_ref().to_string_lossy().to_string(),
79 line_number,
80 ))
81 }
82 Some(Weight::Hard) => {
83 let clause =
84 Clause::from_unnormalized_lits(current_lits.clone())
85 .into();
86 database.constraints.push(clause);
87 }
88 Some(Weight::Soft(coeff)) => {
89 match current_lits.len() {
90 0 => {
91 objective_constant += coeff;
92 }
93 1 => {
94 // Unit soft clauses are added directly to the objective.
95 let mut unit_lit = current_lits.pop().unwrap();
96 unit_lit.negate();
97 objective_terms
98 .push(GeneralPBTerm::new(coeff, unit_lit));
99 }
100 _ => {
101 let blocking_lit = Lit::from_var(
102 var_name_manager.add_by_name(
103 &(String::from("_b")
104 + (clause_counter)
105 .to_string()
106 .as_str()),
107 ),
108 true,
109 );
110 current_lits.push(blocking_lit);
111 let clause = Clause::from_unnormalized_lits(
112 current_lits.clone(),
113 )
114 .into();
115 database.constraints.push(clause);
116 objective_terms
117 .push(GeneralPBTerm::new(coeff, blocking_lit));
118 }
119 }
120 }
121 }
122 current_lits.clear();
123 }
124 ..0 => {
125 current_lits.push(Lit::from_var(
126 var_name_manager
127 .add_by_name(&(String::from("x") + &lex.slice()[1..])),
128 true,
129 ));
130 }
131 1.. => {
132 current_lits.push(Lit::from_var(
133 var_name_manager
134 .add_by_name(&(String::from("x") + lex.slice())),
135 false,
136 ));
137 }
138 }
139 }
140 }
141 Ok(WCNFToken::HardClause) => {
142 if weight.is_some() {
143 return Err(ParserError::token_error_with_file(
144 lex.span(),
145 "previous clause has to end before next weight",
146 filename.as_ref().to_string_lossy().to_string(),
147 line_number,
148 ));
149 }
150 weight = Some(Weight::Hard);
151 }
152 Ok(WCNFToken::Comment) => {}
153 _ => {
154 return Err(ParserError::token_error_with_file(
155 lex.span(),
156 "integer or comment",
157 filename.as_ref().to_string_lossy().to_string(),
158 line_number,
159 ));
160 }
161 }
162 }
163 }
164
165 database.objective = Some(PBObjective::from_terms(
166 objective_terms,
167 objective_constant,
168 false,
169 ));
170
171 Ok(database)
172}