C api minor issues

[recoules]

Some enum constants are defined in btoropt.h (e.g. BTOR_SAT_ENGINE_CADICAL) but are not exported in btortypes.h nor boolector.h (they are still documented there). Thus, I think the enum definition part should be moved to btortypes.h so user can see them.

Also, I found a little disturbing that constant constructors do not always follow the same convention:

• boolector_consth and boolector_constd have sort before the value
• boolector_unsigned_int and boolector_int have sort after the value

(Yet, I do not expect you to break the api for such minor issue but, who knows...)

Finally, as a suggestion, I am wondering if there could be a set of functions that would work directly on bitvector:

BoolectorNode *boolector_bv (Btor *btor, BoolectorBv *bv);
BoolectorBv *boolector_bv_raw_assignment(Btor *btor, BoolectorNode *node);
void boolector_release_bv(Btor *btor, BoolectorBv *bv);

I think it would ease the reinjection of model values into the formula.

[aytey]

My guess would that, if you want to set options (e.g., you want to set BTOR_SAT_ENGINE_CADICAL), then you need to #include btoropt.h.

The C API Examples even include an example where it shows including btoropt.h.

I agree that boolector_consth/boolector_constd seem inconsistent if you compare them with boolector_unsigned_int/boolector_int. I believe that Bitwuzla might have an updated API, so maybe this can be fixed there (which saves breaking the current API).

As for your three API suggestions, I am not entirely sure what you want them to do -- what type do you expect BoolectorBv to be?

[recoules]

My guess would that, if you want to set options (e.g., you want to set BTOR_SAT_ENGINE_CADICAL), then you need to #include btoropt.h.

Correct me if I am wrong but the problem is that btoropt.h is not installed/exported (by default at least). Moreover, it actually includes some other files that are not installed too. I suggested to move just the enum types into btortypes.h̀ to avoid cascading effect of include/install.

The C API Examples even include an example where it shows including btoropt.h.

I guess it works because it is compiled in the build system. It is not a problem for me but could be for other users.

I believe that Bitwuzla might have an updated API, so maybe this can be fixed there (which saves breaking the current API).

Since I discovered its existence (not so long ago yet), I am looking forward to hear news about its release. Will it share a similar architecture with boolector or is it totally distinct project?

As for your three API suggestions, I am not entirely sure what you want them to do -- what type do you expect BoolectorBv to be?

In fact, the type of BoolectorBv do not really matter (opaque). The goal here is to bypass the conversion internal bv -> string + size -> internal bv (because I imagine constants are of type bv). Would it have a performance impact? Probably not but it actually could not be worse, is it?

[aytey]

My guess would that, if you want to set options (e.g., you want to set BTOR_SAT_ENGINE_CADICAL), then you need to #include btoropt.h.

Correct me if I am wrong but the problem is that btoropt.h is not installed/exported (by default at least). Moreover, it actually includes some other files that are not installed too. I suggested to move just the enum types into btortypes.h̀ to avoid cascading effect of include/install.

Sorry, yes, you're totally correct! ~See: https://github.com/Boolector/boolector/pull/141~

edit: my PR was rubbish, I closed it.

Will it share a similar architecture with boolector

Similar architecture, but, importantly, I believe the maintainers are willing to make "breaking changes" for the new API.

In fact, the type of BoolectorBv do not really matter (opaque).

It is private currently (I believe), but take a look at btor_model_get_bv.

[aniemetz]

Some enum constants are defined in btoropt.h (e.g. BTOR_SAT_ENGINE_CADICAL) but are not exported in btortypes.h nor boolector.h (they are still documented there). Thus, I think the enum definition part should be moved to btortypes.h so user can see them.

Hm, that must have slipped through. In theory, all enums that are needed in the API should be defined in btortypes.h, so if there are some missing, that's an error on our part. We'll double check.

Also, I found a little disturbing that constant constructors do not always follow the same convention:

* `boolector_consth` and `boolector_constd` have `sort` before the value

* `boolector_unsigned_int` and `boolector_int` have `sort` after the value

That's historical. The reason being that we didn't want to break the API for the functions that existed even before sorts were introduced (originally, it was only bit-widths). And later we always followed the pattern "sorts first". I agree, it is a bit confusing and not ideal, but we won't make any changes to Boolector's API from here on.

Finally, as a suggestion, I am wondering if there could be a set of functions that would work directly on bitvector:

BoolectorNode *boolector_bv (Btor *btor, BoolectorBv *bv);
BoolectorBv *boolector_bv_raw_assignment(Btor *btor, BoolectorNode *node);
void boolector_release_bv(Btor *btor, BoolectorBv *bv);

I think it would ease the reinjection of model values into the formula.

As mentioned above, not for Boolector. We might consider it for Bitwuzla.

[aniemetz]

Correct me if I am wrong but the problem is that btoropt.h is not installed/exported (by default at least). Moreover, it actually includes some other files that are not installed too. I suggested to move just the enum types into btortypes.h̀ to avoid cascading effect of include/install.

As mentioned above, that's how it is intended. btoropt.h should not be necessary to be installed/included.

I believe that Bitwuzla might have an updated API, so maybe this can be fixed there (which saves breaking the current API).

Since I discovered its existence (not so long ago yet), I am looking forward to hear news about its release. Will it share a similar architecture with boolector or is it totally distinct project?

Eventually, it will not share any code with Boolector, it will be a complete rewrite. We will lift some concepts/architectural design decisions, but which is still to be evaluated. Right now, it is a (significantly extended) fork. However, with a completely rewritten API (will not share a single API function with Boolector). Tentative plan is to release a first version in fall, but no promises :)

[recoules]

Thank you both for your answers.

In fact, I started to play with the C api (thus I found the btoopt.h issue) but my long term goal will be to provide a binding for OCaml and, maybe an opam release of boolector (yet, I would be able to make all the build system but the release will be your decision). I hope the same thing will be possible for Bitwuzla.

[aniemetz]

@recoules sounds great!

[aniemetz]

Fixed and documentation updated.