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