Hi Peter, Patch looks excellent, please commit!
One question, what does this do: + vc_setInterfaceFlags(vc, EXPRDELETE, 0); ? It reads like it disable expression freeing, which sounds scary for memory use. Can you add a comment if it is something subtle? Would it make sense to push the STP guys to make a stable release, which we could recommend to users? That would be one step in the direction of killing off our internal STP copy. - Daniel On Fri, Jul 9, 2010 at 8:24 AM, Peter Collingbourne <peter at pcc.me.uk> wrote: > Hi Daniel, > > Sorry for the slow response. > > On Thu, Apr 08, 2010 at 06:45:58PM -0700, Daniel Dunbar wrote: >> 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. > > I finally got round to doing this -- please see the attached patch. > I'll commit this if OK. > >> > 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? > > On one particular benchmark, we experienced query runtimes of several > hours with the old STP, and approx 12 minutes with the new STP (dual > 2.0GHz machine, using CryptoMiniSat 2). ?I've attached a copy of the > problematic query. ?If you would like a copy of the benchmark itself > (it has a dependency on another library) I can try to do that. > > Thanks, > -- > Peter >
