(* Propositional Horn satisfiability engine.
   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 "fixbool_h";

type ''a horn_clause = ''a option (* * ''a set *) * int ref;
    (* optional head (false if no head),
     (* body (set of variables), *)
     cardinality of body - number of variables in body set to true, knowing
     that the remaining variables are not set to false. *)

type ''a horn = ''a horn_clause list;

type ''a indexing = ''a -m> ''a horn ref; (* maps every variable to the set of horn
					   clauses in which it appears in the body. *)

type ''a units = ''a option list; (* set of unit clauses, waiting to be dealt with *)

type ''a valuation = ''a set; (* set of true variables *)

datatype ''a horn_set = HORN of ''a horn ref * ''a indexing ref * ''a units ref
    * ''a valuation ref;

fun new_horn_set () = HORN (ref nil, ref {}, ref nil, ref {});

fun add_horn_clause (HORN (h, i, u, ref rho), head, body) =
    case rho <-| body of
	{} => u := head :: !u
      | body' => let val clause = (head, ref (card body'))
		 in
		     h := clause :: !h;
		     iterate
		       if x inset !i
			   then let val r = ?(!i) x
				in
				    r := clause :: !r
				end
		       else i := !i ++ {x => ref [clause]}
		     | x in set body' (* normally, body, but this is more economical *)
		     end
		 end;

fun horn_solve (HORN (rh, ri as ref i, u, rhor)) =
    let fun unit_propagate x = (* make variable x true *)
	    if x inset !rhor
		then ()
	    else let val clauses = if x inset i
				       then !(?i x)
				   else nil
		 in
		     rhor := !rhor U {x};
		     iterate
		       (dec nr;
			if !nr=0
			    then u := head :: !u
			else ())
		     | (head, nr) in list clauses
		     end
		 end
	fun solve () =
	    case !u of
		head :: rest =>
		  (u := rest;
		   case head of
		       SOME x => (unit_propagate x; solve ())
		     | _ => raise HornSolveEvt)
	      |  _ => (rh := nil; (* to save memory *)
		       ri := {};
		       !rhor)
    in
	solve ()
    end;

fun horn_copy (HORN (_, _, ref nil, ref rho)) =
    HORN (ref nil, ref {}, ref nil, ref rho)
  | horn_copy _ = raise HornCopy;

