diff --git a/encodings/strips/redundancy.lp b/encodings/strips/redundancy.lp index d2089bb..60ff3ba 100644 --- a/encodings/strips/redundancy.lp +++ b/encodings/strips/redundancy.lp @@ -15,8 +15,12 @@ compatible(A) :- active(A), active(A1), A != A1, _parallel = 1, not selfdefea disable(A,A1,A2) :- compatible(A,A1), compatible(A,A2), compatible(A1,A2), disable(A1,A2), not disable(A1,A). -disabled(A,A2) :- disable(A,A1,A2). disabled(A,A1) :- compatible(A), disable(A,A1). +disabled(A,A2) :- simulate(A,A1), disable(A,A1,A2). + +simulate(A,A1) :- compatible(A,A1), not disable(A1,A), disabled(A,A1). +simulate(A,A1) :- compatible(A,A1), not disable(A1,A), scope(X,V), + postcondition(A1,X,V), not precondition(A1,X,V). % STEP PROGRAM @@ -30,15 +34,15 @@ defeated(A,t) :- compatible(A), precondition(A,X,V), not has_condition(A,X,1), n defeated(A,t) :- compatible(A), has_condition(A,X,1), not has_condition(A,X,0), single(X,t). proceed(A,X,V,t) :- compatible(A), holds(X,V,t-1), scope(X,V). -proceed(A,X,V,t) :- compatible(A,A1), not disable(A1,A), perform(A,A1,t), occurs(A1,t), - scope(X,V), postcondition(A1,X,V), not precondition(A1,X,V). +proceed(A,X,V,t) :- simulate(A,A1), perform(A,A1,t), occurs(A1,t), scope(X,V), + postcondition(A1,X,V), not precondition(A1,X,V). -perform(A,A1,t) :- compatible(A,A1), not disable(A1,A), +perform(A,A1,t) :- simulate(A,A1), proceed(A,X,V,t) : precondition(A1,X,V), _parallel = 2; alright(A,A2,t) : disable(A,A1,A2). alright(A,A1,t) :- disabled(A,A1), not occurs(A1,t). -alright(A,A1,t) :- perform(A,A1,t). +alright(A,A1,t) :- disabled(A,A1), perform(A,A1,t). defeated(A,t) :- compatible(A), precondition(A,X,V), not proceed(A,X,V,t), _parallel = 2. defeated(A,t) :- compatible(A), disable(A,A1), not alright(A,A1,t). diff --git a/encodings/strips/strips-incremental.lp b/encodings/strips/strips-incremental.lp index 060077e..dc74139 100644 --- a/encodings/strips/strips-incremental.lp +++ b/encodings/strips/strips-incremental.lp @@ -7,6 +7,12 @@ #const _parallel = 0. +% Constant '_shallow' to cheaply approximate mutually disabling parallel actions +% - value '0': detect incompatible pre/postconditions to reduce parallel actions +% - otherwise: over-approximate parallel actions (in testing mutual disablement) + +#const _shallow = 0. + % Constant 'planner_on' to enable encoding support for ASP-based planner % - value '0': no compatibility to ASP-based planner (no idle steps permitted) % - otherwise: compatibility to ASP-based planner (idle steps permitted) @@ -22,12 +28,12 @@ selfdefeat(A,X) :- active(A), precondition(A,X,V), _parallel = 1, diverge(A1,A2,X) :- active(A1), active(A2), postcondition(A1,X,V), has_condition(A2,X,1), not postcondition(A2,X,V), - 0 < _parallel, _parallel < 5. + 0 < _parallel, _parallel < 5, _shallow = 0. diverge(A1,A2) :- diverge(A1,A2,X). exclude(A1,A2) :- active(A1), active(A2), precondition(A1,X,V), has_condition(A2,X,0), not precondition(A2,X,V), - 0 < _parallel, _parallel < 5, _parallel != 2. + 0 < _parallel, _parallel < 5, _parallel != 2, _shallow = 0. disable(A1,A2) :- active(A1), active(A2), A1 != A2, postcondition(A1,X,V), has_condition(A2,X,0), not precondition(A2,X,V), @@ -46,6 +52,7 @@ fluent(X,V) :- initialState(X,V), fluent(X). fluent(X,V) :- active(A), postcondition(A,X,V), fluent(X). fluent(X) :- fluent(X,V). fluent(X) :- diverge(A1,A2,X), not exclude(A1,A2). +fluent(X) :- active(A), has_condition(A,X,1), 0 < _parallel, _parallel < 5, _shallow != 0. % Define unsubsumed mutexes