Add 'Send' to glucose

[ChrisJefferson]

This PR adds 'Send' to glucose, so it can be sent between threads, and add a test. This could probably be added to other solvers too, I'd have to quickly skim their code to check for thread-local stuff, but I don't expect to find any.

Adding 'Send' lets you put a solver in a Mutex and pass it between threads. I want to do this as I want to make a threadpool of solvers, and this makes things much easier when I do that :)

if you are generally happy with this, I'm happy to go and add similar code to other solvers (I only added it to the solver I'm currently using).

(I'll write some more here about my understanding of multi-threading in Rust, just in case you haven't done much multithreading in Rust. If you have, you can skip this :) )

There are two concepts in Rust used in multi-threading:

Send: It's safe to send this between threads

Sync: It's safe to const-access this from two threads

I'm confident that solvers are Send -- in C++ it is fine to take a glucose solver, pass it to another thread, and solve on that other thread. The only reason this wouldn't work is if there were any thread-local variables.

It might be fine to be Sync, but that's much trickier, it would involve carefully check if all the methods we treat as 'const' (like get solution, get number of nodes, etc) don't modify any data-structures. Checking that would require a lot more care. However, I also don't think it's particularly useful anyway -- we definately can't use the same solver to solve in two threads at once, and I don't think being able to read the result from two threads would be particularly useful anyway.

[chrjabs]

Looks good to me. I don't have much experience with multithreaded programming in Rust, but I agree that all solvers should be Send. Would you mind going through and doing this for all solvers?

[ChrisJefferson]

Now updated for all solvers. I couldn't test ipasir, as it doesn't have an implementation, and I tested different solvers a bit differently, depending on the supported functionality. Every test at least builds the model in one thread, and solves it in another.

[chrjabs]

Looks good to me so far. Did you intentionally not do CaDiCaL?

[ChrisJefferson]

Nope, just messed my grepping for solver implementations :)

[chrjabs]

Great, thanks