sig
  type 'a t
  val pp : Format.formatter -> 'a Wedge.t -> unit
  val show : 'a Wedge.t -> string
  val join :
    ?integrity:('a Syntax.formula -> unit) ->
    'a Wedge.t -> 'a Wedge.t -> 'a Wedge.t
  val meet : 'a Wedge.t -> 'a Wedge.t -> 'a Wedge.t
  val meet_atoms : 'a Wedge.t -> 'a Syntax.formula list -> unit
  val equal : 'a Wedge.t -> 'a Wedge.t -> bool
  val widen : 'a Wedge.t -> 'a Wedge.t -> 'a Wedge.t
  val of_atoms : 'a Syntax.context -> 'a Syntax.formula list -> 'a Wedge.t
  val to_atoms : 'a Wedge.t -> 'a Syntax.formula list
  val to_formula : 'a Wedge.t -> 'a Syntax.formula
  val exists :
    ?integrity:('a Syntax.formula -> unit) ->
    ?subterm:(Syntax.symbol -> bool) ->
    (Syntax.symbol -> bool) -> 'a Wedge.t -> 'a Wedge.t
  val top : 'a Syntax.context -> 'a Wedge.t
  val bottom : 'a Syntax.context -> 'a Wedge.t
  val is_bottom : 'a Wedge.t -> bool
  val is_top : 'a Wedge.t -> bool
  val farkas_equalities :
    'a Wedge.t -> ('a Syntax.term * Linear.QQVector.t) list
  val symbolic_bounds :
    'a Wedge.t -> Syntax.symbol -> 'a Syntax.term list * 'a Syntax.term list
  val bounds : 'a Wedge.t -> 'a Syntax.term -> Interval.t
  val ensure_nonlinear_symbols : 'a Syntax.context -> unit
  val ensure_min_max : 'a Syntax.context -> unit
  val abstract :
    ?exists:(Syntax.symbol -> bool) ->
    ?subterm:(Syntax.symbol -> bool) ->
    'a Syntax.context -> 'a Syntax.formula -> 'a Wedge.t
  val is_sat :
    'a Syntax.context -> 'a Syntax.formula -> [ `Sat | `Unknown | `Unsat ]
  val symbolic_bounds_formula :
    ?exists:(Syntax.symbol -> bool) ->
    'a Syntax.context ->
    'a Syntax.formula ->
    Syntax.symbol ->
    [ `Sat of 'a Syntax.term option * 'a Syntax.term option | `Unsat ]
  val coordinate_system : 'a Wedge.t -> 'a CoordinateSystem.t
  val polyhedron : 'a Wedge.t -> ([ `Eq | `Geq ] * Linear.QQVector.t) list
  val vanishing_ideal : 'a Wedge.t -> Polynomial.Mvp.t list
  val copy : 'a Wedge.t -> 'a Wedge.t
  val equational_saturation :
    ?integrity:('a Syntax.formula -> unit) ->
    'a Wedge.t -> Polynomial.Rewrite.t
  val strengthen :
    ?integrity:('a Syntax.formula -> unit) -> 'a Wedge.t -> unit
end