]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6b46ffb) | patch
Added cache to lpo implementation.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 16 May 2012 23:32:12 +0000 (23:32 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 16 May 2012 23:32:12 +0000 (23:32 +0000)
commit7684ad8a8fec35563be35c1d5c797dfab83c1e3f
tree85a3072fef61798e3dcfdc028949935bd88766cbtree | snapshot
parent6b46ffbedfb4d105e48319f4bed26fb3f76f17d3commit | diff
Added cache to lpo implementation.
The current cache is based on imperative lists.
Can it be improved with smarter data structures (e.g. HashTables?)
matita/components/ng_paramodulation/orderings.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.