bddd.mli 1.09 KB
Newer Older
1
(*-----------------------------------------------------------------------
2
** Copyright (C) - Verimag.
3 4 5 6 7 8 9 10
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
** File: bddd.mli
** Main author: jahier@imag.fr
*)

11 12
(** Bdd Drawer. *)

13
(** Machinery to perform a draw in a bdd (hence the third d ...) *)
14 15


16
type sol_nb = float
17

18

19 20 21 22 23
val draw_in_bdd : Var.env_in -> Env_state.t -> Exp.var list -> Bdd.t ->
  Bdd.t -> Var.subst list * Store.t' * Store.p
(** [draw_in_bdd inputs state vars bdd comb] returns a draw of the
  Boolean variables as well as a range based and a polyhedron based
  representation of numeric constraints.
24 25 26
*)

val sol_number : Bdd.t -> sol_nb * sol_nb
27
(** Returns the solution number in the then and else branches of the bdd *)
28 29 30 31

(**/**)


32 33 34 35 36 37 38 39 40 41 42
val add_snt_entry : Bdd.t -> sol_nb * sol_nb -> unit
(** mofifies an entry. usefull whenever we realize latter that a bdd
 represents a formula that is unsatifiable for numerical reasons. *)


val init_snt : unit -> unit
val clear_snt : unit -> unit