veripb_parser/
assignment_parser.rs

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

veripb_parser/
assignment_parser.rs
