From 09316b44d3ffda08b199563e0ab986d8e9d2bf3a Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Wed, 30 Dec 2020 00:08:47 +0100
Subject: [PATCH] Add access to function tables using the symbolic context.

---
 .../_impl_symbolic_context.rs                   | 17 +++++++++++++++++
 src/symbolic_async_graph/mod.rs                 |  9 ++++-----
 2 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/src/symbolic_async_graph/_impl_symbolic_context.rs b/src/symbolic_async_graph/_impl_symbolic_context.rs
index 10ef3b8..4399a54 100644
--- a/src/symbolic_async_graph/_impl_symbolic_context.rs
+++ b/src/symbolic_async_graph/_impl_symbolic_context.rs
@@ -111,6 +111,23 @@ impl SymbolicContext {
         &self.state_variables
     }
 
+    /// Getter for the entire function table of an implicit update function.
+    pub fn get_implicit_function_table(&self, variable: VariableId) -> &FunctionTable {
+        let table = &self.implicit_function_tables[variable.0];
+        let table = table.as_ref().unwrap_or_else(|| {
+            panic!(
+                "Variable {:?} does not have an implicit uninterpreted function.",
+                variable
+            );
+        });
+        table
+    }
+
+    /// Getter for the entire function table of an explicit parameter.
+    pub fn get_explicit_function_table(&self, parameter: ParameterId) -> &FunctionTable {
+        &self.explicit_function_tables[parameter.0]
+    }
+
     /// Getter for variables encoding the parameter variables of the network.
     pub fn parameter_variables(&self) -> &Vec<BddVariable> {
         &self.parameter_variables
diff --git a/src/symbolic_async_graph/mod.rs b/src/symbolic_async_graph/mod.rs
index c4d5bc6..3302f73 100644
--- a/src/symbolic_async_graph/mod.rs
+++ b/src/symbolic_async_graph/mod.rs
@@ -112,20 +112,19 @@ pub struct SymbolicContext {
     implicit_function_tables: Vec<Option<FunctionTable>>,
 }
 
-/// **(internal)** Function table maps one the table of an uninterpreted function to corresponding
-/// `Bdd`  variables.
+/// Function table maps one the table of an uninterpreted function to corresponding `Bdd` variables.
 ///
 /// The main functionality of a `FunctionTable` is that it provides an iterator over
 /// pairs of `Vec<bool>` (function input assignment) and `BddVariable`
 /// (corresponding symbolic variable).
 #[derive(Debug, Clone)]
-struct FunctionTable {
+pub struct FunctionTable {
     pub arity: u16,
     rows: Vec<BddVariable>,
 }
 
-/// **(internal)** Iterator over elements of the `FunctionTable`.
-struct FunctionTableIterator<'a> {
+/// Iterator over elements of the `FunctionTable`.
+pub struct FunctionTableIterator<'a> {
     inner_iterator: Enumerate<BddValuationIterator>,
     table: &'a FunctionTable,
 }