(* Zero-suppressed BDDs.
   Copyright (C) 2008 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 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 General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

fun ZBDDnode (_, F0, Z) = F0
  | ZBDDnode (x, F0, F1) = N (x, F0, F1);

fun ZBDDmake x = N (x, Z, I);

fun sless less =
    fn (P Phi, P Phi') => less (Phi, Phi')
     | (P Phi, M Phi') => Phi=Phi' orelse less (Phi, Phi')
     | (M Phi, P Phi') => less (Phi, Phi')
     | (M Phi, M Phi') => less (Phi, Phi')

fun ZBDDops less =
    let (* subset1 (F, x) returns the subset of F consisting of all those
	 sets containing x *)
	memofun subset1 (Z, _) = Z
	      | subset1 (I, _) = Z
	      | subset1 (N (x', F0, F1), x) =
		if x'=x
		    then F1
		else if less (x',x')
			 then ZBDDnode (x', subset1 (F0, x),
					subset1 (F1, x))
		else Z

	(* subset0 (F, x) returns the subset of F consisting of all those
	 sets not containing x *)	 
	memofun subset0 (Z, _) = Z
	      | subset0 (I, _) = I
	      | subset0 (F as N (x', F0, F1), x) =
		if x'=x
		    then F0
		else if less (x',x')
			 then ZBDDnode (x', subset0 (F0, x),
					subset0 (F1, x))
		else F

	(* compute the union of two sets *)
	memofun union (Z, F') = F'
	      | union (F, Z) = F
	      | union (I,I) = I
	      | union (I, N (x', F'0, F'1)) =
		ZBDDnode (x', union (I, F'0), F'1)
	      | union (N (x, F0, F1), I) =
		ZBDDnode (x, union (F0, I), F1)
	      | union (F as N (x, F0, F1), F' as N (x', F'0, F'1)) =
		if x=x'
		    then if F = F'
			     then F (* optimization *)
			 else ZBDDnode (x, union (F0, F'0), union (F1, F'1))
		else if less (x,x')
			 then ZBDDnode (x, union (F0, F'), F1)
		     else ZBDDnode (x', union (F, F'0), F'1)

	(* hasI(F)=I whenever the empty set is an element of F,
	 Z otherwise. *)
	fun hasI I = I
	  | hasI Z = Z
	  | hasI (N (_, F0, _)) = hasI F0

	(* compute the intersection of two sets *)
	memofun inter (Z, _) = Z
	      | inter (_, Z) = Z
	      | inter (I, F') = hasI F'
	      | inter (F, I) = hasI F
	      | inter (F as N (x, F0, F1), F' as N (x', F'0, F'1)) =
		if x=x'
		    then if F=F'
			     then F (* optimization *)
			 else ZBDDnode (x, inter (F0, F'0), inter (F1, F'1))
		else if less (x,x')
			 then inter (F0, F')
		     else inter (F, F'0)

	(* compute the set of all unions s1 U s2, where s1 is in
	 the first set and s2 is in the second. *)
	memofun shuffle (Z, _) = Z
	      | shuffle (_, Z) = Z
	      | shuffle (I, F') = F'
	      | shuffle (F, I) = F
	      | shuffle (F as N (sPhi, F0, F1), F' as N (sPhi', F'0, F'1)) =
		if sPhi = sPhi'
		    then
			if F=F'
			    then F (* optimization *)
			else TDDnode (sPhi,
				      shuffle (F0, F'0),
				      union (shuffle (F0, F'1),
					     union (shuffle (F1, F'0),
						    shuffle (F1, F'1))))
		else if sPhi sl sPhi'
			 then TDDnode (sPhi, shuffle (F0, F'), shuffle (F1, F'))
		     else TDDnode (sPhi', shuffle (F, F'0), shuffle (F, F'1))

	fun replace (F, sPhi, F') =
	    union (subset0 (F, sPhi),
		   shuffle (subset1 (F, sPhi), F'))

	(* wfilter (F,F') returns the set of all paths in F that are not weakenings of
	 some paths in F' *)
	memofun wfilter (Z, _) = Z
	      | wfilter (F, Z) = F
	      | wfilter (_, I) = Z
	      | wfilter (I, F') =
		(case hasI F' of I => Z | Z => I)
	      | wfilter (F as N (sPhi, F0, F1), F' as N (sPhi', F'0, F'1)) =
		if sPhi = sPhi'
		    then if F=F'
			     then Z (* optimization *)
			 else TDDnode (sPhi, wfilter (F0, F'0),
				       wfilter (F1, union (F'0, F'1)))
		else if sPhi sl sPhi'
			 then TDDnode (sPhi, wfilter (F0, F'),
				       wfilter (F1, F'))
		     else wfilter (F, F'0)

	(* sfilter (F,F') returns the set of all paths in F that are not strengthenings
	 (subpaths) of paths in F' *)
	memofun sfilter (Z, _) = Z
	      | sfilter (F, Z) = F
	      | sfilter (I, _) = Z
	      | sfilter (N (sPhi, F0, F1), I) = TDDnode (sPhi, sfilter (F0, I), F1)
	      | sfilter (F as N (sPhi, F0, F1), F' as N (sPhi', F'0, F'1)) =
		if sPhi=sPhi'
		    then if F=F'
			     then Z (* optimization *)
			 else TDDnode (sPhi, sfilter (F0, union (F'0, F'1)),
				       sfilter (F1, F'1))
		else if sPhi sl sPhi'
			 then TDDnode (sPhi, sfilter (F0, F'),
				       F1)
		     else sfilter (F, union (F'0, F'1))

	memofun subtab (Z, _) = true
	      | subtab (_, Z) = false
	      | subtab (I, I) = true
	      | subtab (I, N (_, F0, _)) = subtab (I, F0)
	      | subtab (N _, I) = false
	      | subtab (F as N (sPhi, F0, F1), N (sPhi', F'0, F'1)) =
		if sPhi=sPhi'
		    then subtab (F0, F'0) andalso subtab (F1, F'1)
		else if sPhi sl sPhi'
			 then false
		     else subtab (F, F'0)
    in
	|[subset1 = subset1,
	   subset0 = subset0,
	   union = union,
	   inter = inter,
	   shuffle = shuffle,
	   replace = replace,
	   wfilter = wfilter,
	   sfilter = sfilter,
	   subtab = subtab
	   ]|
    end;

exception TDDITER;

fun TDDiter f =
    let fun iter (I, p) = f p
	  | iter (Z, p) = raise TDDITER (* fail *)
	  | iter (N (sPhi, F0, F1), p) =
	    iter (F0, p) handle TDDITER => iter (F1, sPhi::p)
    in
	fn t => iter (t,nil)
    end;

fun pathtoTDD p = (* build TDD corresponding to a given path, as a list passed
		   to f by TDDiter above (with deeper kernels before) *)
    let fun tdd (nil,r) = r
	  | tdd (a::l, r) = tdd (l, N (a, Z, r))
    in
	tdd (p, I)
    end
