Struct biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext

pub struct SymbolicContext { /* private fields */ }

Symbolic context manages the mapping between entities of the Boolean network (variables, parameters, uninterpreted functions) and BddVariables used in bdd-lib.

It also provides utility methods for creating Bdd objects that match different conditions imposed on the parameter space of the network.

Note that while this is technically public, it should not be used unless absolutely necessary. Playing with raw BDDs is dangerous.

Implementations

impl SymbolicContext

pub fn new(network: &BooleanNetwork) -> Result<SymbolicContext, String>

Create a new SymbolicContext that encodes the given BooleanNetwork, but otherwise has no additional symbolic variables.

pub fn with_extra_state_variables( network: &BooleanNetwork, extra: &HashMap<VariableId, u16> ) -> Result<SymbolicContext, String>

Create a new SymbolicContext that is based on the given BooleanNetwork, but also contains additional symbolic variables associated with individual network variables.

The “symbolic vs. network variable” association is used to provide a place for the additional variables in the BDD variable ordering. Specifically, the additional variables are placed directly after the corresponding state variable. Consequently, depending on the actual meaning of these extra variables, you might want to place them close to the “most related” state variable to reduce BDD size.

Keep in mind that the total number of symbolic variables cannot exceed u16::MAX. The names of the extra variables will be "{network_variable}_extra_{i}, with i starting at zero (in case you want to reference them by name somewhere).

pub fn network_variables(&self) -> VariableIdIterator

Iterator over all VariableId network variables managed by this SymbolicContext.

pub fn find_network_variable(&self, name: &str) -> Option<VariableId>

Obtain a VariableId of a state variable, assuming such state variable exists.

pub fn get_network_variable_name(&self, variable: VariableId) -> String

Obtain the name of a specific state variable.

pub fn network_parameters(&self) -> ParameterIdIterator

Iterator over all ParameterId of the parameter functions managed by this SymbolicContext.

pub fn network_implicit_parameters(&self) -> Vec<VariableId>

The list of all network variables that have an associated implicit parameter function.

pub fn find_network_parameter(&self, name: &str) -> Option<ParameterId>

Obtain a ParameterId of a parameter function based on a name.

pub fn get_network_parameter_arity(&self, id: ParameterId) -> u16

Obtain the arity of an underlying parameter function.

pub fn get_network_implicit_parameter_arity(&self, id: VariableId) -> u16

Obtain the arity of an underlying implicit function.

pub fn get_network_parameter_name(&self, id: ParameterId) -> String

Obtain the name of an underlying parameter function.

pub fn eliminate_network_variable( &self, variable: VariableId ) -> SymbolicContext

Create a new SymbolicContext which is compatible with the current context (it uses the same BddVariableSet), but is missing the given VariableId.

The new context uses the same ParameterId identifiers as the old context, but has different VariableId identifiers, since one of the variables is no longer used, and VariableId identifiers must be always a contiguous sequence. You should use variable names to “translate” VariableId identifiers between the two symbolic context. Of course, SymbolicContext::transfer_from should also still work.

If the eliminated variable has an implicit parameter associated with it, this parameter is added as a new explicit parameter to ensure it is still accessible. This also makes sense in the context of inlining variables (where this method is used), as the inlined implicit function still “exists” within the network (i.e. we eliminated the variable, but not its function).

Note that the extra state variables and parameter variables do not disappear, even if they are only used by the eliminated variable. However, you cannot access them using the normal methods (e.g. SymbolicContext::get_extra_state_variable), only through the full list (i.e. SymbolicContext::all_extra_state_variables).

pub fn as_canonical_context(&self) -> SymbolicContext

Create a copy of this SymbolicContext which only contains the relevant state and parameter variables.

In other words, the new context is equivalent to calling SymbolicContext::new with the original network that was also used to create this context.

In general, if you are using extra variables in your algorithm, it is preferred to export the result in such a way that the BDDs are compatible with this “canonical” context whenever possible. To do that, you can use this method to create the canonical context, and then use SymbolicContext::transfer_from to translate the output BDDs.

pub fn num_state_variables(&self) -> usize

The number of state variables (should be equal to the number of network variables).

pub fn num_parameter_variables(&self) -> usize

The number of symbolic variables encoding network parameters.

pub fn num_extra_state_variables(&self) -> usize

The number of extra symbolic variables.

pub fn bdd_variable_set(&self) -> &BddVariableSet

Provides access to the raw Bdd context.

pub fn state_variables(&self) -> &Vec<BddVariable>

Getter for variables encoding the state variables of the network.

pub fn parameter_variables(&self) -> &Vec<BddVariable>

Getter for variables encoding the parameter variables of the network.

pub fn all_extra_state_variables(&self) -> &Vec<BddVariable>

Get the list of all extra symbolic variables across all BN variables.

pub fn extra_state_variables(&self, variable: VariableId) -> &Vec<BddVariable>

Get the list of extra symbolic variables associated with a particular BN variable.

pub fn extra_state_variables_by_offset( &self, offset: usize ) -> Vec<(VariableId, BddVariable)>

Retrieve all extra symbolic variables associated with a particular offset across all network variables. If a variable does not have enough extra symbolic variables, it is not included in the result.

pub fn get_state_variable(&self, variable: VariableId) -> BddVariable

Get the BddVariable representing the network variable with the given VariableId.

pub fn find_state_variable( &self, symbolic_variable: BddVariable ) -> Option<VariableId>

Try to find a VariableId which corresponds to the given BddVariable, assuming the BddVariable is one of the Self::state_variables.

pub fn get_extra_state_variable( &self, variable: VariableId, offset: usize ) -> BddVariable

Get the BddVariable extra symbolic variable associated with a particular BN variable and an offset (within the domain of said variable).

pub fn get_implicit_function_table( &self, variable: VariableId ) -> Option<&FunctionTable>

Getter for the entire function table of an implicit update function.

pub fn get_explicit_function_table( &self, parameter: ParameterId ) -> &FunctionTable

Getter for the entire function table of an explicit parameter.

pub fn mk_constant(&self, value: bool) -> Bdd

Create a constant true/false Bdd.

pub fn mk_state_variable_is_true(&self, variable: VariableId) -> Bdd

Create a Bdd that is true when given network variable is true.

pub fn mk_extra_state_variable_is_true( &self, variable: VariableId, offset: usize ) -> Bdd

Create a Bdd that is true when the given extra symbolic variable is true.

pub fn mk_uninterpreted_function_is_true( &self, parameter: ParameterId, args: &[FnUpdate] ) -> Bdd

Create a Bdd that is true when given explicit uninterpreted function (aka parameter) is true for given arguments.

pub fn mk_implicit_function_is_true( &self, variable: VariableId, args: &[VariableId] ) -> Bdd

Create a Bdd that is true when given implicit uninterpreted function is true for given arguments.

Panic: Variable must have an implicit uninterpreted function.

pub fn mk_fn_update_true(&self, function: &FnUpdate) -> Bdd

Create a Bdd that is true when given FnUpdate evaluates to true.

pub fn mk_function_table_true( &self, function_table: &FunctionTable, args: &[Bdd] ) -> Bdd

Create a Bdd that is true when given FunctionTable evaluates to true, assuming each argument is true when the corresponding Bdd in the args array is true.

pub fn instantiate_implicit_function( &self, valuation: &BddValuation, variable: VariableId, args: &[VariableId] ) -> Bdd

Create a Bdd which represents the instantiated implicit uninterpreted function.

pub fn instantiate_uninterpreted_function( &self, valuation: &BddValuation, parameter: ParameterId, args: &[FnUpdate] ) -> Bdd

Create a Bdd which represents the instantiated explicit uninterpreted function.

pub fn instantiate_fn_update( &self, valuation: &BddValuation, function: &FnUpdate ) -> Bdd

Create a Bdd which represents the instantiated FnUpdate.

pub fn mk_instantiated_fn_update( &self, valuation: &BddValuation, function: &Bdd ) -> FnUpdate

Build a DNF representation of an instantiated update function (given as Bdd).

pub fn transfer_from(&self, bdd: &Bdd, ctx: &SymbolicContext) -> Option<Bdd>

This is similar to BddVariableSet::transfer_from, but applied at the level of symbolic contexts.

Note that in theory, this method can translate between different types of symbolic objects (e.g. variable to parameter), but it requires that the two use equivalent names. Hence it is not really possible to create such situation organically, because state, parameter and extra variables are intentionally created with names that are incompatible.

Trait Implementations

impl Clone for SymbolicContext

fn clone(&self) -> SymbolicContext

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SymbolicContext

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for SymbolicContext

fn eq(&self, other: &Self) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for SymbolicContext