postprocessing encoding checked

This commit is contained in:
gebser 2016-11-15 09:07:36 +01:00
parent e2c38b5459
commit 03c83702ad

View File

@ -6,19 +6,17 @@ time :- time(T).
:- goal(X,V), not initialState(X,V), not time. :- goal(X,V), not initialState(X,V), not time.
next(T1,T2) :- time(T1), time(T2), T1 < T2, T <= T1 : time(T), T < T2. last(T2) :- time, T2 = #max{T1 : time(T1)}.
init(T2) :- time(T2), #false : next(T1,T2).
stop(T1) :- time(T1), #false : next(T1,T2).
offset(T2,M) :- time(T2), M = #count{A,T1 : occurs(A,T1), T1 < T2}. offset(T2,M) :- time(T2), M = #count{A,T1 : occurs(A,T1), T1 < T2}.
actions(T,N) :- time(T), N = #count{A : occurs(A,T)}. finish(T,M+N) :- offset(T,M), N = #count{A : occurs(A,T)}.
index(T,M+1..M+N) :- offset(T,M), actions(T,N). index(T,M+1..N) :- offset(T,M), finish(T,N).
postcondition(A,X,V) :- postcondition(A,E,X,V), occurs(A,T). postcondition(A,X,V) :- postcondition(A,E,X,V), occurs(A,T).
postcondition(A,X) :- postcondition(A,X,V). postcondition(A,X) :- postcondition(A,X,V).
before(A1,A2,T) :- occurs(A1,T), occurs(A2,T), A1 != A2, before(A1,A2,T) :- occurs(A1,T), occurs(A2,T), A1 != A2,
precondition(A1,X,V1), postcondition(A2,X,V2), V1 != V2. precondition(A1,X,V), postcondition(A2,X), not postcondition(A2,X,V).
order(A1,A2,T) :- occurs(A1,T), occurs(A2,T), A1 < A2, A <= A1 : occurs(A,T), A < A2. order(A1,A2,T) :- occurs(A1,T), occurs(A2,T), A1 < A2, A <= A1 : occurs(A,T), A < A2.
first(A2,T) :- occurs(A2,T), #false : order(A1,A2,T). first(A2,T) :- occurs(A2,T), #false : order(A1,A2,T).
@ -29,23 +27,23 @@ undone(A,T,N) :- undone(A,T,N-1), select(A1,T,N), A != A1, index(T,N+1).
done(A,T,N) :- select(A,T,N). done(A,T,N) :- select(A,T,N).
done(A,T,N) :- done(A,T,N-1), index(T,N). done(A,T,N) :- done(A,T,N-1), index(T,N).
:- offset(T,M), actions(T,N), occurs(A,T), not done(A,T,M+N). :- finish(T,N), occurs(A,T), not done(A,T,N).
holds(X,V,0) :- initialState(X,V), time. hold(X,V,0) :- initialState(X,V).
holds(X,V,N) :- select(A,T,N), postcondition(A,X,V). hold(X,V,N) :- select(A,T,N), postcondition(A,X,V).
holds(X,V,N) :- select(A,T,N), holds(X,V,N-1), not postcondition(A,X). hold(X,V,N) :- select(A,T,N), hold(X,V,N-1), not postcondition(A,X).
:- stop(T), offset(T,M), actions(T,N), goal(X,V), not holds(X,V,M+N). :- last(T), finish(T,N), goal(X,V), not hold(X,V,N).
holds(X,N) :- holds(X,V,N). hold(X,N) :- hold(X,V,N).
:- holds(X,N), #count{V : holds(X,V,N) } > 1. :- hold(X,N), #count{V : hold(X,V,N)} > 1.
preconditions(A,T,N) :- undone(A,T,N), holds(X,V,N) : precondition(A,X,V). preconditions(A,T,N) :- undone(A,T,N), hold(X,V,N) : precondition(A,X,V).
applicable(A,T,N) :- preconditions(A,T,N), done(A1,T,N) : before(A1,A,T). applicable(A,T,N) :- preconditions(A,T,N), done(A1,T,N) : before(A1,A,T).
inapplicable(A,T,N) :- done(A,T,N), index(T,N+1). inapplicable(A,T,N) :- done(A,T,N), index(T,N+1).
inapplicable(A,T,N) :- undone(A,T,N), precondition(A,X,V1), holds(X,V2,N), V1 != V2. inapplicable(A,T,N) :- undone(A,T,N), precondition(A,X,V1), hold(X,V2,N), V1 != V2.
inapplicable(A,T,N) :- undone(A1,T,N), before(A1,A,T). inapplicable(A,T,N) :- undone(A1,T,N), before(A1,A,T).
continue(A2,T,N) :- order(A1,A2,T), inapplicable(A1,T,N), first(A1,T). continue(A2,T,N) :- order(A1,A2,T), inapplicable(A1,T,N), first(A1,T).
@ -54,8 +52,7 @@ continue(A2,T,N) :- order(A1,A2,T), inapplicable(A1,T,N), continue(A1,T,N).
select(A,T,N+1) :- applicable(A,T,N), first(A,T). select(A,T,N+1) :- applicable(A,T,N), first(A,T).
select(A,T,N+1) :- applicable(A,T,N), continue(A,T,N). select(A,T,N+1) :- applicable(A,T,N), continue(A,T,N).
sequence(A,N) :- select(A,T,N).
% DISPLAY PART % DISPLAY PART
#show sequence/2. #show.
#show sequence(A,N) : select(A,T,N).