From 6a47f4db30dfb19982ce1ce19c07da69f10ffae9 Mon Sep 17 00:00:00 2001
From: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
Date: Wed, 30 Mar 2022 13:15:49 +0200
Subject: [PATCH] Add debugging infos

Currently the stable models (counting-based) has issues with a couple
of
instances (e.g. adfgen_nacyc_se05_a_02_s_02_b_02_t_02_x_02_c_sXOR_Planning2AF_ferry2.pfile-L2-C1-03.pddl.1.cnf_123_211.apx.adf )
of the examples in the res-folder.

Need further debugging and analysis.
---
 lib/src/adf.rs  | 17 ++++++++++++++++-
 lib/src/obdd.rs | 24 ++++++++++++++++++++++++
 2 files changed, 40 insertions(+), 1 deletion(-)

diff --git a/lib/src/adf.rs b/lib/src/adf.rs
index 1caeff5..0efc77c 100644
--- a/lib/src/adf.rs
+++ b/lib/src/adf.rs
@@ -5,7 +5,9 @@ This module describes the abstract dialectical framework
  - computing fixpoints
 */
 
-use serde::{Deserialize, Serialize};
+use std::collections::HashSet;
+
+use serde::{ser::SerializeMap, Deserialize, Serialize};
 
 use crate::{
     datatypes::{
@@ -27,6 +29,8 @@ pub struct Adf {
     ordering: VarContainer,
     bdd: Bdd,
     ac: Vec<Term>,
+    #[serde(skip)]
+    callcache: HashSet<Vec<Term>>,
 }
 
 impl Default for Adf {
@@ -35,6 +39,7 @@ impl Default for Adf {
             ordering: VarContainer::default(),
             bdd: Bdd::new(),
             ac: Vec::new(),
+            callcache: HashSet::new(),
         }
     }
 }
@@ -50,6 +55,7 @@ impl Adf {
             ),
             bdd: Bdd::new(),
             ac: vec![Term(0); parser.namelist_rc_refcell().as_ref().borrow().len()],
+            callcache: HashSet::new(),
         };
         (0..parser.namelist_rc_refcell().borrow().len())
             .into_iter()
@@ -87,6 +93,7 @@ impl Adf {
             ordering: VarContainer::copy(ordering),
             bdd: Bdd::new(),
             ac: vec![Term(0); bio_ac.len()],
+            callcache: HashSet::new(),
         };
         result
             .ac
@@ -397,8 +404,15 @@ impl Adf {
         will_be: &[Term],
         depth: usize,
     ) -> Vec<Vec<Term>> {
+        if self.callcache.contains(&interpr.to_vec()) {
+            panic!("moo");
+        }
+        self.callcache.insert(interpr.to_vec());
         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()
@@ -466,6 +480,7 @@ impl Adf {
                     }
                     res
                 });
+            log::trace!("results found so far:{}", result.len());
             // checked one alternative, we can now conclude that only the other option may work
             log::trace!("checked one alternative, concluding the other value");
             let new_int = interpr
diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs
index e9be1ca..3f4e718 100644
--- a/lib/src/obdd.rs
+++ b/lib/src/obdd.rs
@@ -286,6 +286,25 @@ impl Bdd {
         }
     }
 
+    pub fn max_depth(&self, term: Term) -> usize {
+        #[cfg(feature = "adhoccounting")]
+        {
+            return self.count_cache.borrow().get(&term).expect("The term should be originating from this bdd, otherwise the result would be inconsistent anyways").1;
+        }
+        #[cfg(not(feature = "adhoccounting"))]
+        match self.count_cache.borrow().get(&term) {
+            Some((mc, depth)) => *depth,
+            None => {
+                if term.is_truth_value() {
+                    0
+                } else {
+                    self.max_depth(self.nodes[term.0].hi())
+                        .max(self.max_depth(self.nodes[term.0].lo()))
+                }
+            }
+        }
+    }
+
     #[allow(dead_code)] // dead code due to more efficient ad-hoc building, still used for a couple of tests
     /// Computes the number of counter-models, models, and variables for a given BDD-tree
     fn modelcount_naive(&self, term: Term) -> CountNode {
@@ -598,6 +617,11 @@ mod test {
             bdd.modelcount_naive(Term::BOT),
             bdd.modelcount_memoization(Term::BOT)
         );
+
+        assert_eq!(bdd.max_depth(Term::BOT), 0);
+        assert_eq!(bdd.max_depth(v1), 1);
+        assert_eq!(bdd.max_depth(formula3), 2);
+        assert_eq!(bdd.max_depth(formula4), 3);
     }
 
     #[cfg(feature = "variablelist")]