Struct biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext

pub struct SymbolicContext {
    bdd: BddVariableSet,
    state_variables: Vec<BddVariable>,
    parameter_variables: Vec<BddVariable>,
    explicit_function_tables: Vec<FunctionTable>,
    implicit_function_tables: Vec<Option<FunctionTable>>,
}

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.

Fields

bdd: BddVariableSet

state_variables: Vec<BddVariable>

parameter_variables: Vec<BddVariable>

explicit_function_tables: Vec<FunctionTable>

implicit_function_tables: Vec<Option<FunctionTable>>

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.

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

(internal) 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.

Note that this actually allows functions which do not have just variables as arguments.

fn instantiate_function_table(
    &self,
    valuation: &BddValuation,
    function_table: &FunctionTable,
    args: &[Bdd]
) -> Bdd

Create a Bdd which represents an instantiated function table.

This means the Bdd only depends on variables which appear in args and the actual semantics to each row of the FunctionTable is assigned based on the given valuation.

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.

fn prepare_args(&self, args: &[VariableId]) -> Vec<Bdd>

(internal) Utility method for converting VariableId arguments to Bdd arguments.

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.