Unclear meaning of ccadical_val return value

[timvermeulen]

I'd love some guidance to understand the meaning of the return value of ccadical_val, particularly when the argument is a negative literal.

ccadical_val calls Solver::val, which is documented as

cadical/src/cadical.hpp

Line 289 in 2df7b7f

// Get value (-lit=false, lit=true) of valid non-zero literal.

but it seems as though its actual behavior is flipped in the case that lit is negative, i.e. abs(lit) is returned when lit is true, and -abs(lit) is returned when lit is false. I get the impression that this behavior deviates from the above documentation (as well as from the IPASIR standard), am I mistaken?

Solver::val calls the ival function on External, which is implemented as follows:

cadical/src/external.hpp

Lines 294 to 306 in 2df7b7f

	inline int ival (int elit) const {
	assert (elit != INT_MIN);
	int eidx = abs (elit), res;
	if (eidx > max_var)
	res = -eidx;
	else if ((size_t) eidx >= vals.size ())
	res = -eidx;
	else
	res = vals[eidx] ? eidx : -eidx;
	if (elit < 0)
	res = -res;
	return res;
	}

Indeed, in case elit is negative and is also part of the assignment, then res is first set to -eidx (i.e. elit) on line 302, after which it is negated to eidx (i.e. -elit) on line 304.

[arminbiere]

It looks something is off here.

In general there was a misunderstanding between Tomas and me when we defined 'value' semantics in the IPASIR interface. At least I wanted to just return a ternary value (-1,0,1) as in PicoSAT, but then for some reason in IPASIR we defined value semantics to return for a literal 'lit' which is true 'lit' itself and otherwise if it is false its negation '-lit'.

#include "../src/cadical.hpp"

void test_value_semantics_in_CPP_interface () {
  CaDiCaL::Solver solver;
  solver.clause (1, 2);
  solver.clause (1, -2);
  solver.clause (-1, -2);
  int res = solver.solve ();
  assert (res == 10);
  assert (solver.val (1) == 1);
  assert (solver.val (2) == -2);
  assert (solver.val (-1) == 1);
  assert (solver.val (-2) == -2);
}

And for the C interface the following should succeed

#include "../src/ccadical.h"

void test_value_semantics_in_C_interface () {
  auto solver = ccadical_init ();
  ccadical_add (solver, 1), ccadical_add (solver, 2),
      ccadical_add (solver, 0);
  ccadical_add (solver, 1), ccadical_add (solver, -2),
      ccadical_add (solver, 0);
  ccadical_add (solver, -1), ccadical_add (solver, -2),
      ccadical_add (solver, 0);
  int res = ccadical_solve (solver);
  assert (res == 10);
  assert (ccadical_val (solver, 1) == 1);
  assert (ccadical_val (solver, 2) == -2);
  assert (ccadical_val (solver, -1) == 1);
  assert (ccadical_val (solver, -2) == -2);
  ccadical_release (solver);
}

but both tests fail when getting the value of '-1'.

Originally I only had the ternary version implemented and then later returned a literal, but probably, as you suggest , the wrong one in case literal is negative.

[arminbiere]

There is now a fix on the ccadical-val-issue-108 branch. We will incorporate this in the next release. For now the work-around is to not use negative literals in 'ccadical_val' or 'Solver::val'.