
% Version 1.1-2

%1
% aggiunto filter_on
% aggiunto varie replace_rule per normalizzazione (per ora commentate)
% in r3 cambiato dinters con inters
% aggiunto parametro in equiv_rules

% 2
% aggiunto regola di inferenza per X is A - B


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% User-defined rewriting rules
% for {log} version 4.7.0-1 or newer
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%           by Maximiliano Cristia' and  Gianfranco Rossi
%                          April 2014
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

filter_on.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%% General rules %%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%% equivalence rules 

% equiv_rule(A,B), with A, B {log} predicates: if the input goal contains B then  
% then B matches with both filtering rules for A and filtering rules for B (since B => A)

% (TO BE REMOVED) N.B. conviene che le regole (in questo file) siano tutte per 
% subset mentre i goal contengono sia subset che esubset. Se nel goal c'e' subset 
% allora unifica con la regola senza bisogno della equiv_rule, mentre se nel
% goal c'e' esubset allora unifica con ebsubset tramite la equiv_rule

:- op(700,xfx,[ein,enin]).

equiv_rule(e2,inters(X,Y,Z),dinters(X,Y,Z)).     % e2. dinters(X,Y,Z) => inters(X,Y,Z)   
equiv_rule(e3,ssubset(X,Y),dssubset(X,Y)).       % e3. dssubset(X,Y) => ssubset(X,Y)   
equiv_rule(e4,nsubset(X,Y),dnsubset(X,Y)).       % e4. dnsubset(X,Y) => nsubset(X,Y)   
equiv_rule(e5,X in Y,X ein Y).                   % e5. X ein Y => X in Y   
equiv_rule(e6,X nin Y,X enin Y).                 % e6. X enin Y => X nin Y  
%TO BE COMPLETED: esubset, einters, ...


%%%%%%%%%%%%%%%%%%%%%%%% replace rules

% replace_rule(
%     W: when,
%     C: atomic constraint
%     C_Conds: list of conditions for C
%     D: list of other atomic constraints to be checked
%     D_Conds: list of conditions for atomic constraints in D and C
%     AddC: constraint to be replaced to C)
        
% X < Y -replace-> Y > X
replace_rule(initial(br1),X < Y,[var(X),var(Y)],[],[],Y > X).

% X =< Y -replace-> Y >= X
replace_rule(initial(br2),X =< Y,[var(X),var(Y)],[],[],Y >= X).

% t = X -replace-> X = t
replace_rule(initial(br3),T=X,[var(X),nonvar(T)],[],[],X=T).

% inters(X,{...},t3) -replace-> inters({...},X,t3)
replace_rule(initial(r3),inters(X,T2,T3),[var(X),nonvar(T2)],[],[],inters(T2,X,T3)).

%%%%%% not active yet (to be used to obtain a "normalized" form of goals to be processed)
%
% X = Y -replace-> X with Y everywhere
% replace_rule(initial(rr1),X=Y,[var(X),var(Y),X=Y],[],[],true).

% inters(t1,t2,{...}) -replace-> inters(t1,t2,X) & X = {...}
% replace_rule(initial(rr6),inters(T1,T2,T3),[nonvar(T3)],[],[],inters(T1,T2,X) & X = T3).

% inters(X,t2,t3) & X=t1 -replace-> inters(t1,t2,t3)
% replace_rule(initial(rr7),inters(X,T2,T3),[var(X)],
%                       [X1 = T1],[var(X1),nonvar(T1),X1==X],inters(T1,T2,T3)).

% inters(t1,Y,t3) & Y=t2 -replace-> inters(t1,t2,t3)
% replace_rule(initial(rr8),inters(T1,Y,T3),[var(Y)],
%                       [Y1 = T2],[var(Y1),nonvar(T2),Y1==Y],inters(T1,T2,T3)).

% t neq X -replace-> X neq t (t nonvar)
% replace_rule(initial(rr9),T neq X,[var(X),nonvar(T)],[],[],X neq T).

% X neq Y & Y = t -replace-> X neq t
% replace_rule(initial(rr11),X neq Y,[var(X),var(Y)],
%                        [Y1 = T],[var(Y1),nonvar(T),Y1==Y],X neq T).

% X neq Y & X = t -replace-> Y neq t
% replace_rule(initial(rr12),X neq Y,[var(X),var(Y)],
%                        [X1 = T],[var(X1),nonvar(T),X1==X],Y neq T).

%TO BE COMPLETED: subset, ssubset, ...


%%%%%%%%%%%%%%%%%%%%%%%% inference rules

% inference_rule(
%     W: when,
%     C: atomic constraint
%     C_Conds: list of conditions for C
%     D: list of other atomic constraints to be checked
%     D_Conds: list of conditions for atomic constraints in D and C
%     E: list of constraints in D to be NOT checked
%     AddC: constraint to be added)
        
%%%%% integers

% X > Y & Y > Z -add-> X > Z
inference_rule(initial,X > Y,[var(X),var(Y)],[Y1 > Z],[Y1==Y,Z\==X],[X > Y], X > Z).
        
% X >= Y & Y >= X -add-> X = Y
inference_rule(initial,X >= Y,[var(X),var(Y)],[Y1 >= X1],[Y1==Y,X1==X],[], X = Y).

% X is A - B & A > 0 & B > 0 & X > 0 -add-> A > B
inference_rule(initial,X is A - B,[var(X),var(A),var(B)],[A1 > 0, B1 > 0, X1 > 0],[A1==A,B1==B,X1==X],[], A > B).

%%%%% sets

% un(X,Y,Z) & disj(X,Z) -add-> X = {}
inference_rule(initial,un(X,Y,Z),[var(X),var(Y),var(Z)],[disj(X1,Z1)],[X1==X,Z1==Z],[], X = {}).

%%%%% lists

% length(L,N) & length(L,M) -add-> N = M
inference_rule(initial,length(L,N),[var(L)],[length(L1,M)],[L1==L],[length(L,N)], N = M).


%%%%%%%%%%%%%%%%%%%%%%%% fail rules

% fail_rule(
%     W: when,
%     C: atomic constraint
%     C_Conds: list of conditions for C
%     D: list of other atomic constraints to be checked
%     D_Conds: list of conditions for atomic constraints in D and C
%     E: list of constraints in D to be NOT checked)

% bf1. X > Y & Y > X
fail_rule(initial,X > Y,[],[V > W],[V==Y,W==X],[]).
% it works also for X > X

% bf2. X >= Y & Y > X 
fail_rule(initial,X >= Y,[],[V > W],[V==Y,W==X],[]).

% bf3. X in S & X nin S 
fail_rule(initial,X in S,[var(S)],[X1 nin S1],[X1==X,S1==S],[]).

% bf4. NotSubsetOfSingleton
% A neq {} & ssubset(A,{X})            
fail_rule(initial,ssubset(A,S),[nonvar(S),S={} with _X],[A1 neq E],[nonvar(E),E={},A1==A],[]).

% bf5. NatRangeNotEmpty
% X is Z+k & Y is Z+h & I = int(X,Y) & I = {}  and k =< h, k, h integer constants
fail_rule(initial,I=int(X,Y),[var(X),var(Y)],[X1 is Expr1,Y1 is Expr2,I=E],[nonvar(Expr1),Expr1=(Z+A),integer(A),nonvar(Expr2),Expr2=(Z1+B),integer(B),A=<B,nonvar(E),E={},X1==X,Y1==Y,Z1==Z],[]).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%% More specific rules %%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Add here other more specific user-defined rewriting rules

%%%%%%%%%%%%%%%%%%%%%%%% for the TTF
 
:- (exists_file('TTF_rules.pl'),!,consult('TTF_rules.pl') 
    ; 
    true).
