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

use crate::symbolic_async_graph::{FunctionTable, FunctionTableIterator};
use biodivine_lib_bdd::{BddVariable, BddVariableSetBuilder, ValuationsOfClauseIterator};

impl FunctionTable {
    /// Construct a new `FunctionTable`, registering each row of the table as `BddVariable` in
    /// the given `bdd_builder`.
    ///
    /// The `name` is necessary to give some semantic names to the
    /// symbolic variables.
    pub fn new(name: &str, arity: u16, bdd_builder: &mut BddVariableSetBuilder) -> FunctionTable {
        let rows: Vec<BddVariable> = ValuationsOfClauseIterator::new_unconstrained(arity)
            .map(|arg_valuation| {
                let bdd_var_name = format!("{}{}", name, arg_valuation);
                bdd_builder.make_variable(bdd_var_name.as_str())
            })
            .collect();
        FunctionTable { arity, rows }
    }
}

/// Converts a `FunctionTable` into an iterator of `Vec<bool>` (function table row) and
/// `BddVariable` (corresponding symbolic variable).
impl<'a> IntoIterator for &'a FunctionTable {
    type Item = (Vec<bool>, BddVariable);
    type IntoIter = FunctionTableIterator<'a>;

    fn into_iter(self) -> Self::IntoIter {
        FunctionTableIterator::new(self)
    }
}

impl FunctionTableIterator<'_> {
    /// Create a new `FunctionTableIterator` for a given `FunctionTable`.
    pub fn new(table: &FunctionTable) -> FunctionTableIterator {
        FunctionTableIterator {
            table,
            inner_iterator: ValuationsOfClauseIterator::new_unconstrained(table.arity).enumerate(),
        }
    }
}

/// Iterator implementation for the `FunctionTableIterator`.
impl Iterator for FunctionTableIterator<'_> {
    type Item = (Vec<bool>, BddVariable);

    fn next(&mut self) -> Option<Self::Item> {
        if let Some((index, valuation)) = self.inner_iterator.next() {
            Some((valuation.vector(), self.table.rows[index]))
        } else {
            None
        }
    }
}

#[cfg(test)]
mod tests {
    use crate::symbolic_async_graph::FunctionTable;
    use biodivine_lib_bdd::{BddVariable, BddVariableSetBuilder};

    #[test]
    fn test_function_table() {
        let mut builder = BddVariableSetBuilder::new();
        let table = FunctionTable::new("test", 3, &mut builder);
        let bdd = builder.build();
        let bdd_variables = bdd.variables();
        let table_variables: Vec<BddVariable> = table.into_iter().map(|(_, v)| v).collect();
        assert_eq!(bdd_variables, table_variables);
        assert_eq!(8, table_variables.len());
    }
}