add: data structures draft

src/main.rs

@@ -1,3 +1,17 @@
+use crate::options::{GcSchedule, InitialVTree, SddOptions, VTreeStrategy};
+
+pub mod options;
+pub mod sdd;
+pub mod structs;
+pub mod vtree;
+
 fn main() {
-    println!("Hello, world!");
+    let options = SddOptions::default()
+        .set_gc_schedule(GcSchedule::Automatic(1120))
+        .set_gc_strategy(VTreeStrategy::Cycle)
+        .set_initial_vtree(InitialVTree::Balanced)
+        .to_owned();
+
+    #[allow(unused)]
+    let mut manager = sdd::SDDManager::new(options);
 }

src/options.rs

@@ -0,0 +1,58 @@
+#[derive(Debug, Clone, Copy)]
+pub enum GcSchedule {
+    Manual,
+    Automatic(usize), // usize denotes the threshold when the GC would be triggered
+}
+
+#[derive(Debug, Clone, Copy)]
+pub enum VTreeStrategy {
+    Custom(()), // TODO: Add type for custom function that will manipulate vtrees when GC is triggered
+    Cycle, // This is the "default" strategy in the original C SDD library that cycles through all vtrees within the given resources.
+}
+
+#[derive(Debug, Clone, Copy)]
+pub enum InitialVTree {
+    Balanced,
+    LeftLinear,
+    RightLinear,
+}
+
+#[derive(Debug, Clone, Copy)]
+pub struct SddOptions {
+    gc_schedule: GcSchedule,
+
+    vtree_strategy: VTreeStrategy,
+    initial_vtree: InitialVTree,
+}
+
+impl Default for SddOptions {
+    fn default() -> Self {
+        SddOptions {
+            gc_schedule: GcSchedule::Automatic(1000),
+
+            vtree_strategy: VTreeStrategy::Cycle,
+            initial_vtree: InitialVTree::Balanced,
+        }
+    }
+}
+
+impl SddOptions {
+    pub fn new() -> SddOptions {
+        SddOptions::default()
+    }
+
+    pub fn set_gc_strategy(&mut self, strategy: VTreeStrategy) -> &mut Self {
+        self.vtree_strategy = strategy;
+        self
+    }
+
+    pub fn set_gc_schedule(&mut self, schedule: GcSchedule) -> &mut Self {
+        self.gc_schedule = schedule;
+        self
+    }
+
+    pub fn set_initial_vtree(&mut self, initial_vtree: InitialVTree) -> &mut Self {
+        self.initial_vtree = initial_vtree;
+        self
+    }
+}

src/sdd.rs

@@ -0,0 +1,74 @@
+use std::collections::HashMap;
+use std::hash::{Hash, Hasher};
+
+use crate::options::SddOptions;
+use crate::structs::{VarLabel, VarLabelManager};
+use crate::vtree::{VTree, VTreeManager};
+
+pub enum SDDNode {
+    // TODO: Is `neg` in the original C library the same as `Reg` and `Compl` in rsdd?
+    // TODO: Why is `Reg` and `Compl` defined in here in rsdd?
+    False,
+    True,
+    Literal(VarLabel),
+    Decision(SDDOr), // Decision node represents decomposition
+}
+
+impl Hash for SDDNode {
+    fn hash<H: Hasher>(&self, state: &mut H) {}
+}
+
+// Decision node, disjunction of its elements
+pub struct SDDOr {
+    // TODO: In rsdd, SddOr contains also VTreeIndex (and a scratch field), do we need it as well?
+    // TODO: Should `element` be a vector or a single SDDAnd node? Original C library uses a single node,
+    // rsdd uses a vector. What's the difference?
+    element: Vec<SDDAnd>,
+
+    // for GC
+    ref_count: usize,
+}
+// Element node (a paired box), conjunction of prime and sub
+pub struct SDDAnd {
+    // prime, sub, both are either: ptr to decision node, constant (True or False) or a literal (X or !X)
+    prime: Box<SDDNode>,
+    sub: Box<SDDNode>,
+
+    // for GC
+    ref_count: usize,
+}
+
+pub struct SDDManager {
+    options: SddOptions,
+
+    vtree_manager: VTreeManager,
+    vtree_root: VTree,
+
+    var_label_manager: VarLabelManager,
+
+    nodes: HashMap<u64, SDDNode>,
+}
+
+impl SDDManager {
+    pub fn new(options: SddOptions) -> SDDManager {
+        SDDManager {
+            options,
+            vtree_manager: VTreeManager::new(),
+            vtree_root: VTree::new(None, None),
+            var_label_manager: VarLabelManager::new(),
+            nodes: HashMap::new(),
+        }
+    }
+
+    pub fn conjoin() {}
+    pub fn disjoin() {}
+    pub fn negate() {}
+    pub fn imply() {}
+    pub fn equiv() {}
+
+    pub fn condition() {}
+    pub fn exist() {}
+    pub fn forall() {}
+
+    // TODO: expose operations manipulating the vtree.
+}

src/structs.rs

@@ -0,0 +1,39 @@
+pub struct VarLabel {
+    // TODO: uint64, int64 or String?
+    // uint64: rsdd (=> varset)
+    // int64: original c library (=> negation of variable with index X represented as -X)
+    // ?String: biodivine-lib-bdd?
+
+    // can be true or false
+}
+
+impl VarLabel {
+    pub fn new() -> VarLabel {
+        VarLabel {}
+    }
+}
+
+pub struct VarLabelManager {
+    // TODO: bitset?, vector, hashmap?
+}
+
+impl VarLabelManager {
+    pub fn new() -> VarLabelManager {
+        VarLabelManager {}
+    }
+}
+
+// Either true or false
+pub struct Literal {
+    var_label: VarLabel,
+    polarity: bool,
+}
+
+impl Literal {
+    pub fn new(polarity: bool, var_label: VarLabel) -> Literal {
+        Literal {
+            var_label,
+            polarity,
+        }
+    }
+}

src/vtree.rs

@@ -0,0 +1,59 @@
+pub struct VTree {
+    // TODO: Search states, shadow vtree.
+    left: Option<Box<VTree>>,
+    right: Option<Box<VTree>>,
+}
+
+impl VTree {
+    pub fn new(left: Option<Box<VTree>>, right: Option<Box<VTree>>) -> VTree {
+        VTree { left, right }
+    }
+
+    // right-linear fragment:
+    //         X
+    //        / \
+    //       Y   Z
+    //          / \
+    //         G   D
+    // idea: cycle through all the 12 different configurations of the right-linear fragment using rotations and swapping.
+    //  => fragment operations: next, previous, goto
+    //  => greedy search for better vtree when the SDD is too large:
+    //     - enumerate all (24 = 12 + 12) vtrees over a window
+    //     - greedily accept best vtree, move window
+
+    // Explore dissections but not all possible vtrees,
+    // since it's not possible to explore different variable orders because rotations preserve the order of the variables.
+    // TODO: For systematic methods check 'Art of Computer Programming, Volume 4, Fascicle 4: Generating all Tree'
+    pub fn right_rotate(&self) {}
+
+    // Explore dissections but not all possible vtrees,
+    // since it's not possible to explore different variable orders because rotations preserve the order of the variables.
+    // TODO: For systematic methods check 'Art of Computer Programming, Volume 4, Fascicle 4: Generating all Tree'
+    pub fn left_rotate(&self) {}
+
+    // TODO: Is swapping done only on siblings? What about swapping a leaf with its cousin? Seems so.
+    // Dynamic Minimization of Sentential Decision Diagrams paper.
+    pub fn swap(&self) {}
+
+    // fragment operations: next, previous, goto
+    pub fn next() {}
+    pub fn previous() {}
+    pub fn goto() {}
+}
+
+pub struct VTreeManager {
+    root: Option<VTree>,
+
+    dfs_to_bfs: Vec<u64>,
+    bfs_to_dfs: Vec<u64>,
+}
+
+impl VTreeManager {
+    pub fn new() -> VTreeManager {
+        VTreeManager {
+            root: None,
+            dfs_to_bfs: Vec::new(),
+            bfs_to_dfs: Vec::new(),
+        }
+    }
+}