]> matita.cs.unibo.it Git - helm.git/commit
use of discrimination trees instead of path indexes, for a little
authorAlberto Griggio <griggio@fbk.eu>
Wed, 22 Jun 2005 09:07:45 +0000 (09:07 +0000)
committerAlberto Griggio <griggio@fbk.eu>
Wed, 22 Jun 2005 09:07:45 +0000 (09:07 +0000)
commit969fb8763a6d4afb88aef1eaa4a4d1ce7d626264
treeb338b760c091964fa0a7eba1c437b5dbcaf939cc
parent7e0973fe9cb31ea68d8a046766f64fc978fbcdf6
use of discrimination trees instead of path indexes, for a little
performance gain
helm/ocaml/paramodulation/Makefile
helm/ocaml/paramodulation/discrimination_tree.ml
helm/ocaml/paramodulation/indexing.ml
helm/ocaml/paramodulation/path_indexing.ml
helm/ocaml/paramodulation/test_indexing.ml