move varsize

src/algs/flatten.rs

@@ -0,0 +1,30 @@
+use crate::sat::{KnfSat, Variable};
+
+/**
+ * **Algorithm**: Rename Variables to fill [0..n]
+ * **Complexity**: Polynomial `O(n^2)`
+ */
+pub fn flatten(mut sat: KnfSat) -> KnfSat {
+    let mut reference = vec![];
+
+    for clausel in &mut sat.eq {
+        for literal in clausel {
+            let pos = reference.iter().position(|&r| r == literal.abs());
+
+            let new_val: Variable = if let Some(p) = pos {
+                p as Variable + 1
+            } else {
+                reference.push((literal).abs());
+                reference.len() as Variable
+            };
+
+            if literal > &mut 0 {
+                *literal = new_val;
+            } else {
+                *literal = -new_val;
+            }
+        }
+    }
+
+    sat
+}

src/algs/mod.rs

@@ -1,5 +1,7 @@
 pub mod bf0;
+pub mod flatten;
 pub mod knf3;
+pub mod varsize;
 
 // pub fn get_algorithm<T: SatSolver>(sat: KnfSat, alg: u8) -> T {
 //     match alg {

src/algs/varsize.rs

@@ -0,0 +1,23 @@
+use crate::sat::KnfSat;
+
+impl KnfSat {
+    /**
+     * **Algorithm**: Count Variables in Equation
+     * **Complexity**: Polynomial
+     */
+    pub fn varsize(sat: &KnfSat) -> usize {
+        let mut reference = vec![];
+
+        for clausel in &sat.eq {
+            for literal in clausel {
+                let pos = reference.iter().position(|&r| r == literal.abs());
+
+                if let None = pos {
+                    reference.push((literal).abs());
+                };
+            }
+        }
+
+        reference.len()
+    }
+}

src/main.rs

@@ -44,7 +44,7 @@ fn main() {
     }
 
     if let Ok(mut sat) = knf_sat {
-        sat.flatten();
+        // sat.flatten();
         // TODO
         // let mut algorithm = algs::get_algorithm(sat, version);
         // algorithm.optimise();

src/sat/mod.rs

@@ -1,5 +1,3 @@
-pub mod knf_sat;
-
 /**
  * A Variable is denoted as a non-zero number with negatives implying negations of the variable.
  */
@@ -32,3 +30,12 @@ pub type SolveSat = dyn Fn(KnfSat) -> Vec<Variable>;
  * SatSolver
  */
 pub type SolveAllSat = dyn Fn(KnfSat) -> Vec<Vec<Variable>>;
+
+/**
+ * Implementations
+ */
+impl KnfSat {
+    pub fn new() -> Self {
+        Self { eq: vec![vec![]] }
+    }
+}