Question: array or not array?

[Udopia]

IPASIR-2 uses zero-terminated arrays of literals in several places:

• in the classic learned clause callback for the exported learned clause (inherited from IPASIR)
• in the import clause callback for the imported learned clause
• in the notify callback for the exported assignment

IPASIR-2 even uses zero-terminated arrays of structs:

• in the options getter for returning the available options

IPASIR-2 also uses zero-terminated C-style strings:

• in ipasir2_signature (inherited from IPASIR)
• as option identifiers

The only exceptions to this pattern where no arrays are used are the following (all inherited from IPASIR):

• ipasir2_add sets clauses literal-wise (zero terminated)
• ipasir2_assume accumulates assumptions literal-wise
• ipasir2_val to receive the model literal-wise
• ipasir2_failed to receive failed assumptions literal-wise

With IPASIR-2 we have the opportunity to make this more homogeneous if the community wishes for that. That means using arrays in the setters of clauses (add) and assumptions (assume) and getters of models (val) and failed assumptions (failed) as well, or only in a subset of those. Moreover, we could move from zero terminated arrays to arrays with length, which would imply adding an additional parameter per array and function to specify the array-length. That would solve some issues, e.g., if models are returned via array and zero indicates don't care literals (which would conflict with zero-termination anyway). In any case, I would aim at staying homogeneous, i.e., either stick to zero-termination or length termination, but not mix both.

So, shall we open that can of worms or leave everything as it is? :)

[Froleyks]

Good morning from China, I wouldn't change this since the two groups of functions you mentioned are used differently. On top of that the majority of users only ever touch the bottom four, so not changing their signature would be beneficial.

…

On Sat, Aug 19, 2023, 00:36 Markus Iser ***@***.***> wrote: IPASIR-2 uses zero-terminated arrays of literals in several places: - in the classic *learned clause callback* for the exported learned clause (inherited from IPASIR) - in the *import clause callback* for the imported learned clause - in the *notify callback* for the exported assignment IPASIR-2 even uses zero-terminated arrays of structs: - in the *options getter* for returning the available options IPASIR-2 also uses zero-terminated C-style strings: - in *ipasir2_signature* (inherited from IPASIR) - as option identifiers The only exceptions to this pattern where no arrays are used are the following (all inherited from IPASIR): - *ipasir2_add* sets clauses literal-wise (zero terminated) - *ipasir2_assume* accumulates assumptions literal-wise - *ipasir2_val* to receive the model literal-wise - *ipasir2_failed* to receive failed assumptions literal-wise With IPASIR-2 we have the opportunity to make this more homogeneous if the community wishes for that. That means using arrays in the setters of clauses (add) and assumptions (assume) and getters of models (val) and failed assumptions (failed) as well, or only in a subset of those. Moreover, we could move from zero terminated arrays to arrays with length, which would imply adding an additional parameter per array and function to specify the array-length. That would solve some issues, e.g., if models are returned via array and zero indicates don't care literals (which would conflict with zero-termination anyway). In any case, I would aim at staying homogeneous, i.e., either stick to zero-termination or length termination, but not mix both. So, shall we open that can of worms or leave everything as it is? :) — Reply to this email directly, view it on GitHub <#30>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACF2LLT2YFWJCOJHG2B4OMDXV6KZTANCNFSM6AAAAAA3VYHO7M> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[Udopia]

Thanks for commenting! That would be my preferred choice as well. If there are no other strong opinions, I will stick to it. Cheers, from Finland to China :)

[Udopia]

The discussion on the "specification of concurrency support" sort of reopens this discussion, since we have an additional good reason to change the signature of ipasir2_add. Also see Felix Kutzners comment below

[fkutzner]

I agree that it is important to have a consistent data structure for clauses, but I don't think we need to apply that principle to all arrays in IPASIR-2.

I'm currently writing a prototype C++ wrapper for IPASIR-2, so some thoughts on clauses:

Explicitly passing the size would be a better fit for clauses than zero-termination. For example, it would play nicer with things like std::vector, std::span, memcpy etc. I don't think that the extra size parameter adds complexity to the IPASIR-2 functions: with zero-termination, it’s just hidden at the end of the clause. Also, with a size parameter, passing clauses is simpler since no terminator needs to be appended.

However, zero-terminated clauses shouldn't become too much of a problem either. The performance impact (copying clauses to add trailing zeros, and iterating to determine their length) should be tiny even compared to the amount of time needed to learn a clause, especially since the overhead is mostly just linear memory access. But to be on the safe side, we should profile example applications when the interface is stable enough.

All in all, I'd welcome switching to pointer+size representation, but sticking with zero-terminated clauses should be viable too.

[arminbiere]

As was pointed out to me recently since C++11 there is this 'std::vector::data' which (similar to 'std::string::c_string') would give us an effective and both time and space efficient way to get a continuous C-style array of int's ('int *') from a 'std::vector' (I always used the idiom '&v[0]' before). Therefore I am tempted to suggest we move to 'pointer + size' as this would give an in-place no performance overhead usage for C++ users (which are probably the most common users anyhow). Adding the zero on the C++ side before to obtain a zero terminated int array is awkward in case the C++ users wants to work with the vector of literals afterwards (and also always needs to remember that). An IPASIR C++ wrapper could further simplify that:

class IPASIR {
...
public:
  virtual void add (size_t, int *);
  void add (std::vector<int> & v) { add (v.size (), v.data ()); }
...
};

[m-fleury]

Remark that data is part of C++11. So using it might introduce some restrictions on possible compilers (but: C++11 is from 2011, so 12 years old at that point).

[arminbiere]

Yes C++11 is a restriction and the '&v[0]' should also continue work. One could of course also have a core C++ wrapper which and a second extended one (which requires C++11).

[fkutzner]

I think it's reasonable to require C++11 in the main wrapper. All major compilers have been supporting it for a long time now. There might be a few IPASIR2 clients who are stuck on C++03 or earlier (thinking of old proprietary compilers for embedded systems), but they could write an ad-hoc IPASIR2 wrapper for their use case.

[Udopia]

Okay, so this looks like we have some support for switching to array+length in at least some signatures. Regarding ipasir2_add(), we should also consider the clause-lifetime fix of fkutzner, i.e., the import-callback calls add (cf. https://github.com/orgs/ipasir2/discussions/31#discussioncomment-6815887). All in all, this boils down to the following new signature for add:

IPASIR_API ipasir2_errorcode ipasir2_add(void* solver, size_t len, int const* literals, ipasir2_redundancy type);

I recommend to propagate this switch to the other methods. Then assume(), val(), and failed() would look as follows:

IPASIR_API ipasir2_errorcode ipasir2_assume(void* solver, size_t len, int const* literals);
IPASIR_API ipasir2_errorcode ipasir2_model(void* solver, size_t* len, int** literals);
IPASIR_API ipasir2_errorcode ipasir2_failed(void* solver, size_t* len, int** literals);

Note that some of the signatures would not even grow, as the parameter int lit vanishes when all results are returned at once.

[fkutzner]

It's a small issue but we should switch the parameter order: pointer to the array first, then length, since that's how the C standard library and POSIX tend to place these parameters (see for example fread(), strncpy(), getcwd(), read(), write() etc.)

Would the array-based ipasir2_assume() set all assumptions for the next ipasir2_solve() call? If so, we could remove the function and add the assumption array to the parameters of ipasir2_solve().

How would ipasir2_model() and ipasir2_failed() fill the literals arrays? If clients should still be able to do O(1) literal value lookups directly, they'd need to be able to index into these arrays using the variable number. But then, I think literal-wise getter functions would be a better fit.

[arminbiere]

I agree. For some applications single literal 'failed' and 'model' are more efficient than requiring the SAT solver to produce a full model every time. What about two functions? Also note that I assume we will keep the semantics that the model and the failed information might become invalid as soon we add a new clause (or assumption). Therefore the user needs to copy the whole model in case multiple clauses based on the model are added. So even in that case the user might better use the single literal variant.

[Udopia]

Okay, from your comments I got that we should distinguish setters (add, assume) from getters (val, failed), and that we should either leave the getters as they are, and if necessary rather introduce a second getter (probably not necessary).

But for the setters, the change to array+len is less problematic, and so I changed the signatures from literal-wise to array+len: ipasir2_add. I made one additional change: To solve the scoping of assumptions in a more intuitive way, I removed assume() and integrated it into solve(): ipasir2_solve