blob: a91c69fca28a79249cfa076961fdc82f18062a07 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
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
|
