(* Propositional Horn satisfiability engine, 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.
*)

extern datatype ''a horn_set;

extern val new_horn_set : unit -> ''_a horn_set;
extern val add_horn_clause : ''_a horn_set * ''_a option * ''_a set -> unit;
	   (* add_horn_clause (hs, head, body) adds the clause
	    head :- body to set hs.
	    head=NONE means false; otherwise head=SOME x means head is variable x;
	    body is set of variables in body. *)
exception HornSolveEvt;
extern val horn_solve : ''_a horn_set -> ''_a set;
	   (* find smallest model, as set of true variables, of horn set
	    in argument.
	    If no model exists, then raises HornSolveEvt.
	    This may be used in alternation with add_horn_clause,
	    *)

exception HornCopy;

extern val horn_copy : ''_a horn_set -> ''_a horn_set;
	   (* copy a horn_set, which must have gone through
	    horn_solve first.
	    Otherwise, raises HornCopy. *)
