(* Resolution prover on h1 clauses.
   Copyright (C) 2003 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.
*)

open "clause_h";
open "heap_h";
open "verbose_h";
open "rel_h";
open "sort_h";
open "scc_h";
open "topsort_h";

(*
val compute_toprels = false; (* sometimes a bit faster, sometimes much too slow to compute. *)
*)

fun head_vars (HVAR _) = {1}
  | head_vars (HFUN (_, _, _, xs, _)) = xs
  | head_vars _ = {};

fun al_vars al = union {tvars t
		       | (_, t) in list al};

fun clause_vars (CL (h, ql, al, Bs, ...)) =
    head_vars h U
    al_vars al U
    dom Bs;

(* Clause printing functions: *)

fun print_q (f as |[put, ...]|) q =
    let val delimr = ref "ne("
    in
	iterate
	  (put (!delimr); delimr := "_&_"; put P)
	| P in set q
	end;
	put ")"
    end;

exception PrintVarNotInEnv of int;

fun print_head (f as |[put, ...]|, xname, vars) =
    let val pdterm1 = print_term (f, vars)
	val pq = print_q f
	fun phead (HVAR P) = (put P; put " "; pdterm1 (V 1))
	  | phead (HFUN (P, f, k, xs, t)) =
	    (put P; put " "; pdterm1 t)
	  | phead (HQ q) = pq q
	  | phead (HBOT name) = put name
    in
	phead
    end;

fun clause_var_names xname =
    let val f as |[convert, put, seek, ...]| = outstring xname
	val n = size xname
    in
	fn c =>
	   {i => (seek n;
		  print f (pack i);
		  convert ())
	   | i in set clause_vars c}
    end;

fun perr_by pi =
    (#put stderr "   ";
     (case pi of
	  P_GIVEN "<recipe>" => ()
	| P_GIVEN _ => #put stderr "[given]"
	| P_RESOLVE _ => #put stderr "[by resolution]"
	| P_SPLIT_USE _ => #put stderr "[by splitting]"
	| P_SPLIT_DEF _ =>
	  #put stderr "[defining clause for splitting symbol]"
	| _ => #put stderr "[?]");
	  #put stderr "\n");

fun print_clause (f as |[put, ...]|, xname) =
    let val pq = print_q f
	val cvarnames = clause_var_names xname
    in
	fn (c as CL (h, ql, al, Bs, ...)) =>
	   let val vars = cvarnames c
	       val getvars = ?vars
	       val pt = print_term (f, getvars)
	       val delimr = ref " :- "
	   in
	       print_head (f, xname, getvars) h;
	       iterate
		 (put (!delimr); delimr := ", "; pq q)
	       | q in set ql
	       end;
	       iterate
		 (put (!delimr); delimr := ", ";
		  put P; put " "; pt t)
	       | (P, t) in list al
	       end;
	       iterate
		 iterate
		   (put (!delimr); delimr := ", ";
		    put P; put " ";
		    if i inset vars
			then put (?vars i)
		    else raise PrintVarNotInEnv i)
		 | P in set blk
		 end
	       | i => blk in map Bs
	       end;
	       put "."
	   end
    end;

val perrclause = print_clause (stderr, "X");

fun print_h_al (f as |[put, ...]|, xname) =
    let val pq = print_q f
    in
	fn ((h, al), Bss) =>
	   let val fvars = head_vars h U al_vars al U
		   union {dom Bs | Bs in set Bss}
	       val vars = let val f as |[convert, put, seek, ...]| = outstring xname
			      val n = size xname
			  in
			      {i => (seek n;
				     print f (pack i);
				     convert ())
			      | i in set fvars}
			  end
	       val getvars = ?vars
	       val pt = print_term (f, getvars)
	       val delimr = ref " :- "
	   in
	       print_head (f, xname, getvars) h;
	       iterate
		 (put (!delimr); delimr := ", ";
		  put P; put " "; pt t)
	       | (P, t) in list al
	       end;
	       put (!delimr);
	       delimr := "| ";
	       iterate
		 (put (!delimr);
		  delimr := "";
		  iterate
		    iterate
		      (put (!delimr); delimr := ", ";
		       put P; put " ";
		       if i inset vars
			   then put (?vars i)
		       else raise PrintVarNotInEnv i)
		    | P in set blk
		    end
		  | i => blk in map Bs
		  end;
		  put ".";
		  perr_by pi;
		  delimr := "\t... | ")
	       | Bs => (_, pi) in map Bss
	       end
	   end
    end;

val perr_h_al = print_h_al (stderr, "X");

fun sig_add (f, k, sigmap) =
    if f inset sigmap
	then if ?sigmap f = k
		 then sigmap
	     else raise InconsistentSig f
    else sigmap ++ {f => k};

fun head_sig (HVAR _, acc) = acc
  | head_sig (HFUN (_, f, k, ...), acc) = sig_add (f, k, acc)
  | head_sig (_, acc) = acc;

fun t_sig (V _, acc) = acc
  | t_sig (f $ l, acc) =
    tl_sig (l, sig_add (f, len l, acc))
and tl_sig (nil, acc) = acc
  | tl_sig (t::l, acc) =
    tl_sig (l, t_sig (t, acc));

fun al_sig (nil, acc) = acc
  | al_sig ((_, t)::al, acc) =
    al_sig (al, t_sig (t, acc));

fun clause_sig (CL (h, ql, al, Bs, ...), acc) =
    head_sig (h, al_sig (al, acc));

fun clause_list_sig_1 (nil, acc) = acc
  | clause_list_sig_1 (c :: l, acc) =
    clause_list_sig_1 (l, clause_sig (c, acc));

fun clause_list_sig cl = clause_list_sig_1 (cl, {});

fun head_preds (HVAR P) = {P}
  | head_preds (HFUN (P, ...)) = {P}
  | head_preds _ = {};

fun al_preds nil = {}
  | al_preds ((P, _)::al) =
    {P} U al_preds al;

fun Bs_preds Bs = union {blk
			| _ => blk in map Bs};

fun clause_preds (CL (h, ql, al, Bs, ...)) =
    head_preds h U al_preds al U Bs_preds Bs;

fun clause_list_preds cl = union {clause_preds c
				 | c in list cl};

fun clause_bots (CL (HBOT botname, ...)) = {botname}
  | clause_bots _ = {};

fun clause_list_bots cl = union {clause_bots c
				| c in list cl};

(* The standard ordering on atoms: *)
(* Assume there are nf function symbols.
 Given a random ground term t, the probability P(u) that it is matched by
 some term u, under simplistic probabilistic assumptions, is:
 P(V x) = 1
 P(f(u1, ..., un)) = 1/nf . P(u1) ... P(un).
 So:
 log P (V x) = 0
 log P(f(u1,...,un)) = -log nf + sum_i log P (ui).
 In particular, log P(u) is the size of u, counting variables as 0,
 up to some (negative) multiplicative constant.

 We prefer to select negative literals u that have the least chance of
 being matched, that is, with log P(u) minimal, therefore of maximal size.
 We then organize bodies of clauses (the al field) so that atoms (of depth>=1)
 are listed in reverse order of size.
 For any two atoms with the same size, we then select the one with the
 lexicographically smallest predicate symbol.
*)

memofun t_size (V _) = 0
      | t_size (f $ l) =
	tl_size (l, 1)
with tl_size (t::l, n) = tl_size (l, t_size t+n)
   | tl_size (_, n) = n;

fun atom_less ((P, t), (P', t')) =
    let val n = t_size t
	val n' = t_size t'
    in
	n > n' orelse
	n=n' andalso P strless P'
    end;

fun atom_merge (atl as at::atr, atl' as at' :: atr') =
    if atom_less (at, at')
	then at' :: atom_merge (atl, atr')
    else if at=at'
	then at :: atom_merge (atr, atr')
    else at :: atom_merge (atr, atl')
  | atom_merge (nil, atl') = atl'
  | atom_merge (atl, nil) = atl;

fun atom_sort {} = []
  | atom_sort {at} = [at]
  | atom_sort ats = let val (ats1, ats2) = split ats
		    in
			atom_merge (atom_sort ats1, atom_sort ats2)
		    end;

exception GenResolvent;

fun default_do_bot c = raise BotFoundEvt c;

fun al_less (nil, nil) = false
  | al_less (nil, _) = true
  | al_less ((maxd, atl)::al, (maxd', atl')::al') =
    maxd < maxd' orelse (maxd=maxd' andalso
			 let val l = len atl
			     val l' = len atl'
			 in
			     l < l' orelse
			     (l=l' andalso al_less (al, al'))
			 end)
  | al_less _ = false;

fun al_len ((_, t)::al, acc) =
    al_len (al, t_size t+acc+1)
  | al_len (_, acc) = acc;

(*
memofun Bs_len {} = 0
      | Bs_len {x => B} = card B
      | Bs_len Bs = let val (Bs1, Bs2) = split Bs
		    in
			Bs_len Bs1 + Bs_len Bs2
		    end;
*)

fun Bs_len {} = 0
  | Bs_len {_ => B} U rest = card B + Bs_len rest;

fun clause_category (CL (_, {}, nil, {}, ...)) = 0
  | clause_category (CL (HBOT _, _, ...)) = 3
  | clause_category (CL (_, _, nil, {}, ...)) = 1
  | clause_category (CL (h, ql, al, Bs, ...)) =
    if empty ql
	then if null al
		 then 4 + Bs_len Bs
	     else al_len (al, 10000000 + Bs_len Bs)
    else 2;

fun h_al_category (_, nil) = 0
  | h_al_category (HBOT _, _) = 3
  | h_al_category (_, al) =
    if null al
	then 4
    else al_len (al, 10000000)

(* forward linear subsumption: *)

datatype share_atom = SHARE_PX of string * int
(*
       | SHARE_Q of block
       | SHARE_A of atom
*)
	 ;

datatype body_share = BS_OK
       | BS_NO
       | BS_IF of share_atom * body_share * body_share;
	 (* BS_IF (a, b1, b2) = {a /\ C | C in b1} U b2. *)

val pred_less = op strless;
val pred_sort = sort pred_less;
val xsort = sort (op <);

fun bs_if (_, BS_NO, b2) = b2
  | bs_if arg = BS_IF arg;

fun share_funs () =
    let (*memofun atom_before (a, a') = not (atom_less (a, a'))*)
	(*fun q_before (q, q') = (q = choose {q, q'})*)
	(*memo*)fun share_before (SHARE_PX (P, k), SHARE_PX (P', k')) =
		k<k' orelse
		k=k' andalso pred_less (P, P')
		(*
	      | share_before (SHARE_PX _, _) = false
	      | share_before (SHARE_A a, SHARE_A a') =
		atom_before (a, a')
	      | share_before (SHARE_A _, _) = false
	      | share_before (SHARE_Q q, SHARE_Q q') =
		q_before (q, q')
	      | share_before _ = true
		 *)

	memofun before_k k = 1 to (k-1)
	val body_subsumed =
	    let fun Bs_subsumed Bs =
		    let memofun Bssubsumed BS_OK = true
			      | Bssubsumed BS_NO = false
			      | Bssubsumed (BS_IF (a, b1, b2)) =
				(case a of
				     SHARE_PX (P, k) =>
				     (k inset Bs andalso P inset ?Bs k
				      andalso Bssubsumed b1)
				     orelse Bssubsumed b2
				   | _ => Bssubsumed b2)
		    in
			Bssubsumed
		    end
		(*
		memofun al_Bs_subsumed (b as BS_IF (SHARE_PX _, ...), (_, Bs)) =
			Bs_subsumed Bs b
		      | al_Bs_subsumed (BS_OK, _) = true
		      | al_Bs_subsumed (BS_NO, _) = false
		      | al_Bs_subsumed (BS_IF (_, _, b2), alBs as (nil, _)) =
			al_Bs_subsumed (b2, alBs)
		      | al_Bs_subsumed (BS_IF (SHARE_Q _, _, b2), alBs) =
			al_Bs_subsumed (b2, alBs)
		      | al_Bs_subsumed (b as BS_IF (SHARE_A a, b1, b2),
					alBs as (a'::al, Bs)) =
			if a=a'
			    then let val alBs' = (al, Bs)
				 in
				     al_Bs_subsumed (b1, alBs') orelse
				     al_Bs_subsumed (b2, alBs')
				 end
			else if atom_before (a, a')
			    then al_Bs_subsumed (b2, alBs)
			else al_Bs_subsumed (b, (al, Bs))
		memofun ql_al_Bs_subsumed (b as BS_IF (SHARE_PX _, ...), (_, (_, Bs))) =
			Bs_subsumed Bs b
		      | ql_al_Bs_subsumed (BS_OK, _) = true
		      | ql_al_Bs_subsumed (BS_NO, _) = false
		      | ql_al_Bs_subsumed (b as BS_IF (SHARE_A _, ...), (_, alBs)) =
			al_Bs_subsumed (b, alBs)
		      | ql_al_Bs_subsumed (BS_IF (_, _, b2), body as ({}, _)) =
			ql_al_Bs_subsumed (b2, body)
		      | ql_al_Bs_subsumed (b as BS_IF (SHARE_Q q, b1, b2), body as ({q'} U rest, alBs)) =
			if q=q'
			    then let val body' = (rest, alBs)
				 in
				     ql_al_Bs_subsumed (b1, body') orelse
				     ql_al_Bs_subsumed (b2, body')
				 end
			else if q_before (q, q')
			    then ql_al_Bs_subsumed (b2, body)
			else ql_al_Bs_subsumed (b, (rest, alBs))
		      | ql_al_Bs_subsumed (BS_IF (_, _, b2), (_, alBs)) =
			al_Bs_subsumed (b2, alBs)
		 *)
	    in
		(*ql_al_*)Bs_subsumed
	    end

	fun list_from_body (*(ql, (al,*) Bs (*))*) =
	    (*[SHARE_Q q | q in set ql] @
	      [SHARE_A a | a in list al] @
	     *)
		let val xs = xsort Bs
		in
		    append [[SHARE_PX (P, x)
			    | P in list pred_sort B]
			   | x in list xs
			       val B = ?Bs x]
		end

	val list_add_body =
	    let memofun remove_subsumed (_, nil) = BS_NO
		      (* remove_subsumed (b, l) removes every subsumed by l from b. *)
		      | remove_subsumed (BS_OK, _) = BS_OK
		      | remove_subsumed (BS_NO, _) = BS_NO
		      | remove_subsumed (b as BS_IF (sa, b1, b2), list as (sa' :: rest)) =
			if sa=sa'
			    then bs_if (sa, remove_subsumed (b1, rest), b2)
			else if share_before (sa, sa')
			    then bs_if (sa,
					remove_subsumed (b1, list),
					remove_subsumed (b2, list))
			else b
		fun share_from_list nil = BS_OK
		  | share_from_list (sa::rest) =
		    bs_if (sa, share_from_list rest, BS_NO)
		memofun add_body (_, nil) = BS_OK
			(* add_body (b, l) adds l to b, while removing all branches
			 of b subsumed by l. *)
		      | add_body (BS_OK, _) = BS_OK
		      | add_body (BS_NO, l) = share_from_list l
		      | add_body (b as BS_IF (sa, b1, b2),
				  l as sa' :: rest) =
			if sa=sa'
			    then bs_if (sa, add_body (b1, rest), b2)
			else if share_before (sa, sa')
			    then bs_if (sa,
					remove_subsumed (b1, l),
					add_body (b2, l))
			else bs_if (sa', share_from_list rest, b)
	    in
		add_body
	    end
    in
	|[ body_subsumed = body_subsumed,
	   body_add = (fn (b, body) => list_add_body (b, list_from_body body))
	   ]|
    end

(* The prover: *)

memofun match_k 0 = {}
      | match_k 1 = {~1 => V 1}
      | match_k n = {~n => V n} ++ match_k (n-1);

exception ResolvePF_Depth0;
exception ResolvePF_BadSelF;
exception ResolvePF_BadSelX;
exception ResolvePF_BadSelQ;
exception ResolvePF_BlackHole;
exception ResolvePFs_BlackHole;

fun is_tautology (CL (HVAR P, _, _, Bs, ...)) =
    1 inset Bs andalso P inset ?Bs 1
  | is_tautology (CL (HFUN _, _, nil, ...)) = false
  | is_tautology (CL (HFUN (P, _, _, _, t), _, al, ...)) =
    let val a = (P, t)
    in
	exists a=a' | a' in list al end
    end
  | is_tautology (CL (HQ q, ql, ...)) = q inset ql
  | is_tautology _ = false;

fun is_h_al_tauto (HFUN (P, _, _, _, t), al) =
    let val a = (P, t)
    in
	exists a=a' | a' in list al end
    end
  | is_h_al_tauto _ = false;

datatype predicate = P_BOT of string
       | P_PRED of string
       | P_ROOT;

exception ResolveUseful;
exception InfosMax;

fun opt_inter (NONE, fso) = fso
  | opt_inter (fso, NONE) = fso
  | opt_inter (SOME fs, SOME fs') = SOME (fs & fs');


(*
    (* funtrees represent sets of lists of strings.
     FT_OF (ft, ftmap) is the list of:
     - all lists s::l, for any s, and for l in ft (if ft is present;
     and then ft should be non-empty);
     - all lists s::l, with s in ftmap and l in ?ftmap s;
     the int
     *)
datatype funtree = FT_NIL
       | FT_OF of funtree option * (string -m> funtree);

val ft_empty = FT_OF (NONE, {});

fun ft_trivial FT_NIL = true
  | ft_trivial (FT_OF (SOME ft, _)) = ft_trivial ft
  | ft_trivial _ = false;

exception FtInter;

fun ft_inter (FT_OF (ftopt, ftmap), FT_OF (ftopt', ftmap')) =
    FT_OF ((case ftopt of
		SOME ft =>
		(case ftopt' of
		     SOME ft' => SOME (ft_inter (ft, ft'))
		   | _ => NONE)
	      | _ => NONE),
		{f => funt''
		| f => funt in map (ftmap' <| ftmap)
		    val funt' = ?ftmap' f
		    val funt'' = ft_inter (funt, funt')
		    such that funt''<>ft_empty})
  | ft_inter (FT_NIL, FT_NIL) = FT_NIL
  | ft_inter _ = raise FtInter;

fun ft_all 0 = FT_NIL
  | ft_all k = FT_OF (SOME (ft_all (k-1)), {});

datatype toprel = TR_ALL (* set of all terms *)
       | TR_ENUM of string -m> funtree option; (* TR_ENUM ftmap denotes the set of all terms f(l)
						where f in ftmap and either
						?ftmap l=NONE, or
						?ftmap l=SOME s where s contains l. *)

val tr_empty = TR_ENUM {};

fun tr_inter (TR_ALL, tr) = tr
  | tr_inter (tr, TR_ALL) = tr
  | tr_inter (TR_ENUM ftmap, TR_ENUM ftmap') =
    TR_ENUM {f => ftopt''
	    | f => ftopt in map ftmap' <| ftmap
		val ftopt' = ?ftmap' f
		val ftopt'' = (case ftopt of
				   SOME ft => (case ftopt' of
						   SOME ft' => SOME (ft_inter (ft, ft'))
						 | _ => ftopt)
				 | _ => ftopt')
		    such that ftopt''<>SOME ft_empty};
*)

datatype pathset = PS_ALL
       | PS_ENUM of string * int -m> pathset; (* maps (f, i) to non-empty pathset;
					       maps (f, 0) to PS_ALL in case f is a constant. *)

fun print_pathset (|[put, ...]|) =
    let val delimr = ref ""
	val buf as |[put=puts, convert, tell, seek, truncate, ...]| = outstring ""
	fun printps PS_ALL = (put (!delimr); delimr := ", ";
			      truncate (); put (convert ()); put "*")
	  | printps (PS_ENUM fimap) =
	    let val pos = tell ()
	    in
		iterate
		  (seek pos;
		   if i=0
		       then (put (!delimr); delimr := ", ";
			     truncate (); put (convert ()); put f)
		   else (puts f; puts "[";
			 print buf (pack i);
			 puts "]";
			 printps ps)
		       )
		| (f, i) => ps in map fimap
		end
	    end
    in
	fn ps => (delimr := ""; seek 0; printps ps)
    end;

val perr_pathset = print_pathset stderr;

val ps_empty = PS_ENUM {};

fun ps_inter (PS_ALL, ps) = ps
  | ps_inter (ps, PS_ALL) = ps
  | ps_inter (PS_ENUM fimap, PS_ENUM fimap') =
    PS_ENUM {fi => ps''
	    | fi => ps in map (fimap' <| fimap)
		val ps' = ?fimap' fi
		val ps'' = ps_inter (ps, ps')
		such that ps''<>ps_empty};

fun ps_funs PS_ALL = NONE
  | ps_funs (PS_ENUM fimap) = SOME {f | (f, _) in set fimap}

exception NoPathSetEvt;
(*
exception TrMatchTermList;
exception FtUnion;
*)

(*
fun print_tr (f as |[put, ...]|) =
    let val pq = print_q f
    in
	fn (P, TR_ALL) => (put P; put "(*)")
	 | (P, TR_ENUM ftmap) =>
	   let val delimr = ref ""
	   in
	       iterate
		 (case ftopt of
		      SOME funt =>
		      let fun iter (FT_NIL, acc) =
			      let val dr = ref ""
			      in
				  put (!delimr); delimr := ", ";
				  put P; put " "; put f; put "(";
				  iterate
				    (put (!dr); dr := ",";
				     case sopt of
					 SOME s => put s
				       | _ => put "*")
				  | sopt in list rev acc
				  end;
				  put ")"
			      end
			    | iter (FT_OF (NONE, ftmap), acc) =
			      iterate
				iter (funt, SOME s::acc)
			      | s => funt in map ftmap
			      end
			    | iter (FT_OF (SOME ft, ftmap), acc) =
			      (iter (ft, NONE::acc);
			       iter (FT_OF (NONE, ftmap), acc))
		      in
			  iter (funt, nil)
		      end
		    | _ => (put (!delimr); delimr := ", ";
			    put P; put "("; put f; put "(...))"))
	       | f => ftopt in map ftmap
	       end
	   end
    end;
*)

fun compute_skeleta (cl, maxpathlen) =
    let val pathsets = ref ({} : string -m> pathset)
			 (*
	val toprels = ref ({} : string -m> toprel)
			  *)
	val qs = ref ({} : block set)
	val bots = ref ({} : string set)

	val clause_index = inv_rel {c => {P
					 | (P, _) in list al}
				     U union (rng Bs)
				   | c as CL (_, _, al, Bs, ...) in list cl}

	val changed_P = ref ({} : string set)

			 (*
	memofun ft_union (FT_OF (ftopt, ftmap), FT_OF (ftopt', ftmap')) =
		let val ftopt'' = case ftopt of
				      SOME ft =>
				      (case ftopt' of
					   SOME ft' => SOME (ft_union (ft, ft'))
					 | _ => ftopt)
				    | _ => ftopt'
		in
		    if case ftopt'' of
			   SOME ft => ft_trivial ft
			 | _ => false
			then FT_OF (ftopt'', {})
		    else FT_OF (ftopt'',
				(ftmap delta ftmap') ++ {f => ft_union (funt, funt')
							| f => funt in map ftmap' <| ftmap
							    val funt' = ?ftmap' f})
		end
	      | ft_union (FT_NIL, FT_NIL) = FT_NIL
	      | ft_union _ = raise FtUnion

	fun tr_union (TR_ALL, _) = TR_ALL
	  | tr_union (_, TR_ALL) = TR_ALL
	  | tr_union (TR_ENUM ftmap, TR_ENUM ftmap') =
	    TR_ENUM ((ftmap delta ftmap') ++
			 {f => (case ftopt of
				    SOME ft => (case ftopt' of
						    SOME ft' => SOME (ft_union (ft, ft'))
						  | _ => NONE)
				  | _ => NONE)
			 | f => ftopt in map ftmap' <| ftmap
			     val ftopt' = ?ftmap' f})

	fun tr_dunion {} = tr_empty
	  | tr_dunion {tr} = tr
	  | tr_dunion trs = let val (trs1, trs2) = split trs
			    in
				tr_union (tr_dunion trs1, tr_dunion trs2)
			    end
			  *)

	fun ps_union (PS_ALL, _) = PS_ALL
	  | ps_union (_, PS_ALL) = PS_ALL
	  | ps_union (PS_ENUM fimap, PS_ENUM fimap') =
	    PS_ENUM ((fimap delta fimap') ++ {fi => ps_union (ps, ps')
					     | fi => ps in map fimap' <| fimap
						 val ps' = ?fimap' fi})

	fun ps_add (P, ps) =
	    (do_verbose (3, fn () =>
			 (#put stderr "  ==> ";
			  #put stderr P;
			  #put stderr "(";
			  perr_pathset ps;
			  #put stderr ")\n"));
	     if P inset !pathsets
		 then let val old = ?(!pathsets) P
			  val new = ps_union (ps, old)
		      in
			  if old=new
			      then ()
			  else (pathsets := !pathsets ++ {P => new};
				changed_P := !changed_P ++ {P})
		      end
	     else (pathsets := !pathsets ++ {P => ps};
		   changed_P := !changed_P ++ {P}))

		(*
	fun tr_add (P, tr) =
	    let val old = if P inset !toprels
			      then ?(!toprels) P
			  else tr_empty
		val new = tr_union (tr, old)
	    in
		if old=new
		    then ()
		else (do_verbose (2, fn () =>
				  (#put stderr "=> ";
				   print_tr stderr (P, new);
				   #put stderr "\n";
				   #flush stderr ()));
		      toprels := !toprels ++ {P => new};
		      changed_P := !changed_P U {P})
	    end
		 *)

	fun ps_chop (PS_ALL, _) = PS_ALL
	  | ps_chop (_, 0) = PS_ALL
	  | ps_chop (PS_ENUM fimap, n) =
	    let val n' = n-1
	    in
		PS_ENUM {fi => ps_chop (ps, n')
			| fi => ps in map fimap}
	    end

	fun ps_match_term (V x, ps, env) =
	    if x inset env
		then let val ps' = ps_inter (ps, ?env x)
		     in
			 if ps' = ps_empty
			     then raise NoPathSetEvt
			 else env ++ {x => ps'}
		     end
	    else env ++ {x => ps}
	  | ps_match_term (_, PS_ALL, env) = env
	  | ps_match_term (f $ nil, PS_ENUM fimap, env) =
	    if (f, 0) inset fimap
		then env
	    else raise NoPathSetEvt
	  | ps_match_term (f $ l, PS_ENUM fimap, env) =
	    ps_match_term_list (f, l, 1, fimap, env)
	and ps_match_term_list (_, nil, _, _, env) = env
	  | ps_match_term_list (f, ti::l, i, fimap, env) =
	    let val fi = (f, i)
	    in
		if fi inset fimap
		    then let val env' = ps_match_term (ti, ?fimap fi, env)
			 in
			     ps_match_term_list (f, l, i+1, fimap, env')
			 end
		else raise NoPathSetEvt
	    end

			 (*
	memofun tr_match_term_list (nil, FT_NIL, env) = {env}
	      | tr_match_term_list ((_, t)::l, FT_OF (ftopt, ftmap), env) =
		(case ftopt of
		     SOME ft => tr_match_term_list (l, ft, env)
		   | _ => {}) U
		     (case t of
			  f $ _ => if f inset ftmap
					     then tr_match_term_list (l, ?ftmap f, env)
					 else {}
			| V x => let val vx = tr_inter (if x inset env
							     then ?env x
							 else TR_ALL,
							     TR_ENUM {f => NONE
								     | f in set ftmap})
				  in
				      if vx = tr_empty
					  then {}
				      else case vx of
					       TR_ALL => union {tr_match_term_list (l, ft, env)
							       | f => ft in map ftmap}
					     | TR_ENUM ftmap' =>
					       union {tr_match_term_list (l, ?ftmap f,
									  env ++ {x => TR_ENUM {f => fopt}})
						     | f => fopt in map ftmap'}
				  end)
	      | tr_match_term_list _ = raise TrMatchTermList

	fun tr_match_term (V x, tr, env) =
	    if x inset env
		then let val tr' = tr_inter (tr, ?env x)
		     in
			 if tr' = tr_empty
			     then {}
			 else {env ++ {x => tr'}}
		     end
	    else {env ++ {x => tr}}
	  | tr_match_term (_, TR_ALL, env) = {env}
	  | tr_match_term (f $ l, TR_ENUM ftmap, env) =
	    if f inset ftmap
		then case ?ftmap f of
			 SOME funt => tr_match_term_list (l, funt, env)
		       | _ => {env}
	    else {}
			  *)

	fun ps_match_atom ((P, t), env) =
	    if P inset !pathsets
		then ps_match_term (t, ?(!pathsets) P, env)
	    else raise NoPathSetEvt

			 (*
	fun tr_match_atom ((P, t), env) =
	    if P inset !toprels
		then tr_match_term (t, ?(!toprels) P, env)
	    else {}
			  *)

	fun ps_match_al (nil, env) = env
	  | ps_match_al (a::al, env) =
	    ps_match_al (al, ps_match_atom (a, env))

			 (*
	fun tr_match_al (nil, env) = {env}
	  | tr_match_al (a::al, env) =
	    union {tr_match_al (al, env')
			 | env' in set tr_match_atom (a, env)}
	    *)

	fun blk_pathsets {} = PS_ALL
	  | blk_pathsets {P} = if P inset !pathsets
				   then ?(!pathsets) P
			       else raise NoPathSetEvt
	  | blk_pathsets blk = let val (blk1, blk2) = split blk
				   val ps = ps_inter (blk_pathsets blk1,
						      blk_pathsets blk2)
			       in
				   if ps=ps_empty
				       then raise NoPathSetEvt
				   else ps
			       end

	  (*
	fun blk_toprels {} = TR_ALL
	  | blk_toprels {P} = if P inset !toprels
				  then ?(!toprels) P
			      else raise NoPathSetEvt
	  | blk_toprels blk = let val (blk1, blk2) = split blk
				  val tr = tr_inter (blk_toprels blk1,
						     blk_toprels blk2)
			      in
				  if tr = tr_empty
				      then raise NoPathSetEvt
				  else tr
			      end
	   *)

	fun ps_match_blk (x, blk, env) =
	    let val ps = blk_pathsets blk
	    in
		if x inset env
		    then let val ps' = ps_inter (ps, ?env x)
			 in
			     if ps' = ps_empty
				 then raise NoPathSetEvt
			     else env ++ {x => ps'}
			 end
		else env ++ {x => ps}
	    end

	  (*
	fun tr_match_blk (x, blk, env) =
	    let val tr = blk_toprels blk
	    in
		if x inset env
		    then let val tr' = tr_inter (tr, ?env x)
			 in
			     if tr' = tr_empty
				 then raise NoPathSetEvt
			     else env ++ {x => tr'}
			 end
		else env ++ {x => tr}
	    end
	   *)

	fun ps_match_blks ({}, env) = env
	  | ps_match_blks ({x => blk} U rest, env) =
	    ps_match_blks (rest, ps_match_blk (x, blk, env))

	  (*
	fun tr_match_blks ({}, env) = env
	  | tr_match_blks ({x => blk} U rest, env) =
	    tr_match_blks (rest, tr_match_blk (x, blk, env))
	   *)

	fun ps_eval_clause (c as CL (h, ql, al, Bs, ...)) =
	    if ql subset !qs
		then (do_verbose (3, fn () =>
				  (#put stderr "Triggering clause: ";
				   perrclause c;
				   #put stderr "\n")
				  );
		      let val env = ps_match_blks (Bs, ps_match_al (al, {}))
		      in
			  case h of
			      HQ q => qs := !qs U {q}
			    | HBOT botname => bots := !bots U {botname}
			    | HVAR P => if 1 inset env
					    then ps_add (P, ?env 1)
					else ps_add (P, PS_ALL)
			    | HFUN (P, f, k, vars, ...) =>
			      let val ps = if k=0
					       then PS_ENUM {(f, 0) => PS_ALL}
					  else PS_ENUM {(f, i) => ps_chop (psi, maxpathlen)
						       | i in set vars
							   val psi = if i inset env
									 then ?env i
								     else PS_ALL}
			      in
				  ps_add (P, ps)
			      end
		      end handle NoPathSetEvt => ())
	    else ()

	  (*
	fun tr_refine (tr, PS_ALL) = TR_ALL (* should be tr, but in most cases,
					     when ps=PS_ALL, tr_saturate will eventually
					     set tr to TR_ALL, so do this faster. *)
	  | tr_refine (TR_ALL, ps) =
	    (case ps_funs ps of
		 SOME {} => raise NoPathSetEvt
	       | SOME fs => TR_ENUM {f => NONE
				    | f in set fs})
	  | tr_refine (tr as TR_ENUM ftmap, ps) =
	    (case ps_funs ps of
		 SOME fs => (case fs <| ftmap of
				 {} => raise NoPathSetEvt
			       | ftmap' => TR_ENUM ftmap')
	       | _ => tr)

	fun tr_eval_clause (CL (HVAR P, ql, al, Bs, ...)) =
	    if ql subset !qs
		then (let val env' = tr_match_blks (Bs, {})
			  val vx = tr_dunion {if 1 inset env
						  then ?env 1
					      else TR_ALL
					     | env in set tr_match_al (al, env')}
			  val vx' = if P inset !pathsets
					then tr_refine (vx, ?(!pathsets) P)
				    else vx
		      in
			  tr_add (P, vx)
		      end handle NoPathSetEvt => ())
	    else ()
	  | tr_eval_clause (CL (HFUN (P, f, k, ...), ql, al, Bs, ...)) =
	    if ql subset !qs
		then (let val env' = tr_match_blks (Bs, {})
			  val psenv = ps_match_blks (Bs, ps_match_al (al, {}))
			  memofun tv_l (n, env) =
				  if n<k
				      then let val n'=n+1
					       val vx = if n' inset env
							    then ?env n'
							else TR_ALL
					       val vx' = if n' inset psenv
							     then tr_refine (vx, ?psenv n')
							 else vx
					   in
					       case vx' of
						   TR_ALL => FT_OF (SOME (tv_l (n', env)), {})
						 | TR_ENUM ftmap =>
						   FT_OF (NONE, {f => tv_l (n', env)
								| f in set ftmap})
					   end
				  else FT_NIL
			  val vt = tr_dunion {TR_ENUM {f => SOME (tv_l (0, env))}
					     | env in set tr_match_al (al, env')}
		      in
			  tr_add (P, vt)
		      end handle NoPathSetEvt => ())
	    else ()
	  | tr_eval_clause _ = ()

	fun tr_eval_clause_v c =
	    (do_verbose (2, fn () =>
			 (#put stderr "(TR) eval clause ";
			  perrclause c;
			  #put stderr "\n"));
	     tr_eval_clause c)
	    *)

	fun ps_saturate clauses =
	    (changed_P := {};
	     iterate
	       ps_eval_clause c
	     | c in list cl
	     end;
	     while not (empty (!changed_P)) do
		 let val Ps = !changed_P
		 in
		     changed_P := {};
		     iterate
		       ps_eval_clause c
		     | c in set union {cs
				      | _ => cs in map Ps <| clause_index}
		     end
		 end)

	(*
	fun tr_saturate clauses =
	    (changed_P := {};
	     iterate
	       tr_eval_clause_v c
	     | c in list cl
	     end;
	     while not (empty (!changed_P)) do
		 let val Ps = !changed_P
		 in
		     changed_P := {};
		     iterate
		       tr_eval_clause_v c
		     | c in set union {cs
				      | _ => cs in map Ps <| clause_index}
		     end
		 end)
	 *)
    in
	ps_saturate cl;
	(*
	tr_saturate cl;
	 *)
	(!pathsets, (* !toprels, *) !bots)
    end;

(*
fun opt_dinter {} = NONE
  | opt_dinter {fso} = fso
  | opt_dinter fsos = let val (fsos1, fsos2) = split fsos
		      in
			  opt_inter (opt_dinter fsos1, opt_dinter fsos2)
		      end;
*)

fun iter_sub_Bs f =
    let fun iter ({i => B} U rest) =
	    let val iter' = iter rest
	    in
		fn Bs_acc =>
		   iterate
		     if empty B'
			 then iter' Bs_acc
		     else iter' (Bs_acc ++ {i => B'})
		   | B' sub map B
		   end
	    end
	  | iter _ = f
    in
	fn Bs => iter Bs {}
    end;

fun t_get_table t x =
    (case t_get t x of
	 SOME t' => t'
       | _ => let val t' = table ()
	      in
		  t_put t (x, t');
		  t'
	      end);

fun t_get_mapr t x =
    (case t_get t x of
	 SOME t' => t'
       | _ => let val t' = ref {}
	      in
		  t_put t (x, t');
		  t'
	      end);

fun resolver (do_bot : clause -> unit, maxpathlen, wantproof) =
    let val (p_resolve, p_split_def, p_split_use) =
	    if wantproof
		then (P_RESOLVE, P_SPLIT_DEF, P_SPLIT_USE)
	    else let val dummy_pi = P_GIVEN "<recipe>"
		 in
		     (fn _ => dummy_pi, fn _ => dummy_pi, fn _ => dummy_pi)
		 end

	val predicate_graph = ref ({} : predicate digraph)
	val clause_list = ref (nil : clause list)
	val skeleta = ref ({} : string -m> pathset)
	val skel_bots = ref ({} : string set)
	val tr_bots = ref ({} : string set)

	fun add_graph (pred, CL (_, ql, al, Bs, ...)) =
	    predicate_graph := !predicate_graph Urel {pred => union {{P_PRED P
								     | P in set blk}
								    | blk in set ql}
						       U {P_PRED P
							 | (P, _) in list al}
						       U union {{P_PRED P
								| P in set blk}
							       | _ => blk in map Bs}}
	fun new_clause (c as CL (HBOT botname, ...)) =
	    (predicate_graph := !predicate_graph Urel {P_ROOT => {P_BOT botname}};
	     add_graph (P_BOT botname, c);
	     clause_list := c :: !clause_list)
	  | new_clause (c as CL (HVAR P, ...)) =
	    (add_graph (P_PRED P, c);
	     clause_list := c :: !clause_list)
	  | new_clause (c as CL (HFUN (P, f, ...), ...)) =
	    (add_graph (P_PRED P, c);
	     clause_list := c :: !clause_list)
	  | new_clause (c as CL (HQ blk, ...)) =
	    (iterate
	       add_graph (P_PRED P, c)
	     | P in set blk
	     end;
	       clause_list := c :: !clause_list)

	val dfs_info = ref ({} : predicate -m> int * int) (* dfsnum, revtopsort number of low *)
	val scc_info = ref ({} : int -m> predicate set) (* map (revtopsort of) low to corresponding scc *)
	val dfs_q_info = ref ({} : block -m> int * int) (* max {(revnum P, low P) | P in blk},
							 where the max is taken in the right-to-left
							 lexicographic ordering. *)
	fun useful (CL (HBOT botname, ...)) = P_BOT botname inset !dfs_info
	  | useful (CL (HVAR P, ...)) = P_PRED P inset !dfs_info
	  | useful (CL (HFUN (P, ...), ...)) = P_PRED P inset !dfs_info
	  | useful (CL (HQ blk, ...)) =
	    all
	      P_PRED P inset !dfs_info
	    | P in set blk
	    end

	fun info_less ((revnum, low), (revnum', low')) =
	    low<low' orelse low=low' andalso revnum<revnum'
	fun info_max (dlow, dlow') =
	    if info_less (dlow, dlow')
		then dlow'
	    else dlow
	fun infos_max {} = raise InfosMax
	  | infos_max {dlow} = dlow
	  | infos_max dlows = let val (dlows1, dlows2) = split dlows
			      in
				  info_max (infos_max dlows1, infos_max dlows2)
			      end
	fun p_info P = ?(!dfs_info) P
	fun h_info (HBOT botname) = p_info (P_BOT botname)
	  | h_info (HVAR P) = p_info (P_PRED P)
	  | h_info (HFUN (P, ...)) = p_info (P_PRED P)
	  | h_info (HQ blk) =
	    let val dfs_q = !dfs_q_info
	    in
		if blk inset dfs_q
		    then ?dfs_q blk
		else let val info = !dfs_info
			 val m = infos_max {p_info (P_PRED P)
					   | P in set blk}
		     in
			 dfs_q_info := dfs_q ++ {blk => m};
			 m
		     end
	    end
	fun head_info (CL (h, ...)) = h_info h

	val back_subs : (clause, unit) table
	    (* set of backward subsumed clauses. *)
	    = table ()
	val bs_get = t_get back_subs
	val bs_put1 = t_put_behind back_subs
	fun bs_put c = bs_put1 (c, ())

	fun b_set c =
	    do_verbose_else (2,
			     fn () =>
				(case bs_get c of
				     SOME _ => ()
				   | _ =>
				     (#put stderr "  Removing backward subsumed clause: ";
				      perrclause c;
				      #put stderr "\n";
				      #flush stderr ();
				      bs_put c)),
				     fn () => bs_put c)

	val eps_back : (head, (int -m> block) ref
			* (int -m> block, clause list ref) table) table
	    = table ()
	val eps_back_get = t_get eps_back
	val eps_back_put = t_put eps_back

	fun eps_back_head (HFUN _) = true
	  | eps_back_head (HVAR _) = true
	  | eps_back_head _ = false
	    (* used to backward subsume clauses. *)
	fun eps_back_subsume (CL (h, {}, nil, Bs, ...)) =
	    if eps_back_head h
		then case eps_back_get h of
			 SOME (ref dBs, bbr) =>
			 let val bbget = t_get bbr
			     val bbrem = t_remove bbr
			     fun bb_set Bs' =
				 (case bbget Bs' of
				      SOME (ref cl) =>
				      (iterate
					 b_set c
				       | c in list cl
				       end;
					 bbrem Bs';
					 iterate
					   iterate
					     bb_set (if i inset Bs'
							 then Bs' ++ {i => ?Bs' i U {P}}
						     else Bs' ++ {i => {P}})
					   | P in set B
					   end
					 | i => B in map diff_rel (dBs, Bs')
					 end)
				    | _ => ())
			 in
			     bb_set Bs
			 end
		       | _ => ()
	    else ()
	  | eps_back_subsume _ = ()
	fun compile_eps_back (c as CL (h, ql, al, Bs, ...)) =
	    if eps_back_head h (*andalso empty ql*)
		then let val (dBsr, bbr) =
			     case eps_back_get h of
				 SOME x => x
			       | _ => let val newr = (ref {}, table ())
				      in
					  eps_back_put (h, newr);
					  newr
				      end
			 val cl = [c]
			 val bbget = t_get bbr
			 val bbput = t_put bbr
		     in
			 if empty ql andalso null al
			     then
				 iterate
				   iterate
				     (case bbget Bs' of
					  SOME clr => clr := c :: !clr
					| _ => bbput (Bs', ref cl))
				   | P in set B
				   val B' = B \ {P}
				   val Bs' = if empty B'
						 then {i} <-| Bs
					     else Bs ++ {i => B'}
				   end
				 | i => B in map Bs
				 end
			 else (case bbget Bs of
				   SOME clr => clr := c :: !clr
				 | _ => bbput (Bs, ref cl));
			     dBsr := !dBsr Urel Bs;
			     iter_sub_Bs (fn Bs' =>
					     (case bbget Bs' of
						  SOME _ => ()
						| _ => bbput (Bs', ref nil))
						  ) Bs
		     end
	    else ()
	(*
	    if empty ql andalso null al
		then ()
	    else if h inset !eps_back
		then let val bbr = ?(!eps_back) h
		     in
			 if Bs inset !bbr
			     then let val clr = ?(!bbr) Bs
				  in
				      clr := c :: !clr
				  end
			 else bbr := !bbr ++ {Bs => ref [c]}
		     end
	    else let val cl = [c]
		 in
		     eps_back := !eps_back ++ {h => ref {Bs => ref cl}}
		 end
	 *)
	  | compile_eps_back _ = ()

	val waitq as |[ insert = wait_insert_basic,
			popmin = wait_pop,
			empty = wait_empty,
			dump_list = get_clauses,
			... ]|
	    = mheap (fn (n, n') => n<n')
	    (*= mheap (fn (((revnum, low), n), ((revnum', low'), n')) =>
			n<n' orelse
			(n=n' andalso (low<low' orelse
				       (low=low' andalso revnum<revnum'))))
	     *)

	(* list of unprocessed clauses; may even be automaton clauses,
	 we do not know yet. *)

	fun wait_insert_1 (c_env as (c, psenv)) =
	    (*
	    if c inset !dealtwith
		then do_verbose (2, fn () =>
				 (#put stderr "Removed clause early: ";
				  perrclause c;
				  #put stderr "\n";
				  #flush stderr ()))
	    else
	     *)
	    (do_verbose (1, fn () => (#put stderr "|- ";
				      perrclause c;
				      let val CL (_, _, _, _, pi, ...) = c
				      in
					  perr_by pi
				      end;
				      #flush stderr ()));
	     compile_eps_back c;
	     wait_insert_basic ((*(head_info c,*) clause_category c (*)*), c_env))

	memofun q_skeleta {} = PS_ALL
	      | q_skeleta {P} = if P inset !skeleta then ?(!skeleta) P else ps_empty
	      | q_skeleta blk = let val (blk1, blk2) = split blk
				in
				    ps_inter (q_skeleta blk1, q_skeleta blk2)
				end

	fun ps_check_empty (PS_ENUM {}) = raise NoPathSetEvt
	  | ps_check_empty env = env

	fun ps_env_inter (psenv, psenv') =
	    (psenv delta psenv') ++ {i => ps_check_empty (ps_inter (ps, ps'))
				    | i => ps in map psenv' <| psenv
					val ps' = ?psenv' i}

	fun ps_match_term (V x, ps, env) =
	    if x inset env
		then let val ps' = ps_inter (ps, ?env x)
		     in
			 env ++ {x => ps_check_empty ps'}
		     end
	    else env ++ {x => ps}
	  | ps_match_term (_, PS_ALL, env) = env
	  | ps_match_term (f $ nil, PS_ENUM fimap, env) =
	    if (f, 0) inset fimap
		then env
	    else raise NoPathSetEvt
	  | ps_match_term (f $ l, PS_ENUM fimap, env) =
	    ps_match_term_list (f, l, 1, fimap, env)
	and ps_match_term_list (_, nil, _, _, env) = env
	  | ps_match_term_list (f, ti::l, i, fimap, env) =
	    let val fi = (f, i)
	    in
		if fi inset fimap
		    then let val env' = ps_match_term (ti, ?fimap fi, env)
			 in
			     ps_match_term_list (f, l, i+1, fimap, env')
			 end
		else raise NoPathSetEvt
	    end

	fun ps_match_al ((P, t)::al, env) =
	    if P inset !skeleta
		then ps_match_al (al,
				  ps_match_term (t,
						 ps_check_empty (?(!skeleta) P),
						 env))
	    else raise NoPathSetEvt
	  | ps_match_al (_, env) = env;

	fun ps_match_Bs ({i => B} U rest, env) =
	    ps_match_Bs (rest,
			 if i inset env
			     then env ++ {i => ps_check_empty (ps_inter (?env i, q_skeleta B))}
			 else env ++ {i => ps_check_empty (q_skeleta B)})
	  | ps_match_Bs (_, env) = env

	(* gen_resolvent ([t1, ..., tn], [B1, ..., Bn], al, Bs, psenv)
	 adds B1(t1), ..., Bn(tn) to part of clause referenced as al, Bs.
	 This is only done provided pathsets are compatible with those
	 given in environment psenv. *)

	fun gen_resolvent (t1n, B1n, al, Bs, psenv) =
	    let val Bsr = ref Bs
		val atomsr = ref ({} : atom set)
		val psenvr = ref psenv
	    in
		iterate
		  (case t of
		       V x => let val curBs = !Bsr
				  val B1ps = ps_check_empty (q_skeleta B1)
			      in
				  if x inset !psenvr
				      then psenvr := !psenvr ++
					  {x =>
					    ps_check_empty (ps_inter (?(!psenvr) x,
								      B1ps))}
				  else psenvr := !psenvr ++ {x => B1ps};
				  if x inset curBs
				      then Bsr := curBs ++ {x => ?curBs x U B1}
				  else if empty B1
				      then ()
				  else Bsr := curBs ++ {x => B1}
			      end
		     | _ => atomsr := !atomsr ++ {(P, t) | P in set B1})
		|| t in list t1n
		and B1 in list B1n
		end;
		let val al' = atom_sort (!atomsr)
		in
		    psenvr := ps_match_al (al', !psenvr);
		    (atom_merge (al', al), !Bsr, !psenvr)
		end
	    end

	fun wait_insert (c_env as (c, psenv)) =
	    if is_tautology c
		then ()
	    else let val CL (h, ql, al, Bs, _) = c
		     val splitBs1 = head_vars h <-| Bs
		     val splitBs = if empty splitBs1
				       then {}
				   else al_vars al <-| splitBs1
		 in
		     if empty splitBs
			 then wait_insert_1 c_env
		     else
			 (* split: first generate splitting clauses *)
			 (iterate
			    wait_insert_1 (CL (HQ blk, {}, nil, {1 => blk},
					       p_split_def (c, splitBs, x)),
					   if x inset psenv
					       then {1 => ?psenv x}
					   else {})
			  | x => blk in map splitBs
			  end; (* then process split clause *)
			    wait_insert_1 (CL (h, rng splitBs, al, splitBs <-| Bs,
					       p_split_use (c, splitBs)),
					   splitBs <-| psenv))
		 end

	val fargsq = ref ({} : string -m> int * int set * int term);
	(* map f to (k, {1, ..., k}, f(x1,...,xk)),
	 where k is the arity of f.*)

	val univq = ref ({} : automaton_univ_trans)
	(* set of predicates P for which we have a clause +P(x). *)
	val qq = ref ({} : block -m> proof);
	(* current set of unit clauses +q. *)

	val selfq : (string,
		     (string,
		      (head * atom list,
		       ((int -m> block) -m> (int -m> pathset) * proof) ref)
		      table)
		     table) table
	    = table ()
	val selfq_get = t_get selfq
	val selfq_get_table = t_get_table selfq
	val selfq_put = t_put selfq
	val selfq_rem = t_remove selfq
	(* maps P, f to clauses C \/ -P(f(...))
	 where -P(f(...)) is selected. *)

	val selxq : (string, (clause, int -m> pathset) table) table
	    = table ()
	val selxq_get = t_get selxq
	val selxq_put = t_put selxq
	val selxq_rem = t_remove selxq
	(* maps P to clauses C \/ -P(x), with -P(x) selected. *)

	val selqq : (block, (clause, int -m> pathset) table) table
	    =  table ()
	val selqq_get = t_get selqq
	val selqq_put = t_put selqq
	val selqq_rem = t_remove selqq
	(* maps q to clauses C \/ -q, with -q selected. *)

	val botq = ref ({} : string set);
	(* current set of bot names that have been derived. *)

	val autoinfoq : (string, (string, (block list, proof) table) table) table
	    = table ()
	(* current set of automata clauses, maps P, f, to blocks
	 where blkls is the set of possible bodies, each mapped to a proof of the
	 corresponding pop clause;
	 each body is a list of blocks, one for each variable argument (1, ..., k) to f.
	 *)
	val a_get = t_get autoinfoq
	val a_rem = t_remove autoinfoq

	val subsumers : (head, body_share ref) table
	    = table ()
	val s_get = t_get subsumers
	val s_put = t_put subsumers
	val s_rem = t_remove subsumers
	val |[ body_subsumed, body_add, ...]| = share_funs ()

	fun insert_selfq (_, {}, ...) = ()
	  | insert_selfq (h_al, Bss, P, f) =
	    (do_verbose (1, fn () =>
			 (let val (h, al) = h_al
			  in
			      case Bss of
				  {Bs => (_, pi)} =>
				    (#put stderr "Insert clause into selfq: ";
				     perrclause (CL (h, {}, al, Bs, pi));
				     perr_by pi)
				| _ =>
				  (#put stderr "Insert clauses into selfq:\n";
				   iterate
				     (#put stderr "- ";
				      perrclause (CL (h, {}, al, Bs, pi));
				      perr_by pi)
				   | Bs => (_, pi) in map Bss
				  end)
			  end;
			      #flush stderr ()));
	     let val fmapr = selfq_get_table P
		 val clsr = t_get_table fmapr f
		 val bssr = t_get_mapr clsr h_al
	     in
		 bssr := Bss ++ !bssr
	     end)

	fun clause_compile_subsumed (h, body) =
	    let val shr = case s_get h of
			      SOME shr => shr
			    | _ => let val r = ref BS_NO
				   in
				       s_put (h, r);
				       r
				   end
	    in
		shr := body_add (!shr, body)
	    end

	fun clause_compile_auto (P, f, blkl, pi) =
	    let val fmapr = t_get_table autoinfoq P
		val blklsr = t_get_table fmapr f
	    in
		t_put_behind blklsr (blkl, pi)
	    end

	fun ct_subsumed (CL (h, {}, nil, Bs, ...)) =
	    (case h of
		 HVAR P => P inset !univq
	       | HFUN (P, ...) => P inset !univq
	       | HQ q => q inset !qq
	       | HBOT botname => botname inset !botq)
		 orelse (case s_get h of
			     SOME shr => body_subsumed Bs (!shr) (* (!shr, ({}, (nil, Bs))) *)
			   | _ => false)
	  | ct_subsumed (CL (h, ...)) =
	    (case h of
		 HVAR P => P inset !univq
	       | HFUN (P, ...) => P inset !univq
	       | HQ q => q inset !qq
	       | HBOT botname => botname inset !botq)

	fun elim_subsumed_by_univ P =
	    (a_rem P;
	     s_rem (HVAR P);
	     iterate
	       s_rem (HFUN (P, f, k, vars, t))
	     | f => (k, vars, t) in map !fargsq
	     end
	     )

	(* resolve_P_f (c, psenv)
	 Resolves clause c against all automata clauses in autoinfoq, qq (if c is a non-automaton clause)
	 or against all non-automata clauses in selfq, selxq (if c is an automaton clause).
	 Adds all resolvents to waitq, as objects of type 'clause', even though
	 some are automata clauses.
	 psenv is a pathset environment that constrains variables.
	 *)
	fun resolve_P_f (c_env as (c as CL (h, {q} U ql, al, Bs, pi), psenv)) =
	    (if q inset !qq
		 then wait_insert (CL (h, ql, al, Bs,
				       p_resolve (AC_Q (q, ?(!qq) q), c, MGU_EMPTY)),
				   psenv)
	     (* resolve C \/ -q with +q, and return C in front of acc.
	      Do not add c either to forward subsumption structures or to selqq,
	      because resolvent subsumes premise. *)
	     else ( (* otherwise cannot resolve. *)
		   (* Now update selqq: *)
		   let val clsr = t_get_table selqq q
		   in
		       t_put_behind clsr c_env
		   end
		 ))
	  | resolve_P_f (c_env as (c as CL (h, {}, al as (P, t as f $ l) :: rest, Bs,
					    pi),
				   psenv)) =
	    (if P inset !univq
		 then wait_insert (CL (h, {},
				       rest, Bs,
				       p_resolve (AC_UNIV (P, ?(!univq) P), c,
						  MGU_AUTO_X1_IS t)),
				   psenv)
	     (* Do not add c either to forward subsumption structures or to selfq,
	      because resolvent subsumes premise. *)
	     else ((case a_get P of
			SOME fmap =>
			(case t_get fmap f of
			     SOME blkls =>
			     let val (k, vars, t) = ?(!fargsq) f
			     in
				 t_iter blkls
				 (fn (blkl, pi') =>
				     (
				      (* Resolve C <= P(f(t1, ..., tn)) [where l = [t1, ..., tn]]
				       with P (f (x1, ..., xn)) <= B1(x1), ..., Bn(xn)
				       [where blkl = [B1, ..., Bn]]
				       => generate C <= B1(t1), ..., Bn(tn)
				       *)
				      let val (al', Bs', psenv') =
					      gen_resolvent (l, blkl, rest, Bs, psenv)
				      in
					  if al'=rest andalso Bs'=Bs
					      then b_set c
					  else ();
					      wait_insert (CL (h, {}, al', Bs',
							       p_resolve (AC_POP (P, f, blkl, pi'),
									  c, MGU_AUTO_Xs_ARE l)),
							   psenv');
					      false
				      end handle NoPathSet => false));
				     ()
			     end
			   | _ => () (* cannot resolve: no automaton clause with head P (f (...)). *)
			     )
		      | _ => () (* cannot resolve: no automaton clause with head P(...) *)
			);
			(* Now update selfq: *)
			insert_selfq ((h, al), {Bs => (psenv, pi)}, P, f)
			))
	  | resolve_P_f (CL (_, _, (_, V _) :: _, ...), _) =
	    raise ResolvePF_Depth0
	  | resolve_P_f (c_env as (c as CL (h as HFUN (P, f, k, vars, t), {}, nil, Bs, pi), psenv)) =
	    (* automaton clause *)
	    (
	     (* first try to resolve with some C \/ -P(f(...)) with -P(f(...)) selected: *)
	     (case selfq_get P of
		  SOME fmapr =>
		  (case t_get fmapr f of
		       SOME clausesr =>
		       let val c_raw = AC_POP_RAW c
		       in
			   t_iter clausesr
			   (fn (h_al as (h', al' as (_, _ $ l') ::rest'), ref Bss) =>
			       (let val ir = ref 0
				    val blkl = [(inc ir;
						 if !ir inset Bs
						     then ?Bs (!ir)
						 else {})
					       |while !ir<k]
				    val (al'', Bs'', psenv'') =
					gen_resolvent (l', blkl, rest', {}, {})
				    val mgu' = MGU_AUTO_Xs_ARE l'
				in
				    iterate
				      let val c' = CL (h', {}, al', Bs', pi')
				      in
					  case bs_get c' of
					      NONE => (* check c' is not
						       backward subsumed. *)
					      let val Bs1 = (Bs' delta Bs'') ++
						      {i => B U B'
						      | i => B in map Bs'' <| Bs'
							  val B' = ?Bs'' i}
					      in
						  if al''=rest' andalso Bs1=Bs'
						      then b_set c'
						  else ();
						      wait_insert (CL (h', {}, al'', Bs1,
								       p_resolve (c_raw, c', mgu')),
								   pse)
					      end
					    | _ => ()
				      end
				    | Bs' => (psenv', pi') in map Bss
				    val SOME pse =
					SOME (ps_env_inter (psenv', psenv''))
					handle NoPathSetEvt => NONE
				    end
				    (*waits_insert ((h', al''), Bss')*)
				end handle NoPathSetEvt => ();
				    false));
			       if empty Bs (* unit clause *)
				   then t_remove fmapr f
			       else ()
		       end
		     | _ => ())
		| _ => ());
		  (* then try to resolve with some C \/ -P(x) with -P(x) selected: *)
		  (case selxq_get P of
		       SOME cls =>
		       (t_iter cls
			(fn (c' as CL (h', {}, nil, {1 => B}, pi'), psenv') =>
			    (* with h' of the form P'(x1), q, or bot, and B
			     containing P. *)
			    (case bs_get c' of
				 SOME _ => false
			       | _ =>
				 (let val h'' = case h' of
						    HVAR P' => HFUN (P', f, k, vars, t)
						  | _ => h'
				      val B' = B \ {P}
				      val al' = if empty B'
						    then nil
						else atom_sort {(Q, t) | Q in set B'}
				      val pse = ps_match_al (al', ps_match_Bs (Bs, {}))
				  in
				      wait_insert (CL (h'', {}, al', Bs,
						       p_resolve (AC_POP_RAW c, c',
								  MGU_OTHER_X1_IS t)),
						   pse)
				  end handle NoPathSetEvt => ();
				      false)
			       | _ => raise ResolvePF_BadSelX));
			    ())
		     | _ => ());
		     (* Finally, update autoinfoq: *)
		     let val ir = ref 0
			 val blkl = [(inc ir;
				      if !ir inset Bs
					  then ?Bs (!ir)
				      else {})
				    |while !ir<k]
		     in
			 do_verbose (2, fn () =>
				     (#put stderr "  Recording automaton clause: ";
				      perrclause c;
				      #put stderr "\n";
				      #flush stderr ())
				     );
			 clause_compile_subsumed (h, (*({}, (nil,*) Bs (*))*));
			 clause_compile_auto (P, f, blkl, pi)
		     end
		 )
	  | resolve_P_f (c_env as (c as CL (h as HVAR P, {}, nil, Bs, pi), psenv)) =
	    (* epsilon-clause *)
	    (case Bs of
		 {_ => {P1} U rest} => (* clause is P(x1) <= P1(x1), ..., with P1(x1) selected.
					Resolve with all automata clauses P1(f(...)) <= ... *)
		   (if P1 inset !univq (* first resolve with the universal clause P1(x1)
					if any. *)
			then wait_insert (CL (h, {}, nil,
					      if empty rest
						  then {}
					      else {1 => rest},
						  p_resolve (AC_UNIV (P1, ?(!univq) P1), c,
							     MGU_OTHER_X1_IS (V 1))),
					  if empty rest
					      then {}
					  else psenv)
		    (* Do not update forward subsumption structures or selxq
		     since resolvent subsumes premise. *)
		    else ((case a_get P1 of
			       SOME fmap =>
			       (t_iter fmap
				(fn (f, blkls) =>
				    let val (k, vars, t) = ?(!fargsq) f
					val h' = HFUN (P, f, k, vars, t)
				    in
					t_iter blkls
					(fn (blkl, pi') =>
					    let val jr = ref 0
						val Bs' = {!jr => blk
							  | blk in list blkl
							      such that (inc jr; not (empty blk))}
					    in
						(let val al' = if empty rest
								   then nil
							       else atom_sort {(Q, t) | Q in set rest}
						     val pse = ps_match_al (al', ps_match_Bs (Bs', {}))
						 in
						     wait_insert (CL (h', {}, al', Bs',
								      p_resolve (AC_POP (P1, f, blkl,
											 pi'),
										 c, MGU_OTHER_X1_IS t)),
								  pse);
						     false
						 end handle NoPathSetEvt => false)
					    end)
				    end);
				    ())
			     | _ => () (* no resolvent *)
			       );
			       clause_compile_subsumed (h, (*({}, (nil,*) Bs (*))*));
			       (* Now update selxq *)
			       let val csr = t_get_table selxq P1
			       in
				   t_put_behind csr c_env
			       end
			      ))
	       | _ => (* clause is just P(x): resolve with all clauses C \/ -P(...) *)
		 ( (* first try to resolve with some C \/ -P (f (...)) with -P(f(...)) selected *)
		  (case selfq_get P of
		       SOME fmapr =>
		       (t_iter fmapr
			(fn (f, clausesr) =>
			    (t_iter clausesr
			     (fn (h_al, ref Bss) =>
				 (
				  (case h_al of
				       (h', al' as (_, t' as _ $ _)::rest') =>
				       (let val mgu' = MGU_AUTO_X1_IS t'
					    val acu' = AC_UNIV (P, pi)
					in
					    iterate
					      let val c' = CL (h', {}, al', Bs', pi')
					      in
						  case bs_get c' of
						      NONE => (* check that c' is not
							       backward subsumed. *)
						      (bs_put c';
						       wait_insert (CL (h', {}, rest', Bs',
									p_resolve (acu', c', mgu')),
								    psenv'))
						    | _ => ()
					      end
					    | Bs' => (psenv', pi') in map Bss
					    end
					end handle NoPathSetEvt => ())
				     | _ => raise ResolvePF_BadSelF);
				       false))));
			    (* Now erase the P entry in selfq. *)
			    selfq_rem P)
		     | _ => ());
		      (* then resolve with clauses C \/ -P(x) with -P(x) selected *)
		       (case selxq_get P of
			    SOME cls =>
			    (t_iter cls
			     (fn (c' as CL (h', {}, nil, {x => B}, pi'), psenv') =>
				 (case bs_get c' of
				      SOME _ => false
				    | _ => (b_set c';
					    let val Bs' = case B \ {P} of
							      {} => {}
							    | B' => {x => B'}
						val pse = ps_match_Bs (Bs', {})
					    in
						wait_insert (CL (h', {}, nil, Bs',
								 p_resolve (AC_UNIV (P, pi), c',
									    MGU_AUTO_X1_IS (V x))),
							     pse)
					    end handle NoPathSetEvt => ();
					    false))
			       | _ => raise ResolvePF_BadSelX);
				 (* Now remove the P entry from selxq *)
				 selxq_rem P)
			  | _ => ());
			  do_verbose (2, fn () =>
				      (#put stderr "  Recording universal clause: ";
				       perrclause c;
				       #put stderr "\n";
				       #flush stderr ()));
			  (* and backward subsume: *)
			  elim_subsumed_by_univ P;
			  (* Now update univq *)
			  univq := !univq ++ {P => pi}
			  ))
	  | resolve_P_f (c as CL (h as HBOT botname, {}, nil, {}, pi), _) =
	    (do_bot c;
	     do_verbose (2, fn () =>
			 (#put stderr "  Recording bottom clause: ";
			  perrclause c;
			  #put stderr "\n";
			  #flush stderr ()));
	     (* Now update botq: *)
	     botq := !botq U {botname})
	  | resolve_P_f (c_env as (c as CL (h as HQ q, {}, nil, Bs, pi), psenv)) =
	    (case Bs of
		 {} => (* clause is just q *)
		   (case selqq_get q of
			SOME cls =>
			(t_iter cls
			 (fn (c' as CL (h', ql', al', Bs', pi'), psenv') =>
			     (case bs_get c' of
				  SOME _ => false
				| _ => (b_set c';
					wait_insert (CL (h', ql' \ {q}, al', Bs',
							 p_resolve (AC_Q (q, pi), c', MGU_EMPTY)),
						     psenv');
					false))
			   | _ => raise ResolvePF_BadSelQ);
			     (* Now erase the q entry from selqq: *)
			     selqq_rem q)
		      | _ => ();
			do_verbose (2, fn () =>
				    (#put stderr "  Recording non-emptiness clause: ";
				     perrclause c;
				     #put stderr "\n";
				     #flush stderr ()));
			(* Now update qq: *)
			qq := !qq ++ {q => pi}
			)
	       | {1 => {P1} U rest} => (* clause is q <= P1(x1), ..., with P1(x1) selected.
					Resolve with all automata clauses P1(f(...)) <= ... *)
		 (if P1 inset !univq (* first resolve with the universal clause P1(x1) if any. *)
		      then wait_insert (CL (h, {}, nil,
					    if empty rest
						then {}
					    else {1 => rest},
						p_resolve (AC_UNIV (P1, ?(!univq) P1), c,
							   MGU_OTHER_X1_IS (V 1))),
					if empty rest
					    then {}
					else psenv)
			  (* Do not update forward subsumption structures or selxq
			   because resolvent is subsumed by premise. *)
		  else ((case a_get P1 of
			     SOME fmap =>
			     (t_iter fmap
			      (fn (f, blkls) =>
				  let val (k, vars, t) = ?(!fargsq) f
				  in
				      t_iter blkls
				      (fn (blkl, pi') =>
					  let val jr = ref 0
					      val Bs' = {!jr => blk
							| blk in list blkl
							    such that (inc jr; not (empty blk))}
					  in
					      (let val al' = if empty rest
								 then nil
							     else atom_sort {(Q, t) | Q in set rest}
						   val pse = ps_match_al (al', ps_match_Bs (Bs', {}))
					       in
						   wait_insert (CL (h, {}, al', Bs',
								    p_resolve (AC_POP (P1, f, blkl, pi'),
									       c, MGU_OTHER_X1_IS t)),
								pse);
						   false
					       end handle NoPathSetEvt => false)
					  end)
				  end);
				  ())
			   | _ => () (* no resolvent *)
			     );
			     clause_compile_subsumed (h, (*({}, (nil,*) Bs (*))*));
			     (* Update forward subsumption structures: *)
			     (* Now update selxq *)
			     let val csr = t_get_table selxq P1
			     in
				 t_put_behind csr c_env
			     end
			    ))
	       | _ => raise ResolvePF_BlackHole
		 )
	  | resolve_P_f _ = raise ResolvePF_BlackHole; (* remaining cases for resolve_P_f:
							should never happen. *)

	fun resolve_P_fs ((h, nil), Bss) =
	    iterate
	      (case bs_get c of
		   SOME _ => ()
		 | _ => wait_insert (c, psenv))
	    | Bs => (psenv, pi) in map Bss
	    val c = CL (h, {}, nil, Bs, pi)
	    end
	  | resolve_P_fs (h_al as (h, al as (P, t' as f $ l)::rest), Bss) =
	    (if P inset !univq
		 then let val pi' = ?(!univq) P
			  val acu' = AC_UNIV (P, pi')
			  val mgu' = MGU_AUTO_X1_IS t'
		      in
			  iterate
			    let val c' = CL (h, {}, al, Bs, pi)
			    in
				case bs_get c' of
				    NONE => (* check that c' is not
					     backward subsumed. *)
				    (bs_put c';
				     wait_insert (CL (h, {}, rest, Bs,
						      p_resolve (acu', c', mgu')),
						  psenv))
				  | _ => ()
			    end
			  | Bs => (psenv, pi) in map Bss
			  end
		      end
	     else ();
		 (case a_get P of
		      SOME fmap =>
		      (case t_get fmap f of
			   SOME blkls =>
			   let val (k, vars, t) = ?(!fargsq) f
			   in
			       t_iter blkls
			       (fn (blkl, pi') =>
				   (let val (al', Bs', psenv') =
					    gen_resolvent (l, blkl, rest, {}, {})
					val mgu' = MGU_AUTO_Xs_ARE l
					val c_raw = AC_POP (P, f, blkl, pi')
				    in
					iterate
					  let val c = CL (h, {}, al, Bs, pi)
					  in
					      case bs_get c of
						  NONE => (* check that c
							   is not backward
							   subsumed. *)
						  let val Bs1 = (Bs delta Bs') ++
							  {i => B U B'
							  | i => B in map Bs' <| Bs
							      val B' = ?Bs' i}
						  in
						      if al'=rest andalso Bs1=Bs
							  then b_set c
						      else ();
							  wait_insert (CL (h, {}, al', Bs1,
									   p_resolve (c_raw, c, mgu')),
								       pse)
						  end
						| _ => ()
					  end
					| Bs => (psenv, pi) in map Bss
					val SOME pse =
					    SOME (ps_env_inter (psenv,
								psenv'))
					    handle NoPathSetEvt => NONE
					end;
					false
				    end handle NoPathSetEvt => false));
				   ()
			   end
			 | _ => ())
		    | _ => ());
		      insert_selfq (h_al, Bss, P, f))
	  | resolve_P_fs _ = raise ResolvePFs_BlackHole

	    (*
	val current_low = ref max_int
	     *)

	fun resolve () =
	    (let val (info, cc) = scc (!predicate_graph, P_ROOT)
		 val (condensed, root) = scc_condense (!predicate_graph, P_ROOT, info, cc)
		 val numbering = revtopsort (condensed, root)
		 val inv_cc = overwrite [{P => low
					 | P in set preds}
					| low => preds in map cc]
		 val dfsinfo = {P => (dfsnum, ?numbering (?inv_cc P))
			       | P => (dfsnum, _) in map info}
		 val sccinfo = cc O inv numbering
	     in
		 dfs_info := dfsinfo;
		 scc_info := sccinfo;
		 dfs_q_info := {};
			   (*
		 current_low := 0;
			    *)
		 univq := {}; qq := {}; t_reset selfq; t_reset selxq; t_reset selqq; botq := {};
		 t_reset autoinfoq; t_reset back_subs;
		 let val (sk, (* tr, *) bots) = compute_skeleta (!clause_list, maxpathlen)
		 in
		     skeleta := sk;
			   (*
		     toprels := tr;
			    *)
		     skel_bots := bots
		 end;
		 do_verbose (3, fn () => (#put stderr "Found ";
					  print stderr (pack (card sccinfo));
					  #put stderr " strongly connected components:\n";
					  iterate
					    (#put stderr "  [";
					     print stderr (pack low);
					     #put stderr "] ";
					     let val cc = sort (fn (pred, pred') =>
								   #1 (?dfsinfo pred) > #1 (?dfsinfo pred'))
						     (?sccinfo low)
						 val delimr = ref ""
					     in
						 iterate
						   (#put stderr (!delimr);
						    delimr := ", ";
						    case pred of
							P_ROOT => #put stderr "*"
						      | P_BOT botname => #put stderr botname
						      | P_PRED P => #put stderr P)
						 | pred in list cc
						 end;
						 #put stderr "\n"
					     end)
					  | low in list sort (op <) sccinfo
					  end;
					  #put stderr "Skeleta:\n";
					  iterate
					    (#put stderr P;
					     #put stderr ": ";
					     perr_pathset (?(!skeleta) P);
					     #put stderr "\n")
					  | P in list pred_sort (!skeleta)
					    val ps = ?(!skeleta) P
					  end;
					  #flush stderr ()))
	     end;
	     let val fsig = clause_list_sig (!clause_list)
		 val ir = ref 0
	     in
		 fargsq := {f => (ir := 0;
				  (k, 1 to k, f $ [V (inc ir; !ir)
						  |while !ir<k]))
			   | f => k in map fsig}
	     end;
	     iterate
		 if useful c
		     then (let val CL (_, _, al, Bs, ...) = c
			       val psenv = ps_match_al (al, ps_match_Bs (Bs, {}))
			   in
			       wait_insert (c, psenv)
			   end handle NoPathSetEvt => ())
		 else (do_verbose (1, fn () =>
				   (#put stderr "Ignoring useless clause ";
				    perrclause c;
				    #put stderr "\n";
				    #flush stderr ()));
		       case c of (* c is useless, but we need to produce a model of it:
				  just take the head to be always true. *)
			   CL (HVAR P, ...) => univq := !univq ++ {P => P_GIVEN "*magic*"}
			 | CL (HFUN (P, ...), ...) => univq := !univq ++ {P => P_GIVEN "*magic*"}
			 | _ => raise ResolveUseful)
	     | c in list !clause_list
	     end;
	     clause_list := nil;
	     (*dealtwith := {};*)
	     while true do
		 let val (_, (c_env as (c, _))) = wait_pop ()
		 in
		     case bs_get c of
			 SOME _ => ()
		       | _ =>
			 if (* c inset !dealtwith orelse *) ct_subsumed c
			     then do_verbose (2, fn () =>
					      (#put stderr "  Removing forward subsumed clause: ";
					       perrclause c;
					       #put stderr "\n";
					       #flush stderr ()))
			 else (do_verbose (2, fn () => (#put stderr "  Picking clause: ";
							perrclause c;
							#put stderr "\n";
							#flush stderr ()));
			       ( (*dealtwith := !dealtwith U {c};*)
				eps_back_subsume c;
				resolve_P_f c_env))
		 end)
		 handle MHeapEmptyEvt => ()
    in
	|[ new_clause = new_clause,
	   resolve = resolve,
	   get_automaton = (fn () => (t_collect autoinfoq
				      (fn (P, fmap) =>
					  {P => t_collect fmap
					    (fn (f, blkls) =>
						let val (k, vars, ...) = ?(!fargsq) f
						    val blkls' = t_collect blkls
							(fn (blkl, pi) =>
							    {blkl => pi})
						in
						    {f => (blkls', k, vars)}
						end
						)}
					    ),
					  !univq)),
	   get_clauses = (fn () => !clause_list @ map #1 (get_clauses ())),
	   get_true_botnames = (fn () => !botq)
	   ]|
    end;

fun clause_from_automaton_clause (AC_UNIV (P, pi)) =
    CL (HVAR P, {}, nil, {}, pi)
  | clause_from_automaton_clause (AC_Q (q, pi)) =
    CL (HQ q, {}, nil, {}, pi)
  | clause_from_automaton_clause (AC_POP (P, f, bl, pi)) =
    let val ir = ref 0
	val Bs = {(inc ir; !ir) => B
		 | B in list bl}
	val k = len bl
	val vars = 1 to k
	val t = (ir := 0; f $ [V (inc ir; !ir)
			      | _ in list bl])
    in
	CL (HFUN (P, f, k, vars, t), {}, nil, Bs, pi)
    end
  | clause_from_automaton_clause (AC_POP_RAW c) = c;

fun clean_automaton (Pmap, umap) =
    AUTO ({P => {f => ({blkl | blkl in set blkls}, k, vars)
		| f => (blkls, k, vars) in map fmap}
	  | P => fmap in map Pmap},
	    dom umap);
