]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/TEMPI
Initial revision
[helm.git] / helm / interface / TEMPI
diff --git a/helm/interface/TEMPI b/helm/interface/TEMPI
new file mode 100644 (file)
index 0000000..dc2bc85
--- /dev/null
@@ -0,0 +1,214 @@
+prima di UriManager.ml:
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m50.266s
+   user        0m44.160s
+   sys 0m0.700s
+
+dopo UriManager.ml, ma prima di passare da = a ==:
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m51.388s
+   user        0m45.430s
+   sys 0m0.530s
+
+dopo UriManager.ml e popo il passaggio (parziale?) da = a ==:
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m50.767s
+   user        0m44.750s
+   sys 0m0.510s
+
+dopo il passaggio alla cache che usa ancora =:
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m50.646s
+   user        0m44.680s
+   sys 0m0.530s
+
+dopo il passaggio alla cache con utilizzo di ==:
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m50.861s
+   user        0m45.030s
+   sys 0m0.500s
+
+con funzione di hashing costante ;-(
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m51.442s
+   user        0m45.440s
+   sys 0m0.530s
+
+con implementazione isomorfa all'albero delle uri:
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m54.081s
+   user        0m47.590s
+   sys 0m0.780s
+
+con implementazione con doppio RB-albero:
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m52.504s
+   user        0m46.120s
+   sys 0m0.720s
+
+con implementazione semplice, gestite anche le uri delle var:
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m51.850s
+   user        0m46.060s
+   sys 0m0.530s
+
+con implementazione con doppio RB-albero, gestite anche le uri delle var:
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m51.495s
+   user        0m45.660s
+   sys 0m0.540s
+
+=========================================================
+
+con implementazione con doppio RB-albero, gestite anche le uri delle var
+e spostata nell'uri-manager is_prefix:
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m50.465s
+   user        0m45.710s
+   sys 0m0.590s
+
+con implementazione semplice (e tutto il resto):
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m49.710s
+   user        0m43.850s
+   sys 0m0.500s
+
+con implementazione banale (e tutto il resto):
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m49.289s
+   user        0m44.840s
+   sys 0m0.570s
+
+con implementazione banale SOLO PARSING ;-)
+
+ [ABCI]* (terza passata, uguale alla seconda):
+
+   real        0m48.395s
+   user        0m42.830s
+   sys 0m0.850s
+
+=========================================================
+
+con implementazione con doppio RB-albero, gestite anche le uri delle var
+e spostata nell'uri-manager is_prefix:
+
+ REAL (prima passata, dopo un sync):
+
+   real        10m58.033s
+   user        10m37.690s
+   sys 0m2.570s
+
+con implementazione semplice (e tutto il resto):
+
+ REAL (prima passata, dopo un sync):
+
+   real        10m31.035s
+   user        10m9.350s
+   sys 0m3.230s
+
+con implementazione banale (e tutto il resto):
+
+ REAL (prima passata, dopo un sync):
+
+   real        11m4.026s
+   user        10m43.930s
+   sys 0m3.070s
+
+=================================================
+
+con implementazione banale, SOLO PARSING di tutto:
+
+   real        6m54.336s
+   user        6m13.850s
+   sys 0m6.580s
+
+con implementazione banale, anche typechecking di tutto:
+
+   real        20m17.739s
+   user        19m14.740s
+   sys 0m8.550s
+
+con implementazione semplice, anche typechecking di tutto:
+
+   real        19m36.079s
+   user        18m36.480s
+   sys 0m7.760s
+
+con implementazione con doppio RB-albero, anche typechecking di tutto:
+
+   real        17m30.423s
+   user        16m30.840s
+   sys 0m6.170s
+
+***************************************************************************
+                         APPLICATA EURISTICA
+***************************************************************************
+
+con implementazione con doppio RB-albero, anche typechecking di tutto
+(universita') ????????:
+
+real    5m37.805s
+user    5m1.640s
+sys     0m5.010s
+
+tutto (ma a casa):
+
+real   7m36.663s
+user   6m52.220s
+sys    0m5.860s
+
+
+solo REAL:
+
+real   2m52.860s
+user   2m41.050s
+sys    0m2.820s
+
+==========================================================================
+
+tutto (ma a casa) dopo eliminazione buri:
+
+real   7m52.773s
+user   6m52.110s
+sys    0m7.130s
+
+"solo parsing" di tutto dopo eliminazione buri:
+
+real   7m8.379s
+user   6m15.250s
+sys    0m6.700s
+
+===========================================================================
+
+TUTTO ALL'UNIVERSITA' CON EURISTICA MA SENZA UNIVERSI:
+
+real    5m47.920s
+user    5m14.600s
+sys     0m5.010s
+