Module Formula

module Formula: sig .. end

Boolean expressions

type cond = CondDD.cond 

type typ = CondDD.typ 

type typdef = CondDD.typdef 

type expr = [ `Arith of ArithDD.t
       | `Benum of Bddenum.t
       | `Bint of Bddint.t
       | `Bool of Bdd.t ] 

type leaf = [ `Arith of Arith.expr ] 

class type db = object .. end

class make_db : Manager.t -> CondDD.db

val typ_of_expr : expr -> typ

val print_cond : Format.formatter -> cond -> unit

val print_typ : Format.formatter -> typ -> unit

val print_typdef : Format.formatter -> typdef -> unit

val print_expr : #db -> Format.formatter -> expr -> unit

val print_bdd : #db -> Format.formatter -> Bdd.t -> unit

val print_db : Format.formatter -> #db -> unit

module Bool: sig .. end

module Bint: sig .. end

module Benum: sig .. end

module Arith: sig .. end

val eq : #db -> expr -> expr -> Bool.t

val ite : #db -> Bool.t -> expr -> expr -> expr

val compose_of_substitution : #db ->
       expr Var.Map.t -> Bdd.t array option * expr Var.Map.t

val substitute : #db -> expr -> expr Var.Map.t -> expr

val var : #db -> Var.t -> expr

val cofactor : expr -> Bdd.t -> expr

val tdrestrict : expr -> Bdd.t -> expr

val support_cond : #db -> expr -> Bdd.t

val vectorsupport_cond : #db -> expr list -> Bdd.t

val support : #db -> expr -> Var.Set.t

val print_expr : #db -> Format.formatter -> expr -> unit

val print_bdd : #db -> Format.formatter -> Bdd.t -> unit

val cleanup : #db -> SetteI.t -> expr list -> unit