English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
compiler bug?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2006-05-18 (19:30)
From: Jacques Carette <carette@m...>
Subject: Re: [Caml-list] compiler bug?
Xavier Leroy wrote:

>Clearly, you're not the guy who would have to support both compilers :-)
Clearly :-).  [Although I've done my time maintaining ancient software 
used by ~2 million users, so you only get so much sympathy from me ;-) ]

>Actually, George and Appel found that compilation times with their
>approach were almost reasonable (e.g. a few minutes instead of a few
>seconds for a standard compiler), but they had to use a commercial ILP
>solver.  If only there were *really good* ILP and SAT solvers under free
In Computer Algebra, people use Groebner bases all the time.  They have 
doubly-exponential worst-case complexity -- but seem to work rather well 
in practice.  So I have stopped paying attention to worst-case; average 
case, when available, does matter a lot more.

For ILP, I have found
to be quite informative about current sources of "free" ILP solvers.  Of 
particular interest are:
GLPK: http://www.gnu.org/software/glpk/glpk.html
lp_solve: http://groups.yahoo.com/group/lp_solve/ 

For SAT, things are weirder.  Of course there is
as well as SVC
and CVC Lite
(these last 2 for SMT rather than pure SAT) which are under compatible 
licenses.  But at
there are a number of additional candidates.

Of course, getting an agreement with SRI to use Yices 
(http://fm.csl.sri.com/yices/) would go a long way towards satisfying 
the "really good" requirement...