(* 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";
open "gensym_h";

(*$P+*)

datatype smash = SMASH_NONE
       | SMASH_ONE_NEG_LIT;

val smash = SMASH_NONE;

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_UNIT _ => #put stderr "[obvious]"
	| P_AUTO_RESOLVE _ => #put stderr "[by automaton resolution]"
	| P_Q_RESOLVE _ => #put stderr "[by q-resolution]"
	| P_EPS_RESOLVE _ => #put stderr "[by epsilon resolution]"
	| P_SPLIT_USE _ => #put stderr "[by splitting]"
	| P_SPLIT_DEF =>
	  #put stderr "[defining clause for splitting symbol]"
	| P_SPLIT_SPLIT _ => #put stderr "[by q-splitting]"
	| _ => #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 CheckAtomSort;

fun check_atom_sort (a :: (l as a' :: _)) =
    if a=a' orelse atom_less (a, a')
	then raise CheckAtomSort
    else check_atom_sort l
  | check_atom_sort _ = ();
*)

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;

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)

val pred_less = op strless;
val pred_sort = sort pred_less;

(* The prover: *)

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

exception ResolvePF_BadHead;
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');


(*
exception RandChoose;

fun rand_choose {} = raise RandChoose
  | rand_choose {i} =  i
  | rand_choose s = let val (s1, s2) = split s
		    in
			if maybe ()
			    then rand_choose s1
			else rand_choose s2
		    end;

fun random_oracle_funs (fargs : string -m> int * int set * int term, dsize : int) =
    let val dsize2 = dsize*dsize
	val D = 0 to dsize-1
	fun rand_table (a, siz) =
	    let val ir = ref siz
	    in
		while (dec ir; !ir>=0) do
		    iupdate (a, !ir, irand dsize)
	    end
	fun rand_permut {} = nil
	  | rand_permut s =
	    let val i = rand_choose s
	    in
		i :: rand_permut (s \ {i})
	    end
	val cons_table = iarrayoflist [j mod dsize
				      | j in list rand_permut (0 to dsize2-1)]
	(* we draw a random surjective function to represent cons pairs;
	 n-ary functions f (t1, ..., tn) are encoded as
	 f (cons (t1, cons (..., cons (tn, nil)))),
	 where nil = 0, and f is a random function from 0..dsize-1 to 0..dsize-1.
	 *)
	val f_tables = {f => iarrayoflist (rand_permut D)
		       | f => (k, ...) in map fargs}
	(* t_table (vars, t) produces a relation mapping
	 cons (x1, ..., cons (xn, nil)) to t
	 where vars = {x1, ..., xn} contains all free variables of t.
	 *)
	fun cons (i, j) =
	    isub (cons_table, dsize*i+j)
	val nihil = 0
	memofun t_table (vars, V x) =
		let val x1 = choose vars
		    val vars' = vars \ {x1}
		in
		    if x1=x
			then if empty vars'
				 then union_rel {{cons (d, nihil) => {d}}
						| d in set D}
			     else union_rel
		end
    in
	rand_table (cons_table, dsize2);

    end;
*)

(*
datatype qenv_set = Q_ONE
       | Q_Z
       | Q_B of int * (string -m> qenv_set); (* variable, then a q_env_set
					      for each value of the variable
					      (which should be a state, i.e.,
					      a string). *)

exception QEnvInter;

fun qenv_funs () =
    let fun q_b (x, {}) = Q_Z
	  | q_b xmap = Q_B xmap
	memofun qenv_union {} = Q_Z
	      | qenv_union {qe} = qe
	      | qenv_union {qe1, qe2} =
		(case qe1 of
		     Q_Z => qe2
		   | Q_ONE => Q_ONE
		   | Q_B (x1, map1) =>
		     (case qe2 of
			  Q_Z => qe1
			| Q_ONE => Q_ONE
			| Q_B (x2, map2) =>
			  if x1 = x2
			      then Q_B (x1, (map1 delta map2) ++
					{P => qenv_union {qe'1, qe'2}
					| P => qe'1 in map map2 <| map1
					  val qe'2 = ?map2 P})
			  else if x1 < x2
			      then Q_B (x1, {P => qenv_union {qe'1, qe2}
					    | P => qe'1 in map map1})
			  else Q_B (x2, {P => qenv_union {qe1, qe'2}
					| P => qe'2 in map map2})
			      ))
	      | qenv_union qes =
		let val (qes1, qes2) = split qes
		in
		    qenv_union {qenv_union qes1, qenv_union qes2}
		end
	memofun qenv_inter {} = raise QEnvInter
	      | qenv_inter {qe} = qe
	      | qenv_inter {qe1, qe2} =
		(case qe1 of
		     Q_Z => Q_Z
		   | Q_ONE => Q_ONE
		   | Q_B (x1, map1) =>
		     (case qe2 of
			  Q_Z => Q_Z
			| Q_ONE => qe1
			| Q_B (x2, map2) =>
			  if x1 = x2
			      then q_b (x1, {P => qe'
					    | P => qe'1 in map map2 <| map1
						val qe'2 = ?map2 P
						val qe' = qenv_inter {qe'1, qe'2}
						    such that qe'<>Q_Z})
			  else if x1 < x2
			      then q_b (x1, {P => qe'
					    | P => qe'1 in map map1
						val qe' = qenv_inter {qe'1, qe2}
						    such that qe'<>Q_Z})
			  else q_b (x2, {P => qe'
					| P => qe'2 in map map2
					    val qe' = qenv_inter {qe1, qe'2}
					    such that qe'<>Q_Z})
			  ))
	      | qenv_inter qes =
		let val (qes1, qes2) = split qes
		in
		    qenv_inter {qenv_inter qes1, qenv_inter qes2}
		end
    in
	|[ union = qenv_union,
	   inter = qenv_inter
	   ]|
    end;

fun auto_match_funs (AUTO (auto, univ)) =
    let val |[union = qenv_union, inter = qenv_inter, ...]| = qenv_funs ()
	memofun auto_match_term (P, t) =
		if P inset univ
		    then Q_ONE
		else case t of
			 V x => Q_B (x, {P => Q_ONE})
		       | f $ l =>
			 if P inset auto
			     then let val fmap = ?auto P
				  in
				      if f inset fmap
					  then qenv_union {auto_match_terml (blkl, l)
							  | blkl in set #1 (?fmap f)}
				      else Q_Z
				  end
			 else Q_Z
	with auto_match_terml (blk::blkl, t::l) =
	     qenv_inter ({auto_match_terml (blkl, l)} U
			   {auto_match_term (P, t)
			   | P in set blk})
	   | auto_match_terml (nil, nil) = Q_ONE
	   | auto_match_terml _ = Q_Z
	fun auto_eval_var (x, Q_ONE) = 
    in
 !!!
    end;
*)

(*
datatype path = PS_ALL
       | PS_CONT of string * string option list * string option list * path;

fun neighbors_included (l, l') =
    all
      (case sopt' of
	   SOME s' =>
	   (case sopt of
		SOME s => s=s'
	      | _ => false)
	 | _ => true)
    || sopt in list l
    and sopt' in list l'
    end handle ParSweep => false;

fun path_included (_, PS_ALL) = true
  | path_included (PS_ALL, _) = false
  | path_included (PS_CONT (f, left, right, p),
		   PS_CONST (f', left', right', p')) =
    f=f' andalso
    neighbors_included (left, left') andalso
    neighbors_included (right, right') andalso
    path_included (p, p');
*)
	    
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. *)

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_collect (PS_ALL, ps) = ps
  | ps_collect (ps, PS_ALL) = ps
  | ps_collect (PS_ENUM fimap, PS_ENUM fimap') =
    PS_ENUM ((fimap delta fimap') ++
		 {fi => ps''
		 | fi => ps in map (fimap' <| fimap)
		     val ps' = ?fimap' fi
		     val ps'' = ps_collect (ps, ps')
		     such that ps''<>ps_empty});

fun ps_dcollect {} = PS_ALL
  | ps_dcollect {ps} = ps
  | ps_dcollect pss =
    let val (pss1, pss2) = split pss
    in
	ps_collect (ps_dcollect pss1, ps_dcollect pss2)
    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_dunion {} = ps_empty
  | ps_dunion {ps} = ps
  | ps_dunion pss =
    let val (pss1, pss2) = split pss
    in
	ps_union (ps_dunion pss1, ps_dunion pss2)
    end;
*)

fun ps_from_term (V _) = PS_ALL
  | ps_from_term (f $ nil) =
    PS_ENUM {(f, 0) => PS_ALL}
  | ps_from_term (f $ l) =
    let val ir = ref 0
    in
	PS_ENUM {(inc ir; (f, !ir)) => ps_from_term t
		| t in list l}
    end;

fun ps_from_clause (CL (h, _, al, Bs, ...)) =
    ps_collect ((case h of
		     HVAR _ => PS_ALL
		   | HFUN (_, _, _, _, t) =>
		     ps_from_term t
		   | _ => ps_empty),
		     ps_dcollect {ps_from_term t
				 | (_, t) in list al});

fun ps_from_clauses cl =
    ps_dcollect {ps_from_clause c
		| c in list cl};

fun ps_chop (_, t as V _) = t
  | ps_chop (_, t as _ $ nil) = t
  | ps_chop (PS_ALL, _) = V ()
  | ps_chop (PS_ENUM fimap, f $ l) =
    let val ir = ref 0
    in
	f $ [let val fi = (inc ir; (f, !ir))
	     in
		 if fi inset fimap
		     then ps_chop (?fimap fi, t)
		 else ps_chop (PS_ALL, t)
	     end
	    | t in list l]
    end;

exception SimpleMatchEvt;

fun simple_term_inter (V _, t) = t
  | simple_term_inter (t, V _) = t
  | simple_term_inter (f $ l, f' $ l') =
    if f=f'
	then f $ [simple_term_inter (t, t')
		 || t in list l and
		    t' in list l']
    else raise SimpleMatchEvt;

fun sk_inter (NONE, sk) = sk
  | sk_inter (sk, NONE) = sk
  | sk_inter (SOME fmap, SOME fmap') =
    SOME ((fmap delta fmap') ++
	      {f => tset_inter
	      | f => tset in map fmap' <| fmap
		  val tset' = ?fmap' f
		  val tset_inter = {t_inter
				   | t in set tset and
				     t' in set tset'
				       val SOME t_inter = SOME (simple_term_inter (t, t'))
					   handle SimpleMatchEvt => NONE}});

fun sk_env_inter (psenv, psenv') =
    (psenv delta psenv') ++
    {x => sk_inter (sk, sk')
    | x => sk in map psenv' <| psenv
      val sk' = ?psenv' x};

fun simple_match_term (V x, t, sigma) =
    let val sigma_x = if x inset sigma
			  then ?sigma x
		      else V ()
    in
	sigma ++ {x => simple_term_inter (sigma_x, t)}
    end
  | simple_match_term (f $ l, f' $ l', sigma) =
    if f=f'
	then simple_match_term_list (l, l', sigma)
    else raise SimpleMatchEvt
  | simple_match_term (pat, V (), sigma) =
    {x => V ()
    | x in set tvars pat}
and simple_match_term_list (nil, nil, sigma) = sigma
  | simple_match_term_list (t::l, t' :: l', sigma) =
    simple_match_term_list (l, l', simple_match_term (t, t', sigma))
  | simple_match_term_list _ = raise SimpleMatchEvt;

type simple_terms = (string -m> unit term set) option;
type simple_env = int -m> simple_terms;

fun ps_in (_, NONE) = true
  | ps_in (V _, _) = false
  | ps_in (t as f $ _, SOME fmap) =
    f inset fmap andalso
    t inset ?fmap f;

fun ps_compat (_, NONE) = true
  | ps_compat (_, SOME {}) = false
  | ps_compat (V _, _) = true
  | ps_compat (t as f $ l, SOME fmap) =
    f inset fmap andalso
    exists
      ((simple_term_inter (t, t'); true) handle SimpleMatchEvt => false)
    | t' in set ?fmap f
    end;

fun ps_add (V _, _) = NONE
  | ps_add (_, NONE) = NONE
  | ps_add (t as f $ _, SOME fmap) =
    SOME (fmap ++ {f => if f inset fmap
			    then ?fmap f U {t}
			else {t}});

val perr_skterm = print_term (stderr, fn _ => "*");

datatype simple_clause = SCL of head * (string * int term) list * (int -m> unit term);

exception ComputeSkeletaP;

fun compute_skeleta (cl, maxpathlen) =
    let val facts = ref ({} : string -m> simple_terms)
	val bots = ref ({} : string set)

	val all_ps = ps_from_clauses cl

	val selq : (string, simple_clause set) table
	    = table ()
	val selq_get = t_get selq
	val selq_put = t_put selq

	val waitq : simple_clause list ref =
	    ref [SCL (h,
		      al @ append [[(P, V i)
				   | P in set B]
				  | i => B in map Bs],
		      {})
		| CL (h, _, al, Bs, ...) in list cl
		  such that (case h of
				 HQ _ => false
			       | _ => true)]
    in
	while not (null (!waitq)) do
	    let val c :: others = !waitq
	    in
		waitq := others;
		case c of
		    SCL (HBOT botname, nil, _) =>
		    bots := !bots U {botname}
		  | SCL (h, nil, sigma) =>
		    let val P = (case h of
				     HFUN (P, ...) => P
				   | HVAR P => P
				   | _ => raise ComputeSkeletaP)
			val t = (case h of
				     HFUN (_, f, k, ...) =>
				     if k=0
					 then f $ nil
				     else (case all_ps of
					       PS_ALL =>
					       let val ir = ref 0
					       in
						   f $ [(inc ir; V ())
						       |while !ir < k]
					       end
					     | PS_ENUM fimap => 
					       let val ir = ref 0
					       in
						   f $ [let val fi = (inc ir; (f, !ir))
							in
							    if fi inset fimap
								then ps_chop (?fimap fi,
									      if !ir inset sigma
										  then ?sigma (!ir)
									      else V ())
							    else V ()
							end
						       |while !ir<k]
					       end)
				   | HVAR _ =>
				     if 1 inset sigma
					 then ?sigma 1
				     else V ())
			val oldP =
			    if P inset !facts
				then ?(!facts) P
			    else SOME {}
		    in
			if ps_in (t, oldP)
			    then ()
			else (facts := !facts ++ {P => ps_add (t, oldP)};
			      do_verbose (2, fn () =>
					  (#put stderr "|~ ";
					   #put stderr P;
					   #put stderr " ";
					   perr_skterm t;
					   #put stderr "\n";
					   #flush stderr ()));
			      case selq_get P of
				  SOME cs =>
				  iterate
				    (let val sigma' = simple_match_term (pat, t, sigma)
				     in
					 waitq := SCL (h, al, sigma') :: !waitq
				     end handle SimpleMatchEvt => ())
				  | SCL (h, (_, pat)::al, sigma) in set cs
				  end
				| _ => ()
			      )
		    end
		  | (c as SCL (h, (P, pat)::al, sigma)) =>
		    ((case selq_get P of
			  SOME cs =>
			  selq_put (P, cs U {c})
			| _ => selq_put (P, {c}));
			  if P inset !facts
			      then case ?(!facts) P of
				       NONE =>
				       (let val sigma' = simple_match_term (pat, V (), sigma)
					in
					    waitq := SCL (h, al, sigma') :: !waitq
					end handle SimpleMatchEvt => ())
				     | SOME fmap => 
				       iterate
					 iterate
					   (let val sigma' = simple_match_term (pat, t, sigma)
					    in
						waitq := SCL (h, al, sigma') :: !waitq
					    end handle SimpleMatchEvt => ())
					 | t in set tset
					 end
				       | _ => tset in map fmap
				       end
			  else ()
			      )
	    end;
	    (!facts, !bots)
    end;

(*	    
datatype pathset = PS_ALL
       | PS_ENUM of string * string list * string list -m> pathset;
(* maps (f, left, right) non-empty pathset; left and right form the
 neighbor information: they are lists of possible function symbols at the top of
 arguments 1..i-1, resp. i+1..n, of f;
 maps (f, nil, nil) 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 putsopt s = puts s
	fun printps PS_ALL = (put (!delimr); delimr := ", ";
			      truncate (); put (convert ()); put "*")
	  | printps (PS_ENUM fimap) =
	    let val pos = tell ()
	    in
		iterate
		  (seek pos;
		   if null left andalso null right
		       then (put (!delimr); delimr := ", ";
			     truncate (); put (convert ()); put f)
		   else let val delr = ref "["
			in
			    puts f;
			    iterate
			      (puts (!delr);
			       delr:=",";
			       putsopt sopt)
			    | sopt in list left
			    end;
			    puts (!delr);
			    delr := ",";
			    puts "_";
			    iterate
			      (puts (!delr);
			       delr:=",";
			       putsopt sopt)
			    | sopt in list right
			    end;
			    puts "]";
			    printps ps
			end
		       )
		| (f, left, right) => 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;
*)

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

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

	val ci = clause_index cl

	val changed_P = ref ({} : string set)

	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 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, nil, nil) 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_atom ((P, t), env) =
	    if P inset !pathsets
		then ps_match_term (t, ?(!pathsets) P, env)
	    else raise NoPathSetEvt

	fun ps_match_al (nil, env) = env
	  | ps_match_al (a::al, env) =
	    ps_match_al (al, ps_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 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 ps_match_blks ({}, env) = env
	  | ps_match_blks ({x => blk} U rest, env) =
	    ps_match_blks (rest, ps_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 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 <| ci}
		     end
		 end)
    in
	ps_saturate cl;
	(!pathsets, !bots)
    end;
*)

(*!!! to finish; probably a good idea.
fun compute_char_states (cl, maxq) =
    let val preds : (string, automaton) table = table ()
	fun newstate_0 () = gensym "q"
	val remaining_states = ref maxq
	val existing_states = ref {}
	fun random_state {} = newstate_0 ()
	  | random_state {q} = q
	  | random_state s =
	    let val (s1, s2) = split s
	    in
		random_state (if maybe ()
				  then s1
			      else s2)
	    end
	fun newstate () =
	    if !remaining_states=0
		then random_state (!existing_states)
	    else let val q = newstate_0 ()
		 in
		     dec remaining_states;
		     existing_states := !existing_states U {q};
		     q
		 end
    in
    end;
*)

(* compute_witnesses tries to compute obvious facts
 derivable from a list cl of clauses. *)
datatype wshape = W_CST
       | W_APP of string -m> wshape list set;

fun w_from_term (V _) = W_CST
  | w_from_term (f $ l) =
    (case l of
	 nil => W_CST
       | _ => W_APP {f => {[w_from_term t | t in list l]}});

fun w_union (W_CST, w) = w
  | w_union (w, W_CST) = w
  | w_union (W_APP fmap, W_APP fmap') =
    W_APP (fmap Urel fmap');

fun w_dunion {} = W_CST
  | w_dunion {w} = w
  | w_dunion ws =
    let val (ws1, ws2) = split ws
    in
	w_union (w_dunion ws1, w_dunion ws2)
    end;

fun w_from_head (HVAR _) = W_CST
  | w_from_head (HFUN (_, _, _, _, t)) = w_from_term t
  | w_from_head _ = W_CST;

fun w_from_clause (CL (h, _, al, Bs, ...)) =
    w_dunion {w_from_term t
	     | (_, t) in list al};

fun w_match (V _, _) = true
  | w_match (_ $ nil, _) = true
  | w_match (_ $ _, W_CST) = false
  | w_match (f $ l, W_APP fmap) =
    f inset fmap andalso
    exists
      all
	w_match (t, w)
      || t in list l and
	 w in list wl
      end
    | wl in set ?fmap f
    end;

exception MatchTermEvt;

fun compute_witnesses cl =
    let val ci = clause_index cl
	val wsh = w_dunion {w_from_clause c
			   | c in list cl}
	val facts = ref ({} : string -m> unit term -m> unit_proof)
	    (* Facts are ground terms.  The special variable V () denotes
	     some fixed constant. *)
	val bots = ref ({} : string -m> unit_proof)
	    (* maps botname to proof. *)
	fun match_term (sigma, V x, t) =
	    if x inset sigma
		then if ?sigma x=t
			 then sigma
		     else raise MatchTermEvt
	    else sigma ++ {x => t}
	  | match_term (sigma, f $ l, t) =
	    (case t of
		 f' $ l' =>
		 if f=f'
		     then match_tl (sigma, l, l')
		 else raise MatchTermEvt
	       | _ => raise MatchTermEvt)
	and match_tl (sigma, nil, nil) = sigma
	  | match_tl (sigma, t::l, t'::l') =
	    match_tl (match_term (sigma, t, t'), l, l')
	  | match_tl _ = raise MatchTermEvt

	val changed_P = ref ({} : string set)

	fun add_fact (P, v, up) =
	    if P inset !facts
		then let val vs = ?(!facts) P
		     in
			 if v inset vs
			     then ()
			 else (do_verbose (3, fn () =>
					   (#put stderr "New fact ";
					    #put stderr P;
					    #put stderr " ";
					    print_term (stderr, fn () => "*") v;
					    #put stderr "\n";
					    #flush stderr ()));
			       facts := !facts ++ {P => vs ++ {v => up}};
			       changed_P := !changed_P U {P})
		     end
	    else (do_verbose (3, fn () =>
			      (#put stderr "New fact ";
			       #put stderr P;
			       #put stderr " ";
			       print_term (stderr, fn () => "*") v;
			       #put stderr "\n";
			       #flush stderr ()));
		  facts := !facts ++ {P => {v => up}};
		  changed_P := !changed_P U {P})

	fun w_eval_clause (c as CL (h, _, al, Bs, ...), newfacts) =
	    if (case h of
		    HBOT botname => botname inset !bots
		  | HQ _ => true (* ignore q heads. *)
		  | _ => false)
		then ()
	    else let fun w_eval_Bs ({}, sigma, upl) =
			 (case h of
			      HVAR P =>
			      let val v = if 1 inset sigma
					      then ?sigma 1
					  else V ()
			      in
				  add_fact (P, v, UP (c, sigma, rev upl))
			      end
			    | HFUN (P, f, k, vars, ...) =>
			      let val sigma' = sigma ++ {x => V ()
							| x in set sigma <-| vars}
				  val ir = ref 0
				  val v = f $ [(inc ir;
						?sigma' (!ir)
						)
					      |while !ir<k]
			      in
				  if w_match (v, wsh)
				      then add_fact (P, v, UP (c, sigma', rev upl))
				  else () (* term too large: ignore it. *)
			      end
			    | HBOT botname =>
			      bots := !bots ++ {botname => UP (c, sigma, rev upl)}
			    | _ => ())
		       | w_eval_Bs ({i => B0 as ({P} U B)} U rest, sigma, upl) =
			 if i inset sigma
			     then let val v = ?sigma i
				  in
				      if P inset newfacts
					  then let val vs = ?newfacts P
					       in
						   if v inset vs
						       then w_eval_Bs (if empty B
									   then rest
								       else rest ++ {i => B},
									   sigma, ?vs v :: upl)
						   else ()
					       end
				      else ()
				 end
			 else if (case h of
				 HVAR _ => i<>1
			       | HFUN _ => false
			       | _ => true) (* if we don't need to browse through all values v
					     such that P(v) is derivable; we just need to check
					     whether there is one. *)
			     then (case inter {if Q inset newfacts
						   then ?newfacts Q
					       else {}
					      | Q in set B0} of
				       {v => _, ...} =>
					 w_eval_Bs (if empty B
							then rest
						    else rest ++ {i => B},
							sigma ++ {i => v},
							?(?newfacts P) v :: upl)
				     | _ => ())
			 else let val Bs' = if empty B
						then rest
					    else rest ++ {i => B}
			      in
				  iterate
				    w_eval_Bs (Bs', sigma ++ {i => v}, up::upl)
				  | v => up in map
				    if P inset newfacts
					then if empty B
						 then ?newfacts P
					     else (inter {?newfacts Q
							 | Q in set B}
						   <| ?newfacts P
						   handle MapGet => {})
				    else {}
				  end
			      end
		     fun w_eval_al (nil, sigma, upl) =
			 w_eval_Bs (Bs, sigma, upl)
		       | w_eval_al ((P, t) :: al, sigma, upl) =
			 iterate
			   (let val sigma' = match_term (sigma, t, v)
			    in
				w_eval_al (al, sigma', up::upl)
			    end handle MatchTermEvt => ())
			 | v => up in map
			   if P inset newfacts
			       then ?newfacts P
			   else {}
			 end
	    in
		w_eval_al (al, {}, nil)
	    end

	fun w_saturate clauses =
	    (changed_P := {};
	     iterate
	       w_eval_clause (c, {})
	     | c in list cl
	     end;
	     while not (empty (!changed_P)) do
		 let val Ps = !changed_P
		     val newfacts = !facts
		 in
		     changed_P := {};
		     iterate
		       w_eval_clause (c, newfacts)
		     | c in set union {cs
				      | _ => cs in map Ps <| ci}
		     end
		 end
	     )
    in
	w_saturate cl;
	(!facts, !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);

exception CtSubsumedEvt;

fun resolver (do_bot : clause -> unit, maxpathlen, wantproof) =
    let val (p_unit, p_auto_resolve, p_eps_resolve, p_q_resolve,
	     p_split_use, p_split_split) =
	    if wantproof
		then (P_UNIT, P_AUTO_RESOLVE, P_EPS_RESOLVE, P_Q_RESOLVE,
		      P_SPLIT_USE, P_SPLIT_SPLIT)
	    else let val dummy_pi = P_GIVEN "<recipe>"
		 in
		     (fn _ => dummy_pi, fn _ => dummy_pi, fn _ => dummy_pi, 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> (string -m> unit term set) option)
	val skel_bots = ref ({} : string set)
	val sure_facts = ref ({} : string -m> unit term -m> unit_proof)

	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 selqq : (block, (clause, simple_env) table) table
	    =  table ()
	    (* maps q to each clause of the form C \/ -q with -q selected. *)
	val selqq_get = t_get selqq
	val selqq_put = t_put selqq
	val selqq_rem = t_remove selqq

	val selfq : (string,
		     (string,
		      (head * atom list * atom list,
		       ((int -m> block) -m> simple_env * 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, (head * (int -m> block), simple_env * proof) 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 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

	fun blkl_from_Bs (Bs, k) =
	    let val ir = ref 0
	    in
		[(inc ir;
		  if !ir inset Bs
		      then ?Bs (!ir)
		  else {})
		|while !ir<k]
	    end

	     (* remove clause from tables selqq, selxq, selfq, autoinfoq. *)
	fun bs_put (c as CL (_, {q, ...}, ...)) =
	    (case selqq_get q of
		 SOME clsr =>
		 t_remove clsr c
	       | _ => ())
	  | bs_put (c as CL (h, _, al as (P, f $ _) :: _, Bs, ...)) =
	    (case selfq_get P of
		 SOME fmapr =>
		 (case t_get fmapr f of
		      SOME clsr =>
		      let val cls_get = t_get clsr
			  fun al_rem (nil, _) = ()
			    | al_rem (al as a::rest, acc) =
			      (case cls_get (h, al, acc) of
				   SOME bssr => bssr := {Bs} <-| !bssr
				 | _ => ();
				   al_rem (rest, a::acc))
		      in
			  al_rem (al, nil)
		      end
		    | _ => ())
	       | _ => ())
	  | bs_put (c as CL (HFUN (P, f, k, ...), _, _, Bs, ...)) =
	    (case a_get P of
		 SOME fmapr =>
		 (case t_get fmapr f of
		      SOME blklsr =>
		      t_remove blklsr (blkl_from_Bs (Bs, k))
		    | _ => ())
	       | _ => ())
	  | bs_put (c as CL (HVAR _, ...)) = ()
	  | bs_put (c as CL (h, _, _, Bs, ...)) =
	    if empty Bs
		then ()
	    else let val {i => {P, ...}, ...} = Bs
		 in
		     case selxq_get P of
			 SOME cls =>
			 t_remove cls (h, Bs)
		       | _ => ()
		 end

	fun b_set c = 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 ()
	  | 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')

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

	fun wait_insert_1 (c_env as (c, psenv : simple_env)) =
	    (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 (clause_category c, c_env))

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

	fun se_check_empty (SOME {}) = raise SimpleMatchEvt
	  | se_check_empty sk = sk

	fun se_match_term (t, NONE : simple_terms, env : simple_env) =
	    env
	  | se_match_term (V x, sk as SOME fmap, env) =
	    let val sk' =
		    if x inset env
			then sk_inter (?env x, sk)
		    else sk
	    in
		if sk' = SOME {}
		    then raise SimpleMatchEvt
		else env ++ {x => sk'}
	    end
	  | se_match_term (pat as f $ _, SOME fmap, env) =
	    if f inset fmap
		then if
		    exists
		      (let val sigma = simple_match_term (pat, t, {})
		       in
			   all
			     ps_compat (v, ?env x)
			   | x => v in map env <| sigma
			   end
		       end handle SimpleMatchEvt => false)
		    | t in set ?fmap f
		    end
			 then env
		     else raise SimpleMatchEvt
	    else raise SimpleMatchEvt

	fun se_match_al ((P, t)::al, psenv) =
	    if P inset !skeleta
		then se_match_al (al,
				  se_match_term (t,
						 ?(!skeleta) P,
						 psenv))
	    else raise SimpleMatchEvt
	  | se_match_al (_, psenv) = psenv;

	fun se_match_Bs ({i => B} U rest, psenv) =
	    if i inset psenv
		then se_match_Bs (rest, psenv ++ {i => sk_inter (?psenv i, q_skeleta B)})
	    else se_match_Bs (rest, psenv ++ {i => q_skeleta B})
	  | se_match_Bs (_, psenv) = psenv

	(* 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 skeleta are compatible with those
	 given in environment psenv. *)

	fun gen_resolvent (t1n, B1n, al, Bs, psenv : simple_env) =
	    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 = se_check_empty (q_skeleta B1)
			      in
				  if x inset !psenvr
				      then psenvr := !psenvr ++
					  {x =>
					    se_check_empty (sk_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)
		    val al'' = atom_merge (al', al)
		in
		    psenvr := se_match_al (al', !psenvr);
		    (al'', !Bsr, !psenvr)
		end
	    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 splitdefq : (block, unit) table = table ()
	    (* memoizes which splitting literals have been defined already. *)
	val sdq_get = t_get splitdefq
	val sdq_put = t_put splitdefq
	val sdq_rem = t_remove splitdefq

	fun new_q (q, pi) =
	    (sdq_rem q;
	     qq := !qq ++ {q => pi})

	fun prove_q_simple q =
	    if q inset !qq
		then SOME (?(!qq) q)
	    else let val witnesses = inter {if P inset !sure_facts
						then ?(!sure_facts) P
					    else {}
					   | P in set q}
		 in
		     if empty witnesses
			 then 
			     some
			       let val pi = ?(!qq) blk
				   val pi' = p_split_split (CL (HQ blk, {}, nil, {}, pi))
			       in
				   new_q (q, pi');
				   pi'
			       end
			     | blk sub map q
				 such that blk<>q
				     andalso blk inset !qq
			     end
		     else let val splitdef = CL (HQ q, {}, nil, {1 => q},
						 P_SPLIT_DEF)
			      val ut = choose witnesses
			      val up = UP (splitdef, {1 => ut},
					   [? (?(!sure_facts) P) ut
					   | P in set q])
			      val pi = P_UNIT up
			  in
			      new_q (q, pi);
			      SOME pi
			  end
		 end

	fun wait_insert_2 (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
			    (case prove_q_simple blk of
				 SOME _ => ()
			       | _ => (case sdq_get blk of
					   SOME _ => ()
					 | _ =>
					   (wait_insert_1 (CL (HQ blk, {}, nil, {1 => blk},
							       P_SPLIT_DEF),
							   if x inset psenv
							       then {1 => ?psenv x}
							   else {});
					    sdq_put (blk, ()))))
			  | x => blk in map splitBs
			  end; (* then process split clause *)
			    let fun process_split_clause (c as CL (h, ql, al, Bs, pi), pse) =
				    case ql <| !qq of
					{} =>
					  (case ql of
					       {} => wait_insert_1 (c, pse)
					     | {q => _, ...} => 
					       (* do as if we had called resolve_P_f directly,
						and insert clause into selqq: *)
					       (compile_eps_back c;
						let val clsr = t_get_table selqq q
						in
						    t_put_behind clsr (c, pse)
						end))
				      | {q => pi'} U ql' =>
					(* resolve directly with known q's: *)
					process_split_clause (CL (h, ql \ {q}, al, Bs,
								  p_q_resolve (c, AC_Q (q, pi'))),
							      pse)
			    in
				process_split_clause (CL (h, rng splitBs, al, splitBs <-| Bs,
							  p_split_use (c, splitBs)),
						      splitBs <-| psenv)
			    end)
		 end

	val wait_insert =
	    case smash of
		SMASH_ONE_NEG_LIT =>
		(fn (c as CL (h, ql, a::al, Bs, pi), psenv) =>
		    wait_insert_2 (CL (h, ql, [a], Bs, pi), psenv)
		  | ce => wait_insert_2 ce)
	      | _ => wait_insert_2

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

	fun record_bot (c as CL (HBOT botname, ...)) =
	    (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})

	fun insert_selfq (_, _, {}, ...) = ()
	  | insert_selfq (h, al, Bss) =
	    (do_verbose (1, fn () =>
			 (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
			       );
			      #flush stderr ()));
	     let fun ins (nil, ...) = ()
		   | ins (al as (a as (P, f $ _))::rest, acc) =
		     let val fmapr = selfq_get_table P
			 val clsr = t_get_table fmapr f
			 val bssr = t_get_mapr clsr (h, al, acc)
		     in
			 bssr := Bss ++ !bssr;
			 ins (rest, a::acc)
		     end
	     in
		 ins (al, nil)
	     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, ql, al, Bs, ...)) =
	    (case h of
		 HVAR P => P inset !univq
	       | HFUN (P, ...) => P inset !univq
	       | HQ q => q inset !qq
	       | HBOT botname => botname inset !botq)

	fun ct_subsumed_simple (CL (h, _, al as (P, f $ l)::rest, Bs, ...)) =
	    (case selfq_get P of
		 SOME fmap =>
		 (case t_get fmap f of
		      SOME cls =>
		      (case t_get cls (h, al, nil) of
			   SOME (ref bss) =>
			   Bs inset bss
			 | _ => false)
		    | _ => false)
	       | _ => false)
	  | ct_subsumed_simple (CL (HFUN (P, f, k, ...), _, nil, Bs, ...)) =
	    (case a_get P of
		 SOME fmap =>
		 (case t_get fmap f of
		      SOME blkls =>
		      ((iter_sub_Bs (fn Bs' =>
					(case t_get blkls (blkl_from_Bs (Bs', k)) of
					     SOME _ => raise CtSubsumedEvt
					   | _ => ())
					) Bs;
			false)
		       handle CtSubsumedEvt => true)
		    | _ => false)
	       | _ => false)
	  | ct_subsumed_simple (c as CL (h, _, nil, Bs, ...)) =
	    ((iter_sub_Bs (fn (Bs' as {i => B, ...}) =>
			      (case selxq_get (choose B) of
				   SOME cls =>
				   (case t_get cls (h, Bs') of
					SOME _ => raise CtSubsumedEvt
				      | _ => ())
				 | _ => ())
			    | _ => ()) Bs;
	      false)
		 handle CtSubsumedEvt => true)

	fun elim_subsumed_by_univ P =
	    a_rem P

	fun resolve_non_auto (h, nil, newal, Bs, pi_l, c, psenv) =
	    wait_insert (CL (h, {}, newal, Bs,
			     p_auto_resolve (c, pi_l)),
			 psenv)
	  | resolve_non_auto (h, (P, t as f $ l) :: rest, newal, Bs, pi_l, c, psenv) =
	    if P inset !univq
		then resolve_non_auto (h, rest, newal, Bs,
				       (AC_UNIV (P, ?(!univq) P), MGU_AUTO_X1_IS t)::pi_l,
				       c, psenv)
	    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 (newal', Bs', psenv') =
					   gen_resolvent (l, blkl, newal, Bs, psenv)
				   in
				       (* Resolve with P (f(x1,...,xn)) <= B1(x1), ..., Bn(xn) *)
				       resolve_non_auto (h, rest, newal', Bs',
							 (AC_POP (P, f, blkl, pi'),
							  MGU_AUTO_Xs_ARE l)::pi_l,
							 c, psenv');
				       false
				   end handle SimpleMatchEvt => false
				   );
				   ()
			   end
			 | _ => () (* cannot resolve: no automaton clause with head P(f(...)) *)
			   )
		    | _ => () (* cannot resolve: no automaton clause with head P (...) *)
		      )

	(* 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_q_resolve (c, AC_Q (q, ?(!qq) q))),
				   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 [_, ...], Bs, pi),
				   psenv)) =
	    (resolve_non_auto (h, al, nil, Bs, nil, c, psenv);
	     (* Now update selfq: *)
	     insert_selfq (h, al, {Bs => (psenv, pi)})
	     )
	  | 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 (_, _ $ l') ::rest', acc'), ref Bss) =>
			       (let val blkl = blkl_from_Bs (Bs, k)
				    val other_al = revappend (acc', rest')
				    val (al'', Bs'', psenv'') =
					gen_resolvent (l', blkl, nil, {}, {})
				    val mgu' = MGU_AUTO_Xs_ARE l'
				in
				    iterate
				      let val c' = CL (h', {}, revappend (acc', al'), Bs', pi')
					  val Bs1 = (Bs' delta Bs'') ++
					      {i => B U B'
					      | i => B in map Bs'' <| Bs'
						  val B' = ?Bs'' i}
				      in
					  resolve_non_auto (h', other_al, al'', Bs1,
							    [(c_raw, mgu')], c', pse)
				      end
				    | Bs' => (psenv', pi') in map Bss
				    val SOME pse =
					SOME (sk_env_inter (psenv', psenv''))
					handle SimpleMatchEvt => NONE
				    end;
				    false
				end handle SimpleMatchEvt => 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 ((h', Bs' as {1 => B}), (psenv', pi')) =>
			    (* with h' of the form P'(x1), q, or bot, and B
			     containing P. *)
			    let val c' = CL (h', {}, nil, Bs', pi')
				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 = se_match_al (al', se_match_Bs (Bs, {}))
			    in
				wait_insert (CL (h'', {}, al', Bs,
						 p_eps_resolve (c', AC_POP_RAW c, t)),
					     pse);
				false
			    end handle SimpleMatchEvt => false
			    );
			    ())
		     | _ => ());
		     (* Finally, update autoinfoq: *)
		     let val blkl = blkl_from_Bs (Bs, k)
		     in
			 do_verbose (2, fn () =>
				     (#put stderr "  Recording automaton clause: ";
				      perrclause c;
				      #put stderr "\n";
				      #flush stderr ())
				     );
			 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_eps_resolve (c, AC_UNIV (P1, ?(!univq) P1),
								 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 = se_match_al (al',
									    se_match_Bs (Bs', {}))
						 in
						     wait_insert (CL (h', {}, al', Bs',
								      p_eps_resolve (c,
										     AC_POP (P1, f,
											     blkl,
											     pi'),
										     t)),
								  pse);
						     false
						 end handle SimpleMatchEvt => false)
					    end)
				    end);
				    ())
			     | _ => () (* no resolvent *)
			       );
			       (* Now update selxq *)
			       let val csr = t_get_table selxq P1
			       in
				   t_put_behind csr ((h, Bs), (psenv, pi))
			       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' as (_, t' as _ $ _)::rest', acc'), ref Bss) =>
				 (let val mgu' = MGU_AUTO_X1_IS t'
				      val acu' = AC_UNIV (P, pi)
				  in
				      iterate
					let val c' = CL (h', {}, revappend (acc', al'), Bs', pi')
					in
						wait_insert (CL (h', {}, revappend (acc', rest'), Bs',
								 p_auto_resolve (c', [(acu', mgu')])),
							     psenv')
					end
				      | Bs' => (psenv', pi') in map Bss
				      end;
				      false
				  end handle SimpleMatchEvt => false)
			       | _ => raise ResolvePF_BadSelF)));
			    (* 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 ((h', Bs' as {x => B}), (psenv', pi')) =>
				 (let val c' = CL (h', {}, nil, Bs', pi')
				      val Bs' = case B \ {P} of
						    {} => {}
						  | B' => {x => B'}
				      val pse = se_match_Bs (Bs', {})
				  in
				      wait_insert (CL (h', {}, nil, Bs',
						       p_auto_resolve (c',
								       [(AC_UNIV (P, pi),
									 MGU_AUTO_X1_IS (V x))])),
						   pse);
				      false
				  end handle SimpleMatchEvt => 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_env as (c as CL (h, {}, nil, Bs, pi), psenv)) =
	    (case Bs of
		 {} => (* clause is just q *)
		   (case h of
			HBOT botname => record_bot c
		      | HQ q => 
			(case selqq_get q of
			     SOME cls =>
			     (t_iter cls
			      (fn (c' as CL (h', ql', al', Bs', pi'), psenv') =>
				  (wait_insert (CL (h', ql' \ {q}, al', Bs',
						    p_q_resolve (c', AC_Q (q, pi))),
						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: *)
			     new_q (q, pi)
			     )
		      | _ => raise ResolvePF_BadHead)
	       | {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_eps_resolve (c, AC_UNIV (P1, ?(!univq) P1),
							       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 = se_match_al (al',
									  se_match_Bs (Bs', {}))
					       in
						   wait_insert (CL (h, {}, al', Bs',
								    p_eps_resolve (c,
										   AC_POP (P1, f, blkl,
											   pi'),
										   t)),
								pse);
						   false
					       end handle SimpleMatchEvt => false)
					  end)
				  end);
				  ())
			   | _ => () (* no resolvent *)
			     );
			     (* Update forward subsumption structures: *)
			     (* Now update selxq *)
			     let val csr = t_get_table selxq P1
			     in
				 t_put_behind csr ((h, Bs), (psenv, pi))
			     end
			    ))
	       | _ => raise ResolvePF_BlackHole
		 )
	  | resolve_P_f _ = raise ResolvePF_BlackHole; (* remaining cases for resolve_P_f:
							should never happen. *)

	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 := {};
		 univq := {}; qq := {}; t_reset selfq; t_reset selxq; t_reset selqq; botq := {};
		 t_reset autoinfoq;
		 t_reset splitdefq;
		 let val (sk, bots) = compute_skeleta (!clause_list, maxpathlen)
		 in
		     skeleta := sk;
		     skel_bots := bots
		 end;
		 sure_facts := {};
			   (*
		 let val (facts, bots) = compute_witnesses (!clause_list)
		 in
		     sure_facts := facts;
		     iterate
		       record_bot (CL (HBOT botname, {}, nil, {},
				       p_unit up))
		     | botname => up in map bots
		     end
		 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;
					  #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 = se_match_al (al, se_match_Bs (Bs, {}))
			   in
			       wait_insert (c, psenv)
			   end handle SimpleMatchEvt => ())
		 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;
	     while true do
		 let val (_, (c_env as (c, _))) = wait_pop ()
		 in
		     if ct_subsumed_simple c
			 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 ()));
			   (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);
