(*
 *  $ID: $
 *
 * 
 * CBG Squanderer ROBDD BDD toy package in SML.
 * (C) 2003 DJ Greaves.
 *
 * Look carefully at this code, it uses a hash tree to avoid replication of identical subtrees
 * but it still has a fatal flaw!  Dynamic programming must be added to the body of jb_apply.
 *
 * a) Explain the idea of dynamic programming
 * b) Explain what is wrong with the software in this file
 * c) Add a second array to act as a cache of computed subexpressions
 * d) Add a garbage collector for your new array. When should this be called ?
 * 
 *
 * Harder: Automatic re-ordering is frequently implemented in a bdd package.  How would
 * you go about adding this facility ? 
 *)


datatype jb_t = JB_false | JB_true | JB of int * int * bool ref * jb_t * jb_t
;


exception jb_sfault of string
;

val jb_current_marx = ref false
;

val jb_hash_base = 81973
;

val JB_TAB = Array.array(jb_hash_base, []);


fun 
  jb_level(JB_false) = 0 (* some systems may have this maxint instead *)
| jb_level(JB_true) = 0  
| jb_level(JB(lev, h, marx, hi, lo)) = lev
;

fun 
  jb_hash(JB_false) = 0  
| jb_hash(JB_true) = 1  
| jb_hash(JB(lev, h, marx, hi, lo)) = h
;


fun jb_hash_form(lev, hl, hr) =
	let val s = (lev * 4 + hl * 64 + hr)
	in s mod jb_hash_base
	end
;

fun 
  jb_scan(nil, lev, ll, lr) = NONE
| jb_scan(JB(l, h, marx, hi, lo)::tt, lev, ll, lr) = 
	if (lev=l andalso lo=ll andalso hi=lr) then SOME(JB(l, h, marx, hi, lo)) else jb_scan(tt, lev, ll, lr)
;


fun jb_gen(lev, ll, rr) = if (ll=rr) then ll else
    let val hl = jb_hash(ll)
	val hr = jb_hash(rr)
        val h = jb_hash_form(lev, hl, hr) 
	val ov = Array.sub(JB_TAB, h)
	val k = jb_scan(ov, lev, ll, rr)
	in if (k<> NONE) then valOf(k)
	else let val nv = JB(lev, h, ref(!jb_current_marx), ll, rr)
 		 val _ = Array.update(JB_TAB, h, nv::ov)
	in nv
	end end
;



fun jb_lo(JB(lev, h, marx, hi, lo)) = lo
 | jb_lo(_) = raise jb_sfault("jb_lo")
;

fun jb_hi(JB(lev, h, marx, hi, lo)) = hi
 | jb_hi(_) = raise jb_sfault("jb_hi")
;




fun 
  jb_and(JB_true, r) = r
| jb_and(r, JB_true) = r
| jb_and(r, JB_false) = JB_false
| jb_and(JB_false, r) = JB_false
| jb_and(_, _) = raise jb_sfault("jb_and")
;

fun 
  jb_or(JB_true, r) = JB_true
| jb_or(r, JB_true) = JB_true
| jb_or(r, JB_false) = r
| jb_or(JB_false, r) = r
| jb_or(_, _) = raise jb_sfault("jb_or")
;

fun jb_leaf(JB_true) = true
| jb_leaf(JB_false) = true
| jb_leaf(_) = false
;
  

(*
 * The first arg is the TRUE/hi one and the second is the FALSE/lo one.
 * This is the same way around as the traditional QUERY or MUX2.
 *)
fun jb_leaf_gen(l) = jb_gen(l, JB_true, JB_false)
;

fun 
  jb_not(JB_true) = JB_false
| jb_not(JB_false) = JB_true
| jb_not(JB(l, h, marx, hi, lo)) = jb_gen(l, jb_not(hi), jb_not(lo))
;


fun jb_xor(a, b) = 
    let val a1 = jb_apply(jb_and, a, jb_not(b))
        val b1 = jb_apply(jb_and, jb_not(a), b)
    in  jb_apply(jb_or, a1, b1)
    end
;
	
fun jb_apply(f, u1, u2) =
	if (jb_leaf(u1) andalso jb_leaf(u2)) then f(u1, u2)
	else 
	let val l1 = jb_level(u1)
	    val l2 = jb_level(u2)
	in if (l1=l2) then jb_gen(l1, jb_apply(f, jb_hi(u1), jb_hi(u2)), jb_apply(f, jb_lo(u1), jb_lo(u2)))
	else if (l1<l2) then jb_gen(l2, jb_apply(f, u1, jb_hi(u2)), jb_apply(f, u1, jb_lo(u2)))
	else jb_gen(l1, jb_apply(f, jb_hi(u1), u2), jb_apply(f, jb_lo(u1), u2))
	end
;

(*
 * Evaluate a bdd under a given substitution
 *)
fun 
  jb_restrict(JB_true, l, v) = JB_true
| jb_restrict(JB_false, l, v) = JB_false
| jb_restrict(JB(ll, h, marx, hi, lo), l, v) = 
	if (l < ll) then jb_gen(ll, jb_restrict(hi, l, v), jb_restrict(lo, l, v))
	else if (l > ll) then JB(ll, h, marx, hi, lo)
	else if (v) then hi else lo
;


(*
 * Existential quant \E x. P(x) implemented as P(0) \/ P(1)
 *)
fun jb_exists(lev, q) = jb_or(jb_restrict(q, lev, true),  jb_restrict(q, lev, false))
;

(*
 * Universal quant \E x. P(x) implemented as P(0) /\ P(1)
 *)
fun jb_forall(lev, q) = jb_and(jb_restrict(q, lev, true),  jb_restrict(q, lev, false))
;
  

(*
 * Existential quantifier: BDDs are efficient at quantifying over a number of variables
 * at once.  We can conveniently represent a list of variables with the BDD for their conjunction, so that
 * the list is in the correct order to perform over the whole list with a single walk of the tree.
 *)
fun
  jb_exists(JB_true, b) = b
| jb_exists(_, JB_true) = JB_true
| jb_exists(_, JB_false) = JB_false
| jb_exists(a, b) = 
	let val la = jb_level(a)
	    val lb = jb_level(b)
	in if (la>lb) then jb_exists(jb_hi(a), b)
	else if (la=lb) then jb_apply(jb_orf, jb_exists(jb_hi(a), jb_hi(b)), 
			                      jb_exists(jb_hi(a), jb_lo(b)))
	else jb_gen(lb, jb_exists(a, jb_hi(b)), jb_exists(a, jb_lo(b)))
	end
;


(* The jb_forall routine is the same as jb_exists with then jb_orf changed to jb_andf *)

fun
  jb_fold(JB_true, f, cc) = cc
| jb_fold(JB_false, f, cc) = cc
| jb_fold(JB(lev, h, marx, hh, ll), f, cc) = f(lev, jb_fold(hh, f, jb_fold(ll, f, cc)))
;



fun 
  jb_truth(JB_true) = true
| jb_truth(_) = false
;

fun 
  jb_invalid(JB_false) = true
| jb_invalid(_) = false
;




(* Garbage Collector - it is necessary to call the garbage collector from time to time *)


fun 
   jb_garb_mark_scan(JB_true) = ()
|  jb_garb_mark_scan(JB_false) = ()
|  jb_garb_mark_scan(JB(lev, h, marx, hi, lo)) =
	if (!marx)=(!jb_current_marx) then ()
	else (
		marx := (!jb_current_marx);
		jb_garb_mark_scan(lo);
		jb_garb_mark_scan(hi);
		()
	)
;


fun jb_garb_sweep(n:int) = 
	if (n >= jb_hash_base) then ()
	else
    let val ov = Array.sub(JB_TAB, n)
	fun jb_garb_sweep1(nil) = nil
	    | jb_garb_sweep1(JB(l, h, marx, hi, lo)::tt) = 	
		if ((!marx)=(!jb_current_marx)) then JB(l, h, marx, hi, lo)::jb_garb_sweep1(tt)
		else jb_garb_sweep1(tt)
	val nv = jb_garb_sweep1(ov)
	val _ = Array.update(JB_TAB, n, nv)
	val _ = jb_garb_sweep(n+1)
	in ()
	end
;

val jb_gc_timer = ref 0;


(*
 * l is a list of things we wish to keep.
 *)
fun jb_garbage(l) =
	if (!jb_gc_timer = 0) then
	(
	jb_current_marx := not(!jb_current_marx);
	app jb_garb_mark_scan l;
	jb_garb_sweep(0);
	jb_gc_timer := 40	
	)
	else jb_gc_timer := (!jb_gc_timer - 1)
;


(* eof *)