sig
  val s_bool : Lang.F.term -> Lang.F.term list
  val s_cnf_ite :
    Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term list
  val s_dnf_ite :
    Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term list
  val s_cnf_iff : Lang.F.term -> Lang.F.term -> Lang.F.term list
  val s_dnf_iff : Lang.F.term -> Lang.F.term -> Lang.F.term list
  val s_cnf_xor : Lang.F.term -> Lang.F.term -> Lang.F.term list
  val s_dnf_xor : Lang.F.term -> Lang.F.term -> Lang.F.term list
  val is_cnf : Lang.F.term -> bool
  val e_cnf : ?depth:int -> Lang.F.term -> Lang.F.term
  val is_dnf : Lang.F.term -> bool
  val e_dnf : ?depth:int -> Lang.F.term -> Lang.F.term
end