Skip to content

Commit

Permalink
Add access to function tables using the symbolic context.
Browse files Browse the repository at this point in the history
  • Loading branch information
daemontus committed Dec 29, 2020
1 parent ef430ae commit 09316b4
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 5 deletions.
17 changes: 17 additions & 0 deletions src/symbolic_async_graph/_impl_symbolic_context.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
9 changes: 4 additions & 5 deletions src/symbolic_async_graph/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
}

0 comments on commit 09316b4

Please sign in to comment.