From 6ee643ae20ae8817ec5a7f55e9c76489e665eb0a Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 14 Mar 2023 17:13:45 +0100 Subject: [PATCH] Add first 3 value nogood handling Tests for conclusions drawn upon an no-good has been done --- lib/src/nogoods.rs | 57 ++++++ lib/src/nogoods/threevalued.rs | 307 +++++++++++++++++++++++++++++++-- 2 files changed, 352 insertions(+), 12 deletions(-) diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index 238fa6c..b59e4a2 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -2,4 +2,61 @@ pub mod threevalued; pub mod twovalued; +use std::fmt::Display; + pub use twovalued::*; + +// pub trait NoGood: std::fmt::Debug + Eq { +// /// Returns the number of set (i.e. active) variables. +// fn len(&self) -> usize; +// } + +// #[derive(Debug)] +// pub struct NoGoodStore +// where +// N: NoGood + Clone, +// { +// store: Vec>, +// } + +// impl NoGoodStore +// where +// T: NoGood + Clone, +// { +// /// Creates a new [NoGoodStore] and assumes a size compatible with the underlying [NoGood] implementations. +// pub fn new(size: u32) -> Self { +// Self { +// store: vec![Vec::new(); size as usize], +// } +// } + +// /// Tries to create a new [NoGoodStore]. +// /// Does not succeed if the size is too big for the underlying [NoGood] implementations. +// pub fn try_new(size: usize) -> Option { +// Some(Self::new(size.try_into().ok()?)) +// } + +// pub fn add_ng(&mut self, nogood: T) { +// let mut idx = nogood.len(); +// if idx > 0 { +// idx -= 1; +// if !self.store[idx].contains(&nogood) { +// self.store[idx].push(nogood); +// } +// } +// } +// } + +// impl Display for NoGoodStore +// where +// T: NoGood + Clone, +// { +// fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { +// writeln!(f, "NoGoodStats: [")?; +// for (arity, vec) in self.store.iter().enumerate() { +// writeln!(f, "{arity}: {}", vec.len())?; +// log::debug!("Nogoods:\n {:?}", vec); +// } +// write!(f, "]") +// } +// } diff --git a/lib/src/nogoods/threevalued.rs b/lib/src/nogoods/threevalued.rs index 2809145..7fc87e8 100644 --- a/lib/src/nogoods/threevalued.rs +++ b/lib/src/nogoods/threevalued.rs @@ -1,7 +1,5 @@ //! Three-valued NoGoods -use std::borrow::Borrow; - use roaring::RoaringBitmap; use crate::datatypes::Term; @@ -25,22 +23,154 @@ impl Interpretation { self.0 = self.0.invert(); self } + + fn active(&self) -> RoaringBitmap { + self.0.active() + } + + fn hint(&self) -> RoaringBitmap { + ((&self.0.can_be_true & &self.0.can_be_false) + | (&self.0.can_be_true & &self.0.can_be_und) + | (&self.0.can_be_false & &self.0.can_be_und)) + & &self.active() + } + + pub fn len(&self) -> usize { + self.0.len() + } + + fn idx_as_triple(&self, idx: u32) -> (bool, bool, bool) { + self.0.idx_as_triple(idx) + } + + pub fn conclude(mut self, ng: &NoGood) -> Conclusion { + log::debug!("conclude: {:?} with NoGood {:?}", self, ng); + if self.len() + 1 < ng.len() { // not matching + } + let interpretation_cred_active = self.active(); + let interpretation_active = &interpretation_cred_active & (self.hint() ^ self.0.full()); + let nogood_active = ng.active(); + + let implication = (&interpretation_active ^ &nogood_active) & &nogood_active; + let scep_match = self.sceptical_matches(ng); + + match implication.len() { + // learning might be possible + 1 => { + if (scep_match & interpretation_active).len() == nogood_active.len() - 1 { + let idx: u32 = implication + .min() + .expect("Checked that implication has a minimal value to be found."); + let (ng_t, ng_f, ng_u) = ng.idx_as_triple(idx); + let mut changes: u8 = 0; + if ng_t && self.0.can_be_true.remove(idx) { + changes += 1; + } + if ng_f && self.0.can_be_false.remove(idx) { + changes += 1; + } + if ng_u && self.0.can_be_und.remove(idx) { + changes += 1; + } + if self.0.can_be_true.contains(idx) + || self.0.can_be_false.contains(idx) + || self.0.can_be_und.contains(idx) + { + if changes > 0 { + Conclusion::Update(self) + } else { + Conclusion::NoChange(self) + } + } else { + // inconsistency + Conclusion::Inconsistent(self) + } + } else { + Conclusion::NoChange(self) + } + } + // ng-consistency check might be possible + _ => { + if (scep_match & interpretation_active).len() == nogood_active.len() { + Conclusion::Inconsistent(self) + } else { + Conclusion::NoChange(self) + } + } + } + } + fn credulous_matches(&self, other: &NoGood) -> RoaringBitmap { + let true_match = (&self.0.can_be_true ^ &other.can_be_true) ^ self.0.full(); + let false_match = (&self.0.can_be_false ^ &other.can_be_false) ^ self.0.full(); + let und_match = (&self.0.can_be_und ^ &other.can_be_und) ^ self.0.full(); + + true_match | false_match | und_match + } + + fn sceptical_matches(&self, other: &NoGood) -> RoaringBitmap { + let true_match = (&self.0.can_be_true ^ &other.can_be_true) ^ self.0.full(); + let false_match = (&self.0.can_be_false ^ &other.can_be_false) ^ self.0.full(); + let und_match = (&self.0.can_be_und ^ &other.can_be_und) ^ self.0.full(); + + true_match & false_match & und_match + } + + /// Returns the credulous and sceptical matches of the [Interpretation] and a given [NoGood] + fn matches(&self, other: &NoGood) -> (RoaringBitmap, RoaringBitmap) { + let true_match = (&self.0.can_be_true ^ &other.can_be_true) ^ self.0.full(); + let false_match = (&self.0.can_be_false ^ &other.can_be_false) ^ self.0.full(); + let und_match = (&self.0.can_be_und ^ &other.can_be_und) ^ self.0.full(); + + ( + &true_match | &false_match | &und_match, + true_match & false_match & und_match, + ) + } +} + +#[derive(Debug)] +pub enum Conclusion { + Update(Interpretation), + NoChange(Interpretation), + Inconsistent(Interpretation), +} + +impl Conclusion { + fn consistent(self) -> Option { + match self { + Conclusion::Update(val) => Some(val), + Conclusion::NoChange(val) => Some(val), + Conclusion::Inconsistent(_) => None, + } + } } /// Representation of an Interpretation with Hints about truth-values. -#[derive(Debug, Default, Clone)] +#[derive(Debug, Clone)] pub struct NoGood { can_be_true: RoaringBitmap, can_be_false: RoaringBitmap, can_be_und: RoaringBitmap, + size: u32, +} + +impl Default for NoGood { + fn default() -> Self { + Self { + can_be_true: Default::default(), + can_be_false: Default::default(), + can_be_und: Default::default(), + size: Default::default(), + } + } } impl Eq for NoGood {} impl PartialEq for NoGood { fn eq(&self, other: &Self) -> bool { - (self.can_be_true.borrow() ^ other.can_be_true.borrow()).is_empty() - && (self.can_be_false.borrow() ^ other.can_be_false.borrow()).is_empty() - && (self.can_be_und.borrow() ^ other.can_be_und.borrow()).is_empty() + (&self.can_be_true ^ &other.can_be_true).is_empty() + && (&self.can_be_false ^ &other.can_be_false).is_empty() + && (&self.can_be_und ^ &other.can_be_und).is_empty() } } @@ -52,22 +182,42 @@ impl From for NoGood { impl NoGood { fn invert(mut self) -> Self { - self.can_be_true ^= RoaringBitmap::full(); - self.can_be_false ^= RoaringBitmap::full(); - self.can_be_und ^= RoaringBitmap::full(); + self.can_be_true ^= self.full(); + self.can_be_false ^= self.full(); + self.can_be_und ^= self.full(); self } + fn idx_as_triple(&self, idx: u32) -> (bool, bool, bool) { + ( + self.can_be_true.contains(idx), + self.can_be_false.contains(idx), + self.can_be_und.contains(idx), + ) + } + + fn full(&self) -> RoaringBitmap { + let mut result = RoaringBitmap::default(); + result.insert_range(0..self.size); + result + } + /// Creates a [NoGood], based on the given Vector of [Terms][Term] pub fn from_term_vec(term_vec: &[Term]) -> Self { let mut result = Self { - can_be_true: RoaringBitmap::full(), - can_be_false: RoaringBitmap::full(), - can_be_und: RoaringBitmap::full(), + can_be_true: RoaringBitmap::default(), + can_be_false: RoaringBitmap::default(), + can_be_und: RoaringBitmap::default(), + size: TryInto::::try_into(term_vec.len()).expect("no-good learner implementation is based on the assumption that only u32::MAX-many variables are in place"), }; + result.can_be_true.insert_range(0..result.size); + result.can_be_false.insert_range(0..result.size); + result.can_be_und.insert_range(0..result.size); + log::debug!("{:?}", result); term_vec.iter().enumerate().for_each(|(idx, val)| { let idx:u32 = idx.try_into().expect("no-good learner implementation is based on the assumption that only u32::MAX-many variables are in place"); if val.is_truth_value() { + log::trace!("idx {idx} val: {val:?}"); if val.is_true() { result.can_be_false.remove(idx); result.can_be_und.remove(idx); @@ -77,6 +227,139 @@ impl NoGood { } } }); + log::debug!("{:?}", result); result } + + /// Returns the number of set variables. + pub fn len(&self) -> usize { + self.active() + .len() + .try_into() + .expect("Expecting to be on a 64 bit system") + } + + fn active(&self) -> RoaringBitmap { + (&self.can_be_true & &self.can_be_false & &self.can_be_und) ^ &self.full() + } + + fn no_matches(&self, other: &NoGood) -> RoaringBitmap { + let no_true_match = &self.can_be_true ^ &other.can_be_true; + let no_false_match = &self.can_be_false ^ &other.can_be_false; + let no_und_match = &self.can_be_und ^ &other.can_be_und; + + no_true_match | no_false_match | no_und_match + } +} +#[cfg(test)] +mod test { + use super::*; + use test_log::test; + + #[test] + fn create_ng() { + let terms = vec![Term::TOP, Term(22), Term(13232), Term::BOT, Term::TOP]; + let ng = NoGood::from_term_vec(&terms); + + assert_eq!(terms.len(), 5); + assert_eq!(ng.size, 5); + log::debug!("{:?}", ng.active()); + assert_eq!(ng.active().len(), 3); + assert_eq!(ng.idx_as_triple(0), (true, false, false)); + assert_eq!(ng.idx_as_triple(1), (true, true, true)); + assert_eq!(ng.idx_as_triple(2), (true, true, true)); + assert_eq!(ng.idx_as_triple(3), (false, true, false)); + assert_eq!(ng.idx_as_triple(4), (true, false, false)); + } + + #[test] + fn create_interpretation() { + let terms = vec![Term::TOP, Term(22), Term(13232), Term::BOT, Term::TOP]; + let interpretation = Interpretation::from_term_vec(&terms); + + assert_eq!(interpretation.active().len(), 3); + assert_eq!(interpretation.idx_as_triple(0), (true, false, false)); + assert_eq!(interpretation.idx_as_triple(1), (true, true, true)); + assert_eq!(interpretation.idx_as_triple(2), (true, true, true)); + assert_eq!(interpretation.idx_as_triple(3), (false, true, false)); + assert_eq!(interpretation.idx_as_triple(4), (true, false, false)); + } + + #[test] + fn conclude() { + let ng1 = Interpretation::from_term_vec(&[ + Term::TOP, + Term(22), + Term::TOP, + Term::BOT, + Term::TOP, + Term(22), + ]); + let ng2 = Interpretation::from_term_vec(&[ + Term::TOP, + Term(22), + Term(13232), + Term::BOT, + Term::TOP, + Term(22), + ]); + let ng3 = Interpretation::from_term_vec(&[ + Term::TOP, + Term(22), + Term::BOT, + Term::BOT, + Term::TOP, + Term(22), + ]); + + let mut ng4 = ng3.clone(); + ng4.0.can_be_und.insert(2); + ng4.0.can_be_false.remove(2); + + let ng_too_big = Interpretation::from_term_vec(&[ + Term::TOP, + Term(22), + Term::TOP, + Term::BOT, + Term::TOP, + Term::BOT, + ]); + + assert!(ng1.clone().conclude(&ng2.0).consistent().is_none()); + let result = ng2.clone().conclude(&ng1.0).consistent().unwrap(); + assert_eq!(result.idx_as_triple(0), (true, false, false)); + assert_eq!(result.idx_as_triple(1), (true, true, true)); + assert_eq!(result.idx_as_triple(2), (false, true, true)); + assert_eq!(result.idx_as_triple(3), (false, true, false)); + assert_eq!(result.idx_as_triple(4), (true, false, false)); + + let result = result.conclude(&ng3.0).consistent().unwrap(); + assert_eq!(result.idx_as_triple(0), (true, false, false)); + assert_eq!(result.idx_as_triple(1), (true, true, true)); + assert_eq!(result.idx_as_triple(2), (false, false, true)); + assert_eq!(result.idx_as_triple(3), (false, true, false)); + assert_eq!(result.idx_as_triple(4), (true, false, false)); + + assert!(result.conclude(&ng4.0).consistent().is_none()); + + let result = ng2 + .clone() + .conclude(&ng1.0) + .consistent() + .and_then(|i| i.conclude(&ng4.0).consistent()) + .unwrap(); + + assert_eq!(result.idx_as_triple(0), (true, false, false)); + assert_eq!(result.idx_as_triple(1), (true, true, true)); + assert_eq!(result.idx_as_triple(2), (false, true, false)); + assert_eq!(result.idx_as_triple(3), (false, true, false)); + assert_eq!(result.idx_as_triple(4), (true, false, false)); + + log::debug!("{:?}", ng2.clone().conclude(&ng_too_big.0)); + if let Conclusion::NoChange(interpretation) = ng2.clone().conclude(&ng_too_big.0) { + assert_eq!(interpretation, ng2); + } else { + panic!("test failed"); + } + } }