Sketches out manual test using new BooleanSemiring

src/builder/decision_nnf/standard.rs

@@ -59,3 +59,63 @@ impl<'a> StandardDecisionNNFBuilder<'a> {
         }
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use std::collections::HashMap;
+
+    use crate::{
+        builder::{
+            bdd::robdd::{BddPtr, DDNNFPtr, VarLabel},
+            decision_nnf::{builder::DecisionNNFBuilder, standard::StandardDecisionNNFBuilder},
+        },
+        repr::{
+            bdd::{VarOrder, WmcParams},
+            cnf::Cnf,
+        },
+        util::semirings::{boolean::BooleanSemiring, semiring_traits::Semiring},
+    };
+
+    fn gen_bs_mappings(
+        instantations: &[bool],
+    ) -> HashMap<VarLabel, (BooleanSemiring, BooleanSemiring)> {
+        HashMap::from_iter(instantations.iter().enumerate().map(|(index, polarity)| {
+            (
+                VarLabel::new(index as u64),
+                (BooleanSemiring(!polarity), BooleanSemiring(*polarity)),
+            )
+        }))
+    }
+
+    fn bs_wmc(dnnf: &BddPtr, instantations: &[bool], order: &VarOrder) -> bool {
+        dnnf.evaluate(
+            order,
+            &WmcParams::new_with_default(
+                BooleanSemiring::zero(),
+                BooleanSemiring::one(),
+                gen_bs_mappings(instantations),
+            ),
+        )
+        .0
+    }
+
+    #[test]
+    fn trivial_evaluation_test() {
+        static CNF: &str = "
+        p cnf 2 1
+        1 2 0
+        ";
+
+        let cnf = Cnf::from_file(String::from(CNF));
+
+        let linear_order = VarOrder::linear_order(cnf.num_vars());
+
+        let builder = StandardDecisionNNFBuilder::new(linear_order.clone());
+        let dnnf = builder.compile_cnf_topdown(&cnf);
+
+        assert!(bs_wmc(&dnnf, &[true, true], &linear_order));
+        assert!(bs_wmc(&dnnf, &[true, false], &linear_order));
+        assert!(bs_wmc(&dnnf, &[false, true], &linear_order));
+        assert!(!bs_wmc(&dnnf, &[false, false], &linear_order));
+    }
+}

src/repr/ddnnf.rs

@@ -2,8 +2,8 @@
 //! (d-DNNF) pointer type
 use core::fmt::Debug;
 
-use crate::util::semirings::finitefield::FiniteField;
 use crate::util::semirings::semiring_traits::Semiring;
+use crate::util::semirings::{boolean::BooleanSemiring, finitefield::FiniteField};
 use rand::{Rng, SeedableRng};
 use rand_chacha::ChaCha8Rng;
 
@@ -96,6 +96,10 @@ pub trait DDNNFPtr<'a>: Clone + Debug + PartialEq + Eq + Hash + Copy {
         })
     }
 
+    fn evaluate(&self, o: &Self::Order, params: &WmcParams<BooleanSemiring>) -> BooleanSemiring {
+        self.wmc(o, params)
+    }
+
     /// compute the semantic hash for this pointer
     fn semantic_hash<const P: u128>(
         &self,

src/util/semirings/boolean.rs

@@ -0,0 +1,38 @@
+use std::{fmt::Display, ops};
+
+use super::semiring_traits::Semiring;
+
+#[derive(Debug, Clone, Copy, PartialEq, PartialOrd)]
+pub struct BooleanSemiring(pub bool);
+
+impl Semiring for BooleanSemiring {
+    fn one() -> Self {
+        BooleanSemiring(true)
+    }
+
+    fn zero() -> Self {
+        BooleanSemiring(false)
+    }
+}
+
+impl Display for BooleanSemiring {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", self.0)
+    }
+}
+
+impl ops::Add<BooleanSemiring> for BooleanSemiring {
+    type Output = BooleanSemiring;
+
+    fn add(self, rhs: BooleanSemiring) -> Self::Output {
+        BooleanSemiring(self.0 || rhs.0)
+    }
+}
+
+impl ops::Mul<BooleanSemiring> for BooleanSemiring {
+    type Output = BooleanSemiring;
+
+    fn mul(self, rhs: BooleanSemiring) -> Self::Output {
+        BooleanSemiring(self.0 && rhs.0)
+    }
+}

src/util/semirings/mod.rs

@@ -1,3 +1,4 @@
+pub mod boolean;
 pub mod expectation;
 pub mod finitefield;
 pub mod realsemiring;