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