fix bug in is_unique

This commit is contained in:
Folkert 2020-03-22 13:22:52 +01:00
parent db502fe2e7
commit c6fa301d8b

View file

@ -94,34 +94,44 @@ impl Bool {
Atom::Zero => Err(Atom::Zero), Atom::Zero => Err(Atom::Zero),
Atom::One => Err(Atom::One), Atom::One => Err(Atom::One),
Atom::Variable(var) => { Atom::Variable(var) => {
let mut result = Vec::new(); // The var may still point to Zero or One!
result.push(var); match subs.get_without_compacting(var).content {
Content::Structure(FlatType::Boolean(nested)) => nested.simplify(subs),
_ => {
let mut result = Vec::new();
result.push(var);
for atom in &self.1 { for atom in &self.1 {
match atom { match atom {
Atom::Zero => {} Atom::Zero => {}
Atom::One => return Err(Atom::One), Atom::One => return Err(Atom::One),
Atom::Variable(v) => match subs.get_without_compacting(*v).content { Atom::Variable(v) => {
Content::Structure(FlatType::Boolean(nested)) => { match subs.get_without_compacting(*v).content {
match nested.simplify(subs) { Content::Structure(FlatType::Boolean(nested)) => {
Ok(variables) => { match nested.simplify(subs) {
for var in variables { Ok(variables) => {
result.push(var); for var in variables {
result.push(var);
}
}
Err(Atom::Zero) => {}
Err(Atom::One) => return Err(Atom::One),
Err(Atom::Variable(_)) => {
panic!("TODO nested variable")
}
}
}
_ => {
result.push(*v);
} }
} }
Err(Atom::Zero) => {}
Err(Atom::One) => return Err(Atom::One),
Err(Atom::Variable(_)) => panic!("TODO nested variable"),
} }
} }
_ => { }
result.push(*v);
} Ok(result)
},
} }
} }
Ok(result)
} }
} }
} }