sig
  type ast_type = string
  module Symbol :
    sig
      type symbol = string
      and t = Ast.Symbol.symbol
      val compare : Ast.Symbol.t -> Ast.Symbol.t -> int
      val toString : Ast.Symbol.symbol -> string
      val print : Format.formatter -> Ast.Symbol.symbol -> unit
    end
  module Constant :
    sig
      type constant =
          Int of int
        | Float of float
        | String of string
        | EnumC of int * string
      val toString : Ast.Constant.constant -> string
    end
  module Expression :
    sig
      type access_op = Dot | Arrow
      and assign_op =
          Assign
        | AssignBitAnd
        | AssignBitOr
        | AssignDiv
        | AssignLShift
        | AssignMinus
        | AssignMul
        | AssignPlus
        | AssignRem
        | AssignRShift
        | AssignXor
      and unary_op =
          UnaryMinus
        | Not
        | BitNot
        | Address
        | UnaryPlus
        | DestructorCall
        | Assume
        | Assert
        | PreInc
        | PreDec
        | PostInc
        | PostDec
      and binary_op =
          BitAnd
        | BitOr
        | Div
        | LShift
        | Minus
        | Mul
        | Plus
        | Rem
        | RShift
        | Xor
        | Eq
        | Ge
        | Gt
        | Le
        | Lt
        | Ne
        | Index
        | And
        | Or
        | Comma
        | FieldOffset
      and lval =
          Symbol of Ast.Symbol.symbol
        | Access of Ast.Expression.access_op * Ast.Expression.expression *
            Ast.Symbol.symbol
        | Dereference of Ast.Expression.expression
        | Indexed of Ast.Expression.expression * Ast.Expression.expression
      and expression =
          Lval of Ast.Expression.lval
        | Chlval of Ast.Expression.lval * string
        | Assignment of Ast.Expression.assign_op * Ast.Expression.lval *
            Ast.Expression.expression
        | Binary of Ast.Expression.binary_op * Ast.Expression.expression *
            Ast.Expression.expression
        | Cast of Ast.ast_type * Ast.Expression.expression
        | Constant of Ast.Constant.constant
        | Constructor of Ast.Symbol.symbol * Ast.ast_type
        | FunctionCall of Ast.Expression.expression *
            Ast.Expression.expression list
        | Sizeof of int
        | Unary of Ast.Expression.unary_op * Ast.Expression.expression
      and t = Ast.Expression.expression
      val compare : Ast.Expression.t -> Ast.Expression.t -> int
      val unaryOpToString : Ast.Expression.unary_op -> string
      val unaryOpToVanillaString : Ast.Expression.unary_op -> string
      val assignOpToString : Ast.Expression.assign_op -> string
      val accessOpToString : Ast.Expression.access_op -> string
      val binaryOpToString : Ast.Expression.binary_op -> string
      val binaryOpToVanillaString : Ast.Expression.binary_op -> string
      val print : Format.formatter -> Ast.Expression.expression -> unit
      val print_lval : Format.formatter -> Ast.Expression.lval -> unit
      val toString : Ast.Expression.expression -> string
      val lvalToString : Ast.Expression.lval -> string
      val addressOf : Ast.Expression.expression -> Ast.Expression.expression
      val replaceChlvals :
        Ast.Expression.expression -> Ast.Expression.expression
      val isRelOp : Ast.Expression.binary_op -> bool
      val isDeref : Ast.Expression.expression -> bool
      val push_deref : Ast.Expression.lval -> Ast.Expression.lval
      val derefedVar : Ast.Expression.lval -> Ast.Expression.expression
      val getParents :
        Ast.Expression.lval list -> Ast.Expression.expression list
      val allVarExps :
        Ast.Expression.expression -> Ast.Expression.expression list
      val negateRel : Ast.Expression.expression -> Ast.Expression.expression
      val fresh_lval : Ast.Expression.lval -> Ast.Expression.expression
      val alpha_convert :
        (Ast.Expression.lval -> Ast.Expression.lval) ->
        Ast.Expression.expression -> Ast.Expression.expression
      val alpha_convert_lval :
        (Ast.Expression.lval -> Ast.Expression.lval) ->
        Ast.Expression.lval -> Ast.Expression.lval
      val deep_alpha_convert :
        (Ast.Expression.lval -> Ast.Expression.expression) ->
        Ast.Expression.expression -> Ast.Expression.expression
      val substituteExpression :
        (Ast.Expression.expression * Ast.Expression.expression) list ->
        Ast.Expression.expression -> Ast.Expression.expression
      val assignments_of_expression :
        Ast.Expression.expression ->
        (Ast.Expression.expression * Ast.Expression.expression) list
    end
  module Predicate :
    sig
      type predicate =
          True
        | False
        | And of Ast.Predicate.predicate list
        | Or of Ast.Predicate.predicate list
        | Not of Ast.Predicate.predicate
        | Implies of Ast.Predicate.predicate * Ast.Predicate.predicate
        | Iff of Ast.Predicate.predicate * Ast.Predicate.predicate
        | All of Ast.Symbol.symbol * Ast.Predicate.predicate
        | Exist of Ast.Symbol.symbol * Ast.Predicate.predicate
        | Atom of Ast.Expression.expression
      val normalize : Ast.Predicate.predicate -> Ast.Predicate.predicate
      val conjoinL : Ast.Predicate.predicate list -> Ast.Predicate.predicate
      val disjoinL : Ast.Predicate.predicate list -> Ast.Predicate.predicate
      val implies :
        Ast.Predicate.predicate ->
        Ast.Predicate.predicate -> Ast.Predicate.predicate
      val iff :
        Ast.Predicate.predicate ->
        Ast.Predicate.predicate -> Ast.Predicate.predicate
      val negate : Ast.Predicate.predicate -> Ast.Predicate.predicate
      val negateAtom : Ast.Predicate.predicate -> Ast.Predicate.predicate
      val convertDNF : Ast.Predicate.predicate -> Ast.Predicate.predicate
      val to_dnf : Ast.Predicate.predicate -> Ast.Predicate.predicate list
      val toString : Ast.Predicate.predicate -> string
      val print : Format.formatter -> Ast.Predicate.predicate -> unit
      val allVarExps :
        Ast.Predicate.predicate -> Ast.Expression.expression list
      val allVarExps_deep :
        Ast.Predicate.predicate -> Ast.Expression.lval list
      val getAtoms : Ast.Predicate.predicate -> Ast.Predicate.predicate list
      val map :
        (Ast.Symbol.symbol -> Ast.Symbol.symbol) ->
        ((Ast.Expression.lval -> bool) ->
         Ast.Expression.expression -> Ast.Expression.expression) ->
        Ast.Predicate.predicate -> Ast.Predicate.predicate
      val alpha_convert :
        (Ast.Expression.lval -> Ast.Expression.lval) ->
        Ast.Predicate.predicate -> Ast.Predicate.predicate
      val deep_alpha_convert :
        (Ast.Expression.lval -> Ast.Expression.expression) ->
        Ast.Predicate.predicate -> Ast.Predicate.predicate
      val substitute :
        (Ast.Expression.expression * Ast.Expression.expression) list ->
        Ast.Predicate.predicate -> Ast.Predicate.predicate
      val canonicize : Ast.Predicate.predicate -> Ast.Predicate.predicate
    end
end