%======================================================================
%----Procedures for rearranging clauses in TPTP format, using standard
%----Prolog. 
%----
%----Written by Geoff Sutcliffe, November 1992.
%----Revised by Geoff Sutcliffe, January 1994.
%======================================================================
%----------------------------------------------------------------------
%----Reverse the literals in each input clause
reverse_literals_in_clauses([],[]).

reverse_literals_in_clauses([input_clause(Name,Status,Literals)|
Rest_of_input_clauses],[input_clause(Name,Status,Reversed_literals)|
Rest_of_new_input_clauses]):-
    fast_reverse_list(Literals,[],Reversed_literals),
    reverse_literals_in_clauses(Rest_of_input_clauses,
Rest_of_new_input_clauses).
%----------------------------------------------------------------------
%----Randomize a list of literals
randomize_literals([],0,[]).

randomize_literals(Literals,NumberOfLiterals,[SelectedLiteral|
RestOfRandomizedLiterals]):-
    tptp2X_random_integer(1,NumberOfLiterals,LiteralToSelect),
    tptp2X_select_Nth(SelectedLiteral,Literals,LiteralToSelect,
OtherLiterals),
    NewNumberOfLiterals is NumberOfLiterals - 1,
    randomize_literals(OtherLiterals,NewNumberOfLiterals,
RestOfRandomizedLiterals).
%----------------------------------------------------------------------
%---Put the clauses in random order, with randomly ordered literals
randomize_clauses([],0,[]).

randomize_clauses(InputClauses,NumberOfInputClauses,[input_clause(
Name,Status,RandomizedLiterals)|RestOfOutputClauses]):-
    tptp2X_random_integer(1,NumberOfInputClauses,ClauseToSelect),
    tptp2X_select_Nth(input_clause(Name,Status,Literals),InputClauses,
ClauseToSelect,OtherInputClauses),
    tptp2X_length(Literals,NumberOfLiterals),
    randomize_literals(Literals,NumberOfLiterals,RandomizedLiterals),
    NewNumberOfInputClauses is NumberOfInputClauses - 1,
    randomize_clauses(OtherInputClauses,NewNumberOfInputClauses,
RestOfOutputClauses).
%----------------------------------------------------------------------
%----Randomly reorder formulae
randomize_formulae([],0,[]).

randomize_formulae(InputFormulae,NumberOfInputFormulae,[RandomFormula|
RestOfOutputFormulae]):-
    tptp2X_random_integer(1,NumberOfInputFormulae,FormulaToSelect),
    tptp2X_select_Nth(RandomFormula,InputFormulae,FormulaToSelect,
OtherInputFormulae),
    NewNumberOfInputFormulae is NumberOfInputFormulae - 1,
    randomize_formulae(OtherInputFormulae,NewNumberOfInputFormulae,
RestOfOutputFormulae).
%----------------------------------------------------------------------
%----Reverse a unit equality clause
reverse_unit_equality(input_clause(Name,Status,[Literal]),input_clause(
Name,Status,[ReversedLiteral])):-
    Literal =.. [Sign,'$tptp_equal'(T1,T2)],
    ReversedLiteral =.. [Sign,'$tptp_equal'(T2,T1)].
%----------------------------------------------------------------------
%----Reverse all the terms in only unit equality clauses (fail if
%----anything else appears)
reverse_unit_equalities([],[]).

reverse_unit_equalities([input_clause(Name,Status,[Literal])|RestOfClauses],
[ReversedClause|RestOfReversedClauses]):-
%----Check it's a unit equality
    Literal =.. [_,'$tptp_equal'(_,_)],
    !,
    reverse_unit_equality(input_clause(Name,Status,[Literal]),ReversedClause),
    reverse_unit_equalities(RestOfClauses,RestOfReversedClauses).

reverse_unit_equalities([FirstClause|RestOfClauses],[FirstClause|
RestOfReversedClauses]):-
    reverse_unit_equalities(RestOfClauses,RestOfReversedClauses).
%----------------------------------------------------------------------
%----Randomly reverse terms in unit equalities
randomly_reverse_unit_equalities([],[]).

%----If a unit equality and the random number says yeah, then reverse
randomly_reverse_unit_equalities([input_clause(Name,Status,[Literal])|
RestOfClauses],[ReversedClause|RestOfReversedClauses]):-
    Literal =.. [_,'$tptp_equal'(_,_)],
%----Cannot unify here as that might cause shit in the random number
%----generator (which might expect to produce what ever)
    tptp2X_random_integer(1,2,OneOrTwo),
    OneOrTwo == 1,
    !,
    reverse_unit_equality(input_clause(Name,Status,[Literal]),
ReversedClause),
    randomly_reverse_unit_equalities(RestOfClauses,RestOfReversedClauses).

%----Otherwise leave as is
randomly_reverse_unit_equalities([FirstClause|RestOfClauses],[FirstClause|
RestOfReversedClauses]):-
    randomly_reverse_unit_equalities(RestOfClauses,RestOfReversedClauses).
%----------------------------------------------------------------------
%----Depending on the option, rearrange the clauses accordingly
none(Clauses,Dictionary,none,Clauses,Dictionary,'').

%----For reversing literals in clauses
lr(InputClauses,Dictionary,lr,OutputClauses,Dictionary,'+lr'):-
    tptp_clauses(InputClauses),
    reverse_literals_in_clauses(InputClauses,OutputClauses).

%----For reversing CNF clause order
cr(InputClauses,Dictionary,cr,OutputClauses,Dictionary,'+cr'):-
    tptp_clauses(InputClauses),
    fast_reverse_list(InputClauses,[],OutputClauses).

%----For reversing clause and literal order
clr(InputClauses,Dictionary,clr,OutputClauses,Dictionary,'+clr'):-
    tptp_clauses(InputClauses),
    fast_reverse_list(InputClauses,[],IntermediateClauses),
    reverse_literals_in_clauses(IntermediateClauses,OutputClauses).

%----For reversing FOF formulae order
fr(InputFormulae,Dictionary,fr,OutputFormulae,Dictionary,'+fr'):-
    tptp_formulae(InputFormulae),
    fast_reverse_list(InputFormulae,[],OutputFormulae).

%----For randomly reordering literals and clauses
random(InputClauses,Dictionary,random,OutputClauses,Dictionary,'+ran'):-
    tptp_clauses(InputClauses),
    tptp2X_length(InputClauses,NumberOfInputClauses),
    randomize_clauses(InputClauses,NumberOfInputClauses,OutputClauses).

random(InputFormulae,Dictionary,random,OutputFormulae,Dictionary,'+ran'):-
    tptp_formulae(InputFormulae),
    tptp2X_length(InputFormulae,NumberOfInputFormulae),
    randomize_formulae(InputFormulae,NumberOfInputFormulae,OutputFormulae).

%----For reversing equalities in unit equality clauses
er(InputClauses,Dictionary,er,OutputClauses,Dictionary,'+er'):-
    tptp_clauses(InputClauses),
    reverse_unit_equalities(InputClauses,OutputClauses).

%----For randomly reversing equalities in unit equality clauses
ran_er(InputClauses,Dictionary,ran_er,OutputClauses,Dictionary,'+rer'):-
    tptp_clauses(InputClauses),
    randomly_reverse_unit_equalities(InputClauses,OutputClauses).
%----------------------------------------------------------------------
arrange_file_information(transform,none,'').
arrange_file_information(transform,lr,'Literals reversed').
arrange_file_information(transform,cr,'Clauses reversed').
arrange_file_information(transform,clr,'Clauses and literals reversed').
arrange_file_information(transform,random,
    'Clauses and literals randomly reordered').
arrange_file_information(transform,fr,'Formulae reversed').
arrange_file_information(transform,er,'Equality arguments reversed').
arrange_file_information(transform,ran_er,
'Equality arguments randomly reversed').
%----------------------------------------------------------------------