(* h1fi finite model finder engine.
   Copyright (C) 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.
*)

open "h1ficc_h";
open "rel_h";
open "verbose_h";
open "gensym_h";

(* Find finite models, in the form:
 - domains D is a sub-term closed finite set of terms;
 - this is equipped with a ground equational theory,
   represented using congruence closure, as a convergent
   rewrite system on D; (we call color any normal term in D)
 - semantics is given by:
   * set of values is D union a special constant bot;
   * the value of f(d1,...,dn) is its color if
     f(d1,...,dn) is in D, bot otherwise;
   * equal(d,d') iff d and d' are the same color exactly (in D);
     so equal is not reflexive, since equal(bot,bot) is false.
   * P(d1,...,dn) holds iff it is equal to (the color of)
     true, a special constant assumed to be in D,
     where P is not "equal".  In particular, if any of
     d1, ..., dn is bot, then P(d1,...,dn) is false.
*)

fun herbrand_policy (cc, eq) (gc,a,rho) = ();

exception PolicyArityErr of string * int * int;

exception PredPolicy;

fun make_pred_policy (special_var : ''_var -> bool) =
    let val pred_store = table ()
	    : (string * ''_var cenv, ''_var term list) table
	val hget = t_get pred_store
	val hput = t_put pred_store
	fun pred_policy (cc,eq) (gc,P $ ul, rho) =
	    let val special_rho = {x => c | x => c in map rho
					      such that special_var x}
		val subst = tsubst rho
		val ul' = [subst u | u in list ul]
	    in
		case hget (P, special_rho) of
		    SOME vl =>
		    (iterate
		       eq (u,v,rho)
		     || u in list ul' and v in list vl
		     end handle ParSweep =>
		       raise PolicyArityErr (P, len ul, len vl))
		  | _ => hput ((P,special_rho), ul')
	    end
	  | pred_policy (cc,eq) (gc,a,rho) = raise PredPolicy
    in
	pred_policy
    end;

exception HeamPolicy;

fun make_heam_policy (special_var : ''_var -> bool) =
    let val heam_store = table ()
	    : (''_var gclause * string * ''_var cenv, ''_var term list) table
	val hget = t_get heam_store
	val hput = t_put heam_store
	fun heam_policy (cc,eq) (gc,P $ ul, rho) =
	    let val special_rho = {x => c | x => c in map rho
					      such that special_var x}
		val subst = tsubst rho
		val ul' = [subst u | u in list ul]
	    in
		case hget (gc, P, special_rho) of
		    SOME vl =>
		    (iterate
		       eq (u,v,rho)
		     || u in list ul' and v in list vl
		     end handle ParSweep =>
		       raise PolicyArityErr (P, len ul, len vl))
		  | _ => hput ((gc,P,special_rho), ul')
	    end
	  | heam_policy (cc,eq) (gc,a,rho) = raise HeamPolicy
    in
	heam_policy
    end;

(* given two sets of variable environments rhos and rhos',
 build set of environments r that are compatible unions
 of environments from rhos and rhos'. *)
fun env_and (rhos, rhos') =
    {rho ++ rho'
    | rho in set rhos and rho' in set rhos'
      such that rho <| rho' = rho' <| rho};

fun forcers (cc as |[universe, colors, find, equate,
		     (* set_varnames, *)
		     ... ]|,
	     policy, vars) =
    let memofun forcetv (V x, d) = {{x => d}}
	      | forcetv ("equal" $ [u,v], _) =
		(* force "u=v" to be true; one cannot force
		 an atom to be anything else but true.
		 *)
		union {env_and (forcetv (u, d),
				forcetv (v, d))
		      | d in set colors ()}
	      (* U env_and (forcebot u, forcebot v) *)
	      | forcetv (f $ tl, d) =
		let val colormap = colors ()
		in
		    if d inset colormap
			then let val ts = ?colormap d
				 val donedlr = ref {}
				 val unv = universe ()
			     in
				 union {
					let val dl = [?unv t | t in list tl']
					in
					    if dl inset !donedlr
						then {}
					    else (donedlr := !donedlr U {dl};
						  forcetvl (tl, dl))
					end
				       | f' $ tl' in set ts
					   such that f=f'}
			     end
		    else {}
		end
	and forcetvl (nil, _) = {{}}
	  | forcetvl (t::tl, d::dl) =
	    env_and (forcetv (t,d), forcetvl (tl,dl))

	(* equate_under_rho assumes clauses are in range-restricted form *)
	fun equate_under_rho (u, v, rho) =
	    let val subst = tsubst rho
		val u' = subst u
		val v' = subst v
	    in
		if find u'=find v'
		    then false
		else (do_verbose (1,
			    fn () =>
			       (#put stderr "Force ";
				print_term (stderr, vars) u';
				#put stderr "=";
				print_term (stderr, vars) v';
				#put stderr ".\n";
				#flush stderr ())
			       );
		      equate (u', v');
		      true)
	    end

	val p = policy (cc, equate_under_rho)
	val truet = "$true" $ nil

	fun force_gclause (gc as GCLAUSE (negs, poss)) =
	    let val truec = find (truet)
		fun force_atoms_true nil = {{}}
		  | force_atoms_true (a::al) =
		    env_and (forcetv (a, truec),
			     force_atoms_true al)
		val rhos = force_atoms_true negs
		val colormap = {truec} <-| colors ()
		    (* only "honest" colors, i.e., not of predicates
		     found true. *)
		fun all_extend_rhos (a, rho, do_rho) =
		    let fun aller ({}, rho) = do_rho rho
			  | aller ({x} U rest, rho) =
			    iterate
			      aller (rest, rho ++ {x => c})
			    | c in set colormap
			    end
		    in
			aller (tvars a, rho)
		    end
	    in
		if empty rhos
		    then () (* body is always false, hence clause is always true *)
		else case poss of
			 nil => raise ForceContradictionEvt
		       | [a as ("equal" $ [u,v])] =>
			 iterate
			   all_extend_rhos (a, rho,
					    fn rho =>
					       if equate_under_rho (u,v,rho)
						   then (equate_under_rho
							 (a,truet, rho);
							 ())
					       else () (* don't do anything
							more when u rho
							already equals v rho *)
						   )
			 | rho in set rhos
			 end
		       | [a] =>
			 iterate
			   all_extend_rhos (a, rho,
					    fn rho =>
					       if equate_under_rho
						   (a,truet,rho)
						   then p (gc,a,rho)
					       else () (* don't do anything
							more when u rho
							already equals v rho *)
						   )
			 | rho in set rhos
			 end
		       | _ => raise ForceNonHornEvt
	    end
     in
(*
set_varnames vars;
*)
	|[force_term_value = forcetv,
	  force_gclause = force_gclause
	  ]|
    end;

fun auto_fmap_union {} = {}
  | auto_fmap_union {fmap} = fmap
  | auto_fmap_union fmaps =
    let val (fmaps1, fmaps2) = split fmaps
	val fmap1 = auto_fmap_union fmaps1
	val fmap2 = auto_fmap_union fmaps2
    in
	(fmap1 delta fmap2) ++
	{f => (blkls1 U #1 (?fmap2 f), k, ks)
	| f => (blkls1, k, ks) in map fmap2 <| fmap1}
    end;

fun auto_from_cc (|[colors, find, ...]|, q) =
    let val truet = "$true" $ nil
	val truec = find (truet)
	(* we now create a fresh state for each color in the universe,
	 except truec. *)
	val colormap = colors ()
	memofun qname c = gensym q
	val auto = {qname c =>
		    let val funcs = {f => len l | f $ l in set ts}
		    in
			{f =>
			 ({[{qname (find t)}
			   | t in list l]
			  | g $ l in set ts
			      such that g=f},
			    k,
			    1 to k)
			| f => k in map funcs}
		    end
		   | c => ts in map colormap
		     such that c<>truec}
	val preds = if truec inset colormap
			then let val trueatoms = ?colormap truec
				 val preds = {P => len l
					     | P $ l in set trueatoms}
			     in
				 {P =>
				  if k=1
				      then auto_fmap_union
					  {let val q = qname (find t)
					   in
					       if q inset auto
						   then ?auto q
					       else {}
					   end
					  | Q $ [t] in set trueatoms
					      such that Q=P}
				  else
				      {"#" ^ P => ({[{qname (find t)}
						    | t in list tl]
						   | Q $ tl in set trueatoms
						     such that Q=P},
						   k, 1 to k)}
				 | P => k in map preds
				   such that P<>"$true"}
			     end
		    else {}
	val untrimmed = auto ++ preds
	val used_states = union {union {union {union (elems blkl)
					      | blkl in set blkls}
				       | f => (blkls, ...) in map fmap}
				| P => fmap in map untrimmed}
    in
	AUTO ((used_states <| auto) ++ preds, {})
    end;
