sig
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
method add_typ : Var.t -> Formula.typdef -> unit
method add_var : Var.t -> Formula.typ -> unit
method bddincr : int
method bddindex : int
method careset : Bdd.t
method cond : CondDD.DHashCond.t
method cond_of_idb : int * bool -> Formula.cond
method idcondvar : Var.t MappeI.t
method manager : Manager.t
method mem_typ : Var.t -> bool
method mem_var : Var.t -> bool
method print_external_idcondb : Format.formatter -> int * bool -> unit
method print_order : Format.formatter -> unit
method set_bddincr : int -> unit
method set_bddindex : int -> unit
method set_careset : Bdd.t -> unit
method set_idcondvar : Var.t MappeI.t -> unit
method set_print_external_idcondb :
(Format.formatter -> int * bool -> unit) -> unit
method set_typdef : Formula.typdef Var.Map.t -> unit
method set_varinfo : Bddvar.info Var.Map.t -> unit
method set_varset : Bdd.t Var.Map.t -> unit
method set_vartyp : Formula.typ Var.Map.t -> unit
method typ_of_var : Var.t -> Formula.typ
method typdef : Formula.typdef Var.Map.t
method typdef_of_typ : Var.t -> Formula.typdef
method var_of_idcond : int -> Var.t
method varinfo : Bddvar.info Var.Map.t
method varset : Bdd.t Var.Map.t
method vartyp : Formula.typ Var.Map.t
end
class make_db : Manager.t -> CondDD.db
val typ_of_expr : Formula.expr -> Formula.typ
val print_cond : Format.formatter -> Formula.cond -> unit
val print_typ : Format.formatter -> Formula.typ -> unit
val print_typdef : Format.formatter -> Formula.typdef -> unit
val print_expr : #db -> Format.formatter -> expr -> unit
val print_bdd : #db -> Format.formatter -> Bdd.t -> unit
val print_db : Format.formatter -> #Formula.db -> unit
module Bool :
sig
type t = Bdd.t
val of_expr : Formula.expr -> Formula.Bool.t
val to_expr : Formula.Bool.t -> Formula.expr
val dtrue : #Formula.db -> Formula.Bool.t
val dfalse : #Formula.db -> Formula.Bool.t
val of_bool : #Formula.db -> bool -> Formula.Bool.t
val var : #Formula.db -> Var.t -> Formula.Bool.t
val dnot : #Formula.db -> Formula.Bool.t -> Formula.Bool.t
val dand :
#Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
val dor :
#Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
val xor :
#Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
val nand :
#Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
val nor :
#Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
val nxor :
#Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
val eq :
#Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
val ite :
#Formula.db ->
Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
val is_included_in :
?sem:bool -> #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> bool
val is_inter_empty :
?sem:bool -> #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> bool
val exists :
?sem:bool ->
#Formula.db -> Var.t list -> Formula.Bool.t -> Formula.Bool.t
val forall :
?sem:bool ->
#Formula.db -> Var.t list -> Formula.Bool.t -> Formula.Bool.t
val print : #Formula.db -> Format.formatter -> Formula.Bool.t -> unit
end
module Bint :
sig
type t = Bddint.t
val of_expr : Formula.expr -> Formula.Bint.t
val to_expr : Formula.Bint.t -> Formula.expr
val of_int :
#Formula.db -> [> `Tbint of bool * int ] -> int -> Formula.Bint.t
val var : #Formula.db -> Var.t -> Formula.Bint.t
val neg : #Formula.db -> Formula.Bint.t -> Formula.Bint.t
val succ : #Formula.db -> Formula.Bint.t -> Formula.Bint.t
val pred : #Formula.db -> Formula.Bint.t -> Formula.Bint.t
val add :
#Formula.db -> Formula.Bint.t -> Formula.Bint.t -> Formula.Bint.t
val sub :
#Formula.db -> Formula.Bint.t -> Formula.Bint.t -> Formula.Bint.t
val shift_left : #Formula.db -> int -> Formula.Bint.t -> Formula.Bint.t
val shift_right :
#Formula.db -> int -> Formula.Bint.t -> Formula.Bint.t
val scale : #Formula.db -> int -> Formula.Bint.t -> Formula.Bint.t
val ite :
#Formula.db ->
Bdd.t -> Formula.Bint.t -> Formula.Bint.t -> Formula.Bint.t
val zero : #Formula.db -> Formula.Bint.t -> Bdd.t
val eq : #Formula.db -> Formula.Bint.t -> Formula.Bint.t -> Bdd.t
val eq_int : #Formula.db -> Formula.Bint.t -> int -> Bdd.t
val supeq : #Formula.db -> Formula.Bint.t -> Formula.Bint.t -> Bdd.t
val supeq_int : #Formula.db -> Formula.Bint.t -> int -> Bdd.t
val sup : #Formula.db -> Formula.Bint.t -> Formula.Bint.t -> Bdd.t
val print : #Formula.db -> Format.formatter -> Formula.Bint.t -> unit
end
module Benum :
sig
type t = Bddenum.t
val of_expr : Formula.expr -> Formula.Benum.t
val to_expr : Formula.Benum.t -> Formula.expr
val var : #Formula.db -> Var.t -> Formula.Benum.t
val ite :
#Formula.db ->
Bdd.t -> Formula.Benum.t -> Formula.Benum.t -> Formula.Benum.t
val eq : #Formula.db -> Formula.Benum.t -> Formula.Benum.t -> Bdd.t
val eq_label : #Formula.db -> Formula.Benum.t -> Var.t -> Bdd.t
val print : #Formula.db -> Format.formatter -> Formula.Benum.t -> unit
end
module Arith :
sig
type t = ArithDD.t
val of_expr : [> `Arith of Formula.Arith.t ] -> Formula.Arith.t
val to_expr : Formula.Arith.t -> [> `Arith of Formula.Arith.t ]
val var : #Formula.db -> Var.t -> Formula.Arith.t
val cst : Mpqf.t -> Formula.Arith.t
val add :
#Formula.db -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
val mul :
#Formula.db -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
val sub :
#Formula.db -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
val div :
#Formula.db -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
val gmod :
#Formula.db -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
val other :
#Formula.db -> Var.t -> Formula.Arith.t list -> Formula.Arith.t
val negate : #Formula.db -> Formula.Arith.t -> Formula.Arith.t
val ite :
#Formula.db ->
Bdd.t -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
val condition :
#Formula.db -> Arith.Condition.typ -> Formula.Arith.t -> Bdd.t
val supeq : #Formula.db -> Formula.Arith.t -> Bdd.t
val sup : #Formula.db -> Formula.Arith.t -> Bdd.t
val eq : #Formula.db -> Formula.Arith.t -> Bdd.t
val substitute_expr :
#Formula.db ->
Arith.expr ->
[> `Arith of Formula.Arith.t ] Var.Map.t -> Formula.Arith.t
val substitute_cond :
#Formula.db ->
Arith.Condition.t ->
[> `Arith of Formula.Arith.t ] Var.Map.t -> Bdd.t
val print : #Formula.db -> Format.formatter -> Formula.Arith.t -> unit
end
val eq : #Formula.db -> Formula.expr -> Formula.expr -> Formula.Bool.t
val ite :
#Formula.db ->
Formula.Bool.t -> Formula.expr -> Formula.expr -> Formula.expr
val compose_of_substitution :
#Formula.db ->
Formula.expr Var.Map.t -> Bdd.t array option * Formula.expr Var.Map.t
val substitute :
#Formula.db -> Formula.expr -> Formula.expr Var.Map.t -> Formula.expr
val var : #Formula.db -> Var.t -> Formula.expr
val cofactor : Formula.expr -> Bdd.t -> Formula.expr
val tdrestrict : Formula.expr -> Bdd.t -> Formula.expr
val support_cond : #Formula.db -> Formula.expr -> Bdd.t
val vectorsupport_cond : #Formula.db -> Formula.expr list -> Bdd.t
val support : #Formula.db -> Formula.expr -> Var.Set.t
val print_expr : #Formula.db -> Format.formatter -> Formula.expr -> unit
val print_bdd : #Formula.db -> Format.formatter -> Bdd.t -> unit
val cleanup : #Formula.db -> SetteI.t -> Formula.expr list -> unit
end