sig
module type PreDomain =
sig
type 'a t
val pp : Format.formatter -> 'a Iteration.PreDomain.t -> unit
val show : 'a Iteration.PreDomain.t -> string
val closure : 'a Iteration.PreDomain.t -> 'a Syntax.formula
val join :
'a Iteration.PreDomain.t ->
'a Iteration.PreDomain.t -> 'a Iteration.PreDomain.t
val widen :
'a Iteration.PreDomain.t ->
'a Iteration.PreDomain.t -> 'a Iteration.PreDomain.t
val equal :
'a Iteration.PreDomain.t -> 'a Iteration.PreDomain.t -> bool
val tr_symbols :
'a Iteration.PreDomain.t -> (Syntax.symbol * Syntax.symbol) list
end
module type Domain =
sig
type 'a t
val pp : Format.formatter -> 'a t -> unit
val show : 'a t -> string
val closure : 'a t -> 'a Syntax.formula
val join : 'a t -> 'a t -> 'a t
val widen : 'a t -> 'a t -> 'a t
val equal : 'a t -> 'a t -> bool
val tr_symbols : 'a t -> (Syntax.symbol * Syntax.symbol) list
val abstract_iter :
?exists:(Syntax.symbol -> bool) ->
'a Syntax.context ->
'a Syntax.formula -> (Syntax.symbol * Syntax.symbol) list -> 'a t
end
module type DomainPlus =
sig
type 'a t
val pp : Format.formatter -> 'a t -> unit
val show : 'a t -> string
val closure : 'a t -> 'a Syntax.formula
val join : 'a t -> 'a t -> 'a t
val widen : 'a t -> 'a t -> 'a t
val equal : 'a t -> 'a t -> bool
val tr_symbols : 'a t -> (Syntax.symbol * Syntax.symbol) list
val abstract_iter :
?exists:(Syntax.symbol -> bool) ->
'a Syntax.context ->
'a Syntax.formula -> (Syntax.symbol * Syntax.symbol) list -> 'a t
val closure_plus : 'a t -> 'a Syntax.formula
end
module WedgeVector : DomainPlus
module WedgeVectorOCRS : DomainPlus
module WedgeMatrix : DomainPlus
module Split : functor (Iter : DomainPlus) -> Domain
module Sum :
functor (A : PreDomain) (B : PreDomain) ->
sig
type 'a t
val pp : Format.formatter -> 'a t -> unit
val show : 'a t -> string
val closure : 'a t -> 'a Syntax.formula
val join : 'a t -> 'a t -> 'a t
val widen : 'a t -> 'a t -> 'a t
val equal : 'a t -> 'a t -> bool
val tr_symbols : 'a t -> (Syntax.symbol * Syntax.symbol) list
val left : 'a A.t -> 'a t
val right : 'a B.t -> 'a t
end
end