1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128

use super::*;
use std::collections::HashMap;
use std::convert::TryInto;

impl BddVariableSetBuilder {
    /// Create a new builder without any variables.
    pub fn new() -> BddVariableSetBuilder {
        BddVariableSetBuilder {
            var_names: Vec::new(),
            var_names_set: HashSet::new(),
        }
    }

    /// Create a new variable with the given `name`. Returns a `BddVariable`
    /// instance that can be later used to create and query actual BDDs.
    ///
    /// *Panics*:
    ///  - Each variable name has to be unique.
    ///  - Currently, there can be at most 65535 variables.
    ///  - The name must not contain `!`, `&`, `|`, `^`, `=`, `<`, `>`, `(` or `)`.
    pub fn make_variable(&mut self, name: &str) -> BddVariable {
        let new_variable_id = self.var_names.len();
        if new_variable_id >= (u16::MAX - 1) as usize {
            panic!(
                "Too many BDD variables. There can be at most {} variables.",
                u16::MAX - 1
            )
        }
        if self.var_names_set.contains(name) {
            panic!("BDD variable {} already exists.", name);
        }
        if name.chars().any(|c| NOT_IN_VAR_NAME.contains(&c)) {
            panic!(
                "Variable name {} is invalid. Cannot use {:?}",
                name, NOT_IN_VAR_NAME
            );
        }
        self.var_names_set.insert(name.to_string());
        self.var_names.push(name.to_string());
        BddVariable(new_variable_id as u16)
    }

    /// A more convenient version of `make_variables` which allows irrefutable pattern matching
    /// on the result, because it is an array instead of a vector.
    pub fn make<const X: usize>(&mut self, names: &[&str; X]) -> [BddVariable; X] {
        self.make_variables(names).try_into().unwrap()
    }

    /// Similar to `make_variable`, but allows creating multiple variables at the same time.
    pub fn make_variables(&mut self, names: &[&str]) -> Vec<BddVariable> {
        names.iter().map(|name| self.make_variable(name)).collect()
    }

    /// Convert this builder to an actual variable set.
    pub fn build(self) -> BddVariableSet {
        let mut mapping: HashMap<String, u16> = HashMap::new();
        for name_index in 0..self.var_names.len() {
            let name = self.var_names[name_index].clone();
            mapping.insert(name, name_index as u16);
        }
        BddVariableSet {
            num_vars: self.var_names.len() as u16,
            var_names: self.var_names,
            var_index_mapping: mapping,
        }
    }
}

impl Default for BddVariableSetBuilder {
    fn default() -> Self {
        Self::new()
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    #[should_panic]
    fn bdd_variables_builder_too_large() {
        let mut builder = BddVariableSetBuilder::new();
        for i in 0..u16::MAX {
            builder.make_variable(&format!("v{}", i));
        }
    }

    #[test]
    #[should_panic]
    fn bdd_variables_builder_duplicate_variable() {
        let mut builder = BddVariableSetBuilder::new();
        builder.make_variable("var1");
        builder.make_variable("var1");
    }

    #[test]
    fn bdd_variables_builder() {
        let mut builder = BddVariableSetBuilder::new();
        let v1 = builder.make_variable("v1");
        let v2 = builder.make_variable("v2");
        let v3 = builder.make_variable("v3");
        let variables = builder.build();
        assert_eq!(3, variables.num_vars());
        assert_eq!(Some(v1), variables.var_by_name("v1"));
        assert_eq!(Some(v2), variables.var_by_name("v2"));
        assert_eq!(Some(v3), variables.var_by_name("v3"));
        assert_eq!(None, variables.var_by_name("v4"));
    }

    #[test]
    fn bdd_variables_builder_batch() {
        let mut builder = BddVariableSetBuilder::new();
        let [v1, v2, v3] = builder.make(&["v1", "v2", "v3"]);
        let variables = builder.build();
        assert_eq!(3, variables.num_vars());
        assert_eq!(Some(v1), variables.var_by_name("v1"));
        assert_eq!(Some(v2), variables.var_by_name("v2"));
        assert_eq!(Some(v3), variables.var_by_name("v3"));
        assert_eq!(None, variables.var_by_name("v4"));
    }

    #[test]
    #[should_panic]
    fn bdd_variables_builder_invalid_name() {
        let mut builder = BddVariableSetBuilder::new();
        builder.make_variable("a^b");
    }
}