% Suggested call
% ./clingo -t 6 --sat-prepro=2 --time-limit=7200 <this-solver> <graph-files>
% Constants and options
#const num_predicates = 12.
#const max_action_arity = 3.
#const null_arg = (null,).
#const opt_equal_objects = 0. % Allow same obj as argument for grounded actions
#const opt_allow_negative_precs = 1. % Allow for negative preconditions
#const opt_fill = 1. % Fill in missing negative valuations for primitive predicates
#const opt_symmetries = 1. % Some (simple) symmetry breaking

% Input Instances defined by instance/1, and graphs by tlabel/3 and node/2
% O2D features defined by feature/1, f_arity/2, f_static/2, fval/3, and fval/4
nullary(F) :- feature(F), f_arity(F,1), 1 { fval(I,(F,null_arg),0..1) }. % Explicit zero_arity predicates
nullary(F) :- feature(F), f_arity(F,1), 1 { fval(I,(F,null_arg),S,0..1) : node(I,S) }. % Explicit zero_arity predicates
p_arity(F,N) :- feature(F), f_arity(F,N), not nullary(F). % Explicit zero_arity predicates
p_arity(F,0) :- nullary(F). % Explicit zero_arity predicates
:- p_arity(F,N), nullary(F), N > 0. % Explicit zero_arity predicates

% Relevant nodes (all relevant by default; overriden by incremental solver)
#defined filename/1.
#defined partial/2.
relevant(I,S) :- node(I,S), not partial(I,File) : filename(File).

% Actions and objects (objects come from denotation of concept Top)
action(A) :- tlabel(I,(S,T),A), relevant(I,S).
{ a_arity(A,0..max_action_arity) } = 1 :- action(A).
object(I,O) :- fval(I,(top,(O,)),1).

% Choose predicates from high-level language
{ pred(F) : feature(F) } num_predicates.

% Tuples of variables/constants for lifted effects and preconditions
#defined constant/1.
argtuple(null_arg,0). % Explicit zero arity predicates
argtuple((C1,),1) :- constant(C1).
argtuple((V1,),1) :- V1 = 1..max_action_arity.
argtuple((C1,C2),2) :- constant(C1), constant(C2).
argtuple((C1,V2),2) :- constant(C1), V2 = 1..max_action_arity.
argtuple((V1,C2),2) :- V1 = 1..max_action_arity, constant(C2).
argtuple((V1,V2),2) :- V1 = 1..max_action_arity, V2 = 1..max_action_arity.

% Tuples of objects that ground the action schemas and atoms
objtuple(I, null_arg,0) :- instance(I). % Explicit zero arity predicates
objtuple(I, (O1,),1) :- object(I,O1), not constant(O1).
objtuple(I, (O1,O2),2) :- object(I,O1), object(I,O2), not constant(O1), not constant(O2), O1 != O2.
objtuple(I, (O1,O1),2) :- object(I,O1), not constant(O1), opt_equal_objects = 1.

% Tuples of objects/constants that appear as arguments to atoms
const_or_obj(I,O) :- object(I,O).
const_or_obj(I,O) :- instance(I), constant(O).
constobjtuple(I, null_arg,0) :- instance(I). % Explicit zero arity predicates
constobjtuple(I, (O1,),1) :- const_or_obj(I,O1).
constobjtuple(I, (O1,O2),2) :- const_or_obj(I,O1), const_or_obj(I,O2), O1 != O2.
constobjtuple(I, (O1,O1),2) :- const_or_obj(I,O1), opt_equal_objects = 1.

% Assumption: predicates have arity < 3
:- p_arity(F,N), N > 2.

% Assert missing values for atoms (if some atom is not true, it is false)
fval(I,(F,OO),0) :- feature(F), f_static(I,F), p_arity(F,N), constobjtuple(I,OO,N), not fval(I,(F,OO),1), opt_fill = 1.
fval(I,(F,OO),S,0) :- feature(F), not f_static(I,F), p_arity(F,N), constobjtuple(I,OO,N), node(I,S), not fval(I,(F,OO),S,1), opt_fill = 1.

% Make sure we have full valuation of atoms
:- f_static(I,F), p_arity(F,N), constobjtuple(I,OO,N), { fval(I,(F,OO),0..1) } != 1, opt_fill = 1.
:- not f_static(I,F), p_arity(F,N), constobjtuple(I,OO,N), node(I,S), { fval(I,(F,OO),S,0..1) } != 1, opt_fill = 1.

% Mapping of lifted arguments for atoms into grounded arguments. Lifted atom is pair (P,T) where P is
% predicate and T is tuple of variables and constants used to construct argument OO of grounded atom (P,OO).

% for nullary actions
map(I,(0,0,0,0),null_arg,null_arg,0) :- instance(I).
map(I,(0,0,0,0),(C,),(C,),1) :- constobjtuple(I,(C,),1), constant(C).
map(I,(0,0,0,0),(C1,C2),(C1,C2),2) :- constobjtuple(I,(C1,C2),2), constant(C1), constant(C2).

% for unary actions
map(I,(O1,0,0,0),null_arg,null_arg,0) :- objtuple(I,(O1,),1).
map(I,(O1,0,0,0),(C,),(C,),1) :- objtuple(I,(O1,),1), constobjtuple(I,(C,),1), constant(C).
map(I,(O1,0,0,0),(1,),(O1,),1) :- objtuple(I,(O1,),1).
map(I,(O1,0,0,0),(C1,C2),(C1,C2),2) :- objtuple(I,(O1,),1), constobjtuple(I,(C1,C2),2), constant(C1), constant(C2).
map(I,(O1,0,0,0),(C,1),(C,O1),2) :- objtuple(I,(O1,),1), constobjtuple(I,(C,O1),2), constant(C).
map(I,(O1,0,0,0),(1,C),(O1,C),2) :- objtuple(I,(O1,),1), constobjtuple(I,(O1,C),2), constant(C).

% for actions of arity >= 2
map(I,(O1,O2,0,0),null_arg,null_arg,0) :- objtuple(I,(O1,O2),2).
map(I,(O1,O2,0,0),(C,),(C,),1) :- objtuple(I,(O1,O2),2), constobjtuple(I,(C,),1), constant(C).
map(I,(O1,O2,0,0),(1,),(O1,),1) :- objtuple(I,(O1,O2),2).
map(I,(O1,O2,0,0),(2,),(O2,),1) :- objtuple(I,(O1,O2),2).
map(I,(O1,O2,0,0),(C1,C2),(C1,C2),2) :- objtuple(I,(O1,O2),2), constobjtuple(I,(C1,C2),2), constant(C1), constant(C2).
map(I,(O1,O2,0,0),(C,1),(C,O1),2) :- objtuple(I,(O1,O2),2), constobjtuple(I,(C,O1),2), constant(C).
map(I,(O1,O2,0,0),(C,2),(C,O2),2) :- objtuple(I,(O1,O2),2), constobjtuple(I,(C,O2),2), constant(C).
map(I,(O1,O2,0,0),(1,C),(O1,C),2) :- objtuple(I,(O1,O2),2), constobjtuple(I,(O1,C),2), constant(C).
map(I,(O1,O2,0,0),(2,C),(O2,C),2) :- objtuple(I,(O1,O2),2), constobjtuple(I,(O2,C),2), constant(C).
map(I,(O1,O2,0,0),(1,1),(O1,O1),2) :- objtuple(I,(O1,O2),2), constobjtuple(I,(O1,O1),2).
map(I,(O1,O2,0,0),(1,2),(O1,O2),2) :- objtuple(I,(O1,O2),2), constobjtuple(I,(O1,O2),2).