More scasp tests

I am using scasp on swish.

I am trying to understand the denials still…

My code:
https://swish.swi-prolog.org/p/scasp_constraint_tests.pl

% s(CASP) Programming
:- use_module(library(scasp)).

false :- list1_list2(_List1,List2),my_length(List2,4).

p(1).
p(2).
p(3).

my_length([],0).
my_length([_|List],Len):-my_length(List,Len0),Len is Len0+1.

list1_list2(List,[P|List]):- p(P).

list1_list2_h(List1,List2):- list1_list2(List1,List2),my_length(List2,_Len).

/** <examples> Your example queries go here, e.g.

?- ? list1_list2([],List).
?- ? list1_list2([3,4],List).
?- ? list1_list2([a,b,c],List).

?- ? list1_list2_h([],List).
?- ? list1_list2_h([3,4],List).
?- ? list1_list2_h([a,b,c],List).

*/

I expected ?- ? list1_list2([a,b,c],List). or at least ?- ? list1_list2_h([a,b,c],List). to fail (due to the explicit call to my_length/2) but neither do.

Am I misunderstanding something here?

I don’t know yet. It looks a bit odd program, but I tend to agree ? list1_list2([a,b,c],List). should fail. The original Ciao version loops, so something weird is going on …

Ok. It is getting a bit clearer to me

  • ? list1_list2(_List1,List2) creates lists [1|_], [2|_] and [3|_].
  • ? my_length([1|_],4). correctly succeeds, but on backtracking it goes into an infinite loop. This is correct: it doesn’t know that increasing lengths will never be 4 again. It is still a computer :slight_smile:
  • Somehow, the conjunction ? list1_list2(_List1,List2), my_length(List2,4). fails. This must be a bug and the Ciao version correctly succeeds once and again goes into an infinite loop.

As a result of the failure in the current implementation, the global constraint holds and therefore we get this result. The global constraint makes Ciao go into a loop. I think that can be improved as if the body of a global constraint succeeds we can cut.

Note that the global constraint is logically always false and therefore no matter which query you use, if it considers this global constraint it will fail.

Now I must figure out why this conjunction fails :frowning: Thanks for the report!

ok…

The other one I have tried is with the global constraint:

false :- list1_list2(_List1,List2),member(1,List2).
?- ? list1_list2([a,b],List2).
List2 = [1, a, b];

I think any conjunction fails when asked as a query…

? p(1),p(2).
false

I noticed that … That part is fixed (also on public SWISH). Unfortunately that was a simple mistake in the query preparation and doesn’t solve the global constraint problem.

My previous remark on the constraints are wrong though. The “correct” response is a model that includes all lists that do not have a length of 4 (in the original example) or, in the new version, all lists that do not contain a 1. As there are an infinite number of such lists, this query should not terminate. There is indeed a bug :frowning:

I think there is no bug after all :slight_smile: I’ve reduced the program to this:

% :- c(L).
:- p(_, List2), my_length(List2,2).

c(List2) :-
    p(_, List2),
    my_length(List2,2).

p(X, [P|X]) :-
    p(P).

p(1).

my_length([], 0).
my_length([_|List], Len) :-
    my_length(List, Len0),
    Len is Len0+1.

Now, ? not c(X). is true with one model, complicated language for "Any list that does not start with a 1.

{ not c([A | {A∉[1]}|B]), not p(A | {A∉[1]}), not p(B,[A | {A∉[1]}|B])
}

And ? p(X,Y).

% Model
{ not p(A | {A∉[1]}), p(1),  p(X,[1|X]),  not p(B,[A | {A∉[1]}|B])
}
% Bindings
Y = [1|X] ? 

Which is consistent (I think; not sure this is all Common Sense :slight_smile: ). The model comes with a list that starts with 1. The constraint prohibits lists that start with anything but 1.

I think this is just a simplification of your original program.

hmm.

With your program:

?- ? c([1,2]). Is true. This is not what I expect.

I would understand to say no model with list2 of a length of 2 is allowed. So a model could have list2 with length 1 or >3 according to the constraint, but :
c(List2) :- p(_, List2), my_length(List2,2).

Says that it has to be length 2. So I would expect ‘false’. As there can be no model where both of these are true.

From Joaquin I got this answer:

Nice example.

The denial :- p(, List2), my_length(List2,2). Means that forall _ and List2 the atoms p(, List2), my_length(List2,2) cannot be simultaneously true.

Since p(,[1,]) holds and my_length([1,_],2) also holds there are no models.

The denial :- c(L) means that forall L the atom c(L) must be false.

Again, since c([1,_]) holds the denial discard any tentative model.

Under s(CASP) using --sasp_forall or —prev_forall flags the evaluation generates the model >obtained under Swi-Prolog — which is incorrect.

I’m still scratching my head about all the negations :slight_smile: It gave me some hope I had messed up the option processing. Unfortunately that is not the case :frowning: