Leander Tentrup comments

Results 6 comments of


                                            Leander Tentrup

static linking

Probably due to the dependency on cryptominisat. It's a C++ library so Rust flags won't affect the way it's built. Other than that, everything should build statically.

Thanks for using CMS! What was the issue using the newest CMS, do you have some examples perhaps?

@msoos Thanks for providing CMS! I have never had problems using your solver and CAQE would be quite less competitive without CMS. @vale1410 Thank you for the examples, I do...

Thanks for using CMS! What was the issue using the newest CMS, do you have some examples perhaps?

@msoos I am not opposed to using the official rust bindings. The only reason that I use a fork is that I really want to link statically against CMS and...

Thanks for using CMS! What was the issue using the newest CMS, do you have some examples perhaps?

@msoos I think a static-lib variant could be realized using cargo "features" (https://doc.rust-lang.org/cargo/reference/manifest.html#the-features-section) which are basically compile-time flags. Getting rid of the double-git setup is probably incompatible with this change:...

How to extract Herbrand functions?

That’s not possible in the current version of caqe

how to use preprocessor?

From the code it seems that the blower binary has to be in the working dir: https://github.com/ltentrup/caqe/blob/643a2e9db61836ca06ac5a773307404fc6fd6ced/src/preprocessor.rs#L85 If I remember correctly, you might need to apply a patch to bloqqer...