(* utility functions for sets of gclauses, 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 "gclause_h";

extern val range_restrict : (string * string * ''var gclause) list * string
	     * (int -> ''var) * string
	   -> (string * string * ''var gclause) list;
	   (* range_restrict (named_gcl, dompred, varname, defcst)
	    transforms input clause list named_gcl, as given by tptpparse,
	    into a similar list of range-restricted clauses that
	    is equi-satisfiable to the input.
	    May introduce a fresh "domain" predicate dompred, whose name
	    is given as second argument.
	    The theory of dompred is built through clauses whose variables
	    are generated using varname.  It is the collection of
	    (automata) clauses of the form dompred(f(X1,...,Xn)) :-
	    dompred(X1), ..., dompred(Xn), for each function f in
	    the signature.
	    If no function symbol in the input clause set has arity 0,
	    then the transformation does not preserve completeness.
	    To make sure it does, we may need to add a clause
	    dompred(a) for some added constant a: this is the defcst argument.
	    *)



(* TODO: detect variables that can only be mapped to finitely many terms. *)
