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 ] 

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