Mantis: A Fast, Small, and Exact Large-Scale Sequence-Search Index