Reputation: 146
When I write :
move( a, b).
move( b, c).
move( c, d).
{ p( 0, A, B) : move( A, B) } = 1 .
0 { p( N+1, B, C) : p( N, A, B), move( B, C) } 1.
Then I get the result:
Solving...
Answer: 1
p(0,c,d)
Answer: 2
p(0,a,b)
Answer: 3
p(1,b,c) p(0,a,b)
Answer: 4
p(0,b,c)
Answer: 5
p(1,c,d) p(0,b,c)
SATISFIABLE
Here I am missing the combination p(2,c,d) p(1,b,c) p(0,a,b) .
I can simulate it by partitioning the recursion steps:
move( a, b).
move( b, c).
move( c, d).
{ p( 0, A, B) : move( A, B) } = 1 .
0 { p2( N+1, B, C) : p( N, A, B), move( B, C) } 1.
0 { p3( N+1, B, C) : p2( N, A, B), move( B, C) } 1.
leads to:
Solving...
Answer: 1
p(0,c,d)
Answer: 2
p(0,b,c)
Answer: 3
p(0,b,c) p2(1,c,d)
Answer: 4
p(0,a,b)
Answer: 5
p2(1,b,c) p(0,a,b)
Answer: 6
p3(2,c,d) p2(1,b,c) p(0,a,b)
SATISFIABLE
In this case I have the result : p3(2,c,d) p2(1,b,c) p(0,a,b) .
Why don't I get this in the first code variant?
Thanks in advance for your answers.
Upvotes: 2
Views: 38