veripb_parser/
substitution_parser.rs

1//! Parsing functions for VeriPB substitutions.
2//!
3//! A substitution in VeriPB format is a list of pairs of variables and literals or truth values. For instance:
4//! ```ignore
5//! x1 1 x12 0 variable x1 another ~x1
6//! ```
7//! maps `x1` to true, `x12` to false, `variable` to `x1`, and `another` to not `x1`.
8//!
9//! Optionally, it is possible to add the arrow `->` inside a pair, so that our example becomes:
10//! ```ignore
11//! x1 -> 1 x12 -> 0 variable -> x1 another -> ~x1
12//! ```
13//!
14//! Tokenization is performed by using [`SubstitutionToken`].
15
16use std::io::{Error, ErrorKind};
17
18use logos::Lexer;
19use veripb_formula::prelude::*;
20
21use crate::substitution_token::SubstitutionToken;
22
23/// Parse a substitution in VeriPB format into the [`Substitution`] data structure.
24///
25/// The substitution is parsed from a lexer that generates tokens of the substitution. A format of a substitution is a list of mappings. A the domain of the mapping are variables and the range of the mapping is `0`, `1`, or a literal.
26pub fn parse_substitution(
27    lex: &mut Lexer<SubstitutionToken>,
28    var_names: &mut VarNameManager,
29) -> Result<Substitution, Error> {
30    let mut sub = Substitution::default();
31    while let Some(token) = lex.next() {
32        // Parse the domain variable of the substitution map.
33        let var = match token {
34            Ok(SubstitutionToken::PositiveLit) => var_names.add_by_name(lex.slice()),
35            Ok(SubstitutionToken::Semicolon) => break,
36            Ok(_) => return Err(Error::new(ErrorKind::InvalidData, "Expected variable.")),
37            Err(_) => return Err(Error::new(ErrorKind::InvalidData, "Unrecognized token.")),
38        };
39
40        // Parse the image of the parsed variable.
41        if let Some(token) = lex.next() {
42            let already_set = match token {
43                Ok(SubstitutionToken::Zero) => sub.set(var, SubstitutionValue::FALSE),
44                Ok(SubstitutionToken::One) => sub.set(var, SubstitutionValue::TRUE),
45                Ok(SubstitutionToken::PositiveLit) => sub.set(
46                    var,
47                    SubstitutionValue::lit(Lit::from_var(
48                        var_names.add_by_name(lex.slice()),
49                        false,
50                    )),
51                ),
52                Ok(SubstitutionToken::NegativeLit) => sub.set(
53                    var,
54                    SubstitutionValue::lit(Lit::from_var(
55                        var_names.add_by_name(&lex.slice()[1..]),
56                        true,
57                    )),
58                ),
59                Ok(_) => {
60                    return Err(Error::new(
61                        ErrorKind::InvalidData,
62                        "Expected '0', '1', or literal.",
63                    ))
64                }
65                Err(_) => return Err(Error::new(ErrorKind::InvalidData, "Unrecognized token.")),
66            };
67            if already_set {
68                return Err(Error::new(
69                    ErrorKind::InvalidData,
70                    "A variable is assigned twice in the substitution.",
71                ));
72            }
73        } else {
74            return Err(Error::new(
75                ErrorKind::InvalidData,
76                "Substitution ended unexpectedly after variable.",
77            ));
78        }
79    }
80
81    Ok(sub)
82}
veripb_parser/substitution_parser.rs

veripb_parser/
substitution_parser.rs
