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]).
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

(*

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
(*

*)

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 = ()

```