(* h1fi finite model finder engine, headers.
   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 "cc_h";
open "gclause_h";
open "auto_h";

exception ForceContradictionEvt;
exception ForceNonHornEvt;

type ''var cenv = ''var -m> ''var color; (* color environments: map variables to colors. *)

type (''var, 'a) policy =
     (''var, 'a) cc * (''var term * ''var term * ''var cenv -> bool)
     -> ''var gclause * ''var term * ''var cenv -> unit;
(* A policy p is called on (cc, eq) and (gc,a,rho), where the term a
 is in fact an atom P(u1,...,un), and should be the head of clause gc.
 It is meant to find terms v1, ..., vn already in D such that we already knew
 P(v1,...,vn)=$true in cc.  Then it equates each ui with vi under
 substitution, using the function eq (which returns true iff ui rho
 was not already equal to vi rho).
 It can also decide to equate nothing.
*)

extern val herbrand_policy : (''var, 'a) policy;
(* The Herbrand policy does not equate any term.
 Named so because then the forcers below will gradually
 build a (possibly infinite) Herbrand model. *)

extern val make_pred_policy : (''_var -> bool) -> (''_var, '_a) policy;
(* The Pred policy make_pred_policy(special_var)
 works by storing which atoms P(v1,...,vn)
 it was already asked to force to true, for each clause gc.
 Whenever it is asked to force P(u1 rho,...,un rho) to true for some
 clause gc, it will equate ui rho=vi for each i, provided some
 atom P(v1,...,vn) was already stored that was created with the
 same values of the variables x such that special_var x is true.
 In the extreme case that special_var is always false, creates
 at most one true atom P(u1,...,un) for each tuple of colors
 of u1, ..., un.
*)

extern val make_heam_policy : (''_var -> bool) -> (''_var, '_a) policy;
(* The Heam policy make_heam_policy(special_var)
 works by storing which atoms P(v1,...,vn)
 it was already asked to force to true, for each clause gc.
 Whenever it is asked to force P(u1 rho,...,un rho) to true for some
 clause gc, it will equate ui rho=vi for each i, provided some
 atom P(v1,...,vn) (with the same P, for the same clause gc,
 and for the same values of rho(x), where x ranges over the
 variables such that special_var x is true) was stored.
 In the extreme case where special_var x is always false,
 this forces ui rho=vi independently of rho.
 After an idea by Pierre-Cyril Heam implemented in Thomas Genet's Timbuk.
*)
 

extern val forcers : (''_var, '_a) cc * (''_var, '_a) policy * (''_var -> string) ->
	   |[force_term_value : ''_var term * ''_var color -> ''_var cenv set,
	     force_gclause : ''_var gclause -> unit
	     ]|;

(* forcers (cc,policy, vars) [where vars is meant for printing variables,
   in verbose mode]
   returns a record of functions:
 - force_term_value (t, d)
   returns all variable environments that will make t
   have value d (d in D);
- force_gclause (gc)
   computes all variable environments that will make
   the body of the gclause gc true.
   gc should be range-restricted (see gclauseutils.ml),
   otherwise the procedure will be wrong.
   If gc is not Horn, will raise ForceNonHornEvt.
   If body can be made true but gc has no head, then raises ForceContradictionEvt.
   Otherwise, will install new equalities into congruence closure structure
   so as to arrange for head to be true.
   If head is equal(u,v), then this will install the two equations
   "u=v" and "equal(u,v)=$true".
   If head is of the form P(u1,...,un) (P!=equal), then this will
   install the equation "P(u1,...,un)=$true" at least.  In general,
   the policy will try to equate u1 with v1, ..., un with vn,
   for some v1, ..., vn already in D such that we already knew
   P(v1,...,vn)=$true.
 *)

extern val auto_from_cc : (''_var, '_a) cc * string -> automaton;
 (* auto_from_cc (cc, q) produce equivalent (non-deterministic,
   and even almost deterministic) automaton from cc.
  q is used to create names for fresh states.
  *)
