(*
 *  This file is a component of PropPlan - a model-based planner
 *  Copyright (C) 2000-2007  Michael Paul Fourman
 *  homepages.inf.ed.ac.uk/mfourman/tools/propplan
 *  sourceforge.net/projects/propplan
 *  michael.fourman (AT) gmail.com
 *
 *  This program is free software: you can redistribute it and/or modify
 *  it under the terms of version 3 of the GNU Affero General Public License
 *  as published by the Free Software Foundation.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *  GNU Affero General Public License for more details.
 *
 *  You should have received the file COPYING, a copy of the GNU Affero 
 *  Public License, along with this program.  
 *  If not, see <http://www.gnu.org/licenses/>.
 
 *  $Id: BUDDYLOGIC.ML,v 1.3 2007/12/31 19:56:32 michaelfourman Exp $
 *)

infix 2 ==>
infix 3 OR ||
infix 4 AND &&
infix 5 == <=> <>
infix 3 OR
infix 4 AND
infix 5 IMP IFF INTERSECTS IMPLIES;
nonfix -- ++;

functor BUDDYLOGIC (structure Lib  : BUDDY
	       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
(*  this provides the following types and value specified in LOGICSIG:
    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
*)

(* some alternative names *)
      val bdd_if      = bdd_var
      and bdd_then    = bdd_high
      and bdd_else    = bdd_low
      and bdd_free    = bdd_delref
      and bdd_implies = bdd_imp
      and bdd_reduce  = bdd_simplify
      and bdd_satisfy = bdd_satone

      fun length [] = 0 |length (h :: t) = 1 + length t
      datatype 'a Option = None | Some of 'a
  
      fun message s = ()  (*TextIO.print s;*)

      fun Vars xs = Vs xs

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

      fun NOT x = 	  
	  let val r = bdd_addref (bdd_not x)
	  in bdd_free x; r 
	  end;
	
      fun x AND y = 
	  let val r = bdd_addref (bdd_and x y)
	  in bdd_free  x; bdd_free  y; r 
	  end;
		
      fun x INTERSECTS y = 
	  let val b = x AND y
              val r = b <> FALSE ()
	  in 
	      bdd_free b; r
	  end;
		
      fun x OR y = 
	  let val r = bdd_addref (bdd_or  x y)
	  in bdd_free  x; bdd_free  y; r 
	  end;

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

      fun x IMP y = 	  
	  let val r = bdd_addref (bdd_ite  x y (bdd_false ()))
	  in bdd_free  x; bdd_free  y; r 
	  end;

      fun x IMPLIES y = 
	  let val b = x IMP y
              val r = b = TRUE ()
	  in 
	      bdd_free b; r
	  end;

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

      fun EXISTS a f = 
	  let val r = bdd_addref (bdd_exist f a)
	  in bdd_free f; r 
	  end;

      fun PROD a f g = 
	  let val r = bdd_addref (bdd_relprod f g a)
	  in bdd_free f; bdd_free g; r 
	  end;

      fun SUBST s f = 
	  let val a = bdd_setbddpairs s; 
	      val r = bdd_addref (bdd_veccompose f a)
	  in bdd_free f; bdd_freepair a; r 
	  end;

      fun SUPPORT f = 
      	  let fun supp b = if b = FALSE() orelse b = TRUE() then []
              else bdd_if b :: supp(bdd_then b) @ supp(bdd_else b)
              val sf = bdd_addref(bdd_support f)
              val r = supp sf
          in  
              bdd_free sf; r
          end

      fun SATISFY f = bdd_satisfy f;

(*      fun FRACTION f = bdd_satis f *)

      fun REDUCE f g = 
	  let val r = bdd_addref (bdd_reduce f g)
	  in
	      bdd_free f; bdd_free g; r 
	  end;

      fun REORDER () = bdd_reorder (DEFAULT_REORDERING);(* make this adjustable later *)

      fun REORDERING m = (bdd_autoreorder m; ())

      fun GC () = bdd_gbc ();      
      (*fun STATS () = bdd_stats ();      *)
      fun TOTALSIZE () = bdd_getnodenum ();
      fun SIZE f = bdd_nodecount f;

      fun ++ f = bdd_addref f
	
      fun -- f = (bdd_delref 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 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 *)
	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-1) true *)
	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 isGoal isInit 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 isGoal isInit 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 isGoal isInit types constants (v o (tr s)) p ) subs
		  end
		| ev (GOAL p) = isGoal (ev p)
                | ev (INIT p) = isInit (ev p)
		| ev (LT ((n,vars), p)) = 
		  let val subs = substitutions types constants vars
		  in
		      BDDLT n (map (fn s => eval isGoal isInit 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 isGoal isInit 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 isGoal isInit 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 isGoal isInit 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 isGoal isInit 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   (* number used = index of next to use *)
	  val noVars'  = ref (TRUE ())
	  val allVars' = ref (TRUE ())
          val nodesize = 500000
          and cachesize= 10000
      in	
	  fun bdd_restart () =
	      (message "\nReinitialising BDDs\n";
               bdd_start ();
               if not (bdd_isrunning()) then bdd_init {nodesize=nodesize, cachesize=cachesize} else true;
	       (*bdd_setvarnum 20;*)
	       lit2var' := Lit2Var.empty;
	       var2lit' := Var2Lit.empty;
	       nVars'   := 0;
	       noVars'  := TRUE ();
	       allVars' := TRUE ())

	  fun lit2var x = 
	      let val e = Lit2Var.lookup (! lit2var') x (* existing *)
		  handle Lit2Var.Lookup =>
		     let val n =  !nVars' in
		          if n = bdd_varnum () then bdd_extvarnum 1 else n;
			  nVars'   := n + 1;
			  lit2var' := Lit2Var.enter ((x,Var n),! lit2var');
			  var2lit' := Var2Lit.enter ((Var n,x),! var2lit');
			  noVars'  := ! noVars' AND NOT (++(V (Var n)));
			  allVars' := ! allVars' AND (++(V (Var n)));
			  Var 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   = 42 	(*????????*)
	  fun rmLit x = let val v = lit2var x
			    val lit2var' = Lit2Var.remove (x, ! lit2var');
			    val var2lit' = Var2Lit.remove (v, ! var2lit');
			    val av = Vars [v]
			in
			    nVars' := !nVars' - 1;
			    noVars' := EXISTS av (! noVars');
			    allVars' := 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 = Vars [v]
			in
			    nVars' := !nVars' - 1;
			    noVars' := EXISTS av (! noVars');
			    allVars' := 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 f
		       val vbl = A(var2lit v)
		   in
		       simp(
			    simp (vbl && symb (bdd_then f))
			  ||
			    simp (~ vbl  && symb (bdd_else f))
			    )
		   end

      fun LITWITHINDEX i = var2lit(Var i) 
      fun CACHERATIO i = bdd_setcacheratio i
      fun VO () =  ()
(*      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;