help
This commit is contained in:
		
							parent
							
								
									2e061e32bd
								
							
						
					
					
						commit
						6b0d72c3a1
					
				
					 1 changed files with 141 additions and 78 deletions
				
			
		
							
								
								
									
										219
									
								
								src/main.rs
									
										
									
									
									
								
							
							
						
						
									
										219
									
								
								src/main.rs
									
										
									
									
									
								
							|  | @ -12,14 +12,9 @@ trait Incrementable { | |||
|     fn increment(&mut self) -> IncrementResult; | ||||
| } | ||||
| 
 | ||||
| #[derive(Debug, Default, Clone)] | ||||
| struct Atom { | ||||
|     smaller: Vec<bool>, | ||||
| } | ||||
| 
 | ||||
| impl Incrementable for Atom { | ||||
| impl Incrementable for Vec<bool> { | ||||
|     fn increment(&mut self) -> IncrementResult { | ||||
|         for a in &mut self.smaller { | ||||
|         for a in self { | ||||
|             *a = !*a; | ||||
|             if *a { | ||||
|                 return Good; | ||||
|  | @ -29,14 +24,38 @@ impl Incrementable for Atom { | |||
|     } | ||||
| } | ||||
| 
 | ||||
| #[derive(Debug, Default, Clone)] | ||||
| struct Atom { | ||||
|     smaller: Vec<bool>, | ||||
| } | ||||
| 
 | ||||
| impl Incrementable for Atom { | ||||
|     fn increment(&mut self) -> IncrementResult { | ||||
|         self.smaller.increment() | ||||
|     } | ||||
| } | ||||
| 
 | ||||
| #[derive(Debug, Default, Clone)] | ||||
| struct AtomSet { | ||||
|     included: Vec<bool>, | ||||
| } | ||||
| 
 | ||||
| impl Incrementable for AtomSet { | ||||
|     fn increment(&mut self) -> IncrementResult { | ||||
|         self.included.increment() | ||||
|     } | ||||
| } | ||||
| 
 | ||||
| #[derive(Debug, Default)] | ||||
| struct Lattice<I: Incrementable + Default> { | ||||
| struct Lattice<I: Incrementable + Default, Ext = ()> { | ||||
|     ext: Ext, | ||||
|     order: Vec<I>, | ||||
| } | ||||
| 
 | ||||
| trait LatticeAbstract { | ||||
|     fn le(&self, a: usize, b: usize) -> bool; | ||||
|     fn grow(&mut self); | ||||
|     fn grow(&mut self) -> IncrementResult; | ||||
|     fn is_lattice(&self) -> bool; | ||||
| } | ||||
| 
 | ||||
| impl Display for Lattice<Atom> { | ||||
|  | @ -64,41 +83,24 @@ impl<I: Incrementable + Default> Incrementable for Lattice<I> { | |||
|     } | ||||
| } | ||||
| 
 | ||||
| impl<I: Incrementable> Lattice<I> | ||||
| impl<I: Incrementable + Default> Lattice<I> | ||||
| where | ||||
|     Self: LatticeAbstract, | ||||
| { | ||||
|     fn next_lattice(&mut self) { | ||||
|     fn next_lattice(&mut self) -> IncrementResult { | ||||
|         self.increment(); | ||||
|         while !self.is_lattice() { | ||||
|             if let Overflow = self.increment() { | ||||
|                 self.grow(); | ||||
|                 if let Overflow = self.grow() { | ||||
|                     return Overflow; | ||||
|                 } | ||||
|             } | ||||
|         } | ||||
|         return Good; | ||||
|     } | ||||
|     fn ge(&self, a: usize, b: usize) -> bool { | ||||
|         return self.le(b, a); | ||||
|     } | ||||
|     // The underlying ordering might not be transitive, this makes it so
 | ||||
|     fn le_transitive(&self, a: usize, b: usize) -> bool { | ||||
|         if self.le(a, b) { | ||||
|             return true; | ||||
|         } | ||||
|         for (b, &active) in self.order[b].smaller.iter().enumerate() { | ||||
|             if active && self.le_transitive(a, b) { | ||||
|                 return true; | ||||
|             } | ||||
|         } | ||||
|         return false; | ||||
|     } | ||||
|     fn is_transitive(&self) -> bool { | ||||
|         for (i, j) in (0..self.order.len()).cartesian_product(0..self.order.len()) { | ||||
|             if !self.le(i, j) && self.le_transitive(i, j) { | ||||
|                 return false; | ||||
|             } | ||||
|         } | ||||
|         return true; | ||||
|     } | ||||
|     fn is_bounded<C, F>(&self, subset: &Vec<usize>, bound_candidates: C, rel: F) -> bool | ||||
|     where | ||||
|         C: Iterator<Item = usize>, | ||||
|  | @ -122,10 +124,7 @@ where | |||
|         return true; | ||||
|     } | ||||
| 
 | ||||
|     fn is_lattice(&self) -> bool { | ||||
|         if !self.is_transitive() { | ||||
|             return false; | ||||
|         } | ||||
|     fn has_lub_glb(&self) -> bool { | ||||
|         // A top/bottom element are inherent as are partial order conditions.
 | ||||
|         // Lattice condition can only fail if a set of elements have non comparable upper/lower bounds
 | ||||
|         // Possible optimization: a lack of LUB might imply no GLB so may only need to check one of them
 | ||||
|  | @ -141,6 +140,49 @@ where | |||
|         } | ||||
|         return true; | ||||
|     } | ||||
|     fn monotone<Inc, Ext>(&self, other: &Lattice<Inc, Ext>) -> bool | ||||
|     where | ||||
|         Inc: Incrementable + Default, | ||||
|         Lattice<Inc, Ext>: LatticeAbstract, | ||||
|     { | ||||
|         assert_eq!(self.order.len(), other.order.len()); | ||||
|         for (a, b) in (0..self.order.len()).cartesian_product((0..other.order.len())) { | ||||
|             if self.le(a, b) && !other.le(a, b) { | ||||
|                 return false; | ||||
|             } | ||||
|         } | ||||
|         return true; | ||||
|     } | ||||
|     fn equal<Inc, Ext>(&self, other: &Lattice<Inc, Ext>) -> bool | ||||
|     where | ||||
|         Inc: Incrementable + Default, | ||||
|         Lattice<Inc, Ext>: LatticeAbstract, | ||||
|     { | ||||
|         self.monotone(other) && other.monotone(self) | ||||
|     } | ||||
| } | ||||
| 
 | ||||
| impl Lattice<Atom> { | ||||
|     fn is_transitive(&self) -> bool { | ||||
|         for (i, j) in (0..self.order.len()).cartesian_product(0..self.order.len()) { | ||||
|             if !self.le(i, j) && self.le_transitive(i, j) { | ||||
|                 return false; | ||||
|             } | ||||
|         } | ||||
|         return true; | ||||
|     } | ||||
|     // The underlying ordering might not be transitive, this makes it so
 | ||||
|     fn le_transitive(&self, a: usize, b: usize) -> bool { | ||||
|         if self.le(a, b) { | ||||
|             return true; | ||||
|         } | ||||
|         for (b, &active) in self.order[b].smaller.iter().enumerate() { | ||||
|             if active && self.le_transitive(a, b) { | ||||
|                 return true; | ||||
|             } | ||||
|         } | ||||
|         return false; | ||||
|     } | ||||
| } | ||||
| 
 | ||||
| impl LatticeAbstract for Lattice<Atom> { | ||||
|  | @ -156,13 +198,17 @@ impl LatticeAbstract for Lattice<Atom> { | |||
|         } | ||||
|         return false; | ||||
|     } | ||||
|     fn grow(&mut self) { | ||||
|     fn grow(&mut self) -> IncrementResult { | ||||
|         self.order = vec![Default::default(); self.order.len() + 1]; | ||||
|         for (i, atom) in self.order.iter_mut().enumerate() { | ||||
|             *atom = Atom { | ||||
|                 smaller: vec![false; i], | ||||
|             } | ||||
|         } | ||||
|         return Good; | ||||
|     } | ||||
|     fn is_lattice(&self) -> bool { | ||||
|         self.is_transitive() && self.has_lub_glb() | ||||
|     } | ||||
| } | ||||
| 
 | ||||
|  | @ -183,6 +229,7 @@ mod tests { | |||
|     #[test] | ||||
|     fn test_is_lattice() -> Result<(), Box<dyn Error>> { | ||||
|         let lattice = Lattice { | ||||
|             ext: (), | ||||
|             order: vec![ | ||||
|                 Atom { smaller: vec![] }, | ||||
|                 Atom { | ||||
|  | @ -195,6 +242,7 @@ mod tests { | |||
|         }; | ||||
|         assert!(lattice.is_lattice()); | ||||
|         let lattice = Lattice { | ||||
|             ext: (), | ||||
|             order: vec![ | ||||
|                 Atom { smaller: vec![] }, | ||||
|                 Atom { | ||||
|  | @ -211,6 +259,7 @@ mod tests { | |||
|     #[test] | ||||
|     fn test_is_not_lattice() -> Result<(), Box<dyn Error>> { | ||||
|         let lattice = Lattice { | ||||
|             ext: (), | ||||
|             order: vec![ | ||||
|                 Atom { smaller: vec![] }, | ||||
|                 Atom { | ||||
|  | @ -223,6 +272,7 @@ mod tests { | |||
|         }; | ||||
|         assert!(!lattice.is_transitive()); | ||||
|         let lattice = Lattice { | ||||
|             ext: (), | ||||
|             order: vec![ | ||||
|                 Atom { smaller: vec![] }, | ||||
|                 Atom { | ||||
|  | @ -242,45 +292,58 @@ mod tests { | |||
|     } | ||||
| } | ||||
| 
 | ||||
| // struct Operator<'a> {
 | ||||
| //     lattice: &'a Lattice,
 | ||||
| //     top: Vec<bool>,
 | ||||
| //     ul: Vec<bool>,
 | ||||
| //     ur: Vec<bool>,
 | ||||
| //     dl: Vec<bool>,
 | ||||
| //     dr: Vec<bool>,
 | ||||
| //     bot: Vec<bool>,
 | ||||
| // }
 | ||||
| 
 | ||||
| // impl<'a> Operator<'a> {
 | ||||
| //     fn new(lattice: &'a Lattice) -> Self {
 | ||||
| //         Operator {
 | ||||
| //             lattice,
 | ||||
| //             top: vec![false; lattice.order.len()],
 | ||||
| //             ul: vec![false; lattice.order.len()],
 | ||||
| //             ur: vec![false; lattice.order.len()],
 | ||||
| //             dl: vec![false; lattice.order.len()],
 | ||||
| //             dr: vec![false; lattice.order.len()],
 | ||||
| //             bot: vec![false; lattice.order.len()],
 | ||||
| //         }
 | ||||
| //     }
 | ||||
| //     fn increment(&mut self) {
 | ||||
| //         let mut data = [
 | ||||
| //             &mut self.bot,
 | ||||
| //             &mut self.dr,
 | ||||
| //             &mut self.dl,
 | ||||
| //             &mut self.ur,
 | ||||
| //             &mut self.ul,
 | ||||
| //             &mut self.top,
 | ||||
| //         ];
 | ||||
| //         data[4][0] = false;
 | ||||
| //         for (i, el) in data.iter_mut().enumerate() {
 | ||||
| //             for a in el.iter_mut() {
 | ||||
| //                 *a = !*a;
 | ||||
| //                 if *a {
 | ||||
| //                     return;
 | ||||
| //                 }
 | ||||
| //             }
 | ||||
| //         }
 | ||||
| //     }
 | ||||
| // }
 | ||||
| struct Mapping<'a> { | ||||
|     domain: &'a Lattice<Atom>, | ||||
|     image: &'a Lattice<Atom>, | ||||
| } | ||||
| 
 | ||||
| // function: Lattice<AtomSet>,
 | ||||
| 
 | ||||
| type Operator<'a> = Lattice<AtomSet, Mapping<'a>>; | ||||
| 
 | ||||
| impl<'a> Operator<'a> { | ||||
|     fn new(domain: &'a Lattice<Atom>, image: &'a Lattice<Atom>) -> Operator<'a> { | ||||
|         Lattice { | ||||
|             ext: Mapping { domain, image }, | ||||
|             order: vec![AtomSet { included: vec![] }; image.order.len()], | ||||
|         } | ||||
|     } | ||||
|     fn all_nonempty(&self) -> bool { | ||||
|         self.order.iter().all(|set| set.included.iter().any(|&x| x)) | ||||
|     } | ||||
|     fn le_helper<I: Iterator<Item = usize> + Clone>(&self, a: I, b: I) -> bool { | ||||
|         b.clone() | ||||
|             .all(|right| a.clone().any(|left| self.ext.domain.le(left, right))) | ||||
|     } | ||||
| } | ||||
| 
 | ||||
| impl<'a> LatticeAbstract for Operator<'a> { | ||||
|     fn le(&self, a: usize, b: usize) -> bool { | ||||
|         let pick = |which: usize| { | ||||
|             self.order[which] | ||||
|                 .included | ||||
|                 .iter() | ||||
|                 .enumerate() | ||||
|                 .filter_map(|(i, &included)| if included { Some(i) } else { None }) | ||||
|         }; | ||||
|         let left = pick(a); | ||||
|         let right = pick(b); | ||||
| 
 | ||||
|         if !self.le_helper(left.clone(), right.clone()) { | ||||
|             return false; | ||||
|         } | ||||
|         if !self.le_helper(right, left) { | ||||
|             return false; | ||||
|         } | ||||
|         return true; | ||||
|     } | ||||
| 
 | ||||
|     fn grow(&mut self) -> IncrementResult { | ||||
|         return Overflow; | ||||
|     } | ||||
| 
 | ||||
|     fn is_lattice(&self) -> bool { | ||||
|         self.all_nonempty() && self.ext.image.equal() | ||||
|     } | ||||
| } | ||||
|  |  | |||
		Loading…
	
	Add table
		
		Reference in a new issue