On Thu, Apr 8, 2010 at 6:42 PM, Daniel Dunbar <daniel at zuster.org> wrote: > 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).
Um, ignore this question, since you obviously attached a patch for exactly this! :) It would be cool if we could tweak the patch to use the internal STP if --with-stp isn't specified, then we could go ahead and put it in trunk. - Daniel > 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 >> >> >
