Expose a C api

[Storyyeller]

Hi, I am working on adding Rust bindings to Cryptominisat, and as part of that, I needed to wrap the useful functions in C. I think exposing a C api would be useful for FFI in general, because C++ has no stable ABI, while C is a lingua franca that can work with nearly any language.

Here are the wrappers I wrote. Is this something you would be interested in upstreaming? https://github.com/Storyyeller/cryptominisat/blob/c05907873eb67b9385ae169c863fdc89b251b5ea/src/cwrapper.cpp

(I'm interested in upstreaming the Rust part too, but I haven't found any way to make the repository layout compatible with cargo package yet)

[msoos]

Hey, yep, that sounds great! I don't know how that works with Lit, as you seem to be using it but Lit is a C++ class. However, if you make a merge request, we can add it. Some changes:

• it needs to be cryptominisat5_c.h or similar so it doesn't clash :)
• we need a very simple example C file that uses this, and add it to README.markdown. Just add one into tests/ and I'll copy it to the README.markdown
• I'll add an automated test using the example .c file above so we know it compiles and runs on every push. You don't need to hook it up into the test infra (though if you do, great, but no need)

Great work :) Looking forward to the merge request!

Mate

[Storyyeller]

Lit just contains a u32, and I didn't see any virtual functions, so I assumed it was C compatible to treat it as just a struct {u32 }. Is there anything special you have to do to gaurentee layout?

Note: The same also apples to lbool, which is just a u8.

[msoos]

No, nothing special. If it compiles and a simple C program can be written to prove it works, I'm good with it :) I'm not an expert at bindings. Thanks again and looking forward to the merge request!

Cheers!

[Storyyeller]

I already wrote Rust code to test it. I'll try porting that over to C.

On Sun, Jul 17, 2016 at 8:39 AM, Mate Soos notifications@github.com wrote:

No, nothing special. If it compiles and a simple C program can be written to prove it works, I'm good with it :) I'm not an expert at bindings. Thanks again and looking forward to the merge request!

Cheers!

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/354#issuecomment-233188025, or mute the thread https://github.com/notifications/unsubscribe-auth/AA9A-r3homeKVPhKXGomNsad5l5TqG1Yks5qWky4gaJpZM4JOPWX .

[msoos]

That'd be great. But maybe something trivial is good, too, like:

#include "cryptominisat5_c.h"

int main()
{
add_vars();
add_clause();
solve();
//check solution
return 0;
}

I just literally need it to compile and run so I know that the C binding is working with a C compiler :)

[Storyyeller]

One thing I'm not sure about is how to write a header that works in both C++ and C. Any ideas?

[msoos]

No need :) Just write one that works in C, e.g. "cryptominisat5_c.h" and it doesn't need to have all the functionality that the C++ header does. I suggest adding the following:

• new_var(s)
• add_clause
• solve()
• get_model
• get_conflict
• set_num_threads()
• simplify()

That's all that's needed. Last two are optional, but useful and simple :)

[Storyyeller]

Here: https://github.com/msoos/cryptominisat/pull/357

I'm not sure how to make it run as a test, but I created a c file (ctest.c) with example usage which includes the header and successfully compiles.

[msoos]

OK, merged, fixed, things should now build fine on Travis CI. Thanks a ton for this!