nonfix -- ++;

infix AND OR IMPLIES IMP IFF <=>;

functor BDD (structure Lib  : LIBBDD
	       and Proposition : PROPOSITIONSIG
	       and Lit2Var : DICTIONARY
	       and Var2Lit : DICTIONARY
	       sharing type Var2Lit.Key  = Lib.Var
	       sharing type Lit2Var.Key  = Proposition.Lit ): LOGICSIG
= struct
      open Lib Proposition
(*
    type Bdd = Lib.Bdd
    type Var = Lib.Var
    type Assoc = Lib.Assoc
    type Subst = Lib.Subst
    type Method = Lib.Method
    type Lit = Proposition.Lit
    val bdd_start = Lib.bdd_start
*)
      fun length [] = 0 |length (h :: t) = 1 + length t
(* From Lib     datatype 'a Option = None | Some of 'a *)
      val m = ref (None : Bddm Option) ;
      fun bdd_start () =  (Lib.bdd_start (); m := Some(bdd_init()))
      fun !% (ref(Some x)) = x
	| !% (ref None) = raise Error "Bdds not initialised"

      fun message s = ()  (*TextIO.print s;*)
(**)

      fun Assoc xs = bdd_new_assoc (!% m) xs

      fun Subst xs = bdd_new_subst (!% m) xs
	
      fun FALSE() = bdd_zero (!% m)

      fun TRUE () = bdd_one  (!% m)

      fun NEW ()  = bdd_new_var_first (!% m)

      val V = Lib.V : Var -> Bdd
      val I = Lib.I : Var -> int

      fun NOT x = 	  
	  let val r = bdd_not (!% m) x 
	  in bdd_free (!% m) x; r 
	  end;
	
      fun x AND y = 
	  let val r = bdd_and (!% m) x y
	  in bdd_free (!% m) x; bdd_free (!% m) y; r 
	  end;
		
      
      fun x INTERSECTS y = 
	  let val r = bdd_intersects (!% m) x y
	      val b = r <> bdd_zero (!% m)
	  in bdd_free(!% m) x;  bdd_free(!% m) y; bdd_free(!% m) r ;b
	  end;

      fun x IMPLIES y =
	  let val r = bdd_implies (!% m) x y
	      val b = r = bdd_zero (!% m)
	  in bdd_free(!% m) x; bdd_free(!% m) y; bdd_free(!% m) r ;b
	  end;
		
      fun x OR y = 
	  let val r = bdd_or (!% m) x y
	  in bdd_free (!% m) x; bdd_free (!% m) y; r 
	  end;

      fun ITE x y z = 
	  let val r = bdd_ite (!% m) x y z
	  in bdd_free (!% m) x; bdd_free (!% m) y; bdd_free (!% m) z; r 
	  end;

      fun x IMP y = 	  
	  let val r = bdd_ite (!% m) x y (bdd_one (!% m))
	  in bdd_free (!% m) x; bdd_free (!% m) y; r 
	  end;

      fun x IFF y = 
	  let val r = bdd_ite (!% m) x y (bdd_not (!% m) y)
	  in bdd_free (!% m) x; bdd_free (!% m) y; r 
	  end;

      fun EXISTS a f = 
	  let val () = bdd_assoc (!% m) a; 
	      val r = bdd_exists (!% m) f;
	  in bdd_free (!% m) f; r 
	  end;

      fun PROD a f g = 
	  let val () = bdd_assoc (!% m) a; 
	      val r = bdd_rel_prod (!% m) f g;
	  in bdd_free (!% m) f; bdd_free (!% m) g; r 
	  end;

      fun SUBST s f =
	  let val () = bdd_subst (!% m) s; 
	      val r = bdd_substitute (!% m) f;
	  in bdd_free (!% m) f; r 
	  end;

      fun SUPPORT f = bdd_support (!% m) f;

      fun SATISFY f = bdd_satisfy (!% m) f;
      fun SAT f =
	  let val FF = bdd_zero (!% m)
	      and TT = bdd_one (!% m)
	  in
	      if f = FF then None else
		  let
		      fun sats g = 
			  if g = TT then []
			  else if bdd_then (!% m) g = FF then sats (bdd_else (!% m) g)
			       else bdd_if (!% m) g :: sats (bdd_then (!% m) g)
		  in 
		      Some (sats f)
		  end
	  end
      (*   
       returns a list of variables such that making these true and all
       others false gives a satisfying assignment      
       *)

      fun FRACTION f = bdd_satisfying_fraction (!% m) f

      fun REDUCE f g = 
	  let val r = bdd_reduce (!% m) f g
	  in
	      bdd_free (!% m) f; bdd_free (!% m) g; r 
	  end;

      fun REORDER () = bdd_reorder (!% m);

      fun REORDERING method = bdd_dynamic_reordering (!% m) method

      fun GC () = bdd_gc (!% m);      
      fun STATS () = bdd_stats (!% m);      
      fun TOTALSIZE () = bdd_total_size (!% m);
      fun SIZE f = bdd_size (!% m) f false;
      fun SIZEMULTIPLE fs = bdd_size_multiple (!% m) fs false;

      fun ++ f = bdd_identity (!% m) f
	
      fun -- f = bdd_free (!% m) f 

      fun ANDL [] = TRUE ()
	| ANDL [p] = p
	| ANDL (p :: ps) = p AND ANDL ps
      fun ORL [] = FALSE ()
	| ORL [p] = p
	| ORL (p :: ps) = p OR ORL ps
      exception Triv;
      fun LANDL f ps =
	  let val FF = FALSE()
  	      fun emap [] = []
                | emap (p :: ps) =
	         let val fp = f p in
		     if fp = FF then 
                        raise Triv 
		     else fp :: emap ps
                 end
	  in
	      (ANDL (emap ps))handle Triv => FF
	  end

      fun LORL f ps =
	  let val TT = TRUE()
  	      fun emap [] = []
                | emap (p :: ps) =
	         let val fp = f p in
		     if fp = TT then 
                        raise Triv 
		     else fp :: emap ps
                 end
	  in
	      (ORL (emap ps))handle Triv => TT
	  end

      fun list 0 x = []
	| list n x = x :: list (n-1) x;
      (* returns list [ 0 true, 1 true, 2 true, ...., n true] *)
      fun countTrue n [] = TRUE() :: list n (FALSE())
	| countTrue n (h :: t) =
		let val prev = countTrue n t
	            fun red [n, m] = [ITE h n m]
		      | red (n :: (rest as (m :: xs))) = ITE (++h) n (++m) :: red rest
                in
		    red (FALSE() :: prev)
		end

      fun countFalse [] = [TRUE()]
      (* returns list of bdds [all False,(N-1)False,..,1 False,0 False] *)
      (* which is also [0 True, 1 True,.. , all True]                    *)
        | countFalse (h :: t) = 
		let val prev = countFalse t
	            fun red (n :: m :: xs) = ITE (++h) n (++m) :: red (m :: xs)
                      | red [n] = [h AND n]
                      | red [] = []
                in
		    red (FALSE() :: prev)
		end

      fun BDDLT n bdds = (* less than n true, which is 0 true --- (n-1) true *)
	  ORL (countTrue (n-1) bdds)
(*	let val FF = FALSE()
	    fun first n [] = FF
	      | first 0 xs = (map -- xs; FF)
              | first n (h :: t) = h OR first (n-1) t
	in  
	    first n (countFalse bdds) 
        end
*)
      fun BDDLE n bdds = (* less than n true, which is 0 true --- (n) true *)
	  ORL (countTrue n bdds)
(*	let val FF = FALSE()
	    fun first n [] = FF
	      | first 0 xs = (map -- xs; FF)
              | first n (h :: t) = h OR first (n-1) t
	in  
	    first (n+1) (countFalse bdds) 
        end
*)
      fun BDDEQ n bdds = (* exactly n true *)
        let val FF = FALSE()
	    fun nth _ [] = FF
              | nth 0 (h :: t) = (map -- t; h)
              | nth n (h :: t) = (-- h;nth (n-1) t)
        in
           nth n (countFalse bdds)
        end

      fun BDDGT n bdds = (* more than n true *)
        let fun drop _ [] = []
              | drop 0 xs = xs
              | drop n (h :: t) = (-- h;drop (n-1) t)
        in
           ORL (drop (n+1) (countFalse bdds))
        end  

      fun BDDGE n bdds = (* n or more true *)
        let fun drop _ [] = []
              | drop 0 xs = xs
              | drop n (h :: t) = (-- h;drop (n-1) t)
        in
           ORL (drop n (countFalse bdds))
        end

      (* tried this but no speedup on gripper-x-5
      local 
	  datatype Digit = Zero | One of Bdd

	  fun add f b [] = [One b]
	    | add f b (Zero::xs) = One b :: xs
	    | add f b (One x :: xs) = Zero:: add f (f(b,x)) xs
	  fun sum f e [] = e
	    | sum f e (Zero::xs) = sum f e xs
	    | sum f e (One x :: xs) = sum f (f(e,x)) xs
	  fun comb f [] xs = xs
	    | comb f (h :: t) xs = comb f t (add f h xs)
      in 
	  fun ANDL [] = TRUE ()
	    | ANDL [p] = p
	    | ANDL (p :: ps) = sum (op AND) p (comb (op AND) ps [])
	  fun ORL [] = FALSE ()
	    | ORL [p] = p
	    | ORL (p :: ps) = sum (op OR) p (comb (op OR) ps [])
      end
*)
      fun eval types constants v =
	  let val TT = TRUE()
              and FF = FALSE()
              fun ev T = TT
		| ev F = FF
		| ev (A x) = v x
		| ev (p && q) = 
			let val evp = ev p 
			in if evp = FF then FF 
			   else evp AND ev q
			end
		| ev (p || q) =
			let val evp = ev p 
			in if evp = TT then TT 
			   else evp OR ev q
			end
	        | ev (p ==> q) =
			let val evp = ev p 
			in if evp = FF then TT 
			   else evp IMP ev q
			end
	        | ev (p <=> q) = ev p IFF ev q
		| ev (&&& ps) = LANDL ev ps
		| ev (||| qs) = LORL  ev qs
		| ev (~ p) = NOT (ev p)
		| ev (ALL (vars, p)) = 
		  let val subs = substitutions types constants vars
		  in
		      LANDL (fn s => eval   types constants (v o (tr s)) p) subs
		  end
		| ev (EXS (vars, p)) = 
		  let val subs = substitutions types constants vars
		  in
		      LORL (fn s => eval   types constants (v o (tr s)) p ) subs
		  end
		| ev (LT ((n,vars), p)) = 
		  let val subs = substitutions types constants vars
		  in
		      BDDLT n (map (fn s => eval   types constants (v o (tr s)) p ) subs)
		  end
		| ev (LE ((n,vars), p)) = 
		  let val subs = substitutions types constants vars
		  in
		      BDDLE n (map (fn s => eval   types constants (v o (tr s)) p ) subs)
		  end
		| ev (GT ((n,vars), p)) = 
		  let val subs = substitutions types constants vars
		  in
		      BDDGT n (map (fn s => eval   types constants (v o (tr s)) p ) subs)
		  end
		| ev (EQ ((n,vars), p)) = 
		  let val subs = substitutions types constants vars
		  in
		      BDDEQ n (map (fn s => eval   types constants (v o (tr s)) p ) subs)
		  end
		| ev (GE ((n,vars), p)) = 
		  let val subs = substitutions types constants vars
		  in
		      BDDGE n (map (fn s => eval   types constants (v o (tr s)) p ) subs)
		  end
	  in
	      ev
	  end;

      local
	  val lit2var' = ref (Lit2Var.empty:Lib.Var Lit2Var.Dict)
	  val var2lit' = ref (Var2Lit.empty:Lit Var2Lit.Dict)
	  val nVars'   = ref 0
	  val noVars'  = ref(None : Bdd Option)
	  val allVars' = ref(None : Bdd Option)
      in	
	  fun bdd_restart () =
	      ((case !m of Some m => bdd_quit m
		  | None => ());
               message "\nReinitialising BDDs\n";
               m := Some(bdd_init());
	       lit2var' := Lit2Var.empty;
	       var2lit' := Var2Lit.empty;
	       nVars'   := 0;
	       noVars'  := Some (TRUE ());
	       allVars' := Some (FALSE()))

	  fun lit2var x = 
	      let val e = Lit2Var.lookup (!lit2var') x (* existing *)
		  handle Lit2Var.Lookup =>
		      let val n = NEW()
		      in 
			  nVars' := !nVars' + 1;
			  lit2var' := Lit2Var.enter ((x,n),! lit2var');
			  var2lit' := Var2Lit.enter ((n,x),! var2lit');
			  noVars'  := Some( !% noVars' AND NOT (++(V n)));
			  allVars' := Some( !% allVars' AND (++(V n)));
			  n
		      end
	      in
		  (++(V e);e)
	      end
	  fun var2lit v  = Var2Lit.lookup (!var2lit') v
	  fun noVars ()  = let val r = !% noVars' in ++r; r end
	  fun allVars () = let val r = !% allVars' in ++r; r end
	  fun nVars ()   = ! nVars'
	  fun STATES f   = let fun icount 0 m = m
                                 | icount n m = icount (n-1) (2 * m)
                               fun count 0 r = floor r
				 | count n r = count (n-1) (2.0 * r) 
						handle Prod => icount n (floor r)
			   in
			       count (!nVars') (FRACTION f)
			   end   	
	  fun rmLit x = let val v = lit2var x
			    val lit2var' = Lit2Var.remove (x, ! lit2var');
			    val var2lit' = Var2Lit.remove (v, ! var2lit');
			    val av = Assoc [v]
			in
			    nVars' := !nVars' - 1;
			    noVars' := Some(EXISTS av (!% noVars'));
			    allVars' := Some(EXISTS av (!% allVars'));
			    --(V v)
			end
	  fun rmVar v = let val x = var2lit v
			    val lit2var' = Lit2Var.remove (x, ! lit2var');
			    val var2lit' = Var2Lit.remove (v, ! var2lit');
			    val av = Assoc [v]
			in
			    nVars' := !nVars' - 1;
			    noVars' := Some(EXISTS av (!% noVars'));
			    allVars' := Some(EXISTS av (!% allVars'));
			    --(V v)
			end
      end

      fun symb f = 
	  if f = TRUE () then T else 
	      if f = FALSE () then F
	      else let val v = bdd_if (!% m) f
		       val vbl = A(var2lit v)
		   in
		       simp(
			    simp (vbl && symb (bdd_then (!% m) f))
			  ||
			    simp (~ vbl  && symb (bdd_else (!% m) f))
			    )
		   end

      fun LITWITHINDEX i = var2lit(bdd_var_with_index (!% m) i)
      fun CACHERATIO i = bdd_cache_ratio (!% m) i

      fun VO() = 
	  let val n = nVars()
	      fun pVars 0 = message("\n" ^ PolyML.makestring n ^ " variables")
		| pVars i = ( 
			     pVars (i-1);
			     message("\n"^lit2string (LITWITHINDEX (i-1)))
			     )
	  in
	      pVars n
	  end

  end;