(*
 *	Copyright (c) 2002 by Laboratoire Spécification et Vérification (LSV),
 *	CNRS UMR 8643 & ENS Cachan.
 *	Written by Jean Goubault-Larrecq.  Not derived from licensed software.
 *
 *	Permission is granted to anyone to use this software for any
 *	purpose on any computer system, and to redistribute it freely,
 *	subject to the following restrictions:
 *
 *	1. Neither the author nor its employer is responsible for the consequences of use of
 *		this software, no matter how awful, even if they arise
 *		from defects in it.
 *
 *	2. The origin of this software must not be misrepresented, either
 *		by explicit claim or by omission.
 *
 *	3. Altered versions must be plainly marked as such, and must not
 *		be misrepresented as being the original software.
 *
 *	4. This software is restricted to non-commercial use only.  Commercial
 *		use is subject to a specific license, obtainable from LSV.
 *)

open Intervalle

(* Le domaine des intervalles flottants est un couple (itv, nan),
	ou itv est un intervalle decrivant les flottants possibles,
	et nan est un booleen qui est vrai si et seulement s'il
	est possible d'obtenir un NaN (not a number) comme valeur.
	Par exemple, 0.0/0.0 donne un NaN.  Par contre, 1.0/0.0
	done +inf, qui est un flottant valide dans la norme IEEE 754. *)

val itv_float_bot : itv * bool
	(* Le bottom du treillis des intervalles flottants:
	un intervalle vide, et pas de NaN. *)
val itv_float_top : itv * bool
	(* Le top du treillis des intervalles flottants. *)
val itv_float_union :
  itv * bool -> itv * bool -> itv * bool
	(* L'union dans le treillis. *)
val itv_float_widen :
  itv * bool -> itv * bool -> itv * bool
	(* L'elargissement dans le treillis. *)
val itv_float_equal : itv * bool -> itv * bool -> bool
	(* Teste si deux intervalles flottants sont les memes
	(designent les memes ensembles de flottants). *)
	
val itv_float_cst : Cparse.constant_val -> itv * bool
	(* convertit une constante en un intervalle flottant. *)
val itv_float_add :
  itv * bool -> itv * bool -> itv * bool
	(* L'addition. *)
val itv_float_minus : itv * bool -> itv * bool
	(* Le calcul de l'oppose. *)
val itv_float_sub :
  itv * bool -> itv * bool -> itv * bool
	(* La soustraction. *)
val itv_float_mul :
  itv * bool -> itv * bool -> itv * bool
	(* La multiplication. *)
val itv_float_div :
  itv * bool -> itv * bool -> itv * bool
	(* La division. *)
val itv_float_convert_int : itv -> itv * bool
	(* La convert d'entier vers flottant.
	En argument, un intervalle d'entiers; en sortie,
	un intervalle flottant. *)
val itv_float_le :
  itv * bool -> itv * bool -> itv
	(* La relation <=; retourne un intervalle d'entiers possibles
	(les tests C retournent 1 si vrai, 0 si faux). *)
val itv_float_lt :
  itv * bool -> itv * bool -> itv
	(* La relation <; retourne un intervalle d'entiers possibles
	(les tests C retournent 1 si vrai, 0 si faux). *)
val itv_float_eq :
  itv * bool -> itv * bool -> itv
	(* La relation =; retourne un intervalle d'entiers possibles
	(les tests C retournent 1 si vrai, 0 si faux). *)