add: check trimming, compression; global node storage

src/structs.rs → src/literal.rs

@@ -1,23 +1,10 @@
-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
-}
+#[derive(Hash, Eq, PartialEq, Debug, Copy, Clone)]
+pub struct VarLabel(u64);
 
 impl VarLabel {
     #[must_use]
-    pub fn new() -> VarLabel {
-        VarLabel {}
-    }
-}
-
-impl Default for VarLabel {
-    #[must_use]
-    fn default() -> Self {
-        VarLabel::new()
+    pub fn new(vl: u64) -> VarLabel {
+        VarLabel(vl)
     }
 }
 
@@ -40,6 +27,7 @@ impl Default for VarLabelManager {
 }
 
 // Either true or false
+#[derive(Hash, Eq, PartialEq, Debug, Clone, Copy)]
 pub struct Literal {
     var_label: VarLabel,
     polarity: bool,
@@ -53,4 +41,22 @@ impl Literal {
             polarity,
         }
     }
+
+    #[must_use]
+    pub fn negate(literal: &Literal) -> Literal {
+        Literal {
+            var_label: VarLabel::new(literal.var_label.0),
+            polarity: !literal.polarity,
+        }
+    }
+
+    #[must_use]
+    pub fn polarity(self) -> bool {
+        self.polarity
+    }
+
+    #[must_use]
+    pub fn var_label(self) -> VarLabel {
+        self.var_label
+    }
 }

src/main.rs

@@ -1,17 +1,19 @@
-use crate::options::{GcSchedule, InitialVTree, SDDOptions, VTreeStrategy};
+use crate::manager::SddManager;
+use crate::options::{GcSchedule, InitialVTree, SddOptions, VTreeStrategy};
 
+pub mod manager;
 pub mod options;
 pub mod sdd;
-pub mod structs;
+pub mod literal;
 pub mod vtree;
 
 fn main() {
-    let options = SDDOptions::default()
+    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);
+    let mut manager = SddManager::new(options);
 }

src/manager.rs

@@ -0,0 +1,57 @@
+use std::collections::HashMap;
+
+use crate::literal::VarLabelManager;
+use crate::options::SddOptions;
+use crate::sdd::Node;
+use crate::sdd::Sdd;
+use crate::vtree::VTreeManager;
+
+#[allow(clippy::module_name_repetitions)]
+pub struct SddManager {
+    options: SddOptions,
+
+    vtree_manager: VTreeManager,
+
+    var_label_manager: VarLabelManager,
+
+    nodes: HashMap<u64, Node>,
+}
+
+impl SddManager {
+    #[must_use]
+    pub fn new(options: SddOptions) -> SddManager {
+        SddManager {
+            options,
+            vtree_manager: VTreeManager::new(),
+            var_label_manager: VarLabelManager::new(),
+            nodes: HashMap::new(),
+        }
+    }
+
+    #[must_use]
+    pub fn new_with_nodes(options: SddOptions, nodes: HashMap<u64, Node>) -> SddManager {
+        SddManager {
+            options,
+            vtree_manager: VTreeManager::new(),
+            var_label_manager: VarLabelManager::new(),
+            nodes,
+        }
+    }
+
+    #[must_use]
+    pub fn get_node(&self, id: &u64) -> Option<&Node> {
+        self.nodes.get(id)
+    }
+
+    pub fn conjoin(&self, _fst: &Sdd, _snd: &Sdd) {}
+    pub fn disjoin(&self, _fst: &Sdd, _snd: &Sdd) {}
+    pub fn negate(&self, _fst: &Sdd) {}
+    pub fn imply(&self, _fst: &Sdd, _snd: &Sdd) {}
+    pub fn equiv(&self, _fst: &Sdd, _snd: &Sdd) {}
+
+    pub fn condition() {}
+    pub fn exist() {}
+    pub fn forall() {}
+
+    // TODO: expose operations manipulating the vtree.
+}

src/options.rs

@@ -19,17 +19,17 @@ pub enum InitialVTree {
 
 #[allow(clippy::module_name_repetitions)]
 #[derive(Debug, Clone, Copy)]
-pub struct SDDOptions {
+pub struct SddOptions {
     gc_schedule: GcSchedule,
 
     vtree_strategy: VTreeStrategy,
     initial_vtree: InitialVTree,
 }
 
-impl Default for SDDOptions {
+impl Default for SddOptions {
     #[must_use]
     fn default() -> Self {
-        SDDOptions {
+        SddOptions {
             gc_schedule: GcSchedule::Automatic(1000),
 
             vtree_strategy: VTreeStrategy::Cycle,
@@ -38,10 +38,10 @@ impl Default for SDDOptions {
     }
 }
 
-impl SDDOptions {
+impl SddOptions {
     #[must_use]
-    pub fn new() -> SDDOptions {
-        SDDOptions::default()
+    pub fn new() -> SddOptions {
+        SddOptions::default()
     }
 
     pub fn set_gc_strategy(&mut self, strategy: VTreeStrategy) -> &mut Self {