This commit is contained in:
Spencer Killen 2023-12-21 23:13:11 -07:00
parent 2b7373698b
commit f948eecaaa
Signed by: sjkillen
GPG Key ID: 3AF3117BA6FBB75B
1 changed files with 101 additions and 16 deletions

View File

@ -74,8 +74,8 @@ impl Display for Lattice<Atom, ()> {
impl<I: Incrementable + Default, Ext> Incrementable for Lattice<I, Ext> {
fn increment(&mut self) -> IncrementResult {
for atom in &mut self.order {
if let Good = atom.increment() {
for element in &mut self.order {
if let Good = element.increment() {
return Good;
}
}
@ -88,16 +88,17 @@ where
Self: LatticeAbstract,
{
fn next_lattice(&mut self) -> IncrementResult {
self.increment();
while !self.is_lattice() {
loop {
if let Overflow = self.increment() {
if let Overflow = self.grow() {
return Overflow;
}
}
}
if self.is_lattice() {
return Good;
}
}
}
fn ge(&self, a: usize, b: usize) -> bool {
return self.le(b, a);
}
@ -140,7 +141,7 @@ where
}
return true;
}
fn monotone<IncB, ExtB>(&self, other: &Lattice<IncB, ExtB>) -> bool
fn order_preserving<IncB, ExtB>(&self, other: &Lattice<IncB, ExtB>) -> bool
where
IncB: Incrementable + Default,
Lattice<IncB, ExtB>: LatticeAbstract,
@ -158,7 +159,7 @@ where
IncB: Incrementable + Default,
Lattice<IncB, ExtB>: LatticeAbstract,
{
self.monotone(other) && other.monotone(self)
self.order_preserving(other) && other.order_preserving(self)
}
}
@ -299,15 +300,24 @@ 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()],
order: vec![
AtomSet {
included: vec![false; domain.order.len()]
};
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 {
fn le_helper<I, F>(&self, a: I, b: I, rel: F) -> bool
where
I: Iterator<Item = usize> + Clone,
F: Fn(&Lattice<Atom, ()>, usize, usize) -> bool,
{
b.clone()
.all(|right| a.clone().any(|left| self.ext.domain.le(left, right)))
.all(|right| a.clone().any(|left| rel(&self.ext.domain, left, right)))
}
}
@ -323,10 +333,10 @@ impl<'a> LatticeAbstract for Operator<'a> {
let left = pick(a);
let right = pick(b);
if !self.le_helper(left.clone(), right.clone()) {
if !self.le_helper(left.clone(), right.clone(), Lattice::<Atom, ()>::le) {
return false;
}
if !self.le_helper(right, left) {
if !self.le_helper(right, left, Lattice::<Atom, ()>::ge) {
return false;
}
return true;
@ -362,6 +372,78 @@ mod operator_tests {
#[test]
fn test_operator() {
let domain = &Lattice {
ext: (),
order: vec![
Atom { smaller: vec![] },
Atom {
smaller: vec![true],
},
Atom {
smaller: vec![true, false],
},
],
};
let image = &Lattice {
ext: (),
order: vec![
Atom { smaller: vec![] },
Atom {
smaller: vec![true],
},
Atom {
smaller: vec![true, false],
},
],
};
assert!(domain.is_lattice());
assert!(image.is_lattice());
assert!(image.equal(domain));
// Identity operator
let operator = Lattice {
ext: Mapping { domain, image },
order: vec![
AtomSet {
included: vec![true, false, false],
},
AtomSet {
included: vec![false, true, false],
},
AtomSet {
included: vec![false, false, true],
},
],
};
assert!(operator.is_lattice());
}
#[test]
fn test_order_preserving() {
let lattice_a = Lattice {
ext: (),
order: vec![
Atom { smaller: vec![] },
Atom {
smaller: vec![true],
},
Atom {
smaller: vec![true, false],
},
],
};
let lattice_b = Lattice {
ext: (),
order: vec![
Atom { smaller: vec![] },
Atom {
smaller: vec![true],
},
Atom {
smaller: vec![true, false],
},
],
};
assert!(lattice_a.order_preserving(&lattice_b));
}
}
@ -379,12 +461,15 @@ fn main() {
},
],
};
loop {
domain.next_lattice();
while let Good = domain.next_lattice() {
if domain.order.len() != image.order.len() || !domain.order_preserving(&image) {
continue;
}
println!("{}", domain);
let mut operator = Operator::new(&domain, &image);
while let Good = operator.next_lattice() {
println!("{}", operator);
while let Good = operator.increment() {
// println!("ah: {}", operator);
// TODO doesn't work because we generate a domain larger than the image lol
}
}
}