Hi Peter, This is awesome!
I would much prefer to use an external, unmodified version of STP, as long as it is properly packaged so that it is possible to write sane instructions about how to install and build it. This also assumes that STP is stable, or has some stable tags. The main reason I sucked STP in to the build is that it is very important to me that KLEE support objdir != srcdir builds, and the simplest way to do that was to integrate it with the LLVM makefiles. However, if we just support STP as a configure time library, then that also solves this problem. Please keep me in the loop w.r.t. any discussion with the STP developers that will make it possible to do this. Also, have you worked at all on the necessary KLEE changes for this (probably as simple as ripping out the internal STP and adding a configure option, I imagine). It should be possible for us to support both options, initially, which is nice for comparing the performance of them side by side. Do you have any hard numbers that show that the new STP is better, or by how much? - Daniel On Thu, Apr 8, 2010 at 1:17 PM, Peter Collingbourne <peter at pcc.me.uk> wrote: > Hello, > > The latest version of STP is a significant improvement over the older > version that we are using. ?For example, it can use a much more > efficient SAT solver called CryptoMiniSat. > > I think it would be ideal to be able to use an external unmodified > installation of STP. ?That way we can easily integrate new versions > of STP as they are developed. ?I am working with the STP developers > to try to get STP into a state where Klee can use it unmodified. > > I am undecided as to whether we should continue to include our own > version of STP with Klee. ?I imagine this would make things easier > for users but OTOH it could encourage divergence from upstream STP > making it harder to integrate new versions. > > The recent changes to Klee to integrate STP into the LLVM build > system may make this harder to do, due to certain paths and filenames > having changed. > > I have had success integrating a recent version of STP and having > it pass the tests. ?I am attaching a patch which replaces the > in-tree version of STP with an out-of-tree version installed at a > path specified at configure time (please note the instructions for > applying the patch, supplied inline). > > If you want to make this work please note that it depends on a patch > to STP [1] which has not yet been applied. > > [1] http://groups.google.com/group/stp-users/t/3eaeac520cbd5978 > > Thanks, > -- > Peter > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > >
