sig
  type predicate =
    Ast.Predicate.predicate =
      True
    | False
    | And of predicate list
    | Or of predicate list
    | Not of predicate
    | Implies of predicate * predicate
    | Iff of predicate * predicate
    | All of Ast.Symbol.symbol * predicate
    | Exist of Ast.Symbol.symbol * predicate
    | Atom of Ast.Expression.expression
  val normalize : predicate -> predicate
  val conjoinL : predicate list -> predicate
  val disjoinL : predicate list -> predicate
  val implies : predicate -> predicate -> predicate
  val iff : predicate -> predicate -> predicate
  val negate : predicate -> predicate
  val negateAtom : predicate -> predicate
  val convertDNF : predicate -> predicate
  val to_dnf : predicate -> predicate list
  val toString : predicate -> string
  val print : Format.formatter -> predicate -> unit
  val allVarExps : predicate -> Ast.Expression.expression list
  val allVarExps_deep : predicate -> Ast.Expression.lval list
  val getAtoms : predicate -> predicate list
  val map :
    (Ast.Symbol.symbol -> Ast.Symbol.symbol) ->
    ((Ast.Expression.lval -> bool) ->
     Ast.Expression.expression -> Ast.Expression.expression) ->
    predicate -> predicate
  val alpha_convert :
    (Ast.Expression.lval -> Ast.Expression.lval) -> predicate -> predicate
  val deep_alpha_convert :
    (Ast.Expression.lval -> Ast.Expression.expression) ->
    predicate -> predicate
  val substitute :
    (Ast.Expression.expression * Ast.Expression.expression) list ->
    predicate -> predicate
  val canonicize : predicate -> predicate
end