PUBS: A Practical Upper Bounds Solver

(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 *
 * File:
 *   bitvectors.raml
 *
 * Author:
 *   Jan Hoffmann (2010)
 *
 * Resource Bound:
 *   O(n^2)
 *
 * Description:
 *   A library for bit vectors.
 *    
 *   A bit vector is an integer list of 0's and 1's.  The first value in
 *   the list is the least significant bit.  For example [1,0] is 1 and
 *   [0,1] is 2.  We interpret the empty list as zero., i.e., [] =
 *   [0].
 *
 *   We a assume an arbitrary but fixed word length (e.g. 32 bit) for the
 *   vectors.
 *    
 *   The library contains the following functions.
 *    
 *     - add(b1,b2): addition b1+b2 of two bit vectors b1 b2.  Can produce an
 *          overflow.
 *    
 *     - sub(b1,b2): subtraction of b2 from b1 (b1-b2).  Returns [0,...,0] if the
 *               result is negative.
 *
 *     - compare(b1,b2): -1 if b1 is less then b2, 0 if b1 is equal to b2,
                and 1 if b1 is greater then b2.
 *    
 *     - leq(b1,b2): b1 < b2 ?
 *    
 *     - mult(b1,b2): multiplication of two bit vectors
 *    
 *     - Div(b1,b2): division of b1 by b2.  The result is undefined in case
 *               of division by zero. (The function name is upper case
 *               since div is a RAML key word.)
 *
 *)

mult : (L(int),L(int)) -> L(int)
(* Multiplies two bit vectors. *)

mult (b1,b2) = let _=tick(1) in
                match b1 with
                 | nil -> nil
                 | (x::xs) -> let zs = +0::mult(xs,b2) in
                              if x == 1 then add(b2,zs) else zs;


mult3 : (L(int),L(int),L(int)) -> L(int)
mult3 (b1,b2,b3) = let _=tick(1) in 
                    mult(mult(b1,b2),b2); 
(*
eq(mult3(A,B,C),1,[mult(A,B),mult(A,B)],[]).
eq(mult(B1,B2),1,[],[B1=0]). 
eq(mult(B1,B2),1,[mult(B1s,B2)],[B1>=1,B1s = B1-1,Zs >=1+B1s]). 
eq(mult(B1,B2),1,[mult(B1s,B2),add(B2,Zs)],[B1>=1,B1s = B1-1,Zs =< B1s+1]). 

eq(out_mult(B1,B2),0,[],[B1=0]). 
eq(out_mult(B1,B2),1,[out_mult(B1s,B2)],[B1>=1,B1s=B1-1]). 
eq(out_mult(B1,B2),0,[out_mult(B1s,B2),outadd(B2,Zs)],[B1>=1,B1s=B1-1,Zs=<
B1s+1]). 

*)

bitToInt : L(int) -> int
(* Converts a bit vector into an integer. *)

bitToInt b = let _=tick(1) in
             bitToInt'(b,+1);


add : (L(int),L(int)) -> L(int)
(* Addition of two bit vectors.*) 

add (b1,b2) = let _=tick(1) in
              add' (b1,b2,+0);

(*
eq(add(B1,B2),1,[addp(B1,B2,I)],[I=0]).

eq(bitToInt(A),1,[bitToIntp(A,I)],[I=1]).

*)

bitToInt' : (L(int),int) -> int
(* Converts a bit vector into an integer. *)

bitToInt' (b,n) = let _=tick(1) in 
                 match b with
       		 | nil -> +0
                 | (x::xs) -> x*n + bitToInt'(xs,n*2);
(*
eq(bitToIntp(B,N),1,[],[B=0]).
eq(bitToIntp(B,N),1,[bitToIntp(Bs,M)],[B>=1,Bs=B-1,M=N*2]).
*)

add' : (L(int),L(int),int) -> L(int)
(* Helper function for the addition that takes care of the carryover. *)

add' (b1,b2,r) = let _=tick(1) in
                  match b1 with
                    | nil -> nil
                    | (x::xs) -> match b2 with 
		    	           | nil -> nil
                                   | (y::ys) -> let (z,r') = sum(x,y,r) in
				                z::add'(xs,ys,r');
(*
eq(addp(B1,B2,R),1,[],[B1=0]).
eq(addp(B1,B2,R),1,[],[B1>=1,B2=0]).
eq(addp(B1,B2,R),1,[sum(X,Y,R),addp(B1s,B2s,Rs)],[B1>=1,B2>=1,B1s=B1-1,B2s=B2-1]).
 
*)

sum : (int,int,int) -> (int,int)
(* Helper function for add' that computes the new bit and the new carryover. *)

sum (x,y,r) = let _=tick(1) in
              let s = x + y + r in
              if s == 0 then (+0,+0)
              else if s == 1 then (+1,+0)
              else if s == 2 then (+0,+1)
              else (+1,+1);

(*
   eq(sum(X,Y,R),1,[],[]).
*)

sub : (L(int),L(int)) -> L(int)
(* Subtraction of two bit vectors.
 *)

sub (b1,b2) = let (b,_) = sub'(b1,b2,+0) in b;

sub' : (L(int),L(int),int) -> (L(int),int)
(* Helper function of sub that deals with the carryover.
 *)
sub' (b1,b2,r) =  let _=tick(1) in
                  match b1 with
                    | nil -> (nil,r)
                    | (x::xs) -> match b2 with 
		    	           | nil -> (nil,r)
                                   | (y::ys) -> let (z,r') = diff(x,y,r) in
				                let (zs,s) = sub'(xs,ys,r') in
                                                (if s == 1 then +0::zs else z::zs,s);

(*
eq(subp(B1,B2,R),1,[],[B1=0]).
eq(subp(B1,B2,R),1,[],[B1>=1,B2=0]).
eq(subp(B1,B2,R),1,[diff(X,Y,R),subp(B1s,B2s,Rp)],[B1>=1,B2>=1,B1s=B1-1,B2s=B2-1]).

*)

diff : (int,int,int) -> (int,int)
(* Helper function for sub' that computes the new bit and the new carryover. *)

diff(x,y,r) = let _=tick(1) in 
              ( x+y+r mod 2,if x - y - r < 0 then +1 else +0 );

(*
eq(diff(A,B,C),1,[],[]).
*)

leq : (L(int),L(int)) -> bool

leq (b1,b2) = (compare(b1,b2)) < 1;

(*
eq(leq(B1,B2),0,[compare(B1,B2)],[B1>=0,B2>=0]).
*)

compare : (L(int),L(int)) -> int
(* Returns 0 if both arguments are equal,
           -1 if the first argument is smaller,
           1 if the first argument is greater then the second        
*)

compare (b1,b2) = let _=tick(1) in
                  match b1 with
                  | nil -> +0
                  | (x::xs) -> match b2 with
                                | nil -> +0
                                | (y::ys) -> let r = compare (xs,ys) in
				    	     if r == 0 then if xy then +1 else +0
                                             else r;
(*
eq(compare(B1,B2),1,[],[B1=0]).
eq(compare(B1,B2),1,[],[B1>=1,B2=0]).
eq(compare(B1,B2),1,[compare(B1s,B2s)],[B1>=1,B2>=1,B1s=B1-1,B2s=B2-1]).
*)

main = ()