s(SCAP) minimum issue

Help!
1

in s(CASP) we can get the minimum of something by demanding there not to be something smaller, e.g.

min_rate(D) :-
    rate(D),
    not notmin(D).

notmin(D) :-
    rate(D1),
    D > D1.

rate(2).
rate(1).
rate(30).

This works fine and produces a reasonable justification:

102 ?- ?++ min_rate(D).
D = 1,
% s(CASP) model
{ min_rate(1),    not notmin(1),  not rate(_A),   rate(1),        rate(2),        rate(30)
},
% s(CASP) justification
query ←
   min_rate(1) ←
      rate(1) ∧
      not notmin(1) ←
         not rate(_A) ∧
         proved(rate(1)) ∧
         1=<1 ∧
         rate(2) ∧
         1=<2 ∧
         rate(30) ∧
         1=<30,
_A ∉ [1,2,30] ;
false.

But, if we add an extra argument, all goes wrong. This seems an issue with the forall implementation, but I have a hard time understanding the details. The new program is this and the correct answer should be min_rate(30,5)

min_rate(D,A) :-
    rate(D,A),
    not notmin(D,A).

notmin(D,A) :-
    rate(D1,A1),
    A/D > A1/D1.

rate(2,4).
rate(1,2).
rate(30,5).

… But, this happens. Somehow it doesn’t seem to take the rate(30,5) into consideration!?

103 ?- ?++ min_rate(A,D).
A = 2,
D = 4,
% s(CASP) model
{ min_rate(2,4),    not rate(_A,4),   rate(1,2),        rate(2,4),
  not notmin(2,4),  not rate(1,_B),   not rate(2,_C),   not rate(30,4)
},
% s(CASP) justification
query ←
   min_rate(2,4) ←
      rate(2,4) ∧
      not notmin(2,4) ←
         not rate(1,_B) ∧
         rate(1,2) ∧
         4/2=<2/1 ∧
         rate(2,4) ∧
         4/2=<4/2 ∧
         not rate(2,_C) ∧
         not rate(_A,4) ∧
         not rate(30,4),
_B ∉ [2],
_C ∉ [2,4],
_A ∉ [1,2,30]
Here is the detailed trace 
104 ?- ?+++ min_rate(A,D).
A = 2,
D = 4,
% s(CASP) model
{ min_rate(2,4),    not rate(_A,4),   rate(1,2),        rate(2,4),
  not notmin(2,4),  not rate(1,_B),   not rate(2,_C),   not rate(30,4)
},
% s(CASP) justification
query ←
   min_rate(2,4) ←
      rate(2,4) ∧
      not notmin(2,4) ←
         not o_user:notmin_1(2,4) ←
            forall(_D,forall(_E,not'o_user:notmin_1_vh4'(2,4,_D,_E))) ←
               not o_user:notmin_1_vh4(2,4,1,_B) ←
                  not rate(1,_B) ←
                     not o_user:rate_1(1,_B) ←
                        1\=2 ∧
                     not o_user:rate_2(1,_B) ←
                        1=1 ∧
                        _B\=2 ∧
                     not o_user:rate_3(1,_B) ←
                        1\=30 ∧
               not o_user:notmin_1_vh4(2,4,1,2) ←
                  rate(1,2) ∧
                  4/2=<2/1 ∧
               not o_user:notmin_1_vh4(2,4,2,4) ←
                  rate(2,4) ∧
                  4/2=<4/2 ∧
               not o_user:notmin_1_vh4(2,4,2,_C) ←
                  not rate(2,_C) ←
                     not o_user:rate_1(2,_C) ←
                        2=2 ∧
                        _C\=4 ∧
                     not o_user:rate_2(2,_C) ←
                        2\=1 ∧
                     not o_user:rate_3(2,_C) ←
                        2\=30 ∧
               not o_user:notmin_1_vh4(2,4,_A,4) ←
                  not rate(_A,4) ←
                     not o_user:rate_1(_A,4) ←
                        _A\=2 ∧
                     not o_user:rate_2(_A,4) ←
                        _A\=1 ∧
                     not o_user:rate_3(_A,4) ←
                        _A\=30 ∧
               not o_user:notmin_1_vh4(2,4,30,4) ←
                  not rate(30,4) ←
                     not o_user:rate_1(30,4) ←
                        30\=2 ∧
                     not o_user:rate_2(30,4) ←
                        30\=1 ∧
                     not o_user:rate_3(30,4) ←
                        30=30 ∧
                        4\=5 ∧
   o_nmr_check,
_B ∉ [2],
_C ∉ [2,4],
_A ∉ [1,2,30]
And the dual program 
106 ?- scasp_show(min_rate(A,D), code(duals(true))).
% User Predicates

min_rate(A, B) :-
    rate(A, B),
    not notmin(A, B).

notmin(A, B) :-
    rate(C, D),
    B/A>D/C.

rate(2, 4).
rate(1, 2).
rate(30, 5).

% Dual Rules

not notmin(A, B) :-
    not o_user:notmin_1(A, B).

not o_user:notmin_1(A, B) :-
    forall(C,
           forall(D,
                  not'o_user:notmin_1_vh4'(A, B, C, D))).

not o_user:notmin_1_vh4(_, _, A, B) :-
    not rate(A, B).
not o_user:notmin_1_vh4(A, B, C, D) :-
    rate(C, D),
    B/A=<D/C.

not rate(A, B) :-
    not o_user:rate_1(A, B),
    not o_user:rate_2(A, B),
    not o_user:rate_3(A, B).

not o_user:rate_1(A, _) :-
    A\=2.
not o_user:rate_1(A, B) :-
    A=2,
    B\=4.

not o_user:rate_2(A, _) :-
    A\=1.
not o_user:rate_2(A, B) :-
    A=1,
    B\=2.

not o_user:rate_3(A, _) :-
    A\=30.
not o_user:rate_3(A, B) :-
    A=30,
    B\=5.

not min_rate(A, B) :-
    not o_user:min_rate_1(A, B).

not o_user:min_rate_1(A, B) :-
    not rate(A, B).
not o_user:min_rate_1(A, B) :-
    rate(A, B),
    notmin(A, B).
true.

The behavior is consistent with the Ciao version. Can some scasper explain this in human terms :slight_smile: Maybe @Xuaco ?

2

Hi Jan,
The error is due to the implementation of c_forall/2.
Using the --prev_forall flag the behavior is as expected:

scasp --prev_forall jan.pl
% QUERY:?- min_rate(D,A).

ANSWER: 1 (in 7.479 ms)

MODEL:
{ min_rate(30,5), rate(30,5), not notmin(30,5), not rate(Var2 | {Var2 = 1,Var2 = 2,Var2 = 30},Var3), not rate(1,Var4 | {Var4 = 2}), rate(1,2), not rate(2,Var5 | {Var5 = 4}), rate(2,4), not rate(30,Var6 | {Var6 = 5}) }
BINDINGS:
D = 30
A = 5 ? ;

3

Hi Joaquin, Thanks. Only --prev_forall causes other issues in our code :frowning: We now worked around it using findall/3 and then take the minimum of the list.