%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*- fundamental -*-
% fftwgel_simdvectorization_verification.pl		
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Description:	The code in this module can be used for proving that a 
%		sequence of SIMD instructions is not equivalent to a 
%		sequence of scalar instructions, which is useful in the
%		context of verifying a solution of the vectorization process.
% Language:	SICStus Prolog 3
% Copyright:	2003, Stefan Kral
% Author: 	Stefan Kral (URL mailto:skral@complang.tuwien.ac.at)
% License:	GNU General Public License (GPL) Version 2 (or higher)
% History:	Fri Feb 21 12:00:26 CET 2003: created
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- block scalarinstrsForSIMDInstrs(-,-,?).
scalarinstrsForSIMDInstrs([]) -->
   [].
scalarinstrsForSIMDInstrs([X|Xs]) -->
   scalarinstrsForSIMDInstr(X),
   scalarinstrsForSIMDInstrs(Xs).

:- block scalarinstrsForSIMDInstr(-,-,?).
scalarinstrsForSIMDInstr(simd_load2(P1,A1,X1,P2,A2,X2,D1+D2)) -->
   { validSplitAccessPair_(P1, P2) },
   [load(P1,A1,X1,D1), load(P2,A2,X2,D2)].
scalarinstrsForSIMDInstr(simd_load2(P1,A,X,P2,A,X,D1+D2)) -->
   { validInterleavedAccessPair_(P1, P2) },
   [load(P1,A,X,D1), load(P2,A,X,D2)].
scalarinstrsForSIMDInstr(simd_store2(S1+S2,P1,A1,X1,P2,A2,X2)) -->
   { validSplitAccessPair_(P1, P2) },
   [store(S1,P1,A1,X1), store(S2,P2,A2,X2)].
scalarinstrsForSIMDInstr(simd_store2(S1+S2,P1,A,X,P2,A,X)) -->
   { validInterleavedAccessPair_(P1, P2) },
   [store(S1,P1,A,X), store(S2,P2,A,X)].
scalarinstrsForSIMDInstr(simd_unaryop2(Op1,Op2,S1+S2,D1+D2)) -->
   [unaryop(Op1,S1,D1), unaryop(Op2,S2,D2)].
scalarinstrsForSIMDInstr(simd_unaryop1(P, Op, S12, D12)) -->
   scalarinstrsForSIMDUnaryOp1(P, Op, S12, D12).
scalarinstrsForSIMDInstr(simd_binop2(BType, Op1, Op2, Xl+Xh, Yl+Yh, D1+D2)) -->
   { binop_binop_bindingtypes(Op1, Op2, BTypes) },
   { member_of(BType, BTypes) },
   { bindingtype_(BType, S1, S2, T1, T2, Xl, Xh, Yl, Yh) },
   [binop(Op1,S1,S2,D1), binop(Op2,T1,T2,D2)].
scalarinstrsForSIMDInstr(simd_binop2(acc, Op, Op, S1+S2, D2+0, D1+D2)) -->
   { binop_binop_bindingtypes(Op, Op, BTypes) },
   { member_of(acc, BTypes) },
   [binop(Op,S1,S2,D1)].
scalarinstrsForSIMDInstr(simd_binop2(acc, Op, Op, D1+0, S1+S2, D1+D2)) -->
   { binop_binop_bindingtypes(Op, Op, BTypes) },
   { member_of(acc, BTypes) },
   [binop(Op,S1,S2,D2)].
scalarinstrsForSIMDInstr(simd_load1(P,A,X,D+0)) -->
   [load(P,A,X,D)].

scalarinstrsForSIMDUnaryOp1(lo, Op, S1+D2, D1+D2) -->
   [unaryop(Op,S1,D1)].
scalarinstrsForSIMDUnaryOp1(hi, Op, D1+S2, D1+D2) -->
   [unaryop(Op,S2,D2)].