(* Model-checking functions, headers.
   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 "auto_h";
open "gclause_h";

type epsilon_gclause = string set * string set;

datatype simple_model = SM of
	 (string -m> int) (* map each state (not each predicate,
			   just those that occur in bodies of automaton
			   clauses) to values, which are simply numbered
			   from 1 to k.  The special value 0 is meant
			   to denote undefined. *)
	 * (string -m> int list -m> int)
	 (* map function symbols (except those with an empty table)
	  to their tables; the undefined value 0 is never mentioned. *)
	 ;

(* OBSOLETE
datatype vc_justif = VC_NO (* proves that any closed term with value i
			    satisfies predicate P. *)
       | VC_IND_HYP of int * string (* Here we have got an induction hypothesis (i,P). *)
       | VC_CUT_HISTORY of (int * string) set * vc_justif
	 (* We need only the induction hypotheses in the first argument. *)
       | VC_UNIV of int * string (* (i,P) holds because P is universal. *)
       | VC_INDUCT of (int * string)
	 * (string -m> int list -m>
	    (string * string * block list) * vc_justif list list)
	 ;
*)

datatype ''var mc_justif =
	 MC_TAUTO of ''var gclause * int
	 (* MC_TAUTO (c, i): clause c is a tautology,
	  positive atom number i also occurs negatively. *)
       | MC_CUT_HISTORY of epsilon_gclause set * ''var mc_justif
	 (* prove same clause in smaller history *)
       | MC_NORMALIZE of ''var gclause * (''var -m> ''var)
	 * ''var mc_justif
	 (* MC_NORMALIZE (c, sigma, j): sigma is a renaming,
	  and c sigma is propositionally equivalent to c',
	  where j is a justification for c'. *)
       | MC_SUBSUMED_UNIV of ''var gclause * string * int
	 (* MC_SUBSUMED_UNIV (c, P, i): clause c is subsumed
	  by clause +P(x), and positive atom number i is +P(t)
	  for some t. *)
(* Obsolete:
       | MC_SUBSUMED_AUTO of ''var gclause *
	 string * string * int * (int -m> ''var term) * block list * int
	 (* MC_SUBSUMED_AUTO (c, P, f, k, sigma, blkl, i):
	  clause c is subsumed by automaton clause
	  P(f(x1,...,xk)) <= blkl,
	  with substitution sigma (of domain x1, ..., xk);
	  head instantitates to positive atom number i of c. *)
*)
       | MC_SUBSUMED_HISTORY of ''var gclause * epsilon_gclause * ''var term
	 (* MC_SUBSUMED_HISTORY (c, epsc, t):
	  clause c is subsumed by epsilon clause epsc in history
	  (introduced by some MC_INDUCT above it);
	  more precisely, c contains epsc(t);
	  clause epsc=(Bneg, Bpos) is an epsilon clause -Bneg(x) \/ +Bpos(x),
	  where Bneg is not empty and contains some predicate P,
	  and epsc(t) denotes -Bneg(t) \/ +Bpos(t).
	  Moreover, t is a variable.
	  *)
       | MC_SUBSUMED_EPSC of ''var gclause * ''var term * ''var mc_justif
	 (* MC_SUBSUMED_EPSC (c, t, j):
	  clause c is of the form c'{X1:=t} \/ c'', where c' is
	  an epsilon clause justified by j. *)
       | MC_ELIM_UNIV_NEG of ''var gclause * string * int * ''var mc_justif
	 (* MC_ELIM_UNIV_NEG (c, P, i, j)
	  clause c is of the form c' \/ -P(t) for some t,
	  and where -P(t) needs not be in first position in c,
	  rather at position i;
	  j is justification of c'.
	  *)
       | MC_ELIM_NEG of ''var gclause *
	 ''var term * int * (int -m> ''var term) * ''var mc_justif list
	 (* MC_ELIM_NEG (c, P(t), k, sigma, [j1, ..., jp]):
	  clause c is of the form c' \/ -P(t), with t = f(t1,...,tk),
	  sigma = {x1 => t1, ..., xk => tk},
	  giving rise to the jp justifications obtained by resolving c
	  on -P(t) with all universal clauses +P(x) and all automaton
	  clauses of the form P(f(x1,...,xk)) <= ...
	  *)
       | MC_ELIM_EPSILON_NEG of ''var gclause *
	 ''var term * (string * ''var mc_justif) list
	 (* MC_ELIM_EPSILON_NEG (c, P(t), [(q1,j1), ..., (qp,jp)]):
	  clause c is of the form c' \/ -P(t), and we can
	  show that P(X) => q1(X) \/ ... \/ qp(X) for all X.
	  Then ji is a justification of c' \/ -qi(t).
	  *)
       | MC_DEDUCE_POS of ''var gclause *
	 ''var term * int *
	 block list set * ''var mc_justif
	 (* MC_DEDUCE_POS (c, P(t), i, blkls, j):
	  clause c is of the form c' \/ +P(t), with t = f(t1,...,tk),
	  +P(t) is positive atom number i in c,
	  j is a justification of the superclause
	  c' \/ \/_{P(f(x1,...,xk)) <= B1(x1),...,Bk(xk) in auto}
	           (B1(t1) /\ ... /\ Bk(tk)).
	  *)
       | MC_DISTR_POS of ''var gclause * ''var term list list *
	 ''var mc_justif list
	 (* MC_DISTR_POS (c, orandl, [j1, ..., jp]):
	  superclause is c \/ orandl, where orandl is a disjunction of
	  conjunctions of positive atoms (as above).  Distribute
	  disjunctions over conjunctions, and get the conjuncts: then
	  j1, ..., jp are justifications for each conjunct.
	  *)
       | MC_SUBSUMED_SUPER of ''var gclause * ''var term list list *
	 ''var mc_justif
       (* MC_SUBSUMED_SUPER (c, orandl, j)
	superclause is c \/ orandl with orandl a disjunction of
	at least two conjunctions of positive atoms.
	j justifies a superclause of the form c \/ andl,
	with andl one of the disjuncts.
	*)
       | MC_SUBSUMED of ''var gclause * ''var mc_justif
	 (* MC_SUBSUMED (c, j)
	  clause c is of the form c' \/ c'', where
	  c' is justified by j.
	  *)
       | MC_SPLIT of ''var gclause * ''var mc_justif
	 (* MC_SPLIT (c, j):
	  clause c is a disjunction of blocks (disjunctions of +-Pi(x)
	  for some variable x) B1(x1) \/ ... \/ Bk(xk),
	  and j is a justification for some Bi(xi).
	  *)
       | MC_INDUCT of ''var * epsilon_gclause * string option *
	 (string * int * ''var mc_justif) list
	 (* MC_INDUCT (x, epsc, optP, side, jl):
	  clause epsc=(Bneg, Bpos) is an epsilon clause -Bneg(x) \/ +Bpos(x),
	  where Bneg is not empty and contains some predicate P (if optP=SOME P)
	  or Bneg is empty, and optP=NONE.
	  List jl = [(f1, k1, j1), ..., (fp, kp, jp)]
	  is the list of justifications for
	  -Bneg(fi(x1,...,xki)) \/ +Bpos(fi(x1,...,xki))
	  where fi ranges over the function symbols such that
	  there is a clause P(fi(x1,...,xki)) <= ... in the automaton
	  (if optP=SOME P) or ranges over the whole signature (if optP=NONE).
	  *)
       | MC_EXPLICIT_UNIV of ''var * string set * (string -m> block list -m> string)
	 (* MC_EXPLICIT_UNIV (x, qs, info)
	  clause is an epsilon clause +qs(x).
	  info maps each f in the signature to a map sending
	  all blocks [q1(x1), ..., qn(xn)], with q1, ..., qn taken from qs,
	  to some q, such that some automaton clause
	  subsumes q(X) :- q1 (X1), ..., qn (Xn).
	  *)
       | MC_VS of ''var * string * string * simple_model
	 (* MC_VS (x,q,q',sm)
	  clause is -q(x) \/ -q'(x), stating that q and q' are disjoint.
	  sm is a simple model such that every t satisfying q
	  is mapped to a value i, every t satisfying q' is mapped to
	  a value j, and i<>j.
	  *)
(* OBSOLETE
       | MC_VS_NEG1 of ''var gclause * ''var term * vc_justif
	 * simple_model * (''var -m> int)
	 (* MC_VS_NEG1 (c, t, vcj, sm, rho)
	  clause c is of the form c- \/ +P (t) \/ c+, where c- contains
	  the negative literals of c, c+ the positive literals other
	  than +P(t),
	  where c- contains only atoms of the form Q(x) (no function
	  symbol), and where all free variables of t occur in c-.
	  Then rho maps each variable x to the unique value in
	  the model sm that makes Q(x) true (for each Q(x) in c-).
	  We then observe that the value of t in sm is i,
	  and that all terms that have value i in sm must satisfy P.
	  (So c+ holds under rho.)  This is what is proved in the
	  auxiliary proof vcj.
	  *)
*)
       | MC_CUT of ''var gclause * ''var mc_justif *
	 (''var mc_justif * ''var term) list
	 (* MC_CUT (c, j, jl)
	  clause c is of the form c0 \/ c1 \/ ... \/ cn (n>=1)
	  where c0 \/ +a1 \/ ... \/ +an is justified by j,
	  a1, ..., an are atoms,
	  and -ai \/ ci is justified by ji, where jl=[(j1,a1), ..., (jn,an)].
	  The atoms a1, ..., an are required to be pairwise distinct.
	  *)
	 ;

extern val model_check : automaton * (int -> ''_var) * (string -m> int) option ->
	   |[mc : ''_var gclause -> ''_var mc_justif option,
	     reset : unit -> unit
	     ]|;
	   (* #mc (model_check (auto, xgen, xfsig)) (c)
	    checks whether clause c is true in model described by automaton auto;
	    requires xgen to build variables (given int i, xgen i should returned some
	    predefined variable variable, such that i<>j => xgen i<>xgen j);
	    returns NONE if c is false;
	    returns SOME (j, newdone), where j is some mc_justif, otherwise.
	    xfsig is either NONE, meaning we check that clause holds in
	    model described by automaton, whatever the signature [provided
	    it extends the signature Sigma of the automaton and the clause];
	    or SOME fsig, where fsig is the signature we must use [which
	    should extend Sigma].
	    The point is that, eg, checking the clause P(X) in an
	    automaton with no univ clause and automaton clauses P(a) and P(b)
	    should: fail if xfsig=NONE (because we may always extend the
	    signature and add a constant c, so that P(c) fails), succeed
	    if xfsig=SOME {a/0,b/0}, and fail if xfsig is a larger signature.

	    #reset resets internal hash tables (to save memory).
	    *)

(* OBSOLETE
extern val vcjustif_ip : vc_justif -> int * string;
*)

extern val justif_gclause : ''var mc_justif -> ''var gclause;

extern val justif_has_gclause : ''var mc_justif -> bool;
