(* 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 p_resolve = P_RESOLVE;
val p_split_def = P_SPLIT_DEF;
val p_split_use = P_SPLIT_USE;

(*
val dummy_pi = P_GIVEN "<recipe>";
fun p_resolve _ = dummy_pi;
fun p_split_def _ = dummy_pi;
fun p_split_use _ = dummy_pi;
 *)

(*$P+*)

fun dterm1_vars (DV x) = {x}
  | dterm1_vars (DAPP (_, l)) =
    union {dterm1_vars t | (_, t) in list l};

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

fun atl_vars atl = union {dterm1_vars t
			 | (_, t) in list atl};
fun al_vars al = union {atl_vars atl
		       | (_, atl) 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_dterm1 (f as |[put, ...]|, vars) =
    let fun pdterm1 (DV x) =
	    if x inset vars
		then put (?vars x)
	    else raise PrintVarNotInEnv x
	  | pdterm1 (DAPP (f, nil)) = put f
	  | pdterm1 (DAPP (f, [(_, t)])) = (put f; put " "; pdterm1 t)
	  | pdterm1 (DAPP (f, l)) =
	    let val delimr = ref "("
	    in
		put f;
		iterate
		  (put (!delimr); delimr := ","; pdterm1 t)
		| (_, t) in list l
		end;
		put ")"
	    end
    in
	pdterm1
    end;

fun print_head (f as |[put, ...]|, xname, vars) =
    let val pdterm1 = print_dterm1 (f, vars)
	val pq = print_q f
	fun phead (HVAR P) = (put P; put " "; pdterm1 (DV 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 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 pt = print_dterm1 (f, vars)
	       val delimr = ref " :- "
	   in
	       print_head (f, xname, vars) h;
	       iterate
		 (put (!delimr); delimr := ", "; pq q)
	       | q in set ql
	       end;
	       iterate
		 iterate
		   (put (!delimr); delimr := ", ";
		    (*put "["; print f (pack maxd); put "] ";*)
		    put P; put " "; pt t)
		 | (P, t) in list atl
		 end
	       | (_, atl) 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 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 dt_sig (DV _, acc) = acc
  | dt_sig (DAPP (f, l), acc) =
    dtl_sig (l, sig_add (f, len l, acc))
and dtl_sig (nil, acc) = acc
  | dtl_sig ((_, t)::l, acc) =
    dtl_sig (l, dt_sig (t, acc));

fun atl_sig (nil, acc) = acc
  | atl_sig ((_, t)::l, acc) =
    atl_sig (l, dt_sig (t, acc));

fun al_sig (nil, acc) = acc
  | al_sig ((_, atl)::al, acc) =
    al_sig (al, atl_sig (atl, 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 atl_preds nil = {}
  | atl_preds ((P, _)::l) =
    {P} U atl_preds l;

fun al_preds nil = {}
  | al_preds ((_, atl)::al) =
    atl_preds atl 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: *)

fun dt_less ((d, t), (d', t')) =
    d<d' orelse
    (d=d' andalso t_less (t, t'))
and t_less (DV _, DAPP _) = true
  | t_less (DV x, DV y) = x<y
  | t_less (DAPP (f, l), DAPP (f', l')) =
    f strless f' orelse
    (f=f' andalso tl_less (l, l'))
  | t_less _ = false
and tl_less (d::l, d'::l') =
    dt_less (d, d') orelse
    (d=d' andalso tl_less (l, l'))
  | tl_less (nil, nil) = false
  | tl_less (nil, _) = true
  | tl_less _ = false;

fun atom_less ((P, t), (P', t')) =
    P strless P'
    orelse (P=P' andalso t_less (t, t'));

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 GrInsert;

val depth_sort = sort (op <);

fun gr_insert (d, atl1, al as (d', atl)::al') = (* with d>=1 *)
    if d<d'
	then (d, atl1)::al
    else if d=d'
	then (d, atom_merge (atl1, atl))::al'
    else (d', atl)::gr_insert (d, atl1, al')
  | gr_insert (d, atl1, nil) = [(d, atl1)]
  | gr_insert _ = raise GrInsert;
    
(* gen_resolvent ([t1, ..., tn], [B1, ..., Bn], al, Bs)
 adds B1(t1), ..., Bn(tn) to part of clause referenced as al, Bs. *)

exception GenResolvent;

fun gen_resolvent (t1n, B1n, al, Bs) =
    let val Bsr = ref Bs
	val atomsr = ref ({} : int -m> atom set)
    in
	iterate
	  (case t of
	       DV x => let val curBs = !Bsr
		       in
			   if x inset curBs
			       then Bsr := curBs ++ {x => ?curBs x U B1}
			   else if empty B1
			       then ()
			   else Bsr := curBs ++ {x => B1}
		       end
	     | _ => let val curatoms = !atomsr
			val newatoms = {(P, t) | P in set B1}
		    in
			if empty newatoms
			    then ()
			else if d inset curatoms
			    then atomsr := curatoms ++ {d => ?curatoms d U newatoms}
			else atomsr := curatoms ++ {d => newatoms}
		    end)
	|| (d, t) in list t1n
	and B1 in list B1n
	end;
	       let val atoml = !atomsr
		   val depthl = depth_sort atoml
		   fun grl_insert (nil, al) = al
		     | grl_insert (d::dl, nil) =
		       (d, atom_sort (?atoml d)) :: grl_insert (dl, nil)
		     | grl_insert (dl1 as (d::dl), al as (d', atl)::al') =
		       if d<d'
			   then (d, atom_sort (?atoml d)) :: grl_insert (dl, al)
		       else if d=d'
			   then (d, atom_merge (atom_sort (?atoml d), atl))
			       :: grl_insert (dl, al')
		       else (d', atl) :: grl_insert (dl1, al')
	       in
		   (grl_insert (depthl, al), !Bsr)
	       end
    end;

(*
fun approximate_gen_resolvent (t1n, B1n, al, Bs) =
    gen_resolvent (t1n, B1n, nil, {});
*)

fun approximate_gen_resolvent arg =
    let val (al', Bs') = gen_resolvent arg
    in
	([da | da as (maxd, _) in list al'
		 such that maxd<=1],
	   Bs')
    end;

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 nil = 0
  | al_len ((maxd, atl)::rest) = maxd * len atl + al_len rest;

(*
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 4 + al_len al + Bs_len Bs
    else 2;

(* forward linear subsumption by automaton clauses: *)

datatype blocks = BS_ONE of proof (* {{}} *)
       | BS_ZERO (* {} *)
       | BS_BRANCH of int * (string * int) * blocks * blocks;
	 (* BS_BRANCH (minlen, (P, k), b1, b2) = {P(xk) /\ C | C in b1} U b2
	  minlen is the least length of all conjunctions starting from here. *)

fun trivial_blkl (0, acc) = acc
  | trivial_blkl (n, acc) = trivial_blkl (n-1, {}::acc);

fun blkls_from_blocks (BS_ONE pi, acc, i, n) = {rev (trivial_blkl (n-i, acc)) => pi}
  | blkls_from_blocks (BS_ZERO, ...) = {}
  | blkls_from_blocks (BS_BRANCH (_, (P, k), b1, b2), acc, i, n) =
    let val acc' = if i=k
		       then (hd acc U {P}) :: tl acc
		   else {P} :: trivial_blkl (k-i-1, acc)
    in
	blkls_from_blocks (b1, acc', k, n)
    end ++ blkls_from_blocks (b2, acc, i, n);
    
val pred_less = op strless;
val pred_sort = sort pred_less;

fun body_from_block_list blkl =
    let val ir = ref 0
    in
	append [let val k = (inc ir; !ir)
		in
		    [(P, k) | P in list pred_sort blk]
		end
	       | blk in list blkl]
    end;

fun blocks_from_body pi =
    let fun b_from_body (nil, _) = BS_ONE pi
	  | b_from_body (P_k :: rest, n) =
	    BS_BRANCH (n, P_k, b_from_body (rest, n-1), BS_ZERO)
    in
	b_from_body
    end;

fun bs_branch (_, _, BS_ZERO, b2) = b2
  | bs_branch c = BS_BRANCH c;

fun blocks_remove_subsumed (b as BS_ONE _, ...) = b
  | blocks_remove_subsumed (BS_ZERO, ...) = BS_ZERO
  | blocks_remove_subsumed (_, nil, ...) = BS_ZERO
  | blocks_remove_subsumed (b as BS_BRANCH (minlen, P_k, b1, b2), body as (P_k' :: rest), n) =
    if P_k = P_k'
	then bs_branch (minlen, P_k, blocks_remove_subsumed (b1, rest, n-1), b2)
    else let val (P, k) = P_k and (P', k') = P_k'
	 in
	     if pred_less (P, P') orelse P=P' andalso k<k'
		 then bs_branch (minlen, P_k, blocks_remove_subsumed (b1, body, n),
				 blocks_remove_subsumed (b2, body, n))
	     else b
	 end;

fun blocks_add_body pi = (* adds a body to a blocks structure, while removing all bodies
			  from it that are subsumed by body.
			  n is length of body. *)
    let val b_from_body = blocks_from_body pi
	fun b_add_body (_, nil, _) = BS_ONE pi
	  | b_add_body (BS_ONE pi', ...) = BS_ONE pi'
	  | b_add_body (BS_ZERO, body, n) = b_from_body (body, n)
	  | b_add_body (b as BS_BRANCH (minlen, P_k, b1, b2), body as (P_k' :: rest), n) =
	    if P_k = P_k'
		then BS_BRANCH (min (minlen, n), P_k, b_add_body (b1, rest, n-1), b2)
	    else let val (P, k) = P_k and (P', k') = P_k'
		 in
		     if pred_less (P, P') orelse P=P' andalso k<k'
			 then bs_branch (min (minlen, n), P_k,
					 blocks_remove_subsumed (b1, body, n),
					 b_add_body (b2, body, n))
		     else BS_BRANCH (min (minlen, n), P_k', b_from_body (rest, n-1), b)
		 end
    in
	b_add_body
    end;

fun b_set (c as CL (_, _, _, _, _, bsubsr)) =
    do_verbose_else (2,
		     fn () =>
			if !bsubsr
			    then ()
			else (#put stderr "  Removing backward subsumed non-automaton clause: ";
			      perrclause c;
			      #put stderr "\n";
			      #flush stderr ();
			      bsubsr := true),
			    fn () => bsubsr := true);

(* The prover: *)

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

exception ResolvePF_Depth0;
exception ResolvePF_EmptyAtomList;
exception ResolvePF_BadSelF;
exception ResolvePF_BadSelX;
exception ResolvePF_BadSelQ;
exception ResolvePF_BlackHole;

exception AlLast;

fun al_last [atl] = atl
  | al_last (_ :: rest) = al_last rest
  | al_last nil = raise AlLast;

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, f, k, vars, t), _, al, ...)) =
    let val a = (P, t)
	val (d, atl) = al_last al
    in
	d=1 (* Note: f (x1, ..., xk) is of depth 1. *)
	andalso exists a=a' | a' in list atl end
    end
  | is_tautology (CL (HQ q, ql, ...)) = q inset ql
  | is_tautology _ = 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');

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_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_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};

exception NoPathSetEvt;

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

	fun ps_add (P, ps) =
	    if P inset !pathsets
		then pathsets := !pathsets ++ {P => ps_union (ps, ?(!pathsets) P)}
	    else pathsets := !pathsets ++ {P => ps}

	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 match_term (DV 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}
	  | match_term (_, PS_ALL, env) = env
	  | match_term (DAPP (f, nil), PS_ENUM fimap, env) =
	    if (f, 0) inset fimap
		then env
	    else raise NoPathSetEvt
	  | match_term (DAPP (f, l), PS_ENUM fimap, env) =
	    match_term_list (f, l, 1, fimap, env)
	and match_term_list (_, nil, _, _, env) = env
	  | match_term_list (f, (_, ti)::l, i, fimap, env) =
	    let val fi = (f, i)
	    in
		if fi inset fimap
		    then let val env' = match_term (ti, ?fimap fi, env)
			 in
			     match_term_list (f, l, i+1, fimap, env')
			 end
		else raise NoPathSetEvt
	    end
	fun match_atom ((P, t), env) =
	    if P inset !pathsets
		then match_term (t, ?(!pathsets) P, env)
	    else raise NoPathSetEvt
	fun match_atl (nil, env) = env
	  | match_atl (a::atl, env) =
	    match_atl (atl, match_atom (a, env))
	fun match_al (nil, env) = env
	  | match_al ((_, atl)::al, env) =
	    match_al (al, match_atl (atl, 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 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 match_blks ({}, env) = env
	  | match_blks ({x => blk} U rest, env) =
	    match_blks (rest, match_blk (x, blk, env))

	fun eval_clause (CL (h, ql, al, Bs, ...)) =
	    if ql subset !qs
		then (let val env = match_blks (Bs, match_al (al, {}))
		      in
			  case h of
			      HQ q => qs := !qs U {q}
			    | HBOT _ => ()
			    | 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 saturate () =
	    let val oldpathsets = !pathsets
	    in
		iterate
		  eval_clause c
		| c in list cl
		end;
		if !pathsets=oldpathsets
		    then ()
		else saturate ()
	    end
    in
	saturate ();
	!pathsets
    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;
*)

exception FunHeadOptEvt;

fun resolver (do_bot : clause -> unit, (split_approx, resolve_approx), maxpathlen) =
    let val gen = case resolve_approx of
		      CLAUSE_NO_APPROX => gen_resolvent
		    | CLAUSE_2_CLAUSE => approximate_gen_resolvent
	val predicate_graph = ref ({} : predicate digraph)
	val clause_list = ref (nil : clause list)
	val funheads = ref ({} : string -m> string set option)
	    (* map P to SOME fs: then P(t) only holds when t=f(...) with f in fs;
	     if P is mapped to NONE, then we do not know. *)
	val pathsets = ref ({} : string -m> pathset)

	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 union {{P_PRED P
								| (P, _) in list atl}
							       | (_, atl) 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);
	     funheads := !funheads ++ {P => NONE};
	     clause_list := c :: !clause_list)
	  | new_clause (c as CL (HFUN (P, f, ...), ...)) =
	    (add_graph (P_PRED P, c);
	     if P inset !funheads
		 then case ?(!funheads) P of
			  SOME fs => funheads := !funheads ++ {P => SOME (fs U {f})}
			| _ => ()
	     else funheads := !funheads ++ {P => SOME {f}};
	     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 head_info (CL (HBOT botname, ...)) = p_info (P_BOT botname)
	  | head_info (CL (HVAR P, ...)) = p_info (P_PRED P)
	  | head_info (CL (HFUN (P, ...), ...)) = p_info (P_PRED P)
	  | head_info (CL (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

	val waitq as |[ insert = wait_insert_basic,
			popmin = wait_pop,
			empty = wait_empty,
			dump_list = get_clauses,
			... ]|
	    = 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 =
	    (do_verbose (1, fn () => (#put stderr "|- ";
				      perrclause c;
				      let val CL (_, _, _, _, pi, ...) = c
				      in
					  #put stderr "   ";
					  case pi of
					      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 "[?]"
				      end;
				      #put stderr "\n";
				      #flush stderr ()));
	     wait_insert_basic ((head_info c, clause_category c), c))

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

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

	fun match_term_shape (PS_ALL, _) = true
	  | match_term_shape (_, DV _) = true
	  | match_term_shape (PS_ENUM fimap, DAPP (f, nil)) =
	    (f, 0) inset fimap
	  | match_term_shape (PS_ENUM fimap, DAPP (f, l)) =
	    let val ir = ref 0
	    in
		all
		  let val fi = (inc ir; (f, !ir))
		  in
		      fi inset fimap
		      andalso match_term_shape (?fimap fi, ti)
		  end
		| (_, ti) in list l
		end
	    end

	fun wait_insert_2 (c as CL (h, _, al, Bs, ...)) =
	    (* check that funheads can be satisfied *)
	    (if exists
		 q_funheads blk = SOME {}
		| _ => blk in map Bs
		end orelse
		 exists
		   exists
		     not (P inset !funheads andalso
			  (case ?(!funheads) P of
			       SOME fs => f inset fs
			     | NONE => true))
		   | (P, DAPP (f, _)) in list atl
		   end
		 | (_, atl) in list al
		 end
		 then do_verbose (3, fn () =>
				  (#put stderr "Removed clause by funheads optimization(2): ";
				   perrclause c;
				   #put stderr "\n";
				   #flush stderr ()))
	     else if exists
		 q_pathsets blk = ps_empty
		     | _ => blk in map Bs
		     end orelse
		     exists
		       exists
			 not (P inset !pathsets andalso
			      match_term_shape (?(!pathsets) P, t))
		       | (P, t) in list atl
		       end
		     | (_, atl) in list al
		     end
		 then do_verbose (3, fn () =>
				  (#put stderr "Removed clause by funheads optimization(4): ";
				   perrclause c;
				   #put stderr "\n";
				   #flush stderr ()))
	     else
		 wait_insert_1 c)

	fun wait_insert c =
	    if is_tautology c
		then ()
	    else let val CL (h, ql, al, Bs, _, bsubsr) = 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_2 c
		     else
			 case split_approx of
			     SPLIT_NO_APPROX =>
			     (* split: first generate splitting clauses *)
			     ((iterate
				 (case q_funheads blk of
				      SOME {} =>
				      (do_verbose (3, fn () =>
						   (#put stderr "Removed clause \
						    \by funheads optimization(1): ";
						    perrclause c;
						    #put stderr "\n";
						    #flush stderr ()));
				       raise FunHeadOptEvt)
				    | _ =>
				      if q_pathsets blk = ps_empty
					  then (do_verbose (3, fn () =>
							    (#put stderr "Removed clause \
							     \by funheads optimization(3): ";
							     perrclause c;
							     #put stderr "\n";
							     #flush stderr ()));
						raise FunHeadOptEvt)
				      else
					  wait_insert_1 (CL (HQ blk, {}, nil, {1 => blk},
							     p_split_def (c, splitBs, x), ref false)))
			       | x => blk in map splitBs
			       end; (* then process split clause *)
				 wait_insert_2 (CL (h, rng splitBs, al, splitBs <-| Bs,
						    p_split_use (c, splitBs), bsubsr))
				 )
				  handle FunHeadOptEvt => ())
			   | SPLIT_APPROX_AND =>
			     ((iterate
				 (case q_funheads blk of
				      SOME {} => (do_verbose (3, fn () =>
							      (#put stderr "Removed clause \
							       \by funheads optimization(1): ";
							       perrclause c;
							       #put stderr "\n";
							       #flush stderr ()));
						  raise FunHeadOptEvt)
				    | _ =>
				      (wait_insert_1 (CL (HQ blk, {{P} | P in set blk}, nil, {},
							  P_GIVEN "*magic*", ref false));
				       iterate
					 wait_insert_1 (CL (HQ {P}, {}, nil, {1 => {P}},
							    p_split_def (c, splitBs, x), ref false))
				       | P in set blk
				       end))
			       | x => blk in map splitBs
			       end; (* then process split clause *)
				 wait_insert_2 (CL (h, rng splitBs, al, splitBs <-| Bs,
						    p_split_use (c, splitBs), bsubsr))
				 )
				  handle FunHeadOptEvt => ())
			   | SPLIT_APPROX_OR =>
			     ((iterate
				 (case q_funheads blk of
				      SOME {} => (do_verbose (3, fn () =>
							      (#put stderr "Removed clause \
							       \by funheads optimization(1): ";
							       perrclause c;
							       #put stderr "\n";
							       #flush stderr ()));
						  raise FunHeadOptEvt)
				    | _ =>
				      (iterate
					 (wait_insert_1 (CL (HQ blk, {{P}}, nil, {},
							     P_GIVEN "*magic*", ref false));
					  wait_insert_1 (CL (HQ {P}, {}, nil, {1 => {P}},
							     p_split_def (c, splitBs, x), ref false)))
				       | P in set blk
				       end))
			       | x => blk in map splitBs
			       end; (* then process split clause *)
				 wait_insert_2 (CL (h, rng splitBs, al, splitBs <-| Bs,
						    p_split_use (c, splitBs), bsubsr))
				 )
				  handle FunHeadOptEvt => ())
			   | SPLIT_IGNORE =>
			     ((iterate
				 (case q_funheads blk of
				      SOME {} => (do_verbose (3, fn () =>
							      (#put stderr "Removed clause \
							       \by funheads optimization(1): ";
							       perrclause c;
							       #put stderr "\n";
							       #flush stderr ()));
						  raise FunHeadOptEvt)
				    | _ => wait_insert_1 (CL (HQ blk, {}, nil, {}, P_GIVEN "*magic*",
							      ref false)))
			       | x => blk in map splitBs
			       end; (* then process split clause *)
				 wait_insert_2 (CL (h, rng splitBs, al, splitBs <-| Bs,
						    p_split_use (c, splitBs), bsubsr))
				 )
				  handle FunHeadOptEvt => ())
		 end

	val fargsq = ref ({} : string -m> int * int set * dterm1);
	(* 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 = ref ({} : string -m> (string -m> clause set ref) ref)
	(* maps P, f to clauses C \/ -P(f(...))
	 where -P(f(...)) is selected. *)
	val selxq = ref ({} : string -m> clause set ref)
	(* maps P to clauses C \/ -P(x), with -P(x) selected. *)
	val selqq = ref ({} : block -m> clause set ref)
	(* 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 = ref ({} : string -m> (string -m> blocks) ref)
	(* 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.
	 Also used by subsumption engine. *)

	fun clause_compile_subsumed (P, f, blkl, pi) =
	    let val body = body_from_block_list blkl
	    in
		if P inset !autoinfoq
		    then let val fmapr = ?(!autoinfoq) P
			 in
			     if f inset !fmapr
				 then let val blocks = blocks_add_body pi (?(!fmapr) f, body, len body)
				      in
					  fmapr := !fmapr ++ {f => blocks}
				      end
			     else fmapr := !fmapr ++ {f => blocks_from_body pi (body, len body)}
			 end
		else autoinfoq := !autoinfoq ++ {P => ref {f => blocks_from_body pi (body, len body)}}
	    end

	fun block_subsumed Bs =
	    let val n = Bs_len Bs
		fun bsubsumed (BS_ONE _, ...) = true
		  | bsubsumed (BS_ZERO, ...) = false
		  | bsubsumed (BS_BRANCH (minlen, (P, k), b1, b2), n) =
		    minlen<=n andalso
		    (k inset Bs andalso P inset ?Bs k andalso bsubsumed (b1, n-1)
		     orelse bsubsumed (b2, n))
	    in
		fn blocks => bsubsumed (blocks, n)
	    end

	fun ct_subsumed (CL (HVAR P, ...)) =
	    (* check whether +P(x1) is already in univq first: *)
	    P inset !univq
	    (* Otherwise, clause can only be subsumed by non-automata clauses [in selfq or selxq or selqq],
	     with head +P(x1) as well.  We don't test this. *)
	  | ct_subsumed (CL (HFUN (P, f, ...), _, _, blkl, ...)) =
	    P inset !univq orelse
	    P inset !autoinfoq andalso
	    let val fmap = !(?(!autoinfoq) P)
	    in
		f inset fmap andalso block_subsumed blkl (?fmap f)
	    end
	  | ct_subsumed (CL (HQ q, ...)) =
	    q inset !qq
	  | ct_subsumed (CL (HBOT botname, ...)) =
	    botname inset !botq

	fun elim_subsumed_by_univ P =
	    (autoinfoq := {P} <-| !autoinfoq)

	(* resolve_P_f c
	 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.
	 *)
	fun resolve_P_f (c as CL (h, {q} U ql, al, Bs, pi, bsubsr)) =
	    (if q inset !qq
		 then wait_insert (CL (h, ql, al, Bs,
				       p_resolve (AC_Q (q, ?(!qq) q), c, MGU_EMPTY),
				       bsubsr))
	     (* 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: *)
		   if q inset !selqq
		       then let val clsr = ?(!selqq) q
			    in
				clsr := !clsr U {c}
			    end
		   else selqq := !selqq ++ {q => ref {c}})
		 )
	  | resolve_P_f (c as CL (h, {}, al as (maxd, (P, t as DAPP (f, l))::atl) :: rest, Bs,
				  pi, bsubsr)) =
	    (if P inset !univq
		 then wait_insert (CL (h, {},
				       if null atl
					   then rest
				       else (maxd, atl)::rest, Bs,
					   p_resolve (AC_UNIV (P, ?(!univq) P), c,
						      MGU_AUTO_X1_IS t),
					   bsubsr))
	     (* Do not add c either to forward subsumption structures or to selfq,
	      because resolvent subsumes premise. *)
	     else (if P inset !autoinfoq
		       then let val fmap = !(?(!autoinfoq) P)
			    in
				if f inset fmap
				    then let val (k, vars, t) = ?(!fargsq) f
					     val blkls = blkls_from_blocks (?fmap f, nil, 0, k)
					 in
					     iterate
					       (* 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') = gen (l, blkl,
									 if null atl
									     then rest
									 else (maxd, atl)::rest, Bs)
					       in
						   wait_insert (CL (h, {}, al', Bs',
								    p_resolve (AC_POP (P, f, blkl,
										       k, vars, t, pi'),
									       c, MGU_AUTO_Xs_ARE l),
								    ref false))
					       end
					     | blkl => pi' in map blkls
					     end
					 end
				else () (* cannot resolve: no automaton clause with head P (f (...)). *)
			    end
		   else () (* cannot resolve: no automaton clause with head P(...) *);
		       (* Now update selfq: *)
		       if P inset !selfq
			   then let val fmapr = ?(!selfq) P
				in
				    if f inset !fmapr
					then let val clsr = ?(!fmapr) f
					     in
						 clsr := !clsr U {c}
					     end
				    else fmapr := !fmapr ++ {f => ref {c}}
				end
		       else selfq := !selfq ++ {P => ref {f => ref {c}}}
			   ))
	  | resolve_P_f (CL (_, _, (_, (_, DV _) :: _) :: _, ...)) =
	    raise ResolvePF_Depth0
	  | resolve_P_f (CL (_, _, (_, nil) :: _, ...)) =
	    raise ResolvePF_EmptyAtomList
	  | resolve_P_f (c as CL (h as HFUN (P, f, k, vars, t), {}, nil, Bs, pi, bsubsr)) =
	    (* automaton clause *)
	    (
	     (* first try to resolve with some C \/ -P(f(...)) with -P(f(...)) selected: *)
	     if P inset !selfq
		 then let val fmap = !(?(!selfq) P)
		      in
			  if f inset fmap
			      then let val clauses = !(?fmap f)
				   in
				       iterate
					 (case c' of
					      CL (h', {},
						  (maxd', (_, DAPP (_, l'))::atl')::rest',
						  Bs', pi', ref subsumed) =>
					      if subsumed
						  then ()
					      else
						  let val ir = ref 0
						      val blkl = [(inc ir;
								   if !ir inset Bs
								       then ?Bs (!ir)
								   else {})
								 |while !ir<k]
						      val (al'', Bs'') =
							  gen (l', blkl,
							       if null atl'
								   then rest'
							       else (maxd', atl') :: rest',
								   Bs')
						  in
						      wait_insert (CL (h', {}, al'', Bs'',
								       p_resolve (AC_POP_RAW c, c',
										  MGU_AUTO_Xs_ARE l'),
								       ref false))
						  end
					    | _ => raise ResolvePF_BadSelF
					      )
				       | c' in set clauses
				       end
				   end
			  else ()
		      end
	     else ();
		 (* then try to resolve with some C \/ -P(x) with -P(x) selected: *)
		 if P inset !selxq
		     then let val clauses = !(?(!selxq) P)
			  in
			      iterate
				(case c' of
				     CL (h', {}, nil, {1 => B}, pi', ref subsumed) =>
				     (* with h' of the form P'(x1), q, or bot, and B
				      containing P. *)
				     if subsumed
					 then ()
				     else
					 let val h'' = case h' of
							   HVAR P' => HFUN (P', f, k, vars, t)
							 | _ => h'
					     val B' = B \ {P}
					 in
					     wait_insert (CL (h'', {},
							      if empty B'
								  then nil
							      else
								  [(1, [(Q, t)
								       | Q in set B'])],
								    Bs,
								    p_resolve (AC_POP_RAW c, c',
									       MGU_OTHER_X1_IS t),
								    ref false))
					 end
				   | _ => raise ResolvePF_BadSelX
				     )
			      | c' in set clauses
			      end
			  end
		 else ();
		     (* 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 (P, f, blkl, pi)
		     end
		 )
	  | resolve_P_f (c as CL (h as HVAR P, {}, nil, Bs, pi, bsubsr)) =
	    (* 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 (DV 1)),
						  bsubsr))
		    (* Do not update forward subsumption structures or selxq
		     since resolvent subsumes premise. *)
		    else (if P1 inset !autoinfoq
			      then
				  iterate
				    iterate
				      wait_insert (CL (h', {},
						       if empty rest
							   then nil
						       else
							   [(1, [(Q, t)
								| Q in set rest])],
							     Bs',
							     p_resolve (AC_POP (P1, f, blkl,
										k, vars, t, pi'),
									c, MGU_OTHER_X1_IS t),
							     ref false))
				    | blkl => pi' in map blkls
				    val jr = ref 0
				    val Bs' = {!jr => blk
					      | blk in list blkl
						  such that (inc jr; not (empty blk))}
				    end
				  | f => blocks in map !(?(!autoinfoq) P1)
				  val (k, vars, t) = ?(!fargsq) f
				  val blkls = blkls_from_blocks (blocks, nil, 0, k)
				  val h' = HFUN (P, f, k, vars, t)
				  end
			  else (); (* no resolvent *)
			      (* Now update selxq *)
			      if P1 inset !selxq
				  then let val csr = ?(!selxq) P1
				       in
					   csr := !csr U {c}
				       end
			      else selxq := !selxq ++ {P1 => ref {c}}
				  ))
	       | _ => (* clause is just P(x): resolve with all clauses C \/ -P(...) *)
		 ( (* first try to resolve with some C \/ -P (f (...)) with -P(f(...)) selected *)
		  if P inset !selfq
		      then
			  iterate
			    iterate
			      (case c' of
				   CL (h', {},
				       (maxd', (_, t' as DAPP (_, l'))::atl')::rest',
				       Bs', pi', bsubsr') =>
				   if !bsubsr'
				       then () (* already subsumed *)
				   else (b_set c';
					 wait_insert (CL (h', {},
							  if null atl'
							      then rest'
							  else (maxd', atl')::rest', Bs',
							      p_resolve (AC_UNIV (P, pi), c',
									 MGU_AUTO_X1_IS t'),
							      ref false)))
				 | _ => raise ResolvePF_BadSelF)
			    | c' in set clauses
			    end
			  | f => ref clauses in map !(?(!selfq) P)
			  end
		  else ();
		      (* then resolve with clauses C \/ -P(x) with -P(x) selected *)
		      if P inset !selxq
			  then 
			      iterate
				(case c' of
				     CL (h', {}, nil, {x => B}, pi', bsubsr') =>
				     if !bsubsr'
					 then ()
				     else (b_set c';
					   wait_insert (CL (h', {}, nil,
							    case B \ {P} of
								{} => {}
							      | B' => {x => B'},
								p_resolve (AC_UNIV (P, pi), c',
									   MGU_AUTO_X1_IS (DV x)),
								ref false)))
				   | _ => raise ResolvePF_BadSelX)
			      | c' in set !(?(!selxq) P)
			      end
		      else ();
			  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, bsubsr)) =
	    (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 as CL (h as HQ q, {}, nil, Bs, pi, bsubsr)) =
	    (case Bs of
		 {} =>
		   (if q inset !selqq
			then
			    iterate
			      (case c' of
				   CL (h', ql', al', Bs', pi', bsubsr') =>
				   if !bsubsr'
				       then ()
				   else (b_set c';
					 wait_insert (CL (h', ql' \ {q}, al', Bs',
							  p_resolve (AC_Q (q, pi), c', MGU_EMPTY),
							  ref false)))
				 | _ => raise ResolvePF_BadSelQ)
			    | c' in set !(?(!selqq) q)
			    end
		    else ();
			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 (DV 1)),
						bsubsr))
			  (* Do not update forward subsumption structures or selxq
			   because resolvent is subsumed by premise. *)
		  else (if P1 inset !autoinfoq
			    then
				iterate
				  iterate
				    wait_insert (CL (h, {},
						     if empty rest
							 then nil
						     else
							 [(1, [(Q, t)
							      | Q in set rest])],
							   Bs',
							   p_resolve (AC_POP (P1, f, blkl,
									      k, vars, t, pi'),
								      c, MGU_OTHER_X1_IS t),
							   ref false))
				  | blkl => pi' in map blkls
				  val jr = ref 0
				  val Bs' = {!jr => blk
					    | blk in list blkl
						such that (inc jr; not (empty blk))}
				  end
				| f => blocks in map !(?(!autoinfoq) P1)
				val (k, vars, t) = ?(!fargsq) f
				val blkls = blkls_from_blocks (blocks, nil, 0, k)
				end
			else (); (* no resolvent *)
			    (* Update forward subsumption structures: *)
			    (* Now update selxq *)
			    if P1 inset !selxq
				then let val csr = ?(!selxq) P1
				     in
					 csr := !csr U {c}
				     end
			    else selxq := !selxq ++ {P1 => ref {c}}
				))
	       | _ => raise ResolvePF_BlackHole
		 )
	  | resolve_P_f _ = raise ResolvePF_BlackHole; (* remaining cases for resolve_P_f:
							should never happen. *)

	    (*
	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 := {}; selfq := {}; selxq := {}; selqq := {}; botq := {};
		 autoinfoq := {};
		 pathsets := compute_pathsets (!clause_list, maxpathlen);
		 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 "Funheads:\n";
					  iterate
					    (#put stderr P;
					     #put stderr ":";
					     (case fso of
						  SOME fs =>
						  (iterate
						     (#put stderr " ";
						      #put stderr f)
						   | f in set fs
						   end;
						     #put stderr "\n")
						| _ => #put stderr " *all*.\n"))
					  | P in list pred_sort (!funheads)
					    val fso = ?(!funheads) P
					  end;
					  #put stderr "Pathsets:\n";
					  iterate
					    (#put stderr P;
					     #put stderr ": ";
					     pretty stderr (pack (?(!pathsets) P)))
					  | P in list pred_sort (!pathsets)
					    val ps = ?(!pathsets) 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, DAPP (f, [(1, DV (inc ir; !ir))
						       |while !ir<k])))
			   | f => k in map fsig}
	     end;
	     iterate
		 if useful c
		     then wait_insert c
		 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 (((_, low), _), c as CL (_, _, _, _, _, ref bsubs)) = wait_pop ()
		 in
			       (*
		     if low > !current_low
			 then (do_verbose (1, fn () =>
					   (if !current_low<>0
						then (#put stderr "  Clean sweep: removing all non-automata\
						 \ clauses on ";
						      print stderr (pack (?(!scc_info) (!current_low)));
						      #put stderr "\n";
						      #flush stderr ())
					    else ()));
			       selfq := {}; selxq := {}; selqq := {};
			       (* in fact, do not erase qq. *)
			       current_low := low)
		     else ();
			 *)
		     if bsubs orelse ct_subsumed c
			 then do_verbose (2, fn () => (#put stderr "  Removing forward subsumed clause: [";
						       print stderr (pack low);
						       #put stderr "] ";
						       perrclause c;
						       #put stderr "\n";
						       #flush stderr ()))
		     else (do_verbose (2, fn () => (#put stderr "  Picking clause: [";
						    print stderr (pack low);
						    #put stderr "] ";
						    perrclause c;
						    #put stderr "\n";
						    #flush stderr ()));
			   resolve_P_f c)
		 end)
		 handle MHeapEmptyEvt => ();
    in
	|[ new_clause = new_clause,
	   resolve = resolve,
	   get_automaton = (fn () => ({P => {f => (blkls_from_blocks (blocks, nil, 0, k), k, vars)
					    | f => blocks in map fmap
					      val (k, vars, ...) = ?(!fargsq) f}
				      | P => ref fmap in map !autoinfoq},
					!univq)),
	   get_clauses = (fn () => !clause_list @ get_clauses ()),
	   get_true_botnames = (fn () => !botq)
	   ]|
    end;

fun clause_from_automaton_clause (AC_UNIV (P, pi)) =
    CL (HVAR P, {}, nil, {}, pi, ref false)
  | clause_from_automaton_clause (AC_Q (q, pi)) =
    CL (HQ q, {}, nil, {}, pi, ref false)
  | clause_from_automaton_clause (AC_POP (P, f, bl, k, vars, t, pi)) =
    let val ir = ref 0
	val Bs = {(inc ir; !ir) => B
		 | B in list bl}
    in
	CL (HFUN (P, f, k, vars, t), {}, nil, Bs, pi, ref false)
    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);
