Module CondDD


module CondDD: sig .. end

Utility functions



type typ = [ `Benum of Var.t | `Bint of bool * int | `Bool | `Int | `Real ] 
type typdef = Bddvar.typdef 
type cond = [ `Arith of Arith.Condition.t ] 

type ('a, 'b) ddexpr =
| Leaf of 'a
| Mtbdd of 'b
module HashCond: Hashhe.S  with type key = cond
module DHashCond: DHashhe.S  with module HashX=HashCond
			      and module HashY=HashheIB
class type db = object .. end
class make_db : Manager.t -> db
val print_cond : Format.formatter -> cond -> unit
val print_typ : Format.formatter -> typ -> unit
val print_typdef : Format.formatter -> typdef -> unit
val print_db : Format.formatter -> #db -> unit
val cond_support : cond -> Var.Set.t
val condition : leaf_of_id:(int -> 'a) ->
cond_of_leaf:('a -> [ `Arith of Arith.Condition.t | `Bool of bool ]) ->
#db -> ('a, 'b) ddexpr -> Bdd.t
val substitute_ddexpr : substitute_leaf:((#db as 'a) ->
'b -> 'c Var.Map.t -> ('b, 'd) ddexpr) ->
guardleafs:('d -> (Bdd.t * 'b) array) ->
ite:('a ->
Bdd.t ->
('b, 'd) ddexpr ->
('b, 'd) ddexpr -> ('b, 'd) ddexpr) ->
'a ->
('b, 'd) ddexpr ->
Bdd.t array option -> 'c Var.Map.t -> ('b, 'd) ddexpr
val compute_careset : #db -> unit