Change the return type of constraint_slack to int64_t instead of uint64_t to match the m_slack member of the constraint struct

[rljacobson]

Brief summary:

In src/sat/sat_local_search.h, the return type of constraint_slack should be int64_t instead of uint64_t, as the m_slack member of the constraint struct has type int64_t. This change currently does not affect behavior for reasons explained below but may prevent the introduction of bugs in the future.

Background:

This issue affects the local_search class of the sat solver: src/sat/sat_local_search.*

Commit 5e4276b fixes issue #4197 by making a local variable holding the return value of constraint_slack signed but fails to correctly adjust the return type of constraint_slack. Fortunately, the (implicit) conversion from uint64_t to int64_t introduced in that commit prevents the incorrect return type of constraint_slack from having an effect. However, it is possible to imagine new code being introduced that calls constraint_slack and takes the returned type at face value, failing to convert to a signed type.

Details:

In the class local_search, we find the constraint_slack private method:

/* src/sat/sat_local_search.h: line 190 */
uint64_t constraint_slack(unsigned ci) const { return m_constraints[ci].m_slack; }

It looks up the ci^th constraint in the m_constraints vector and returns the constraint's m_slack value. The m_slack member of the constraint struct has type int64_t:

/* src/sat/sat_local_search.h: lines 112, 115, 124 */
struct constraint {
    ⋮
    int64_t         m_slack;
    ⋮
};

Moreover, constraint_slack is apparently called only twice, both times from within local_search::pick_flip_walksat():

/* src/sat/sat_local_search.cpp: lines 605, 620 */
int64_t slack = constraint_slack(pbc.m_constraint_id);
⋮
int64_t slack = constraint_slack(it->m_constraint_id);

In each case, a conversion from the uint64_t value returned by constraint_slack to an int64_t is performed. (Clang-Tidy points out that such conversion is implementation defined, though in practice I don't think there is an issue here.) As constraint_slack is a private method of local_search, no API or client code should be affected.

The "fix" is to change the return type of constraint_slack to int64_t.

Related Observations:

• The "slack" in this context appears to be a difference of pb_coeffs, which themselves are unsigned, but I do not understand the algorithm enough to know what slack does.
• In other z3 solvers, "slack" is unsigned, though it's not clear to me if the use of the word has any relation at all to its use here.
• The use of int64_t/uint64_t vs. unsigned/int/long long/etc. does not appear to be consistent. (Note that int and int64_t can be different sizes.) For example, we have:

/* src/sat/sat_local_search.h: lines 90, 99, 110 */
struct varinfo {
    ⋮
    int m_slack_score{ 0 }
    ⋮
}

(It's not clear to me if "slack score" and "slack" have the same units/dimension.)

• More generally, there are many places where unsigned typed values are assigned to their corresponding signed types without an explicit cast.