Optimise ng learner further on and fix a verification bug

Introduce a new flag to handle big instances (modelcount vs adhoccount)

bin/Cargo.toml

@@ -33,3 +33,4 @@ adhoccounting = ["adf_bdd/adhoccounting"]    # count models ad-hoc - disable if
 importexport = ["adf_bdd/importexport"]
 variablelist = [ "HashSet", "adf_bdd/variablelist" ]
 HashSet = ["adf_bdd/HashSet"]
+adhoccountmodels = ["adf_bdd/adhoccountmodels"]

lib/Cargo.toml

@@ -41,7 +41,8 @@ quickcheck_macros = "1"
 
 [features]
 default = ["adhoccounting", "variablelist" ]   
-adhoccounting = []    # count models ad-hoc - disable if counting is not needed
+adhoccounting = []    # count paths ad-hoc - disable if counting is not needed
 importexport = []
 variablelist = [ "HashSet" ]
 HashSet = []
+adhoccountmodels = [ "adhoccounting" ] # count models as well as paths ad-hoc

lib/src/adf.rs

@@ -136,6 +136,8 @@ impl Adf {
                     }
                 }
             });
+        log::trace!("ordering: {:?}", result.ordering);
+        log::trace!("adf {:?} instantiated with bdd {}", result.ac, result.bdd);
         result
     }
 
@@ -812,6 +814,24 @@ impl Adf {
                 }
             }
 
+            let ac_consistent_interpr = self.apply_interpretation(&self.ac.clone(), &cur_interpr);
+            log::trace!(
+                "checking consistency of {:?} against {:?}",
+                ac_consistent_interpr,
+                cur_interpr
+            );
+            if cur_interpr
+                .iter()
+                .zip(ac_consistent_interpr.iter())
+                .any(|(cur, ac)| {
+                    cur.is_truth_value() && ac.is_truth_value() && cur.is_true() != ac.is_true()
+                })
+            {
+                log::trace!("ac_inconsistency");
+                backtrack = true;
+                continue;
+            }
+
             cur_interpr = self.update_interpretation_fixpoint_upd(&cur_interpr, &mut update_fp);
             if update_fp {
                 log::trace!("fixpount updated");
@@ -827,12 +847,14 @@ impl Adf {
                     backtrack = true;
                 } else {
                     // not stable
+                    log::trace!("2 val not stable");
                     stack.push((false, cur_interpr.as_slice().into()));
                     backtrack = true;
                 }
             }
         }
         log::info!("{ng_store}");
+        log::debug!("{:?}", ng_store);
         result
     }
 }

lib/src/nogoods.rs

@@ -2,7 +2,7 @@
 
 use std::{
     borrow::Borrow,
-    fmt::Display,
+    fmt::{Debug, Display},
     ops::{BitAnd, BitOr, BitXor, BitXorAssign},
 };
 
@@ -191,6 +191,7 @@ impl Display for NoGoodStore {
         writeln!(f, "NoGoodStats: [")?;
         for (arity, vec) in self.store.iter().enumerate() {
             writeln!(f, "{arity}: {}", vec.len())?;
+            log::debug!("Nogoods:\n {:?}", vec);
         }
         write!(f, "]")
     }

lib/src/obdd.rs

@@ -277,11 +277,14 @@ impl Bdd {
                             hi_paths.models,
                             hidepth
                         );
+                        #[cfg(feature = "adhoccountmodels")]
                         let (lo_exp, hi_exp) = if lodepth > hidepth {
                             (1, 2usize.pow((lodepth - hidepth) as u32))
                         } else {
                             (2usize.pow((hidepth - lodepth) as u32), 1)
                         };
+                        #[cfg(not(feature = "adhoccountmodels"))]
+                        let (lo_exp, hi_exp) = (0, 0);
                         log::debug!("lo_exp {}, hi_exp {}", lo_exp, hi_exp);
                         count_cache.insert(
                             new_term,
@@ -310,11 +313,11 @@ impl Bdd {
     ///
     /// Use the flag `_memoization` to choose between using the memoization approach or not. (This flag does nothing, if the feature `adhoccounting` is used)
     pub fn models(&self, term: Term, _memoization: bool) -> ModelCounts {
-        #[cfg(feature = "adhoccounting")]
+        #[cfg(feature = "adhoccountmodels")]
         {
             return self.count_cache.borrow().get(&term).expect("The term should be originating from this bdd, otherwise the result would be inconsistent anyways").0;
         }
-        #[cfg(not(feature = "adhoccounting"))]
+        #[cfg(not(feature = "adhoccountmodels"))]
         if _memoization {
             self.modelcount_memoization(term).0
         } else {