veripb_parser/
assignment_parser.rs

1//! Parsing functions for VeriPB assignments.
2//!
3//! A VeriPB assignment is a list of OPB literals. For instance:
4//! ```ignore
5//! x1 ~x13 x42 ~x21 ~variable
6//! ```
7//! sets variables `x1` and `x42` to true and `x13`, `x21`, and `variable` to false.
8//!
9//! Tokenization is preformed using the [`AssignmentToken`].
10
11use std::io::{Error, ErrorKind};
12
13use logos::Lexer;
14use veripb_formula::prelude::*;
15
16use crate::assignment_token::AssignmentToken;
17
18/// Parse an assignment from a lexer to an [`Assignment`] of [`BooleanVar`]. This function returns a new [`Assignment`].
19///
20/// See [`parse_bool_assignment_into()`] for more details.
21pub fn parse_bool_assignment(
22    lex: &mut Lexer<AssignmentToken>,
23    var_names: &mut VarNameManager,
24) -> Result<Assignment<BooleanVar>, Error> {
25    let mut assignment = Assignment::with_size(var_names.len());
26
27    parse_bool_assignment_into(lex, var_names, &mut assignment)?;
28
29    Ok(assignment)
30}
31
32/// Parse an assignment from a lexer into an existing [`Assignment`] of [`BooleanVar`].
33///
34/// The assignment is formatted as a list of literals. A positive literal represents an assignment of the variable to true and a negative literal represents an assignment of the variable to false.
35///
36/// If a variable is already assigned in `assignment`, then it will be overwritten by the parsed assignment.
37pub fn parse_bool_assignment_into(
38    lex: &mut Lexer<AssignmentToken>,
39    var_names: &mut VarNameManager,
40    assignment: &mut Assignment<BooleanVar>,
41) -> Result<(), Error> {
42    assignment.resize(var_names.len());
43
44    while let Some(lit) = lex.next() {
45        match lit {
46            Ok(AssignmentToken::PositiveVar) => {
47                let var = var_names.add_by_name(lex.slice());
48                if var >= assignment.len() {
49                    assignment.resize(var + 1);
50                }
51                assignment.set_value(var, BoolValue::Assigned(true));
52            }
53            Ok(AssignmentToken::NegativeVar) => {
54                let var = var_names.add_by_name(&lex.slice()[1..]);
55                if var >= assignment.len() {
56                    assignment.resize(var + 1);
57                }
58                assignment.set_value(var, BoolValue::Assigned(false));
59            }
60            Err(_) => {
61                return Err(Error::new(
62                    ErrorKind::InvalidData,
63                    format!("The token '{}' is not a literal!", lex.slice()),
64                ));
65            }
66        }
67    }
68
69    Ok(())
70}
71
72/// Parse an assignment from a lexer to a raw [`Vec<Lit>`].
73///
74/// This vector can be used to initialize an assignment or a propagation trail.
75pub fn parse_bool_assignment_to_raw_vec(
76    lex: &mut Lexer<AssignmentToken>,
77    var_names: &mut VarNameManager,
78) -> Result<Vec<Lit>, Error> {
79    let mut assignment = Vec::new();
80
81    while let Some(lit) = lex.next() {
82        match lit {
83            Ok(AssignmentToken::PositiveVar) => {
84                let var = var_names.add_by_name(lex.slice());
85                assignment.push(Lit::from_var(var, false));
86            }
87            Ok(AssignmentToken::NegativeVar) => {
88                let var = var_names.add_by_name(&lex.slice()[1..]);
89                assignment.push(Lit::from_var(var, true));
90            }
91            Err(_) => {
92                return Err(Error::new(
93                    ErrorKind::InvalidData,
94                    format!("The token '{}' is not a literal!", lex.slice()),
95                ));
96            }
97        }
98    }
99
100    Ok(assignment)
101}
veripb_parser/assignment_parser.rs

veripb_parser/
assignment_parser.rs
