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 is based on the given BooleanNetwork.

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 get_implicit_function_table(
    &self,
    variable: VariableId
) -> &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 parameter_variables(&self) -> &Vec<BddVariable>

Getter for variables encoding the parameter variables of the network.

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_uninterpreted_function_is_true(
    &self,
    parameter: ParameterId,
    args: &[VariableId]
) -> 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 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: &[VariableId]
) -> 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.

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.