Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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: -- (:)
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:

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 
( would go a long way towards satisfying 
the "really good" requirement...