1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

//! *Legacy* symbolic representation of parameter space of a `BooleanNetwork` using `Bdds`.
//!
//! Specifically, there is the `BddParams` struct which represents the set of valuations
//! and the `BddParameterEncoder` struct which allows creating new `Bdd` and `BddParams` that
//! correspond to situations where individual parameters have a specific value.

use crate::VariableId;
use biodivine_lib_bdd::{Bdd, BddVariable, BddVariableSet};

mod _impl_bdd_parameter_encoder;
mod _impl_bdd_params;
mod _impl_fn_update;
mod _impl_function_table_entry;
mod _impl_static_constraints;
mod _impl_witness_generator;

pub use _impl_static_constraints::build_static_constraints;

/// A wrapper for the `Bdd` object that implements a basic `Set` trait.
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
pub struct BddParams(Bdd);

/// Handles the translation between parameters of the `BooleanNetwork` and `BddVariables`.
///
/// There are two types of parameters in the `BooleanNetwork` - explicit and implicit.
///
/// Explicit are the named parameters that are specifically declared in the update functions.
/// Implicit are the anonymous parameters representing the missing update functions.
///
/// Every explicit and implicit `Parameter` maps to a set of `BddVariables` that represent
/// the values in its function table. The responsibility of this struct is to create all
/// `BddVariables` and maintain how they map to individual parameters.
#[derive(Clone)]
pub struct BddParameterEncoder {
    /// The actual `BddVariableSet` used to represent the parameters - use this for `.dot` printing etc.
    pub bdd_variables: BddVariableSet,
    /// The actual regulators of each variable - these are used when evaluating implicit parameters.
    regulators: Vec<Vec<VariableId>>,
    /// A vector of function tables indexed by explicit `ParameterId`s of the `BooleanNetwork`.
    explicit_function_tables: Vec<Vec<BddVariable>>,
    /// A vector of implicit function tables indexed by `VariableId`s of the `BooleanNetwork`.
    /// If the variable has an explicit update function, the table is empty.
    implicit_function_tables: Vec<Vec<BddVariable>>,
}

/// **(experimental)** Represents one "line" in a Boolean function table.
///
/// You can query the state of input variables on this line or make a new line
/// with updated variable values.
pub struct FunctionTableEntry<'a> {
    entry_index: usize, // index into the specific table
    table: usize,       // index into the vector of tables
    regulators: &'a Vec<VariableId>,
}