raw
ffa_ch2_logicals.kv     1 with W_Pred; use W_Pred;
ffa_ch2_logicals.kv     2 
ffa_ch2_logicals.kv     3 
ffa_ch2_logicals.kv     4 package body FZ_Pred is
ffa_ch2_logicals.kv     5    
ffa_ch2_logicals.kv     6    ---------------------------------------------------------------------------
ffa_ch2_logicals.kv     7    -- Fundamental Predicate Operations on FZ (finite integers)
ffa_ch2_logicals.kv     8    ---------------------------------------------------------------------------
ffa_ch2_logicals.kv     9    
ffa_ch2_logicals.kv    10    -- 1 iff N == 0 (branch-free); else 0
ffa_ch2_logicals.kv    11    function FZ_ZeroP(N : in FZ) return WBool is
ffa_ch2_logicals.kv    12       A : WBool := 1;
ffa_ch2_logicals.kv    13    begin
ffa_ch2_logicals.kv    14       for i in N'Range loop
ffa_ch2_logicals.kv    15          A := A and W_ZeroP(N(i));
ffa_ch2_logicals.kv    16       end loop;
ffa_ch2_logicals.kv    17       return A;
ffa_ch2_logicals.kv    18    end FZ_ZeroP;
ffa_ch2_logicals.kv    19    pragma Inline_Always(FZ_ZeroP);
ffa_ch2_logicals.kv    20    
ffa_ch2_logicals.kv    21    
ffa_ch2_logicals.kv    22    -- 1 iff N is odd
ffa_ch2_logicals.kv    23    function FZ_OddP(N : in FZ) return WBool is
ffa_ch2_logicals.kv    24    begin
ffa_ch2_logicals.kv    25       return W_OddP(N(N'First));
ffa_ch2_logicals.kv    26    end FZ_OddP;
ffa_ch2_logicals.kv    27    pragma Inline_Always(FZ_OddP);
ffa_ch2_logicals.kv    28    
ffa_ch2_logicals.kv    29 end FZ_Pred;