From 8d9e7f09e1a5fd5e847ff53ddfb68556de9971f9 Mon Sep 17 00:00:00 2001
From: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
Date: Mon, 4 Apr 2022 12:56:12 +0200
Subject: [PATCH] Add new heuristics approach

Selecting the minimal number of paths in the bdds, then choosing
variable with the highest impact.
---
 lib/src/adf.rs | 24 ++++++------------------
 1 file changed, 6 insertions(+), 18 deletions(-)

diff --git a/lib/src/adf.rs b/lib/src/adf.rs
index 5a72c67..0996587 100644
--- a/lib/src/adf.rs
+++ b/lib/src/adf.rs
@@ -404,20 +404,7 @@ impl Adf {
         will_be: &[Term],
         depth: usize,
     ) -> Vec<Vec<Term>> {
-        let cacheitem = interpr
-            .iter()
-            .enumerate()
-            .map(|(idx, val)| *val.min(&will_be[idx]))
-            .collect::<Vec<Term>>();
-        if !self.callcache.insert(cacheitem) {
-            panic!("trying to check the same model candidate twice");
-            return Vec::new();
-        }
-        log::trace!("two_val_model_counts({:?}) called", interpr);
         log::debug!("two_val_model_recursion_depth: {}/{}", depth, interpr.len());
-        //for (idx, &ac) in interpr.iter().enumerate() {
-        //    log::trace!("idx{}, ac: Term({}), modelc-/+: {:?}, depth:{}, impact: {}, num_interpr+: {}, num interpr-: {}", idx, ac, self.bdd.models(ac, true), self.bdd.max_depth(ac), self.bdd.var_impact(Var(idx),interpr), self.bdd.interpretations(ac, true, Var(idx), &[], &[]).len(),self.bdd.interpretations(ac, false, Var(idx), &[], &[]).len());
-        //}
         if let Some((idx, ac)) = interpr
             .iter()
             .enumerate()
@@ -425,20 +412,21 @@ impl Adf {
             .min_by(|(idx_a, val_a), (idx_b, val_b)| {
                 match self
                     .bdd
-                    .var_impact(Var(*idx_b), interpr)
-                    .cmp(&self.bdd.var_impact(Var(*idx_a), interpr))
+                    .paths(**val_a, true)
+                    .minimum()
+                    .cmp(&self.bdd.paths(**val_b, true).minimum())
                 {
                     // if the minimal counts are equal, choose the maximal var_impact
                     std::cmp::Ordering::Equal => self
                         .bdd
-                        .max_depth(**val_a)
-                        .cmp(&self.bdd.max_depth(**val_b)),
+                        .var_impact(Var(*idx_b), interpr)
+                        .cmp(&self.bdd.var_impact(Var(*idx_a), interpr)),
                     value => value,
                 }
             })
         {
             let mut result = Vec::new();
-            let check_models = !self.bdd.models(*ac, true).more_models();
+            let check_models = !self.bdd.paths(*ac, true).more_models();
             log::trace!(
                 "Identified Var({}) with ac {:?} to be {}",
                 idx,