summaryrefslogblamecommitdiff
path: root/abstract/num_domain.ml
blob: a91c69fca28a79249cfa076961fdc82f18062a07 (plain) (tree)
1
2
3
4
5
6
7
8
9


            




                                                            
                                              
          
            

                      


                                                                         
                               
                               

                             
                                           

                                                                                
                                    
 








                                                          
                            

                                             

                                                    
                         
                                                   
                                                              
                                                     


   
open Ast
open Formula

(*
  Interface specification for a numerical environment domain
  (relationnal with Apron or nonrelationnal with intervals)
*)

module type NUMERICAL_ENVIRONMENT_DOMAIN = sig
    type t
    type itv

    (* construction *)
    val top         : (id * bool) list -> t
    val bottom      : (id * bool) list -> t
    val vbottom     : t -> t       (* bottom value with same variables *)
    val is_bot      : t -> bool
    val is_top      : t -> bool

    (* variable management *)
    val vars        : t -> (id * bool) list

    val forgetvar   : t -> id -> t             (* remove var from constraints *)
    val project     : t -> id -> itv

    (* set-theoretic operations *)
    val join        : t -> t -> t       (* union *)
    val meet        : t -> t -> t       (* intersection *)
    val widen       : t -> t -> t

    (* order *)
    val subset      : t -> t -> bool
    val eq          : t -> t -> bool

    (* abstract operation *)
    val apply_cons  : t -> num_cons -> t
    val apply_cl    : t -> num_cons list -> t
    val assign      : t -> (id * num_expr) list -> t

    (* pretty-printing *)
    val print       : Format.formatter -> t -> unit
    val print_vars  : Format.formatter -> t -> id list -> unit
    val print_itv   : Format.formatter -> itv -> unit
end