Cannot find a way to free GPU resources

[msoos]

Hi Nicolas,

First of all, thanks for the library, it's great! Unfortunately, I can't seem to find a way to free the memory that is used by makeGpuClauseSharerPtr, and to delete the associated GPU resources (so I can create another solver, etc). Did I overlook something? I need to be able to create/delete these as needed, since many people use the solver like:

for(int i = 0; i < 10; i++) {
  SATSolver mysolver;
  mysolver.set_num_threads(4);
  //do some kind of solving with a CNF that's parametrized by "i"
}

So being able to create/delete solvers is important. Some of my own systems use the solver this way :)

Thanks for looking into this and thanks again for this awesome work,

Mate

[nicolasprevot]

Hi When the destructor of the object returned is called, it should invoke more destructors, which should free the memory.

Thanks for trying to it from cryptominisat! Nicolas

[msoos]

Hi!

Thanks for the quick answer. I am a bit confused, though. GpuClauseSharer doesn't seem to have a virtual destructor in GpuClauseSharer.h so I don't understand how it would call the right destructor. Or is that not needed? I thought it's needed for the destructor to be correctly called in these cases, no?

Thanks,

Mate

[nicolasprevot]

Hi

Indeed, it was missing a virtual destructor, thanks for noticing this! I've pushed a change to add it. (I didn't notice it was an issue because so far, I just exit once the gpu run is finished. But obviously, if someone uses it from a library, it's different) Maybe I should try running valgrind to detect more memory leaks, although I think cuda makes it harder. Thanks for the help

Nicolas

[msoos]

Thanks so much for fixing! Glad that I could help :) I usually use clang with ASAN, it's faster and in my experience slightly better (can detect e.g. unsigned integer overflow which is undefined, float issues, etc). Thanks again for looking into this and fixing,

Mate