(* Model-checking functions.
   Copyright (C) 2003,2008 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

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

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

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

exception Bug of string;

open "model_h";
open "verbose_h";
open "sort_h";
open "rel_h";
open "cc_h";

exception McActualHistory;

(*
exception McInductBug;

fun mc_induct (x,epsc,P,side,jl) =
    if exists true
       | (_, _, MC_SUBSUMED_HISTORY _) in list jl
       end
       then raise McInductBug
    else MC_INDUCT (x,epsc,P,side,jl);
*)

(* Let A be an alternating tree automaton (with universal clauses).
 There are many ways we can check whether A |= C, where C is a clause.
 (By A |= C we mean that C holds in the least model of A.)

 First method.
 =============

 Just tabulate the least model.  Define values as sets of predicates.
 Let I_f (v1, ..., vn) =
 {P | exists P(x) in A or P(f(x1,...,xn)) <= B1(x1), ..., Bn(xn) in A
 such that B1 subseteq v1, and ..., and Bn subseteq vn.}
 Let I_P (v) be true if and only if P in v.
 Tabulate all this, and evaluate clause C in this model.

 Problem: generates exponential-sized model.
 This is actually a subset construction, and in fact builds a complete
 deterministic automaton from A (aka. a first-order model!).
 Could be solved by minimizing the automaton, at least partially
 (eliminating empty states, states simulated by others, etc.)

 Second method.
 ==============

 Generate complement A' of A, as an automaton again.
 Then A |/= C, with C = (h <= B1, ..., Bn) if and only if there are
 values of free variables in clause C such that B1, ..., Bn hold but
 not h.  This can be done by replacing the head predicate symbol of h
 by its complement state in A', building h', then testing whether
 A + the clause bot <= h', B1, ..., Bn is unsatisfiable.
 Unsatisfiability means that A |/= C, i.e.,
 satisfiability means A |= C.

 Problem: requires building the complement of A, may be exponential.
 Of course this is a subset construction, as in the first method.

 Third method. (the one chosen here.)
 =============

 A |= C if and only if
 - either C is a tautology
 - or C is subsumed by a clause of A
 - or C is of the form C1 \/ -P(t) [with P(t) selected],
   and:
   . for every universal clause P(x) in A, A |= C1
   . if t=f(t1,...,tn), then for every automaton clause
     P(f(x1,...,xn)) <= B1(x1), ..., Bn(xn) in A,
     A |= C1 \/ -B1(t1) \/ ... \/ -Bn(tn)
   . if t=x, then for every automaton clause
     P(f(x1,...,xn)) <= B1(x1), ..., Bn(xn) in A,
     A |= C1 sigma \/ -B1(x1) \/ ... \/ -Bn(xn),
     where sigma = {x:=f(x1,...,xn)}.
 - or C is of the form C1 \/ +P(t), t = f(t1, ..., tk),
   and A |= C1 \/ \/_{P(x) in A} true
         \/ \/_{P(f(x1,...,xk)) <= B1(x1), ..., Bk(xk) in A} (B1(t1) /\ ... /\ Bk(tk))
 - or C is a disjunction of literals +-Pi(xi) [only variables],
   of the form C1(x1) \/ ... \/ Ck(xk) [with k>=2: splittable]
   and A |= C1(x1) or ... or A |= Ck(xk)
 - or C is a disjunction of literals +-Pi(x) [only one variable],
   and [term induction] for every function symbol f, A |= C[x:=f(x1,...,xk)].
   This part requires a history mechanism to detect looping.
   Loop detection entails a true answer.
   The loop detection mechanism can be restricted to only check such clauses,
   disjunctions of +-Pi(x) with the same x.

 This is also exponential.  After all, testing whether A |= (P(x)<=Q(x))
 is equivalent to testing whether the language of Q is included in that of P,
 and this is DEXPTIME-complete.  (Testing A |= C is therefore DEXPTIME-hard,
 hence DEXPTIME-complete; membership in DEXPTIME is by the first or second method.)

 However there is hope that the worst-case running time is not reached,
 and this is easier to translate to Coq.
 Also, we use a *lot* of optimizations.
 *)

(*datatype Var = VAR of string;*)

(*
infix 0 otherwise;

fun (action : 'a option) otherwise (rest : 'a option promise)
    : 'a option =
    (case action of
	 (res as SOME _) => res
       | _ => force rest);

fun do_in_priority (l : 'a option promise list) : 'a option =
    (case l of
	 nil => NONE
       | action::rest =>
	 (case force action of
	      (res as SOME _) => res
	    | _ => do_in_priority rest));
*)

fun mc_subsumed_epsc (c as GCLAUSE (_, [_]),t,MC_TAUTO (_, i)) =
    MC_TAUTO (c, i)
  | mc_subsumed_epsc (c,t,j) =
    MC_SUBSUMED_EPSC (c,t,j);

(* OBSOLETE
exception VCJustifIP;

fun vcjustif_ip VC_NO = raise VCJustifIP
  | vcjustif_ip (VC_IND_HYP ip) = ip
  | vcjustif_ip (VC_CUT_HISTORY (_, vcj)) = vcjustif_ip vcj
  | vcjustif_ip (VC_UNIV ip) = ip
  | vcjustif_ip (VC_INDUCT (ip, _)) = ip;
*)

exception FilterJustifSubsumedUniv;
exception JustifGclause;

fun justif_gclause (MC_TAUTO (c, _)) = c
  | justif_gclause (MC_CUT_HISTORY (_, j)) =
    justif_gclause j
  | justif_gclause (MC_NORMALIZE (c, ...)) = c
  | justif_gclause (MC_SUBSUMED_UNIV (c, ...)) = c
(*
  | justif_gclause (MC_SUBSUMED_AUTO (c, ...)) = c
*)
  | justif_gclause (MC_SUBSUMED_HISTORY (c, ...)) = c
  | justif_gclause (MC_SUBSUMED_EPSC (c, ...)) = c
  | justif_gclause (MC_ELIM_UNIV_NEG (c, ...)) = c
  | justif_gclause (MC_ELIM_NEG (c, ...)) = c
  | justif_gclause (MC_ELIM_EPSILON_NEG (c, ...)) = c
  | justif_gclause (MC_DEDUCE_POS (c, ...)) = c
  | justif_gclause (MC_DISTR_POS (c, ...)) = raise JustifGclause
  | justif_gclause (MC_SUBSUMED_SUPER (c, ...)) = raise JustifGclause
  | justif_gclause (MC_SUBSUMED (c, ...)) = c
  | justif_gclause (MC_SPLIT (c, ...)) = c
  | justif_gclause (MC_EXPLICIT_UNIV (x, qs, info)) =
    GCLAUSE (nil, [P $ [V x] | P in set qs])
  | justif_gclause (MC_VS (x, q, q', sm)) =
    GCLAUSE ([q $ [V x], q' $ [V x]], nil)
(* OBSOLETE
  | justif_gclause (MC_VS_NEG1 (c, ...)) = c
*)
  | justif_gclause (MC_CUT (c, ...)) = c
  | justif_gclause (MC_INDUCT (x, (negP, posP), ...)) = 
	    GCLAUSE ([P $ [V x]
		     | P in set negP],
		       [P $ [V x]
		       | P in set posP])
	    ;

fun filter_justif (MC_SPLIT (_, j')) = filter_justif j'
  | filter_justif (MC_TAUTO (GCLAUSE (neg, pos), i)) =
    let val a = pos nth i
    in
	MC_TAUTO (GCLAUSE ([a], [a]), 0)
    end
  | filter_justif (MC_CUT_HISTORY (h, j)) =
    MC_CUT_HISTORY (h, filter_justif j)
  | filter_justif (MC_NORMALIZE (GCLAUSE (neg, pos), sigma, j)) =
    let val j' = filter_justif j
	val GCLAUSE (neg', pos') = justif_gclause j'
	fun norm_subst (V x) =
	    if x inset sigma
		then V (?sigma x)
	    else V x
	  | norm_subst (f $ l) =
	    f $ [norm_subst t | t in list l]
	val negs = elems neg' (* {norm_subst a | a in list neg'} *)
	val poss = elems pos' (* {norm_subst a | a in list pos'} *)
	val c' = GCLAUSE ([a | a in list neg
				 such that norm_subst a inset negs],
			    [a | a in list pos
				   such that norm_subst a inset poss])
    in
	MC_NORMALIZE (c', sigma, j')
    end
  | filter_justif (MC_SUBSUMED_UNIV (GCLAUSE (_, pos), P, _)) =
    (case some a
	  | a as Q $ _ in list pos
	      such that Q=P
	  end of
	 SOME a => MC_SUBSUMED_UNIV (GCLAUSE (nil, [a]), P, 0)
       | NONE => raise FilterJustifSubsumedUniv)
(* Obsolete:
  | filter_justif (MC_SUBSUMED_AUTO (GCLAUSE (neg, pos),
				     P, f, k, sigma, blkl, i)) =
 ...
*)
  | filter_justif (MC_SUBSUMED_HISTORY (GCLAUSE (neg, pos),
					epsc as (negs, poss), t)) =
    let val neg' = [a
		   | a as P $ [u] in list neg
		     such that u=t andalso P inset negs]
	val pos' = [a
		   | a as Q $ [v] in list pos
		     such that v=t andalso Q inset poss]
    in
	MC_SUBSUMED_HISTORY (GCLAUSE (neg', pos'), epsc, t)
    end
  | filter_justif (MC_SUBSUMED_EPSC (GCLAUSE (neg, pos), t, j)) =
    let val j' = filter_justif j
	val GCLAUSE (negeps, poseps) = justif_gclause j'
	val negs = {P | P $ _ in list negeps}
	val poss = {Q | Q $ _ in list poseps}
	val neg' = [a
		   | a as P $ [u] in list neg
		     such that u=t andalso P inset negs]
	val pos' = [a
		   | a as Q $ [v] in list pos
		     such that v=t andalso Q inset poss]
    in
	MC_SUBSUMED_EPSC (GCLAUSE (neg', pos'), t, j')
    end
  | filter_justif (MC_SUBSUMED (c, j)) =
    filter_justif j
  | filter_justif j = j;

fun is_tauto (MC_TAUTO _) = true
  | is_tauto (MC_CUT_HISTORY (_, j)) = is_tauto j
  | is_tauto _ = false;

fun filter_distr_justif jl =
    let val andorlr = ref ({} (* : (term set * term set) -m> mc_distr_justif *))
	fun condense_gclause (GCLAUSE (neg, pos)) =
	    (elems neg, elems pos)
	fun cond_subsumed ((negs, poss), (negs', poss')) =
	    negs' subset negs andalso poss' subset poss
	fun add_justif j =
	    let val c = justif_gclause j
		val cc = condense_gclause c
	    in
		if exists cond_subsumed (cc, cc') | cc' in set !andorlr end
		    then ()
		else (andorlr := {cc' => j
				 | cc' => j in map !andorlr
				   such that not (cond_subsumed (cc', cc))}
		      ++ {cc => j})
	    end
    in
	iterate
	  if is_tauto j' (* eliminate tautologies *)
	      then ()
	  else add_justif j'
	| j in list jl
	val j' = filter_justif j
	end;
	[j | _ => j in map !andorlr]
    end;
(*
    [j'
    | j in list jl
	val j' = filter_justif j
	such that not (is_tauto j') 
	  ];
*)

exception FindUniv;
exception FindAutoSubsumer;
exception ResolveAutoNeg;
exception ResolveAutoPos;
exception GSplit1;
exception CheckEpsClause;
exception EpscSubsumesNoInst;
exception EpscSubsumes;
exception CutHistory;
exception PosCheckValue;
exception GetNegValues;

exception ModelCheckFailEvt;
exception EvalUndefinedEvt;
exception VcEvt;

(* @@@ Note: in the MC_DISTR_POS case, it would be fine
 if the algorithm kept a trace of how to prove that
 the conjunction of disjunctions implies the disjunction
 of conjunctions; Tauto works in simple cases, but would
 be lost as soon as the formula gets a bit bigger.
*)

fun p_eps_clause (f as |[put, ...]|) =
    let fun p_atom P = (put P; put "(X)")
	fun p_negs {} = put "."
	  | p_negs {Q} = (p_atom Q; put ".")
	  | p_negs ({Q} U rest) = (p_atom Q;
				   put ", ";
				   p_negs rest)
	fun p_epsc_neg {} = put "."
	  | p_epsc_neg neg = (put " :- "; p_negs neg)
	fun p_epsc (neg, {}) =
	    (put "#false"; p_epsc_neg neg)
	  | p_epsc (neg, {P}) =
	    (p_atom P; p_epsc_neg neg)
	  | p_epsc (neg, {P} U rest) =
	    (p_atom P; put " \\/ "; p_epsc (neg, rest))
    in
	p_epsc
    end;

val perr_eps_clause = p_eps_clause stderr;

fun perr_spaces 0 = ()
  | perr_spaces n = (#put stderr " "; perr_spaces (n-1));

fun perr_bars 0 = ()
  | perr_bars n = (#put stderr "| "; perr_bars (n-1));

fun perr_funs () =
    let val cntr = ref 0
	val f as |[tell, seek, truncate, convert, ...]| = outstring "X"
	val n = tell ()
	memofun varname x =
		(inc cntr;
		 seek n; truncate ();
		 print f (pack (!cntr));
		 convert ())
	val perr_term = print_term (stderr, varname)
    in
	|[perr_gclause = print_gclause_pl (stderr, varname),
	  perr_term = perr_term,
	  perr_varname = varname,
	  perr_sigma = fn (_, _, {}) => ()
			| (popen, pclose, sigma) =>
			  let val delimr = ref popen
			  in
			      iterate
				(#put stderr (!delimr); delimr := ",";
				 #put stderr (varname x);
				 #put stderr "=";
				 perr_term t)
			      | x => t in map sigma
			      end;
			      #put stderr pclose
			  end
	  ]|
    end

(*
fun perr_subst ({}, o, c) = ()
  | perr_subst (sigma, o, c) =
    let val delimr = ref o
    in
	iterate
	  (perr_term 
	| x => t in map sigma
	end;
    end;
*)

(* Loop-checking requires to check whether we have already seen
 a given epsilon clause, or a smaller one.
 Checking this "same or smaller" relation
 is the purpose of the hsub (history subsumer) datatype below.
 *)

datatype 'a epssub = ESEmpty
       | ESLeaf
       | ESTest of (string*bool) * bool
	 * 'a epssub * 'a epssub; (* (P,sign), clauses that contain P,
			       clauses that do not; sign is true
			       iff on the left of clause. *)
(*
 [[ ESTest (signedP, false, present, absent) ]] =
   {l U {signedP} | l in [[present]]} U [[absent]].
 [[ ESTest (signedP, true, present, absent) ]] =
   {l U {signedP} | l in [[present]]} U [[absent]] U {empty clause}.
 [[ ESLeaf ]] =
   {empty clause}.
 [[ESEmpty]] = {}
 (ignoring 'a fields).
*)

fun eps_subsumers (epsc as (negs, poss) : epsilon_gclause) =
    let fun epssub (_, _, ESEmpty) = {}
	  | epssub (negs', poss', ESLeaf) = {(negs', poss')}
	  | epssub (negs', poss', ESTest (Psign,true,present,absent)) =
	    {(negs', poss')} U epssub (negs', poss',
				       ESTest (Psign,false,present,absent))
	  | epssub (negs', poss', ESTest ((P,sign),false,present,absent)) =
	    epssub (negs', poss', absent) U
	    (if sign
		 then if P inset negs
			  then epssub (negs' U {P}, poss', present)
		      else {}
	     else if P inset poss
		 then epssub (negs', poss' U {P}, present)
	     else {})
    in
	fn es => epssub ({}, {}, es)
    end;

(*
fun epssub_find (epsc as (negs,poss): epsilon_gclause) =
    let fun esfin ESEmpty = NONE
	  | esfin (ESLeaf a) = SOME a
	  | esfin (ESTest ((P,sign),present,absent)) =
	    case esfin absent of
		(res as SOME _) => res
	      | NONE =>
		if (if sign then P inset negs else P inset poss)
		    then esfin present
		else NONE
    in
	esfin
    end;
*)

fun signed_less ((P,signp),(Q,signq)) =
    P strless Q orelse (P=Q andalso not signp andalso signq);

val signed_sort = sort signed_less;

fun epssub_add (epsc as (negs,poss) : epsilon_gclause) =
    let fun esadd (nil, ESTest (Psign,_,present,absent)) =
	    ESTest (Psign,true,present,absent)
	  | esadd (nil, _) = ESLeaf
	  | esadd (signedP::l, ESEmpty) =
	    ESTest (signedP, false, esadd (l, ESEmpty), ESEmpty)
	  | esadd (signedP::l, ESLeaf) =
	    ESTest (signedP, true, esadd (l, ESEmpty), ESEmpty)
	  | esadd (l as (signedP::rest),
		   es as ESTest (signedQ, here, present, absent)) =
	    if signed_less (signedP, signedQ)
		then ESTest (signedP, false, esadd (rest, es), es)
	    else if signedP=signedQ
		then ESTest (signedP, here, esadd (rest,present), absent)
	    else ESTest (signedQ, here, present, esadd (l,absent))
	val signedl = signed_sort ({(P,true) | P in set negs} U
				     {(Q,false) | Q in set poss})
    in
	fn es => esadd (signedl, es)
    end;

fun term_less (P $ tl, Q $ tl') =
    P strless Q
    orelse (P=Q andalso tl_less (tl, tl'))
  | term_less (V x, V y) =
    system_less (x, y) (* incomparable, so use random-looking ordering *)
  | term_less (V _, _ $ _) = true
  | term_less _ = false
and tl_less (nil, nil) = false
  | tl_less (nil, _) = true
  | tl_less (t::tl, t' :: tl') =
    term_less (t, t') orelse
    (t=t' andalso tl_less (tl, tl'))

val term_sort = sort term_less;

fun list_vars (nil, acc, done) : ''var list * ''var set
    = (acc, done)
  | list_vars (t::tl, acc, done) =
    let val (varl, vars) = tl_vars (t, acc, done)
    in
	list_vars (tl, varl, vars)
    end
and tl_vars (V x, acc, done) =
    if x inset done
	then (acc, done)
    else (x::acc, done U {x})
  | tl_vars (_ $ l, acc, done) = list_vars (l, acc, done);

(* Take orandl, a disjunction of conjunctions,
 and return an equivalent conjunction of disjunctions,
 as set of sets. *)
fun distr_and_or nil = (* true *) {{}}
  | distr_and_or (andl::rest) =
    let val andorl1 = distr_and_or rest
	val andorlr = ref {}
	fun addao orl =
	    let val ao = !andorlr
	    in
		if orl inset ao
		    then ()
		else if exists orl' subset orl | orl' in set ao end
		    then () (* forward subsumed *)
		else (iterate
			andorlr := !andorlr \ {orl'}
			(* backward subsumed *)
		      | orl' in set ao
			such that orl subset orl'
		      end;
			andorlr := !andorlr U {orl})
	    end
    in
	iterate
	  iterate
	    addao (orl U {a})
	  | orl in set andorl1
	  end
	| a in list andl
	end;
	!andorlr
    end;

(* Functions to help model-checking finite models as found by Paradox. *)
(* First, recognize set of actual states _q<i>.
 These are the predicates that occur at least once in the body
 of automaton clauses; and also universal predicates. *)

fun auto_states (AUTO (auto, univ)) =
    univ U union {union {union {union {blk
				      | blk in list blkl}
			       | blkl in set blkls}
			| f => (blkls, ...) in map fmap}
		 | P => fmap in map auto};

(* Now, recognize epsilon-transitions.  Ie,
 given set of states q<i> in automaton, try
 to find non-state predicates (i.e., occurring only
 on heads of clauses in auto) P whose definition
 could be stated as a finite set of epsilon-clauses
 P(X) :- q<i>(X), where i varies among some set.
 I.e., P(X) <=> \/_{i \in I} q<i>(X).
 This is equivalent to:
 P(f(X1,...,Xn)) <=> \/_{i \in I} q<i>(f(X1,...,Xn)) for every f.
 It is enough to check that the set of bodies B
 such that there is a clause P(f(X1,...,Xn)) :- B
 is exactly the same as the set of bodies B
 such that there is an i and a clause q<i>(f(X1,...,Xn)) :- B.
 *)
fun recover_epsilon_trans (AUTO (auto, univ), states, P) =
    (* where P is not in states, in particular not in univ. *)
    if P inset auto
	then let val fmap = ?auto P
		 (* For each f and each automaton clause P(f(X1,...,Xn)) :- B,
		  find those states q with an automaton clause
		  q(f(X1,...,Xn)) :- B: *)
		 val qs = union {union {{q
					| q in set auto <| states
					    val qfmap = ?auto q
						such that f inset qfmap
						    andalso blkl inset #1 (?qfmap f)}
				       | blkl in set blkls}
				| f => (blkls, ...) in map fmap}
	     in
		 (* Then check the converse: for every f,
		  for every q in qs, for every clause
		  q(f(X1,...,Xn)) :- B
		  there should be a clause P(f(X1,...,Xn)) :- B.
		  *)
		 if all
		     all
		       if f inset fmap
			   then blkls subset #1 (?fmap f)
		       else empty blkls
		     | f => (blkls, ...) in map qfmap
		     end
		    | q in set qs
		      val qfmap = ?auto q
		    end
		     then SOME qs
		 else NONE
	     end
    else SOME {} (* P is false: take the empty set of states. *)
	;

local
    val nfa = re_make_nfa [(re_parse "^#", fn _ => ())]
in
    fun percent_matches P =
	case nfa_run (nfa, P) of
	    SOME _ => true
	  | _ => false
end;

fun auto_epsilon_trans (a as AUTO (auto, _), states) =
    let val preds = {P
		    | P => fmap in map states <-| auto
		      such that case fmap of
				    {f => _} => not (percent_matches f)
				  | _ => true}
    in
	{P => qs
	| P in set preds
	    val SOME qs = recover_epsilon_trans (a, states, P)}
    end;

exception CheckExplicitUnivEvt;

fun enum_block_lists (do_block, k, qs) =
    let fun ebl1 (0, blkl) = {blkl => do_block blkl}
	  | ebl1 (k, blkl) =
	    let val k' = k-1
	    in
		overwrite [ebl1 (k', {q}::blkl)
			  | q in set qs]
	    end
    in
	ebl1 (k, nil)
    end;

fun block_subsumes (nil, nil) = true
  | block_subsumes (l' :: rest', l :: rest) =
    l' subset l andalso block_subsumes (rest', rest)
  | block_subsumes _ = false;

fun check_explicit_univ (AUTO (auto, _), fsig, qs) =
    (* Given automaton auto, signature fsig, and
     qs = {q1, ..., qn}
     check that forall X . q1(X) \/ ... \/ qn (X).
     We just check that for every f in fsig, of arity k,
     for every indices i1, ..., ik between 1 and n,
     there is a clause in auto that subsumes
     qj(f(X1,...,Xk)) :- qi1(X1), ..., qik(Xk)
     for some j.
     *)
    SOME {f => enum_block_lists (fn blkl =>
				    (case some q
					  | q => fmap in map qs <| auto
					      such that f inset fmap andalso
						  let val (blkls, ...)
							  = ?fmap f
						  in
						      blkl inset blkls orelse
						      exists
							block_subsumes
							(blkl', blkl)
						      | blkl' in set blkls
						      end
						  end
					  end of
					 SOME q => q
				       | NONE => raise CheckExplicitUnivEvt),
				    k, qs)
	 | f => k in map fsig}
    handle CheckExplicitUnivEvt => NONE;

exception JOfIj;
exception JOfIjBug;
exception DjPreds;
exception JOfDj;
exception JOfDjBug;

datatype simple_inclusion_justif = SIJ_NO
       | SIJ_CUT_HISTORY of (string * string) set * simple_inclusion_justif
       | SIJ_UNIV of string (* justified by universal clause Q(X). *)
       | SIJ_TAUTO of string (* tautology Q(X) :- Q(X). *)
       | SIJ_IND_HYP of string * string (* use induction hypothesis P subseteq Q,
					 i.e., Q(X) :- P(X). *)
	 (* analogous to MC_SUBSUMED_HISTORY *)
       | SIJ_INDUCT of (string * string) *
	 (string -m> int * (block list -m> block list * block_incl_justif list))
(* prove P subseteq Q (Q(X) :- P(X)) by induction.
 Map associates each f to pair (k, Pblkl) where
 k is arity of f, and
 Pblkl=[Pblk1,...,Pblkk] in ?auto P
 (i.e., each automaton clause P(f(X1...Xk)) :- Pblk1(X1),...,Pblkk(Xk)) to
 Qblkl (i.e., some automaton clause Q(f(X1...Xk)) :- Qblk1(X1),...,Qblkk(Xk))
 and justifications that Pblki subseteq Qblki, 1<=i<=k (see right below).
 *)
and block_incl_justif = BIJ of string -m> string * simple_inclusion_justif;
    (* prove that Pblk subseteq Qblk:
     each Q1 in Qblk \ Pblk is mapped to some
     P1 in Pblk and some justification j that P1 subseteq Q1. *)

exception SimpleInclusionFailEvt;
exception VerySimpleDisjointTooHardEvt;
exception SimpleDisjointFailEvt;

datatype simple_disjoint_justif = DJ_NO
       | DJ_CUT_HISTORY of (string * string) set * simple_disjoint_justif
       | DJ_IND_HYP of string * string (* use induction hypothesis
					bot :- P(X), Q(X). *)
       | DJ_VS of string * string * simple_model
	 (* use simple_model to show bot :- P(X), Q(X). *)
       | DJ_SUBSUMED of string set * simple_disjoint_justif
       | DJ_INDUCT of (string * string) *
	 (string -m> int * (block list -m> block list -m> int * simple_disjoint_justif))
	 (* Maps f to set of bodies
	  Pblkl=[Pblk1,...,Pblkk] in ?auto P and
	  Qblkl=[Qblk1,...,Qblkk] in ?auto Q,
	  each pair mapped to index i, 0<=i<k such that
	  Pblk<i+1> U Qblk<i+1> is empty.
	  *)
	 ;

exception FindP;
(*exception NonGround;*)

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

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

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

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

val split_sort = sort splitcmp;

fun model_check (a as AUTO (auto, univ), xgen : int -> ''_var, xfsig) =
    let val |[perr_gclause, perr_term, perr_varname, ...]| = perr_funs ()
	fun find_univ_1 (nil, _) = NONE
	  | find_univ_1 ((P $ _)::l, i) =
	    if P inset univ
		then SOME (P, i)
	    else find_univ_1 (l, i+1)
	  | find_univ_1 _ = raise FindUniv
	fun find_univ (GCLAUSE (_, pos)) =
	    find_univ_1 (pos, 0)
	fun find_neg_univ (GCLAUSE (neg, _)) =
	    find_univ_1 (neg, 0)
	fun find_auto_subsumer_1 (_, nil, _) = NONE
	  | find_auto_subsumer_1 (neg (*: ''_var term list*), (P $ [f $ l] (*: ''_var term*)) :: rest, i) =
	    if P inset auto
		then let val fmap = ?auto P
		     in
			 if f inset fmap
			     then let val (blkls, k, vars) = ?fmap f
				      val ir = ref 0
				      val sigma = {(inc ir; !ir) => t
						  | t in list l}
				      val negs = elems neg
				  in
				      (*
#put stderr " ** Testing ";
pretty stderr (pack (blkls : block list set));
#flush stderr ();
				       *)
				      case
					  some
					    blkl
					  | blkl in set blkls
					  val jr = ref 0
					      such that
						  all
						    let val tj = (inc jr;
								  if !jr inset sigma
								      then ?sigma (!jr)
								  else raise FindAutoSubsumer)
						    in
							all
							  (P $ [tj]) inset negs
							| P in set blk
							end
						    end
						  | blk in list blkl
						  end
					  end of
					  SOME blkl => SOME (P, f, k, sigma, blkl, i)
					| _ => find_auto_subsumer_1 (neg, rest, i+1)
				  end
			 else find_auto_subsumer_1 (neg, rest, i+1)
		     end
	    else find_auto_subsumer_1 (neg, rest, i+1)
	  | find_auto_subsumer_1 (neg, _ :: rest, i) =
	    find_auto_subsumer_1 (neg, rest, i+1)
	fun find_auto_subsumer (GCLAUSE (neg, pos)) =
	    find_auto_subsumer_1 (neg, pos, 0)
	(*
(#put stderr "*** find_auto_subsumer ";
 let val ir = ref 0
     val f as |[convert, put, seek, truncate, ...]| = outstring "X"
 in
     print_gclause (stderr, memofn _ => (inc ir; seek 1; truncate ();
					 print f (pack (!ir));
					 convert ()),
	 ?tptp_keywords "3.3.0")
     (GCLAUSE (neg, pos));
     #put stderr "\n";
     #flush stderr ()
 end;
	    find_auto_subsumer_1 (neg, pos, 0)
)
	 *)
	fun epsc_subsumes_noinst ((negs as {P, ...}, poss), neg, pos) =
	    some
	      t
	    | Q $ [t as V _] in set neg
		such that P=Q andalso
		    all
		      (P $ [t]) inset neg
		    | P in set negs
		    end andalso
		    all
		      (P $ [t]) inset pos
		    | P in set poss
		    end
	    end
	  | epsc_subsumes_noinst ((negs, poss as {P, ...}), neg, pos) =
	    some
	      t
	    | Q $ [t as V _] in set pos
	      such that P=Q andalso
		  all
		    (P $ [t]) inset neg
		  | P in set negs
		  end andalso
		  all
		    (P $ [t]) inset pos
		  | P in set poss
		  end
	    end
	  | epsc_subsumes_noinst _ = raise EpscSubsumesNoInst
	fun find_history_subsumer_1 ({}, ...) = NONE
	  | find_history_subsumer_1 ({epsc} U rest, neg, pos) =
	    (case epsc_subsumes_noinst (epsc, neg, pos) of
		 NONE => find_history_subsumer_1 (rest, neg, pos)
	       | SOME t => SOME (epsc, t)
		 )
	fun find_history_subsumer (history, GCLAUSE (neg, pos)) =
	    find_history_subsumer_1 (history, elems neg, elems pos)

	val epsdoner = ref ESEmpty
	fun find_epsc_subsumers (GCLAUSE (neg, pos)) =
	    let val terms = {t | _ $ [t] in list neg}
		    U {t | _ $ [t] in list pos}
	    in
		{t => let val epsc = ({P | P $ [u] in list neg
					     such that u=t},
					{Q | Q $ [v] in list pos
					       such that v=t})
		      in
			  eps_subsumers epsc (!epsdoner)
		      end
		| t in set terms}
	    end

	fun find_non_var_atom (nil, _, _) = NONE
	  | find_non_var_atom ((a as P $ [_ $ _]) :: l, i, acc) =
	    SOME (a, revappend (acc, l), i)
	  | find_non_var_atom (a::l, i, acc) = find_non_var_atom (l, i+1, a::acc)
	fun find_non_var_neg_atom (GCLAUSE (neg, _)) =
	    find_non_var_atom (neg, 0, nil)
	    (* It is interesting to choose a best possible non variable positive atom.
	     If we choose such an atom +P(f(t1,...,tn)) (C being the rest of the clause),
	     look at all clauses P(f(\bar X)) <= body_i (\bar X), 1<=i<=m,
	     and generate C \/ \/_i=1..m body_i (\bar t).
	     Let us say that body_i contains k_i atoms.
	     In the general case, we generate k_1...k_m new clauses by building
	     the CNF, all of length |C|+m.
	     In the simplified case, we try to satisfy C \/ body_i (\bar t)
	     for some i: this one generates k_i clauses, and we must choose
	     one among m.
	     Anyway, it seems OK to try and minimize k_1...k_m, or
	     equivalently sum_{i=1}^m log k_i.
	     *)
	fun sum {} = 0.0
	  | sum {a} = a
	  | sum s = let val (s1, s2) = split s
		    in
			sum s1 #+ sum s2
		    end
	fun find_non_var_atom_opt (nil, _, _, res) = res
	  | find_non_var_atom_opt ((a as P $ [f $ _]) :: l, i, acc, res) =
	    if P inset auto
		then let val fmap = ?auto P
		     in
			 if f inset fmap
			     then let val (blkls, k, vars) = ?fmap f
				      val weight = sum {log (sum {num (card B)
								 | B in list blkl})
						       | blkl in set blkls}
				      val better = case res of
						       SOME (_, _, _, oldw) => weight #< oldw
						     | _ => true
				  in
				      if better
					  then find_non_var_atom_opt (l, i+1, a::acc,
								      SOME (a, revappend (acc, l),
									    i, weight))
				      else find_non_var_atom_opt (l, i+1, a::acc, res)
				  end
			 else SOME (a, revappend (acc, l), i, 0.0) (* definitely simpler! *)
		     end
	    else SOME (a, revappend (acc, l), i, 0.0) (* definitely simpler! *)
	  | find_non_var_atom_opt (a::l, i, acc, res) =
	    find_non_var_atom_opt (l, i+1, a::acc, res)
	fun find_non_var_pos_atom (GCLAUSE (_, pos)) =
	    find_non_var_atom_opt (pos, 0, nil, NONE)
	val qs = auto_states a
	val epsilon_trans = auto_epsilon_trans (a, qs)
	(*$V-*)
	val _ = do_verbose (1, fn () =>
			    (#put stderr "Found epsilon equivalences:\n";
			     iterate
			       (#put stderr P;
				#put stderr " <=> ";
				(case qs of
				     {} => #put stderr "False.\n"
				   | _ =>
				     let val delimr = ref ""
				     in
					 iterate
					   (#put stderr (!delimr);
					    delimr := " \\/ ";
					    #put stderr q)
					 | q in set qs
					 end;
					 #put stderr ".\n"
				     end
				     ))
			     | P => qs in map epsilon_trans
			     end;
				#flush stderr ()
			     ))
	(*$V+*)
	fun find_neg_epsilon_atom (GCLAUSE (neg, pos)) =
	    let val nr = ref max_int
		val Pr = ref ""
		val lr = ref nil
		val qsr = ref {}
	    in
		iterate
		  let val qs = ?epsilon_trans P
		      val n = card qs
		  in
		      if n < !nr
			  then (nr := n; Pr := P; lr := l; qsr := qs)
		      else ()
		  end
		| P $ l in list neg
		  such that P inset epsilon_trans
		end;
		if !nr<max_int
		    then let val P = !Pr
			     val l = !lr
			     val qs = !qsr
			     fun find_P ((t as P' $ _) :: rest, left) =
				 if P'=P
				     then (left, rest)
				 else find_P (rest, t::left)
			       | find_P (nil, left) = raise FindP
			     val (left, right) = find_P (neg, nil)
			 in
			     SOME (P, l, qs, left, right, pos)
			 end
		else NONE
	    end
	fun resolve_neg_univ (GCLAUSE (neg, pos), P) =
	    let fun univ_neg_find ((a as Q $ _):: l) =
		    if Q=P
			then l
		    else a::univ_neg_find l
	    in
		GCLAUSE (univ_neg_find neg, pos)
	    end
	fun resolve_auto_neg (GCLAUSE (_, pos), neg, blkl, sigma) =
	    let val ir = ref 0
	    in
		GCLAUSE (append [let val i = (inc ir; !ir)
				     val ti = if i inset sigma
						  then ?sigma i
					      else raise ResolveAutoNeg
				 in
				     [P $ [ti]
				     | P in set blk]
				 end
				| blk in list blkl] @ neg,
			 pos)
	    end
	fun resolve_univ_neg (GCLAUSE (_, pos), neg) = GCLAUSE (neg, pos)
	fun resolve_univ_pos (GCLAUSE (neg, _), pos) = GCLAUSE (neg, pos)
	fun resolve_auto_pos (GCLAUSE (neg, _), pos, blkls, sigma) =
	    let val ir = ref 0
	    in
		(GCLAUSE (neg, pos),
		 [(ir := 0;
		   append [let val i = (inc ir; !ir)
			       val ti = if i inset sigma
					    then ?sigma i
					else raise ResolveAutoPos
			   in
			       [P $ [ti]
			       | P in set B]
			   end
			  | B in list blkl])
		 | blkl in set blkls])
	    end
	fun g_from_superclause (GCLAUSE (neg, pos), orandl) =
	    let val poss = elems pos
	    in
		{GCLAUSE (neg, [a | a in set poss U orl])
		| orl in set distr_and_or orandl}
	    end
	    (*
	fun g_from_superclause (GCLAUSE (neg, pos), nil) =
	    let val poss = elems pos (* eliminate duplicates *)
	    in
		{GCLAUSE (neg, [a
			       | a in set poss])}
	    end
	  | g_from_superclause (GCLAUSE (neg, pos), andl::rest) =
	    union {g_from_superclause (GCLAUSE (neg, a::pos), rest)
		  | a in list andl}
	    *)

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

	fun g_split_1 ((P $ [V x]) :: neg, pos, splits) =
	    let val (sneg, spos) = if x inset splits
				       then ?splits x
				   else ({}, {})
	    in
		g_split_1 (neg, pos, splits ++ {x => (sneg U {P}, spos)})
	    end
	  | g_split_1 (nil, (P $ [V x]) :: pos, splits) =
	    let val (sneg, spos) = if x inset splits
				       then ?splits x
				   else ({}, {})
	    in
		g_split_1 (nil, pos, splits ++ {x => (sneg, spos U {P})})
	    end
	  | g_split_1 (nil, nil, splits) = splits
	  | g_split_1 arg = raise GSplit1
	fun g_split (GCLAUSE (neg, pos)) = g_split_1 (neg, pos, {})
	fun g_split_sort c =
	    let val s = g_split c
	    in
		[(x, eps) | x => eps as ({_, ...}, {_, ...}) in map s] @
		[(x, eps) | x => eps as ({_, ...}, {}) in map s] @
		[(x, eps) | x => eps as ({}, {_, ...}) in map s]
	    end
(*
	fun xi (i : int) =
	    let val f as |[convert, ...]| = outstring xname
	    in
		print f (pack i);
		V (convert ())
	    end
*)
	fun g_from_eps_clause (t, negP, posP) =
	    GCLAUSE ([P $ [t]
		     | P in set negP],
		       [P $ [t]
		       | P in set posP])

	fun P_auto P = if P inset auto (* P should not be in univ *)
			   then ?auto P
		       else {}
	    
	fun find_var_lit1 {} = raise CheckEpsClause
	  | find_var_lit1 {P} = (P, card (P_auto P))
	  | find_var_lit1 {Q} U rest =
	    let val n = card (P_auto Q)
		val (P, m) = find_var_lit1 rest
	    in
		if n<=m
		    then (Q, n)
		else (P, m)
	    end
	fun find_var_lit l = #1 (find_var_lit1 l)

	fun sij_cut_history (_, SIJ_NO) = SIJ_NO
	  | sij_cut_history args = SIJ_CUT_HISTORY args

	memofun sij_actual_history SIJ_NO = raise SimpleInclusionFailEvt
	      | sij_actual_history (SIJ_CUT_HISTORY (h', _)) = h'
	      | sij_actual_history (SIJ_UNIV _) = {}
	      | sij_actual_history (SIJ_TAUTO _) = {}
	      | sij_actual_history (SIJ_IND_HYP PQ) = {PQ}
	      | sij_actual_history (SIJ_INDUCT (eps, fmap)) =
		union {union {union {union {sij_actual_history ij
					   | Q1 => (P1, ij) in map Q1map}
				    | BIJ Q1map in list ji}
			     | Pblkl => (Qblkl, ji) in map blkmap}
		      | f => (k, blkmap) in map fmap}
		\ {eps}

	val simple_inclusions_r =
	    ref ({} : string * string -m> (string * string) set
		   -m> simple_inclusion_justif)
	fun find_simple_inclusion (pair, history) =
	    if pair inset !simple_inclusions_r
		then let val hs = ?(!simple_inclusions_r) pair
		     in
			 if history inset hs
			     then SOME (?hs history, history)
			 else
			     some
			       (ij, history')
			      | history' => ij in map hs
				  such that history' subset history
				      andalso ij<>SIJ_NO
			      end
		     end
	    else NONE
	fun add_simple_inclusion (pair, history, ij) =
	    if pair inset !simple_inclusions_r
		then simple_inclusions_r := !simple_inclusions_r
		    ++ {pair => ?(!simple_inclusions_r) pair ++ {history => ij}}
	    else simple_inclusions_r := !simple_inclusions_r
		++ {pair => {history => ij}}
	fun check_inclusion_simple (history : (string * string) set,
				    pair as (P, Q)) =
	    (* test whether P subseteq Q, i.e., Q(X) :- P(X)
	     holds in the model.  This is done by finding
	     a bisimulation, which can be done (if doable at
	     all) in polynomial time.
	     Imitated from auto_simple_inclusions, in auto.ml.
	     *)
	    if Q inset univ
		then SIJ_UNIV Q
	    else if P=Q
		then SIJ_TAUTO Q
	    else if P inset univ
		then SIJ_NO
	    else if pair inset history
		then SIJ_IND_HYP pair
	    else (case find_simple_inclusion (pair, history) of
		      SOME (ij,history') =>
		      if history=history'
			  then ij
		      else let val res = sij_cut_history (history', ij)
			   in
			       add_simple_inclusion (pair, history, res);
			       res
			   end
		    | NONE =>
		      (let val Qfmap = if Q inset auto
					   then ?auto Q
				       else {}
			   val Pfmap = if P inset auto
					   then ?auto P
				       else {}
			   val new_history = history U {pair}
			   val res =
			       SIJ_INDUCT (pair,
					   {f =>
					    (Pk,
					     if f inset Qfmap
						 then let val (Qblkls, ...) = ?Qfmap f
						      in
							  {Pblkl =>
							   (case
								some
								  (Qblkl, bij)
								| Qblkl in set Qblkls
								val SOME bij =
								    check_blockl_incl
								    (new_history, Pblkl, Qblkl)
								end of
								SOME x => x
							      | _ =>
								raise SimpleInclusionFailEvt)
							  | Pblkl in set Pblkls}
						      end
					     else raise SimpleInclusionFailEvt
						 )
					   | f => (Pblkls, Pk, Pvars) in map Pfmap
					     })
			       handle SimpleInclusionFailEvt =>
			       SIJ_NO
			   val history' = sij_actual_history res
			       handle SimpleInclusionFailEvt => history
		       in
			   add_simple_inclusion (pair, history', res);
			   if history=history'
			       then res
			   else let val res' = sij_cut_history (history', res)
				in
				    add_simple_inclusion (pair, history, res');
				    res'
				end
		       end
			   ))
	and check_block_incl (history, Pblk, Qblk) =
	    (SOME (BIJ {Q1 => (case
				   some
				     (P1, x)
				   | P1 in set Pblk
				   val x =
				       check_inclusion_simple (history, (P1, Q1))
				       such that x<>SIJ_NO
				   end of
				   SOME x => x
				 | _ => raise SimpleInclusionFailEvt)
		       | Q1 in set Qblk \ Pblk})
	     handle SimpleInclusionFailEvt => NONE)
	and check_blockl_incl (history, Pblkl, Qblkl) =
	    (SOME [(case check_block_incl (history, Pblk, Qblk) of
			SOME bij => bij
		      | _ => raise SimpleInclusionFailEvt)
		  || Pblk in list Pblkl
		  and Qblk in list Qblkl
		       ]
	     handle SimpleInclusionFailEvt => NONE)

	val j_of_ij_memo_r = table ()
	    : (simple_inclusion_justif
	       * string * string * ''_var term,
	       ''_var mc_justif) table
	val j_of_ij_get = t_get j_of_ij_memo_r
	val j_of_ij_put = t_put j_of_ij_memo_r
	fun j_of_ij_memo input =
	    (case j_of_ij_get input of
		 SOME res => res
	       | _ => let val res = j_of_ij input
		      in
			  j_of_ij_put (input, res);
			  res
		      end)
	and j_of_ij (SIJ_NO, ...) = raise JOfIj
	  | j_of_ij (SIJ_CUT_HISTORY (h, j), P0, Q0, t) =
	    MC_CUT_HISTORY ({({P}, {Q})
			    | (P,Q) in set h},
			      j_of_ij (j, P0, Q0, t))
	  | j_of_ij (SIJ_UNIV _, P, Q, t) =
	    MC_SUBSUMED_UNIV (GCLAUSE ([P $ [t]], [Q $ [t]]), Q, 0)
	  | j_of_ij (SIJ_TAUTO _, P, Q, t) =
	    MC_TAUTO (GCLAUSE ([P $ [t]], [Q $ [t]]), 0)
	  | j_of_ij (SIJ_IND_HYP _, P, Q, t) =
	    MC_SUBSUMED_HISTORY (GCLAUSE ([P $ [t]], [Q $ [t]]), ({P}, {Q}), t)
	  | j_of_ij (ij as SIJ_INDUCT (_, fmap), P, Q, V x) =
	    MC_INDUCT (x, ({P}, {Q}), SOME P,
		       [let val ir = ref 0
			    val args = [V (xgen (inc ir; !ir))
				       |while !ir < k]
			    val t = f $ args
			    val Pt = P $ [t]
			    val Qt = Q $ [t]
			    val c = GCLAUSE ([Pt], [Qt])
			    val sigma = (ir := 0;
					 {(inc ir; !ir) => ti
					 | ti in list args})
			in
			    (f, k, (* now produce justifications for Q(t) :- P(t). *)
			     MC_ELIM_NEG (c, Pt, k, sigma,
					  (* produce justifications for
					   Q(t) :- Pblk1(X1), ..., Pblkk(Xk)
					   *)
					  [MC_DEDUCE_POS (GCLAUSE (Pneg, [Qt]),
							  Qt, 0,
							  (* produce justification
							   for superclause
							   Qblkl(X1...Xk) :-
							   Pblk1(X1), ..., Pblkk(Xk)
							   *)
							  {Qblkl},
							  MC_DISTR_POS (GCLAUSE (Pneg, nil),
									orandl,
									(* Now produce justifications
									 for Pblki subseteq Qblki: *)
									append [[(case Pneg of
										      [_] => j
										    | _ =>
										      MC_SUBSUMED (GCLAUSE (Pneg, [Q1 $ [x]]),
												   j)
										      )
										| Q1 in set Qblk
										    val j =
											if Q1 inset Q1map
											    then let val (P1, ij) =
													 ?Q1map Q1
												 in
												     j_of_ij_memo (ij, P1, Q1, x)
												 end
											else j_of_ij_memo (SIJ_TAUTO Q1,
												      Q1, Q1, x)
											    ]
									       || Qblk in list Qblkl
									       and Pblk in list Pblkl
									       and x in list args
									       and BIJ Q1map in list ji]
									)
							  )
					  | Pblkl => (Qblkl, ji) in map blkmap
					      val Pneg =
						  append [[Pi $ [xi]
							  | Pi in set Pblk]
							 || Pblk in list Pblkl
							 and xi in list args]
					      val andl = append [[Qi $ [x]
								 | Qi in set Qblk]
								|| Qblk in list Qblkl
								and x in list args]
					      val orandl = [andl]
							  ])
			     )
			end
		       | f => (k, blkmap) in map fmap])
	  | j_of_ij arg = raise JOfIjBug

	val |[find, equate, select, equate_all, reset, ...]| = cc ()

	fun val_of_state q =
	    ("!" ^ q) $ nil

	val vsdj =
	    (let val fr = ref {}
	     in
		 iterate
		   find (val_of_state q)
		 (* add q to the universe, for each state q. *)
		 | q in set qs \ univ
		 end;
		 find (val_of_state ""); (* the bottom state *)
		 (* Now, for each automaton clause
		  q(f(X1,...,Xn)) :- B1(X1), ..., Bn(Xn)
		  with q in qs,
		  add the equations f(B1, ..., Bn)=q
		  together with, for each block B=q1,...,qk,
		  equations B=q1=...=qk.
		  In case some Bi is empty, we just fail.
		  (It might be allowable to let one Bi be empty,
		  then instantiate the ith argument to f by
		  every possible color, but more than one Bi
		  would be prohibitive.)
		  This defines an evaluation function Eval,
		  such that Eval t is a color (or bottom,
		  if outside the universe) for each ground term t.
		  The point is that, if q(t) holds
		  then Eval t = Eval q,
		  so that if Eval q <> Eval q', then
		  there is no term t with both q(t) and q'(t).

		  Assumes, for correctness, that no automaton
		  clause is such that q, or in fact any predicate
		  in any Bi, is universal.  (We remove those clauses
		  with q in univ, and remove universal predicates
		  from bodies.)
		  *)
		 iterate
		   iterate
		     (fr := !fr U {f};
		      iterate
			let val ir = ref 0
			    val args = [(inc ir;
					 if blk subset univ
					     then raise VerySimpleDisjointTooHardEvt
					 else let val {q} U rest = blk \ univ
						  val vq = val_of_state q
					      in
						  iterate
						    (do_verbose (4, fn () =>
								 (#put stderr "--- equate ";
								  #put stderr q;
								  #put stderr "=";
								  #put stderr q';
								  #put stderr "\n";
								  #flush stderr ()));
						    equate (vq,
							    val_of_state q')
						    )
						  | q' in set rest
						  end;
						  vq
					      end)
				       | blk in list blkl]
			    val fargs = f $ args
			in
			    do_verbose (4, fn () =>
					(#put stderr "--- equate all ";
					 print stderr (pack fargs);
					 #put stderr "=";
					 #put stderr P;
					 #put stderr "\n";
					 #flush stderr ()));
			    equate (fargs, val_of_state P)
			    (* equate_all (fargs, val_of_state P,
			                   tvars fargs)
			     *)
			end
		      | blkl in set blkls
		      end
		      )
		   | f => (blkls, ...) in map fmap
		   end
		 | P => fmap in map (qs \ univ) <| auto
		 end;
		 let val colors = {q => find (val_of_state q)
				  | q in set qs \ univ}
		     val allcolors = rng colors
		     val ir = ref 0
		     val numbering = {col => (inc ir; !ir)
				     | col in set allcolors}
			 ++ {find (val_of_state "") => 0}
		     val qmap = numbering O colors
		     val invqmap = invrel qmap
		 in
		     SOME (qmap : string -m> int,
			   invqmap : int -m> string set,
			   (* maps each state q to an index i,
			    representative of its color. *)
			   {f => overwrite [{args' => i
					    | _ $ args in set terms
						val args' = [?numbering (find u)
							    | u in list args]}
					   | c in set allcolors
					       val i = ?numbering c
					       val terms = select ({f}, c)]
			   | f in set !fr}
			   : string -m> int list -m> int
			   (* describe model: map each f to possibly incomplete
			    map from tuples of values (indices) to the
			    value of f on this tuple.
			    *)
			   )
		     before reset ()
		 end
	     end
	     handle VerySimpleDisjointTooHardEvt => (reset (); NONE))

	    (*$V-*)
	    val _ = do_verbose (1, fn () =>
				case vsdj of
				    SOME (qmap, invqmap, ftables) =>
				    (#put stderr "Found state equivalence classes \
				     \(states mapped to distinct numbers have empty intersection):\n";
				     iterate
				       (#put stderr " ";
					#put stderr q;
					#put stderr ":";
					print stderr (pack i))
				     | q => i in map qmap
				     end;
				     #put stderr "\n";
				     #flush stderr ()
				     )
				  | NONE =>
				    (#put stderr "No interesting equivalence relation on states found.\n";
				     #flush stderr ()))
	    (*$V+*)

(*
val _ = (case vsdj of
	     SOME (qmap, invqmap, ftables) =>
	     (#put stderr "*** qmap = ";
	      pretty stderr (pack qmap);
	      #put stderr "*** ftables = ";
	      pretty stderr (pack ftables);
	      #flush stderr ())
	   | NONE => (#put stderr "*** very simple disjoint too hard!\n";
		      #flush stderr ()))
*)

	fun dj_cut_history (_, DJ_NO) = DJ_NO
	  | dj_cut_history args = DJ_CUT_HISTORY args

	memofun dj_actual_history DJ_NO = raise SimpleDisjointFailEvt
	      | dj_actual_history (DJ_CUT_HISTORY (h', _)) = h'
	      | dj_actual_history (DJ_IND_HYP PQ) = {PQ}
	      | dj_actual_history (DJ_VS _) = {}
	      | dj_actual_history (DJ_SUBSUMED (_, dj)) =
		dj_actual_history dj
	      | dj_actual_history (DJ_INDUCT (PQ, fmap)) =
		union {union {union {dj_actual_history dj
				    | Qblkl => (_, dj) in map Qblklmap}
			     | Pblkl => Qblklmap in map Pblklmap}
		      | f => (_, Pblklmap) in map fmap}
		\ {PQ}

	val simple_disjoints_r =
	    ref ({} : string * string -m> (string * string) set
		   -m> simple_disjoint_justif)
	fun find_simple_disjoint (pair, history) =
	    if pair inset !simple_disjoints_r
		then let val hs = ?(!simple_disjoints_r) pair
		     in
			 if history inset hs
			     then SOME (?hs history, history)
			 else
			     some
			       (dj, history')
			      | history' => dj in map hs
				  such that history' subset history
				      andalso dj<>DJ_NO
			      end
		     end
	    else NONE
	fun add_simple_disjoint (pair, history, dj) =
	    if pair inset !simple_disjoints_r
		then simple_disjoints_r := !simple_disjoints_r
		    ++ {pair => ?(!simple_disjoints_r) pair ++ {history => dj}}
	    else simple_disjoints_r := !simple_disjoints_r
		++ {pair => {history => dj}}
	fun find_simple_disjoint_s (_, {}) = NONE
	  | find_simple_disjoint_s (_, {_}) = NONE
	  | find_simple_disjoint_s (history, {P,Q}) =
	    (* First attempt to find a pair {P,Q} subset Ps such
	     that false :- P(X), Q(X) would be a consequence of history.
	     This mostly replacates the beginning of check_disjoint_pair.
	     *)
	    if (P, Q) inset history
		then SOME (DJ_IND_HYP (P, Q))
	    else (case find_simple_disjoint ((P, Q), history) of
		      SOME (dj, history') =>
		      if history=history'
			  then SOME dj
		      else let val res = dj_cut_history (history', dj)
			   in
			       add_simple_disjoint ((P, Q), history, res);
			       SOME res
			   end
		    | NONE => NONE)
	  | find_simple_disjoint_s (history, Ps) =
	    (* Now the following duplicates parts of check_disjoint_simple1 *)
	    let val (left, right) = split Ps
	    in
		case find_simple_disjoint_s (history, left) of
		    NONE =>
		    (case find_simple_disjoint_s (history, right) of
			 NONE =>
			 (case some
			      dj
			       | P in set left and Q in set right
			       val SOME dj = find_simple_disjoint_s (history,
								     {P, Q})
			       end of
			      SOME (DJ_SUBSUMED (_, dj)) =>
			      SOME (DJ_SUBSUMED (Ps, dj))
			    | optdj => optdj)
			 | dj => dj
			 )
		  | dj => dj
	    end
	fun check_disjoint_very_simple Ps =
	    (case vsdj of
		 SOME (qmap, invqmap, ftables) =>
		 (case {i | q => i in map Ps <| qmap} of
		      {i,j,...} => (* two different colors: so there
				    are two states q,q' in Ps that
				    have empty intersection. *)
		      let val {q, ...} = ?invqmap i & Ps
			  val {q', ...} = ?invqmap j & Ps
			  val dj = DJ_VS (q, q', SM (qmap, ftables))
		      in
			  if Ps={q,q'}
			      then SOME dj
			  else SOME (DJ_SUBSUMED (Ps, dj))
		      end
		    | _ => NONE)
	       | NONE => NONE)
	fun check_disjoint_simple (history : (string * string) set, Ps) =
	    (case check_disjoint_very_simple Ps of
		 SOME dj =>
		 if empty history
		     then dj
		 else DJ_CUT_HISTORY ({}, dj)
	       | NONE => 
	    (case find_simple_disjoint_s (history, Ps) of
		 SOME dj => dj
	       | NONE => check_disjoint_simple1 (history, Ps)))
	and check_disjoint_simple1 (history : (string * string) set,
				   pair as {P, Q}) =
	    (* test whether no term is recognized at both P and Q,
	     i.e., whether we can prove false :- P(X), Q(X).
	     This is done by a technique resembling bisimulation checking.
	     *)
	    check_disjoint_pair (history, (P, Q))
	  | check_disjoint_simple1 (history, {P}) = DJ_NO
	  | check_disjoint_simple1 (history, {}) = DJ_NO
	  | check_disjoint_simple1 (history, Ps) =
	    (* refuse to check intersection of more than two predicates.
	     So pick two.  This is done by splitting Ps, and finding
	     two in the left part, or two in the right part, or one in each. *)
	    let val (left, right) = split Ps
	    in
		case check_disjoint_simple1 (history, left) of
		    DJ_NO =>
		    (case check_disjoint_simple1 (history, right) of
			 DJ_NO =>
			 (case some dj
			       | P in set left and Q in set right
				 val dj = check_disjoint_simple1 (history,
								 {P, Q})
				     such that dj<>DJ_NO
			       end of
			      SOME (DJ_SUBSUMED (_, dj)) =>
			      DJ_SUBSUMED (Ps, dj)
			    | SOME dj =>
			      DJ_SUBSUMED (Ps, dj)
			    | NONE => DJ_NO)
		       | dj => dj)
		  | dj => dj
	    end
	and check_disjoint_pair (history, pair as (P, Q)) =
	     (* with P<>Q, and P, Q not in univ *)
	    (
	     if pair inset history
		 then DJ_IND_HYP pair
	     else (
(*
#put stderr "Check disjoint pair ";
#put stderr P;
#put stderr ", ";
#put stderr Q;
#put stderr " (card history=";
print stderr (pack (card history));
#put stderr ")\n";
#flush stderr ();
*)
		   case find_simple_disjoint (pair, history) of
		       SOME (dj, history') =>
		       if history=history'
			   then dj
		       else let val res = dj_cut_history (history', dj)
			    in
				add_simple_disjoint (pair, history, res);
				res
			    end
		     | NONE =>
		       (let val Qfmap = if Q inset auto
					   then ?auto Q
				       else {}
			   val Pfmap = if P inset auto
					   then ?auto P
				       else {}
			   val new_history = history U {pair}
			   val res =
			       DJ_INDUCT (pair,
					  {f =>
					   (Pk,
					    {Pblkl =>
					     {Qblkl =>
					      check_blockl_disjoint (new_history,
								     0, Pblkl, Qblkl)
					     | Qblkl in set Qblkls}
					    | Pblkl in set Pblkls
						val Qblkls =
						    if f inset Qfmap
							then #1 (?Qfmap f)
						    else {}}
					    )
					  | f => (Pblkls, Pk, Pvars) in map Pfmap})
(*
val _ = (#put stderr "Compute actual history..."; #flush stderr ())
*)
			   val history' = dj_actual_history res
			       handle SimpleDisjointFailEvt => history
(*
val _ = (#put stderr " done.\n"; #flush stderr ())
*)
			in
			    add_simple_disjoint (pair, history', res);
			    if history=history'
				then res
			    else let val res' = dj_cut_history (history', res)
				 in
				     add_simple_disjoint (pair, history, res');
				     res'
				 end
			end handle SimpleDisjointFailEvt => DJ_NO
		       ))
)
	and check_blockl_disjoint (_, _, nil, nil) =
	    raise SimpleDisjointFailEvt
	  | check_blockl_disjoint (history, i, Pblk::Prest, Qblk::Qrest) =
	    (case check_disjoint_simple (history, Pblk U Qblk) of
		 DJ_NO => check_blockl_disjoint (history, i+1, Prest, Qrest)
	       | dj => (i, dj))

	fun dj_preds DJ_NO = raise DjPreds
	  | dj_preds (DJ_CUT_HISTORY (_, dj)) = dj_preds dj
	  | dj_preds (DJ_IND_HYP (P, Q)) = {P, Q}
	  | dj_preds (DJ_VS (P, Q, _)) = {P, Q}
	  | dj_preds (DJ_SUBSUMED (Ps, _)) = Ps
	  | dj_preds (DJ_INDUCT ((P, Q), ...)) = {P, Q}

	val j_of_dj_memo_r = table ()
	    : (simple_disjoint_justif * ''_var term,
	       ''_var mc_justif) table
	val j_of_dj_get = t_get j_of_dj_memo_r
	val j_of_dj_put = t_put j_of_dj_memo_r
	fun j_of_dj_memo input =
	    (case j_of_dj_get input of
		 SOME res => res
	       | _ => let val res = j_of_dj input
		      in
			  j_of_dj_put (input, res);
			  res
		      end)
	and j_of_dj (DJ_NO, ...) = raise JOfDj
	  | j_of_dj (DJ_CUT_HISTORY (h, dj), t) =
	    MC_CUT_HISTORY ({({P,Q}, {})
			    | (P, Q) in set h},
			      j_of_dj (dj, t))
	  | j_of_dj (DJ_IND_HYP (P, Q), t) =
	    MC_SUBSUMED_HISTORY (GCLAUSE ([P $ [t], Q $ [t]], nil),
				 ({P,Q}, {}), t)
	  | j_of_dj (DJ_VS (P, Q, sm), V x) =
	    MC_VS (x, P, Q, sm)
	  | j_of_dj (DJ_SUBSUMED (Ps, dj), t) =
	    MC_SUBSUMED (GCLAUSE ([P $ [t] | P in set Ps], nil),
			 j_of_dj (dj, t))
	  | j_of_dj (DJ_INDUCT ((P, Q), fmap), V x) =
	    MC_INDUCT (x, ({P,Q}, {}), SOME P,
		       [let val ir = ref 0
			    val args = [V (xgen (inc ir; !ir))
				       |while !ir < k]
			    val t = f $ args
			    val neg as [Pt, Qt] = [q $ [t] | q in set {P, Q}]
			    val c = GCLAUSE (neg, nil)
			    val sigma = (ir := 0;
					 {(inc ir; !ir) => ti
					 | ti in list args})
			in
			    (f, k, (* now produce justifications 
				    for false :- P(t), Q(t). *)
			     MC_ELIM_NEG (c, Pt, k, sigma,
					  (* produce justifications for
					   false :- Q (t),
					   Pblk1(X1), ..., Pblkk(Xk)
					   *)
					  [MC_ELIM_NEG (c', Qt, k, sigma,
							(* produce justifications
							 for
							 false :- Pblk1 U Qblk1(X1),
							 ..., Pblkk U Qblkk (Xk)
							 *)
							[if k=1
							     then j
							 else MC_SPLIT (GCLAUSE ([a | a in set lits], nil),
									j)
							| Qblkl => (i, dj)
							  in map Qblklmap
							    val xi = args nth i
							    val j =
								j_of_dj_memo (dj, xi)
							    val lits =
								elems Pneg
								U union {{Qi $ [xi]
									 | Qi in set Qblk}
									|| Qblk in list Qblkl
									   and xi in list args}
							      ]
							)
					  | Pblkl => Qblklmap in map Pblklmap
					    val Pneg =
						append [[Pi $ [xi]
							| Pi in set Pblk]
							 || Pblk in list Pblkl
						       and xi in list args]
					    val c' = GCLAUSE (Qt :: Pneg, nil)
					    ]))
			end
		       | f => (k, Pblklmap) in map fmap])
	  | j_of_dj arg = raise JOfDjBug

(* OBSOLETE: never succeeds in practice
	val pos_value_checker =
	    (case vsdj of
		 NONE => (fn _ => NONE)
	       | SOME (qmap, invqmap, ftables) =>
		 let fun pv_admissible (i,P) = P inset univ
			 orelse (P inset qmap andalso i = ?qmap P)
		     fun blk_admissible (i,blk) =
			 all
			   pv_admissible (i,P)
			 | P in set blk
			 end
		     fun blkl_admissible (il,blkl) =
			 all
			   blk_admissible (i,blk)
			 || i in list il and blk in list blkl
			 end
		     memofun args_from_res f =
			     if f inset ftables
				 then let val fmap = ?ftables f
					  val invfmap = invrel fmap
				      in
					  fn i =>
					     if i inset invfmap
						 then ?invfmap i
					     else {}
				      end
			     else (fn _ => {})
		     val vcr = ref ({} : int * string -m> (int * string) set
				      -m> vc_justif)
		     fun find_vc (ip, history) =
			 if ip inset !vcr
			     then let val hs = ?(!vcr) ip
				  in
				      if history inset hs
					  then SOME (?hs history, history)
				      else
					  some
					    (vcj, history')
					  | history' => vcj in map hs
					    such that history' subset history
						andalso vcj<>VC_NO
					  end
				  end
			 else NONE
		     fun add_vc (ip, history, vcj) =
			 if ip inset !vcr
			     then vcr := !vcr ++ {ip => ?(!vcr) ip ++ {history => vcj}}
			 else vcr := !vcr ++ {ip => {history => vcj}}
		     fun vc_cut_history (_, VC_NO) = VC_NO
		       | vc_cut_history args = VC_CUT_HISTORY args
		     fun vc_actual_history VC_NO = raise VcEvt
		       | vc_actual_history (VC_CUT_HISTORY (h', _)) = h'
		       | vc_actual_history (VC_IND_HYP jq) = {jq}
		       | vc_actual_history (VC_UNIV _) = {}
		       | vc_actual_history (VC_INDUCT (ip, fmap)) =
			 union {union {union {union {vc_actual_history vcj
						    | vcj in list vcjl}
					     | vcjl in list vcjll}
				      | _ => (_, vcjll) in map argsmap}
			       | _ => argsmap in map fmap}
			 \ {ip}

		     fun vc1 (history, ip as (i, P)) =
			 (* check that every ground term
			  that has value i in the finite model
			  described by fvalues
			  is recognized at state P in (univ, auto).
			  We assume pv_admissible(i,P) holds.
			  *)
			 if ip inset history
			     then VC_IND_HYP ip
			 else (case find_vc (ip, history) of
				   SOME (vcj, history') =>
				   if history=history'
				       then vcj
				   else let val res = vc_cut_history (history', vcj)
					in
					    add_vc (ip, history, res);
					    res
					end
				 | NONE =>
				   let val new_history = history U {ip}
				       val res =
					   if P inset univ
					       then VC_UNIV ip
					   else if P inset auto
					       then let val fmap = ?auto P
						    in
							VC_INDUCT (ip,
								   {f =>
								    if f inset fmap
									then let val (blkls, ...) = ?fmap f
									     in
										 {args => (case eres of
											       SOME (blkl, z) => ((P, f, blkl), z)
											     | _ => raise VcEvt
											       )
										 | args in set argss
										     val eres =
											 some z
											 | blkl in set blkls
											 val SOME z =
											     if blkl_admissible (args, blkl)
												 then SOME (blkl,
													    [[(case vc1 (new_history,
															 (j,Q)) of
														   VC_NO => raise VcEvt
														 | vcj => vcj)
													     | Q in set blk]
													    || j in list args
													    and blk in list blkl])
												     handle VcEvt => NONE
											     else NONE
											 end
											 }
									     end
								    else raise VcEvt
								   | f in set ftables
								       val argss = args_from_res f i
									   })
							handle VcEvt => VC_NO
						    end
					   else VC_NO
				       val history' = vc_actual_history res
					   handle VcEvt => history
				   in
				       add_vc (ip, history, res);
				       if history=history'
					   then res
				       else let val res' = vc_cut_history (history', res)
					    in
						add_vc (ip, history, res');
						res'
					    end
				   end handle VcEvt => VC_NO
				   )
(*
			 if ip inset !vcr
			     then ?(!vcr) ip
			 else (vcr := !vcr ++ {ip => true};
			       let val res =
				       if P inset univ
					   then true
				       else if P inset auto
					   then let val fmapa = ?auto P
						in
						    all
						      all
							f inset fmapa andalso
							exists
							  all
							    all
							      vc1 (j, Q)
							    | Q in set blk
							    end
							  || j in list args
							  and blk in list blkl
							  end
							| blkl in set #1 (?fmapa f)
							    such that
								blkl_admissible (args,
										 blkl)
							end
						      | args in set argss
						      end
						    | f in set ftables
						    val argss = args_from_res f i
						    end
						end
				       else false
			       in
				   vcr := !vcr ++ {ip => res};
				   res
			       end
			       )
		     fun vc ip = pv_admissible ip andalso vc1 ip
*)
		     fun vc ip = if pv_admissible ip
				     then vc1 ({}, ip)
				 else VC_NO

		     fun eval_value (V x, rho) =
			 if x inset rho
			     then ?rho x
			 else raise EvalUndefinedEvt
		       | eval_value (f $ l, rho) =
			 if f inset ftables
			     then let val fmap = ?ftables f
				      val vals = [eval_value (t, rho) | t in list l]
				  in
				      if vals inset fmap
					  then ?fmap vals
				      else raise EvalUndefinedEvt
				  end
			 else raise EvalUndefinedEvt
		     fun check_atom_value (P $ [t], rho) =
			 (let val i = eval_value (t, rho)
			  in
(*
#put stderr "\nvalue of ";
perr_term t;
#put stderr " is ";
print stderr (pack i);
*)
			      vc (i,P)
			  end handle EvalUndefinedEvt => VC_NO)
		       | check_atom_value (a, rho) = raise PosCheckValue

		     fun get_neg_values (nil, rho) = rho
		       | get_neg_values ((P $ [V x]) :: neg, rho) =
			 if P inset univ
			     then get_neg_values (neg, rho)
			 else if P inset qmap
			     then let val i = ?qmap P
				      val rho' = 
					  if x inset rho
					      then if ?rho x=i
						       then rho
						   else raise EvalUndefinedEvt
					  else rho ++ {x => i}
				  in
				      get_neg_values (neg, rho')
				  end
			      else raise EvalUndefinedEvt
		       | get_neg_values (neg, rho) = raise GetNegValues
		 in
		     fn (gc as GCLAUSE (neg, pos)) =>
			(
(*
#put stderr "\n*** pos_value_checker: ";
perr_gclause gc;
*)
			 let val rho = get_neg_values (neg, {})
			 in
(*
#put stderr "\nrho =";
iterate
  (#put stderr " "; #put stderr (perr_varname x); #put stderr "=";
   print stderr (pack i))
| x => i in map rho
end;
*)
			     some
			       (t, vcj, rho, SM (qmap, ftables))
			     | a as P $ [t] in list pos
			     val vcj = check_atom_value (a, rho)
				 such that vcj<>VC_NO
			     end
			 end handle EvalUndefinedEvt =>
			 NONE
(*
(#put stderr "\nCannot check."; NONE)
*)
			 )
		 end
		 )
*)

	fun neg_split_1 ((P $ [V x]) :: neg, varsplits, othersplits) =
	    let val sneg = if x inset varsplits
			       then ?varsplits x
			   else {}
	    in
		neg_split_1 (neg, varsplits ++ {x => sneg U {P}},
			     othersplits)
	    end
	  | neg_split_1 ((P $ [t]) :: neg, varsplits, othersplits) =
	    let val sneg = if t inset othersplits
			       then ?othersplits t
			   else {}
	    in
		neg_split_1 (neg, varsplits, othersplits ++ {t => sneg U {P}})
	    end
	  | neg_split_1 (a :: neg, varsplits, othersplits) =
	    neg_split_1 (neg, varsplits, othersplits)
	  | neg_split_1 (nil, varsplits, othersplits) =
	    (varsplits, othersplits)
	fun find_neg_empty_inter (history, c as GCLAUSE (neg, _)) =
	    let val (sxneg, stneg) = neg_split_1 (neg, {}, {})
		val h = {(P, Q)
			| ({P,Q}, {}) in set history}
	    in
		case
		    some
		      let val x' = xgen 1
			  val t' = V x'
			  (*val c' = GCLAUSE ([P $ [t'] | P in set Ps], nil)*)
			  val j = j_of_dj_memo (dj, t')
		      in
			  MC_SUBSUMED_EPSC (c, t, j)
		      end
		    | x => Ps in map sxneg
		    val t = V x
		    val dj = check_disjoint_simple (h, Ps)
			such that dj<>DJ_NO
		    end of
		    SOME res => SOME res
		  | NONE =>
		    some
		       MC_SUBSUMED_EPSC (c, t,
					 j_of_dj_memo (dj', V (xgen 1)))
		    | t => Ps in map stneg
		    val SOME dj = check_disjoint_very_simple Ps
		    val dj' = case dj of
				  DJ_SUBSUMED (_, dj') => dj'
				| _ => dj
		    end
	    end

	fun check_epsc_simple_1 (history, P, Q, t) = (* find a proof of Q(t) :- P(t)
					     from simple inclusion P subseteq Q. *)
	    let val h = {(P,Q)
			| ({P}, {Q}) in set history}
	    in
		case check_inclusion_simple (h, (P, Q)) of
		    SIJ_NO => NONE
		  | sij => SOME (j_of_ij_memo (sij, P, Q, t))
	    end
	fun check_epsc_simple (history, neg, head as P $ [t as V _]) =
	    some j
	    | Q $ [t'] in list neg
	    val SOME j = if t=t'
			     then check_epsc_simple_1 (history, Q, P, t)
			 else NONE
	    end
	  | check_epsc_simple _ = NONE
	fun check_horn_simple (history, neg) =
	    let memofun chs (head as P $ [t]) =
			if P inset univ
			    then SOME (MC_SUBSUMED_UNIV (GCLAUSE (neg, [head]), P, 0))
			else (case check_epsc_simple (history, neg, head) of
				  (sj as SOME j) =>
				  (case neg of
				       [_] => sj
				     | _ => SOME (MC_SUBSUMED (GCLAUSE (neg, [head]), j)))
				| NONE =>
				  (case t of
				       f $ l =>
				       if P inset auto
					   then let val fmap = ?auto P
						in
						    if f inset fmap
							then let val (blkls, k, ...) = ?fmap f
							     in
								 some
								   MC_DEDUCE_POS (GCLAUSE (neg, [head]),
										  head, 0,
										  {blkl},
										  MC_DISTR_POS (GCLAUSE (neg, nil),
												[andl],
												jl)
										  )
								 | blkl in set blkls
								 val andl =
								     append [[Qi $ [xi]
									     | Qi in set blk]
									    || blk in list blkl
									    and xi in list l]
								 val SOME jl =
								     SOME [(case chs newhead of
										SOME j => j
									      | NONE => raise ModelCheckFailEvt)
									  | newhead in list andl]
								     handle ModelCheckFailEvt => NONE
								 end
							     end
						    else NONE
						end
				       else NONE
				     | _ => NONE
				       )
				  )
	    in
		chs
	    end

	fun check_simple (history, c as GCLAUSE (neg, pos))
	    : ''_var mc_justif option =
	    some
	      j
	    | head in list pos
	    val SOME j = check_horn_simple (history, neg) head
	    end

	val normalized_r = table ()
	    : (''_var gclause, ''_var gclause * (''_var -m> ''_var)) table
	val n_get = t_get normalized_r
	val n_put = t_put normalized_r
	fun normalize_clause c =
	    (case n_get c of
		 SOME c_sigma => c_sigma
	       | NONE =>
		 let val (c', sigma) =
			 case c of
			     GCLAUSE (nil, nil) => (c, {})
			   | GCLAUSE (neg, pos) =>
			     let val neg' = term_sort {A | A in list neg}
				 val pos' = term_sort {A | A in list pos}
				 val (vars_pos, done_pos) = list_vars (pos', nil, {})
				 val (vars_neg, _) = list_vars (neg', vars_pos, done_pos)
				 val vars = rev vars_neg
				 val cntr = ref 0
				 val sigma = {x => (inc cntr; xgen (!cntr))
					     | x in list vars}
				 fun norm_subst (V x) =
				     if x inset sigma
					 then V (?sigma x)
				     else V x
				   | norm_subst (f $ l) =
				     f $ [norm_subst t | t in list l]
			     in
				 (GCLAUSE ([norm_subst A | A in list neg'],
					     [norm_subst A | A in list pos']),
				  sigma)
			     (* so that c sigma ~ c',
			      where ~ is propositional equivalence. *)
			     end
		 in
		     (* memoize, while ensuring that normalize_clause
		      is idempotent. *)
		     case n_get c' of
			 SOME (c'', sigma') =>
			 (* so c' sigma' ~ c'';
			  since c sigma ~ c',
			  we have c sigma sigma' ~ c''. *)
			 let val sigmasigma' =
				 {x => if y inset sigma'
					   then ?sigma' y
				       else y
				 | x => y in map sigma}
			     val res = (c'', sigmasigma')
			 in
			     n_put (c, res);
			     res
			 end
		       | NONE =>
			 let val res = (c', sigma)
			 in
			     n_put (c', (c', {}));
			     n_put (c, res);
			     res
			 end
		 end);

	fun gclause_from_eps (negs, poss) : ''_var gclause =
	    (* produce normalized gclause directly
	     from epsilon clause. *)
	    let val Xl = [V (xgen 1)]
		val c = GCLAUSE (term_sort {P $ Xl | P in set negs},
				 term_sort {Q $ Xl | Q in set poss})
	    in
		case n_get c of
		    SOME (c', sigma) => c'
		  | NONE => (n_put (c, (c, {}));
			     c)
	    end

	memofun check_univ_or pos =
		case xfsig of
		    SOME fsig => check_explicit_univ (a, fsig, pos)
		  | _ => NONE

	fun find_necessary_qs qs =
	    case check_univ_or qs of
		SOME info =>
		(case some res
		      | q in set qs
		      val SOME res = find_necessary_qs (qs \ {q})
		      end of
		     (res as SOME _) => res
		   | NONE => SOME (info, qs)
		     )
	      | NONE => NONE

	val necessary_qs = delay (find_necessary_qs qs)

	fun find_some_case_analysis (GCLAUSE (neg, pos)) =
	    (* Try to find a variable x free in pos but not
	     in neg, so that we can replace model-checking
	     -neg \/ +pos by model-checking the clauses
	     -neg \/ -Pi(x) \/ +pos, 1<=i<= n,
	     where we know that +P1(x) \/ ... \/ +Pn(x)
	     holds, through necessary_qs. *)
	    case force necessary_qs of
		SOME res =>
		let val candidate_vars =
			union {tvars a | a in list pos}
			\ union {tvars a | a in list neg}
		in
		    case candidate_vars of
			{x, ...} => SOME (res, x)
		      | _ => NONE
		end
	      | NONE => NONE

	memofun rec_ground_term (q, f $ l) =
		(* is f $ l recognized at state q? *)
		q inset univ orelse
		q inset auto andalso
		let val fmap = ?auto q
		in
		    f inset fmap andalso
		    exists
		      all
			all
			  rec_ground_term (q', t)
			| q' in set blk
			end
		      || t in list l and blk in list blkl
		      end
		    | blkl in set #1 (?fmap f)
		    end
		end
	      | rec_ground_term arg = true;

	val ground_terms = table () : (string, ''_var term option) table
	val gt_get = t_get ground_terms
	val gt_put = t_put ground_terms

	val some_constant = delay (case xfsig of
				       SOME fsig =>
				       some
					 a
				       | a => 0 in map fsig
				       end
				     | NONE => SOME "*"
				       (* dummy, we don't care here. *)
				       )
	fun find_rec_ground_term_simple q =
	    (* find some term recognized at q; we
	     assume q is not in univ. *)
	    case gt_get q of
		SOME (res as SOME _) => res
	      | SOME NONE => (* loop *) NONE
	      | NONE =>
		if q inset auto
		    then (gt_put (q, NONE);
			  let val res =
				  some
				    t
				  | f => (blkls, ...) in map ?auto q
				  val SOME t =
				      some
					f $ l
				      | blkl in set blkls
				      val SOME l =
					  find_rec_ground_term_list blkl
				      end
				  end
			  in
			      case res of
				  SOME t => (gt_put (q, res);
					     res)
				| NONE => NONE
			  end
			  )
		else NONE
	and find_rec_ground_term_list nil = SOME nil
	  | find_rec_ground_term_list ({}::blkl) =
	    (case force some_constant of
		 SOME a =>
		 (case find_rec_ground_term_list blkl of
		      SOME l => SOME ((a $ nil) :: l)
		    | NONE => NONE)
	       | NONE => NONE)
	  | find_rec_ground_term_list (({q} U rest)::blkl) =
	    (case find_rec_ground_term_simple q of
		 SOME t =>
		 if all rec_ground_term (q', t) | q' in set rest end
		     then case find_rec_ground_term_list blkl of
			      SOME l => SOME (t::l)
			    | NONE => NONE
		 else NONE
	       | NONE => NONE)

	fun find_rec_ground_terms neg =
	    let val splits = g_split_1 (neg, nil, {})
		val blkl = [blk | _ => (blk, _) in map splits]
	    in
		case find_rec_ground_term_list blkl of
		    SOME l => SOME {x => t
				   || x => _ in map splits
				   and t in list l}
		  | NONE => NONE
	    end

	fun check_for_counterexample (GCLAUSE (neg, pos)) =
	    (* We assume neg contains only atoms of the form
	     Pi (xi) --- no function symbol.
	     Then we find a canonical substitution sigma that
	     will satisfy all Pi(xi), and check whether pos sigma
	     is false, i.e., whether all atoms in pos sigma
	     are false.
	     If so, we return SOME sigma:
	     the clause cannot be true in the model.
	     *)
	    (case find_rec_ground_terms neg of
		 SOME sigma =>
		 let val subst = tsubst sigma
		 in
		     if not
			 exists
			   (case l of
				[t] => rec_ground_term (q, subst t)
			      | _ => true (* don't know *)
				)
			 | q $ l in list pos
			 end
			 then SOME sigma
		     else NONE
		 end
	       | NONE => NONE)

(*!!! insert new functions here *)

	val doner = table () : (''_var gclause,
				epsilon_gclause set -m>
				''_var mc_justif option) table
	val d_get = t_get doner
	val d_put = t_put doner
	fun find_done (c, history) =
	    (* may return:
	     SOME (SOME (j,history')): already done, with success;
	     SOME NONE: already done, same history, but failed;
	     NONE: not done yet. *)
	    (case d_get c of
		 SOME hs =>
		 let val found_exact =
			 if history inset hs
			     then case ?hs history of
				      SOME j =>
				      SOME (SOME (j,history))
				    | NONE =>
				      SOME NONE (* cannot be done ever *)
			 else NONE (* not done yet *)
		 in
		     case found_exact of
			 NONE =>
			 some
			   SOME (j, history')
			 | history' => SOME j in map hs
			     such that history' subset history
			 end
		       | _ => found_exact
		 end
	       | _ => NONE)

	    (*
	    if c inset !doner
		then let val hs = ?(!doner) c
			 val found_exact =
			     if history inset hs
				 then case ?hs history of
					  SOME j =>
					  SOME (SOME (j,history))
					| NONE =>
					  SOME NONE (* cannot be done ever *)
			     else NONE (* not done yet *)
		     in
			 case found_exact of
			     NONE =>
			     some
			       SOME (j, history')
			     | history' => SOME j in map hs
				 such that history' subset history
			     end
			   | _ => found_exact
		     end
	    else NONE
		*)
	fun add_done (c,history,res) =
	    (case d_get c of
		 SOME hs => d_put (c, hs ++ {history => res})
	       | _ => d_put (c, {history => res}))
	    (*
	    if c inset !doner
		then doner := !doner ++ {c => ?(!doner) c ++ {history => res}}
	    else doner := !doner ++ {c => {history => res}}
	     *)

	val edoner = table ()
	    : (epsilon_gclause, epsilon_gclause set -m>
	       ''_var mc_justif) table
	val ed_get = t_get edoner
	val ed_put = t_put edoner
	fun find_edone (epsc,history) =
	    (* as find_done, for epsilon clauses,
	     using edoner instead of doner, and
	     restricted to the found_exact case.
	     Returns either:
	     SOME j: already done, with success
	     NONE: already done, but failed, or not done yet.
	     *)
	    (case ed_get epsc of
		 SOME hs =>
		 let val found_exact =
			 if history inset hs
			     then SOME (?hs history)
			 else NONE (* not done yet *)
		 in
		     case found_exact of
			 NONE =>
			 some
			   (j, history')
			 | history' => j in map hs
			     such that history' subset history
			 end
		       | SOME j => SOME (j, history)
		 end
	       | NONE => NONE)
	fun add_edone (epsc,history,SOME j) =
	    (case ed_get epsc of
		 SOME hs =>
		 ed_put (epsc, hs ++ {history => j})
	       | NONE =>
		 ed_put (epsc, {history => j}))
	  | add_edone _ = () (* do not add anything if res=NONE. *)

	memofun mc_actual_history (MC_TAUTO _) = {}
	      | mc_actual_history (MC_CUT_HISTORY (_, j)) =
		mc_actual_history j (* should equal the first
				     argument to MC_CUT_HISTORY. *)
	      | mc_actual_history (MC_NORMALIZE (_, _, j)) =
		mc_actual_history j
	      | mc_actual_history (MC_SUBSUMED_UNIV _) = {}
(*
	      | mc_actual_history (MC_SUBSUMED_AUTO _) = {}
*)
	      | mc_actual_history (MC_SUBSUMED_HISTORY (_, epsc, ...)) =
		{epsc}
	      | mc_actual_history (MC_SUBSUMED_EPSC (_,_,j)) =
		mc_actual_history j
	      | mc_actual_history (MC_ELIM_UNIV_NEG (c,P,i,j)) =
		mc_actual_history j
	      | mc_actual_history (MC_ELIM_NEG (c,_,k,sigma,jl)) =
		union {mc_actual_history j | j in list jl}
	      | mc_actual_history (MC_ELIM_EPSILON_NEG (_, _, qjl)) =
		union {mc_actual_history j | (_, j) in list qjl}
	      | mc_actual_history (MC_DEDUCE_POS (c,_,i,blkls,j)) =
		mc_actual_history j
	      | mc_actual_history (MC_DISTR_POS (c,orandl,jl)) =
		union {mc_actual_history j | j in list jl}
	      | mc_actual_history (MC_SUBSUMED_SUPER (c,orandl,j)) =
		mc_actual_history j
	      | mc_actual_history (MC_SUBSUMED (c,j)) =
		mc_actual_history j
	      | mc_actual_history (MC_SPLIT (c,j)) =
		mc_actual_history j
	      | mc_actual_history (MC_EXPLICIT_UNIV _) = {}
	      | mc_actual_history (MC_VS _) = {}
(* OBSOLETE
	      | mc_actual_history (MC_VS_NEG1 _) = {}
*)
	      | mc_actual_history (MC_CUT (_, j, jal)) =
		mc_actual_history j U
		union {mc_actual_history ji | (ji, _) in list jal}
	      | mc_actual_history (MC_INDUCT (_,epsc,_,jl)) =
		union {mc_actual_history j | (_, _, j) in list jl}
		\ {epsc}
	      | mc_actual_history _ = raise McActualHistory

	fun find_done_subsumer (c, history) =
	    some
	      (j, history', t)
	    | t => epscs in map find_epsc_subsumers c
	    val SOME (j, history') =
		some
		  jh
		| epsc in set epscs
		val SOME jh = find_edone (epsc,history)
		end
	    end

	fun check_gclause (c, history) : ''_var mc_justif option =
	    let val (c', sigma) = normalize_clause c
	    in
		if c=c'
		    then (* clause c is normalized *)
			case find_done (c, history) of
			    SOME (SOME (j, history'))
			    => SOME (if history=history'
					 then j
				     else MC_CUT_HISTORY (history', j))
			  | SOME NONE => NONE
			  | NONE =>
			    (case find_done_subsumer (c, history) of
				 SOME (j, history', t) =>
				 (* where c' is an epsilon clause
				  justified by j in history',
				  and c'{X1:=t} is a subclause of c. *)
				 let val j' = mc_subsumed_epsc (c,t,j)
				 in
				     SOME (if history=history'
					       then j'
					   else MC_CUT_HISTORY (history', j'))
				 end
			       | NONE =>
				 let val res =
					 check_gclause_horn (c, history)
				 in
				     add_done (c,history,res);
				     res
				 end)
		else case check_gclause (c', history) of
			 SOME j => SOME (MC_NORMALIZE (c, sigma, j))
		       | NONE => NONE
	    end
	and check_gclause_horn (c as GCLAUSE (neg, pos as [_, _, ...]),
				history) =
	    (* if c is non-Horn, try to check Horn clauses that imply it.
	     This is unnecessary for completeness, but should provide shorter
	     justifications. *)
	    (case some res
		  | a in list pos
		    val SOME res = check_gclause (GCLAUSE (neg, [a]), history)
		  end of
		  SOME j => SOME (MC_SUBSUMED (c, j))
	       | _ => check_gclause_1 (c, history))
	  | check_gclause_horn (c,history) = check_gclause_1 (c,history)
	and check_gclause_1 (c, history) =
	    (case check_simple (history, c) of
		 SOME j => SOME j
	       | _ => 
	    (case find_history_subsumer (history, c) of
		 SOME (epsc, t) =>
		 SOME (MC_SUBSUMED_HISTORY (c, epsc, t))
	       | _ =>
	    (case find_neg_univ c of
		 SOME (P, i) =>
		 (let val j =
			  check_gclause_exc (resolve_neg_univ (c, P),
					     history)
		  in
		      SOME (MC_ELIM_UNIV_NEG (c, P, i, j))
		  end handle ModelCheckFailEvt => NONE)
	       | _ =>
	    (* Before we continue and test for more complicated rules,
	     let us try to see whether there are two atoms P(X), Q(X)
	     in the body of c such that false :- P(X), Q(X) would
	     be easily provable, or whether there are two atoms
	     P(t), Q(t) with t non-variable such that false :- P(X), Q(X)
	     would be easily provable---without using any induction hypothesis
	     this time.
	     *)
	    (case find_neg_empty_inter (history, c) of
		 SOME j =>
		 (
(*
#put stderr "Found neg empty inter!\n";
#flush stderr ();
*)
		  SOME j
)
	       | _ =>
	    (case gclause_split c of
		 SOME cl =>
(
(*
#put stderr "\n*** split ";
perr_gclause c;
#put stderr " => ";
iterate
  (#put stderr " + ";
  perr_gclause c')
| c' in list cl
end;
#flush stderr ();
*)
		 some
		   MC_SPLIT (c, j)
		 | c' in list cl
		 val SOME j = check_gclause (c', history)
		 end
)
	       | NONE =>
	    (do_verbose (3, fn () =>
			 (#put stderr "\n";
			  perr_bars (card history);
			  #put stderr " >";
			  perr_gclause c;
			  #flush stderr ()));
	     case find_non_var_neg_atom c of
		 SOME (a as P $ [f $ args], l, i) =>
		 (let val ir = ref 0
		      val sigma = {(inc ir; !ir) => t
				  | t in list args}
		      val auto_elim =
			  if P inset auto
			      then let val fmap = ?auto P
				   in
				       if f inset fmap
					   then let val (blkls, ...) = ?fmap f
						in
						    [check_gclause_exc
						     (resolve_auto_neg (c, l,
									blkl,
									sigma),
						      history)
						    | blkl in set blkls]
						end
				       else nil
				   end
			  else nil
		      val elim =
			  if P inset univ (* !!!useless, since
					   MC_ELIM_UNIV_NEG was
					   tested above. *)
			      then check_gclause_exc (resolve_univ_neg (c, l),
						      history)
				  :: auto_elim
			  else auto_elim
		  in
		      SOME (MC_ELIM_NEG (c, a, len args, sigma, elim))
		  end handle ModelCheckFailEvt => NONE)
	       | _ => 
	    (* Now c only has negative atoms of the form -Pi(xi). *)
	    (case check_for_counterexample c of
		 SOME sigma =>
		 (* So c is false, because c sigma is false.
		  We refuse to model-check it.
		  In case the history is empty, this is clear: c is false.
		  Otherwise, it might be that c is still entailed
		  by the induction hypotheses h1, ..., hn in the history.
		  But then, one of these induction hypotheses hi must be wrong.
		  And this hi was introduced in the course of proving
		  hi under induction hypotheses h1, ..., h{i-1}.
		  Since hi is wrong either this goal of proving hi will
		  fail, or, some hj with j<i must be false too.
		  Recursing over i > j > ..., we must conclude that there
		  is some hj (with j minimal) that we were trying
		  to prove under induction hypotheses h1, ..., h{j-1},
		  and such that this must fail.
		  So we fail now. *)
		 (do_verbose (3, fn () =>
			      let val |[perr_gclause, perr_sigma, ...]| =
				      perr_funs ()
			      in
				  #put stderr "\n";
				  perr_bars (card history);
				  #put stderr " ";
				  perr_gclause c;
				  #put stderr " is false: quit";
				  perr_sigma (" [", "]", sigma);
				  #put stderr ".";
				  #flush stderr ()
			      end);
		  NONE)
	       | _ =>
(* OBSOLETE
	    (case pos_value_checker c of
		 SOME (t, vcj, rho, sm) =>
		 SOME (MC_VS_NEG1 (c, t, vcj, sm, rho))
	       | _ => 
*)
	    (case find_neg_epsilon_atom c of
		 SOME (P, l, qs, left, right, pos) =>
		 (SOME (MC_ELIM_EPSILON_NEG (c, P $ l,
					     [(q,
					       check_gclause_exc (GCLAUSE (revappend (left, (q $ l) :: right),
									   pos),
								  history))
					     | q in set qs]))
		  handle ModelCheckFailEvt => NONE)
	       | _ =>
	    (case find_some_case_analysis c of
		 SOME ((info, qs), x) =>
		 let val GCLAUSE (neg, pos) = c
		 in
		     do_verbose (3, fn () =>
				 (#put stderr "\n";
				  perr_bars (card history);
				  #put stderr " case analysis: ";
				  perr_gclause (GCLAUSE (nil,
							 [q $ [V x]
							 | q in set qs]));
				  #flush stderr ()));
		     SOME (MC_CUT (c,
				   MC_EXPLICIT_UNIV (x, qs, info),
				   [(check_gclause_exc (GCLAUSE (a::neg, pos),
							history),
				     a)
				   | q in set qs
				       val a = q $ [V x]]))
		     handle ModelCheckEvt => NONE
		 end
	       | _ => 
	    (case find_non_var_pos_atom c of
		 SOME (a as (P $ [f $ args]), l, i, _) =>
		 ((if P inset auto (* no need to check univ,
				    since c is not subsumed. *)
		       then let val fmap = ?auto P
			    in
				if f inset fmap
				    then let val (blkls, k, vars) = ?fmap f
					     val ir = ref 0
					     val sigma = {(inc ir; !ir) => t
							 | t in list args}
					     val sc = resolve_auto_pos
						 (c, l, blkls, sigma)
					     val j = check_superclause (sc, history)
					 in
					     SOME (MC_DEDUCE_POS
						   (c, a, i, blkls, j))
					 end
				else let val sc = (resolve_univ_pos (c, l), nil)
					 val j = check_superclause (sc, history)
				     in
					 SOME (MC_DEDUCE_POS (c, a, i, {}, j))
				     end
			    end
		   else let val sc = (resolve_univ_pos (c, l), nil)
			    val j = check_superclause (sc, history)
			in
			    SOME (MC_DEDUCE_POS (c, a, i, {}, j))
			end)
		      handle ModelCheckFailEvt => NONE)
	       | _ =>
	    (* Now c only contains atoms +-P(x) for some variables x. *)
		 some
		   MC_SPLIT (c, j)
		 | (x, epsc) in list g_split_sort c
		 (* we have to find an epsc that is non positive;
		  with h1, where we can check whether the model
		  satisfies all formulae *whatever* the first-order
		  signature, positive epsilon clauses cannot be fulfilled,
		  unless they are subsumed by some universal clause:
		  we would then write:
		  | x => (epsc as ({P, ...}, _)) in map g_split c
		  Note that P is not universal either at this point. *)
		 val SOME j =
		     check_eps_clause (x, epsc, history)
		 end
		 ))))))))))
	and check_superclause ((c, nil), history) =
	    check_gclause_exc (c, history)
	  | check_superclause (inp as ((c, orandl), history)) =
	    (* check superclause c \/ orandl,
	     where orandl is a disjunction [list]
	     of conjunctions [list] of positive atoms. *)
	    (* The general case consists in distributing
	     all disjunctions over all conjunctions,
	     and calling check_gclause on each resulting conjunct.
	     This is grossly inefficient...
	     so first, we eliminate disjuncts that are just false
	     for simple reasons, i.e., because they are of the
	     form ... \/ P1(X) \/ P2(X) but one can prove
	     that false :- P1(X), P2(X). *)
	    let val orandl' = [andl
			      | andl in list orandl
				  such that find_neg_empty_inter (history,
							    GCLAUSE (andl, nil))
				      <> NONE]
	    in
		(* Then, we check each disjunct separately, in case one
		 holds. *)
		case orandl' of
		    [_, _, ...] =>
		    (case some res
			  | andl in list orandl'
			  val SOME res =
			      (SOME (check_superclause_1 ((c, [andl]), history))
			       handle ModelCheckFailEvt => NONE)
			  end of
			 SOME j =>
			 MC_SUBSUMED_SUPER (c, orandl', j)
		       | _ => check_superclause_1 inp)
		  | _ => check_superclause_1 inp
	    end
	and check_superclause_1 ((c, orandl), history) =
	    let val jl = [check_gclause_exc (c', history)
			 | c' in set g_from_superclause (c, orandl)]
	    in
		MC_DISTR_POS (c, orandl, filter_distr_justif jl)
	    end
	and check_gclause_exc (c,history) =
	    case check_gclause (c,history) of
		SOME j => j
	      | _ => raise ModelCheckFailEvt
	    (* check_eps_clause is theoretically unnecessary, and we might call
	     check_eps_clause_gnrl, but doing so allows us to get shorter justifications. *)
	and check_eps_clause (x, epsc, history) =
	    let val res = check_eps_clause_gnrl (x, epsc, history)
		val history' = case res of
				   SOME j => mc_actual_history j
				 | NONE => history
	    in
		epsdoner := epssub_add epsc (!epsdoner);
		add_edone (epsc, history', res);
		if history=history'
		    then res
		else case res of
			 SOME j => SOME (MC_CUT_HISTORY (history', j))
		       | NONE => NONE
	    end
	and check_eps_clause_gnrl (x : ''_var,
				   epsc as (neg, pos), history) =
	    if empty neg
		then case xfsig of
			 NONE => NONE (* check must fail, provided signature
				       is extensible *)
		       | SOME fsig =>
			 let val new_history = history U {epsc}
			 in
			     case check_univ_or pos of
				 SOME info =>
				 SOME (MC_EXPLICIT_UNIV (x, pos, info))
			       | NONE => 
			     (do_verbose (2, fn () =>
					  (#put stderr "\n";
					   perr_bars (card history);
					   #put stderr " ?";
					   perr_eps_clause epsc;
					   #flush stderr ()));
			      (SOME (MC_INDUCT (x, epsc, NONE,
						[(f, k, j)
						| f => k in map fsig
						    val ir = ref 0
						    val xl = [V (xgen (inc ir; !ir))
							     |while !ir<k]
						    val c = g_from_eps_clause (f $ xl, neg, pos)
						    val j = check_gclause_exc (c, new_history)]))
			       before do_verbose (2, fn () =>
						  (#put stderr "\n";
						   perr_bars (card history);
						   #put stderr " OK.";
						   #flush stderr ()))
			       )
			      handle ModelCheckFailEvt =>
			      (do_verbose (2, fn () =>
					   (#put stderr "\n";
					    perr_bars (card history);
					    #put stderr " No.";
					    #flush stderr ()));
			       NONE))
			 end
	    else
	    (do_verbose (2, fn () =>
			 (#put stderr "\n";
			  perr_bars (card history);
			  #put stderr " ?";
			  perr_eps_clause epsc;
			  #flush stderr ()));
	     let val P = find_var_lit neg
		 val fmap = P_auto P
		 val new_history = history U {epsc}
	     in (* resolve with all possible clauses P(f(x1,...,xk)) <= body: *)
		 (SOME (MC_INDUCT (x, epsc, SOME P,
				   [(f, k, j)
				   | f => (blkls, k, vars) in map fmap
				       val ir = ref 0
				       val xl = [V (xgen (inc ir; !ir)) |while !ir<k]
				       val c = g_from_eps_clause (f $ xl, neg, pos)
				       val j = check_gclause_exc (c, new_history)]
				   ))
		  before do_verbose (2, fn () =>
				     (#put stderr "\n";
				      perr_bars (card history);
				      #put stderr " OK.";
				      #flush stderr ()))
		  )
		 handle ModelCheckFailEvt =>
		 (do_verbose (2, fn () =>
			      (#put stderr "\n";
			       perr_bars (card history);
			       #put stderr " No.";
			       #flush stderr ()));
		  NONE)
	     end)
	  | check_eps_clause_gnrl _ = raise CheckEpsClause
    in
	|[mc = fn c => check_gclause (c, {}),
	  reset = fn () => (epsdoner := ESEmpty; t_reset doner)
	  ]|
    end;

fun justif_has_gclause (MC_CUT_HISTORY (_, j)) =
    justif_has_gclause j
  | justif_has_gclause (MC_DISTR_POS _) = false
  | justif_has_gclause (MC_SUBSUMED_SUPER _) = false
  | justif_has_gclause _ = true;
