
open "term";
open "gclause";
open "sort";

fun spliteval1 (GCLAUSE ([_, ...], [_])) = 1 (* preferred *)
  | spliteval1 (GCLAUSE ([_, ...], [_, ...])) = 2
  | spliteval1 (GCLAUSE (nil, [_, ...])) = 3
  | spliteval1 (GCLAUSE (_, nil)) = 4;

fun tsize (V _) = 1
  | tsize (_ $ l) = 1 + tlsize l
and tlsize nil = 0
  | tlsize (t::l) = tsize t + tlsize l;

fun gclause_size (GCLAUSE (neg, pos)) = tlsize neg + tlsize pos;

fun splitcmp (c, c') =
    let val p = spliteval1 c and p' = spliteval1 c'
    in
	p<p' orelse p=p' andalso
	let val s = gclause_size c and s' = gclause_size c'
	in
	    s<s'
	end
    end;

val split_sort = sort splitcmp;

	fun gclause_split (c as GCLAUSE (neg, pos)) =
	    let val eqvr = ref {}
		val sigr = ref {}
		val nsplits = ref 0 (* number of split subclauses so far. *)
		fun conc ((neg, pos), (neg', pos')) =
		    (neg U neg', pos U pos')
		fun concs ({}, c) = c
		  | concs ({x}, c) =
		    if x inset !eqvr
			then conc (c, ?(!eqvr) x)
		    else c
		  | concs (vars, c) =
		    let val (vars1, vars2) = split vars
		    in
			concs (vars1, concs (vars2, c))
		    end
		fun fuse (vars, c) =
		    let val c' = concs (vars, c)
		    in
			if c=c'
			    then (eqvr := !eqvr ++ {x => c' | x in set vars};
				  sigr := !sigr ++ {c' => vars};
				  inc nsplits)
			else let val vargroups = {?(!sigr) (?(!eqvr) x)
						 | x in set vars
						     such that x inset !eqvr}
				 val vars' = union vargroups U vars
			     in
				 eqvr := !eqvr ++ {x => c' | x in set vars'};
				 sigr := !sigr ++ {c' => vars'};
				 nsplits := !nsplits - card vargroups + 1
			     end
		    end
		fun somevar (V x) = SOME x
		  | somevar (_ $ l) =
		    some
		      x
		    | t in list l
		      val SOME x = somevar t
		    end
		fun sortsplit (negs, poss) =
		    GCLAUSE ([a | a in list neg such that a inset negs],
			       [a | a in list pos such that a inset poss])
		fun getsplits (al, negp) =
		    {(case somevar a of
			  SOME x => ?(!eqvr) x
			| NONE => if negp
				      then ({a}, {})
				  else ({}, {a}))
		    | a in list al}
	    in
		iterate
		  fuse (tvars a, ({a}, {}))
		| a in list neg
		end;
		iterate
		  fuse (tvars a, ({}, {a}))
		| a in list pos
		end;
		if !nsplits<=1
		    then [c]
		else let val splits =
				getsplits (neg, true) U getsplits (pos, false)
		     in
			 split_sort {sortsplit s | s in set splits}
		     end
	    end
;
