Clingo: Operation undefined while doing computations inside the testing rules

I am new to ASP programming and finding it a bit hard to understand how ASP works. I am using clingo tool for ASP coding. Currently, I am working on a seating arrangement problem. The original problem is a bit complicated as it involves lots of variables and constraints. I have started with a basic version of it which is as follows:

4 persons need to be seated in a horizontal row having 4 seats. There are no constraints among these persons. Each person can move left/right to any other person. The final goal is straightforward

"any person can sit at any location provided it is available"

The only condition is to save the individual steps about how the goal is reached.

To solve it, I have used a predicate

seated(A,B,Shift,Dir,t) which says that at time t A has shifted Shift units in the Dir from B

Example

seated(A,B,left,2,t) implies A has shifted 2 units to the left of B at time t

I have used two files

init.lp describing the initial positions and final goal

person(a).
person(b).    
person(c).    
person(d).

init(pos(a,0)).    
init(pos(b,0)).    
init(pos(c,0)).    
init(pos(d,0)).
    
goal(pos(a,1)).    
goal(pos(b,2)).    
goal(pos(c,3)).
goal(pos(d,4)).

rules.lp where the rules are written

#include<incmode>.

#program base.
% Define
holds(F,0) :- init(F).
%{possible_location(X,Y,1) : person(X),Y = 1..4}.
%%possible_location(X,Y,1) : person(X),Y = 1..4.

#program step(t).
% Generate any seating arrangement

1 { seated(X,Z,Shift,Dir,t) : person(X), person(Z), X != Z,Shift = 1..3, Dir = (left;right) } 1.
    
% Test
% Remove the seated predicates which the shift is not possible
:- seated(X,Z,Shift,right,t), holds(pos(Z,Pos),t-1), Shift + Pos > 4.
:- seated(X,Z,Shift,left,t), holds(pos(Z,Pos),t-1), Pos - Shift < 1.

% Remove the seated predicates if the final position after shifting is already occupied
:- seated(X,Z,Shift,right,t), holds(pos(Z,Pos),t-1), Pos>0, holds(pos(A,Shift + Pos),t-1), A!=X.
:- seated(X,Z,Shift,left,t), holds(pos(Z,Pos1),t-1), Pos1>0, holds(pos(A,Pos1 - Shift),t-1), A!=X.
    
% Define
seateded(X,t) :- seated(X,Z,Shift,Dir,t).

% Relating the current move to the current state %
holds(pos(X,Y),t) :- seated(X,Y,Shift,Dir,t).

% This is for shifting the state to the next time %
holds(pos(X,Z),t) :- holds(pos(X,Z),t-1), not seateded(X,t).

#program check(t).
% Test
:- query(t), goal(F), not holds(F,t).

% Display
#show seated/5.
#show query/1.

On running the above files, it gives an error

rule_new.lp:21:75-87: info: operation undefined:
  (Pos1-Shift)

I have googled it and found out that this error comes when I have not handled any edge case such as X/Y and Y=0 is not handled. In this case, I don't see any edge case. Hence, I am not able to rectify the error.

I have documented the rules so that I can explain the thought process behind writing the rules. I have spent a couple of hours solving it and still couldn't figure out the solution. If my thinking is not in the right direction then I would appreciate if I can get some other solution to the above problem.

Solution

I'm afraid I didn't manage to understand your solution (or problem), but using the option --text can help you figure this error out. According to the error message the problem is in this rule:

seated(X,Z,Shift,left,t),holds(pos(Z,Pos1),t-1),  Pos1 >0, holds(pos(A,Pos1 - Shift),t-1), A !=X.

You try to subtract Shift from Pos1. Both Variables should be substituted by integers to make this work.

Shift comes from the seated predicate and can take a value between 1..3, fine. Pos1 comes from the holds(pos(_,Pos1),_) predicate.

In your rule:

holds(pos(X,Y),t) :- seated(X,Y,Shift,Dir,t).

You clearly derive holds predicates where Y is a person, aka. a, b, c, or d.

So you try to compute 3-a which clingo refuses to do and drops the according rule, raising this warning.