CiaoPP: computational properties and entry assertions

[simonefulvio-rollini]

Hello,

I am trying to perform determinacy checking on the following example:

:- module(test, [p1/4], [assertions,nativeprops]).

:- entry p1(X, Y, Z, U) : (atm(X), atm(Y), atm(Z), var(U)).
:- check success p1(X, Y, Z, U) : (atm(X), atm(Y), atm(Z), var(U)) => flt(U).
:- check comp p1(X, Y, Z, U) : (atm(X), atm(Y), atm(Z), var(U)) + semidet.

:- entry p1(X, Y, Z, _) : (atm(X), atm(Y), var(Z)).
:- check success p1(X, Y, Z, _) : (atm(X), atm(Y), var(Z)) => atm(Z).
:- check comp p1(X, Y, Z, _) : (atm(X), atm(Y), var(Z)) + nondet.

p1('A', 'C', 'E', 1.0).
p1('B', 'D', 'F', 2.0).
p1('B', 'D', 'G', 2.0).
p1('B', 'D', 'H', 2.0).
p1('B', 'D', 'I', 2.0).

Given the available facts, I would expect the first p1 mode to be proven semidet, but the tool identifies it as nondet.

{WARNING (ctchecks_pred_messages): (lns 5-5) Could not verify assertion:
:- check comp p1(X,Y,Z,U)
   : ( atm(X), atm(Y), atm(Z), var(U) )
   + semidet.
because
    semidet
could not be derived from inferred comp:
[shfr]         ground([X,Y,Z,U]) 
[eterms]       rt47(X),rt48(Y),rt53(Z),rt50(U) 
with:
:- regtype rt50/1.
rt50(1.0).
rt50(2.0).

:- regtype rt53/1.
rt53('E').
rt53('F').
rt53('G').
rt53('H').
rt53('I').

:- regtype rt48/1.
rt48('C').
rt48('D').

:- regtype rt47/1.
rt47('A').
rt47('B').

[nfdet]        [native_props:nondet([X,Y,Z,U]),possibly_not_covered([X,Y,Z,U]),possibly_not_mut_exclusive([X,Y,Z,U])] 
[generic_comp] [No info available]
}

Interestingly, if the entry assertion related to the second mode is commented out, the first p1 mode is recognized as semidet.
I do not understand why this happens, since the two entry conditions do not overlap; can you please help me understand what is the reason behind this tool behavior?

[pedro-lopez-garcia]

Hello Simone,
Thank you for spotting this issue. It was indeed a bug. It has now been fixed, and we are reviewing the changes before pushing them to master.
Best regards,

[simonefulvio-rollini]

Hello Pedro, thank you for the feedback; did anybody in the team have the chance to also look at #119 and #121?
Best,
Simone