From d0a897589c5854a3557bc0c0d2fe675b4156cedb Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 9 Feb 2018 17:44:07 -0500 Subject: [PATCH] remove support for congruence closure computation Supporting congruence closure requires the `unioned_keys` iterator, which in turn requires maintaining the parent/sibling pointers. This grows the size of nodes, which in turn leads to a 2% slowdown in various rustc test cases (e.g., the `coercions` benchmark in perf.rust-lang.org). Given that this feature is not used in chalk or anywhere else, no reason to support it. --- src/cc/mod.rs | 429 --------------------------------------------- src/cc/test.rs | 424 -------------------------------------------- src/lib.rs | 12 +- src/unify/mod.rs | 115 +----------- src/unify/tests.rs | 29 --- 5 files changed, 8 insertions(+), 1001 deletions(-) delete mode 100644 src/cc/mod.rs delete mode 100644 src/cc/test.rs diff --git a/src/cc/mod.rs b/src/cc/mod.rs deleted file mode 100644 index e372c14..0000000 --- a/src/cc/mod.rs +++ /dev/null @@ -1,429 +0,0 @@ -#![cfg(feature = "congruence-closure")] - -//! An implementation of the Congruence Closure algorithm based on the -//! paper "Fast Decision Procedures Based on Congruence Closure" by Nelson -//! and Oppen, JACM 1980. - -use petgraph::Direction; -use petgraph::graph::{Graph, NodeIndex}; -use std::collections::HashMap; -use std::fmt::Debug; -use std::hash::Hash; -use unify::{NoError, InPlace, InPlaceUnificationTable, UnifyKey, UnifyValue, UnionedKeys}; - -#[cfg(test)] -mod test; - -pub struct CongruenceClosure { - map: HashMap, - table: InPlaceUnificationTable, - graph: Graph, -} - -pub trait Key: Hash + Eq + Clone + Debug { - // If this Key has some efficient way of converting itself into a - // congruence closure `Token`, then it shold return `Some(token)`. - // Otherwise, return `None`, in which case the CC will internally - // map the key to a token. Typically, this is used by layers that - // wrap the CC, where inference variables are mapped directly to - // particular tokens. - fn to_token(&self) -> Option { - None - } - fn key_kind(&self) -> KeyKind; - fn shallow_eq(&self, key: &Self) -> bool; - fn successors(&self) -> Vec; -} - -#[derive(Copy, Clone, Debug, PartialEq, Eq)] -pub enum KeyKind { - Applicative, - Generative, -} -use self::KeyKind::*; - -#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct Token { - // this is the index both for the graph and the unification table, - // since for every node there is also a slot in the unification - // table - index: u32, -} - -impl Token { - fn new(index: u32) -> Token { - Token { index: index } - } - - fn from_node(node: NodeIndex) -> Token { - Token { - index: node.index() as u32, - } - } - - fn node(&self) -> NodeIndex { - NodeIndex::new(self.index as usize) - } -} - -impl UnifyKey for Token { - type Value = KeyKind; - fn index(&self) -> u32 { - self.index - } - fn from_index(i: u32) -> Token { - Token::new(i) - } - fn tag() -> &'static str { - "CongruenceClosure" - } - fn order_roots( - a: Self, - &a_value: &KeyKind, - b: Self, - &b_value: &KeyKind, - ) -> Option<(Self, Self)> { - if a_value == b_value { - None - } else if a_value == Generative { - Some((a, b)) - } else { - debug_assert!(b_value == Generative); - Some((b, a)) - } - } -} - -impl UnifyValue for KeyKind { - type Error = NoError; - - fn unify_values(&kind1: &Self, &kind2: &Self) -> Result { - match (kind1, kind2) { - (Generative, _) => Ok(Generative), - (_, Generative) => Ok(Generative), - (Applicative, Applicative) => Ok(Applicative), - } - } -} - -impl CongruenceClosure { - pub fn new() -> CongruenceClosure { - CongruenceClosure { - map: HashMap::new(), - table: InPlaceUnificationTable::new(), - graph: Graph::new(), - } - } - - /// Manually create a new CC token. You don't normally need to do - /// this, as CC tokens are automatically created for each key when - /// we first observe it. However, if you wish to have keys that - /// make use of the `to_token` method to bypass the `key -> token` - /// map, then you can use this function to make a new-token. The - /// callback `key_op` will be invoked to create the key for the - /// fresh token (typically, it will wrap the token in some kind of - /// enum indicating an inference variable). - /// - /// **WARNING:** The new key **must** be a leaf (no successor - /// keys) or else things will not work right. This invariant is - /// not currently checked. - pub fn new_token(&mut self, key_kind: KeyKind, key_op: OP) -> Token - where - OP: FnOnce(Token) -> K, - { - let token = self.table.new_key(key_kind); - let key = key_op(token); - let node = self.graph.add_node(key); - assert_eq!(token.node(), node); - token - } - - /// Return the key for a given token - pub fn key(&self, token: Token) -> &K { - &self.graph[token.node()] - } - - /// Indicates they `key1` and `key2` are equivalent. - pub fn merge(&mut self, key1: K, key2: K) { - let token1 = self.add(key1); - let token2 = self.add(key2); - self.algorithm().merge(token1, token2); - } - - /// Indicates whether `key1` and `key2` are equivalent. - pub fn merged(&mut self, key1: K, key2: K) -> bool { - // Careful: you cannot naively remove the `add` calls - // here. The reason is because of patterns like the test - // `struct_union_no_add`. If we unify X and Y, and then unify - // F(X) and F(Z), we need to be sure to figure out that F(Y) - // == F(Z). This requires a non-trivial deduction step, so - // just checking if the arguments are congruent will fail, - // because `Y == Z` does not hold. - - debug!("merged: called({:?}, {:?})", key1, key2); - - let token1 = self.add(key1); - let token2 = self.add(key2); - self.algorithm().unioned(token1, token2) - } - - /// Returns an iterator over all keys that are known to have been - /// merged with `key`. This is a bit dubious, since the set of - /// merged keys will be dependent on what has been added, and is - /// not the full set of equivalencies that one might imagine. See the - /// test `merged_keys` for an example. - pub fn merged_keys(&mut self, key: K) -> MergedKeys { - let token = self.add(key); - MergedKeys { - graph: &self.graph, - iterator: self.table.unioned_keys(token), - } - } - - /// Add a key into the CC table, returning the corresponding - /// token. This is not part of the public API, though it could be - /// if we wanted. - fn add(&mut self, key: K) -> Token { - debug!("add(): key={:?}", key); - - let (is_new, token) = self.get_or_add(&key); - debug!("add: key={:?} is_new={:?} token={:?}", key, is_new, token); - - // if this node is already in the graph, we are done - if !is_new { - return token; - } - - // Otherwise, we want to add the 'successors' also. So, for - // example, if we are adding `Box`, the successor would - // be `Foo`. So go ahead and recursively add `Foo` if it - // doesn't already exist. - let successors: Vec<_> = key.successors().into_iter().map(|s| self.add(s)).collect(); - - debug!("add: key={:?} successors={:?}", key, successors); - - // Now we have to be a bit careful. It might be that we are - // adding `Box`, but `Foo` was already present, and in - // fact equated with `Bar`. That is, maybe we had a graph like: - // - // Box -> Bar == Foo - // - // Now we just added `Box`, but we need to equate - // `Box` and `Box`. - for successor in successors { - // get set of predecessors for each successor BEFORE we add the new node; - // this would be `Box` in the above example. - let predecessors: Vec<_> = self.algorithm().all_preds(successor); - - debug!( - "add: key={:?} successor={:?} predecessors={:?}", - key, - successor, - predecessors - ); - - // add edge from new node `Box` to its successor `Foo` - self.graph.add_edge(token.node(), successor.node(), ()); - - // Now we have to consider merging the old predecessors, - // like `Box`, with this new node `Box`. - // - // Note that in other cases it might be that no merge will - // occur. For example, if we were adding `(A1, B1)` to a - // graph like this: - // - // (A, B) -> A == A1 - // | - // v - // B - // - // In this case, the predecessor would be `(A, B)`; but we don't - // know that `B == B1`, so we can't merge that with `(A1, B1)`. - for predecessor in predecessors { - self.algorithm().maybe_merge(token, predecessor); - } - } - - token - } - - /// Gets the token for a key, if any. - fn get(&self, key: &K) -> Option { - key.to_token().or_else(|| self.map.get(key).cloned()) - } - - /// Gets the token for a key, adding one if none exists. Returns the token - /// and a boolean indicating whether it had to be added. - fn get_or_add(&mut self, key: &K) -> (bool, Token) { - if let Some(token) = self.get(key) { - return (false, token); - } - - let token = self.new_token(key.key_kind(), |_| key.clone()); - self.map.insert(key.clone(), token); - (true, token) - } - - fn algorithm(&mut self) -> Algorithm { - Algorithm { - graph: &self.graph, - table: &mut self.table, - } - } -} - -// # Walking merged keys - -pub struct MergedKeys<'cc, K: Key + 'cc> { - graph: &'cc Graph, - iterator: UnionedKeys<'cc, InPlace>, -} - -impl<'cc, K: Key> Iterator for MergedKeys<'cc, K> { - type Item = K; - - fn next(&mut self) -> Option { - self.iterator - .next() - .map(|token| self.graph[token.node()].clone()) - } -} - -// # The core algorithm - -struct Algorithm<'a, K: Key + 'a> { - graph: &'a Graph, - table: &'a mut InPlaceUnificationTable, -} - -impl<'a, K: Key> Algorithm<'a, K> { - fn merge(&mut self, u: Token, v: Token) { - debug!("merge(): u={:?} v={:?}", u, v); - - if self.unioned(u, v) { - return; - } - - let u_preds = self.all_preds(u); - let v_preds = self.all_preds(v); - - self.union(u, v); - - for &p_u in &u_preds { - for &p_v in &v_preds { - self.maybe_merge(p_u, p_v); - } - } - } - - fn all_preds(&mut self, u: Token) -> Vec { - let graph = self.graph; - self.table - .unioned_keys(u) - .flat_map(|k| graph.neighbors_directed(k.node(), Direction::Incoming)) - .map(|i| Token::from_node(i)) - .collect() - } - - fn maybe_merge(&mut self, p_u: Token, p_v: Token) { - debug!( - "maybe_merge(): p_u={:?} p_v={:?}", - self.key(p_u), - self.key(p_v) - ); - - if !self.unioned(p_u, p_v) && self.shallow_eq(p_u, p_v) && self.congruent(p_u, p_v) { - self.merge(p_u, p_v); - } - } - - // Check whether each of the successors are unioned. So if you - // have `Box` and `Box`, this is true if `X1 == X2`. (The - // result of this fn is not really meaningful unless the two nodes - // are shallow equal here.) - fn congruent(&mut self, p_u: Token, p_v: Token) -> bool { - debug_assert!(self.shallow_eq(p_u, p_v)); - debug!("congruent({:?}, {:?})", self.key(p_u), self.key(p_v)); - let succs_u = self.successors(p_u); - let succs_v = self.successors(p_v); - let r = succs_u.zip(succs_v).all(|(s_u, s_v)| { - debug!("congruent: s_u={:?} s_v={:?}", s_u, s_v); - self.unioned(s_u, s_v) - }); - debug!( - "congruent({:?}, {:?}) = {:?}", - self.key(p_u), - self.key(p_v), - r - ); - r - } - - fn key(&self, u: Token) -> &'a K { - &self.graph[u.node()] - } - - // Compare the local data, not considering successor nodes. So e.g - // `Box` and `Box` are shallow equal for any `X` and `Y`. - fn shallow_eq(&self, u: Token, v: Token) -> bool { - let r = self.key(u).shallow_eq(self.key(v)); - debug!("shallow_eq({:?}, {:?}) = {:?}", self.key(u), self.key(v), r); - r - } - - fn token_kind(&self, u: Token) -> KeyKind { - self.graph[u.node()].key_kind() - } - - fn unioned(&mut self, u: Token, v: Token) -> bool { - let r = self.table.unioned(u, v); - debug!( - "unioned(u={:?}, v={:?}) = {:?}", - self.key(u), - self.key(v), - r - ); - r - } - - fn union(&mut self, u: Token, v: Token) { - debug!("union(u={:?}, v={:?})", self.key(u), self.key(v)); - - // find the roots of `u` and `v`; if `u` and `v` have been unioned - // with anything generative, these will be generative. - let u = self.table.find(u); - let v = self.table.find(v); - - // u and v are now union'd - self.table.union(u, v); - - // if both `u` and `v` were generative, we can now propagate - // the constraint that their successors must also be the same - if self.token_kind(u) == Generative && self.token_kind(v) == Generative { - if self.shallow_eq(u, v) { - let mut succs_u = self.successors(u); - let mut succs_v = self.successors(v); - for (succ_u, succ_v) in succs_u.by_ref().zip(succs_v.by_ref()) { - // assume # of succ is equal because types are WF (asserted below) - self.merge(succ_u, succ_v); - } - debug_assert!(succs_u.next().is_none()); - debug_assert!(succs_v.next().is_none()); - } else { - // error: user asked us to union i32/u32 or Vec/Vec; - // for now just panic. - panic!( - "inconsistent conclusion: {:?} vs {:?}", - self.key(u), - self.key(v) - ); - } - } - } - - fn successors(&self, token: Token) -> impl Iterator + 'a { - self.graph - .neighbors_directed(token.node(), Direction::Outgoing) - .map(Token::from_node) - } -} diff --git a/src/cc/test.rs b/src/cc/test.rs deleted file mode 100644 index 59c527f..0000000 --- a/src/cc/test.rs +++ /dev/null @@ -1,424 +0,0 @@ -// use debug::Logger; -use cc::{CongruenceClosure, Key, KeyKind, Token}; -use self::TypeStruct::*; - -#[derive(Clone, Debug, PartialEq, Eq, Hash)] -enum TypeStruct { - // e.g., `::Item` would be `Assoc(Iterator::Item, vec![T])` - Assoc(&'static str, Vec), - - // skolemized version of in-scope generic, e.g., the `T` when checking `fn foo` - Skolem(u32), - - // inference variable (existentially quantified) - Variable(Token), - - // a nominal type applied to arguments, e.g. `i32` or `Vec` - Nominal(&'static str, Vec), -} - -type Type = Box; - -impl Key for Type { - fn to_token(&self) -> Option { - match **self { - TypeStruct::Variable(t) => Some(t), - _ => None, - } - } - - fn key_kind(&self) -> KeyKind { - match **self { - TypeStruct::Assoc(..) | - TypeStruct::Variable(_) | - TypeStruct::Skolem(_) => KeyKind::Applicative, - - TypeStruct::Nominal(..) => KeyKind::Generative, - } - } - - fn shallow_eq(&self, key: &Type) -> bool { - match (&**self, &**key) { - (&Assoc(i, _), &Assoc(j, _)) => i == j, - (&Skolem(i), &Skolem(j)) => i == j, - (&Nominal(i, _), &Nominal(j, _)) => i == j, - _ => false, - } - } - - fn successors(&self) -> Vec { - match **self { - Assoc(_, ref s) => s.clone(), - Skolem(_) => vec![], - Variable(_) => vec![], - Nominal(_, ref s) => s.clone(), - } - } -} - -fn skolem(x: u32) -> Type { - Box::new(Skolem(x)) -} - -fn iterator_item(t: Type) -> Type { - Box::new(Assoc("Iterator::Item", vec![t])) -} - -fn integer() -> Type { - Box::new(Nominal("integer", vec![])) -} - -fn vec(t: Type) -> Type { - Box::new(Nominal("Vec", vec![t])) -} - -fn inference_var<'tcx>(cc: &mut CongruenceClosure) -> Type { - let token = cc.new_token(KeyKind::Applicative, move |token| { - Box::new(TypeStruct::Variable(token)) - }); - cc.key(token).clone() -} - -#[test] -fn simple_as_it_gets() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - assert!(cc.merged(skolem(0), skolem(0))); - assert!(!cc.merged(skolem(0), skolem(1))); - assert!(cc.merged(skolem(1), skolem(1))); - assert!(cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(0)) - )); - assert!(!cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(1)) - )); - assert!(cc.merged( - iterator_item(skolem(1)), - iterator_item(skolem(1)) - )); -} - -#[test] -fn union_vars() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - cc.merge(skolem(0), skolem(1)); - assert!(cc.merged(skolem(0), skolem(1))); -} - -#[test] -fn union_iterator_item_then_test_var() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - cc.merge(skolem(0), skolem(1)); - assert!(cc.merged(skolem(0), skolem(1))); -} - -#[test] -fn union_direct() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.add(iterator_item(skolem(0))); - cc.add(iterator_item(skolem(1))); - cc.add(skolem(0)); - cc.add(skolem(1)); - - cc.merge(skolem(0), skolem(1)); - assert!(cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(1)) - )); -} - -macro_rules! indirect_test { - ($test_name:ident: $a:expr, $b:expr; $c:expr, $d:expr) => { - #[test] - fn $test_name() { - // Variant 1: call `add` explicitly - // - // This caused bugs because nodes were pre-existing. - { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.add(iterator_item(skolem(0))); - cc.add(iterator_item(skolem(2))); - cc.add(skolem(0)); - cc.add(skolem(1)); - cc.add(skolem(2)); - - cc.merge($a, $b); - cc.merge($c, $d); - assert!(cc.merged(iterator_item(skolem(0)), iterator_item(skolem(2)))); - } - - // Variant 2: never call `add` explicitly - // - // This is more how we expect library to be used in practice. - { - let mut cc2: CongruenceClosure = CongruenceClosure::new(); - cc2.merge($a, $b); - cc2.merge($c, $d); - assert!(cc2.merged(iterator_item(skolem(0)), iterator_item(skolem(2)))); - } - } - } -} - -// The indirect tests test for the case where we merge V0 and V1, and -// we merged V1 and V2, and we want to use this to conclude that -// Assoc(V0) and Assoc(V2) are merged -- but there is no node created for -// Assoc(V1). -indirect_test! { indirect_test_1: skolem(1), skolem(2); skolem(1), skolem(0) } -indirect_test! { indirect_test_2: skolem(2), skolem(1); skolem(1), skolem(0) } -indirect_test! { indirect_test_3: skolem(1), skolem(2); skolem(0), skolem(1) } -indirect_test! { indirect_test_4: skolem(2), skolem(1); skolem(0), skolem(1) } - -// Here we determine that `Assoc(V0) == Assoc(V1)` because `V0==V1`, -// but we never add nodes for `Assoc(_)`. -#[test] -fn merged_no_add() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.merge(skolem(0), skolem(1)); - - assert!(cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(1)) - )); -} - -// Here we determine that `Assoc(V0) == Assoc(V2)` because `V0==V1==V2`, -// but we never add nodes for `Assoc(_)`. -#[test] -fn merged_no_add_indirect() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.merge(skolem(0), skolem(1)); - cc.merge(skolem(1), skolem(2)); - - assert!(cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(2)) - )); -} - -// Here we determine that `Assoc(V0) == Assoc(V2)` because `V0==V1==V2`, -// but we never add nodes for `Assoc(_)`. -#[test] -fn iterator_item_not_merged() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.merge(iterator_item(skolem(0)), iterator_item(skolem(1))); - - assert!(!cc.merged(skolem(0), skolem(1))); - assert!(cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(1)) - )); -} - -// Here we show that merging `Assoc(V1) == Assoc(V2)` does NOT imply that -// `V1 == V2`. -#[test] -fn merge_fns_not_inputs() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.merge(iterator_item(skolem(0)), iterator_item(skolem(1))); - - assert!(!cc.merged(skolem(0), skolem(1))); - assert!(cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(1)) - )); -} - -#[test] -fn inf_var_union() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - let v0 = inference_var(&mut cc); - let v1 = inference_var(&mut cc); - let v2 = inference_var(&mut cc); - let iterator_item_v0 = iterator_item(v0.clone()); - let iterator_item_v1 = iterator_item(v1.clone()); - let iterator_item_v2 = iterator_item(v2.clone()); - - cc.merge(v0.clone(), v1.clone()); - - assert!(cc.map.is_empty()); // inf variables don't take up map slots - - assert!(cc.merged( - iterator_item_v0.clone(), - iterator_item_v1.clone() - )); - assert!(!cc.merged( - iterator_item_v0.clone(), - iterator_item_v2.clone() - )); - - cc.merge(iterator_item_v0.clone(), iterator_item_v2.clone()); - assert!(cc.merged( - iterator_item_v0.clone(), - iterator_item_v2.clone() - )); - assert!(cc.merged( - iterator_item_v1.clone(), - iterator_item_v2.clone() - )); - - assert_eq!(cc.map.len(), 3); // each iterator_item needs an entry -} - -#[test] -fn skolem_union_no_add() { - - // This particular pattern of unifications exploits a potentially - // subtle bug: - // - We merge `skolem(0)` and `skolem(1)` - // and then merge `Assoc(skolem(0))` and `Assoc(skolem(2))`. - // - From this we should be able to deduce that `Assoc(skolem(1)) == Assoc(skolem(2))`. - // - However, if we are not careful with accounting for - // predecessors and so forth, this fails. For example, when - // adding `Assoc(skolem(1))`, we have to consider `Assoc(skolem(0))` - // to be a predecessor of `skolem(1)`. - - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.merge(skolem(0), skolem(1)); - assert!(cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(1)) - )); - assert!(!cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(2)) - )); - - cc.merge(iterator_item(skolem(0)), iterator_item(skolem(2))); - assert!(cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(2)) - )); - assert!(cc.merged( - iterator_item(skolem(1)), - iterator_item(skolem(2)) - )); -} - -#[test] -fn merged_keys() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.merge(skolem(0), skolem(1)); - cc.merge(iterator_item(skolem(0)), iterator_item(skolem(2))); - - // Here we don't yet see `iterator_item(skolem(1))` because it has no - // corresponding node: - let keys: Vec = cc.merged_keys(iterator_item(skolem(2))).collect(); - assert_eq!( - &keys[..], - &[iterator_item(skolem(2)), iterator_item(skolem(0))] - ); - - // But of course `merged` returns true (and adds a node): - assert!(cc.merged( - iterator_item(skolem(1)), - iterator_item(skolem(2)) - )); - - // So now we see it: - let keys: Vec = cc.merged_keys(iterator_item(skolem(2))).collect(); - assert_eq!( - &keys[..], - &[ - iterator_item(skolem(2)), - iterator_item(skolem(1)), - iterator_item(skolem(0)) - ] - ); -} - -// Here we show that merging `Vec == Vec` DOES imply that -// `V1 == V2`. -#[test] -fn merge_vecs() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.merge(vec(skolem(0)), vec(skolem(1))); - - assert!(cc.merged(skolem(0), skolem(1))); - assert!(cc.merged(vec(skolem(0)), vec(skolem(1)))); - assert!(cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(1)) - )); -} - -// Here we show that merging `Vec == Vec` does NOT imply that -// `V1 == V2`. -#[test] -fn merge_vecs_of_items() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.merge(vec(iterator_item(skolem(0))), vec(iterator_item(skolem(1)))); - - assert!(!cc.merged(skolem(0), skolem(1))); - assert!(!cc.merged(vec(skolem(0)), vec(skolem(1)))); - assert!(cc.merged( - vec(iterator_item(skolem(0))), - vec(iterator_item(skolem(1))) - )); - assert!(cc.merged( - iterator_item(vec(iterator_item(skolem(0)))), - iterator_item(vec(iterator_item(skolem(1)))) - )); - assert!(cc.merged( - iterator_item(iterator_item(vec(iterator_item(skolem(0))))), - iterator_item(iterator_item(vec(iterator_item(skolem(1))))) - )); - assert!(cc.merged( - iterator_item(skolem(0)), - iterator_item(skolem(1)) - )); -} - -// Here we merge `Vec::Item` with `Int` and then merge that later -// with an inference variable, and show that we concluded that the -// variable is (indeed) `Int`. -#[test] -fn merge_iterator_item_generative() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - cc.merge(iterator_item(vec(integer())), integer()); - let v0 = inference_var(&mut cc); - cc.merge(iterator_item(vec(integer())), v0.clone()); - assert!(cc.merged(v0.clone(), integer())); - assert!(cc.merged( - vec(iterator_item(vec(integer()))), - vec(integer()) - )); -} - -#[test] -fn merge_ripple() { - let mut cc: CongruenceClosure = CongruenceClosure::new(); - - cc.merge(iterator_item(skolem(1)), vec(skolem(0))); - cc.merge(iterator_item(skolem(2)), vec(integer())); - - assert!(!cc.merged( - iterator_item(skolem(1)), - iterator_item(skolem(2)) - )); - - println!("------------------------------"); - cc.merge(skolem(0), integer()); - - println!("------------------------------"); - assert!(cc.merged( - iterator_item(skolem(1)), - iterator_item(skolem(2)) - )); - assert!(cc.merged( - iterator_item(iterator_item(skolem(1))), - iterator_item(iterator_item(skolem(2))) - )); -} diff --git a/src/lib.rs b/src/lib.rs index 25557c9..233ecf9 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -8,13 +8,9 @@ // option. This file may not be copied, modified, or distributed // except according to those terms. -//! An implementation of union-find and (optionally) -//! congruence-closure. See the `unify` and `cc` modules for more -//! details. Note that congruence-closure requires you to opt-in to -//! the feature "congruence-closure". +//! An implementation of union-find. See the `unify` module for more +//! details. -// The CC code uses `impl Trait` -#![cfg_attr(feature = "congruence-closure", feature(conservative_impl_trait))] #![cfg_attr(feature = "bench", feature(test))] #[macro_use] @@ -23,9 +19,5 @@ extern crate log; #[cfg(feature = "persistent")] extern crate dogged; -#[cfg(feature = "congruence-closure")] -extern crate petgraph; - pub mod snapshot_vec; -pub mod cc; pub mod unify; diff --git a/src/unify/mod.rs b/src/unify/mod.rs index b01d16a..257aa65 100644 --- a/src/unify/mod.rs +++ b/src/unify/mod.rs @@ -158,8 +158,6 @@ pub struct NoError { pub struct VarValue { // FIXME pub parent: K, // if equal to self, this is a root value: K::Value, // value assigned (only relevant to root) - child: K, // if equal to self, no child (relevant to both root/redirect) - sibling: K, // if equal to self, no sibling (only relevant to redirect) rank: u32, // max depth (only relevant to root) } @@ -199,28 +197,23 @@ pub struct Snapshot { impl VarValue { fn new_var(key: K, value: K::Value) -> VarValue { - VarValue::new(key, value, key, key, 0) + VarValue::new(key, value, 0) } - fn new(parent: K, value: K::Value, child: K, sibling: K, rank: u32) -> VarValue { + fn new(parent: K, value: K::Value, rank: u32) -> VarValue { VarValue { parent: parent, // this is a root value: value, - child: child, - sibling: sibling, rank: rank, } } - fn redirect(&mut self, to: K, sibling: K) { - assert_eq!(self.parent, self.sibling); // ...since this used to be a root + fn redirect(&mut self, to: K) { self.parent = to; - self.sibling = sibling; } - fn root(&mut self, rank: u32, child: K, value: K::Value) { + fn root(&mut self, rank: u32, value: K::Value) { self.rank = rank; - self.child = child; self.value = value; } @@ -228,14 +221,6 @@ impl VarValue { self.if_not_self(self.parent, self_key) } - fn child(&self, self_key: K) -> Option { - self.if_not_self(self.child, self_key) - } - - fn sibling(&self, self_key: K) -> Option { - self.if_not_self(self.sibling, self_key) - } - fn if_not_self(&self, key: K, self_key: K) -> Option { if key == self_key { None @@ -289,19 +274,6 @@ impl UnificationTable { key } - /// Returns an iterator over all keys unioned with `key`. - pub fn unioned_keys(&mut self, key: K1) -> UnionedKeys - where - K1: Into, - { - let key = key.into(); - let root_key = self.get_root_key(key); - UnionedKeys { - table: self, - stack: vec![root_key], - } - } - /// Returns the number of keys created so far. pub fn len(&self) -> usize { self.values.len() @@ -408,90 +380,15 @@ impl UnificationTable { new_root_key: S::Key, new_value: S::Value, ) { - let sibling = self.value(new_root_key) - .child(new_root_key) - .unwrap_or(old_root_key); self.update_value(old_root_key, |old_root_value| { - old_root_value.redirect(new_root_key, sibling); + old_root_value.redirect(new_root_key); }); self.update_value(new_root_key, |new_root_value| { - new_root_value.root(new_rank, old_root_key, new_value); + new_root_value.root(new_rank, new_value); }); } } -/// Iterator over keys that have been unioned together. -/// -/// Returned by the `unioned_keys` method. -pub struct UnionedKeys<'a, S> - where - S: UnificationStore + 'a, - S::Key: 'a, - S::Value: 'a, -{ - table: &'a mut UnificationTable, - stack: Vec, -} - -impl<'a, S> UnionedKeys<'a, S> - where - S: UnificationStore + 'a, - S::Key: 'a, - S::Value: 'a, -{ - fn var_value(&self, key: S::Key) -> VarValue { - self.table.value(key).clone() - } -} - -impl<'a, S: 'a> Iterator for UnionedKeys<'a, S> - where - S: UnificationStore + 'a, - S::Key: 'a, - S::Value: 'a, -{ - type Item = S::Key; - - fn next(&mut self) -> Option { - let key = match self.stack.last() { - Some(k) => *k, - None => { - return None; - } - }; - - let vv = self.var_value(key); - - match vv.child(key) { - Some(child_key) => { - self.stack.push(child_key); - } - - None => { - // No child, push a sibling for the current node. If - // current node has no siblings, start popping - // ancestors until we find an aunt or uncle or - // something to push. Note that we have the invariant - // that for every node N that we reach by popping - // items off of the stack, we have already visited all - // children of N. - while let Some(ancestor_key) = self.stack.pop() { - let ancestor_vv = self.var_value(ancestor_key); - match ancestor_vv.sibling(ancestor_key) { - Some(sibling) => { - self.stack.push(sibling); - break; - } - None => {} - } - } - } - } - - Some(key) - } -} - /// //////////////////////////////////////////////////////////////////////// /// Public API diff --git a/src/unify/tests.rs b/src/unify/tests.rs index e4cf0bc..481fd44 100644 --- a/src/unify/tests.rs +++ b/src/unify/tests.rs @@ -16,7 +16,6 @@ extern crate test; #[cfg(feature = "bench")] use self::test::Bencher; -use std::collections::HashSet; use std::cmp; use unify::{NoError, InPlace, InPlaceUnificationTable, UnifyKey, EqUnifyValue, UnifyValue}; use unify::{UnificationStore, UnificationTable}; @@ -232,34 +231,6 @@ fn even_odd() { } } -#[test] -fn even_odd_iter() { - all_modes! { - S for UnitKey => { - let mut ut: UnificationTable = UnificationTable::new(); - let mut keys = Vec::new(); - const MAX: usize = 1 << 10; - - for i in 0..MAX { - let key = ut.new_key(()); - keys.push(key); - - if i >= 2 { - ut.union(key, keys[i - 2]); - } - } - - let even_keys: HashSet = ut.unioned_keys(keys[22]).collect(); - - assert_eq!(even_keys.len(), MAX / 2); - - for key in even_keys { - assert!((key.0 & 1) == 0); - } - } - } -} - #[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)] struct IntKey(u32);