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