note description: "Objects that represent tries, i.e. a ceratin kind of retrieval tree" author: "JSO" date: "Januray 28, 04" class TRIE[G] create make feature {NONE} -- Initialization make -- create an empty TRIE do create ll.make height := 1 ensure is_empty height = 1 end feature -- Status report contains (seq: LINKED_LIST[G]): BOOLEAN -- Returns true if the trie contains the particular sequence local seq_clone: LINKED_LIST[G] do if seq.is_empty then Result := terminal else seq_clone := seq.twin from seq_clone.start ll.start until -- ll.after or ll.item.element.is_equal(seq_clone.item) ll.after or equal(ll.item.element, seq_clone.item) loop ll.forth end seq_clone.remove if ll.after then Result := false elseif seq_clone.is_empty and ll.item.terminal then Result := true else Result := ll.item.contains(seq_clone) end restore_ll_cursor end ensure count_unchanged: count = old count unique_containment: Result implies exists1 (agent same_list (seq,?)) same_terminal: terminal = old terminal -- same_element: equal(element, old clone(element)) -- -- perhaps these are unncessary seq_unchanged: seq.is_equal(old seq.twin) values_in_seq_unchanged: deep_equal (seq, old seq.deep_twin) trie_unchanged: deep_equal (Current, old Current.deep_twin) end count: INTEGER -- The number of sequences in the trie local list: LINKED_LIST[TRIE[G]] t : TRIE[G] do list := ll.twin create t.make if terminal then Result := 1 end from list.start until list.after loop t := list.item -- recursive call Result := Result + t.count list.forth end ensure same_height: height = old height same_terminal: terminal = old terminal -- same_element: equal(element, old clone(element)) -- -- perhaps unnecesary -- same_element: equal(element, old clone(element)) trie_unchanged: deep_equal (Current, old Current.deep_twin) end is_empty: BOOLEAN -- is the trie empty? do Result := count = 0 ensure Result = (count = 0) trie_unchanged: deep_equal (Current, old current.deep_twin) count = old count height = old height end height: INTEGER -- The length of the longest path from the root of the trie to any leaf node -- The height of an empty trie is 1 -- space inefficient; better to implement as a routine feature -- Element change insert (seq: LINKED_LIST[G]) -- Insert `seq' in the trie -- Assumes that the sequence is not already in the trie require not contains (seq) do insert_recursive(seq) ensure contains (seq) exists1 (agent same_list(seq, ?)) count_increased: count = old count + 1 not_empty: not is_empty height_updated: height = ((seq.count +1).max (height)) -- next two unnecessary? height_updated1: (seq.count >= old height) implies (height = seq.count + 1) height_same: (seq.count < old height) = (height = old height) each_sequence_is_unique: for_all(agent unique_entry(?)) end feature {TRIE} -- Implementation element change set_element (el: G) -- Change the element represented by this trie do element := el end set_terminal -- This trie is the valid end of a sequence do terminal := True end set_non_terminal -- This trie is not the valid end of a sequence do terminal := False end feature -- Quantifiers for_all (test: FUNCTION[LINKED_LIST[G], BOOLEAN]): BOOLEAN -- does `test' hold for all sequences in the trie? require test_not_void: test /= Void do Result := hold_count (test) = count ensure Result = ( hold_count (test) = count) end hold_count (test: FUNCTION [LINKED_LIST[G], BOOLEAN]): INTEGER -- Number of times `test' holds in the TRIE require test_not_void: test /= Void local seq: LINKED_LIST[G] do -- debug print("Enter hold_count: " + "%N") end create seq.make Result := hold_count_recursive(test, seq) ensure Result >= 0 end exists (test: FUNCTION[LINKED_LIST[G], BOOLEAN]): BOOLEAN -- Does `test' hold for at least one of the sequences in the trie? require test_not_void: test /= Void do Result := hold_count (test) >= 1 ensure Result =( hold_count (test) >= 1) end exists1 (test: FUNCTION[LINKED_LIST[G], BOOLEAN]): BOOLEAN -- Does `test' hold for at least one of the sequences in the trie? require test_not_void: test /= Void do Result := hold_count (test) = 1 ensure Result = ( hold_count (test) = 1) end feature {TRIE, ES_TEST} -- Implementation element: G terminal: BOOLEAN ll: LINKED_LIST[TRIE[G]] -- Hidden implementation (a trie is a linked list of sub-tries) feature {TRIE} -- Implementation restore_ll_cursor -- restore cursor to what it originally was -- so that `Current' is unchanged do if ll.is_empty then ll.finish else ll.start end end insert_recursive(seq: LINKED_LIST[G]) -- Traverses the tree structure. If a common prefix is found, it follows the -- corresponding link; otherwise it adds a new path require -- not seq.is_empty not contains (seq) local t: TRIE[G] seq_clone: LINKED_LIST[G] do if seq.is_empty then set_terminal else height := ((seq.count +1).max (height)) create t.make seq_clone := seq.twin -- Find next insertion position from ll.start until ll.after or ll.item.element.is_equal(seq_clone.first) loop ll.forth end if ll.after then -- Not a substring; create a new branch t.set_element (seq_clone.first) ll.extend (t) ll.back -- set index to point at new item end --- Remove first element of `seq' seq_clone.start seq_clone.remove if seq_clone.is_empty then ll.item.set_terminal else ll.item.insert_recursive(seq_clone) end end ensure height = ((seq.count +1).max (height)) terminal implies count = old count + 1 end hold_count_recursive(test: FUNCTION [LINKED_LIST[G], BOOLEAN]; seq: LINKED_LIST[G]): INTEGER -- apply `test' to `seq' if `terminal' holds local ll_clone: like ll do if terminal and seq.is_empty and test.item([seq]) then -- null or Void TRIE Result := 1 end ll_clone := ll.twin from ll_clone.start until ll_clone.after loop seq.extend ( ll_clone.item.element) if ll_clone.item.terminal and then test.item([seq]) then Result := Result + 1 end if not ll_clone.item.is_empty then Result := Result + ll_clone.item.hold_count_recursive (test, seq) end seq.finish seq.remove ll_clone.forth end end feature -- Agent tests unique_entry (l: LINKED_LIST[G]): BOOLEAN do Result := exists1 (agent same_list(l,?)) end same_list (l1,l2: LINKED_LIST[G]): BOOLEAN do Result := equal(l1,l2) end invariant count_non_negative: count >= 0 empty_if_no_element: is_empty = (count = 0) height >= 1 -- each_sequence_is_unique: for_all(agent unique_entry(?)) end -- class TRIE